internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Integer.positive_mul_iff_same_sign
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
ab : ℤ := a * b
x✝ : Positive ab
this✝² : Nonzero ab
left✝ : Nonzero a
right✝ : Nonzero b
sa : ℤ
sqrt1✝¹ : Sqrt1 sa
nwsa : NonzeroWithSign a sa
sb : ℤ
sqrt1✝ : Sqrt1 sb
nwsb : NonzeroWithSign b sb
this✝¹ : NonzeroWithSign a sa
this✝ : NonzeroWithSign b sb
nwsac : NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1)
nwsbc : NonzeroWithSign b 1 ∨ NonzeroWithSign b (-1)
this : SameSign a b ∨ NonzeroWithSign ab (-1)
h✝ : NonzeroWithSign ab (-1)
⊢ SameSign a b
Tactic:
have : Negative ab :=
  negative_iff_sign_neg1.mpr ‹NonzeroWithSign ab (-1)›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
ab : ℤ := a * b
x✝ : Positive ab
this✝³ : Nonzero ab
left✝ : Nonzero a
right✝ : Nonzero b
sa : ℤ
sqrt1✝¹ : Sqrt1 sa
nwsa : NonzeroWithSign a sa
sb : ℤ
sqrt1✝ : Sqrt1 sb
nwsb : NonzeroWithSign b sb
this✝² : NonzeroWithSign a sa
this✝¹ : NonzeroWithSign b sb
nwsac : NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1)
nwsbc : NonzeroWithSign b 1 ∨ NonzeroWithSign b (-1)
this✝ : SameSign a b ∨ NonzeroWithSign ab (-1)
h✝ : NonzeroWithSign ab (-1)
this : Negative ab
⊢ SameSign a b
Theorem: Lean4Axiomatic.Integer.positive_mul_iff_same_sign
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
ab : ℤ := a * b
x✝ : Positive ab
this✝³ : Nonzero ab
left✝ : Nonzero a
right✝ : Nonzero b
sa : ℤ
sqrt1✝¹ : Sqrt1 sa
nwsa : NonzeroWithSign a sa
sb : ℤ
sqrt1✝ : Sqrt1 sb
nwsb : NonzeroWithSign b sb
this✝² : NonzeroWithSign a sa
this✝¹ : NonzeroWithSign b sb
nwsac : NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1)
nwsbc : NonzeroWithSign b 1 ∨ NonzeroWithSign b (-1)
this✝ : SameSign a b ∨ NonzeroWithSign ab (-1)
h✝ : NonzeroWithSign ab (-1)
this : Negative ab
⊢ SameSign a b
Tactic:
have positive_and_negative : Positive ab ∧ Negative ab :=
  And.intro ‹Positive ab› ‹Negative ab›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
