mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case pos
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : Even n
ih : ∑ i ∈ range n, x ^ i ≤ 0
⊢ 1 ≤ x * ∑ i ∈ range n, x ^ i + 1

pp: case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : ¬Even n
ih : 1 ≤ ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i + 1 ≤ 0

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : Even n
ih : ∑ i ∈ range n, x ^ i ≤ 0
⊢ 1 ≤ x * ∑ i ∈ range n, x ^ i + 1
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : ¬Even n
ih : 1 ≤ ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i + 1 ≤ 0

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : ¬Even n
ih : 1 ≤ ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i + 1 ≤ 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n✝ : ℕ
a b : ZMod (n✝ + 1)
⊢ (a + b).val ≤ a.val + b.val

Tactic:
·

Goal state after:
case succ
n✝ : ℕ
a b : ZMod (n✝ + 1)
⊢ (a + b).val ≤ a.val + b.val
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
a b : ZMod 0
⊢ (a * b).val = a.val * b.val % 0

pp: case succ
n✝ : ℕ
a b : ZMod (n✝ + 1)
⊢ (a * b).val = a.val * b.val % (n✝ + 1)

Tactic:
·

Goal state after:
case zero
a b : ZMod 0
⊢ (a * b).val = a.val * b.val % 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n✝ : ℕ
a b : ZMod (n✝ + 1)
⊢ (a * b).val = a.val * b.val % (n✝ + 1)

Tactic:
·

Goal state after:
case succ
n✝ : ℕ
a b : ZMod (n✝ + 1)
⊢ (a * b).val = a.val * b.val % (n✝ + 1)
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
hn : 1 < n
⊢ 0 < ∑ i ∈ range 2, x ^ i ∧ ∑ i ∈ range 2, x ^ i < 1

pp: case refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
hn : 1 < n
⊢ ∀ (n : ℕ),
    2 ≤ n →
      0 < ∑ i ∈ range n, x ^ i ∧ ∑ i ∈ range n, x ^ i < 1 →
        0 < ∑ i ∈ range (n + 1), x ^ i ∧ ∑ i ∈ range (n + 1), x ^ i < 1

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
hn : 1 < n
⊢ 0 < ∑ i ∈ range 2, x ^ i ∧ ∑ i ∈ range 2, x ^ i < 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inl
⊢ List.Pairwise (fun x1 x2 ↦ x1.2 > x2.2) (divisorsAntidiagonalList 0)

pp: case inr
n : ℕ
hn : n ≠ 0
⊢ List.Pairwise (fun x1 x2 ↦ x1.2 > x2.2) n.divisorsAntidiagonalList

Tactic:
·

Goal state after:
case inl
⊢ List.Pairwise (fun x1 x2 ↦ x1.2 > x2.2) (divisorsAntidiagonalList 0)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mp
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : (a * b).val = a.val * b.val
⊢ a.val * b.val < n

pp: case mpr
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : a.val * b.val < n
⊢ (a * b).val = a.val * b.val

Tactic:
·

Goal state after:
case mp
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : (a * b).val = a.val * b.val
⊢ a.val * b.val < n
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case zero
n : ℕ
⊢ n ∈ divisors 0 → n ≤ 0

pp: case succ
n m : ℕ
⊢ n ∈ (m + 1).divisors → n ≤ m + 1

Tactic:
·

Goal state after:
case zero
n : ℕ
⊢ n ∈ divisors 0 → n ≤ 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ
n m : ℕ
⊢ n ∈ (m + 1).divisors → n ≤ m + 1

Tactic:
·

Goal state after:
case succ
n m : ℕ
⊢ n ∈ (m + 1).divisors → n ≤ m + 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mpr
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : a.val * b.val < n
⊢ (a * b).val = a.val * b.val

Tactic:
·

Goal state after:
case mpr
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : a.val * b.val < n
⊢ (a * b).val = a.val * b.val
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hx : x + 1 < 0
hn : 1 < n
hx0 : x < 0
⊢ if Even 2 then ∑ i ∈ range 2, x ^ i < 0 else 1 < ∑ i ∈ range 2, x ^ i

