Theorem: Lean4Axiomatic.Rational.Impl.Fraction.from_integer_subst (Lean4Axiomatic/Rational/Impl/Fraction/Core.lean)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a₁ a₂ : ℤ
⊢ a₁ ≃ a₂ → from_integer a₁ ≃ from_integer a₂
Tactic:
intro (_ : a₁ ≃ a₂)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
⊢ from_integer a₁ ≃ from_integer a₂

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
⊢ from_integer a₁ ≃ from_integer a₂
Tactic:
show a₁//1 ≃ a₂//1
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
⊢ a₁//1 ≃ a₂//1

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
⊢ a₁//1 ≃ a₂//1
Tactic:
exact substN ‹a₁ ≃ a₂›
State after:
no goals