Theorem: Lean4Axiomatic.Rational.add_preserves_sign (Lean4Axiomatic/Rational/Sign.lean)

State before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
s : ℤ
p q : ℚ
⊢ sgn p ≃ s → sgn q ≃ s → sgn (p + q) ≃ s
Tactic:
intro (_ : sgn p ≃ s) (_ : sgn q ≃ s)
State after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
s : ℤ
p q : ℚ
x✝¹ : sgn p ≃ s
x✝ : sgn q ≃ s
⊢ sgn (p + q) ≃ s

State before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
s : ℤ
p q : ℚ
x✝¹ : sgn p ≃ s
x✝ : sgn q ≃ s
⊢ sgn (p + q) ≃ s
Tactic:
have (AsRatio.intro (a : ℤ) (b : ℤ) (_ : Integer.Nonzero b) p_eqv) :=
  as_ratio p
State after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
s : ℤ
p q : ℚ
x✝¹ : sgn p ≃ s
x✝ : sgn q ≃ s
a b : ℤ
b_nonzero✝ : Integer.Nonzero b
p_eqv : p ≃ from_integer a / from_integer b
⊢ sgn (p + q) ≃ s

State before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
s : ℤ
p q : ℚ
x✝¹ : sgn p ≃ s
x✝ : sgn q ≃ s
a b : ℤ
b_nonzero✝ : Integer.Nonzero b
p_eqv : p ≃ from_integer a / from_integer b
⊢ sgn (p + q) ≃ s
Tactic:
have (AsRatio.intro (c : ℤ) (d : ℤ) (_ : Integer.Nonzero d) q_eqv) :=
  as_ratio q
State after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
s : ℤ
p q : ℚ
x✝¹ : sgn p ≃ s
x✝ : sgn q ≃ s
a b : ℤ
b_nonzero✝¹ : Integer.Nonzero b
p_eqv : p ≃ from_integer a / from_integer b
c d : ℤ
b_nonzero✝ : Integer.Nonzero d
q_eqv : q ≃ from_integer c / from_integer d
⊢ sgn (p + q) ≃ s

State before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
s : ℤ
p q : ℚ
x✝¹ : sgn p ≃ s
x✝ : sgn q ≃ s
a b : ℤ
b_nonzero✝¹ : Integer.Nonzero b
p_eqv : p ≃ from_integer a / from_integer b
c d : ℤ
b_nonzero✝ : Integer.Nonzero d
q_eqv : q ≃ from_integer c / from_integer d
⊢ sgn (p + q) ≃ s
Tactic:
have : p ≃ a/b := p_eqv
State after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
s : ℤ
p q : ℚ
x✝¹ : sgn p ≃ s
x✝ : sgn q ≃ s
a b : ℤ
b_nonzero✝¹ : Integer.Nonzero b
p_eqv : p ≃ from_integer a / from_integer b
c d : ℤ
b_nonzero✝ : Integer.Nonzero d
q_eqv : q ≃ from_integer c / from_integer d
this : p ≃ from_integer a / from_integer b
⊢ sgn (p + q) ≃ s

State before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
s : ℤ
p q : ℚ
x✝¹ : sgn p ≃ s
x✝ : sgn q ≃ s
a b : ℤ
b_nonzero✝¹ : Integer.Nonzero b
p_eqv : p ≃ from_integer a / from_integer b
c d : ℤ
b_nonzero✝ : Integer.Nonzero d
q_eqv : q ≃ from_integer c / from_integer d
this : p ≃ from_integer a / from_integer b
⊢ sgn (p + q) ≃ s
Tactic:
have : q ≃ c/d := q_eqv
State after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
s : ℤ
p q : ℚ
x✝¹ : sgn p ≃ s
x✝ : sgn q ≃ s
a b : ℤ
b_nonzero✝¹ : Integer.Nonzero b
p_eqv : p ≃ from_integer a / from_integer b
c d : ℤ
b_nonzero✝ : Integer.Nonzero d
q_eqv : q ≃ from_integer c / from_integer d
this✝ : p ≃ from_integer a / from_integer b
this : q ≃ from_integer c / from_integer d
⊢ sgn (p + q) ≃ s

