ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ (J : Box ι), J ∈ π₁ → πi₁ J = πi₂ J
⊢ biUnion π₁ πi₁ = biUnion π₁ πi₂
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
h : π₁ = π₂
hi : ∀ (J : Box ι), J ∈ π₁ → πi₁ J = πi₂ J
⊢ biUnion π₁ πi₁ = biUnion π₂ πi₂
subst π₂
case h
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ (J : Box ι), J ∈ π₁ → πi₁ J = πi₂ J
J : Box ι
⊢ J ∈ biUnion π₁ πi₁ ↔ J ∈ biUnion π₁ πi₂
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ (J : Box ι), J ∈ π₁ → πi₁ J = πi₂ J
⊢ biUnion π₁ πi₁ = biUnion π₁ πi₂
ext J
case h
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ (J : Box ι), J ∈ π₁ → πi₁ J = πi₂ J
J : Box ι
⊢ (∃ J', J' ∈ π₁ ∧ J ∈ πi₁ J') ↔ ∃ J', J' ∈ π₁ ∧ J ∈ πi₂ J'
case h
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ (J : Box ι), J ∈ π₁ → πi₁ J = πi₂ J
J : Box ι
⊢ J ∈ biUnion π₁ πi₁ ↔ J ∈ biUnion π₁ πi₂
simp only [mem_biUnion]
no goals
case h
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ (J : Box ι), J ∈ π₁ → πi₁ J = πi₂ J
J : Box ι
⊢ (∃ J', J' ∈ π₁ ∧ J ∈ πi₁ J') ↔ ∃ J', J' ∈ π₁ ∧ J ∈ πi₂ J'
constructor <;> exact fun ⟨J', h₁, h₂⟩ => ⟨J', h₁, hi J' h₁ ▸ h₂⟩