awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Field.GeomSum
Goal:
K : Type u_1
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : CanonicallyOrderedAdd K
inst_4 : Sub K
inst_5 : OrderedSub K
x : K
h : x < 1
n : ℕ
⊢ ∑ i ∈ range n, x ^ i = (1 - x ^ n) / (1 - x)

Tactic:
eq_div_of_mul_eq (tsub_pos_of_lt h).ne' (geom_sum_mul_of_le_one h.le n)

Premises used: eq_div_of_mul_eq, LT.lt.le, LT.lt.ne', geom_sum_mul_of_le_one, tsub_pos_of_lt
-- Module: Mathlib.Algebra.Order.Field.GeomSum
Goal:
K : Type u_1
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : CanonicallyOrderedAdd K
inst_4 : Sub K
inst_5 : OrderedSub K
x : K
h0 : x ≠ 0
h1 : x < 1
n : ℕ
rw : ∀ (h0 : 0 < x) (h1 : x < 1) (n : ℕ), ∑ i ∈ range n, x ^ i < (1 - x)⁻¹
⊢ ∑ i ∈ range n, x ^ i < (1 - x)⁻¹

Tactic:
rw [← pos_iff_ne_zero] at h0

Premises used: pos_iff_ne_zero
-- Module: Mathlib.Algebra.Order.Field.GeomSum
Goal:
K : Type u_1
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : CanonicallyOrderedAdd K
inst_4 : Sub K
inst_5 : OrderedSub K
x : K
h0 : 0 < x
h1 : x < 1
n : ℕ
rw : LT.lt.{u_1} (α := K) 0 1 ∧ 0 < x ^ n
rw₁ : 1 - x ≠ 0
rw₂ : 0 < 1 - x
⊢ ∑ i ∈ range n, x ^ i < (1 - x)⁻¹

Tactic:
rw [geom_sum_of_lt_one h1, div_lt_iff₀, inv_mul_cancel₀, tsub_lt_self_iff]

Premises used: tsub_lt_self_iff, div_lt_iff₀, geom_sum_of_lt_one, inv_mul_cancel₀
-- Module: Mathlib.Algebra.Order.Field.GeomSum
Goal:
K : Type u_1
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : CanonicallyOrderedAdd K
inst_4 : Sub K
inst_5 : OrderedSub K
x : K
h0 : 0 < x
h1 : x < 1
n : ℕ
⊢ LT.lt.{u_1} (α := K) 0 1 ∧ 0 < x ^ n

Tactic:
⟨h0.trans h1, pow_pos h0 n⟩

Premises used: pow_pos, And.intro, LT.lt.trans
-- Module: Mathlib.Algebra.Order.Field.GeomSum
Goal:
K : Type u_1
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : CanonicallyOrderedAdd K
inst_4 : Sub K
inst_5 : OrderedSub K
x : K
h0 : 0 < x
h1 : x < 1
n : ℕ
⊢ LT.lt.{u_1} (α := K) 0 1 ∧ 0 < x ^ n

Tactic:
exact ⟨h0.trans h1, pow_pos h0 n⟩
-- Module: Mathlib.Algebra.Order.Field.GeomSum
Goal:
K : Type u_1
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : CanonicallyOrderedAdd K
inst_4 : Sub K
inst_5 : OrderedSub K
x : K
h0 : 0 < x
h1 : x < 1
n : ℕ
rwa : ¬1 - x = 0
rwa₁ : ¬1 ≤ x
rwa₂ rwa₃ rwa₄ rwa₅ : x < 1
⊢ 1 - x ≠ 0

Tactic:
rwa [ne_eq, tsub_eq_zero_iff_le, not_le]

Premises used: not_le, tsub_eq_zero_iff_le, ne_eq
-- Module: Mathlib.Algebra.Order.Field.GeomSum
Goal:
K : Type u_1
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : CanonicallyOrderedAdd K
inst_4 : Sub K
inst_5 : OrderedSub K
x : K
h0 : 0 < x
h1 : x < 1
n : ℕ
rwa rwa₁ rwa₂ rwa₃ : x < 1
⊢ 0 < 1 - x

Tactic:
rwa [tsub_pos_iff_lt]

Premises used: tsub_pos_iff_lt
-- Module: Mathlib.Algebra.Order.Field.GeomSum
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
x : K
m n : ℕ
hx : 0 ≤ x
h'x : x < 1
inl : ∀ (hmn : m ≤ n), ∑ i ∈ Ico m n, x ^ i ≤ x ^ m / (1 - x)
inr : ∀ (hmn : n < m), ∑ i ∈ Ico m n, x ^ i ≤ x ^ m / (1 - x)
⊢ ∑ i ∈ Ico m n, x ^ i ≤ x ^ m / (1 - x)