State before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
s : ℤ
p q : ℚ
x✝¹ : sgn p ≃ s
x✝ : sgn q ≃ s
a b : ℤ
b_nonzero✝¹ : Integer.Nonzero b
p_eqv : p ≃ from_integer a / from_integer b
c d : ℤ
b_nonzero✝ : Integer.Nonzero d
q_eqv : q ≃ from_integer c / from_integer d
this✝ : p ≃ from_integer a / from_integer b
this : q ≃ from_integer c / from_integer d
⊢ sgn (p + q) ≃ s
Tactic:
have : Integer.Sqrt1 (sgn b) := Integer.sgn_nonzero.mp ‹Integer.Nonzero b›
State after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
s : ℤ
p q : ℚ
x✝¹ : sgn p ≃ s
x✝ : sgn q ≃ s
a b : ℤ
b_nonzero✝¹ : Integer.Nonzero b
p_eqv : p ≃ from_integer a / from_integer b
c d : ℤ
b_nonzero✝ : Integer.Nonzero d
q_eqv : q ≃ from_integer c / from_integer d
this✝¹ : p ≃ from_integer a / from_integer b
this✝ : q ≃ from_integer c / from_integer d
this : Integer.Sqrt1 (sgn b)
⊢ sgn (p + q) ≃ s

State before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
s : ℤ
p q : ℚ
x✝¹ : sgn p ≃ s
x✝ : sgn q ≃ s
a b : ℤ
b_nonzero✝¹ : Integer.Nonzero b
p_eqv : p ≃ from_integer a / from_integer b
c d : ℤ
b_nonzero✝ : Integer.Nonzero d
q_eqv : q ≃ from_integer c / from_integer d
this✝¹ : p ≃ from_integer a / from_integer b
this✝ : q ≃ from_integer c / from_integer d
this : Integer.Sqrt1 (sgn b)
⊢ sgn (p + q) ≃ s
Tactic:
have : Integer.Sqrt1 (sgn d) := Integer.sgn_nonzero.mp ‹Integer.Nonzero d›
State after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
s : ℤ
p q : ℚ
x✝¹ : sgn p ≃ s
x✝ : sgn q ≃ s
a b : ℤ
b_nonzero✝¹ : Integer.Nonzero b
p_eqv : p ≃ from_integer a / from_integer b
c d : ℤ
b_nonzero✝ : Integer.Nonzero d
q_eqv : q ≃ from_integer c / from_integer d
this✝² : p ≃ from_integer a / from_integer b
this✝¹ : q ≃ from_integer c / from_integer d
this✝ : Integer.Sqrt1 (sgn b)
this : Integer.Sqrt1 (sgn d)
⊢ sgn (p + q) ≃ s

State before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
s : ℤ
p q : ℚ
x✝¹ : sgn p ≃ s
x✝ : sgn q ≃ s
a b : ℤ
b_nonzero✝¹ : Integer.Nonzero b
p_eqv : p ≃ from_integer a / from_integer b
c d : ℤ
b_nonzero✝ : Integer.Nonzero d
q_eqv : q ≃ from_integer c / from_integer d
this✝² : p ≃ from_integer a / from_integer b
this✝¹ : q ≃ from_integer c / from_integer d
this✝ : Integer.Sqrt1 (sgn b)
this : Integer.Sqrt1 (sgn d)
⊢ sgn (p + q) ≃ s
Tactic:
have : sgn (a * b) ≃ s := calc
  sgn (a * b)     ≃ _ := Integer.sgn_compat_mul
  sgn a * sgn b   ≃ _ := Rel.symm sgn_div_integers
  sgn ((a : ℚ)/b) ≃ _ := sgn_subst (eqv_symm ‹p ≃ a/b›)
  sgn p           ≃ _ := ‹sgn p ≃ s›
  s               ≃ _ := Rel.refl
