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

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

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a₁ a₂ : ℤ
x✝ : from_integer a₁ ≃ from_integer a₂
⊢ a₁ ≃ a₂
Tactic:
have : a₁//1 ≃ a₂//1 := ‹from_integer a₁ ≃ from_integer a₂›
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a₁ a₂ : ℤ
x✝ : from_integer a₁ ≃ from_integer a₂
this : a₁//1 ≃ a₂//1
⊢ a₁ ≃ a₂

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

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