Tactic:
rcases le_or_gt m n with (hmn | hmn)

Premises used: le_or_gt
-- Module: Mathlib.Algebra.Order.Field.GeomSum
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
x : K
m n : ℕ
hx : 0 ≤ x
h'x : x < 1
hmn : m ≤ n
inl : (x ^ m - x ^ n) / (1 - x) ≤ x ^ m / (1 - x)
⊢ ∑ i ∈ Ico m n, x ^ i ≤ x ^ m / (1 - x)

Tactic:
rw [geom_sum_Ico' h'x.ne hmn]

Premises used: geom_sum_Ico', LT.lt.ne
-- Module: Mathlib.Algebra.Order.Field.GeomSum
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
x : K
m n : ℕ
hx : 0 ≤ x
h'x : x < 1
hmn : m ≤ n
apply : x ^ m - x ^ n ≤ x ^ m
⊢ (x ^ m - x ^ n) / (1 - x) ≤ x ^ m / (1 - x)

Tactic:
apply div_le_div₀ (pow_nonneg hx _) _ (sub_pos.2 h'x) le_rfl

Premises used: Iff.mpr, sub_pos, div_le_div₀, le_rfl, pow_nonneg
-- Module: Mathlib.Algebra.Order.Field.GeomSum
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
x : K
m n : ℕ
hx : 0 ≤ x
h'x : x < 1
hmn : m ≤ n
⊢ x ^ m - x ^ n ≤ x ^ m

Tactic:
simpa using pow_nonneg hx _

Premises used: pow_nonneg
-- Module: Mathlib.Algebra.Order.Field.GeomSum
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
x : K
m n : ℕ
hx : 0 ≤ x
h'x : x < 1
hmn : n < m
inr : 0 ≤ x ^ m / (1 - x)
inr₁ : ¬m < n
⊢ ∑ i ∈ Ico m n, x ^ i ≤ x ^ m / (1 - x)

Tactic:
rw [Ico_eq_empty, sum_empty]

Premises used: Finset.Ico_eq_empty, Finset.sum_empty
-- Module: Mathlib.Algebra.Order.Field.GeomSum
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
x : K
m n : ℕ
hx : 0 ≤ x
h'x : x < 1
hmn : n < m
inr : 0 ≤ 1 - x
⊢ 0 ≤ x ^ m / (1 - x)

Tactic:
apply div_nonneg (pow_nonneg hx _)

Premises used: pow_nonneg, div_nonneg
-- Module: Mathlib.Algebra.Order.Field.GeomSum
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
x : K
m n : ℕ
hx : 0 ≤ x
h'x : x < 1
hmn : n < m
⊢ 0 ≤ 1 - x

Tactic:
simpa using h'x.le

Premises used: LT.lt.le
-- Module: Mathlib.Algebra.Order.Field.GeomSum
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
x : K
m n : ℕ
hx : 0 ≤ x
h'x : x < 1
hmn : n < m
⊢ ¬m < n

Tactic:
simpa using hmn.le

Premises used: LT.lt.le
-- Module: Mathlib.Algebra.Order.Field.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Nontrivial α
inst_4 : DenselyOrdered α
inst_5 : ExistsAddOfLE α
inst_6 : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
intro : ∀ (val : Fintype ι), ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i
⊢ ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Algebra.Order.Field.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Nontrivial α
inst_4 : DenselyOrdered α
inst_5 : ExistsAddOfLE α
inst_6 : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val : Fintype ι
intro : IsEmpty ι → ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i
intro₁ : Nonempty ι → ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i
⊢ ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Algebra.Order.Field.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Nontrivial α
inst_4 : DenselyOrdered α
inst_5 : ExistsAddOfLE α
inst_6 : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val : Fintype ι
h_1 : IsEmpty ι
intro : ∀ (a : α) (ha : a ≠ 0), ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i
⊢ ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i

Tactic:
obtain ⟨a, ha⟩ := exists_ne (0 : α)

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Field.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Nontrivial α
inst_4 : DenselyOrdered α
inst_5 : ExistsAddOfLE α
inst_6 : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val : Fintype ι
h_1 : IsEmpty ι
a : α
ha : a ≠ 0
intro : ∀ (ha : a < 0), ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i
intro₁ : ∀ (ha : 0 < a), ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i
⊢ ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i

Tactic:
obtain ha | ha := ha.lt_or_gt

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Algebra.Order.Field.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Nontrivial α
inst_4 : DenselyOrdered α
inst_5 : ExistsAddOfLE α
inst_6 : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val : Fintype ι
h_1 : IsEmpty ι
a : α
ha_1 : a ≠ 0
ha : a < 0
intro : ∀ (b : α) (hb : 0 < b), ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i
⊢ ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i

Tactic:
obtain ⟨b, hb, -⟩ := exists_pos_add_of_lt' ha

Premises used: exists_pos_add_of_lt'
-- Module: Mathlib.Algebra.Order.Field.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Nontrivial α
inst_4 : DenselyOrdered α
inst_5 : ExistsAddOfLE α
inst_6 : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val : Fintype ι
h_1 : IsEmpty ι
a : α
ha_1 : a ≠ 0
ha : 0 < a
intro : ∀ (b : α) (hb : 0 < b), ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i
⊢ ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i

Tactic:
obtain ⟨b, hb, -⟩ := exists_pos_add_of_lt' ha

Premises used: exists_pos_add_of_lt'
-- Module: Mathlib.Algebra.Order.Field.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Nontrivial α
inst_4 : DenselyOrdered α
inst_5 : ExistsAddOfLE α
inst_6 : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val : Fintype ι
h_1 : IsEmpty ι
a : α
ha_1 : a ≠ 0
ha : a < 0
b : α
hb : 0 < b
⊢ ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i

Tactic:
⟨b, hb, isEmptyElim⟩

Premises used: isEmptyElim, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Order.Field.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Nontrivial α
inst_4 : DenselyOrdered α
inst_5 : ExistsAddOfLE α
inst_6 : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val : Fintype ι
h_1 : IsEmpty ι
a : α
ha_1 : a ≠ 0
ha : a < 0
b : α
hb : 0 < b
⊢ ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i

Tactic:
exact ⟨b, hb, isEmptyElim⟩
-- Module: Mathlib.Algebra.Order.Field.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Nontrivial α
inst_4 : DenselyOrdered α
inst_5 : ExistsAddOfLE α
inst_6 : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val : Fintype ι
h_1 : IsEmpty ι
a : α
ha_1 : a ≠ 0
ha : 0 < a
b : α
hb : 0 < b
⊢ ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i

Tactic:
⟨b, hb, isEmptyElim⟩

Premises used: isEmptyElim, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Order.Field.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Nontrivial α
inst_4 : DenselyOrdered α
inst_5 : ExistsAddOfLE α
inst_6 : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val : Fintype ι
h_1 : IsEmpty ι
a : α
ha_1 : a ≠ 0
ha : 0 < a
b : α
hb : 0 < b
⊢ ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i

Tactic:
exact ⟨b, hb, isEmptyElim⟩
-- Module: Mathlib.Algebra.Order.Field.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Nontrivial α
inst_4 : DenselyOrdered α
inst_5 : ExistsAddOfLE α
inst_6 : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val : Fintype ι
h_1 : Nonempty ι
intro :
  ∀ (ε : (i : ι) → α) (hε : ∀ (i : ι), 0 < ε i) (hxε : ∀ (i : ι), x i + ε i = y i),
    ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i
⊢ ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i

Tactic:
choose ε hε hxε using fun i => exists_pos_add_of_lt' (h i)

Premises used: exists_pos_add_of_lt'
-- Module: Mathlib.Algebra.Order.Field.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Nontrivial α
inst_4 : DenselyOrdered α
inst_5 : ExistsAddOfLE α
inst_6 : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val : Fintype ι
h_1 : Nonempty ι
ε : (i : ι) → α
hε : ∀ (i : ι), 0 < ε i
hxε : ∀ (i : ι), x i + ε i = y i
⊢ x + ε = y

Tactic:
funext hxε

Premises used: funext
-- Module: Mathlib.Algebra.Order.Field.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Nontrivial α
inst_4 : DenselyOrdered α
inst_5 : ExistsAddOfLE α
inst_6 : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val : Fintype ι
h_1 : Nonempty ι
ε : (i : ι) → α
hε : ∀ (i : ι), 0 < ε i
hxε : ∀ (i : ι), x i + ε i = y i
intro :
  ∀ (h : ∀ (i : ι), x i < (x + ε) i) (hxε : ∀ (i : ι), x i + ε i = (x + ε) i),
    ∃ (ε_1 : α), 0 < ε_1 ∧ ∀ (i : ι), x i + ε_1 < (x + ε) i
⊢ ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i

Tactic:
obtain rfl : x + ε = y := funext hxε

Premises used: funext, rfl
-- Module: Mathlib.Algebra.Order.Field.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Nontrivial α
inst_4 : DenselyOrdered α
inst_5 : ExistsAddOfLE α
inst_6 : Finite ι
x : ι → α
val : Fintype ι
h_1 : Nonempty ι
ε : (i : ι) → α
hε : ∀ (i : ι), 0 < ε i
h : ∀ (i : ι), x i < (x + ε) i
hxε : ∀ (i : ι), x i + ε i = (x + ε) i
⊢ 0 < Finset.inf' Finset.univ ⋯ ε

Tactic:
have hε : 0 < Finset.univ.inf' Finset.univ_nonempty ε := (Finset.lt_inf'_iff _).2 fun i _ => hε _
-- Module: Mathlib.Algebra.Order.Field.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Nontrivial α
inst_4 : DenselyOrdered α
inst_5 : ExistsAddOfLE α
inst_6 : Finite ι
x : ι → α
val : Fintype ι
h_1 : Nonempty ι
ε : (i : ι) → α
hε_1 : ∀ (i : ι), 0 < ε i
h : ∀ (i : ι), x i < (x + ε) i
hxε : ∀ (i : ι), x i + ε i = (x + ε) i
hε : 0 < Finset.inf' Finset.univ ⋯ ε
intro :
  ∀ (δ : α) (hδ : 0 < δ) (hδε : δ < Finset.inf' Finset.univ ⋯ ε),
    ∃ (ε_1 : α), 0 < ε_1 ∧ ∀ (i : ι), x i + ε_1 < (x + ε) i
⊢ ∃ (ε_1 : α), 0 < ε_1 ∧ ∀ (i : ι), x i + ε_1 < (x + ε) i

Tactic:
obtain ⟨δ, hδ, hδε⟩ := exists_between hε

Premises used: exists_between
-- Module: Mathlib.Algebra.Order.Field.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Nontrivial α
inst_4 : DenselyOrdered α
inst_5 : ExistsAddOfLE α
inst_6 : Finite ι
x : ι → α
val : Fintype ι
h_1 : Nonempty ι
ε : (i : ι) → α
hε_1 : ∀ (i : ι), 0 < ε i
h : ∀ (i : ι), x i < (x + ε) i
hxε : ∀ (i : ι), x i + ε i = (x + ε) i
hε : 0 < Finset.inf' Finset.univ ⋯ ε
δ : α
hδ : 0 < δ
hδε : δ < Finset.inf' Finset.univ ⋯ ε
⊢ ∃ (ε_1 : α), 0 < ε_1 ∧ ∀ (i : ι), x i + ε_1 < (x + ε) i

Tactic:
⟨δ, hδ, fun i ↦ add_lt_add_right (hδε.trans_le <| Finset.inf'_le _ <| Finset.mem_univ _) _⟩

Premises used: Finset.mem_univ, add_lt_add_right, LT.lt.trans_le, And.intro, Exists.intro, Finset.inf'_le
-- Module: Mathlib.Algebra.Order.Field.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Nontrivial α
inst_4 : DenselyOrdered α
inst_5 : ExistsAddOfLE α
inst_6 : Finite ι
x : ι → α
val : Fintype ι
h_1 : Nonempty ι
ε : (i : ι) → α
hε_1 : ∀ (i : ι), 0 < ε i
h : ∀ (i : ι), x i < (x + ε) i
hxε : ∀ (i : ι), x i + ε i = (x + ε) i
hε : 0 < Finset.inf' Finset.univ ⋯ ε
δ : α
hδ : 0 < δ
hδε : δ < Finset.inf' Finset.univ ⋯ ε
⊢ ∃ (ε_1 : α), 0 < ε_1 ∧ ∀ (i : ι), x i + ε_1 < (x + ε) i

Tactic:
exact ⟨δ, hδ, fun i ↦ add_lt_add_right (hδε.trans_le <| Finset.inf'_le _ <| Finset.mem_univ _) _⟩
-- Module: Mathlib.Algebra.Order.Field.Pointwise
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a b r : K
hr : 0 < r
⊢ r • Ioo a b = Ioo (r * a) (r * b)

Tactic:
(OrderIso.mulLeft₀ r hr).image_Ioo a b

Premises used: OrderIso.mulLeft₀, OrderIso.image_Ioo
-- Module: Mathlib.Algebra.Order.Field.Pointwise
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a b r : K
hr : 0 < r
⊢ r • Icc a b = Icc (r * a) (r * b)

Tactic:
(OrderIso.mulLeft₀ r hr).image_Icc a b

Premises used: OrderIso.image_Icc, OrderIso.mulLeft₀
-- Module: Mathlib.Algebra.Order.Field.Pointwise
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a b r : K
hr : 0 < r
⊢ r • Ico a b = Ico (r * a) (r * b)

Tactic:
(OrderIso.mulLeft₀ r hr).image_Ico a b

Premises used: OrderIso.image_Ico, OrderIso.mulLeft₀
-- Module: Mathlib.Algebra.Order.Field.Pointwise
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a b r : K
hr : 0 < r
⊢ r • Ioc a b = Ioc (r * a) (r * b)

Tactic:
(OrderIso.mulLeft₀ r hr).image_Ioc a b

Premises used: OrderIso.mulLeft₀, OrderIso.image_Ioc
-- Module: Mathlib.Algebra.Order.Field.Pointwise
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a r : K
hr : 0 < r
⊢ r • Ioi a = Ioi (r * a)

Tactic:
(OrderIso.mulLeft₀ r hr).image_Ioi a

Premises used: OrderIso.mulLeft₀, OrderIso.image_Ioi
-- Module: Mathlib.Algebra.Order.Field.Pointwise
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a r : K
hr : 0 < r
⊢ r • Iio a = Iio (r * a)

Tactic:
(OrderIso.mulLeft₀ r hr).image_Iio a

Premises used: OrderIso.image_Iio, OrderIso.mulLeft₀
-- Module: Mathlib.Algebra.Order.Field.Pointwise
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a r : K
hr : 0 < r
⊢ r • Ici a = Ici (r * a)

Tactic:
(OrderIso.mulLeft₀ r hr).image_Ici a

Premises used: OrderIso.image_Ici, OrderIso.mulLeft₀
-- Module: Mathlib.Algebra.Order.Field.Pointwise
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a r : K
hr : 0 < r
⊢ r • Iic a = Iic (r * a)

Tactic:
(OrderIso.mulLeft₀ r hr).image_Iic a

Premises used: OrderIso.image_Iic, OrderIso.mulLeft₀
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n : ℤ
hn : Even n
a : α
obtain : ∀ (k : ℤ), 0 ≤ a ^ (k + k)
⊢ 0 ≤ a ^ n

Tactic:
obtain ⟨k, rfl⟩ := hn

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
k : ℤ
⊢ a ≠ 0 ∨ k + k ≠ 0 ∨ k = 0 ∧ k = 0

Tactic:
simp [em']

Premises used: em'
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
k : ℤ
rw : 0 ≤ a ^ k * a ^ k
⊢ 0 ≤ a ^ (k + k)

Tactic:
rw [zpow_add' (by simp [em'])]

Premises used: zpow_add'
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
k : ℤ
⊢ 0 ≤ a ^ k * a ^ k

Tactic:
mul_self_nonneg _

Premises used: mul_self_nonneg
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
k : ℤ
⊢ 0 ≤ a ^ k * a ^ k

Tactic:
exact mul_self_nonneg _

Premises used: mul_self_nonneg
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
⊢ 0 ≤ HPow.hPow (β := ℤ) a 2

Tactic:
even_two.zpow_nonneg _

Premises used: even_two, Even.zpow_nonneg
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
⊢ 0 ≤ HPow.hPow (β := ℤ) a (-2)

Tactic:
even_neg_two.zpow_nonneg _

Premises used: even_neg_two, Even.zpow_nonneg
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
n : ℤ
hn : Even n
ha : a ≠ 0
⊢ 0 < a ^ n

Tactic:
(hn.zpow_nonneg _).lt_of_ne' (zpow_ne_zero _ ha)

Premises used: zpow_ne_zero, Even.zpow_nonneg, LE.le.lt_of_ne'
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
ha : a ≠ 0
⊢ 0 < HPow.hPow (β := ℤ) a 2

Tactic:
even_two.zpow_pos ha

Premises used: even_two, Even.zpow_pos
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
n : ℤ
hn : Even n
h : n ≠ 0
obtain : ∀ (k : ℤ) (h : k + k ≠ 0), 0 < a ^ (k + k) ↔ a ≠ 0
⊢ 0 < a ^ n ↔ a ≠ 0

Tactic:
obtain ⟨k, rfl⟩ := hn

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
k : ℤ
h : k + k ≠ 0
⊢ a ≠ 0 ∨ k + k ≠ 0 ∨ k = 0 ∧ k = 0

Tactic:
simp [em']

Premises used: em'
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
k : ℤ
h : k + k ≠ 0
⊢ k ≠ 0

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
k : ℤ
h : k + k ≠ 0
rw : 0 < a ^ k * a ^ k ↔ a ≠ 0
rw₁ : a ^ k ≠ 0 ↔ a ≠ 0
rw₂ rw₃ : a ≠ 0 ↔ a ≠ 0
⊢ 0 < a ^ (k + k) ↔ a ≠ 0

Tactic:
rw [zpow_add' (by simp [em']), mul_self_pos, zpow_ne_zero_iff (by simpa using h)]

Premises used: zpow_add', mul_self_pos, zpow_ne_zero_iff
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
n : ℤ
hn : Odd n
⊢ a ^ n < 0 ↔ a < 0

Tactic:
⟨lt_imp_lt_of_le_imp_le (zpow_nonneg · _), fun ha ↦ ?_⟩

Premises used: zpow_nonneg, Iff.intro, lt_imp_lt_of_le_imp_le
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
n : ℤ
hn : Odd n
refine : ∀ (ha : a < 0), a ^ n < 0
⊢ a ^ n < 0 ↔ a < 0

Tactic:
refine ⟨lt_imp_lt_of_le_imp_le (zpow_nonneg · _), fun ha ↦ ?_⟩
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
n : ℤ
hn : Odd n
ha : a < 0
obtain : ∀ (k : ℤ), a ^ (2 * k + 1) < 0
⊢ a ^ n < 0

Tactic:
obtain ⟨k, rfl⟩ := hn

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
ha : a < 0
k : ℤ
rw : a ^ (2 * k) * a < 0
⊢ a ^ (2 * k + 1) < 0

Tactic:
rw [zpow_add_one₀ ha.ne]

Premises used: zpow_add_one₀, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
ha : a < 0
k : ℤ
⊢ a ^ (2 * k) * a < 0

Tactic:
mul_neg_of_pos_of_neg (Even.zpow_pos (even_two_mul _) ha.ne) ha

Premises used: even_two_mul, mul_neg_of_pos_of_neg, LT.lt.ne, Even.zpow_pos
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
ha : a < 0
k : ℤ
⊢ a ^ (2 * k) * a < 0

Tactic:
exact mul_neg_of_pos_of_neg (Even.zpow_pos (even_two_mul _) ha.ne) ha

Premises used: even_two_mul, mul_neg_of_pos_of_neg, LT.lt.ne, Even.zpow_pos
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
n : ℤ
hn : Odd n
⊢ 0 ≤ a ^ n ↔ 0 ≤ a

Tactic:
le_iff_le_iff_lt_iff_lt.2 hn.zpow_neg_iff

Premises used: Iff.mpr, le_iff_le_iff_lt_iff_lt, Odd.zpow_neg_iff
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
n : ℤ
hn : Odd n
rw : n ≠ 0
⊢ a ^ n ≤ 0 ↔ a ≤ 0

Tactic:
rw [le_iff_lt_or_eq, le_iff_lt_or_eq, hn.zpow_neg_iff, zpow_eq_zero_iff]

Premises used: zpow_eq_zero_iff, le_iff_lt_or_eq, Odd.zpow_neg_iff
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hn : Odd (α := ℤ) 0
⊢ False

Tactic:
Int.not_even_iff_odd.2 hn .zero

Premises used: Iff.mpr, Even.zero, Int.not_even_iff_odd
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hn : Odd (α := ℤ) 0
⊢ False

Tactic:
exact Int.not_even_iff_odd.2 hn .zero

Premises used: Iff.mpr, Even.zero, Int.not_even_iff_odd
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
n : ℤ
hn : Odd n
⊢ 0 < a ^ n ↔ 0 < a

Tactic:
lt_iff_lt_of_le_iff_le hn.zpow_nonpos_iff

Premises used: Odd.zpow_nonpos_iff, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
p : ℤ
⊢ |a ^ p| = |a| ^ p

Tactic:
map_zpow₀ absHom a p

Premises used: abs, absHom, map_zpow₀
-- Module: Mathlib.Algebra.Order.Field.Power
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
p : ℤ
⊢ |HPow.hPow (α := α) (-1) p| = 1

Tactic:
simp