Theorem: Lean4Axiomatic.Integer.add_cancelL (Lean4Axiomatic/Integer/Negation.lean)

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b₁ b₂ : ℤ
⊢ a + b₁ ≃ a + b₂ → b₁ ≃ b₂
Tactic:
intro (_ : a + b₁ ≃ a + b₂)
State after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b₁ b₂ : ℤ
x✝ : a + b₁ ≃ a + b₂
⊢ b₁ ≃ b₂

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b₁ b₂ : ℤ
x✝ : a + b₁ ≃ a + b₂
⊢ b₁ ≃ b₂
Tactic:
have reduce {x y : ℤ} : -x + (x + y) ≃ y := calc
  _ = -x + (x + y) := rfl
  _ ≃ (-x + x) + y := Rel.symm AA.assoc
  _ ≃ 0 + y        := AA.substL AA.inverseL
  _ ≃ y            := AA.identL
State after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b₁ b₂ : ℤ
x✝ : a + b₁ ≃ a + b₂
reduce : ∀ {x y : ℤ}, -x + (x + y) ≃ y
⊢ b₁ ≃ b₂

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b₁ b₂ : ℤ
x✝ : a + b₁ ≃ a + b₂
reduce : ∀ {x y : ℤ}, -x + (x + y) ≃ y
⊢ b₁ ≃ b₂
Tactic:
calc
  _ = b₁            := rfl
  _ ≃ -a + (a + b₁) := Rel.symm reduce
  _ ≃ -a + (a + b₂) := AA.substR ‹a + b₁ ≃ a + b₂›
  _ ≃ b₂            := reduce
State after:
no goals