State after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
s : ℤ
p q : ℚ
x✝¹ : sgn p ≃ s
x✝ : sgn q ≃ s
a b : ℤ
b_nonzero✝¹ : Integer.Nonzero b
p_eqv : p ≃ from_integer a / from_integer b
c d : ℤ
b_nonzero✝ : Integer.Nonzero d
q_eqv : q ≃ from_integer c / from_integer d
this✝³ : p ≃ from_integer a / from_integer b
this✝² : q ≃ from_integer c / from_integer d
this✝¹ : Integer.Sqrt1 (sgn b)
this✝ : Integer.Sqrt1 (sgn d)
this : sgn (a * b) ≃ s
⊢ sgn (p + q) ≃ s

State before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
s : ℤ
p q : ℚ
x✝¹ : sgn p ≃ s
x✝ : sgn q ≃ s
a b : ℤ
b_nonzero✝¹ : Integer.Nonzero b
p_eqv : p ≃ from_integer a / from_integer b
c d : ℤ
b_nonzero✝ : Integer.Nonzero d
q_eqv : q ≃ from_integer c / from_integer d
this✝³ : p ≃ from_integer a / from_integer b
this✝² : q ≃ from_integer c / from_integer d
this✝¹ : Integer.Sqrt1 (sgn b)
this✝ : Integer.Sqrt1 (sgn d)
this : sgn (a * b) ≃ s
⊢ sgn (p + q) ≃ s
Tactic:
have : sgn (c * d) ≃ s := calc
  sgn (c * d)     ≃ _ := Integer.sgn_compat_mul
  sgn c * sgn d   ≃ _ := Rel.symm sgn_div_integers
  sgn ((c : ℚ)/d) ≃ _ := sgn_subst (eqv_symm ‹q ≃ c/d›)
  sgn q           ≃ _ := ‹sgn q ≃ s›
  s               ≃ _ := Rel.refl
State after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
s : ℤ
p q : ℚ
x✝¹ : sgn p ≃ s
x✝ : sgn q ≃ s
a b : ℤ
b_nonzero✝¹ : Integer.Nonzero b
p_eqv : p ≃ from_integer a / from_integer b
c d : ℤ
b_nonzero✝ : Integer.Nonzero d
q_eqv : q ≃ from_integer c / from_integer d
this✝⁴ : p ≃ from_integer a / from_integer b
this✝³ : q ≃ from_integer c / from_integer d
this✝² : Integer.Sqrt1 (sgn b)
this✝¹ : Integer.Sqrt1 (sgn d)
this✝ : sgn (a * b) ≃ s
this : sgn (c * d) ≃ s
⊢ sgn (p + q) ≃ s

State before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
s : ℤ
p q : ℚ
x✝¹ : sgn p ≃ s
x✝ : sgn q ≃ s
a b : ℤ
b_nonzero✝¹ : Integer.Nonzero b
p_eqv : p ≃ from_integer a / from_integer b
c d : ℤ
b_nonzero✝ : Integer.Nonzero d
q_eqv : q ≃ from_integer c / from_integer d
this✝⁴ : p ≃ from_integer a / from_integer b
this✝³ : q ≃ from_integer c / from_integer d
this✝² : Integer.Sqrt1 (sgn b)
this✝¹ : Integer.Sqrt1 (sgn d)
this✝ : sgn (a * b) ≃ s
this : sgn (c * d) ≃ s
⊢ sgn (p + q) ≃ s
Tactic:
have sgn_abdd : sgn (a * b * (d * d)) ≃ s := calc
  sgn (a * b * (d * d))     ≃ _ := Integer.sgn_compat_mul
  sgn (a * b) * sgn (d * d) ≃ _ := AA.substL ‹sgn (a * b) ≃ s›
  s * sgn (d * d)           ≃ _ := AA.substR Integer.sgn_compat_mul
  s * (sgn d * sgn d)       ≃ _ := AA.substR ‹Integer.Sqrt1 (sgn d)›.elim
  s * 1                     ≃ _ := AA.identR
  s                         ≃ _ := Rel.refl
