-- Mathlib/Algebra/Order/Field/Pi.lean
theorem Pi.exists_forall_pos_add_lt [ExistsAddOfLE α] [Finite ι] {x y : ι → α}
    (h : ∀ i, x i < y i) : ∃ ε, 0 < ε ∧ ∀ i, x i + ε < y i

Proof state:
case intro.inr
α : Type u_1
ι : Type u_2
inst✝⁴ : LinearOrderedCancelAddCommMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
h✝ : Nonempty ι
ε : ι → α
hε : ∀ (i : ι), 0 < ε i
hxε : ∀ (i : ι), x i + ε i = y i
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i

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

Result:
case intro.inr
α : Type u_1
ι : Type u_2
inst✝⁴ : LinearOrderedCancelAddCommMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x : ι → α
val✝ : Fintype ι
h✝ : Nonempty ι
ε : ι → α
hε : ∀ (i : ι), 0 < ε i
h : ∀ (i : ι), x i < (x + ε) i
hxε : ∀ (i : ι), x i + ε i = (x + ε) i
⊢ ∃ ε_1, 0 < ε_1 ∧ ∀ (i : ι), x i + ε_1 < (x + ε) i

Proof state:
case intro
α : Type u_1
ι : Type u_2
inst✝⁴ : LinearOrderedCancelAddCommMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i

Tactic:
cases isEmpty_or_nonempty ι

Result:
case intro.inl
α : Type u_1
ι : Type u_2
inst✝⁴ : LinearOrderedCancelAddCommMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
h✝ : IsEmpty ι
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i

case intro.inr
α : Type u_1
ι : Type u_2
inst✝⁴ : LinearOrderedCancelAddCommMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
h✝ : Nonempty ι
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i

Proof state:
α : Type u_1
ι : Type u_2
inst✝⁴ : LinearOrderedCancelAddCommMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i

Tactic:
cases nonempty_fintype ι

Result:
case intro
α : Type u_1
ι : Type u_2
inst✝⁴ : LinearOrderedCancelAddCommMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i

Proof state:
case intro.inr
α : Type u_1
ι : Type u_2
inst✝⁴ : LinearOrderedCancelAddCommMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
h✝ : Nonempty ι
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i

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

Result:
case intro.inr
α : Type u_1
ι : Type u_2
inst✝⁴ : LinearOrderedCancelAddCommMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
h✝ : Nonempty ι
ε : ι → α
hε : ∀ (i : ι), 0 < ε i
hxε : ∀ (i : ι), x i + ε i = y i
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i

Proof state:
case intro.inl.intro
α : Type u_1
ι : Type u_2
inst✝⁴ : LinearOrderedCancelAddCommMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
h✝ : IsEmpty ι
a : α
ha : a ≠ 0
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i

Tactic:
obtain ha | ha := ha.lt_or_lt <;> obtain ⟨b, hb, -⟩ := exists_pos_add_of_lt' ha <;>
  exact ⟨b, hb, isEmptyElim⟩

Result:
no goals

Proof state:
case intro.inr
α : Type u_1
ι : Type u_2
inst✝⁴ : LinearOrderedCancelAddCommMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x : ι → α
val✝ : Fintype ι
h✝ : Nonempty ι
ε : ι → α
hε✝ : ∀ (i : ι), 0 < ε i
h : ∀ (i : ι), x i < (x + ε) i
hxε : ∀ (i : ι), x i + ε i = (x + ε) i
hε : 0 < Finset.univ.inf' ⋯ ε
⊢ ∃ ε_1, 0 < ε_1 ∧ ∀ (i : ι), x i + ε_1 < (x + ε) i

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

Result:
case intro.inr.intro.intro
α : Type u_1
ι : Type u_2
inst✝⁴ : LinearOrderedCancelAddCommMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x : ι → α
val✝ : Fintype ι
h✝ : Nonempty ι
ε : ι → α
hε✝ : ∀ (i : ι), 0 < ε i
h : ∀ (i : ι), x i < (x + ε) i
hxε : ∀ (i : ι), x i + ε i = (x + ε) i
hε : 0 < Finset.univ.inf' ⋯ ε
δ : α
hδ : 0 < δ
hδε : δ < Finset.univ.inf' ⋯ ε
⊢ ∃ ε_1, 0 < ε_1 ∧ ∀ (i : ι), x i + ε_1 < (x + ε) i

Proof state:
case intro.inr
α : Type u_1
ι : Type u_2
inst✝⁴ : LinearOrderedCancelAddCommMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x : ι → α
val✝ : Fintype ι
h✝ : Nonempty ι
ε : ι → α
hε : ∀ (i : ι), 0 < ε i
h : ∀ (i : ι), x i < (x + ε) i
hxε : ∀ (i : ι), x i + ε i = (x + ε) i
⊢ ∃ ε_1, 0 < ε_1 ∧ ∀ (i : ι), x i + ε_1 < (x + ε) i

Tactic:
have hε : 0 < Finset.univ.inf' Finset.univ_nonempty ε := (Finset.lt_inf'_iff _).2 fun i _ => hε _

Result:
case intro.inr
α : Type u_1
ι : Type u_2
inst✝⁴ : LinearOrderedCancelAddCommMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x : ι → α
val✝ : Fintype ι
h✝ : Nonempty ι
ε : ι → α
hε✝ : ∀ (i : ι), 0 < ε i
h : ∀ (i : ι), x i < (x + ε) i
hxε : ∀ (i : ι), x i + ε i = (x + ε) i
hε : 0 < Finset.univ.inf' ⋯ ε
⊢ ∃ ε_1, 0 < ε_1 ∧ ∀ (i : ι), x i + ε_1 < (x + ε) i

Proof state:
case intro.inl
α : Type u_1
ι : Type u_2
inst✝⁴ : LinearOrderedCancelAddCommMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
h✝ : IsEmpty ι
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i

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

Result:
case intro.inl.intro
α : Type u_1
ι : Type u_2
inst✝⁴ : LinearOrderedCancelAddCommMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
h✝ : IsEmpty ι
a : α
ha : a ≠ 0
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i

Proof state:
case intro.inr.intro.intro
α : Type u_1
ι : Type u_2
inst✝⁴ : LinearOrderedCancelAddCommMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x : ι → α
val✝ : Fintype ι
h✝ : Nonempty ι
ε : ι → α
hε✝ : ∀ (i : ι), 0 < ε i
h : ∀ (i : ι), x i < (x + ε) i
hxε : ∀ (i : ι), x i + ε i = (x + ε) i
hε : 0 < Finset.univ.inf' ⋯ ε
δ : α
hδ : 0 < δ
hδε : δ < Finset.univ.inf' ⋯ ε
⊢ ∃ ε_1, 0 < ε_1 ∧ ∀ (i : ι), x i + ε_1 < (x + ε) i

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

Result:
no goals