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

State before:
a b c : Nat
ha : a ≠ zero
⊢ a * b = a * c → b = c
Tactic:
revert c
State after:
a b : Nat
ha : a ≠ zero
⊢ ∀ (c : Nat), a * b = a * c → b = c

State before:
a b : Nat
ha : a ≠ zero
⊢ ∀ (c : Nat), a * b = a * c → b = c
Tactic:
induction b with
| zero =>
  intro c h
  rw [mul_zero] at h
  apply Eq.symm
  show c = 0
  cases eq_zero_or_eq_zero_of_mul_eq_zero (Eq.symm h) with
  | inl ha0 => contradiction
  | inr hc0 => assumption
| succ b' ihb =>
  intro
  | zero =>
    intro h
    rw [mul_zero] at h
    cases eq_zero_or_eq_zero_of_mul_eq_zero h with
    | inl ha => contradiction
    | inr hb => assumption  | succ c' =>
    intro h
    apply succ_eq_succ_of_eq
    show b' = c'
    rw [mul_succ, mul_succ] at h
    have habax : a*b' = a*c' := add_right_cancel h
    have ihbc : a*b' = a*c' → b' = c' := ihb c'
    apply ihbc
    exact habax
State after:
no goals

State before:
case zero
a : Nat
ha : a ≠ zero
⊢ ∀ (c : Nat), a * zero = a * c → zero = c
Tactic:
intro c h
State after:
case zero
a : Nat
ha : a ≠ zero
c : Nat
h : a * zero = a * c
⊢ zero = c

State before:
case zero
a : Nat
ha : a ≠ zero
c : Nat
h : a * zero = a * c
⊢ zero = c
Tactic:
rw [mul_zero] at h
State after:
case zero
a : Nat
ha : a ≠ zero
c : Nat
h : zero = a * c
⊢ zero = c

State before:
case zero
a : Nat
ha : a ≠ zero
c : Nat
h : zero = a * c
⊢ zero = c
Tactic:
apply Eq.symm
State after:
case zero.h
a : Nat
ha : a ≠ zero
c : Nat
h : zero = a * c
⊢ c = zero

State before:
case zero.h
a : Nat
ha : a ≠ zero
c : Nat
h : zero = a * c
⊢ c = zero
Tactic:
show c = 0
State after:
case zero.h
a : Nat
ha : a ≠ zero
c : Nat
h : zero = a * c
⊢ c = 0

State before:
case zero.h
a : Nat
ha : a ≠ zero
c : Nat
h : zero = a * c
⊢ c = 0
Tactic:
cases eq_zero_or_eq_zero_of_mul_eq_zero (Eq.symm h) with
| inl ha0 => contradiction
| inr hc0 => assumption
State after:
no goals

State before:
case zero.h.inl
a : Nat
ha : a ≠ zero
c : Nat
h : zero = a * c
ha0 : a = 0
⊢ c = 0
Tactic:
contradiction
State after:
no goals

State before:
case zero.h.inr
a : Nat
ha : a ≠ zero
c : Nat
h : zero = a * c
hc0 : c = 0
⊢ c = 0
Tactic:
assumption
State after:
no goals

State before:
case succ
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
⊢ ∀ (c : Nat), a * succ b' = a * c → succ b' = c
Tactic:
intro
| zero =>
  intro h
  rw [mul_zero] at h
  cases eq_zero_or_eq_zero_of_mul_eq_zero h with
  | inl ha => contradiction
  | inr hb => assumption  | succ c' =>
  intro h
  apply succ_eq_succ_of_eq
  show b' = c'
  rw [mul_succ, mul_succ] at h
  have habax : a*b' = a*c' := add_right_cancel h
  have ihbc : a*b' = a*c' → b' = c' := ihb c'
  apply ihbc
  exact habax
State after:
no goals

State before:
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ : Nat
⊢ a * succ b' = a * zero → succ b' = zero
Tactic:
intro h
State after:
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ : Nat
h : a * succ b' = a * zero
⊢ succ b' = zero

State before:
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ : Nat
h : a * succ b' = a * zero
⊢ succ b' = zero
Tactic:
rw [mul_zero] at h
State after:
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ : Nat
h : a * succ b' = zero
⊢ succ b' = zero

State before:
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ : Nat
h : a * succ b' = zero
⊢ succ b' = zero
Tactic:
cases eq_zero_or_eq_zero_of_mul_eq_zero h with
| inl ha => contradiction
| inr hb => assumption
State after:
no goals

State before:
case inl
a : Nat
ha✝ : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ : Nat
h : a * succ b' = zero
ha : a = 0
⊢ succ b' = zero
Tactic:
contradiction
State after:
no goals

State before:
case inr
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ : Nat
h : a * succ b' = zero
hb : succ b' = 0
⊢ succ b' = zero
Tactic:
assumption
State after:
no goals

State before:
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ c' : Nat
⊢ a * succ b' = a * succ c' → succ b' = succ c'
Tactic:
intro h
State after:
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ c' : Nat
h : a * succ b' = a * succ c'
⊢ succ b' = succ c'

State before:
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ c' : Nat
h : a * succ b' = a * succ c'
⊢ succ b' = succ c'
Tactic:
apply succ_eq_succ_of_eq
State after:
case a
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ c' : Nat
h : a * succ b' = a * succ c'
⊢ b' = c'

State before:
case a
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ c' : Nat
h : a * succ b' = a * succ c'
⊢ b' = c'
Tactic:
rw [mul_succ, mul_succ] at h
State after:
case a
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ c' : Nat
h : a * b' + a = a * c' + a
⊢ b' = c'

State before:
case a
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ c' : Nat
h : a * b' + a = a * c' + a
⊢ b' = c'
Tactic:
have habax : a*b' = a*c' := add_right_cancel h
State after:
case a
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ c' : Nat
h : a * b' + a = a * c' + a
habax : a * b' = a * c'
⊢ b' = c'

State before:
case a
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ c' : Nat
h : a * b' + a = a * c' + a
habax : a * b' = a * c'
⊢ b' = c'
Tactic:
have ihbc : a*b' = a*c' → b' = c' := ihb c'
State after:
case a
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ c' : Nat
h : a * b' + a = a * c' + a
habax : a * b' = a * c'
ihbc : a * b' = a * c' → b' = c'
⊢ b' = c'

State before:
case a
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ c' : Nat
h : a * b' + a = a * c' + a
habax : a * b' = a * c'
ihbc : a * b' = a * c' → b' = c'
⊢ b' = c'
Tactic:
apply ihbc
State after:
case a
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ c' : Nat
h : a * b' + a = a * c' + a
habax : a * b' = a * c'
ihbc : a * b' = a * c' → b' = c'
⊢ a * b' = a * c'

State before:
case a
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ c' : Nat
h : a * b' + a = a * c' + a
habax : a * b' = a * c'
ihbc : a * b' = a * c' → b' = c'
⊢ a * b' = a * c'
Tactic:
exact habax
State after:
no goals