Theorem: Lean4Axiomatic.Integer.sub_substR (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₂ → b - a₁ ≃ b - a₂
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₂
⊢ b - a₁ ≃ b - a₂

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