State after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
s : ℤ
p q : ℚ
x✝¹ : sgn p ≃ s
x✝ : sgn q ≃ s
a b : ℤ
b_nonzero✝¹ : Integer.Nonzero b
p_eqv : p ≃ from_integer a / from_integer b
c d : ℤ
b_nonzero✝ : Integer.Nonzero d
q_eqv : q ≃ from_integer c / from_integer d
this✝⁴ : p ≃ from_integer a / from_integer b
this✝³ : q ≃ from_integer c / from_integer d
this✝² : Integer.Sqrt1 (sgn b)
this✝¹ : Integer.Sqrt1 (sgn d)
this✝ : sgn (a * b) ≃ s
this : sgn (c * d) ≃ s
sgn_abdd : sgn (a * b * (d * d)) ≃ s
⊢ sgn (p + q) ≃ s

State before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
s : ℤ
p q : ℚ
x✝¹ : sgn p ≃ s
x✝ : sgn q ≃ s
a b : ℤ
b_nonzero✝¹ : Integer.Nonzero b
p_eqv : p ≃ from_integer a / from_integer b
c d : ℤ
b_nonzero✝ : Integer.Nonzero d
q_eqv : q ≃ from_integer c / from_integer d
this✝⁴ : p ≃ from_integer a / from_integer b
this✝³ : q ≃ from_integer c / from_integer d
this✝² : Integer.Sqrt1 (sgn b)
this✝¹ : Integer.Sqrt1 (sgn d)
this✝ : sgn (a * b) ≃ s
this : sgn (c * d) ≃ s
sgn_abdd : sgn (a * b * (d * d)) ≃ s
⊢ sgn (p + q) ≃ s
Tactic:
have sgn_bbcd : sgn (b * b * (c * d)) ≃ s := calc
  sgn (b * b * (c * d))     ≃ _ := Integer.sgn_compat_mul
  sgn (b * b) * sgn (c * d) ≃ _ := AA.substR ‹sgn (c * d) ≃ s›
  sgn (b * b) * s           ≃ _ := AA.substL Integer.sgn_compat_mul
  sgn b * sgn b * s         ≃ _ := AA.substL ‹Integer.Sqrt1 (sgn b)›.elim
  1 * s                     ≃ _ := AA.identL
  s                         ≃ _ := Rel.refl
State after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
s : ℤ
p q : ℚ
x✝¹ : sgn p ≃ s
x✝ : sgn q ≃ s
a b : ℤ
b_nonzero✝¹ : Integer.Nonzero b
p_eqv : p ≃ from_integer a / from_integer b
c d : ℤ
b_nonzero✝ : Integer.Nonzero d
q_eqv : q ≃ from_integer c / from_integer d
this✝⁴ : p ≃ from_integer a / from_integer b
this✝³ : q ≃ from_integer c / from_integer d
this✝² : Integer.Sqrt1 (sgn b)
this✝¹ : Integer.Sqrt1 (sgn d)
this✝ : sgn (a * b) ≃ s
this : sgn (c * d) ≃ s
sgn_abdd : sgn (a * b * (d * d)) ≃ s
sgn_bbcd : sgn (b * b * (c * d)) ≃ s
⊢ sgn (p + q) ≃ s

