Theorem: Lean4Axiomatic.Rational.nonneg_square (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 ℚ
p : ℚ
⊢ sgn (p * p) ≄ -1
Tactic:
intro (_ : sgn (p * p) ≃ -1)
State after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
x✝ : sgn (p * p) ≃ -1
⊢ False

State before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
x✝ : sgn (p * p) ≃ -1
⊢ False
Tactic:
have : sgn p * sgn p ≃ -1 :=
  Rel.trans (Rel.symm sgn_compat_mul) ‹sgn (p * p) ≃ -1›
State after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
x✝ : sgn (p * p) ≃ -1
this : sgn p * sgn p ≃ -1
⊢ False

State before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
x✝ : sgn (p * p) ≃ -1
this : sgn p * sgn p ≃ -1
⊢ False
Tactic:
have : Integer.Nonzero (-1 : ℤ) := Integer.nonzero_sqrt1
State after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
x✝ : sgn (p * p) ≃ -1
this✝ : sgn p * sgn p ≃ -1
this : Integer.Nonzero (-1)
⊢ False

State before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
x✝ : sgn (p * p) ≃ -1
this✝ : sgn p * sgn p ≃ -1
this : Integer.Nonzero (-1)
⊢ False
Tactic:
have : Integer.Nonzero (sgn p * sgn p) :=
  Integer.nonzero_subst (Rel.symm ‹sgn p * sgn p ≃ -1›) this
State after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
x✝ : sgn (p * p) ≃ -1
this✝¹ : sgn p * sgn p ≃ -1
this✝ : Integer.Nonzero (-1)
this : Integer.Nonzero (sgn p * sgn p)
⊢ False

State before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
x✝ : sgn (p * p) ≃ -1
this✝¹ : sgn p * sgn p ≃ -1
this✝ : Integer.Nonzero (-1)
this : Integer.Nonzero (sgn p * sgn p)
⊢ False
Tactic:
have (And.intro (_ : Integer.Nonzero (sgn p)) _) :=
  Integer.nonzero_factors_if_nonzero_product this
State after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
x✝ : sgn (p * p) ≃ -1
this✝¹ : sgn p * sgn p ≃ -1
this✝ : Integer.Nonzero (-1)
this : Integer.Nonzero (sgn p * sgn p)
left✝ right✝ : Integer.Nonzero (sgn p)
⊢ False

State before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
x✝ : sgn (p * p) ≃ -1
this✝¹ : sgn p * sgn p ≃ -1
this✝ : Integer.Nonzero (-1)
this : Integer.Nonzero (sgn p * sgn p)
left✝ right✝ : Integer.Nonzero (sgn p)
⊢ False
Tactic:
have : Integer.Sqrt1 (sgn (sgn p)) :=
  Integer.sgn_nonzero.mp ‹Integer.Nonzero (sgn p)›
State after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
x✝ : sgn (p * p) ≃ -1
this✝² : sgn p * sgn p ≃ -1
this✝¹ : Integer.Nonzero (-1)
this✝ : Integer.Nonzero (sgn p * sgn p)
left✝ right✝ : Integer.Nonzero (sgn p)
this : Integer.Sqrt1 (sgn (sgn p))
⊢ False

State before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
x✝ : sgn (p * p) ≃ -1
this✝² : sgn p * sgn p ≃ -1
this✝¹ : Integer.Nonzero (-1)
this✝ : Integer.Nonzero (sgn p * sgn p)
left✝ right✝ : Integer.Nonzero (sgn p)
this : Integer.Sqrt1 (sgn (sgn p))
⊢ False
Tactic:
have : Integer.Sqrt1 (sgn p) := Integer.sqrt1_subst sgn_idemp this
State after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
x✝ : sgn (p * p) ≃ -1
this✝³ : sgn p * sgn p ≃ -1
this✝² : Integer.Nonzero (-1)
this✝¹ : Integer.Nonzero (sgn p * sgn p)
left✝ right✝ : Integer.Nonzero (sgn p)
this✝ : Integer.Sqrt1 (sgn (sgn p))
this : Integer.Sqrt1 (sgn p)
⊢ False

State before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
x✝ : sgn (p * p) ≃ -1
this✝³ : sgn p * sgn p ≃ -1
this✝² : Integer.Nonzero (-1)
this✝¹ : Integer.Nonzero (sgn p * sgn p)
left✝ right✝ : Integer.Nonzero (sgn p)
this✝ : Integer.Sqrt1 (sgn (sgn p))
this : Integer.Sqrt1 (sgn p)
⊢ False
Tactic:
have : sgn p ≄ sgn p := Integer.mul_sqrt1_neqv.mp ‹sgn p * sgn p ≃ -1›
State after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
x✝ : sgn (p * p) ≃ -1
this✝⁴ : sgn p * sgn p ≃ -1
this✝³ : Integer.Nonzero (-1)
this✝² : Integer.Nonzero (sgn p * sgn p)
left✝ right✝ : Integer.Nonzero (sgn p)
this✝¹ : Integer.Sqrt1 (sgn (sgn p))
this✝ : Integer.Sqrt1 (sgn p)
this : sgn p ≄ sgn p
⊢ False

State before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
x✝ : sgn (p * p) ≃ -1
this✝⁴ : sgn p * sgn p ≃ -1
this✝³ : Integer.Nonzero (-1)
this✝² : Integer.Nonzero (sgn p * sgn p)
left✝ right✝ : Integer.Nonzero (sgn p)
this✝¹ : Integer.Sqrt1 (sgn (sgn p))
this✝ : Integer.Sqrt1 (sgn p)
this : sgn p ≄ sgn p
⊢ False
Tactic:
exact absurd Rel.refl this
State after:
no goals