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

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

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

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