Theorem: MyNat.le_antisymm (TheoremProvingLean/inductive_types.lean)

State before:
a b : Nat
hab : a ≤ b
hba : b ≤ a
⊢ a = b
Tactic:
cases hab with
| intro w hw =>
  cases hba with
    | intro z hz =>
      rw [hz] at hw
      have hw1 : b + z + w = b := Eq.symm hw
      rw [add_assoc] at hw1
      have hzw : z + w = 0 := eq_zero_of_add_right_eq_self hw1
      have hzz : z = 0 := add_right_eq_zero hzw
      rw [hzz] at hz
      assumption
State after:
no goals

State before:
case intro
a b : Nat
hba : b ≤ a
w : Nat
hw : b = a + w
⊢ a = b
Tactic:
cases hba with
  | intro z hz =>
    rw [hz] at hw
    have hw1 : b + z + w = b := Eq.symm hw
    rw [add_assoc] at hw1
    have hzw : z + w = 0 := eq_zero_of_add_right_eq_self hw1
    have hzz : z = 0 := add_right_eq_zero hzw
    rw [hzz] at hz
    assumption
State after:
no goals

State before:
case intro.intro
a b w : Nat
hw : b = a + w
z : Nat
hz : a = b + z
⊢ a = b
Tactic:
rw [hz] at hw
State after:
case intro.intro
a b w z : Nat
hw : b = b + z + w
hz : a = b + z
⊢ a = b

State before:
case intro.intro
a b w z : Nat
hw : b = b + z + w
hz : a = b + z
⊢ a = b
Tactic:
have hw1 : b + z + w = b := Eq.symm hw
State after:
case intro.intro
a b w z : Nat
hw : b = b + z + w
hz : a = b + z
hw1 : b + z + w = b
⊢ a = b

State before:
case intro.intro
a b w z : Nat
hw : b = b + z + w
hz : a = b + z
hw1 : b + z + w = b
⊢ a = b
Tactic:
rw [add_assoc] at hw1
State after:
case intro.intro
a b w z : Nat
hw : b = b + z + w
hz : a = b + z
hw1 : b + (z + w) = b
⊢ a = b

State before:
case intro.intro
a b w z : Nat
hw : b = b + z + w
hz : a = b + z
hw1 : b + (z + w) = b
⊢ a = b
Tactic:
have hzw : z + w = 0 := eq_zero_of_add_right_eq_self hw1
State after:
case intro.intro
a b w z : Nat
hw : b = b + z + w
hz : a = b + z
hw1 : b + (z + w) = b
hzw : z + w = 0
⊢ a = b

State before:
case intro.intro
a b w z : Nat
hw : b = b + z + w
hz : a = b + z
hw1 : b + (z + w) = b
hzw : z + w = 0
⊢ a = b
Tactic:
have hzz : z = 0 := add_right_eq_zero hzw
State after:
case intro.intro
a b w z : Nat
hw : b = b + z + w
hz : a = b + z
hw1 : b + (z + w) = b
hzw : z + w = 0
hzz : z = 0
⊢ a = b

State before:
case intro.intro
a b w z : Nat
hw : b = b + z + w
hz : a = b + z
hw1 : b + (z + w) = b
hzw : z + w = 0
hzz : z = 0
⊢ a = b
Tactic:
rw [hzz] at hz
State after:
case intro.intro
a b w z : Nat
hw : b = b + z + w
hz : a = b + 0
hw1 : b + (z + w) = b
hzw : z + w = 0
hzz : z = 0
⊢ a = b

State before:
case intro.intro
a b w z : Nat
hw : b = b + z + w
hz : a = b + 0
hw1 : b + (z + w) = b
hzw : z + w = 0
hzz : z = 0
⊢ a = b
Tactic:
assumption
State after:
no goals