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

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

Tactic:
exact restrict_mono H

Result:
no goals

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

Tactic:
rcases hJ with ⟨J₁, h₁, hJ⟩

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

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

Tactic:
rw [mem_biUnion] at hJ

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

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

Tactic:
constructor <;> intro H J hJ

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

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

Proof state:
case mpr.intro.intro.intro.intro
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : ∀ J ∈ π, πi J ≤ π'.restrict J
J J₁ : Box ι
h₁ : J₁ ∈ π
hJ : J ∈ πi J₁
J₂ : Box ι
h₂ : J₂ ∈ π'.restrict J₁
Hle : J ≤ J₂
⊢ ∃ I' ∈ π', J ≤ I'

Tactic:
rcases π'.mem_restrict.mp h₂ with ⟨J₃, h₃, H⟩

Result:
case mpr.intro.intro.intro.intro.intro.intro
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H✝ : ∀ J ∈ π, πi J ≤ π'.restrict J
J J₁ : Box ι
h₁ : J₁ ∈ π
hJ : J ∈ πi J₁
J₂ : Box ι
h₂ : J₂ ∈ π'.restrict J₁
Hle : J ≤ J₂
J₃ : Box ι
h₃ : J₃ ∈ π'
H : ↑J₂ = ↑J₁ ⊓ ↑J₃
⊢ ∃ I' ∈ π', J ≤ I'

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

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

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

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

Tactic:
rcases H J₁ h₁ hJ with ⟨J₂, h₂, Hle⟩

Result:
case mpr.intro.intro.intro.intro
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : ∀ J ∈ π, πi J ≤ π'.restrict J
J J₁ : Box ι
h₁ : J₁ ∈ π
hJ : J ∈ πi J₁
J₂ : Box ι
h₂ : J₂ ∈ π'.restrict J₁
Hle : J ≤ J₂
⊢ ∃ I' ∈ π', J ≤ I'

Proof state:
case mpr.intro.intro.intro.intro.intro.intro
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H✝ : ∀ J ∈ π, πi J ≤ π'.restrict J
J J₁ : Box ι
h₁ : J₁ ∈ π
hJ : J ∈ πi J₁
J₂ : Box ι
h₂ : J₂ ∈ π'.restrict J₁
Hle : J ≤ J₂
J₃ : Box ι
h₃ : J₃ ∈ π'
H : ↑J₂ = ↑J₁ ⊓ ↑J₃
⊢ ∃ I' ∈ π', J ≤ I'

Tactic:
exact ⟨J₃, h₃, Hle.trans <| WithBot.coe_le_coe.1 <| H.trans_le inf_le_right⟩

Result:
no goals