-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem le_biUnion_iff {πi : ∀ J, Prepartition J} {π' : Prepartition I} :
    π' ≤ π.biUnion πi ↔ π' ≤ π ∧ ∀ J ∈ π, π'.restrict J ≤ πi J

Proof state:
case refine_2.intro.intro.intro.intro.intro
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π
Hi : ∀ J ∈ π, π'.restrict J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
J : Box ι
hJ : J ∈ π
hle : J' ≤ J
this : J' ∈ π'.restrict J
Ji : Box ι
hJi : Ji ∈ πi J
hlei : J' ≤ Ji
⊢ ∃ I' ∈ π.biUnion πi, J' ≤ I'

Tactic:
exact ⟨Ji, π.mem_biUnion.2 ⟨J, hJ, hJi⟩, hlei⟩

Result:
no goals

Proof state:
case refine_2
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
⊢ (π' ≤ π ∧ ∀ J ∈ π, π'.restrict J ≤ πi J) → π' ≤ π.biUnion πi

Tactic:
rintro ⟨H, Hi⟩ J' hJ'

Result:
case refine_2.intro
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π
Hi : ∀ J ∈ π, π'.restrict J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
⊢ ∃ I' ∈ π.biUnion πi, J' ≤ I'

Proof state:
case refine_1
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π.biUnion πi
J : Box ι
hJ : J ∈ π
⊢ π'.restrict J ≤ (π.biUnion πi).restrict J

Tactic:
exact restrict_mono H

Result:
no goals

Proof state:
case refine_2.intro
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π
Hi : ∀ J ∈ π, π'.restrict J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
⊢ ∃ I' ∈ π.biUnion πi, J' ≤ I'

Tactic:
rcases H hJ' with ⟨J, hJ, hle⟩

Result:
case refine_2.intro.intro.intro
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π
Hi : ∀ J ∈ π, π'.restrict J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
J : Box ι
hJ : J ∈ π
hle : J' ≤ J
⊢ ∃ I' ∈ π.biUnion πi, J' ≤ I'

Proof state:
case refine_2.intro.intro.intro
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π
Hi : ∀ J ∈ π, π'.restrict J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
J : Box ι
hJ : J ∈ π
hle : J' ≤ J
⊢ ∃ I' ∈ π.biUnion πi, J' ≤ I'

Tactic:
have : J' ∈ π'.restrict J :=
  π'.mem_restrict.2 ⟨J', hJ', (inf_of_le_right <| WithBot.coe_le_coe.2 hle).symm⟩

Result:
case refine_2.intro.intro.intro
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π
Hi : ∀ J ∈ π, π'.restrict J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
J : Box ι
hJ : J ∈ π
hle : J' ≤ J
this : J' ∈ π'.restrict J
⊢ ∃ I' ∈ π.biUnion πi, J' ≤ I'

Proof state:
case refine_2.intro.intro.intro
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π
Hi : ∀ J ∈ π, π'.restrict J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
J : Box ι
hJ : J ∈ π
hle : J' ≤ J
this : J' ∈ π'.restrict J
⊢ ∃ I' ∈ π.biUnion πi, J' ≤ I'

Tactic:
rcases Hi J hJ this with ⟨Ji, hJi, hlei⟩

Result:
case refine_2.intro.intro.intro.intro.intro
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π
Hi : ∀ J ∈ π, π'.restrict J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
J : Box ι
hJ : J ∈ π
hle : J' ≤ J
this : J' ∈ π'.restrict J
Ji : Box ι
hJi : Ji ∈ πi J
hlei : J' ≤ Ji
⊢ ∃ I' ∈ π.biUnion πi, J' ≤ I'

Proof state:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
⊢ π' ≤ π.biUnion πi ↔ π' ≤ π ∧ ∀ J ∈ π, π'.restrict J ≤ πi J

Tactic:
refine ⟨fun H => ⟨H.trans (π.biUnion_le πi), fun J hJ => ?_⟩, ?_⟩

Result:
case refine_1
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π.biUnion πi
J : Box ι
hJ : J ∈ π
⊢ π'.restrict J ≤ πi J

case refine_2
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
⊢ (π' ≤ π ∧ ∀ J ∈ π, π'.restrict J ≤ πi J) → π' ≤ π.biUnion πi

Proof state:
case refine_1
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π.biUnion πi
J : Box ι
hJ : J ∈ π
⊢ π'.restrict J ≤ πi J

Tactic:
rw [← π.restrict_biUnion πi hJ]

Result:
case refine_1
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π.biUnion πi
J : Box ι
hJ : J ∈ π
⊢ π'.restrict J ≤ (π.biUnion πi).restrict J