[GOAL]
α : Type u_1
ι : Type u_2
inst✝² : LinearOrderedSemifield α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
α : Type u_1
ι : Type u_2
inst✝² : LinearOrderedSemifield α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i
[PROOFSTEP]
cases isEmpty_or_nonempty ι
[GOAL]
case intro.inl
α : Type u_1
ι : Type u_2
inst✝² : LinearOrderedSemifield α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
h✝ : IsEmpty ι
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i
[PROOFSTEP]
exact ⟨1, zero_lt_one, isEmptyElim⟩
[GOAL]
case intro.inr
α : Type u_1
ι : Type u_2
inst✝² : LinearOrderedSemifield α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
h✝ : Nonempty ι
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i
[PROOFSTEP]
choose ε hε hxε using fun i => exists_pos_add_of_lt' (h i)
[GOAL]
case intro.inr
α : Type u_1
ι : Type u_2
inst✝² : LinearOrderedSemifield α
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
[PROOFSTEP]
obtain rfl : x + ε = y := funext hxε
[GOAL]
case intro.inr
α : Type u_1
ι : Type u_2
inst✝² : LinearOrderedSemifield α
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
[PROOFSTEP]
have hε : 0 < Finset.univ.inf' Finset.univ_nonempty ε := (Finset.lt_inf'_iff _).2 fun i _ => hε _
[GOAL]
case intro.inr
α : Type u_1
ι : Type u_2
inst✝² : LinearOrderedSemifield α
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.inf' Finset.univ (_ : Finset.Nonempty Finset.univ) ε
⊢ ∃ ε_1, 0 < ε_1 ∧ ∀ (i : ι), x i + ε_1 < (x + ε) i
[PROOFSTEP]
exact ⟨_, half_pos hε, fun i => add_lt_add_left ((half_lt_self hε).trans_le <| Finset.inf'_le _ <| Finset.mem_univ _) _⟩
