internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Rational.sqrt1_sgn_nonzero
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
this : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
⊢ Integer.Sqrt1 (sgn p)
Tactic:
have : sgn p ≃ 1 ∨ sgn p ≃ -1 :=
  match this with
  | AA.OneOfThree.first (_ : sgn p ≃ 0) =>
    have : p ≄ 0 := ‹AP (p ≄ 0)›.ev
    have : sgn p ≄ 0 := mt sgn_zero.mpr this
    absurd ‹sgn p ≃ 0› ‹sgn p ≄ 0›
  | AA.OneOfThree.second (_ : sgn p ≃ 1) =>
    Or.inl ‹sgn p ≃ 1›
  | AA.OneOfThree.third (_ : sgn p ≃ -1) =>
    Or.inr ‹sgn p ≃ -1›
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
this✝ : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
this : sgn p ≃ 1 ∨ sgn p ≃ -1
⊢ Integer.Sqrt1 (sgn p)
Theorem: Lean4Axiomatic.Rational.sqrt1_sgn_nonzero
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
this✝ : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
this : sgn p ≃ 1 ∨ sgn p ≃ -1
⊢ Integer.Sqrt1 (sgn p)
Tactic:
have : Integer.Sqrt1 (sgn p) := Integer.sqrt1_cases.mpr this
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
this✝¹ : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
this✝ : sgn p ≃ 1 ∨ sgn p ≃ -1
this : Integer.Sqrt1 (sgn p)
⊢ Integer.Sqrt1 (sgn p)
Theorem: Lean4Axiomatic.Rational.sqrt1_sgn_nonzero
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
this✝¹ : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
this✝ : sgn p ≃ 1 ∨ sgn p ≃ -1
this : Integer.Sqrt1 (sgn p)
⊢ Integer.Sqrt1 (sgn p)
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.sgn_recip
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
⊢ sgn (p⁻¹) ≃ sgn p
Tactic:
have : 1 ≃ sgn p * sgn p := Rel.symm sqrt1_sgn_nonzero.elim
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
this : 1 ≃ sgn p * sgn p
⊢ sgn (p⁻¹) ≃ sgn p
Theorem: Lean4Axiomatic.Rational.sgn_recip
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
this : 1 ≃ sgn p * sgn p
⊢ sgn (p⁻¹) ≃ sgn p
Tactic:
calc
  sgn (p⁻¹)                   ≃ _ := Rel.symm AA.identR
  sgn (p⁻¹) * 1               ≃ _ := AA.substR ‹1 ≃ sgn p * sgn p›
  sgn (p⁻¹) * (sgn p * sgn p) ≃ _ := AA.substR (Rel.symm sgn_compat_mul)
  sgn (p⁻¹) * sgn (p * p)     ≃ _ := Rel.symm sgn_compat_mul
  sgn (p⁻¹ * (p * p))         ≃ _ := sgn_subst (eqv_symm mul_assoc)
  sgn ((p⁻¹ * p) * p)         ≃ _ := sgn_subst (mul_substL mul_inverseL)
  sgn (1 * p)                 ≃ _ := sgn_subst mul_identL
  sgn p                       ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.sgn_idemp
