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

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

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

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

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