ab : ℤ := a * b
x✝ : Positive ab
this✝³ : Nonzero ab
left✝ : Nonzero a
right✝ : Nonzero b
sa : ℤ
sqrt1✝¹ : Sqrt1 sa
nwsa : NonzeroWithSign a sa
sb : ℤ
sqrt1✝ : Sqrt1 sb
nwsb : NonzeroWithSign b sb
this✝² : NonzeroWithSign a sa
this✝¹ : NonzeroWithSign b sb
nwsac : NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1)
nwsbc : NonzeroWithSign b 1 ∨ NonzeroWithSign b (-1)
this✝ : SameSign a b ∨ NonzeroWithSign ab (-1)
h✝ : NonzeroWithSign ab (-1)
this : Negative ab
positive_and_negative : Positive ab ∧ Negative ab
⊢ SameSign a b
Theorem: Lean4Axiomatic.Integer.positive_mul_iff_same_sign
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
ab : ℤ := a * b
x✝ : Positive ab
this✝³ : Nonzero ab
left✝ : Nonzero a
right✝ : Nonzero b
sa : ℤ
sqrt1✝¹ : Sqrt1 sa
nwsa : NonzeroWithSign a sa
sb : ℤ
sqrt1✝ : Sqrt1 sb
nwsb : NonzeroWithSign b sb
this✝² : NonzeroWithSign a sa
this✝¹ : NonzeroWithSign b sb
nwsac : NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1)
nwsbc : NonzeroWithSign b 1 ∨ NonzeroWithSign b (-1)
this✝ : SameSign a b ∨ NonzeroWithSign ab (-1)
h✝ : NonzeroWithSign ab (-1)
this : Negative ab
positive_and_negative : Positive ab ∧ Negative ab
⊢ SameSign a b
Tactic:
exact absurd positive_and_negative not_positive_and_negative
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.positive_mul_iff_same_sign
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
ab : ℤ := a * b
⊢ SameSign a b → Positive (a * b)
Tactic:
intro (_ : SameSign a b)
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
ab : ℤ := a * b
x✝ : SameSign a b
⊢ Positive (a * b)
Theorem: Lean4Axiomatic.Integer.positive_mul_iff_same_sign
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
ab : ℤ := a * b
x✝ : SameSign a b
⊢ Positive (a * b)
Tactic:
show Positive ab
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
ab : ℤ := a * b
x✝ : SameSign a b
⊢ Positive ab
Theorem: Lean4Axiomatic.Integer.positive_mul_iff_same_sign
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
ab : ℤ := a * b
x✝ : SameSign a b
⊢ Positive ab
Tactic:
have (SameSign.intro (s : ℤ) (_ : Sqrt1 s) nwsa nwsb) := ‹SameSign a b›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
ab : ℤ := a * b
x✝ : SameSign a b
s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
⊢ Positive ab
Theorem: Lean4Axiomatic.Integer.positive_mul_iff_same_sign
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
ab : ℤ := a * b
x✝ : SameSign a b
s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
⊢ Positive ab
Tactic:
have : NonzeroWithSign a s := nwsa
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
ab : ℤ := a * b
x✝ : SameSign a b
s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this : NonzeroWithSign a s
⊢ Positive ab
Theorem: Lean4Axiomatic.Integer.positive_mul_iff_same_sign
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
ab : ℤ := a * b
x✝ : SameSign a b
s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this : NonzeroWithSign a s
⊢ Positive ab
Tactic:
have : NonzeroWithSign b s := nwsb
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
ab : ℤ := a * b
x✝ : SameSign a b
s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝ : NonzeroWithSign a s
this : NonzeroWithSign b s
⊢ Positive ab
Theorem: Lean4Axiomatic.Integer.positive_mul_iff_same_sign
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
ab : ℤ := a * b
x✝ : SameSign a b
s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝ : NonzeroWithSign a s
this : NonzeroWithSign b s
⊢ Positive ab
Tactic:
have : s * s ≃ 1 := ‹Sqrt1 s›.elim
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
ab : ℤ := a * b
x✝ : SameSign a b
s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝¹ : NonzeroWithSign a s
this✝ : NonzeroWithSign b s
this : s * s ≃ 1
⊢ Positive ab
Theorem: Lean4Axiomatic.Integer.positive_mul_iff_same_sign
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
ab : ℤ := a * b
x✝ : SameSign a b
s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝¹ : NonzeroWithSign a s
this✝ : NonzeroWithSign b s
this : s * s ≃ 1
⊢ Positive ab
Tactic:
have : NonzeroWithSign ab (s * s) :=
  mul_preserves_nonzeroWithSign nwsa nwsb
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
ab : ℤ := a * b
x✝ : SameSign a b
s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝² : NonzeroWithSign a s
this✝¹ : NonzeroWithSign b s
this✝ : s * s ≃ 1
this : NonzeroWithSign ab (s * s)
⊢ Positive ab
Theorem: Lean4Axiomatic.Integer.positive_mul_iff_same_sign
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
ab : ℤ := a * b
x✝ : SameSign a b
s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝² : NonzeroWithSign a s
this✝¹ : NonzeroWithSign b s
this✝ : s * s ≃ 1
this : NonzeroWithSign ab (s * s)
⊢ Positive ab
Tactic:
have : NonzeroWithSign ab 1 :=
  NonzeroWithSign.subst_sign ‹s * s ≃ 1› ‹NonzeroWithSign ab (s * s)›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
