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

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

State before:
ℕ : Type
inst✝² : Natural ℕ
ℤ : Type
inst✝¹ : Integer ℤ
a₁ a₂ b : ℤ
inst✝ : AP (Positive b)
x✝ : a₁ ≃ a₂
⊢ a₁//b ≃ a₂//b
Tactic:
show a₁ * b ≃ a₂ * b
State after:
ℕ : Type
inst✝² : Natural ℕ
ℤ : Type
inst✝¹ : Integer ℤ
a₁ a₂ b : ℤ
inst✝ : AP (Positive b)
x✝ : a₁ ≃ a₂
⊢ a₁ * b ≃ a₂ * b

State before:
ℕ : Type
inst✝² : Natural ℕ
ℤ : Type
inst✝¹ : Integer ℤ
a₁ a₂ b : ℤ
inst✝ : AP (Positive b)
x✝ : a₁ ≃ a₂
⊢ a₁ * b ≃ a₂ * b
Tactic:
exact AA.substL ‹a₁ ≃ a₂›
State after:
no goals