Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_compat_mul (Lean4Axiomatic/Rational/Impl/Fraction/Sign.lean)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p q : Fraction ℤ
⊢ sgn (p * q) ≃ sgn p * sgn q
Tactic:
revert p
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, sgn (p * q) ≃ sgn p * sgn q

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, sgn (p * q) ≃ sgn p * sgn q
Tactic:
intro (a//b)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
⊢ sgn (a//b * q) ≃ sgn (a//b) * sgn q

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
⊢ sgn (a//b * q) ≃ sgn (a//b) * sgn q
Tactic:
revert q
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
⊢ ∀ {q : Fraction ℤ}, sgn (a//b * q) ≃ sgn (a//b) * sgn q

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
⊢ ∀ {q : Fraction ℤ}, sgn (a//b * q) ≃ sgn (a//b) * sgn q
Tactic:
intro (c//d)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
⊢ sgn (a//b * c//d) ≃ sgn (a//b) * sgn (c//d)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
⊢ sgn (a//b * c//d) ≃ sgn (a//b) * sgn (c//d)
Tactic:
calc
  sgn (a//b * c//d)       ≃ _ := sgn_subst eqv_refl
  sgn ((a * c)//(b * d))  ≃ _ := Rel.refl
  sgn (a * c)             ≃ _ := Integer.sgn_compat_mul
  sgn a * sgn c           ≃ _ := Rel.refl
  sgn (a//b) * sgn (c//d) ≃ _ := Rel.refl
State after:
no goals