Proof 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 (sgn p) ≃ sgn p
Tactic:
have (AsRatio.intro (a : ℤ) (b : ℤ) (_ : Integer.Nonzero b) eqv) :=
  as_ratio p
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
a b : ℤ
b_nonzero✝ : Integer.Nonzero b
eqv : p ≃ from_integer a / from_integer b
⊢ sgn (sgn p) ≃ sgn p
Theorem: Lean4Axiomatic.Rational.sgn_idemp
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
a b : ℤ
b_nonzero✝ : Integer.Nonzero b
eqv : p ≃ from_integer a / from_integer b
⊢ sgn (sgn p) ≃ sgn p
Tactic:
have : p ≃ a/b := eqv
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
a b : ℤ
b_nonzero✝ : Integer.Nonzero b
eqv this : p ≃ from_integer a / from_integer b
⊢ sgn (sgn p) ≃ sgn p
Theorem: Lean4Axiomatic.Rational.sgn_idemp
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
a b : ℤ
b_nonzero✝ : Integer.Nonzero b
eqv this : p ≃ from_integer a / from_integer b
⊢ sgn (sgn p) ≃ sgn p
Tactic:
calc
  sgn (sgn p)               ≃ _ := Integer.sgn_subst (sgn_subst ‹p ≃ a/b›)
  sgn (sgn ((a : ℚ)/b))     ≃ _ := Integer.sgn_subst sgn_div_integers
  sgn (sgn a * sgn b)       ≃ _ := Integer.sgn_compat_mul
  sgn (sgn a) * sgn (sgn b) ≃ _ := AA.substL Integer.sgn_idemp
  sgn a * sgn (sgn b)       ≃ _ := AA.substR Integer.sgn_idemp
  sgn a * sgn b             ≃ _ := Rel.symm sgn_div_integers
  sgn ((a : ℚ)/b)           ≃ _ := sgn_subst (eqv_symm ‹p ≃ a/b›)
  sgn p                     ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.sgn_sqrt1_iff_nonzero
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
⊢ Integer.Sqrt1 (sgn p) ↔ p ≄ 0
Tactic:
have : Integer.Sqrt1 (sgn (sgn p)) ↔ Integer.Sqrt1 (sgn p) :=
  Rel.iff_subst_eqv Integer.sqrt1_subst sgn_idemp
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
this : Integer.Sqrt1 (sgn (sgn p)) ↔ Integer.Sqrt1 (sgn p)
⊢ Integer.Sqrt1 (sgn p) ↔ p ≄ 0
Theorem: Lean4Axiomatic.Rational.sgn_sqrt1_iff_nonzero
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
this : Integer.Sqrt1 (sgn (sgn p)) ↔ Integer.Sqrt1 (sgn p)
⊢ Integer.Sqrt1 (sgn p) ↔ p ≄ 0
Tactic:
calc
  _ ↔ Integer.Sqrt1 (sgn p)       := Rel.refl
  _ ↔ Integer.Sqrt1 (sgn (sgn p)) := this.symm
  _ ↔ Integer.Nonzero (sgn p)     := Integer.sgn_nonzero.symm
  _ ↔ sgn p ≄ 0                   := Integer.nonzero_iff_neqv_zero
  _ ↔ p ≄ 0                       := Logic.iff_subst_contra mt sgn_zero.symm
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.sgn_sub_cancelR_div_pos
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ 1)
⊢ sgn (p / r - q / r) ≃ sgn (p - q)
Tactic:
have : sgn (r⁻¹) ≃ 1 := Rel.trans sgn_recip ‹AP (sgn r ≃ 1)›.ev
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ 1)
this : sgn (r⁻¹) ≃ 1
⊢ sgn (p / r - q / r) ≃ sgn (p - q)
Theorem: Lean4Axiomatic.Rational.sgn_sub_cancelR_div_pos
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ 1)
this : sgn (r⁻¹) ≃ 1
⊢ sgn (p / r - q / r) ≃ sgn (p - q)
Tactic:
calc
  _ ≃ sgn (p/r - q/r)         := Rel.refl
  _ ≃ sgn (p * r⁻¹ - q/r)     := sgn_subst (sub_substL div_mul_recip)
  _ ≃ sgn (p * r⁻¹ - q * r⁻¹) := sgn_subst (sub_substR div_mul_recip)
  _ ≃ sgn (p - q)             := sgn_sub_cancelR_mul_pos this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.sgn_sub_cancelR_div_neg
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ -1)
⊢ sgn (p / r - q / r) ≃ sgn (q - p)
Tactic:
have : sgn (r⁻¹) ≃ -1 := Rel.trans sgn_recip ‹AP (sgn r ≃ -1)›.ev
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ -1)
this : sgn (r⁻¹) ≃ -1
⊢ sgn (p / r - q / r) ≃ sgn (q - p)
Theorem: Lean4Axiomatic.Rational.sgn_sub_cancelR_div_neg
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ -1)
this : sgn (r⁻¹) ≃ -1
⊢ sgn (p / r - q / r) ≃ sgn (q - p)
Tactic:
calc
  _ ≃ sgn (p/r - q/r)         := Rel.refl
  _ ≃ sgn (p * r⁻¹ - q/r)     := sgn_subst (sub_substL div_mul_recip)
  _ ≃ sgn (p * r⁻¹ - q * r⁻¹) := sgn_subst (sub_substR div_mul_recip)
  _ ≃ sgn (q - p)             := sgn_sub_cancelR_mul_neg this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.nonneg_square
Proof 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)
Proof 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
Theorem: Lean4Axiomatic.Rational.nonneg_square
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Rational.nonneg_square
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Rational.nonneg_square
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Rational.nonneg_square
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Rational.nonneg_square
Proof 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)›
Proof 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
Theorem: Lean4Axiomatic.Rational.nonneg_square
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Rational.nonneg_square
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Rational.nonneg_square
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.mul_split_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
⊢ p * q ≃ 0 ↔ p ≃ 0 ∨ q ≃ 0
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
⊢ p * q ≃ 0 → p ≃ 0 ∨ q ≃ 0

