-- Mathlib/Analysis/BoxIntegral/Partition/Filter.lean
theorem tendsto_embedBox_toFilteriUnion_top (l : IntegrationParams) (h : I ≤ J) :
    Tendsto (TaggedPrepartition.embedBox I J h) (l.toFilteriUnion I ⊤)
      (l.toFilteriUnion J (Prepartition.single J I h))

Proof state:
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
⊢ Tendsto (⇑(embedBox I J h)) (l.toFilterDistortioniUnion I c ⊤)
    (⨆ c, l.toFilterDistortioniUnion J c (Prepartition.single J I h))

Tactic:
set π₀ := Prepartition.single J I h

Result:
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
⊢ Tendsto (⇑(embedBox I J h)) (l.toFilterDistortioniUnion I c ⊤) (⨆ c, l.toFilterDistortioniUnion J c π₀)

Proof state:
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
⊢ Filter.map (⇑(embedBox I J h)) (l.toFilterDistortioniUnion I c ⊤) ≤
    l.toFilterDistortioniUnion J (c ⊔ π₀.compl.distortion) π₀

Tactic:
refine ((l.hasBasis_toFilterDistortioniUnion I c ⊤).tendsto_iff
  (l.hasBasis_toFilterDistortioniUnion J _ _)).2 fun r hr => ?_

Result:
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → ↑(Set.Ioi 0)
hr : l.RCond r
⊢ ∃ ia,
    l.RCond ia ∧
      ∀ x ∈ {π | l.MemBaseSet I c ia π ∧ π.iUnion = ⊤.iUnion},
        (embedBox I J h) x ∈ {π | l.MemBaseSet J (c ⊔ π₀.compl.distortion) r π ∧ π.iUnion = π₀.iUnion}

Proof state:
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
⊢ Tendsto (⇑(embedBox I J h)) (l.toFilterDistortioniUnion I c ⊤) (⨆ c, l.toFilterDistortioniUnion J c π₀)

Tactic:
refine le_iSup_of_le (max c π₀.compl.distortion) ?_

Result:
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
⊢ Filter.map (⇑(embedBox I J h)) (l.toFilterDistortioniUnion I c ⊤) ≤
    l.toFilterDistortioniUnion J (c ⊔ π₀.compl.distortion) π₀

Proof state:
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
⊢ ∀ (i : ℝ≥0),
    Tendsto (⇑(embedBox I J h)) (l.toFilterDistortioniUnion I i ⊤)
      (⨆ c, l.toFilterDistortioniUnion J c (Prepartition.single J I h))

Tactic:
intro c

Result:
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
⊢ Tendsto (⇑(embedBox I J h)) (l.toFilterDistortioniUnion I c ⊤)
    (⨆ c, l.toFilterDistortioniUnion J c (Prepartition.single J I h))

Proof state:
case refine_2
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → ↑(Set.Ioi 0)
hr : l.RCond r
π : TaggedPrepartition I
hπ : l.MemBaseSet I c r π ∧ π.iUnion = ↑I
⊢ ((embedBox I J h) π).iUnion = π₀.iUnion

Tactic:
exact hπ.2.trans (Prepartition.iUnion_single _).symm

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → ↑(Set.Ioi 0)
hr : l.RCond r
π : TaggedPrepartition I
hπ : π ∈ {π | l.MemBaseSet I c r π ∧ π.iUnion = ⊤.iUnion}
⊢ (embedBox I J h) π ∈ {π | l.MemBaseSet J (c ⊔ π₀.compl.distortion) r π ∧ π.iUnion = π₀.iUnion}

Tactic:
rw [mem_setOf_eq, Prepartition.iUnion_top] at hπ

Result:
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → ↑(Set.Ioi 0)
hr : l.RCond r
π : TaggedPrepartition I
hπ : l.MemBaseSet I c r π ∧ π.iUnion = ↑I
⊢ (embedBox I J h) π ∈ {π | l.MemBaseSet J (c ⊔ π₀.compl.distortion) r π ∧ π.iUnion = π₀.iUnion}