pp: case refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hx : x + 1 < 0
hn : 1 < n
hx0 : x < 0
⊢ ∀ (n : ℕ),
    2 ≤ n →
      (if Even n then ∑ i ∈ range n, x ^ i < 0 else 1 < ∑ i ∈ range n, x ^ i) →
        if Even (n + 1) then ∑ i ∈ range (n + 1), x ^ i < 0 else 1 < ∑ i ∈ range (n + 1), x ^ i

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hx : x + 1 < 0
hn : 1 < n
hx0 : x < 0
⊢ if Even 2 then ∑ i ∈ range 2, x ^ i < 0 else 1 < ∑ i ∈ range 2, x ^ i
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
a : ZMod 0
⊢ a * a⁻¹ = ↑(a.val.gcd 0)

pp: case succ
n : ℕ
a : ZMod (n + 1)
⊢ a * a⁻¹ = ↑(a.val.gcd (n + 1))

Tactic:
·

Goal state after:
case zero
a : ZMod 0
⊢ a * a⁻¹ = ↑(a.val.gcd 0)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n : ℕ
a : ZMod (n + 1)
⊢ a * a⁻¹ = ↑(a.val.gcd (n + 1))

Tactic:
·

Goal state after:
case succ
n : ℕ
a : ZMod (n + 1)
⊢ a * a⁻¹ = ↑(a.val.gcd (n + 1))
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case zero
n : ℕ
h : 0 ∈ n.divisors
⊢ 0 < 0

pp: case succ
n n✝ : ℕ
h : n✝ + 1 ∈ n.divisors
⊢ 0 < n✝ + 1

Tactic:
·

Goal state after:
case zero
n : ℕ
h : 0 ∈ n.divisors
⊢ 0 < 0
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case pos
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
hn' : Even n
ihn : ∑ i ∈ range n, x ^ i < 0
⊢ 1 < x * ∑ i ∈ range n, x ^ i + 1

pp: case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
hn' : ¬Even n
ihn : 1 < ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i + 1 < 0

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
hn' : Even n
ihn : ∑ i ∈ range n, x ^ i < 0
⊢ 1 < x * ∑ i ∈ range n, x ^ i + 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inl
⊢ 0 ≤ (divisors 0).sup id

pp: case inr
n : ℕ
hn : n ≠ 0
⊢ n ≤ n.divisors.sup id

Tactic:
·

Goal state after:
case inl
⊢ 0 ≤ (divisors 0).sup id
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 0
⊢ n ≤ n.divisors.sup id

Tactic:
·

Goal state after:
case inr
n : ℕ
hn : n ≠ 0
⊢ n ≤ n.divisors.sup id
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
hn' : ¬Even n
ihn : 1 < ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i + 1 < 0

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
hn' : ¬Even n
ihn : 1 < ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i + 1 < 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case refine_1
m n : ℕ
hn : n ≠ 0
h : m ∈ n.properDivisors
⊢ n = m * (n / m)

pp: case refine_2
m n : ℕ
hn : n ≠ 0
⊢ (∃ k > 1, n = m * k) → m ∈ n.properDivisors

Tactic:
·

Goal state after:
case refine_1
m n : ℕ
hn : n ≠ 0
h : m ∈ n.properDivisors
⊢ n = m * (n / m)
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case refine_2
m n : ℕ
hn : n ≠ 0
⊢ (∃ k > 1, n = m * k) → m ∈ n.properDivisors

Tactic:
·

Goal state after:
case refine_2
m n : ℕ
hn : n ≠ 0
⊢ (∃ k > 1, n = m * k) → m ∈ n.properDivisors
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
hn : 0 ≠ 0
⊢ 0 < ∑ i ∈ range 0, x ^ i

pp: case succ.zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
hn : 0 + 1 ≠ 0
⊢ 0 < ∑ i ∈ range (0 + 1), x ^ i

pp: case succ.succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
⊢ 0 < ∑ i ∈ range (n + 1 + 1), x ^ i

Tactic:
·

Goal state after:
case zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
hn : 0 ≠ 0
⊢ 0 < ∑ i ∈ range 0, x ^ i
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case succ.zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
hn : 0 + 1 ≠ 0
⊢ 0 < ∑ i ∈ range (0 + 1), x ^ i

pp: case succ.succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
⊢ 0 < ∑ i ∈ range (n + 1 + 1), x ^ i

