Theorem: Lean4Axiomatic.Integer.mul_cancelL (Lean4Axiomatic/Integer/Subtraction.lean)

State before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b c : ℤ
⊢ a ≄ 0 → a * b ≃ a * c → b ≃ c
Tactic:
intro (_ : a ≄ 0) (_ : a * b ≃ a * c)
State after:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b c : ℤ
x✝¹ : a ≄ 0
x✝ : a * b ≃ a * c
⊢ b ≃ c

State before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b c : ℤ
x✝¹ : a ≄ 0
x✝ : a * b ≃ a * c
⊢ b ≃ c
Tactic:
have : a * b - a * c ≃ 0 := zero_diff_iff_eqv.mpr ‹a * b ≃ a * c›
State after:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b c : ℤ
x✝¹ : a ≄ 0
x✝ : a * b ≃ a * c
this : a * b - a * c ≃ 0
⊢ b ≃ c

State before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b c : ℤ
x✝¹ : a ≄ 0
x✝ : a * b ≃ a * c
this : a * b - a * c ≃ 0
⊢ b ≃ c
Tactic:
have : a * (b - c) ≃ 0 := Rel.trans AA.distribL ‹a * b - a * c ≃ 0›
State after:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b c : ℤ
x✝¹ : a ≄ 0
x✝ : a * b ≃ a * c
this✝ : a * b - a * c ≃ 0
this : a * (b - c) ≃ 0
⊢ b ≃ c

State before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b c : ℤ
x✝¹ : a ≄ 0
x✝ : a * b ≃ a * c
this✝ : a * b - a * c ≃ 0
this : a * (b - c) ≃ 0
⊢ b ≃ c
Tactic:
have : a ≃ 0 ∨ b - c ≃ 0 := mul_split_zero.mp ‹a * (b - c) ≃ 0›
State after:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b c : ℤ
x✝¹ : a ≄ 0
x✝ : a * b ≃ a * c
this✝¹ : a * b - a * c ≃ 0
this✝ : a * (b - c) ≃ 0
this : a ≃ 0 ∨ b - c ≃ 0
⊢ b ≃ c

State before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b c : ℤ
x✝¹ : a ≄ 0
x✝ : a * b ≃ a * c
this✝¹ : a * b - a * c ≃ 0
this✝ : a * (b - c) ≃ 0
this : a ≃ 0 ∨ b - c ≃ 0
⊢ b ≃ c
Tactic:
match ‹a ≃ 0 ∨ b - c ≃ 0› with
| Or.inl (_ : a ≃ 0) =>
  show b ≃ c
  exact absurd ‹a ≃ 0› ‹a ≄ 0›
| Or.inr (_ : b - c ≃ 0) =>
  show b ≃ c
  exact zero_diff_iff_eqv.mp ‹b - c ≃ 0›
State after:
no goals

State before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b c : ℤ
x✝¹ : a ≄ 0
x✝ : a * b ≃ a * c
this✝¹ : a * b - a * c ≃ 0
this✝ : a * (b - c) ≃ 0
this : a ≃ 0 ∨ b - c ≃ 0
h✝ : a ≃ 0
⊢ b ≃ c
Tactic:
exact absurd ‹a ≃ 0› ‹a ≄ 0›
State after:
no goals

State before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b c : ℤ
x✝¹ : a ≄ 0
x✝ : a * b ≃ a * c
this✝¹ : a * b - a * c ≃ 0
this✝ : a * (b - c) ≃ 0
this : a ≃ 0 ∨ b - c ≃ 0
h✝ : b - c ≃ 0
⊢ b ≃ c
Tactic:
exact zero_diff_iff_eqv.mp ‹b - c ≃ 0›
State after:
no goals