ab : ℤ := a * b
x✝ : SameSign a b
s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝³ : NonzeroWithSign a s
this✝² : NonzeroWithSign b s
this✝¹ : s * s ≃ 1
this✝ : NonzeroWithSign ab (s * s)
this : NonzeroWithSign ab 1
⊢ Positive ab
Theorem: Lean4Axiomatic.Integer.positive_mul_iff_same_sign
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
ab : ℤ := a * b
x✝ : SameSign a b
s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝³ : NonzeroWithSign a s
this✝² : NonzeroWithSign b s
this✝¹ : s * s ≃ 1
this✝ : NonzeroWithSign ab (s * s)
this : NonzeroWithSign ab 1
⊢ Positive ab
Tactic:
have : Positive ab := positive_iff_sign_pos1.mpr ‹NonzeroWithSign ab 1›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
ab : ℤ := a * b
x✝ : SameSign a b
s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝⁴ : NonzeroWithSign a s
this✝³ : NonzeroWithSign b s
this✝² : s * s ≃ 1
this✝¹ : NonzeroWithSign ab (s * s)
this✝ : NonzeroWithSign ab 1
this : Positive ab
⊢ Positive ab
Theorem: Lean4Axiomatic.Integer.positive_mul_iff_same_sign
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
ab : ℤ := a * b
x✝ : SameSign a b
s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝⁴ : NonzeroWithSign a s
this✝³ : NonzeroWithSign b s
this✝² : s * s ≃ 1
this✝¹ : NonzeroWithSign ab (s * s)
this✝ : NonzeroWithSign ab 1
this : Positive ab
⊢ Positive ab
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.add_preserves_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
⊢ Positive a → Positive b → Positive (a + b)
Tactic:
intro (_ : Positive a) (_ : Positive b)
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝¹ : Positive a
x✝ : Positive b
⊢ Positive (a + b)
Theorem: Lean4Axiomatic.Integer.add_preserves_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝¹ : Positive a
x✝ : Positive b
⊢ Positive (a + b)
Tactic:
have : sgn a ≃ 1 := sgn_positive.mp ‹Positive a›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝¹ : Positive a
x✝ : Positive b
this : sgn a ≃ 1
⊢ Positive (a + b)
Theorem: Lean4Axiomatic.Integer.add_preserves_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝¹ : Positive a
x✝ : Positive b
this : sgn a ≃ 1
⊢ Positive (a + b)
Tactic:
have : sgn b ≃ 1 := sgn_positive.mp ‹Positive b›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝¹ : Positive a
x✝ : Positive b
this✝ : sgn a ≃ 1
this : sgn b ≃ 1
⊢ Positive (a + b)
Theorem: Lean4Axiomatic.Integer.add_preserves_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝¹ : Positive a
x✝ : Positive b
this✝ : sgn a ≃ 1
this : sgn b ≃ 1
⊢ Positive (a + b)
Tactic:
have : sgn (a + b) ≃ 1 := add_preserves_sign ‹sgn a ≃ 1› ‹sgn b ≃ 1›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝¹ : Positive a
x✝ : Positive b
this✝¹ : sgn a ≃ 1
this✝ : sgn b ≃ 1
this : sgn (a + b) ≃ 1
⊢ Positive (a + b)
Theorem: Lean4Axiomatic.Integer.add_preserves_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝¹ : Positive a
x✝ : Positive b
this✝¹ : sgn a ≃ 1
this✝ : sgn b ≃ 1
this : sgn (a + b) ≃ 1
⊢ Positive (a + b)
Tactic:
have : Positive (a + b) := sgn_positive.mpr this
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝¹ : Positive a
x✝ : Positive b
this✝² : sgn a ≃ 1
this✝¹ : sgn b ≃ 1
this✝ : sgn (a + b) ≃ 1
this : Positive (a + b)
⊢ Positive (a + b)
Theorem: Lean4Axiomatic.Integer.add_preserves_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝¹ : Positive a
x✝ : Positive b
this✝² : sgn a ≃ 1
this✝¹ : sgn b ≃ 1
this✝ : sgn (a + b) ≃ 1
this : Positive (a + b)
⊢ Positive (a + b)
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.mul_preserves_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
⊢ Positive a → Positive b → Positive (a * b)
Tactic:
intro (_ : Positive a) (_ : Positive b)
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝¹ : Positive a
x✝ : Positive b
⊢ Positive (a * b)
Theorem: Lean4Axiomatic.Integer.mul_preserves_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝¹ : Positive a
x✝ : Positive b
⊢ Positive (a * b)
Tactic:
have : NonzeroWithSign a 1 := positive_iff_sign_pos1.mp ‹Positive a›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝¹ : Positive a
x✝ : Positive b
this : NonzeroWithSign a 1
⊢ Positive (a * b)
Theorem: Lean4Axiomatic.Integer.mul_preserves_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝¹ : Positive a
x✝ : Positive b
this : NonzeroWithSign a 1
⊢ Positive (a * b)
Tactic:
have : NonzeroWithSign b 1 := positive_iff_sign_pos1.mp ‹Positive b›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝¹ : Positive a
x✝ : Positive b
this✝ : NonzeroWithSign a 1
this : NonzeroWithSign b 1
⊢ Positive (a * b)
Theorem: Lean4Axiomatic.Integer.mul_preserves_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝¹ : Positive a
x✝ : Positive b
this✝ : NonzeroWithSign a 1
this : NonzeroWithSign b 1
⊢ Positive (a * b)
Tactic:
have : SameSign a b :=
  SameSign.mk ‹NonzeroWithSign a 1› ‹NonzeroWithSign b 1›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝¹ : Positive a
x✝ : Positive b
this✝¹ : NonzeroWithSign a 1
this✝ : NonzeroWithSign b 1
this : SameSign a b
⊢ Positive (a * b)
Theorem: Lean4Axiomatic.Integer.mul_preserves_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝¹ : Positive a
x✝ : Positive b
this✝¹ : NonzeroWithSign a 1
this✝ : NonzeroWithSign b 1
this : SameSign a b
⊢ Positive (a * b)
Tactic:
have : Positive (a * b) := positive_mul_iff_same_sign.mpr ‹SameSign a b›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝¹ : Positive a
x✝ : Positive b
this✝² : NonzeroWithSign a 1
this✝¹ : NonzeroWithSign b 1
this✝ : SameSign a b
this : Positive (a * b)
⊢ Positive (a * b)
Theorem: Lean4Axiomatic.Integer.mul_preserves_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝¹ : Positive a
x✝ : Positive b
this✝² : NonzeroWithSign a 1
this✝¹ : NonzeroWithSign b 1
this✝ : SameSign a b
this : Positive (a * b)
⊢ Positive (a * b)
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.positive_iff_negated_negative
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Positive a ↔ Negative (-a)
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Positive a → Negative (-a)

case mpr
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Negative (-a) → Positive a
Theorem: Lean4Axiomatic.Integer.positive_iff_negated_negative
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Positive a → Negative (-a)
Tactic:
case mp =>
  intro (_ : Positive a)
  show Negative (-a)
  have nwsa : NonzeroWithSign a 1 := positive_iff_sign_pos1.mp ‹Positive a›
  have : NonzeroWithSign a (-(-1)) :=
    NonzeroWithSign.subst_sign (Rel.symm neg_involutive) nwsa
  have : NonzeroWithSign (-a) (-1) :=
    nonzeroWithSign_swap_neg.mpr ‹NonzeroWithSign a (-(-1))›
  have : Negative (-a) :=
    negative_iff_sign_neg1.mpr ‹NonzeroWithSign (-a) (-1)›
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.positive_iff_negated_negative
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Negative (-a) → Positive a
Tactic:
case mpr =>
  intro (_ : Negative (-a))
  show Positive a
  have : NonzeroWithSign (-a) (-1) :=
    negative_iff_sign_neg1.mp ‹Negative (-a)›
  have : NonzeroWithSign a (-(-1)) :=
    nonzeroWithSign_swap_neg.mp ‹NonzeroWithSign (-a) (-1)›
  have : NonzeroWithSign a 1 :=
    NonzeroWithSign.subst_sign neg_involutive ‹NonzeroWithSign a (-(-1))›
  have : Positive a := positive_iff_sign_pos1.mpr ‹NonzeroWithSign a 1›
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.positive_iff_negated_negative
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Positive a → Negative (-a)
Tactic:
intro (_ : Positive a)
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a
⊢ Negative (-a)
Theorem: Lean4Axiomatic.Integer.positive_iff_negated_negative
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a
⊢ Negative (-a)
Tactic:
have nwsa : NonzeroWithSign a 1 := positive_iff_sign_pos1.mp ‹Positive a›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a
nwsa : NonzeroWithSign a 1
⊢ Negative (-a)
Theorem: Lean4Axiomatic.Integer.positive_iff_negated_negative
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a
nwsa : NonzeroWithSign a 1
⊢ Negative (-a)
Tactic:
have : NonzeroWithSign a (-(-1)) :=
  NonzeroWithSign.subst_sign (Rel.symm neg_involutive) nwsa
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a
nwsa : NonzeroWithSign a 1
this : NonzeroWithSign a (- -1)
⊢ Negative (-a)
Theorem: Lean4Axiomatic.Integer.positive_iff_negated_negative
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a
nwsa : NonzeroWithSign a 1
this : NonzeroWithSign a (- -1)
⊢ Negative (-a)
Tactic:
have : NonzeroWithSign (-a) (-1) :=
  nonzeroWithSign_swap_neg.mpr ‹NonzeroWithSign a (-(-1))›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a
nwsa : NonzeroWithSign a 1
this✝ : NonzeroWithSign a (- -1)
this : NonzeroWithSign (-a) (-1)
⊢ Negative (-a)
Theorem: Lean4Axiomatic.Integer.positive_iff_negated_negative
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a
nwsa : NonzeroWithSign a 1
this✝ : NonzeroWithSign a (- -1)
this : NonzeroWithSign (-a) (-1)
⊢ Negative (-a)
Tactic:
have : Negative (-a) :=
  negative_iff_sign_neg1.mpr ‹NonzeroWithSign (-a) (-1)›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a
nwsa : NonzeroWithSign a 1
this✝¹ : NonzeroWithSign a (- -1)
this✝ : NonzeroWithSign (-a) (-1)
this : Negative (-a)
⊢ Negative (-a)
Theorem: Lean4Axiomatic.Integer.positive_iff_negated_negative
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a
nwsa : NonzeroWithSign a 1
this✝¹ : NonzeroWithSign a (- -1)
this✝ : NonzeroWithSign (-a) (-1)
this : Negative (-a)
⊢ Negative (-a)
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.positive_iff_negated_negative
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Negative (-a) → Positive a
Tactic:
intro (_ : Negative (-a))
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Negative (-a)
⊢ Positive a