α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.191544
G : Type ?u.191547
𝕜 : Type ?u.191550
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
h : ∀ (x y : E), x ≠ y → T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0
h_pair : Integrable ↑(pair f g)
⊢ setToSimpleFunc T (map Prod.fst (pair f g)) = setToSimpleFunc T (map Prod.snd (pair f g))
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.191544
G : Type ?u.191547
𝕜 : Type ?u.191550
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
h : ∀ (x y : E), x ≠ y → T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0
⊢ setToSimpleFunc T (map Prod.fst (pair f g)) = setToSimpleFunc T (map Prod.snd (pair f g))
have h_pair : Integrable (f.pair g) μ := integrable_pair hf hg
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.191544
G : Type ?u.191547
𝕜 : Type ?u.191550
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
h : ∀ (x y : E), x ≠ y → T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0
h_pair : Integrable ↑(pair f g)
⊢ ∑ x in SimpleFunc.range (pair f g), ↑(T (↑(pair f g) ⁻¹' {x})) x.fst = setToSimpleFunc T (map Prod.snd (pair f g))
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.191544
G : Type ?u.191547
𝕜 : Type ?u.191550
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
h : ∀ (x y : E), x ≠ y → T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0
h_pair : Integrable ↑(pair f g)
⊢ setToSimpleFunc T (map Prod.fst (pair f g)) = setToSimpleFunc T (map Prod.snd (pair f g))
rw [map_setToSimpleFunc T h_add h_pair Prod.fst_zero]
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.191544
G : Type ?u.191547
𝕜 : Type ?u.191550
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
h : ∀ (x y : E), x ≠ y → T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0
h_pair : Integrable ↑(pair f g)
⊢ ∑ x in SimpleFunc.range (pair f g), ↑(T (↑(pair f g) ⁻¹' {x})) x.fst =
    ∑ x in SimpleFunc.range (pair f g), ↑(T (↑(pair f g) ⁻¹' {x})) x.snd
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.191544
G : Type ?u.191547
𝕜 : Type ?u.191550
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
h : ∀ (x y : E), x ≠ y → T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0
h_pair : Integrable ↑(pair f g)
⊢ ∑ x in SimpleFunc.range (pair f g), ↑(T (↑(pair f g) ⁻¹' {x})) x.fst = setToSimpleFunc T (map Prod.snd (pair f g))
rw [map_setToSimpleFunc T h_add h_pair Prod.snd_zero]
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.191544
G : Type ?u.191547
𝕜 : Type ?u.191550
p✝ : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
h : ∀ (x y : E), x ≠ y → T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0
h_pair : Integrable ↑(pair f g)
p : E × E
hp : p ∈ SimpleFunc.range (pair f g)
⊢ ↑(T (↑(pair f g) ⁻¹' {p})) p.fst = ↑(T (↑(pair f g) ⁻¹' {p})) p.snd
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.191544
G : Type ?u.191547
𝕜 : Type ?u.191550
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
h : ∀ (x y : E), x ≠ y → T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0
h_pair : Integrable ↑(pair f g)
⊢ ∑ x in SimpleFunc.range (pair f g), ↑(T (↑(pair f g) ⁻¹' {x})) x.fst =
    ∑ x in SimpleFunc.range (pair f g), ↑(T (↑(pair f g) ⁻¹' {x})) x.snd
refine' Finset.sum_congr rfl fun p hp => _
case intro
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.191544
G : Type ?u.191547
𝕜 : Type ?u.191550
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
h : ∀ (x y : E), x ≠ y → T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0
h_pair : Integrable ↑(pair f g)
a : α
hp : ↑(pair f g) a ∈ SimpleFunc.range (pair f g)
⊢ ↑(T (↑(pair f g) ⁻¹' {↑(pair f g) a})) (↑(pair f g) a).fst =
    ↑(T (↑(pair f g) ⁻¹' {↑(pair f g) a})) (↑(pair f g) a).snd
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.191544
G : Type ?u.191547
𝕜 : Type ?u.191550
p✝ : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
h : ∀ (x y : E), x ≠ y → T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0
h_pair : Integrable ↑(pair f g)
p : E × E
hp : p ∈ SimpleFunc.range (pair f g)
⊢ ↑(T (↑(pair f g) ⁻¹' {p})) p.fst = ↑(T (↑(pair f g) ⁻¹' {p})) p.snd
rcases mem_range.1 hp with ⟨a, rfl⟩
case pos
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.191544
G : Type ?u.191547
𝕜 : Type ?u.191550
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
h : ∀ (x y : E), x ≠ y → T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0
h_pair : Integrable ↑(pair f g)
a : α
hp : ↑(pair f g) a ∈ SimpleFunc.range (pair f g)
eq : ↑f a = ↑g a
⊢ ↑(T (↑(pair f g) ⁻¹' {↑(pair f g) a})) (↑(pair f g) a).fst =
    ↑(T (↑(pair f g) ⁻¹' {↑(pair f g) a})) (↑(pair f g) a).snd

case neg
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.191544
G : Type ?u.191547
𝕜 : Type ?u.191550
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
h : ∀ (x y : E), x ≠ y → T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0
h_pair : Integrable ↑(pair f g)
a : α
hp : ↑(pair f g) a ∈ SimpleFunc.range (pair f g)
eq : ¬↑f a = ↑g a
⊢ ↑(T (↑(pair f g) ⁻¹' {↑(pair f g) a})) (↑(pair f g) a).fst =
    ↑(T (↑(pair f g) ⁻¹' {↑(pair f g) a})) (↑(pair f g) a).snd
case intro
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.191544
G : Type ?u.191547
𝕜 : Type ?u.191550
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
h : ∀ (x y : E), x ≠ y → T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0
h_pair : Integrable ↑(pair f g)
a : α
hp : ↑(pair f g) a ∈ SimpleFunc.range (pair f g)
⊢ ↑(T (↑(pair f g) ⁻¹' {↑(pair f g) a})) (↑(pair f g) a).fst =
    ↑(T (↑(pair f g) ⁻¹' {↑(pair f g) a})) (↑(pair f g) a).snd
by_cases eq : f a = g a
case pos
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.191544
G : Type ?u.191547
𝕜 : Type ?u.191550
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
h : ∀ (x y : E), x ≠ y → T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0
h_pair : Integrable ↑(pair f g)
a : α
hp : ↑(pair f g) a ∈ SimpleFunc.range (pair f g)
eq : ↑f a = ↑g a
⊢ ↑(T (↑(pair f g) ⁻¹' {(↑f a, ↑g a)})) (↑f a) = ↑(T (↑(pair f g) ⁻¹' {(↑f a, ↑g a)})) (↑g a)
case pos
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.191544
G : Type ?u.191547
𝕜 : Type ?u.191550
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
h : ∀ (x y : E), x ≠ y → T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0
h_pair : Integrable ↑(pair f g)
a : α
hp : ↑(pair f g) a ∈ SimpleFunc.range (pair f g)
eq : ↑f a = ↑g a
⊢ ↑(T (↑(pair f g) ⁻¹' {↑(pair f g) a})) (↑(pair f g) a).fst =
    ↑(T (↑(pair f g) ⁻¹' {↑(pair f g) a})) (↑(pair f g) a).snd
dsimp only [pair_apply]
no goals
case pos
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.191544
G : Type ?u.191547
𝕜 : Type ?u.191550
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
h : ∀ (x y : E), x ≠ y → T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0
h_pair : Integrable ↑(pair f g)
a : α
hp : ↑(pair f g) a ∈ SimpleFunc.range (pair f g)
eq : ↑f a = ↑g a
⊢ ↑(T (↑(pair f g) ⁻¹' {(↑f a, ↑g a)})) (↑f a) = ↑(T (↑(pair f g) ⁻¹' {(↑f a, ↑g a)})) (↑g a)
rw [eq]
case neg
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.191544
G : Type ?u.191547
𝕜 : Type ?u.191550
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
h : ∀ (x y : E), x ≠ y → T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0
h_pair : Integrable ↑(pair f g)
a : α
hp : ↑(pair f g) a ∈ SimpleFunc.range (pair f g)
eq : ¬↑f a = ↑g a
this : T (↑(pair f g) ⁻¹' {(↑f a, ↑g a)}) = 0
⊢ ↑(T (↑(pair f g) ⁻¹' {↑(pair f g) a})) (↑(pair f g) a).fst =
    ↑(T (↑(pair f g) ⁻¹' {↑(pair f g) a})) (↑(pair f g) a).snd
case neg
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.191544
G : Type ?u.191547
𝕜 : Type ?u.191550
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
h : ∀ (x y : E), x ≠ y → T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0
h_pair : Integrable ↑(pair f g)
a : α
hp : ↑(pair f g) a ∈ SimpleFunc.range (pair f g)
eq : ¬↑f a = ↑g a
⊢ ↑(T (↑(pair f g) ⁻¹' {↑(pair f g) a})) (↑(pair f g) a).fst =
    ↑(T (↑(pair f g) ⁻¹' {↑(pair f g) a})) (↑(pair f g) a).snd
have : T (pair f g ⁻¹' {(f a, g a)}) = 0 := by
  have h_eq : T ((⇑(f.pair g)) ⁻¹' {(f a, g a)}) = T (f ⁻¹' {f a} ∩ g ⁻¹' {g a}) := by
    congr; rw [pair_preimage_singleton f g]
  rw [h_eq]
  exact h (f a) (g a) eq
no goals
case neg
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.191544
G : Type ?u.191547
𝕜 : Type ?u.191550
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
h : ∀ (x y : E), x ≠ y → T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0
h_pair : Integrable ↑(pair f g)
a : α
hp : ↑(pair f g) a ∈ SimpleFunc.range (pair f g)
eq : ¬↑f a = ↑g a
this : T (↑(pair f g) ⁻¹' {(↑f a, ↑g a)}) = 0
⊢ ↑(T (↑(pair f g) ⁻¹' {↑(pair f g) a})) (↑(pair f g) a).fst =
    ↑(T (↑(pair f g) ⁻¹' {↑(pair f g) a})) (↑(pair f g) a).snd
simp only [this, ContinuousLinearMap.zero_apply, pair_apply]
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.191544
G : Type ?u.191547
𝕜 : Type ?u.191550
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
h : ∀ (x y : E), x ≠ y → T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0
h_pair : Integrable ↑(pair f g)
a : α
hp : ↑(pair f g) a ∈ SimpleFunc.range (pair f g)
eq : ¬↑f a = ↑g a
h_eq : T (↑(pair f g) ⁻¹' {(↑f a, ↑g a)}) = T (↑f ⁻¹' {↑f a} ∩ ↑g ⁻¹' {↑g a})
⊢ T (↑(pair f g) ⁻¹' {(↑f a, ↑g a)}) = 0
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.191544
G : Type ?u.191547
𝕜 : Type ?u.191550
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
h : ∀ (x y : E), x ≠ y → T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0
h_pair : Integrable ↑(pair f g)
a : α
hp : ↑(pair f g) a ∈ SimpleFunc.range (pair f g)
eq : ¬↑f a = ↑g a
⊢ T (↑(pair f g) ⁻¹' {(↑f a, ↑g a)}) = 0
have h_eq : T ((⇑(f.pair g)) ⁻¹' {(f a, g a)}) = T (f ⁻¹' {f a} ∩ g ⁻¹' {g a}) := by
  congr; rw [pair_preimage_singleton f g]
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.191544
G : Type ?u.191547
𝕜 : Type ?u.191550
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
h : ∀ (x y : E), x ≠ y → T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0
h_pair : Integrable ↑(pair f g)
a : α
hp : ↑(pair f g) a ∈ SimpleFunc.range (pair f g)
eq : ¬↑f a = ↑g a
h_eq : T (↑(pair f g) ⁻¹' {(↑f a, ↑g a)}) = T (↑f ⁻¹' {↑f a} ∩ ↑g ⁻¹' {↑g a})
⊢ T (↑f ⁻¹' {↑f a} ∩ ↑g ⁻¹' {↑g a}) = 0
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.191544
G : Type ?u.191547
𝕜 : Type ?u.191550
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
h : ∀ (x y : E), x ≠ y → T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0
h_pair : Integrable ↑(pair f g)
a : α
hp : ↑(pair f g) a ∈ SimpleFunc.range (pair f g)
eq : ¬↑f a = ↑g a
h_eq : T (↑(pair f g) ⁻¹' {(↑f a, ↑g a)}) = T (↑f ⁻¹' {↑f a} ∩ ↑g ⁻¹' {↑g a})
⊢ T (↑(pair f g) ⁻¹' {(↑f a, ↑g a)}) = 0
rw [h_eq]
no goals
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.191544
G : Type ?u.191547
𝕜 : Type ?u.191550
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
h : ∀ (x y : E), x ≠ y → T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0
h_pair : Integrable ↑(pair f g)
a : α
hp : ↑(pair f g) a ∈ SimpleFunc.range (pair f g)
eq : ¬↑f a = ↑g a
h_eq : T (↑(pair f g) ⁻¹' {(↑f a, ↑g a)}) = T (↑f ⁻¹' {↑f a} ∩ ↑g ⁻¹' {↑g a})
⊢ T (↑f ⁻¹' {↑f a} ∩ ↑g ⁻¹' {↑g a}) = 0
exact h (f a) (g a) eq
case e_a
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.191544
G : Type ?u.191547
𝕜 : Type ?u.191550
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
h : ∀ (x y : E), x ≠ y → T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0
h_pair : Integrable ↑(pair f g)
a : α
hp : ↑(pair f g) a ∈ SimpleFunc.range (pair f g)
eq : ¬↑f a = ↑g a
⊢ ↑(pair f g) ⁻¹' {(↑f a, ↑g a)} = ↑f ⁻¹' {↑f a} ∩ ↑g ⁻¹' {↑g a}
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.191544
G : Type ?u.191547
𝕜 : Type ?u.191550
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
h : ∀ (x y : E), x ≠ y → T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0
h_pair : Integrable ↑(pair f g)
a : α
hp : ↑(pair f g) a ∈ SimpleFunc.range (pair f g)
eq : ¬↑f a = ↑g a
⊢ T (↑(pair f g) ⁻¹' {(↑f a, ↑g a)}) = T (↑f ⁻¹' {↑f a} ∩ ↑g ⁻¹' {↑g a})
congr
no goals
case e_a
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.191544
G : Type ?u.191547
𝕜 : Type ?u.191550
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
h : ∀ (x y : E), x ≠ y → T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0
h_pair : Integrable ↑(pair f g)
a : α
hp : ↑(pair f g) a ∈ SimpleFunc.range (pair f g)
eq : ¬↑f a = ↑g a
⊢ ↑(pair f g) ⁻¹' {(↑f a, ↑g a)} = ↑f ⁻¹' {↑f a} ∩ ↑g ⁻¹' {↑g a}
rw [pair_preimage_singleton f g]