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

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

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

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

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

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

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

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

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

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

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

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

case neg.mpr
a c b : Nat
hc : ¬c = 0
zero_lt_c : 0 < c
⊢ a = b → a * c = b * c
Tactic:
. exact Nat.eq_of_mul_eq_mul_right zero_lt_c
State after:
case neg.mpr
a c b : Nat
hc : ¬c = 0
zero_lt_c : 0 < c
⊢ a = b → a * c = b * c

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

State before:
case neg.mp
a c b : Nat
hc : ¬c = 0
zero_lt_c : 0 < c
⊢ a * c = b * c → a = b
Tactic:
exact Nat.eq_of_mul_eq_mul_right zero_lt_c
State after:
no goals

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

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