case intro.intro
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
H : {i | Box.lower J₁ i = x i} = {i | Box.lower J₂ i = x i}
⊢ J₁ = J₂
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
⊢ InjOn (fun J => {i | Box.lower J i = x i}) {J | J ∈ π ∧ x ∈ ↑Box.Icc J}
rintro J₁ ⟨h₁, hx₁⟩ J₂ ⟨h₂, hx₂⟩ (H : { i | J₁.lower i = x i } = { i | J₂.lower i = x i })
case intro.intro
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
H : {i | Box.lower J₁ i = x i} = {i | Box.lower J₂ i = x i}
⊢ ∀ (i : ι), Set.Nonempty (Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i) ∩ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i))
case intro.intro
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
H : {i | Box.lower J₁ i = x i} = {i | Box.lower J₂ i = x i}
⊢ J₁ = J₂
suffices ∀ i, (Ioc (J₁.lower i) (J₁.upper i) ∩ Ioc (J₂.lower i) (J₂.upper i)).Nonempty by
  choose y hy₁ hy₂ using this
  exact π.eq_of_mem_of_mem h₁ h₂ hy₁ hy₂
case intro.intro
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
H : {i | Box.lower J₁ i = x i} = {i | Box.lower J₂ i = x i}
i : ι
⊢ Set.Nonempty (Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i) ∩ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i))
case intro.intro
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
H : {i | Box.lower J₁ i = x i} = {i | Box.lower J₂ i = x i}
⊢ ∀ (i : ι), Set.Nonempty (Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i) ∩ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i))
intro i
case intro.intro
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), Box.lower J₁ x_1 = x x_1 ↔ Box.lower J₂ x_1 = x x_1
⊢ Set.Nonempty (Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i) ∩ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i))
case intro.intro
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
H : {i | Box.lower J₁ i = x i} = {i | Box.lower J₂ i = x i}
i : ι
⊢ Set.Nonempty (Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i) ∩ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i))
simp only [Set.ext_iff, mem_setOf] at H
case intro.intro.inl
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), Box.lower J₁ x_1 = x x_1 ↔ Box.lower J₂ x_1 = x x_1
hi₁ : Box.lower J₁ i = x i
⊢ Set.Nonempty (Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i) ∩ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i))

