internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Rational.div_preserves_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 q : ℚ
inst✝ : AP (q ≄ 0)
x✝¹ : p ≄ 0
x✝ : p / q ≃ 0
⊢ False
Tactic:
have : p ≃ 0 := div_eqv_0.mp ‹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 : ℚ
inst✝ : AP (q ≄ 0)
x✝¹ : p ≄ 0
x✝ : p / q ≃ 0
this : p ≃ 0
⊢ False
Theorem: Lean4Axiomatic.Rational.div_preserves_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 q : ℚ
inst✝ : AP (q ≄ 0)
x✝¹ : p ≄ 0
x✝ : p / q ≃ 0
this : p ≃ 0
⊢ False
Tactic:
exact absurd ‹p ≃ 0› ‹p ≄ 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.add_preserves_sign
Proof 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)
Proof 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
Theorem: Lean4Axiomatic.Rational.add_preserves_sign
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Rational.add_preserves_sign
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Rational.add_preserves_sign
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Rational.add_preserves_sign
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Rational.add_preserves_sign
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Rational.add_preserves_sign
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Rational.add_preserves_sign
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Rational.add_preserves_sign
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Rational.add_preserves_sign
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Rational.add_preserves_sign
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Rational.add_preserves_sign
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Rational.add_preserves_sign
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.step_neqv
Proof state before:
ℕ : Type
inst✝¹ : Core ℕ
inst✝ : Induction ℕ
n : ℕ
⊢ step n ≄ n
Tactic:
apply ind_on (motive := λ n => step n ≄ n) n
Proof state after:
case zero
ℕ : Type
inst✝¹ : Core ℕ
inst✝ : Induction ℕ
n : ℕ
⊢ step 0 ≄ 0

case step
ℕ : Type
inst✝¹ : Core ℕ
inst✝ : Induction ℕ
n : ℕ
⊢ ∀ (m : ℕ), step m ≄ m → step (step m) ≄ step m
Theorem: Lean4Axiomatic.Natural.step_neqv
Proof state before:
ℕ : Type
inst✝¹ : Core ℕ
inst✝ : Induction ℕ
n : ℕ
⊢ step 0 ≄ 0
Tactic:
case zero =>
  show step 0 ≄ 0
  exact step_neqv_zero
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.step_neqv
Proof state before:
ℕ : Type
inst✝¹ : Core ℕ
inst✝ : Induction ℕ
n : ℕ
⊢ ∀ (m : ℕ), step m ≄ m → step (step m) ≄ step m
Tactic:
case step =>
  intro n (ih : step n ≄ n)
  show step (step n) ≄ step n
  intro (_ : step (step n) ≃ step n)
  show False
  apply ih
  show step n ≃ n
  exact AA.inject ‹step (step n) ≃ step n›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.step_neqv
