Theorem: Lean4Axiomatic.Integer.Impl.Difference.diff_substR (Lean4Axiomatic/Integer/Impl/Difference/Core.lean)

State before:
ℕ : Type
inst✝ : Natural ℕ
n m₁ m₂ : ℕ
⊢ m₁ ≃ m₂ → n——m₁ ≃ n——m₂
Tactic:
intro (_ : m₁ ≃ m₂)
State after:
ℕ : Type
inst✝ : Natural ℕ
n m₁ m₂ : ℕ
x✝ : m₁ ≃ m₂
⊢ n——m₁ ≃ n——m₂

State before:
ℕ : Type
inst✝ : Natural ℕ
n m₁ m₂ : ℕ
x✝ : m₁ ≃ m₂
⊢ n——m₁ ≃ n——m₂
Tactic:
have : n + m₂ ≃ n + m₁ := AA.substR (Rel.symm ‹m₁ ≃ m₂›)
State after:
ℕ : Type
inst✝ : Natural ℕ
n m₁ m₂ : ℕ
x✝ : m₁ ≃ m₂
this : n + m₂ ≃ n + m₁
⊢ n——m₁ ≃ n——m₂

State before:
ℕ : Type
inst✝ : Natural ℕ
n m₁ m₂ : ℕ
x✝ : m₁ ≃ m₂
this : n + m₂ ≃ n + m₁
⊢ n——m₁ ≃ n——m₂
Tactic:
have : n——m₁ ≃ n——m₂ := this
State after:
ℕ : Type
inst✝ : Natural ℕ
n m₁ m₂ : ℕ
x✝ : m₁ ≃ m₂
this✝ : n + m₂ ≃ n + m₁
this : n——m₁ ≃ n——m₂
⊢ n——m₁ ≃ n——m₂

State before:
ℕ : Type
inst✝ : Natural ℕ
n m₁ m₂ : ℕ
x✝ : m₁ ≃ m₂
this✝ : n + m₂ ≃ n + m₁
this : n——m₁ ≃ n——m₂
⊢ n——m₁ ≃ n——m₂
Tactic:
exact this
State after:
no goals