Proof state:
case refine_1.e_a
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → ↑(Set.Ioi 0)
hr : l.RCond r
π : TaggedPrepartition I
hπ : l.MemBaseSet I c r π ∧ π.iUnion = ↑I
x✝ : l.bDistortion = true
⊢ π₀.iUnion = ((embedBox I J h) π).iUnion

Tactic:
exact (Prepartition.iUnion_single h).trans hπ.2.symm

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → ↑(Set.Ioi 0)
hr : l.RCond r
⊢ ∃ ia,
    l.RCond ia ∧
      ∀ x ∈ {π | l.MemBaseSet I c ia π ∧ π.iUnion = ⊤.iUnion},
        (embedBox I J h) x ∈ {π | l.MemBaseSet J (c ⊔ π₀.compl.distortion) r π ∧ π.iUnion = π₀.iUnion}

Tactic:
refine ⟨r, hr, fun π hπ => ?_⟩

Result:
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → ↑(Set.Ioi 0)
hr : l.RCond r
π : TaggedPrepartition I
hπ : π ∈ {π | l.MemBaseSet I c r π ∧ π.iUnion = ⊤.iUnion}
⊢ (embedBox I J h) π ∈ {π | l.MemBaseSet J (c ⊔ π₀.compl.distortion) r π ∧ π.iUnion = π₀.iUnion}

Proof state:
case refine_1
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → ↑(Set.Ioi 0)
hr : l.RCond r
π : TaggedPrepartition I
hπ : l.MemBaseSet I c r π ∧ π.iUnion = ↑I
x✝ : l.bDistortion = true
⊢ ↑J \ π₀.iUnion = ↑J \ ((embedBox I J h) π).iUnion

Tactic:
congr 1

Result:
case refine_1.e_a
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → ↑(Set.Ioi 0)
hr : l.RCond r
π : TaggedPrepartition I
hπ : l.MemBaseSet I c r π ∧ π.iUnion = ↑I
x✝ : l.bDistortion = true
⊢ π₀.iUnion = ((embedBox I J h) π).iUnion

Proof state:
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → ↑(Set.Ioi 0)
hr : l.RCond r
π : TaggedPrepartition I
hπ : l.MemBaseSet I c r π ∧ π.iUnion = ↑I
⊢ (embedBox I J h) π ∈ {π | l.MemBaseSet J (c ⊔ π₀.compl.distortion) r π ∧ π.iUnion = π₀.iUnion}

Tactic:
refine ⟨⟨hπ.1.1, hπ.1.2, fun hD => le_trans (hπ.1.3 hD) (le_max_left _ _), fun _ => ?_⟩, ?_⟩

Result:
case refine_1
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → ↑(Set.Ioi 0)
hr : l.RCond r
π : TaggedPrepartition I
hπ : l.MemBaseSet I c r π ∧ π.iUnion = ↑I
x✝ : l.bDistortion = true
⊢ ∃ π', π'.iUnion = ↑J \ ((embedBox I J h) π).iUnion ∧ π'.distortion ≤ c ⊔ π₀.compl.distortion

case refine_2
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → ↑(Set.Ioi 0)
hr : l.RCond r
π : TaggedPrepartition I
hπ : l.MemBaseSet I c r π ∧ π.iUnion = ↑I
⊢ ((embedBox I J h) π).iUnion = π₀.iUnion

Proof state:
case refine_1
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → ↑(Set.Ioi 0)
hr : l.RCond r
π : TaggedPrepartition I
hπ : l.MemBaseSet I c r π ∧ π.iUnion = ↑I
x✝ : l.bDistortion = true
⊢ ∃ π', π'.iUnion = ↑J \ ((embedBox I J h) π).iUnion ∧ π'.distortion ≤ c ⊔ π₀.compl.distortion

Tactic:
refine ⟨_, π₀.iUnion_compl.trans ?_, le_max_right _ _⟩

Result:
case refine_1
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → ↑(Set.Ioi 0)
hr : l.RCond r
π : TaggedPrepartition I
hπ : l.MemBaseSet I c r π ∧ π.iUnion = ↑I
x✝ : l.bDistortion = true
⊢ ↑J \ π₀.iUnion = ↑J \ ((embedBox I J h) π).iUnion