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

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

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ b : ℤ
x✝ : a₁ + b ≃ a₂ + b
⊢ a₁ ≃ a₂
Tactic:
have : b + a₁ ≃ b + a₂ := calc
  _ = b + a₁ := rfl
  _ ≃ a₁ + b := AA.comm
  _ ≃ a₂ + b := ‹a₁ + b ≃ a₂ + b›
  _ ≃ b + a₂ := AA.comm
State after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ b : ℤ
x✝ : a₁ + b ≃ a₂ + b
this : b + a₁ ≃ b + a₂
⊢ a₁ ≃ a₂

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ b : ℤ
x✝ : a₁ + b ≃ a₂ + b
this : b + a₁ ≃ b + a₂
⊢ a₁ ≃ a₂
Tactic:
have : a₁ ≃ a₂ := add_cancelL ‹b + a₁ ≃ b + a₂›
State after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ b : ℤ
x✝ : a₁ + b ≃ a₂ + b
this✝ : b + a₁ ≃ b + a₂
this : a₁ ≃ a₂
⊢ a₁ ≃ a₂

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ b : ℤ
x✝ : a₁ + b ≃ a₂ + b
this✝ : b + a₁ ≃ b + a₂
this : a₁ ≃ a₂
⊢ a₁ ≃ a₂
Tactic:
exact this
State after:
no goals