case mpr
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
⊢ p ≃ 0 ∨ q ≃ 0 → p * q ≃ 0
Theorem: Lean4Axiomatic.Rational.mul_split_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
⊢ p * q ≃ 0 → p ≃ 0 ∨ q ≃ 0
Tactic:
case mp =>
  intro (_ : p * q ≃ 0)
  show p ≃ 0 ∨ q ≃ 0
  have : sgn p * sgn q ≃ 0 := calc
    sgn p * sgn q ≃ _ := Rel.symm sgn_compat_mul
    sgn (p * q)   ≃ _ := sgn_zero.mp ‹p * q ≃ 0›
    0             ≃ _ := Rel.refl
  have : sgn p ≃ 0 ∨ sgn q ≃ 0 := Integer.mul_split_zero.mp this
  have : p ≃ 0 ∨ q ≃ 0 := match this with
  | Or.inl (_ : sgn p ≃ 0) =>
    have : p ≃ 0 := sgn_zero.mpr ‹sgn p ≃ 0›
    Or.inl this
  | Or.inr (_ : sgn q ≃ 0) =>
    have : q ≃ 0 := sgn_zero.mpr ‹sgn q ≃ 0›
    Or.inr this
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.mul_split_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
⊢ p ≃ 0 ∨ q ≃ 0 → p * q ≃ 0
Tactic:
case mpr =>
  intro (_ : p ≃ 0 ∨ q ≃ 0)
  show p * q ≃ 0
  match ‹p ≃ 0 ∨ q ≃ 0› with
  | Or.inl (_ : p ≃ 0) => calc
    p * q ≃ _ := mul_substL ‹p ≃ 0›
    0 * q ≃ _ := mul_absorbL
    0     ≃ _ := eqv_refl
  | Or.inr (_ : q ≃ 0) => calc
    p * q ≃ _ := mul_substR ‹q ≃ 0›
    p * 0 ≃ _ := mul_absorbR
    0     ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.mul_split_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
⊢ p * q ≃ 0 → p ≃ 0 ∨ q ≃ 0
Tactic:
intro (_ : p * q ≃ 0)
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
x✝ : p * q ≃ 0
⊢ p ≃ 0 ∨ q ≃ 0
Theorem: Lean4Axiomatic.Rational.mul_split_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
x✝ : p * q ≃ 0
⊢ p ≃ 0 ∨ q ≃ 0
Tactic:
have : sgn p * sgn q ≃ 0 := calc
  sgn p * sgn q ≃ _ := Rel.symm sgn_compat_mul
  sgn (p * q)   ≃ _ := sgn_zero.mp ‹p * q ≃ 0›
  0             ≃ _ := Rel.refl
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
x✝ : p * q ≃ 0
this : sgn p * sgn q ≃ 0
⊢ p ≃ 0 ∨ q ≃ 0
Theorem: Lean4Axiomatic.Rational.mul_split_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
x✝ : p * q ≃ 0
this : sgn p * sgn q ≃ 0
⊢ p ≃ 0 ∨ q ≃ 0
Tactic:
have : sgn p ≃ 0 ∨ sgn q ≃ 0 := Integer.mul_split_zero.mp this
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
x✝ : p * q ≃ 0
this✝ : sgn p * sgn q ≃ 0
this : sgn p ≃ 0 ∨ sgn q ≃ 0
⊢ p ≃ 0 ∨ q ≃ 0
Theorem: Lean4Axiomatic.Rational.mul_split_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
x✝ : p * q ≃ 0
this✝ : sgn p * sgn q ≃ 0
this : sgn p ≃ 0 ∨ sgn q ≃ 0
⊢ p ≃ 0 ∨ q ≃ 0
Tactic:
have : p ≃ 0 ∨ q ≃ 0 := match this with
| Or.inl (_ : sgn p ≃ 0) =>
  have : p ≃ 0 := sgn_zero.mpr ‹sgn p ≃ 0›
  Or.inl this
| Or.inr (_ : sgn q ≃ 0) =>
  have : q ≃ 0 := sgn_zero.mpr ‹sgn q ≃ 0›
  Or.inr this
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
x✝ : p * q ≃ 0
this✝¹ : sgn p * sgn q ≃ 0
this✝ : sgn p ≃ 0 ∨ sgn q ≃ 0
this : p ≃ 0 ∨ q ≃ 0
⊢ p ≃ 0 ∨ q ≃ 0