-- -- https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Mechanics.20of.20Proof.201.2E3.2E11.20exercise.2015
import Mathlib

-- -- https://hrmacbeth.github.io/math2001/01_Proofs_by_Calculation.html#id29
example {x y : ℝ} (h1 : x + 3 = 5) (h2 : 2 * x - y * x = 0) : y = 2 :=
  calc
    y = 0 / x + y := by
Goals accomplished! 🐙 ring
Goals accomplished! 🐙
    
_: ℝ
_ = (
2: ℝ
2 * 
x: ℝ
x - 
y: ℝ
y * 
x: ℝ
x) / 
x: ℝ
x + 
y: ℝ
y := by
Goals accomplished! 🐙 rw [
x, y: ℝ
h1: x + 3 = 5
h2: 2 * x - y * x = 0
0 / x + y = (2 * x - y * x) / x + y
h2: 2 * x - y * x = 0
h2
x, y: ℝ
h1: x + 3 = 5
h2: 2 * x - y * x = 0
0 / x + y = 0 / x + y]
Goals accomplished! 🐙
    
_: ℝ
_ = ((
2: ℝ
2 - 
y: ℝ
y) * (
x: ℝ
x + 
3: ℝ
3 - 
3: ℝ
3)) / 
x: ℝ
x + 
y: ℝ
y := by
Goals accomplished! 🐙 ring
Goals accomplished! 🐙
    
_: ℝ
_ = ((
2: ℝ
2 - 
y: ℝ
y) * (
5: ℝ
5 - 
3: ℝ
3)) / 
x: ℝ
x + 
y: ℝ
y := by
Goals accomplished! 🐙 rw [
x, y: ℝ
h1: x + 3 = 5
h2: 2 * x - y * x = 0
(2 - y) * (x + 3 - 3) / x + y = (2 - y) * (5 - 3) / x + y
h1: x + 3 = 5
h1
x, y: ℝ
h1: x + 3 = 5
h2: 2 * x - y * x = 0
(2 - y) * (5 - 3) / x + y = (2 - y) * (5 - 3) / x + y]
Goals accomplished! 🐙
    
_: ℝ
_ = (
2: ℝ
2 - 
y: ℝ
y) * 
2: ℝ
2 / 
x: ℝ
x + 
y: ℝ
y := by
Goals accomplished! 🐙 ring
Goals accomplished! 🐙
    
_: ℝ
_ = (
2: ℝ
2 - 
y: ℝ
y) * 
2: ℝ
2 / (
x: ℝ
x + 
3: ℝ
3 - 
3: ℝ
3) + 
y: ℝ
y := by
Goals accomplished! 🐙 ring
Goals accomplished! 🐙
    
_: ℝ
_ = (
2: ℝ
2 - 
y: ℝ
y) * 
2: ℝ
2 / (
5: ℝ
5 - 
3: ℝ
3) + 
y: ℝ
y := by
Goals accomplished! 🐙 rw [
x, y: ℝ
h1: x + 3 = 5
h2: 2 * x - y * x = 0
(2 - y) * 2 / (x + 3 - 3) + y = (2 - y) * 2 / (5 - 3) + y
h1: x + 3 = 5
h1
x, y: ℝ
h1: x + 3 = 5
h2: 2 * x - y * x = 0
(2 - y) * 2 / (5 - 3) + y = (2 - y) * 2 / (5 - 3) + y]
Goals accomplished! 🐙
    
_: ℝ
_ = (
2: ℝ
2 - 
y: ℝ
y) + 
y: ℝ
y := by
Goals accomplished! 🐙 ring
Goals accomplished! 🐙
    
_: ℝ
_ = 
2: ℝ
2 := by
Goals accomplished! 🐙 ring
Goals accomplished! 🐙

example: 6 = 3 + 3
example : 
6: ℕ
6 = 
3: ℕ
3 + 
3: ℕ
3 := by
Goals accomplished! 🐙
  have 
h: 6 = 2 + 4
h : 
6: ℕ
6 = 
2: ℕ
2 + 
4: ℕ
4 :=
6 = 3 + 3 by
Goals accomplished! 🐙
    calc
      
6: ℕ
6 = 
1: ℕ
1 + 
5: ℕ
5 :=
6 = 2 + 4 by
Goals accomplished! 🐙 rw [
6 = 1 + 5
Nat.one_add: ∀ (n : ℕ), 1 + n = n.succ
Nat.one_add
6 = Nat.succ 5]
Goals accomplished! 🐙
      
_: ℕ
_: ℕ
_ = 
2: ℕ
2 + 
4: ℕ
4 :=
6 = 2 + 4 by
Goals accomplished! 🐙 rw [
1 + 5 = 2 + 4@
Nat.add_right_cancel_iff: ∀ {m k n : ℕ}, m + n = k + n ↔ m = k
Nat.add_right_cancel_iff
1 = 1]
Goals accomplished! 🐙
      
_: ℕ
_: ℕ
_ = 
3: ℕ
3 + 
3: ℕ
3 :=
6 = 2 + 4 by
Goals accomplished! 🐙 rw [
2 + 4 = 3 + 3@
Nat.add_right_cancel_iff: ∀ {m k n : ℕ}, m + n = k + n ↔ m = k
Nat.add_right_cancel_iff
2 = 2]
Goals accomplished! 🐙
  exact 
h: 6 = 2 + 4
h
Goals accomplished! 🐙
  done
Warning: 'done' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`
Goals accomplished! 🐙