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

State before:
ℕ : Type
inst✝ : Natural ℕ
a : Difference ℕ
⊢ a ≃ a
Tactic:
revert a
State after:
ℕ : Type
inst✝ : Natural ℕ
⊢ ∀ {a : Difference ℕ}, a ≃ a

State before:
ℕ : Type
inst✝ : Natural ℕ
⊢ ∀ {a : Difference ℕ}, a ≃ a
Tactic:
intro (a₁——a₂)
State after:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ : ℕ
⊢ a₁——a₂ ≃ a₁——a₂

State before:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ : ℕ
⊢ a₁——a₂ ≃ a₁——a₂
Tactic:
show a₁ + a₂ ≃ a₁ + a₂
State after:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ : ℕ
⊢ a₁ + a₂ ≃ a₁ + a₂

State before:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ : ℕ
⊢ a₁ + a₂ ≃ a₁ + a₂
Tactic:
exact Rel.refl
State after:
no goals