awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Cone (goal)
Goal:
R : Type u_1
inst : Ring R
q : RingCone R
toSubsemiring : Subsemiring R
eq_zero_of_mem_of_neg_mem' : ∀ {a : R}, a ∈ toSubsemiring.carrier → -a ∈ toSubsemiring.carrier → a = 0
h :
  Eq.{u_1 + 1} (α := Set R)
    ((fun (C : RingCone R) ↦ C.carrier)
      { toSubsemiring := toSubsemiring, eq_zero_of_mem_of_neg_mem' := @eq_zero_of_mem_of_neg_mem' })
    ((fun (C : RingCone R) ↦ C.carrier) q)
⊢ { toSubsemiring := toSubsemiring, eq_zero_of_mem_of_neg_mem' := @eq_zero_of_mem_of_neg_mem' : RingCone R } = q
have mk : ∀ (toSubsemiring_1 : Subsemiring R)
  (eq_zero_of_mem_of_neg_mem'_1 : ∀ {a : R}, a ∈ toSubsemiring_1.carrier → -a ∈ toSubsemiring_1.carrier → a = 0)
  (h :
    Eq.{u_1 + 1} (α := Set R)
      ((fun (C : RingCone R) ↦ C.carrier)
        { toSubsemiring := toSubsemiring, eq_zero_of_mem_of_neg_mem' := @eq_zero_of_mem_of_neg_mem' })
      ((fun (C : RingCone R) ↦ C.carrier)
        { toSubsemiring := toSubsemiring_1, eq_zero_of_mem_of_neg_mem' := @eq_zero_of_mem_of_neg_mem'_1 })),
  { toSubsemiring := toSubsemiring, eq_zero_of_mem_of_neg_mem' := @eq_zero_of_mem_of_neg_mem' : RingCone R } =
    { toSubsemiring := toSubsemiring_1, eq_zero_of_mem_of_neg_mem' := @eq_zero_of_mem_of_neg_mem'_1 }
Tactic: cases q
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Cone (goal)
Goal:
R : Type u_1
inst : Ring R
toSubsemiring : Subsemiring R
eq_zero_of_mem_of_neg_mem' : ∀ {a : R}, a ∈ toSubsemiring.carrier → -a ∈ toSubsemiring.carrier → a = 0
toSubsemiring_1 : Subsemiring R
eq_zero_of_mem_of_neg_mem'_1 : ∀ {a : R}, a ∈ toSubsemiring_1.carrier → -a ∈ toSubsemiring_1.carrier → a = 0
h :
  Eq.{u_1 + 1} (α := Set R)
    ((fun (C : RingCone R) ↦ C.carrier)
      { toSubsemiring := toSubsemiring, eq_zero_of_mem_of_neg_mem' := @eq_zero_of_mem_of_neg_mem' })
    ((fun (C : RingCone R) ↦ C.carrier)
      { toSubsemiring := toSubsemiring_1, eq_zero_of_mem_of_neg_mem' := @eq_zero_of_mem_of_neg_mem'_1 })
⊢ { toSubsemiring := toSubsemiring, eq_zero_of_mem_of_neg_mem' := @eq_zero_of_mem_of_neg_mem' : RingCone R } =
    { toSubsemiring := toSubsemiring_1, eq_zero_of_mem_of_neg_mem' := @eq_zero_of_mem_of_neg_mem'_1 }
have mk : toSubsemiring = toSubsemiring_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : NeZero.{u_1} (R := R) 1
inst_4 : AddLeftStrictMono R
n : ℕ
⊢ LT.lt.{u_1} (α := R) (↑n : R) (↑(n + 1) : R)
have rw : (↑n : R) < HAdd.hAdd (α := R) (↑n : R) 1
Tactic: rw [Nat.cast_succ]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Defs (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
a b : R
hab : a * b = 0
⊢ a = 0 ∨ b = 0
have contrapose! : ∀ (hab : a ≠ 0 ∧ b ≠ 0), a * b ≠ 0
Tactic: contrapose! hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Defs (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
a b : R
hab : a ≠ 0 ∧ b ≠ 0
⊢ a * b ≠ 0
have inl : ∀ (ha : a < 0), a * b ≠ 0
Tactic: obtain ha | ha := hab.1.lt_or_gt
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Defs (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
a b : R
hab : a ≠ 0 ∧ b ≠ 0
inl : ∀ (ha : a < 0), a * b ≠ 0
⊢ a * b ≠ 0
have inr : ∀ (ha : 0 < a), a * b ≠ 0
Tactic: obtain ha | ha := hab.1.lt_or_gt
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Defs (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
a b : R
hab : a ≠ 0 ∧ b ≠ 0
ha : a < 0
⊢ a * b ≠ 0
have inl : ∀ (hb : b < 0), a * b ≠ 0
Tactic: obtain hb | hb := hab.2.lt_or_gt
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Defs (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
a b : R
hab : a ≠ 0 ∧ b ≠ 0
ha : a < 0
inl : ∀ (hb : b < 0), a * b ≠ 0
⊢ a * b ≠ 0
have inl₁ : ∀ (hb : 0 < b), a * b ≠ 0
Tactic: obtain hb | hb := hab.2.lt_or_gt
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Defs (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
a b : R
hab : a ≠ 0 ∧ b ≠ 0
ha : 0 < a
⊢ a * b ≠ 0
have inr : ∀ (hb : b < 0), a * b ≠ 0
Tactic: obtain hb | hb := hab.2.lt_or_gt
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Defs (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
a b : R
hab : a ≠ 0 ∧ b ≠ 0
ha : 0 < a
inr : ∀ (hb : b < 0), a * b ≠ 0
⊢ a * b ≠ 0
have inr₁ : ∀ (hb : 0 < b), a * b ≠ 0
Tactic: obtain hb | hb := hab.2.lt_or_gt
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Defs (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
a : R
ha : a ≠ 0
x x_1 : R
h : Eq.{u + 1} (α := R) ((fun (x : R) ↦ a * x) x) ((fun (x : R) ↦ a * x) x_1)
⊢ x = x_1
have inl : ∀ (ha : a < 0), x = x_1
Tactic: obtain ha | ha := ha.lt_or_gt
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Defs (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
a : R
ha : a ≠ 0
x x_1 : R
h : Eq.{u + 1} (α := R) ((fun (x : R) ↦ a * x) x) ((fun (x : R) ↦ a * x) x_1)
inl : ∀ (ha : a < 0), x = x_1
⊢ x = x_1
have inr : ∀ (ha : 0 < a), x = x_1
Tactic: obtain ha | ha := ha.lt_or_gt
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Defs (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
a : R
ha : a ≠ 0
x x_1 : R
h : Eq.{u + 1} (α := R) ((fun (x : R) ↦ x * a) x) ((fun (x : R) ↦ x * a) x_1)
⊢ x = x_1
have inl : ∀ (ha : a < 0), x = x_1
Tactic: obtain ha | ha := ha.lt_or_gt
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Defs (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
a : R
ha : a ≠ 0
x x_1 : R
h : Eq.{u + 1} (α := R) ((fun (x : R) ↦ x * a) x) ((fun (x : R) ↦ x * a) x_1)
inl : ∀ (ha : a < 0), x = x_1
⊢ x = x_1
have inr : ∀ (ha : 0 < a), x = x_1
Tactic: obtain ha | ha := ha.lt_or_gt
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Defs (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b c : R
h : a + b + b * c ≤ c
⊢ 1 + a ≤ (1 - b) * (1 + c)
have rw : 1 + (a + b + b * c) ≤ 1 + c
Tactic: rw [one_sub_mul, mul_one_add, le_sub_iff_add_le, add_assoc, ← add_assoc a]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Defs (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b c : R
h : a + c + b * c ≤ b
⊢ 1 + a ≤ (1 + b) * (1 - c)
have rw : 1 + (a + c + b * c) ≤ 1 + b
Tactic: rw [mul_one_sub, one_add_mul, le_sub_iff_add_le, add_assoc, ← add_assoc a]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Defs (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b c : R
h : b + b * c ≤ a + c
⊢ 1 - a ≤ (1 - b) * (1 + c)
have rw : 1 + (b + b * c) ≤ 1 + (a + c)
Tactic: rw [one_sub_mul, mul_one_add, sub_le_sub_iff, add_assoc, add_comm c]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Defs (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b c : R
h : c + b * c ≤ a + b
⊢ 1 - a ≤ (1 + b) * (1 - c)
have rw : 1 + (c + b * c) ≤ 1 + (a + b)
Tactic: rw [mul_one_sub, one_add_mul, sub_le_sub_iff, add_assoc, add_comm b]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Finset (goal)
Goal:
R : Type u_1
ι : Type u_2
inst : LinearOrder R
inst_1 : NonUnitalNonAssocSemiring R
inst_2 : CanonicallyOrderedAdd R
inst_3 : OrderBot R
s : Finset ι
f : ι → R
a : R
⊢ a * s.sup f = s.sup fun (x : ι) ↦ a * f x
have empty : a * sup ∅ f = sup ∅ fun (x : ι) ↦ a * f x
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert _ _ _ IH => simp only [sup_insert, mul_max, ← IH]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Finset (goal)
Goal:
R : Type u_1
ι : Type u_2
inst : LinearOrder R
inst_1 : NonUnitalNonAssocSemiring R
inst_2 : CanonicallyOrderedAdd R
inst_3 : OrderBot R
s : Finset ι
f : ι → R
a : R
empty : a * sup ∅ f = sup ∅ fun (x : ι) ↦ a * f x
⊢ a * s.sup f = s.sup fun (x : ι) ↦ a * f x
have insert : ∀ (a_1 : ι) (s : Finset ι),
  a_1 ∉ s →
    ∀ (IH : a * s.sup f = s.sup fun (x : ι) ↦ a * f x),
      a * (insert a_1 s).sup f = (insert a_1 s).sup fun (x : ι) ↦ a * f x
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert _ _ _ IH => simp only [sup_insert, mul_max, ← IH]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Finset (goal)
Goal:
R : Type u_1
ι : Type u_2
inst : LinearOrder R
inst_1 : NonUnitalNonAssocSemiring R
inst_2 : CanonicallyOrderedAdd R
inst_3 : OrderBot R
s : Finset ι
f : ι → R
a : R
⊢ a * s.sup f = s.sup fun (x : ι) ↦ a * f x
have empty : a * sup ∅ f = sup ∅ fun (x : ι) ↦ a * f x
Tactic: classical
  induction s using Finset.induction with
  | empty => simp
  | insert _ _ _ IH => simp only [sup_insert, mul_max, ← IH]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Finset (goal)
Goal:
R : Type u_1
ι : Type u_2
inst : LinearOrder R
inst_1 : NonUnitalNonAssocSemiring R
inst_2 : CanonicallyOrderedAdd R
inst_3 : OrderBot R
s : Finset ι
f : ι → R
a : R
empty : a * sup ∅ f = sup ∅ fun (x : ι) ↦ a * f x
⊢ a * s.sup f = s.sup fun (x : ι) ↦ a * f x
have insert : ∀ (a_1 : ι) (s : Finset ι),
  a_1 ∉ s →
    ∀ (IH : a * s.sup f = s.sup fun (x : ι) ↦ a * f x),
      a * (insert a_1 s).sup f = (insert a_1 s).sup fun (x : ι) ↦ a * f x
Tactic: classical
  induction s using Finset.induction with
  | empty => simp
  | insert _ _ _ IH => simp only [sup_insert, mul_max, ← IH]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Finset (goal)
Goal:
R : Type u_1
ι : Type u_2
inst : LinearOrder R
inst_1 : NonUnitalNonAssocSemiring R
inst_2 : CanonicallyOrderedAdd R
inst_3 : OrderBot R
s : Finset ι
f : ι → R
a : R
⊢ s.sup f * a = s.sup fun (x : ι) ↦ f x * a
have empty : sup ∅ f * a = sup ∅ fun (x : ι) ↦ f x * a
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert _ _ _ IH => simp only [sup_insert, max_mul, ← IH]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Finset (goal)
Goal:
R : Type u_1
ι : Type u_2
inst : LinearOrder R
inst_1 : NonUnitalNonAssocSemiring R
inst_2 : CanonicallyOrderedAdd R
inst_3 : OrderBot R
s : Finset ι
f : ι → R
a : R
empty : sup ∅ f * a = sup ∅ fun (x : ι) ↦ f x * a
⊢ s.sup f * a = s.sup fun (x : ι) ↦ f x * a
have insert : ∀ (a_1 : ι) (s : Finset ι),
  a_1 ∉ s →
    ∀ (IH : s.sup f * a = s.sup fun (x : ι) ↦ f x * a),
      (insert a_1 s).sup f * a = (insert a_1 s).sup fun (x : ι) ↦ f x * a
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert _ _ _ IH => simp only [sup_insert, max_mul, ← IH]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Finset (goal)
Goal:
R : Type u_1
ι : Type u_2
inst : LinearOrder R
inst_1 : NonUnitalNonAssocSemiring R
inst_2 : CanonicallyOrderedAdd R
inst_3 : OrderBot R
s : Finset ι
f : ι → R
a : R
⊢ s.sup f * a = s.sup fun (x : ι) ↦ f x * a
have empty : sup ∅ f * a = sup ∅ fun (x : ι) ↦ f x * a
Tactic: classical
  induction s using Finset.induction with
  | empty => simp
  | insert _ _ _ IH => simp only [sup_insert, max_mul, ← IH]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Finset (goal)
Goal:
R : Type u_1
ι : Type u_2
inst : LinearOrder R
inst_1 : NonUnitalNonAssocSemiring R
inst_2 : CanonicallyOrderedAdd R
inst_3 : OrderBot R
s : Finset ι
f : ι → R
a : R
empty : sup ∅ f * a = sup ∅ fun (x : ι) ↦ f x * a
⊢ s.sup f * a = s.sup fun (x : ι) ↦ f x * a
have insert : ∀ (a_1 : ι) (s : Finset ι),
  a_1 ∉ s →
    ∀ (IH : s.sup f * a = s.sup fun (x : ι) ↦ f x * a),
      (insert a_1 s).sup f * a = (insert a_1 s).sup fun (x : ι) ↦ f x * a
Tactic: classical
  induction s using Finset.induction with
  | empty => simp
  | insert _ _ _ IH => simp only [sup_insert, max_mul, ← IH]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
n : ℕ
⊢ 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)
have hx0 : x ≤ 0
Tactic: have hx0 : x ≤ 0 := (le_add_of_nonneg_right zero_le_one).trans hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
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)
have succ : if ¬Even n then x * ∑ i ∈ range n, x ^ i + 1 ≤ 0 else 1 ≤ x * ∑ i ∈ range n, x ^ i + 1
Tactic: simp only [Nat.even_add_one, geom_sum_succ]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
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 then x * ∑ i ∈ range n, x ^ i + 1 ≤ 0 else 1 ≤ x * ∑ i ∈ range n, x ^ i + 1
have pos : ∀ (h : Even n) (ih : LE.le.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0), 1 ≤ x * ∑ i ∈ range n, x ^ i + 1
Tactic: split_ifs at ih ⊢ with h
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
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)
pos : ∀ (h : Even n) (ih : LE.le.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0), 1 ≤ x * ∑ i ∈ range n, x ^ i + 1
⊢ if ¬Even n then x * ∑ i ∈ range n, x ^ i + 1 ≤ 0 else 1 ≤ x * ∑ i ∈ range n, x ^ i + 1
have neg : ∀ (h : ¬Even n) (ih : LE.le.{u_1} (α := R) 1 (∑ i ∈ range n, x ^ i)), x * ∑ i ∈ range n, x ^ i + 1 ≤ 0
Tactic: split_ifs at ih ⊢ with h
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : Even n
ih : LE.le.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0
⊢ 1 ≤ x * ∑ i ∈ range n, x ^ i + 1
have pos : 0 ≤ x * ∑ i ∈ range n, x ^ i
Tactic: rw [le_add_iff_nonneg_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : ¬Even n
ih : LE.le.{u_1} (α := R) 1 (∑ i ∈ range n, x ^ i)
⊢ x * ∑ i ∈ range n, x ^ i + 1 ≤ 0
have neg : x * ∑ i ∈ range n, x ^ i + 1 ≤ x + 1
Tactic: grw [← hx]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : ¬Even n
ih : LE.le.{u_1} (α := R) 1 (∑ i ∈ range n, x ^ i)
⊢ x * ∑ i ∈ range n, x ^ i + 1 ≤ x + 1
have neg : x * ∑ i ∈ range n, x ^ i ≤ x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
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
⊢ 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)
have 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)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
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)
⊢ 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)
have 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)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
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
have refine_1 : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range 2, x ^ i) ∧ LT.lt.{u_1} (α := R) (∑ i ∈ range 2, x ^ i) 1
Tactic: refine Nat.le_induction ?_ ?_ n (show 2 ≤ n from hn)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
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
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ∧ LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 1
have 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
Tactic: refine Nat.le_induction ?_ ?_ n (show 2 ≤ n from hn)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
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 2, x ^ i) ∧ LT.lt.{u_1} (α := R) (∑ i ∈ range 2, x ^ i) 1
have refine_1 : 0 < x + 1 ∧ x + 1 < 1
Tactic: rw [geom_sum_two]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
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
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (n + 1), x ^ i) ∧ LT.lt.{u_1} (α := R) (∑ i ∈ range (n + 1), x ^ i) 1
have refine_2 : -x * ∑ i ∈ range n, x ^ i < 1 ∧ x * ∑ i ∈ range n, x ^ i < 0
Tactic: rw [geom_sum_succ, add_lt_iff_neg_right, ← neg_lt_iff_pos_add', neg_mul_eq_neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (hypothesis)
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
⊢ 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)
have hx0 : x < 0
Tactic: have hx0 : x < 0 := (le_add_of_nonneg_right zero_le_one).trans_lt hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
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)
have 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)
Tactic: refine Nat.le_induction ?_ ?_ n (show 2 ≤ n from hn)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
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)
⊢ 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)
have 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)
Tactic: refine Nat.le_induction ?_ ?_ n (show 2 ≤ n from hn)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
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)
⊢ 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)
have refine_2 : if ¬Even n then x * ∑ i ∈ range n, x ^ i + 1 < 0 else 1 < x * ∑ i ∈ range n, x ^ i + 1
Tactic: simp only [Nat.even_add_one, geom_sum_succ]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
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)
⊢ if ¬Even n then x * ∑ i ∈ range n, x ^ i + 1 < 0 else 1 < x * ∑ i ∈ range n, x ^ i + 1
have pos : ∀ (hn' : Even n) (ihn : LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0), 1 < x * ∑ i ∈ range n, x ^ i + 1
Tactic: split_ifs at ihn ⊢ with hn'
Cleared hypotheses: ihn
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
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
⊢ if ¬Even n then x * ∑ i ∈ range n, x ^ i + 1 < 0 else 1 < x * ∑ i ∈ range n, x ^ i + 1
have neg : ∀ (hn' : ¬Even n) (ihn : LT.lt.{u_1} (α := R) 1 (∑ i ∈ range n, x ^ i)), x * ∑ i ∈ range n, x ^ i + 1 < 0
Tactic: split_ifs at ihn ⊢ with hn'
Cleared hypotheses: ihn
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
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
⊢ 1 < x * ∑ i ∈ range n, x ^ i + 1
have pos : 0 < x * ∑ i ∈ range n, x ^ i
Tactic: rw [lt_add_iff_pos_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
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 + 1 < 0
have neg : x * ∑ i ∈ range n, x ^ i + 1 < x + 1
Tactic: grw [← hx]