State before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
s : ℤ
p q : ℚ
x✝¹ : sgn p ≃ s
x✝ : sgn q ≃ s
a b : ℤ
b_nonzero✝¹ : Integer.Nonzero b
p_eqv : p ≃ from_integer a / from_integer b
c d : ℤ
b_nonzero✝ : Integer.Nonzero d
q_eqv : q ≃ from_integer c / from_integer d
this✝⁴ : p ≃ from_integer a / from_integer b
this✝³ : q ≃ from_integer c / from_integer d
this✝² : Integer.Sqrt1 (sgn b)
this✝¹ : Integer.Sqrt1 (sgn d)
this✝ : sgn (a * b) ≃ s
this : sgn (c * d) ≃ s
sgn_abdd : sgn (a * b * (d * d)) ≃ s
sgn_bbcd : sgn (b * b * (c * d)) ≃ s
⊢ sgn (p + q) ≃ s
Tactic:
have : sgn (p + q) ≃ s := calc
  sgn (p + q)
    ≃ _ := sgn_subst (add_substL ‹p ≃ a/b›)
  sgn ((a : ℚ)/b + q)
    ≃ _ := sgn_subst (add_substR ‹q ≃ c/d›)
  sgn ((a : ℚ)/b + (c : ℚ)/d)
    ≃ _ := sgn_subst add_div_integers
  sgn (((a * d + b * c : ℤ) : ℚ)/((b * d : ℤ) : ℚ))
    ≃ _ := sgn_div_integers
  sgn (a * d + b * c) * sgn (b * d)
    ≃ _ := Rel.symm Integer.sgn_compat_mul
  sgn ((a * d + b * c) * (b * d))
    ≃ _ := Integer.sgn_subst AA.distribR
  sgn (a * d * (b * d) + b * c * (b * d))
    ≃ _ := Integer.sgn_subst (AA.substL AA.expr_xxfxxff_lr_swap_rl)
  sgn (a * b * (d * d) + b * c * (b * d))
    ≃ _ := Integer.sgn_subst (AA.substR AA.expr_xxfxxff_lr_swap_rl)
  sgn (a * b * (d * d) + b * b * (c * d))
    ≃ _ := Integer.add_preserves_sign sgn_abdd sgn_bbcd
  s
    ≃ _ := Rel.refl
State after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
s : ℤ
p q : ℚ
x✝¹ : sgn p ≃ s
x✝ : sgn q ≃ s
a b : ℤ
b_nonzero✝¹ : Integer.Nonzero b
p_eqv : p ≃ from_integer a / from_integer b
c d : ℤ
b_nonzero✝ : Integer.Nonzero d
q_eqv : q ≃ from_integer c / from_integer d
this✝⁵ : p ≃ from_integer a / from_integer b
this✝⁴ : q ≃ from_integer c / from_integer d
this✝³ : Integer.Sqrt1 (sgn b)
this✝² : Integer.Sqrt1 (sgn d)
this✝¹ : sgn (a * b) ≃ s
this✝ : sgn (c * d) ≃ s
sgn_abdd : sgn (a * b * (d * d)) ≃ s
sgn_bbcd : sgn (b * b * (c * d)) ≃ s
this : sgn (p + q) ≃ s
⊢ sgn (p + q) ≃ s

State before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
s : ℤ
p q : ℚ
x✝¹ : sgn p ≃ s
x✝ : sgn q ≃ s
a b : ℤ
b_nonzero✝¹ : Integer.Nonzero b
p_eqv : p ≃ from_integer a / from_integer b
c d : ℤ
b_nonzero✝ : Integer.Nonzero d
q_eqv : q ≃ from_integer c / from_integer d
this✝⁵ : p ≃ from_integer a / from_integer b
this✝⁴ : q ≃ from_integer c / from_integer d
this✝³ : Integer.Sqrt1 (sgn b)
this✝² : Integer.Sqrt1 (sgn d)
this✝¹ : sgn (a * b) ≃ s
this✝ : sgn (c * d) ≃ s
sgn_abdd : sgn (a * b * (d * d)) ≃ s
sgn_bbcd : sgn (b * b * (c * d)) ≃ s
this : sgn (p + q) ≃ s
⊢ sgn (p + q) ≃ s
Tactic:
exact this
State after:
no goals