Proof state before:
ℕ : Type
inst✝¹ : Core ℕ
inst✝ : Induction ℕ
n : ℕ
⊢ step 0 ≄ 0
Tactic:
exact step_neqv_zero
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.step_neqv
Proof state before:
ℕ : Type
inst✝¹ : Core ℕ
inst✝ : Induction ℕ
n : ℕ
⊢ ∀ (m : ℕ), step m ≄ m → step (step m) ≄ step m
Tactic:
intro n (ih : step n ≄ n)
Proof state after:
ℕ : Type
inst✝¹ : Core ℕ
inst✝ : Induction ℕ
n✝ n : ℕ
ih : step n ≄ n
⊢ step (step n) ≄ step n
Theorem: Lean4Axiomatic.Natural.step_neqv
Proof state before:
ℕ : Type
inst✝¹ : Core ℕ
inst✝ : Induction ℕ
n✝ n : ℕ
ih : step n ≄ n
⊢ step (step n) ≄ step n
Tactic:
intro (_ : step (step n) ≃ step n)
Proof state after:
ℕ : Type
inst✝¹ : Core ℕ
inst✝ : Induction ℕ
n✝ n : ℕ
ih : step n ≄ n
x✝ : step (step n) ≃ step n
⊢ False
Theorem: Lean4Axiomatic.Natural.step_neqv
Proof state before:
ℕ : Type
inst✝¹ : Core ℕ
inst✝ : Induction ℕ
n✝ n : ℕ
ih : step n ≄ n
x✝ : step (step n) ≃ step n
⊢ False
Tactic:
apply ih
Proof state after:
ℕ : Type
inst✝¹ : Core ℕ
inst✝ : Induction ℕ
n✝ n : ℕ
ih : step n ≄ n
x✝ : step (step n) ≃ step n
⊢ step n ≃ n
Theorem: Lean4Axiomatic.Natural.step_neqv
Proof state before:
ℕ : Type
inst✝¹ : Core ℕ
inst✝ : Induction ℕ
n✝ n : ℕ
ih : step n ≄ n
x✝ : step (step n) ≃ step n
⊢ step n ≃ n
Tactic:
exact AA.inject ‹step (step n) ≃ step n›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.pow_substL_ge_nonneg
Proof state before:
ℕ ℤ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
ℚ : Type
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Multiplication ℚ
inst✝⁷ : Negation ℚ
inst✝⁶ : Subtraction ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : Metric ℚ
inst✝ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
p q : ℚ
n : ℕ
⊢ p ≥ q ∧ q ≥ 0 → p ^ n ≥ q ^ n ∧ q ^ n ≥ 0
Tactic:
intro (And.intro (_ : p ≥ q) (_ : q ≥ 0))
Proof state after:
ℕ ℤ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
ℚ : Type
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Multiplication ℚ
inst✝⁷ : Negation ℚ
inst✝⁶ : Subtraction ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : Metric ℚ
inst✝ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
p q : ℚ
n : ℕ
left✝ : p ≥ q
right✝ : q ≥ 0
⊢ p ^ n ≥ q ^ n ∧ q ^ n ≥ 0
Theorem: Lean4Axiomatic.Rational.pow_substL_ge_nonneg
Proof state before:
ℕ ℤ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
ℚ : Type
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Multiplication ℚ
inst✝⁷ : Negation ℚ
inst✝⁶ : Subtraction ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : Metric ℚ
inst✝ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
p q : ℚ
n : ℕ
left✝ : p ≥ q
right✝ : q ≥ 0
⊢ p ^ n ≥ q ^ n ∧ q ^ n ≥ 0
Tactic:
apply Natural.ind_on n
Proof state after:
case zero
ℕ ℤ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
ℚ : Type
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Multiplication ℚ
inst✝⁷ : Negation ℚ
inst✝⁶ : Subtraction ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : Metric ℚ
inst✝ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
p q : ℚ
n : ℕ
left✝ : p ≥ q
right✝ : q ≥ 0
⊢ p ^ 0 ≥ q ^ 0 ∧ q ^ 0 ≥ 0

case step
ℕ ℤ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
ℚ : Type
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Multiplication ℚ
inst✝⁷ : Negation ℚ
inst✝⁶ : Subtraction ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : Metric ℚ
inst✝ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
p q : ℚ
n : ℕ
left✝ : p ≥ q
right✝ : q ≥ 0
⊢ ∀ (m : ℕ), p ^ m ≥ q ^ m ∧ q ^ m ≥ 0 → p ^ step m ≥ q ^ step m ∧ q ^ step m ≥ 0
Theorem: Lean4Axiomatic.Rational.pow_substL_ge_nonneg
Proof state before:
ℕ ℤ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
ℚ : Type
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Multiplication ℚ
inst✝⁷ : Negation ℚ
inst✝⁶ : Subtraction ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : Metric ℚ
inst✝ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
p q : ℚ
n : ℕ
left✝ : p ≥ q
right✝ : q ≥ 0
⊢ p ^ 0 ≥ q ^ 0 ∧ q ^ 0 ≥ 0
Tactic:
case zero =>
  show p^0 ≥ q^0 ∧ q^0 ≥ 0
  have : p^(0:ℕ) ≥ q^(0:ℕ) := calc
    _ ≃ p^0 := eqv_refl
    _ ≃ 1   := pow_zero
    _ ≃ q^0 := eqv_symm pow_zero
    _ ≥ q^0 := le_refl
  have : q^(0:ℕ) ≥ 0 := calc
    _ ≃ q^0 := eqv_refl
    _ ≃ 1   := pow_zero
    _ ≥ 0   := one_ge_zero
  exact And.intro ‹p^(0:ℕ) ≥ q^(0:ℕ)› ‹q^(0:ℕ) ≥ 0›
Proof state after:
no goals