Tactic:
·

Goal state after:
case succ.zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
hn : 0 + 1 ≠ 0
⊢ 0 < ∑ i ∈ range (0 + 1), x ^ i
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case succ.succ.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
hx' : x < 0
⊢ 0 < ∑ i ∈ range (n + 1 + 1), x ^ i

pp: case succ.succ.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
hx' : 0 ≤ x
⊢ 0 < ∑ i ∈ range (n + 1 + 1), x ^ i

Tactic:
·

Goal state after:
case succ.succ.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
hx' : x < 0
⊢ 0 < ∑ i ∈ range (n + 1 + 1), x ^ i
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inl
⊢ 1⁻¹ = 1

pp: case inr
n : ℕ
hn : n ≠ 1
⊢ 1⁻¹ = 1

Tactic:
·

Goal state after:
case inl
⊢ 1⁻¹ = 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 1
⊢ 1⁻¹ = 1

Tactic:
·

Goal state after:
case inr
n : ℕ
hn : n ≠ 1
⊢ 1⁻¹ = 1
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case succ.succ.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
hx' : 0 ≤ x
⊢ 0 < ∑ i ∈ range (n + 1 + 1), x ^ i

Tactic:
·

Goal state after:
case succ.succ.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
hx' : 0 ≤ x
⊢ 0 < ∑ i ∈ range (n + 1 + 1), x ^ i
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
h : Odd 0
⊢ 0 < ∑ i ∈ range 0, x ^ i

pp: case succ.zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
h : Odd (0 + 1)
⊢ 0 < ∑ i ∈ range (0 + 1), x ^ i

pp: case succ.succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
k : ℕ
h : Odd (k + 1 + 1)
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i

Tactic:
·

Goal state after:
case zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
h : Odd 0
⊢ 0 < ∑ i ∈ range 0, x ^ i
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case succ.zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
h : Odd (0 + 1)
⊢ 0 < ∑ i ∈ range (0 + 1), x ^ i

pp: case succ.succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
k : ℕ
h : Odd (k + 1 + 1)
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i

Tactic:
·

Goal state after:
case succ.zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
h : Odd (0 + 1)
⊢ 0 < ∑ i ∈ range (0 + 1), x ^ i
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inl
m : ℕ
hmn : m.Coprime 0
⊢ ↑m * ↑(↑m)⁻¹.val = 1

pp: case inr
m n : ℕ
hmn : m.Coprime n
hn : n ≠ 0
⊢ ↑m * ↑(↑m)⁻¹.val = 1

Tactic:
·

Goal state after:
case inl
m : ℕ
hmn : m.Coprime 0
⊢ ↑m * ↑(↑m)⁻¹.val = 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n : ℕ
hmn : m.Coprime n
⊢ ↑m * ↑(↑m)⁻¹.val = 1

Tactic:
by
  obtain rfl | hn := eq_or_ne n 0
  · simp [m.coprime_zero_right.1 hmn]
  have : NeZero n := ⟨hn⟩
  rw [ZMod.natCast_zmod_val, ZMod.coe_mul_inv_eq_one _ hmn]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mp
n d nd : ℕ
⊢ (d ∣ n ∧ n ≠ 0) ∧ n / d = nd → d * nd = n ∧ n ≠ 0

pp: case mpr
n d nd : ℕ
⊢ d * nd = n ∧ n ≠ 0 → (d ∣ n ∧ n ≠ 0) ∧ n / d = nd

Tactic:
·

Goal state after:
case mp
n d nd : ℕ
⊢ (d ∣ n ∧ n ≠ 0) ∧ n / d = nd → d * nd = n ∧ n ≠ 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mpr
n d nd : ℕ
⊢ d * nd = n ∧ n ≠ 0 → (d ∣ n ∧ n ≠ 0) ∧ n / d = nd

Tactic:
·

Goal state after:
case mpr
n d nd : ℕ
⊢ d * nd = n ∧ n ≠ 0 → (d ∣ n ∧ n ≠ 0) ∧ n / d = nd
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
u : (ZMod 0)ˣ
⊢ (↑u).val.Coprime 0

pp: case succ
n : ℕ
u : (ZMod (n + 1))ˣ
⊢ (↑u).val.Coprime (n + 1)

