awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
n : ℕ
hx0 : x ≤ 0
zero :
  if Even (α := ℕ) 0 then LE.le.{u_1} (α := R) (∑ i ∈ range 0, x ^ i) 0
  else LE.le.{u_1} (α := R) 1 (∑ i ∈ range 0, x ^ i)
succ :
  ∀ (n : ℕ)
    (ih :
      if Even n then LE.le.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 else LE.le.{u_1} (α := R) 1 (∑ i ∈ range n, x ^ i)),
    if Even (n + 1) then LE.le.{u_1} (α := R) (∑ i ∈ range (n + 1), x ^ i) 0
    else LE.le.{u_1} (α := R) 1 (∑ i ∈ range (n + 1), x ^ i)
⊢ if Even n then LE.le.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 else LE.le.{u_1} (α := R) 1 (∑ i ∈ range n, x ^ i)

Tactic:
induction n with
  | zero => simp only [range_zero, sum_empty, le_refl, ite_true, Even.zero]
  | succ n ih =>
    simp only [Nat.even_add_one, geom_sum_succ]
    split_ifs at ih ⊢ with h
    · rw [le_add_iff_nonneg_left]
      exact mul_nonneg_of_nonpos_of_nonpos hx0 ih
    · grw [← hx]
      gcongr
      simpa only [mul_one] using mul_le_mul_of_nonpos_left ih hx0

Premises used: Nat.even_add_one, le_refl, Even.zero, ite_true, geom_sum_succ, Finset.sum_empty, mul_one, le_add_iff_nonneg_left, Finset.range_zero
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
hn : 1 < n
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ∧ LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 1

Tactic:
Nat.le_induction ?_ ?_ n (show 2 ≤ n from hn)

Premises used: Nat.le_induction
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
hn : 1 < n
refine_1 : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range 2, x ^ i) ∧ LT.lt.{u_1} (α := R) (∑ i ∈ range 2, x ^ i) 1
refine_2 :
  ∀ (n : ℕ) (hmn : 2 ≤ n),
    LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ∧ LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 1 →
      LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (n + 1), x ^ i) ∧ LT.lt.{u_1} (α := R) (∑ i ∈ range (n + 1), x ^ i) 1
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ∧ LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 1

Tactic:
refine Nat.le_induction ?_ ?_ n (show 2 ≤ n from hn)
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
hn : 1 < n
refine_1 : 0 < x + 1 ∧ x + 1 < 1
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range 2, x ^ i) ∧ LT.lt.{u_1} (α := R) (∑ i ∈ range 2, x ^ i) 1

Tactic:
rw [geom_sum_two]

Premises used: geom_sum_two
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
hn : 1 < n
⊢ 0 < x + 1 ∧ x + 1 < 1

Tactic:
⟨hx', (add_lt_iff_neg_right _).2 hx⟩

Premises used: Iff.mpr, add_lt_iff_neg_right, And.intro
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
hn : 1 < n
⊢ 0 < x + 1 ∧ x + 1 < 1

Tactic:
exact ⟨hx', (add_lt_iff_neg_right _).2 hx⟩
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
n_1 : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
n : ℕ
refine_2 :
  2 ≤ n →
    LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ∧ LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 1 →
      LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (n + 1), x ^ i) ∧ LT.lt.{u_1} (α := R) (∑ i ∈ range (n + 1), x ^ i) 1
⊢ ∀ (hmn : 2 ≤ n),
    LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ∧ LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 1 →
      LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (n + 1), x ^ i) ∧ LT.lt.{u_1} (α := R) (∑ i ∈ range (n + 1), x ^ i) 1

Tactic:
_
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
n_1 : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
n : ℕ
hmn : 2 ≤ n
ihn : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ∧ LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 1
refine_2 : -x * ∑ i ∈ range n, x ^ i < 1 ∧ x * ∑ i ∈ range n, x ^ i < 0
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (n + 1), x ^ i) ∧ LT.lt.{u_1} (α := R) (∑ i ∈ range (n + 1), x ^ i) 1

