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

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁ p₂ : Fraction ℤ
⊢ p₁ ≃ p₂ → sgn p₁ ≃ sgn p₂
Tactic:
revert p₁
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₂ : Fraction ℤ
⊢ ∀ {p₁ : Fraction ℤ}, p₁ ≃ p₂ → sgn p₁ ≃ sgn p₂

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

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

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
⊢ ∀ {p₂ : Fraction ℤ}, a//b ≃ p₂ → sgn (a//b) ≃ sgn p₂
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)
⊢ 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)
⊢ a//b ≃ c//d → sgn (a//b) ≃ sgn (c//d)
Tactic:
intro (_ : a//b ≃ c//d)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
x✝ : 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)
x✝ : a//b ≃ c//d
⊢ sgn (a//b) ≃ sgn (c//d)
Tactic:
have : a * d ≃ c * b := ‹a//b ≃ c//d›
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
x✝ : a//b ≃ c//d
this : a * d ≃ c * b
⊢ 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)
x✝ : a//b ≃ c//d
this : a * d ≃ c * b
⊢ sgn (a//b) ≃ sgn (c//d)
Tactic:
have : Positive b := ‹AP (Positive b)›.ev
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
x✝ : a//b ≃ c//d
this✝ : a * d ≃ c * b
this : Positive b
⊢ 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)
x✝ : a//b ≃ c//d
this✝ : a * d ≃ c * b
this : Positive b
⊢ sgn (a//b) ≃ sgn (c//d)
Tactic:
have : sgn b ≃ 1 := Integer.sgn_positive.mp this
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
x✝ : a//b ≃ c//d
this✝¹ : a * d ≃ c * b
this✝ : Positive b
this : sgn b ≃ 1
⊢ 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)
x✝ : a//b ≃ c//d
this✝¹ : a * d ≃ c * b
this✝ : Positive b
this : sgn b ≃ 1
⊢ sgn (a//b) ≃ sgn (c//d)
Tactic:
have : Positive d := ‹AP (Positive d)›.ev
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
x✝ : a//b ≃ c//d
this✝² : a * d ≃ c * b
this✝¹ : Positive b
this✝ : sgn b ≃ 1
this : Positive 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)
x✝ : a//b ≃ c//d
this✝² : a * d ≃ c * b
this✝¹ : Positive b
this✝ : sgn b ≃ 1
this : Positive d
⊢ sgn (a//b) ≃ sgn (c//d)
Tactic:
have : 1 ≃ sgn d := Rel.symm (Integer.sgn_positive.mp this)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
x✝ : a//b ≃ c//d
this✝³ : a * d ≃ c * b
this✝² : Positive b
this✝¹ : sgn b ≃ 1
this✝ : Positive d
this : 1 ≃ sgn 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)
x✝ : a//b ≃ c//d
this✝³ : a * d ≃ c * b
this✝² : Positive b
this✝¹ : sgn b ≃ 1
this✝ : Positive d
this : 1 ≃ sgn d
⊢ sgn (a//b) ≃ sgn (c//d)
Tactic:
calc
  sgn (a//b)    ≃ _ := Rel.refl
  sgn a         ≃ _ := Rel.symm AA.identR
  sgn a * 1     ≃ _ := AA.substR ‹1 ≃ sgn d›
  sgn a * sgn d ≃ _ := Rel.symm Integer.sgn_compat_mul
  sgn (a * d)   ≃ _ := Integer.sgn_subst ‹a * d ≃ c * b›
  sgn (c * b)   ≃ _ := Integer.sgn_compat_mul
  sgn c * sgn b ≃ _ := AA.substR ‹sgn b ≃ 1›
  sgn c * 1     ≃ _ := AA.identR
  sgn c         ≃ _ := Rel.refl
  sgn (c//d)    ≃ _ := Rel.refl
State after:
no goals