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

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

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

State before:
ℕ : Type
inst✝ : Natural ℕ
b : Difference ℕ
a₁ a₂ : ℕ
⊢ a₁——a₂ ≃ b → b ≃ a₁——a₂
Tactic:
revert b
State after:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ : ℕ
⊢ ∀ {b : Difference ℕ}, a₁——a₂ ≃ b → b ≃ a₁——a₂

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

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

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

State before:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ : ℕ
x✝ : a₁ + b₂ ≃ b₁ + a₂
⊢ b₁ + a₂ ≃ a₁ + b₂
Tactic:
exact Rel.symm ‹a₁ + b₂ ≃ b₁ + a₂›
State after:
no goals