case mp
α : Type u_1
β : Type ?u.103329
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
⊢ ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ

case mpr
α : Type u_1
β : Type ?u.103329
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ
⊢ c ≪ᵥ μ
α : Type u_1
β : Type ?u.103329
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
⊢ c ≪ᵥ μ ↔ ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ
constructor <;> intro h
case mp.right
α : Type u_1
β : Type ?u.103329
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ ↑(↑im c) i = 0
case mp.right
α : Type u_1
β : Type ?u.103329
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
⊢ ↑im c ≪ᵥ μ
intro i hi
no goals
case mp.right
α : Type u_1
β : Type ?u.103329
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ ↑(↑im c) i = 0
simp [h hi]
case mpr
α : Type u_1
β : Type ?u.103329
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ ↑c i = 0
case mpr
α : Type u_1
β : Type ?u.103329
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ
⊢ c ≪ᵥ μ
intro i hi
case mpr
α : Type u_1
β : Type ?u.103329
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ ↑0 + ↑0 * Complex.I = 0

α : Type u_1
β : Type ?u.103329
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ (↑c i).im = 0

α : Type u_1
β : Type ?u.103329
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ (↑c i).re = 0
case mpr
α : Type u_1
β : Type ?u.103329
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ ↑c i = 0
rw [← Complex.re_add_im (c i), (_ : (c i).re = 0), (_ : (c i).im = 0)]
no goals
case mpr
α : Type u_1
β : Type ?u.103329
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ ↑0 + ↑0 * Complex.I = 0

α : Type u_1
β : Type ?u.103329
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ (↑c i).im = 0

α : Type u_1
β : Type ?u.103329
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ (↑c i).re = 0
exacts [by simp, h.2 hi, h.1 hi]
no goals
α : Type u_1
β : Type ?u.103329
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ ↑0 + ↑0 * Complex.I = 0
simp