Tactic:
rw [geom_sum_succ, add_lt_iff_neg_right, ← neg_lt_iff_pos_add', neg_mul_eq_neg_mul]

Premises used: neg_lt_iff_pos_add', add_lt_iff_neg_right, geom_sum_succ, neg_mul_eq_neg_mul
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
n_1 : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
n : ℕ
hmn : 2 ≤ n
ihn : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ∧ LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 1
⊢ -x * ∑ i ∈ range n, x ^ i < 1 ∧ x * ∑ i ∈ range n, x ^ i < 0

Tactic:
⟨mul_lt_one_of_nonneg_of_lt_one_left (neg_nonneg.2 hx.le) (neg_lt_iff_pos_add'.2 hx') ihn.2.le,
      mul_neg_of_neg_of_pos hx ihn.1⟩

Premises used: Iff.mpr, mul_neg_of_neg_of_pos, mul_lt_one_of_nonneg_of_lt_one_left, LT.lt.le, neg_lt_iff_pos_add', neg_nonneg, And.right, And.left, And.intro
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
n_1 : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
n : ℕ
hmn : 2 ≤ n
ihn : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ∧ LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 1
⊢ -x * ∑ i ∈ range n, x ^ i < 1 ∧ x * ∑ i ∈ range n, x ^ i < 0

Tactic:
exact
    ⟨mul_lt_one_of_nonneg_of_lt_one_left (neg_nonneg.2 hx.le) (neg_lt_iff_pos_add'.2 hx') ihn.2.le,
      mul_neg_of_neg_of_pos hx ihn.1⟩
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hx : x + 1 < 0
hn : 1 < n
⊢ x < 0

Tactic:
have hx0 : x < 0 := (le_add_of_nonneg_right zero_le_one).trans_lt hx
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hx : x + 1 < 0
hn : 1 < n
hx0 : x < 0
⊢ if Even n then LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 else LT.lt.{u_1} (α := R) 1 (∑ i ∈ range n, x ^ i)

Tactic:
Nat.le_induction ?_ ?_ n (show 2 ≤ n from hn)

Premises used: Nat.le_induction
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hx : x + 1 < 0
hn : 1 < n
hx0 : x < 0
refine_1 :
  if Even (α := ℕ) 2 then LT.lt.{u_1} (α := R) (∑ i ∈ range 2, x ^ i) 0
  else LT.lt.{u_1} (α := R) 1 (∑ i ∈ range 2, x ^ i)
refine_2 :
  ∀ (n : ℕ) (hmn : 2 ≤ n),
    (if Even n then LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 else LT.lt.{u_1} (α := R) 1 (∑ i ∈ range n, x ^ i)) →
      if Even (n + 1) then LT.lt.{u_1} (α := R) (∑ i ∈ range (n + 1), x ^ i) 0
      else LT.lt.{u_1} (α := R) 1 (∑ i ∈ range (n + 1), x ^ i)
⊢ if Even n then LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 else LT.lt.{u_1} (α := R) 1 (∑ i ∈ range n, x ^ i)

Tactic:
refine Nat.le_induction ?_ ?_ n (show 2 ≤ n from hn)
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hx : x + 1 < 0
hn : 1 < n
hx0 : x < 0
⊢ if Even (α := ℕ) 2 then LT.lt.{u_1} (α := R) (∑ i ∈ range 2, x ^ i) 0
  else LT.lt.{u_1} (α := R) 1 (∑ i ∈ range 2, x ^ i)

Tactic:
simp only [geom_sum_two, lt_add_iff_pos_left, ite_true, hx, even_two]

Premises used: geom_sum_two, even_two, ite_true, lt_add_iff_pos_left
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
n_1 : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
refine_2 :
  2 ≤ n →
    (if Even n then LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 else LT.lt.{u_1} (α := R) 1 (∑ i ∈ range n, x ^ i)) →
      if Even (n + 1) then LT.lt.{u_1} (α := R) (∑ i ∈ range (n + 1), x ^ i) 0
      else LT.lt.{u_1} (α := R) 1 (∑ i ∈ range (n + 1), x ^ i)
⊢ ∀ (hmn : 2 ≤ n),
    (if Even n then LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 else LT.lt.{u_1} (α := R) 1 (∑ i ∈ range n, x ^ i)) →
      if Even (n + 1) then LT.lt.{u_1} (α := R) (∑ i ∈ range (n + 1), x ^ i) 0
      else LT.lt.{u_1} (α := R) 1 (∑ i ∈ range (n + 1), x ^ i)

Tactic:
_
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
n_1 : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn : 2 ≤ n
ihn : if Even n then LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 else LT.lt.{u_1} (α := R) 1 (∑ i ∈ range n, x ^ i)
refine_2 : if ¬Even n then x * ∑ i ∈ range n, x ^ i + 1 < 0 else 1 < x * ∑ i ∈ range n, x ^ i + 1
⊢ if Even (n + 1) then LT.lt.{u_1} (α := R) (∑ i ∈ range (n + 1), x ^ i) 0
  else LT.lt.{u_1} (α := R) 1 (∑ i ∈ range (n + 1), x ^ i)

Tactic:
simp only [Nat.even_add_one, geom_sum_succ]

Premises used: Nat.even_add_one, geom_sum_succ
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
n_1 : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn : 2 ≤ n
ihn : if Even n then LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 else LT.lt.{u_1} (α := R) 1 (∑ i ∈ range n, x ^ i)
pos : ∀ (hn' : Even n) (ihn : LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0), 1 < x * ∑ i ∈ range n, x ^ i + 1
neg : ∀ (hn' : ¬Even n) (ihn : LT.lt.{u_1} (α := R) 1 (∑ i ∈ range n, x ^ i)), x * ∑ i ∈ range n, x ^ i + 1 < 0
⊢ if ¬Even n then x * ∑ i ∈ range n, x ^ i + 1 < 0 else 1 < x * ∑ i ∈ range n, x ^ i + 1

Tactic:
split_ifs at ihn ⊢ with hn'
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
n_1 : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn : 2 ≤ n
hn' : Even n
ihn : LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0
pos : 0 < x * ∑ i ∈ range n, x ^ i
⊢ 1 < x * ∑ i ∈ range n, x ^ i + 1

Tactic:
rw [lt_add_iff_pos_left]

Premises used: lt_add_iff_pos_left
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
n_1 : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn : 2 ≤ n
hn' : Even n
ihn : LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0
⊢ 0 < x * ∑ i ∈ range n, x ^ i

Tactic:
mul_pos_of_neg_of_neg hx0 ihn

Premises used: mul_pos_of_neg_of_neg
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
n_1 : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn : 2 ≤ n
hn' : Even n
ihn : LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0
⊢ 0 < x * ∑ i ∈ range n, x ^ i

Tactic:
exact mul_pos_of_neg_of_neg hx0 ihn

Premises used: mul_pos_of_neg_of_neg
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
n_1 : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn : 2 ≤ n
hn' : ¬Even n
ihn : LT.lt.{u_1} (α := R) 1 (∑ i ∈ range n, x ^ i)
neg : x * ∑ i ∈ range n, x ^ i + 1 < x + 1
⊢ x * ∑ i ∈ range n, x ^ i + 1 < 0

Tactic:
grw [← hx]
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
n_1 : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn : 2 ≤ n
hn' : ¬Even n
ihn : LT.lt.{u_1} (α := R) 1 (∑ i ∈ range n, x ^ i)
neg : x * ∑ i ∈ range n, x ^ i < x
⊢ x * ∑ i ∈ range n, x ^ i + 1 < x + 1

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
n_1 : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn : 2 ≤ n
hn' : ¬Even n
ihn : LT.lt.{u_1} (α := R) 1 (∑ i ∈ range n, x ^ i)
⊢ x * ∑ i ∈ range n, x ^ i < x

Tactic:
simpa only [mul_one] using mul_lt_mul_of_neg_left ihn hx0

Premises used: mul_one, mul_lt_mul_of_neg_left
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hx : 0 < x + 1
hn : n ≠ 0
zero : ∀ (hn : Ne (α := ℕ) 0 0), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range 0, x ^ i)
succ : ∀ (hn : HAdd.hAdd (α := ℕ) 0 1 ≠ 0), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (HAdd.hAdd (α := ℕ) 0 1), x ^ i)
succ₁ : ∀ (n : ℕ) (hn : n + 1 + 1 ≠ 0), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (n + 1 + 1), x ^ i)
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)

