no goals
case refine'_1
ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I J✝ : Box ι
π : TaggedPrepartition I
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π₁ π₂ : TaggedPrepartition I
h : Disjoint (TaggedPrepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
J : Box ι
hJ : J ∈ π₁.boxes
⊢ ↑(↑vol J) (f (tag (TaggedPrepartition.disjUnion π₁ π₂ h) J)) = ↑(↑vol J) (f (tag π₁ J))
rw [disjUnion_tag_of_mem_left _ hJ]
no goals
case refine'_2
ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I J✝ : Box ι
π : TaggedPrepartition I
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π₁ π₂ : TaggedPrepartition I
h : Disjoint (TaggedPrepartition.iUnion π₁) (TaggedPrepartition.iUnion π₂)
J : Box ι
hJ : J ∈ π₂.boxes
⊢ ↑(↑vol J) (f (tag (TaggedPrepartition.disjUnion π₁ π₂ h) J)) = ↑(↑vol J) (f (tag π₂ J))
rw [disjUnion_tag_of_mem_right _ hJ]