internlm/Lean-Github huggingface dataset:
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaNeg : x - a < 0
ybPos : 0 < y - b
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
nlinarith
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaZero : x - a = 0
ybNeg : y - b < 0
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
have xaZero' := le_of_eq xaZero
Proof state after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaZero : x - a = 0
ybNeg : y - b < 0
xaZero' : x - a ≤ 0
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaZero : x - a = 0
ybNeg : y - b < 0
xaZero' : x - a ≤ 0
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
simp at xaZero'
Proof state after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaZero : x - a = 0
ybNeg : y - b < 0
xaZero' : x ≤ a
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaZero : x - a = 0
ybNeg : y - b < 0
xaZero' : x ≤ a
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
have ybNeg' := le_of_lt ybNeg
Proof state after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaZero : x - a = 0
ybNeg : y - b < 0
xaZero' : x ≤ a
ybNeg' : y - b ≤ 0
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaZero : x - a = 0
ybNeg : y - b < 0
xaZero' : x ≤ a
ybNeg' : y - b ≤ 0
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
simp at ybNeg'
Proof state after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaZero : x - a = 0
ybNeg : y - b < 0
xaZero' : x ≤ a
ybNeg' : y ≤ b
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaZero : x - a = 0
ybNeg : y - b < 0
xaZero' : x ≤ a
ybNeg' : y ≤ b
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
exact Or.inl (And.intro xaZero' ybNeg')
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaZero : x - a = 0
ybZero : y - b = 0
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
have xaZero' := le_of_eq xaZero
Proof state after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaZero : x - a = 0
ybZero : y - b = 0
xaZero' : x - a ≤ 0
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaZero : x - a = 0
ybZero : y - b = 0
xaZero' : x - a ≤ 0
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
simp at xaZero'
Proof state after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaZero : x - a = 0
ybZero : y - b = 0
xaZero' : x ≤ a
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaZero : x - a = 0
ybZero : y - b = 0
xaZero' : x ≤ a
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
have ybZero' := le_of_eq ybZero
Proof state after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaZero : x - a = 0
ybZero : y - b = 0
xaZero' : x ≤ a
ybZero' : y - b ≤ 0
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaZero : x - a = 0
ybZero : y - b = 0
xaZero' : x ≤ a
ybZero' : y - b ≤ 0
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
simp at ybZero'
Proof state after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaZero : x - a = 0
ybZero : y - b = 0
xaZero' : x ≤ a
ybZero' : y ≤ b
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaZero : x - a = 0
ybZero : y - b = 0
xaZero' : x ≤ a
ybZero' : y ≤ b
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
exact Or.inl (And.intro xaZero' ybZero')
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaZero : x - a = 0
ybPos : 0 < y - b
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
have xaZero' := ge_of_eq xaZero
Proof state after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaZero : x - a = 0
ybPos : 0 < y - b
xaZero' : x - a ≥ 0
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaZero : x - a = 0
ybPos : 0 < y - b
xaZero' : x - a ≥ 0
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
simp at xaZero'
Proof state after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaZero : x - a = 0
ybPos : 0 < y - b
xaZero' : a ≤ x
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaZero : x - a = 0
ybPos : 0 < y - b
xaZero' : a ≤ x
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
have ybPos' := le_of_lt ybPos
Proof state after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaZero : x - a = 0
ybPos : 0 < y - b
xaZero' : a ≤ x
ybPos' : 0 ≤ y - b
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaZero : x - a = 0
ybPos : 0 < y - b
xaZero' : a ≤ x
ybPos' : 0 ≤ y - b
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
simp at ybPos'
Proof state after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaZero : x - a = 0
ybPos : 0 < y - b
xaZero' : a ≤ x
ybPos' : b ≤ y
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaZero : x - a = 0
ybPos : 0 < y - b
xaZero' : a ≤ x
ybPos' : b ≤ y
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
exact Or.inr (And.intro xaZero' ybPos')
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaPos : 0 < x - a
ybNeg : y - b < 0
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
nlinarith
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaPos : 0 < x - a
ybZero : y - b = 0
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
have xaPos' := le_of_lt xaPos
Proof state after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaPos : 0 < x - a
ybZero : y - b = 0
xaPos' : 0 ≤ x - a
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaPos : 0 < x - a
ybZero : y - b = 0
xaPos' : 0 ≤ x - a
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
simp at xaPos'
Proof state after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaPos : 0 < x - a
ybZero : y - b = 0
xaPos' : a ≤ x
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaPos : 0 < x - a
ybZero : y - b = 0
xaPos' : a ≤ x
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
have ybZero' := ge_of_eq ybZero
Proof state after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaPos : 0 < x - a
ybZero : y - b = 0
xaPos' : a ≤ x
ybZero' : y - b ≥ 0
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaPos : 0 < x - a
ybZero : y - b = 0
xaPos' : a ≤ x
ybZero' : y - b ≥ 0
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
simp at ybZero'
Proof state after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaPos : 0 < x - a
ybZero : y - b = 0
xaPos' : a ≤ x
ybZero' : b ≤ y
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaPos : 0 < x - a
ybZero : y - b = 0
xaPos' : a ≤ x
ybZero' : b ≤ y
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
exact Or.inr (And.intro xaPos' ybZero')
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaPos : 0 < x - a
ybPos : 0 < y - b
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
have xaPos' := le_of_lt xaPos
Proof state after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaPos : 0 < x - a
ybPos : 0 < y - b
xaPos' : 0 ≤ x - a
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaPos : 0 < x - a
ybPos : 0 < y - b
xaPos' : 0 ≤ x - a
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
simp at xaPos'
Proof state after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaPos : 0 < x - a
ybPos : 0 < y - b
xaPos' : a ≤ x
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaPos : 0 < x - a
ybPos : 0 < y - b
xaPos' : a ≤ x
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
have ybPos' := le_of_lt ybPos
Proof state after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaPos : 0 < x - a
ybPos : 0 < y - b
xaPos' : a ≤ x
ybPos' : 0 ≤ y - b
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaPos : 0 < x - a
ybPos : 0 < y - b
xaPos' : a ≤ x
ybPos' : 0 ≤ y - b
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
simp at ybPos'
Proof state after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaPos : 0 < x - a
ybPos : 0 < y - b
xaPos' : a ≤ x
ybPos' : b ≤ y
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
xaPos : 0 < x - a
ybPos : 0 < y - b
xaPos' : a ≤ x
ybPos' : b ≤ y
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
exact Or.inr (And.intro xaPos' ybPos')
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithMulTangentMprUpper
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
h₁ : x ≤ a
h₂ : y ≤ b
⊢ x * y ≥ b * x + a * y - a * b
Tactic:
nlinarith
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithMulTangentMprUpper
Proof state before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
h₁ : x ≥ a
h₂ : y ≥ b
⊢ x * y ≥ b * x + a * y - a * b
Tactic:
nlinarith
Proof state after:
no goals
Theorem: lt
Proof state before:
⊢ "a" < "b"
Tactic:
decide
Proof state after:
no goals
Theorem: neg
Proof state before:
x : ℤ
⊢ - -x = x
Tactic:
smt_show <;> sorry
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.powNegEven
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
⊢ ∀ {k : ℕ} {z : α}, z < 0 → Even k → z ^ k > 0
Tactic:
intros k z h₁ h₂
Proof state after:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
k : ℕ
z : α
h₁ : z < 0
h₂ : Even k
⊢ z ^ k > 0
Theorem: Smt.Reconstruct.Arith.powNegEven
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
k : ℕ
z : α
h₁ : z < 0
h₂ : Even k
⊢ z ^ k > 0
Tactic:
cases k with
| zero    => simp
| succ k' =>
  have k'NotEven := Nat.even_add_one.mp h₂
  have k'Odd := Nat.odd_iff_not_even.mpr k'NotEven
  have rc := powNegOdd h₁ k'Odd
  simp [Pow.pow]
  have mulZ := arith_mul_neg_lt ⟨h₁, rc⟩
  simp at mulZ
  rw [pow_succ, mul_comm]
  exact mulZ
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.powNegEven
Proof state before:
case zero
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
h₂ : Even 0
⊢ z ^ 0 > 0
Tactic:
simp
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.powNegEven
Proof state before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
⊢ z ^ (k' + 1) > 0
Tactic:
have k'NotEven := Nat.even_add_one.mp h₂
Proof state after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
⊢ z ^ (k' + 1) > 0
Theorem: Smt.Reconstruct.Arith.powNegEven
Proof state before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
⊢ z ^ (k' + 1) > 0
Tactic:
have k'Odd := Nat.odd_iff_not_even.mpr k'NotEven
Proof state after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
k'Odd : Odd k'
⊢ z ^ (k' + 1) > 0
Theorem: Smt.Reconstruct.Arith.powNegEven
Proof state before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
k'Odd : Odd k'
⊢ z ^ (k' + 1) > 0
Tactic:
have rc := powNegOdd h₁ k'Odd
Proof state after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
k'Odd : Odd k'
rc : z ^ k' < 0
⊢ z ^ (k' + 1) > 0
Theorem: Smt.Reconstruct.Arith.powNegEven
Proof state before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
k'Odd : Odd k'
rc : z ^ k' < 0
⊢ z ^ (k' + 1) > 0
Tactic:
simp [Pow.pow]
Proof state after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
k'Odd : Odd k'
rc : z ^ k' < 0
⊢ 0 < z ^ (k' + 1)
Theorem: Smt.Reconstruct.Arith.powNegEven
Proof state before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
k'Odd : Odd k'
rc : z ^ k' < 0
⊢ 0 < z ^ (k' + 1)
Tactic:
have mulZ := arith_mul_neg_lt ⟨h₁, rc⟩
Proof state after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
k'Odd : Odd k'
rc : z ^ k' < 0
mulZ : z * z ^ k' > z * 0
⊢ 0 < z ^ (k' + 1)
Theorem: Smt.Reconstruct.Arith.powNegEven
Proof state before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
k'Odd : Odd k'
rc : z ^ k' < 0
mulZ : z * z ^ k' > z * 0
⊢ 0 < z ^ (k' + 1)
Tactic:
simp at mulZ
Proof state after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
k'Odd : Odd k'
rc : z ^ k' < 0
mulZ : 0 < z * z ^ k'
⊢ 0 < z ^ (k' + 1)
Theorem: Smt.Reconstruct.Arith.powNegEven
Proof state before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
k'Odd : Odd k'
rc : z ^ k' < 0
mulZ : 0 < z * z ^ k'
⊢ 0 < z ^ (k' + 1)
Tactic:
rw [pow_succ, mul_comm]
Proof state after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
k'Odd : Odd k'
rc : z ^ k' < 0
mulZ : 0 < z * z ^ k'
⊢ 0 < z * z ^ k'
Theorem: Smt.Reconstruct.Arith.powNegEven
Proof state before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
k'Odd : Odd k'
rc : z ^ k' < 0
mulZ : 0 < z * z ^ k'
⊢ 0 < z * z ^ k'
Tactic:
exact mulZ
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.powNegOdd
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
⊢ ∀ {k : ℕ} {z : α}, z < 0 → Odd k → z ^ k < 0
Tactic:
intros k z h₁ h₂
Proof state after:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
k : ℕ
z : α
h₁ : z < 0
h₂ : Odd k
⊢ z ^ k < 0
Theorem: Smt.Reconstruct.Arith.powNegOdd
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
k : ℕ
z : α
h₁ : z < 0
h₂ : Odd k
⊢ z ^ k < 0
Tactic:
cases k with
| zero    => simp at h₂
| succ k' =>
  simp at h₂
  have k'Even := of_not_not (mt Nat.even_add_one.mpr h₂)
  have rc := powNegEven h₁ k'Even
  simp [Int.pow]
  have mulZ := arith_mul_neg_lt ⟨h₁, rc⟩
  simp at mulZ
  rw [pow_succ, mul_comm]
  exact mulZ
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.powNegOdd
Proof state before:
case zero
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
h₂ : Odd 0
⊢ z ^ 0 < 0
Tactic:
simp at h₂
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.powNegOdd
Proof state before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Odd (k' + 1)
⊢ z ^ (k' + 1) < 0
Tactic:
simp at h₂
Proof state after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : ¬Even (k' + 1)
⊢ z ^ (k' + 1) < 0
Theorem: Smt.Reconstruct.Arith.powNegOdd
Proof state before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : ¬Even (k' + 1)
⊢ z ^ (k' + 1) < 0
Tactic:
have k'Even := of_not_not (mt Nat.even_add_one.mpr h₂)
Proof state after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : ¬Even (k' + 1)
k'Even : Even k'
⊢ z ^ (k' + 1) < 0
Theorem: Smt.Reconstruct.Arith.powNegOdd
Proof state before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : ¬Even (k' + 1)
k'Even : Even k'
⊢ z ^ (k' + 1) < 0
Tactic:
have rc := powNegEven h₁ k'Even
Proof state after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : ¬Even (k' + 1)
k'Even : Even k'
rc : z ^ k' > 0
⊢ z ^ (k' + 1) < 0
Theorem: Smt.Reconstruct.Arith.powNegOdd
Proof state before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : ¬Even (k' + 1)
k'Even : Even k'
rc : z ^ k' > 0
⊢ z ^ (k' + 1) < 0
Tactic:
have mulZ := arith_mul_neg_lt ⟨h₁, rc⟩
Proof state after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : ¬Even (k' + 1)
k'Even : Even k'
rc : z ^ k' > 0
mulZ : z * 0 > z * z ^ k'
⊢ z ^ (k' + 1) < 0
Theorem: Smt.Reconstruct.Arith.powNegOdd
Proof state before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : ¬Even (k' + 1)
k'Even : Even k'
rc : z ^ k' > 0
mulZ : z * 0 > z * z ^ k'
⊢ z ^ (k' + 1) < 0
Tactic:
simp at mulZ
Proof state after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : ¬Even (k' + 1)
k'Even : Even k'
rc : z ^ k' > 0
mulZ : z * z ^ k' < 0
⊢ z ^ (k' + 1) < 0
Theorem: Smt.Reconstruct.Arith.powNegOdd
Proof state before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : ¬Even (k' + 1)
k'Even : Even k'
rc : z ^ k' > 0
mulZ : z * z ^ k' < 0
⊢ z ^ (k' + 1) < 0
Tactic:
rw [pow_succ, mul_comm]
Proof state after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : ¬Even (k' + 1)
k'Even : Even k'
rc : z ^ k' > 0
mulZ : z * z ^ k' < 0
⊢ z * z ^ k' < 0
Theorem: Smt.Reconstruct.Arith.powNegOdd
Proof state before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : ¬Even (k' + 1)
k'Even : Even k'
rc : z ^ k' > 0
mulZ : z * z ^ k' < 0
⊢ z * z ^ k' < 0
Tactic:
exact mulZ
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.powPos
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
⊢ ∀ {k : ℕ} {z : α}, z > 0 → z ^ k > 0
Tactic:
intro k z h
Proof state after:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
k : ℕ
z : α
h : z > 0
⊢ z ^ k > 0
Theorem: Smt.Reconstruct.Arith.powPos
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
k : ℕ
z : α
h : z > 0
⊢ z ^ k > 0
Tactic:
cases k with
| zero    => simp
| succ k' =>
  have ih := @powPos k' z h
  rw [pow_succ]
  have h₂ := arith_mul_pos_lt ⟨h, ih⟩
  simp at h₂
  rw [mul_comm]
  exact h₂
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.powPos
Proof state before:
case zero
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h : z > 0
⊢ z ^ 0 > 0
Tactic:
simp
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.powPos
Proof state before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h : z > 0
k' : ℕ
⊢ z ^ (k' + 1) > 0
Tactic:
have ih := @powPos k' z h
Proof state after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h : z > 0
k' : ℕ
ih : z ^ k' > 0
⊢ z ^ (k' + 1) > 0
Theorem: Smt.Reconstruct.Arith.powPos
Proof state before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h : z > 0
k' : ℕ
ih : z ^ k' > 0
⊢ z ^ (k' + 1) > 0
Tactic:
rw [pow_succ]
Proof state after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h : z > 0
k' : ℕ
ih : z ^ k' > 0
⊢ z ^ k' * z > 0
Theorem: Smt.Reconstruct.Arith.powPos
Proof state before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h : z > 0
k' : ℕ
ih : z ^ k' > 0
⊢ z ^ k' * z > 0
Tactic:
have h₂ := arith_mul_pos_lt ⟨h, ih⟩
Proof state after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h : z > 0
k' : ℕ
ih : z ^ k' > 0
h₂ : z * 0 < z * z ^ k'
⊢ z ^ k' * z > 0
Theorem: Smt.Reconstruct.Arith.powPos
Proof state before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h : z > 0
k' : ℕ
ih : z ^ k' > 0
h₂ : z * 0 < z * z ^ k'
⊢ z ^ k' * z > 0
Tactic:
simp at h₂
Proof state after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h : z > 0
k' : ℕ
ih : z ^ k' > 0
h₂ : 0 < z * z ^ k'
⊢ z ^ k' * z > 0
Theorem: Smt.Reconstruct.Arith.powPos
Proof state before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h : z > 0
k' : ℕ
ih : z ^ k' > 0
h₂ : 0 < z * z ^ k'
⊢ z ^ k' * z > 0
Tactic:
rw [mul_comm]
Proof state after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h : z > 0
k' : ℕ
ih : z ^ k' > 0
h₂ : 0 < z * z ^ k'
⊢ z * z ^ k' > 0