Tactic:
·

Goal state after:
case zero
u : (ZMod 0)ˣ
⊢ (↑u).val.Coprime 0
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case succ.succ.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
hx : x + 1 < 0
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i

pp: case succ.succ.inr.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
hx : x + 1 = 0
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i

pp: case succ.succ.inr.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
hx : 0 < x + 1
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i

Tactic:
·

Goal state after:
case succ.succ.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
hx : x + 1 < 0
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case succ.succ.inr.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
hx : x + 1 = 0
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i

pp: case succ.succ.inr.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
hx : 0 < x + 1
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i

Tactic:
·

Goal state after:
case succ.succ.inr.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
hx : x + 1 = 0
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inl
⊢ ∑ i ∈ divisors 0, i = ∑ i ∈ properDivisors 0, i + 0

pp: case inr
n : ℕ
hn : n ≠ 0
⊢ ∑ i ∈ n.divisors, i = ∑ i ∈ n.properDivisors, i + n

Tactic:
·

Goal state after:
case inl
⊢ ∑ i ∈ divisors 0, i = ∑ i ∈ properDivisors 0, i + 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 0
⊢ ∑ i ∈ n.divisors, i = ∑ i ∈ n.properDivisors, i + n

Tactic:
·

Goal state after:
case inr
n : ℕ
hn : n ≠ 0
⊢ ∑ i ∈ n.divisors, i = ∑ i ∈ n.properDivisors, i + n
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case succ.succ.inr.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
hx : 0 < x + 1
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i

Tactic:
·

Goal state after:
case succ.succ.inr.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
hx : 0 < x + 1
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mp
n : ℕ
h✝ : 0 < n
h : ∑ i ∈ n.properDivisors, i = n
⊢ ∑ i ∈ n.properDivisors, i + n = n + n

pp: case mpr
n : ℕ
h✝ : 0 < n
h : ∑ i ∈ n.properDivisors, i + n = n + n
⊢ ∑ i ∈ n.properDivisors, i = n

Tactic:
·

Goal state after:
case mp
n : ℕ
h✝ : 0 < n
h : ∑ i ∈ n.properDivisors, i = n
⊢ ∑ i ∈ n.properDivisors, i + n = n + n
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : 0 < ∑ i ∈ range n, x ^ i
⊢ Odd n ∨ 0 < x + 1

pp: case refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ Odd n ∨ 0 < x + 1 → 0 < ∑ i ∈ range n, x ^ i

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : 0 < ∑ i ∈ range n, x ^ i
⊢ Odd n ∨ 0 < x + 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mpr
n : ℕ
h✝ : 0 < n
h : ∑ i ∈ n.properDivisors, i + n = n + n
⊢ ∑ i ∈ n.properDivisors, i = n

Tactic:
·

Goal state after:
case mpr
n : ℕ
h✝ : 0 < n
h : ∑ i ∈ n.properDivisors, i + n = n + n
⊢ ∑ i ∈ n.properDivisors, i = n
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ Odd n ∨ 0 < x + 1 → 0 < ∑ i ∈ range n, x ^ i

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ Odd n ∨ 0 < x + 1 → 0 < ∑ i ∈ range n, x ^ i
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case refine_2.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn✝ : n ≠ 0
hn : Odd n
⊢ 0 < ∑ i ∈ range n, x ^ i

pp: case refine_2.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
hx' : 0 < x + 1
⊢ 0 < ∑ i ∈ range n, x ^ i

Tactic:
·

Goal state after:
case refine_2.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn✝ : n ≠ 0
hn : Odd n
⊢ 0 < ∑ i ∈ range n, x ^ i
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case refine_2.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
hx' : 0 < x + 1
⊢ 0 < ∑ i ∈ range n, x ^ i

Tactic:
·

Goal state after:
case refine_2.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
hx' : 0 < x + 1
⊢ 0 < ∑ i ∈ range n, x ^ i
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x ≠ -1
hn : 0 ≠ 0
⊢ ∑ i ∈ range 0, x ^ i ≠ 0

pp: case succ.zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x ≠ -1
hn : 0 + 1 ≠ 0
⊢ ∑ i ∈ range (0 + 1), x ^ i ≠ 0

