Theorem: Misc.mul_eq_mul_left_iff (LeanSAT/Util/Misc.lean)

State before:
a b c : Nat
⊢ a * b = a * c ↔ b = c ∨ a = 0
Tactic:
by_cases ha : a = 0
State after:
case pos
a b c : Nat
ha : a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0

case neg
a b c : Nat
ha : ¬a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0

State before:
case pos
a b c : Nat
ha : a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0

case neg
a b c : Nat
ha : ¬a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0
Tactic:
. simp only [ha, Nat.zero_mul, or_true]
State after:
case neg
a b c : Nat
ha : ¬a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0

State before:
case neg
a b c : Nat
ha : ¬a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0
Tactic:
. simp only [ha, or_false]
  have zero_lt_a : 0 < a := Nat.zero_lt_of_ne_zero ha
  constructor
  . exact Nat.eq_of_mul_eq_mul_left zero_lt_a
  . intro h
    rw [h]
State after:
no goals

State before:
case pos
a b c : Nat
ha : a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0
Tactic:
simp only [ha, Nat.zero_mul, or_true]
State after:
no goals

State before:
case neg
a b c : Nat
ha : ¬a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0
Tactic:
simp only [ha, or_false]
State after:
case neg
a b c : Nat
ha : ¬a = 0
⊢ a * b = a * c ↔ b = c

State before:
case neg
a b c : Nat
ha : ¬a = 0
⊢ a * b = a * c ↔ b = c
Tactic:
have zero_lt_a : 0 < a := Nat.zero_lt_of_ne_zero ha
State after:
case neg
a b c : Nat
ha : ¬a = 0
zero_lt_a : 0 < a
⊢ a * b = a * c ↔ b = c

State before:
case neg
a b c : Nat
ha : ¬a = 0
zero_lt_a : 0 < a
⊢ a * b = a * c ↔ b = c
Tactic:
constructor
State after:
case neg.mp
a b c : Nat
ha : ¬a = 0
zero_lt_a : 0 < a
⊢ a * b = a * c → b = c

case neg.mpr
a b c : Nat
ha : ¬a = 0
zero_lt_a : 0 < a
⊢ b = c → a * b = a * c

State before:
case neg.mp
a b c : Nat
ha : ¬a = 0
zero_lt_a : 0 < a
⊢ a * b = a * c → b = c

case neg.mpr
a b c : Nat
ha : ¬a = 0
zero_lt_a : 0 < a
⊢ b = c → a * b = a * c
Tactic:
. exact Nat.eq_of_mul_eq_mul_left zero_lt_a
State after:
case neg.mpr
a b c : Nat
ha : ¬a = 0
zero_lt_a : 0 < a
⊢ b = c → a * b = a * c

State before:
case neg.mpr
a b c : Nat
ha : ¬a = 0
zero_lt_a : 0 < a
⊢ b = c → a * b = a * c
Tactic:
. intro h
  rw [h]
State after:
no goals

State before:
case neg.mp
a b c : Nat
ha : ¬a = 0
zero_lt_a : 0 < a
⊢ a * b = a * c → b = c
Tactic:
exact Nat.eq_of_mul_eq_mul_left zero_lt_a
State after:
no goals

State before:
case neg.mpr
a b c : Nat
ha : ¬a = 0
zero_lt_a : 0 < a
⊢ b = c → a * b = a * c
Tactic:
intro h
State after:
case neg.mpr
a b c : Nat
ha : ¬a = 0
zero_lt_a : 0 < a
h : b = c
⊢ a * b = a * c

State before:
case neg.mpr
a b c : Nat
ha : ¬a = 0
zero_lt_a : 0 < a
h : b = c
⊢ a * b = a * c
Tactic:
rw [h]
State after:
no goals