Tactic:
obtain _ | _ | n := n
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
hn : Ne (α := ℕ) 0 0
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range 0, x ^ i)

Tactic:
cases hn rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
hn : HAdd.hAdd (α := ℕ) 0 1 ≠ 0
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (HAdd.hAdd (α := ℕ) 0 1), x ^ i)

Tactic:
simp only [zero_add, range_one, sum_singleton, pow_zero, zero_lt_one]

Premises used: zero_add, pow_zero, Finset.sum_singleton, zero_lt_one, Finset.range_one
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
succ : ∀ (hx' : x < 0), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (n + 1 + 1), x ^ i)
succ₁ : ∀ (hx' : 0 ≤ x), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (n + 1 + 1), x ^ i)
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (n + 1 + 1), x ^ i)

Tactic:
obtain hx' | hx' := lt_or_ge x 0

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
hx' : x < 0
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (n + 1 + 1), x ^ i)

Tactic:
(geom_sum_pos_and_lt_one hx' hx n.one_lt_succ_succ).1

Premises used: Nat.one_lt_succ_succ, And.left, geom_sum_pos_and_lt_one
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
hx' : x < 0
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (n + 1 + 1), x ^ i)

Tactic:
exact (geom_sum_pos_and_lt_one hx' hx n.one_lt_succ_succ).1

Premises used: Nat.one_lt_succ_succ, And.left, geom_sum_pos_and_lt_one
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
hx' : 0 ≤ x
⊢ n + 1 + 1 ≠ 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
hx' : 0 ≤ x
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (n + 1 + 1), x ^ i)

