-- Mathlib/Analysis/BoxIntegral/Partition/Split.lean
theorem eventually_splitMany_inf_eq_filter (π : Prepartition I) :
    ∀ᶠ t : Finset (ι × ℝ) in atTop,
      π ⊓ splitMany I t = (splitMany I t).filter fun J => ↑J ⊆ π.iUnion

Proof state:
case refine_1.intro.intro
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
J₁ : Box ι
h₁ : J₁ ∈ splitMany I t
hne : ↑J ⊓ ↑J₁ ≠ ⊥
⊢ ↑J₁ ⊆ ↑J

Tactic:
exact ht I J hJ J₁ h₁ (mt disjoint_iff.1 hne)

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint ↑J ↑J' → J' ≤ J
⊢ π ⊓ splitMany I t = (splitMany I t).filter fun J => ↑J ⊆ π.iUnion

Tactic:
refine le_antisymm ((biUnion_le_iff _).2 fun J hJ => ?_) (le_inf (fun J hJ => ?_) (filter_le _ _))

Result:
case refine_1
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
⊢ (splitMany I t).restrict J ≤ ((splitMany I t).filter fun J => ↑J ⊆ π.iUnion).restrict J

case refine_2
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ (splitMany I t).filter fun J => ↑J ⊆ π.iUnion
⊢ ∃ I' ∈ π, J ≤ I'

Proof state:
case refine_1
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
⊢ ∀ (J_1 : WithBot (Box ι)),
    (∃ a ∈ splitMany I t, ↑J ⊓ ↑a = J_1) →
      J_1 ≠ ⊥ → ∃ J', (∃ a, (a ∈ splitMany I t ∧ ↑a ⊆ π.iUnion) ∧ ↑J ⊓ ↑a = J') ∧ J_1 ≤ J'

Tactic:
rintro _ ⟨J₁, h₁, rfl⟩ hne

Result:
case refine_1.intro.intro
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
J₁ : Box ι
h₁ : J₁ ∈ splitMany I t
hne : ↑J ⊓ ↑J₁ ≠ ⊥
⊢ ∃ J', (∃ a, (a ∈ splitMany I t ∧ ↑a ⊆ π.iUnion) ∧ ↑J ⊓ ↑a = J') ∧ ↑J ⊓ ↑J₁ ≤ J'

Proof state:
case refine_2
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ splitMany I t ∧ ↑J ⊆ π.iUnion
⊢ ∃ I' ∈ π, J ≤ I'

Tactic:
rcases Set.mem_iUnion₂.1 (hJ.2 J.upper_mem) with ⟨J', hJ', hmem⟩

Result:
case refine_2.intro.intro
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ splitMany I t ∧ ↑J ⊆ π.iUnion
J' : Box ι
hJ' : J' ∈ π
hmem : J.upper ∈ ↑J'
⊢ ∃ I' ∈ π, J ≤ I'

Proof state:
case refine_1.intro.intro
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
J₁ : Box ι
h₁ : J₁ ∈ splitMany I t
hne : ↑J ⊓ ↑J₁ ≠ ⊥
⊢ ∃ J', (∃ a, (a ∈ splitMany I t ∧ ↑a ⊆ π.iUnion) ∧ ↑J ⊓ ↑a = J') ∧ ↑J ⊓ ↑J₁ ≤ J'

Tactic:
refine ⟨_, ⟨J₁, ⟨h₁, Subset.trans ?_ (π.subset_iUnion hJ)⟩, rfl⟩, le_rfl⟩

Result:
case refine_1.intro.intro
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
J₁ : Box ι
h₁ : J₁ ∈ splitMany I t
hne : ↑J ⊓ ↑J₁ ≠ ⊥
⊢ ↑J₁ ⊆ ↑J

Proof state:
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
⊢ ∀ᶠ (t : Finset (ι × ℝ)) in atTop, π ⊓ splitMany I t = (splitMany I t).filter fun J => ↑J ⊆ π.iUnion

Tactic:
refine (eventually_not_disjoint_imp_le_of_mem_splitMany π.boxes).mono fun t ht => ?_

Result:
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint ↑J ↑J' → J' ≤ J
⊢ π ⊓ splitMany I t = (splitMany I t).filter fun J => ↑J ⊆ π.iUnion

Proof state:
case refine_2.intro.intro
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ splitMany I t ∧ ↑J ⊆ π.iUnion
J' : Box ι
hJ' : J' ∈ π
hmem : J.upper ∈ ↑J'
⊢ (↑J' ∩ ↑J).Nonempty

Tactic:
exact ⟨J.upper, hmem, J.upper_mem⟩

Result:
no goals

Proof state:
case refine_1
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
⊢ ∀ J_1 ∈ Finset.image (fun J' => ↑J ⊓ ↑J') (splitMany I t).boxes,
    J_1 ≠ ⊥ → ∃ J' ∈ Finset.image (fun J' => ↑J ⊓ ↑J') ((splitMany I t).filter fun J => ↑J ⊆ π.iUnion).boxes, J_1 ≤ J'

Tactic:
simp only [Finset.mem_image, exists_prop, mem_boxes, mem_filter]

Result:
case refine_1
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
⊢ ∀ (J_1 : WithBot (Box ι)),
    (∃ a ∈ splitMany I t, ↑J ⊓ ↑a = J_1) →
      J_1 ≠ ⊥ → ∃ J', (∃ a, (a ∈ splitMany I t ∧ ↑a ⊆ π.iUnion) ∧ ↑J ⊓ ↑a = J') ∧ J_1 ≤ J'

Proof state:
case refine_2.intro.intro
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ splitMany I t ∧ ↑J ⊆ π.iUnion
J' : Box ι
hJ' : J' ∈ π
hmem : J.upper ∈ ↑J'
⊢ ∃ I' ∈ π, J ≤ I'

Tactic:
refine ⟨J', hJ', ht I _ hJ' _ hJ.1 <| Box.not_disjoint_coe_iff_nonempty_inter.2 ?_⟩

Result:
case refine_2.intro.intro
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ splitMany I t ∧ ↑J ⊆ π.iUnion
J' : Box ι
hJ' : J' ∈ π
hmem : J.upper ∈ ↑J'
⊢ (↑J' ∩ ↑J).Nonempty

Proof state:
case refine_2
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ (splitMany I t).filter fun J => ↑J ⊆ π.iUnion
⊢ ∃ I' ∈ π, J ≤ I'

Tactic:
rw [mem_filter] at hJ

Result:
case refine_2
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ splitMany I t ∧ ↑J ⊆ π.iUnion
⊢ ∃ I' ∈ π, J ≤ I'

Proof state:
case refine_1
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
⊢ (splitMany I t).restrict J ≤ ((splitMany I t).filter fun J => ↑J ⊆ π.iUnion).restrict J

Tactic:
refine ofWithBot_mono ?_

Result:
case refine_1
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
⊢ ∀ J_1 ∈ Finset.image (fun J' => ↑J ⊓ ↑J') (splitMany I t).boxes,
    J_1 ≠ ⊥ → ∃ J' ∈ Finset.image (fun J' => ↑J ⊓ ↑J') ((splitMany I t).filter fun J => ↑J ⊆ π.iUnion).boxes, J_1 ≤ J'