pp: case succ.succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x ≠ -1
n : ℕ
hn : n + 1 + 1 ≠ 0
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0

Tactic:
·

Goal state after:
case zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x ≠ -1
hn : 0 ≠ 0
⊢ ∑ i ∈ range 0, x ^ i ≠ 0
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case succ.zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x ≠ -1
hn : 0 + 1 ≠ 0
⊢ ∑ i ∈ range (0 + 1), x ^ i ≠ 0

pp: case succ.succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x ≠ -1
n : ℕ
hn : n + 1 + 1 ≠ 0
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0

Tactic:
·

Goal state after:
case succ.zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x ≠ -1
hn : 0 + 1 ≠ 0
⊢ ∑ i ∈ range (0 + 1), x ^ i ≠ 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case zero
s : Finset ℕ
hsub : s ⊆ properDivisors 0
⊢ ∑ x ∈ s, x = ∑ x ∈ properDivisors 0, x → s = properDivisors 0

pp: case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
⊢ ∑ x ∈ s, x = ∑ x ∈ (n✝ + 1).properDivisors, x → s = (n✝ + 1).properDivisors

Tactic:
·

Goal state after:
case zero
s : Finset ℕ
hsub : s ⊆ properDivisors 0
⊢ ∑ x ∈ s, x = ∑ x ∈ properDivisors 0, x → s = properDivisors 0
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case succ.succ.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
h : x + 1 < 0
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0

pp: case succ.succ.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
h : 0 < x + 1
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0

Tactic:
·

Goal state after:
case succ.succ.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
h : x + 1 < 0
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case pos
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
h : x + 1 < 0
h✝ : Even n.succ.succ
this : ∑ i ∈ range n.succ.succ, x ^ i < 0
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0

pp: case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
h : x + 1 < 0
h✝ : ¬Even n.succ.succ
this : 1 < ∑ i ∈ range n.succ.succ, x ^ i
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
h : x + 1 < 0
h✝ : Even n.succ.succ
this : ∑ i ∈ range n.succ.succ, x ^ i < 0
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
h : x + 1 < 0
h✝ : ¬Even n.succ.succ
this : 1 < ∑ i ∈ range n.succ.succ, x ^ i
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
h : x + 1 < 0
h✝ : ¬Even n.succ.succ
this : 1 < ∑ i ∈ range n.succ.succ, x ^ i
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inl
m n : ℕ
h : Nat.Coprime 0 1
to_fun : ZMod (0 * 1) → ZMod 0 × ZMod 1 := ⇑(castHom ⋯ (ZMod 0 × ZMod 1))
inv_fun : ZMod 0 × ZMod 1 → ZMod (0 * 1) :=
  fun x ↦
    if 0 * 1 = 0 then
      if 0 = 1 then ((RingHom.snd (ZMod 0) (ZMod 1)) x).cast else ((RingHom.fst (ZMod 0) (ZMod 1)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : 0 * 1 = 0
⊢ LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun

pp: case inr
m n : ℕ
h : Nat.Coprime 1 0
to_fun : ZMod (1 * 0) → ZMod 1 × ZMod 0 := ⇑(castHom ⋯ (ZMod 1 × ZMod 0))
inv_fun : ZMod 1 × ZMod 0 → ZMod (1 * 0) :=
  fun x ↦
    if 1 * 0 = 0 then
      if 1 = 1 then ((RingHom.snd (ZMod 1) (ZMod 0)) x).cast else ((RingHom.fst (ZMod 1) (ZMod 0)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : 1 * 0 = 0
⊢ LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun

Tactic:
·

Goal state after:
case inl
m n : ℕ
h : Nat.Coprime 0 1
to_fun : ZMod (0 * 1) → ZMod 0 × ZMod 1 := ⇑(castHom ⋯ (ZMod 0 × ZMod 1))
inv_fun : ZMod 0 × ZMod 1 → ZMod (0 * 1) :=
  fun x ↦
    if 0 * 1 = 0 then
      if 0 = 1 then ((RingHom.snd (ZMod 0) (ZMod 1)) x).cast else ((RingHom.fst (ZMod 0) (ZMod 1)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : 0 * 1 = 0
⊢ LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun