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

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

State before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a₁ a₂ b : ℤ
x✝ : a₁ ≃ a₂
⊢ a₁ - b ≃ a₂ - b
Tactic:
calc
  a₁ - b    ≃ _ := sub_defn
  a₁ + (-b) ≃ _ := AA.substL ‹a₁ ≃ a₂›
  a₂ + (-b) ≃ _ := Rel.symm sub_defn
  a₂ - b    ≃ _ := Rel.refl
State after:
no goals