Tactic:
exact geom_sum_pos hx' (by simp)

Premises used: geom_sum_pos
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
h : Odd n
zero : ∀ (h : Odd (α := ℕ) 0), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range 0, x ^ i)
succ : ∀ (h : Odd (HAdd.hAdd (α := ℕ) 0 1)), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (HAdd.hAdd (α := ℕ) 0 1), x ^ i)
succ₁ : ∀ (k : ℕ) (h : Odd (k + 1 + 1)), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (k + 1 + 1), x ^ i)
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)

Tactic:
rcases n with (_ | _ | k)
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
h : Odd (α := ℕ) 0
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range 0, x ^ i)

Tactic:
(Nat.not_odd_zero h).elim

Premises used: False.elim, Nat.not_odd_zero
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
h : Odd (α := ℕ) 0
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range 0, x ^ i)

Tactic:
exact (Nat.not_odd_zero h).elim

Premises used: False.elim, Nat.not_odd_zero
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
h : Odd (HAdd.hAdd (α := ℕ) 0 1)
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (HAdd.hAdd (α := ℕ) 0 1), x ^ i)

Tactic:
simp only [zero_add, range_one, sum_singleton, pow_zero, zero_lt_one]

Premises used: zero_add, pow_zero, Finset.sum_singleton, zero_lt_one, Finset.range_one
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
k : ℕ
h : Odd (k + 1 + 1)
⊢ ¬Even (k + 1 + 1)

Tactic:
rw [← Nat.not_even_iff_odd] at h

Premises used: Nat.not_even_iff_odd
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
succ : ∀ (hx : x + 1 < 0), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (k + 1 + 1), x ^ i)
succ₁ : ∀ (hx : x + 1 = 0), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (k + 1 + 1), x ^ i)
succ₂ : ∀ (hx : 0 < x + 1), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (k + 1 + 1), x ^ i)
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (k + 1 + 1), x ^ i)

Tactic:
rcases lt_trichotomy (x + 1) 0 with (hx | hx | hx)

Premises used: HAdd.hAdd, OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
hx : x + 1 < 0
⊢ if Even k.succ.succ then LT.lt.{u_1} (α := R) (∑ i ∈ range k.succ.succ, x ^ i) 0
  else LT.lt.{u_1} (α := R) 1 (∑ i ∈ range k.succ.succ, x ^ i)

Tactic:
have := geom_sum_alternating_of_lt_neg_one hx k.one_lt_succ_succ
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
hx : x + 1 < 0
this :
  if Even k.succ.succ then LT.lt.{u_1} (α := R) (∑ i ∈ range k.succ.succ, x ^ i) 0
  else LT.lt.{u_1} (α := R) 1 (∑ i ∈ range k.succ.succ, x ^ i)
⊢ LT.lt.{u_1} (α := R) 1 (∑ i ∈ range k.succ.succ, x ^ i)

Tactic:
simp only [h, if_false] at this

Premises used: if_false
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
hx : x + 1 < 0
this : LT.lt.{u_1} (α := R) 1 (∑ i ∈ range k.succ.succ, x ^ i)
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (k + 1 + 1), x ^ i)

