Theorem: Lean4Axiomatic.Integer.Impl.Difference.from_ℕ_subst (Lean4Axiomatic/Integer/Impl/Difference/Core.lean)

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

State before:
ℕ : Type
inst✝ : Natural ℕ
n₁ n₂ : ℕ
x✝ : n₁ ≃ n₂
⊢ n₁——0 ≃ n₂——0
Tactic:
show from_prod (n₁, 0) ≃ from_prod (n₂, 0)
State after:
ℕ : Type
inst✝ : Natural ℕ
n₁ n₂ : ℕ
x✝ : n₁ ≃ n₂
⊢ from_prod (n₁, 0) ≃ from_prod (n₂, 0)

State before:
ℕ : Type
inst✝ : Natural ℕ
n₁ n₂ : ℕ
x✝ : n₁ ≃ n₂
⊢ from_prod (n₁, 0) ≃ from_prod (n₂, 0)
Tactic:
apply AA.subst₁
State after:
case a
ℕ : Type
inst✝ : Natural ℕ
n₁ n₂ : ℕ
x✝ : n₁ ≃ n₂
⊢ (n₁, 0) ≃ (n₂, 0)

State before:
case a
ℕ : Type
inst✝ : Natural ℕ
n₁ n₂ : ℕ
x✝ : n₁ ≃ n₂
⊢ (n₁, 0) ≃ (n₂, 0)
Tactic:
exact AA.substL ‹n₁ ≃ n₂›
State after:
no goals