case intro.intro.inr
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), Box.lower J₁ x_1 = x x_1 ↔ Box.lower J₂ x_1 = x x_1
hi₁ : Box.lower J₁ i < x i
⊢ Set.Nonempty (Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i) ∩ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i))
case intro.intro
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), Box.lower J₁ x_1 = x x_1 ↔ Box.lower J₂ x_1 = x x_1
⊢ Set.Nonempty (Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i) ∩ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i))
cases' (hx₁.1 i).eq_or_lt with hi₁ hi₁
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
H : {i | Box.lower J₁ i = x i} = {i | Box.lower J₂ i = x i}
y : ι → ℝ
hy₁ : ∀ (i : ι), y i ∈ Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i)
hy₂ : ∀ (i : ι), y i ∈ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i)
⊢ J₁ = J₂
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
H : {i | Box.lower J₁ i = x i} = {i | Box.lower J₂ i = x i}
this : ∀ (i : ι), Set.Nonempty (Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i) ∩ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i))
⊢ J₁ = J₂
choose y hy₁ hy₂ using this
no goals
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
H : {i | Box.lower J₁ i = x i} = {i | Box.lower J₂ i = x i}
y : ι → ℝ
hy₁ : ∀ (i : ι), y i ∈ Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i)
hy₂ : ∀ (i : ι), y i ∈ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i)
⊢ J₁ = J₂
exact π.eq_of_mem_of_mem h₁ h₂ hy₁ hy₂
case intro.intro.inl
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), Box.lower J₁ x_1 = x x_1 ↔ Box.lower J₂ x_1 = x x_1
hi₁ : Box.lower J₁ i = x i
hi₂ : Box.lower J₂ i = x i
⊢ Set.Nonempty (Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i) ∩ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i))
case intro.intro.inl
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), Box.lower J₁ x_1 = x x_1 ↔ Box.lower J₂ x_1 = x x_1
hi₁ : Box.lower J₁ i = x i
⊢ Set.Nonempty (Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i) ∩ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i))
have hi₂ : J₂.lower i = x i := (H _).1 hi₁
case intro.intro.inl
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), Box.lower J₁ x_1 = x x_1 ↔ Box.lower J₂ x_1 = x x_1
hi₁ : Box.lower J₁ i = x i
hi₂ : Box.lower J₂ i = x i
H₁ : x i < Box.upper J₁ i
⊢ Set.Nonempty (Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i) ∩ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i))
case intro.intro.inl
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), Box.lower J₁ x_1 = x x_1 ↔ Box.lower J₂ x_1 = x x_1
hi₁ : Box.lower J₁ i = x i
hi₂ : Box.lower J₂ i = x i
⊢ Set.Nonempty (Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i) ∩ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i))
have H₁ : x i < J₁.upper i := by simpa only [hi₁] using J₁.lower_lt_upper i
case intro.intro.inl
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), Box.lower J₁ x_1 = x x_1 ↔ Box.lower J₂ x_1 = x x_1
hi₁ : Box.lower J₁ i = x i
hi₂ : Box.lower J₂ i = x i
H₁ : x i < Box.upper J₁ i
H₂ : x i < Box.upper J₂ i
⊢ Set.Nonempty (Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i) ∩ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i))
case intro.intro.inl
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), Box.lower J₁ x_1 = x x_1 ↔ Box.lower J₂ x_1 = x x_1
hi₁ : Box.lower J₁ i = x i
hi₂ : Box.lower J₂ i = x i
H₁ : x i < Box.upper J₁ i
⊢ Set.Nonempty (Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i) ∩ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i))
have H₂ : x i < J₂.upper i := by simpa only [hi₂] using J₂.lower_lt_upper i
case intro.intro.inl
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), Box.lower J₁ x_1 = x x_1 ↔ Box.lower J₂ x_1 = x x_1
hi₁ : Box.lower J₁ i = x i
hi₂ : Box.lower J₂ i = x i
H₁ : x i < Box.upper J₁ i
H₂ : x i < Box.upper J₂ i
⊢ x i < Box.upper J₁ i ⊓ Box.upper J₂ i
case intro.intro.inl
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), Box.lower J₁ x_1 = x x_1 ↔ Box.lower J₂ x_1 = x x_1
hi₁ : Box.lower J₁ i = x i
hi₂ : Box.lower J₂ i = x i
H₁ : x i < Box.upper J₁ i
H₂ : x i < Box.upper J₂ i
⊢ Set.Nonempty (Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i) ∩ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i))
rw [Ioc_inter_Ioc, hi₁, hi₂, sup_idem, Set.nonempty_Ioc]
no goals
case intro.intro.inl
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), Box.lower J₁ x_1 = x x_1 ↔ Box.lower J₂ x_1 = x x_1
hi₁ : Box.lower J₁ i = x i
hi₂ : Box.lower J₂ i = x i
H₁ : x i < Box.upper J₁ i
H₂ : x i < Box.upper J₂ i
⊢ x i < Box.upper J₁ i ⊓ Box.upper J₂ i
exact lt_min H₁ H₂
no goals
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), Box.lower J₁ x_1 = x x_1 ↔ Box.lower J₂ x_1 = x x_1
hi₁ : Box.lower J₁ i = x i
hi₂ : Box.lower J₂ i = x i
⊢ x i < Box.upper J₁ i
simpa only [hi₁] using J₁.lower_lt_upper i
no goals
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), Box.lower J₁ x_1 = x x_1 ↔ Box.lower J₂ x_1 = x x_1
hi₁ : Box.lower J₁ i = x i
hi₂ : Box.lower J₂ i = x i
H₁ : x i < Box.upper J₁ i
⊢ x i < Box.upper J₂ i
simpa only [hi₂] using J₂.lower_lt_upper i
case intro.intro.inr
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), Box.lower J₁ x_1 = x x_1 ↔ Box.lower J₂ x_1 = x x_1
hi₁ : Box.lower J₁ i < x i
hi₂ : Box.lower J₂ i < x i
⊢ Set.Nonempty (Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i) ∩ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i))
case intro.intro.inr
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), Box.lower J₁ x_1 = x x_1 ↔ Box.lower J₂ x_1 = x x_1
hi₁ : Box.lower J₁ i < x i
⊢ Set.Nonempty (Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i) ∩ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i))
have hi₂ : J₂.lower i < x i := (hx₂.1 i).lt_of_ne (mt (H _).2 hi₁.ne)
no goals
case intro.intro.inr
ι : Type u_1
I J J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x✝ x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ ↑Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ ↑Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), Box.lower J₁ x_1 = x x_1 ↔ Box.lower J₂ x_1 = x x_1
hi₁ : Box.lower J₁ i < x i
hi₂ : Box.lower J₂ i < x i
⊢ Set.Nonempty (Set.Ioc (Box.lower J₁ i) (Box.upper J₁ i) ∩ Set.Ioc (Box.lower J₂ i) (Box.upper J₂ i))
exact ⟨x i, ⟨hi₁, hx₁.2 i⟩, ⟨hi₂, hx₂.2 i⟩⟩