Tactic:
zero_lt_one.trans this

Premises used: zero_lt_one, LT.lt.trans
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
hx : x + 1 < 0
this : LT.lt.{u_1} (α := R) 1 (∑ i ∈ range k.succ.succ, x ^ i)
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (k + 1 + 1), x ^ i)

Tactic:
exact zero_lt_one.trans this

Premises used: zero_lt_one, LT.lt.trans
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
hx : x + 1 = 0
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (k + 1 + 1), x ^ i)

Tactic:
simp only [eq_neg_of_add_eq_zero_left hx, h, neg_one_geom_sum, if_false, zero_lt_one]

Premises used: if_false, eq_neg_of_add_eq_zero_left, zero_lt_one, neg_one_geom_sum
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
hx : 0 < x + 1
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (k + 1 + 1), x ^ i)

Tactic:
geom_sum_pos' hx k.succ.succ_ne_zero

Premises used: Nat.succ_ne_zero, Nat.succ, geom_sum_pos'
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
hx : 0 < x + 1
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (k + 1 + 1), x ^ i)

Tactic:
exact geom_sum_pos' hx k.succ.succ_ne_zero

Premises used: Nat.succ_ne_zero, Nat.succ, geom_sum_pos'
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ↔ Odd n ∨ 0 < x + 1

Tactic:
⟨fun h => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
refine_1 : ∀ (h : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)), Odd n ∨ 0 < x + 1
refine_2 : Odd n ∨ 0 < x + 1 → LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ↔ Odd n ∨ 0 < x + 1

Tactic:
refine ⟨fun h => ?_, ?_⟩
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)
refine_1 : Even n → ¬x + 1 ≤ 0
⊢ Odd n ∨ 0 < x + 1

Tactic:
rw [or_iff_not_imp_left, ← not_le, Nat.not_odd_iff_even]

Premises used: not_le, Nat.not_odd_iff_even, Classical.or_iff_not_imp_left
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)
⊢ Even n → ¬x + 1 ≤ 0

Tactic:
fun hn hx => h.not_ge ?_

Premises used: LT.lt.not_ge, Not
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)
refine_1 : ∀ (hn : Even n) (hx : x + 1 ≤ 0), LE.le.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0
⊢ Even n → ¬x + 1 ≤ 0

Tactic:
refine fun hn hx => h.not_ge ?_

Premises used: LT.lt.not_ge
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hn_1 : n ≠ 0
h : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)
hn : Even n
hx : x + 1 ≤ 0
⊢ LE.le.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0

Tactic:
simpa [if_pos hn] using geom_sum_alternating_of_le_neg_one hx n

Premises used: geom_sum_alternating_of_le_neg_one, if_pos
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hn_1 : n ≠ 0
hn : Odd n
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)

Tactic:
hn.geom_sum_pos

Premises used: Odd.geom_sum_pos
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hn_1 : n ≠ 0
hn : Odd n
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)

Tactic:
exact hn.geom_sum_pos

Premises used: Odd.geom_sum_pos
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
hx' : 0 < x + 1
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)

Tactic:
geom_sum_pos' hx' hn

Premises used: geom_sum_pos'
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
hx' : 0 < x + 1
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)

Tactic:
exact geom_sum_pos' hx' hn

Premises used: geom_sum_pos'
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hx : x ≠ -1
hn : n ≠ 0
zero : ∀ (hn : Ne (α := ℕ) 0 0), Ne.{u_1 + 1} (α := R) (∑ i ∈ range 0, x ^ i) 0
succ : ∀ (hn : HAdd.hAdd (α := ℕ) 0 1 ≠ 0), Ne.{u_1 + 1} (α := R) (∑ i ∈ range (HAdd.hAdd (α := ℕ) 0 1), x ^ i) 0
succ₁ : ∀ (n : ℕ) (hn : n + 1 + 1 ≠ 0), Ne.{u_1 + 1} (α := R) (∑ i ∈ range (n + 1 + 1), x ^ i) 0
⊢ Ne.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i) 0

Tactic:
obtain _ | _ | n := n
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
hx : x ≠ -1
hn : Ne (α := ℕ) 0 0
⊢ Ne.{u_1 + 1} (α := R) (∑ i ∈ range 0, x ^ i) 0

Tactic:
cases hn rfl

Premises used: rfl