awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β
g : β → γ
hf' : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
hg : Injective g
hg' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (g '' s)
μ : Measure γ
hf : ¬Injective f
neg :
  Eq (α := Measure α)
    (if hf : Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) (comap g μ) then
      OuterMeasure.toMeasure
        ((OuterMeasure.comap f : (a : OuterMeasure β) → OuterMeasure α) (toOuterMeasure (comap g μ))) ⋯
    else 0)
    (comap (g ∘ f) μ)
⊢ Eq (α := Measure α) (comap f (comap g μ)) (comap (g ∘ f) μ)
have neg₁ : Eq (α := Measure α) 0 (comap (g ∘ f) μ)
Tactic: rw [comap, dif_neg <| mt And.left hf, comap, dif_neg fun h ↦ hf h.1.of_comp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β
g : β → γ
hf' : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
hg : Injective g
hg' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (g '' s)
μ : Measure γ
hf : ¬Injective f
neg :
  Eq (α := Measure α)
    (if hf : Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) (comap g μ) then
      OuterMeasure.toMeasure
        ((OuterMeasure.comap f : (a : OuterMeasure β) → OuterMeasure α) (toOuterMeasure (comap g μ))) ⋯
    else 0)
    (comap (g ∘ f) μ)
neg₁ : Eq (α := Measure α) 0 (comap (g ∘ f) μ)
⊢ Eq (α := Measure α) (comap f (comap g μ)) (comap (g ∘ f) μ)
have neg₂ : Eq.{u_1 + 1} (α := Measure α) 0
  (if hf : Injective (g ∘ f) ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (g ∘ f '' s) μ then
    OuterMeasure.toMeasure ((OuterMeasure.comap (g ∘ f) : (a : OuterMeasure γ) → OuterMeasure α) μ.toOuterMeasure) sorry
  else 0)
Tactic: rw [comap, dif_neg <| mt And.left hf, comap, dif_neg fun h ↦ hf h.1.of_comp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β
g : β → γ
hf' : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
hg : Injective g
hg' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (g '' s)
μ : Measure γ
hf : ¬Injective f
neg :
  Eq (α := Measure α)
    (if hf : Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) (comap g μ) then
      OuterMeasure.toMeasure
        ((OuterMeasure.comap f : (a : OuterMeasure β) → OuterMeasure α) (toOuterMeasure (comap g μ))) ⋯
    else 0)
    (comap (g ∘ f) μ)
neg₁ : Eq (α := Measure α) 0 (comap (g ∘ f) μ)
neg₂ :
  Eq.{u_1 + 1} (α := Measure α) 0
    (if hf : Injective (g ∘ f) ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (g ∘ f '' s) μ then
      OuterMeasure.toMeasure ((OuterMeasure.comap (g ∘ f) : (a : OuterMeasure γ) → OuterMeasure α) μ.toOuterMeasure) ⋯
    else 0)
⊢ Eq (α := Measure α) (comap f (comap g μ)) (comap (g ∘ f) μ)
have neg₃ : Eq.{u_1 + 1} (α := Measure α) 0 0
Tactic: rw [comap, dif_neg <| mt And.left hf, comap, dif_neg fun h ↦ hf h.1.of_comp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
c : ℝ≥0∞
⊢ comap f (c • μ) = HSMul.hSMul (β := Measure α) c (comap f μ)
have inl : comap f (HSMul.hSMul (α := ℝ≥0∞) 0 μ) = HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) 0 (comap f μ)
Tactic: obtain rfl | hc := eq_or_ne c 0
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
c : ℝ≥0∞
inl : comap f (HSMul.hSMul (α := ℝ≥0∞) 0 μ) = HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) 0 (comap f μ)
⊢ comap f (c • μ) = HSMul.hSMul (β := Measure α) c (comap f μ)
have inr : ∀ (hc : c ≠ 0), comap f (c • μ) = HSMul.hSMul (β := Measure α) c (comap f μ)
Tactic: obtain rfl | hc := eq_or_ne c 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
c : ℝ≥0∞
hc : c ≠ 0
⊢ comap f (c • μ) = HSMul.hSMul (β := Measure α) c (comap f μ)
have pos : ∀ (h : Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ),
  comap f (c • μ) = HSMul.hSMul (β := Measure α) c (comap f μ)
Tactic: by_cases h : Function.Injective f ∧ ∀ s : Set α, MeasurableSet s → NullMeasurableSet (f '' s) μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
c : ℝ≥0∞
hc : c ≠ 0
pos :
  ∀ (h : Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ),
    comap f (c • μ) = HSMul.hSMul (β := Measure α) c (comap f μ)
⊢ comap f (c • μ) = HSMul.hSMul (β := Measure α) c (comap f μ)
have neg : ∀ (h : ¬(Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ)),
  comap f (c • μ) = HSMul.hSMul (β := Measure α) c (comap f μ)
Tactic: by_cases h : Function.Injective f ∧ ∀ s : Set α, MeasurableSet s → NullMeasurableSet (f '' s) μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
c : ℝ≥0∞
hc : c ≠ 0
h : Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
⊢ comap f (c • μ) = HSMul.hSMul (β := Measure α) c (comap f μ)
have pos : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((comap f (c • μ) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (β := Measure α) c (comap f μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
c : ℝ≥0∞
hc : c ≠ 0
h : Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((comap f (c • μ) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (β := Measure α) c (comap f μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) (c • μ)
Tactic: rw [comap_apply₀ f _ h.1 _ hs.nullMeasurableSet, smul_apply, smul_apply,
      comap_apply₀ f μ h.1 h.2 hs.nullMeasurableSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
c : ℝ≥0∞
hc : c ≠ 0
h : ¬(Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ)
⊢ comap f (c • μ) = HSMul.hSMul (β := Measure α) c (comap f μ)
have h' : ¬(Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) (c • μ))
Tactic: have h' : ¬ (Function.Injective f ∧
        ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) (c • μ)) := by
      simpa [nullMeasurableSet_smul_measure_iff hc] using h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
ma : MeasurableSpace α
mb : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure β
⊢ Measure.comap f (μ + ν) = HAdd.hAdd (α := Measure α) (Measure.comap f μ) (Measure.comap f ν)
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((Measure.comap f (μ + ν) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((HAdd.hAdd (α := Measure α) (Measure.comap f μ) (Measure.comap f ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
ma : MeasurableSpace α
mb : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
⊢ Eq.{u_2 + 1} (α := Measure β) (Measure.comap (⇑e.symm : (a : β) → α) μ) (Measure.map (⇑e : (a : α) → β) μ)
have h : ∀ (s : Set β) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((Measure.comap (⇑e.symm : (a : β) → α) μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.map (⇑e : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
ma : MeasurableSpace α
mb : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((Measure.comap (⇑e.symm : (a : β) → α) μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.map (⇑e : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have rw : ∀ (s : Set β), MeasurableSet s → MeasurableSet.{u_1} (α := α) ((⇑e.symm : (a : β) → α) '' s)
Tactic: rw [e.map_apply, Measure.comap_apply _ e.symm.injective _ _ hs, image_symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
ma : MeasurableSpace α
mb : MeasurableSpace β
μ : Measure α
e : β ≃ᵐ α
⊢ Eq.{u_2 + 1} (α := Measure β) (Measure.map (⇑e.symm : (a : α) → β) μ) (Measure.comap (⇑e : (a : β) → α) μ)
have rw : Eq.{u_2 + 1} (α := Measure β) (Measure.comap (⇑e.symm.symm : (a : β) → α) μ) (Measure.comap (⇑e : (a : β) → α) μ)
Tactic: rw [← comap_symm, symm_symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
ma : MeasurableSpace α
mb : MeasurableSpace β
μ : Measure α
e : β ≃ᵐ α
rw : Eq.{u_2 + 1} (α := Measure β) (Measure.comap (⇑e.symm.symm : (a : β) → α) μ) (Measure.comap (⇑e : (a : β) → α) μ)
⊢ Eq.{u_2 + 1} (α := Measure β) (Measure.map (⇑e.symm : (a : α) → β) μ) (Measure.comap (⇑e : (a : β) → α) μ)
have rw₁ : Eq.{u_2 + 1} (α := Measure β) (Measure.comap (⇑e : (a : β) → α) μ) (Measure.comap (⇑e : (a : β) → α) μ)
Tactic: rw [← comap_symm, symm_symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Complex (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
⊢ { re := (↑s : Set α → ℝ) ∅, im := (↑t : Set α → ℝ) ∅ : ℂ } = 0
have rw : { re := 0, im := 0 : ℂ } = 0
Tactic: rw [s.empty, t.empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Complex (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
i : Set α
hi : ¬MeasurableSet i
⊢ { re := (↑s : Set α → ℝ) i, im := (↑t : Set α → ℝ) i : ℂ } = 0
have rw : { re := 0, im := 0 : ℂ } = 0
Tactic: rw [s.not_measurable hi, t.not_measurable hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Complex (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
R : Type u_2
inst : Semiring R
inst_1 : Module R ℝ
inst_2 : ContinuousConstSMul R ℝ
inst_3 : ContinuousConstSMul R ℂ
r : R
c : ComplexMeasure α
⊢ Equiv.toFun equivSignedMeasure (r • c) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (Equiv.toFun equivSignedMeasure c)
have dsimp : (mapRange (r • c) Complex.reLm.toAddMonoidHom Complex.continuous_re,
    mapRange (r • c) Complex.imLm.toAddMonoidHom Complex.continuous_im) =
  (r • mapRange c Complex.reLm.toAddMonoidHom Complex.continuous_re,
    r • mapRange c Complex.imLm.toAddMonoidHom Complex.continuous_im)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Complex (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
R : Type u_2
inst : Semiring R
inst_1 : Module R ℝ
inst_2 : ContinuousConstSMul R ℝ
inst_3 : ContinuousConstSMul R ℂ
r : R
c : ComplexMeasure α
⊢ (mapRange (r • c) Complex.reLm.toAddMonoidHom Complex.continuous_re,
      mapRange (r • c) Complex.imLm.toAddMonoidHom Complex.continuous_im) =
    (r • mapRange c Complex.reLm.toAddMonoidHom Complex.continuous_re,
      r • mapRange c Complex.imLm.toAddMonoidHom Complex.continuous_im)
have fst : ∀ (i : Set α),
  MeasurableSet i →
    (↑(mapRange (r • c) Complex.reLm.toAddMonoidHom Complex.continuous_re,
                mapRange (r • c) Complex.imLm.toAddMonoidHom Complex.continuous_im).1 :
          Set α → ℝ)
        i =
      (↑(r • mapRange c Complex.reLm.toAddMonoidHom Complex.continuous_re,
                r • mapRange c Complex.imLm.toAddMonoidHom Complex.continuous_im).1 :
          Set α → ℝ)
        i
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Complex (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
R : Type u_2
inst : Semiring R
inst_1 : Module R ℝ
inst_2 : ContinuousConstSMul R ℝ
inst_3 : ContinuousConstSMul R ℂ
r : R
c : ComplexMeasure α
fst :
  ∀ (i : Set α),
    MeasurableSet i →
      (↑(mapRange (r • c) Complex.reLm.toAddMonoidHom Complex.continuous_re,
                  mapRange (r • c) Complex.imLm.toAddMonoidHom Complex.continuous_im).1 :
            Set α → ℝ)
          i =
        (↑(r • mapRange c Complex.reLm.toAddMonoidHom Complex.continuous_re,
                  r • mapRange c Complex.imLm.toAddMonoidHom Complex.continuous_im).1 :
            Set α → ℝ)
          i
⊢ (mapRange (r • c) Complex.reLm.toAddMonoidHom Complex.continuous_re,
      mapRange (r • c) Complex.imLm.toAddMonoidHom Complex.continuous_im) =
    (r • mapRange c Complex.reLm.toAddMonoidHom Complex.continuous_re,
      r • mapRange c Complex.imLm.toAddMonoidHom Complex.continuous_im)
have snd : ∀ (i : Set α),
  MeasurableSet i →
    (↑(mapRange (r • c) Complex.reLm.toAddMonoidHom Complex.continuous_re,
                mapRange (r • c) Complex.imLm.toAddMonoidHom Complex.continuous_im).2 :
          Set α → ℝ)
        i =
      (↑(r • mapRange c Complex.reLm.toAddMonoidHom Complex.continuous_re,
                r • mapRange c Complex.imLm.toAddMonoidHom Complex.continuous_im).2 :
          Set α → ℝ)
        i
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Complex (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
⊢ c ≪ᵥ μ ↔
    AbsolutelyContinuous (M := ℝ) ((re : (a : ComplexMeasure α) → SignedMeasure α) c) μ ∧
      AbsolutelyContinuous (M := ℝ) ((im : (a : ComplexMeasure α) → SignedMeasure α) c) μ
have mp : c ≪ᵥ μ →
  AbsolutelyContinuous (M := ℝ) ((re : (a : ComplexMeasure α) → SignedMeasure α) c) μ ∧
    AbsolutelyContinuous (M := ℝ) ((im : (a : ComplexMeasure α) → SignedMeasure α) c) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Complex (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
mp :
  c ≪ᵥ μ →
    AbsolutelyContinuous (M := ℝ) ((re : (a : ComplexMeasure α) → SignedMeasure α) c) μ ∧
      AbsolutelyContinuous (M := ℝ) ((im : (a : ComplexMeasure α) → SignedMeasure α) c) μ
⊢ c ≪ᵥ μ ↔
    AbsolutelyContinuous (M := ℝ) ((re : (a : ComplexMeasure α) → SignedMeasure α) c) μ ∧
      AbsolutelyContinuous (M := ℝ) ((im : (a : ComplexMeasure α) → SignedMeasure α) c) μ
have mpr : AbsolutelyContinuous (M := ℝ) ((re : (a : ComplexMeasure α) → SignedMeasure α) c) μ ∧
    AbsolutelyContinuous (M := ℝ) ((im : (a : ComplexMeasure α) → SignedMeasure α) c) μ →
  c ≪ᵥ μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Complex (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
⊢ AbsolutelyContinuous (M := ℝ) ((re : (a : ComplexMeasure α) → SignedMeasure α) c) μ ∧
    AbsolutelyContinuous (M := ℝ) ((im : (a : ComplexMeasure α) → SignedMeasure α) c) μ
have mp : AbsolutelyContinuous (M := ℝ) ((re : (a : ComplexMeasure α) → SignedMeasure α) c) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Complex (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
mp : AbsolutelyContinuous (M := ℝ) ((re : (a : ComplexMeasure α) → SignedMeasure α) c) μ
⊢ AbsolutelyContinuous (M := ℝ) ((re : (a : ComplexMeasure α) → SignedMeasure α) c) μ ∧
    AbsolutelyContinuous (M := ℝ) ((im : (a : ComplexMeasure α) → SignedMeasure α) c) μ
have mp₁ : AbsolutelyContinuous (M := ℝ) ((im : (a : ComplexMeasure α) → SignedMeasure α) c) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Complex (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h :
  AbsolutelyContinuous (M := ℝ) ((re : (a : ComplexMeasure α) → SignedMeasure α) c) μ ∧
    AbsolutelyContinuous (M := ℝ) ((im : (a : ComplexMeasure α) → SignedMeasure α) c) μ
i : Set α
hi : (↑μ : Set α → ℝ≥0∞) i = 0
⊢ (↑c : Set α → ℂ) i = 0
have mpr : (↑0 : ℂ) + (↑0 : ℂ) * Complex.I = 0
Tactic: rw [← Complex.re_add_im (c i), (_ : (c i).re = 0), (_ : (c i).im = 0)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Complex (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h :
  AbsolutelyContinuous (M := ℝ) ((re : (a : ComplexMeasure α) → SignedMeasure α) c) μ ∧
    AbsolutelyContinuous (M := ℝ) ((im : (a : ComplexMeasure α) → SignedMeasure α) c) μ
i : Set α
hi : (↑μ : Set α → ℝ≥0∞) i = 0
mpr : (↑0 : ℂ) + (↑0 : ℂ) * Complex.I = 0
⊢ (↑c : Set α → ℂ) i = 0
have rw : ((↑c : Set α → ℂ) i).im = 0
Tactic: rw [← Complex.re_add_im (c i), (_ : (c i).re = 0), (_ : (c i).im = 0)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Complex (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h :
  AbsolutelyContinuous (M := ℝ) ((re : (a : ComplexMeasure α) → SignedMeasure α) c) μ ∧
    AbsolutelyContinuous (M := ℝ) ((im : (a : ComplexMeasure α) → SignedMeasure α) c) μ
i : Set α
hi : (↑μ : Set α → ℝ≥0∞) i = 0
mpr : (↑0 : ℂ) + (↑0 : ℂ) * Complex.I = 0
rw : ((↑c : Set α → ℂ) i).im = 0
⊢ (↑c : Set α → ℂ) i = 0
have rw₁ : ((↑c : Set α → ℂ) i).re = 0
Tactic: rw [← Complex.re_add_im (c i), (_ : (c i).re = 0), (_ : (c i).im = 0)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Content (goal)
Goal:
G : Type w
inst : TopologicalSpace G
μ : Compacts G → ℝ≥0
mono' : ∀ (K₁ K₂ : Compacts G), (↑K₁ : Set G) ⊆ (↑K₂ : Set G) → μ K₁ ≤ μ K₂
sup_disjoint' :
  ∀ (K₁ K₂ : Compacts G),
    Disjoint (↑K₁ : Set G) (↑K₂ : Set G) → IsClosed (↑K₁ : Set G) → IsClosed (↑K₂ : Set G) → μ (K₁ ⊔ K₂) = μ K₁ + μ K₂
sup_le' : ∀ (K₁ K₂ : Compacts G), μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂
v : Compacts G → ℝ≥0
mono'_1 : ∀ (K₁ K₂ : Compacts G), (↑K₁ : Set G) ⊆ (↑K₂ : Set G) → v K₁ ≤ v K₂
sup_disjoint'_1 :
  ∀ (K₁ K₂ : Compacts G),
    Disjoint (↑K₁ : Set G) (↑K₂ : Set G) → IsClosed (↑K₁ : Set G) → IsClosed (↑K₂ : Set G) → v (K₁ ⊔ K₂) = v K₁ + v K₂
sup_le'_1 : ∀ (K₁ K₂ : Compacts G), v (K₁ ⊔ K₂) ≤ v K₁ + v K₂
h :
  Eq.{max (w + 1) 1} (α := (a : Compacts G) → ℝ≥0∞)
    ((fun (μ : Content G) (s : Compacts G) ↦ (↑(μ.toFun s) : ℝ≥0∞))
      { toFun := μ, mono' := mono', sup_disjoint' := sup_disjoint', sup_le' := sup_le' })
    ((fun (μ : Content G) (s : Compacts G) ↦ (↑(μ.toFun s) : ℝ≥0∞))
      { toFun := v, mono' := mono'_1, sup_disjoint' := sup_disjoint'_1, sup_le' := sup_le'_1 })
⊢ { toFun := μ, mono' := mono', sup_disjoint' := sup_disjoint', sup_le' := sup_le' : Content G } =
    { toFun := v, mono' := mono'_1, sup_disjoint' := sup_disjoint'_1, sup_le' := sup_le'_1 }
have h₁ : μ = v
Tactic: congr!
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Content (goal)
Goal:
G : Type w
inst : TopologicalSpace G
μ : Compacts G → ℝ≥0
mono' : ∀ (K₁ K₂ : Compacts G), (↑K₁ : Set G) ⊆ (↑K₂ : Set G) → μ K₁ ≤ μ K₂
sup_disjoint' :
  ∀ (K₁ K₂ : Compacts G),
    Disjoint (↑K₁ : Set G) (↑K₂ : Set G) → IsClosed (↑K₁ : Set G) → IsClosed (↑K₂ : Set G) → μ (K₁ ⊔ K₂) = μ K₁ + μ K₂
sup_le' : ∀ (K₁ K₂ : Compacts G), μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂
v : Compacts G → ℝ≥0
mono'_1 : ∀ (K₁ K₂ : Compacts G), (↑K₁ : Set G) ⊆ (↑K₂ : Set G) → v K₁ ≤ v K₂
sup_disjoint'_1 :
  ∀ (K₁ K₂ : Compacts G),
    Disjoint (↑K₁ : Set G) (↑K₂ : Set G) → IsClosed (↑K₁ : Set G) → IsClosed (↑K₂ : Set G) → v (K₁ ⊔ K₂) = v K₁ + v K₂
sup_le'_1 : ∀ (K₁ K₂ : Compacts G), v (K₁ ⊔ K₂) ≤ v K₁ + v K₂
h :
  Eq.{max (w + 1) 1} (α := (a : Compacts G) → ℝ≥0∞)
    ((fun (μ : Content G) (s : Compacts G) ↦ (↑(μ.toFun s) : ℝ≥0∞))
      { toFun := μ, mono' := mono', sup_disjoint' := sup_disjoint', sup_le' := sup_le' })
    ((fun (μ : Content G) (s : Compacts G) ↦ (↑(μ.toFun s) : ℝ≥0∞))
      { toFun := v, mono' := mono'_1, sup_disjoint' := sup_disjoint'_1, sup_le' := sup_le'_1 })
⊢ μ = v
have h₁ : ∀ (s : Compacts G), μ s = v s
Tactic: ext s : 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Content (goal)
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
⊢ μ.innerContent ⊥ = 0
have rw : μ.innerContent ⊥ ≤ (μ : (a : Compacts G) → ℝ≥0∞) ⊥
Tactic: rw [← nonpos_iff_eq_zero, ← μ.empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Content (goal)
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
⊢ μ.innerContent ⊥ ≤ (μ : (a : Compacts G) → ℝ≥0∞) ⊥
have refine : ∀ (K : Compacts G) (hK : (↑K : Set G) ⊆ (↑⊥ : Set G)),
  LE.le (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) ⊥ : ℝ≥0∞)
Tactic: refine iSup₂_le fun K hK => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Content (goal)
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
K : Compacts G
hK : (↑K : Set G) ⊆ (↑⊥ : Set G)
⊢ K = ⊥
have h : (↑K : Set G) = (↑⊥ : Set G)
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Content (goal)
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
K : Compacts G
hK : (↑K : Set G) ⊆ (↑⊥ : Set G)
⊢ (↑K : Set G) = (↑⊥ : Set G)
have h : ∅ = (↑⊥ : Set G)
Tactic: rw [subset_empty_iff.mp hK, Compacts.coe_bot]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Content (goal)
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
K : Compacts G
hK : (↑K : Set G) ⊆ (↑⊥ : Set G)
h : ∅ = (↑⊥ : Set G)
⊢ (↑K : Set G) = (↑⊥ : Set G)
have h₁ : Eq.{w + 1} (α := Set G) ∅ ∅
Tactic: rw [subset_empty_iff.mp hK, Compacts.coe_bot]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Content (hypothesis)
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
K : Compacts G
hK : (↑K : Set G) ⊆ (↑⊥ : Set G)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) ⊥ : ℝ≥0∞)
have this : K = ⊥
Tactic: have : K = ⊥ := by
    ext1
    rw [subset_empty_iff.mp hK, Compacts.coe_bot]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Content (goal)
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
K : Compacts G
hK : (↑K : Set G) ⊆ (↑⊥ : Set G)
this : K = ⊥
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) ⊥ : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) ⊥ : ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) ⊥ : ℝ≥0∞)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Content (hypothesis)
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
U : Opens G
hU : μ.innerContent U ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
⊢ ∃ (K : Compacts G),
    (↑K : Set G) ⊆ (↑U : Set G) ∧
      μ.innerContent U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
have h'ε : (↑ε : ℝ≥0∞) ≠ 0
Tactic: have h'ε := ENNReal.coe_ne_zero.2 hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Content (goal)
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
U : Opens G
hU : μ.innerContent U ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
h'ε : (↑ε : ℝ≥0∞) ≠ 0
⊢ ∃ (K : Compacts G),
    (↑K : Set G) ⊆ (↑U : Set G) ∧
      μ.innerContent U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
have inl : ∀ (h : μ.innerContent U ≤ (↑ε : ℝ≥0∞)),
  ∃ (K : Compacts G),
    (↑K : Set G) ⊆ (↑U : Set G) ∧
      μ.innerContent U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
Tactic: rcases le_or_gt (μ.innerContent U) ε with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Content (goal)
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
U : Opens G
hU : μ.innerContent U ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
h'ε : (↑ε : ℝ≥0∞) ≠ 0
inl :
  ∀ (h : μ.innerContent U ≤ (↑ε : ℝ≥0∞)),
    ∃ (K : Compacts G),
      (↑K : Set G) ⊆ (↑U : Set G) ∧
        μ.innerContent U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
⊢ ∃ (K : Compacts G),
    (↑K : Set G) ⊆ (↑U : Set G) ∧
      μ.innerContent U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
have inr : ∀ (h : (↑ε : ℝ≥0∞) < μ.innerContent U),
  ∃ (K : Compacts G),
    (↑K : Set G) ⊆ (↑U : Set G) ∧
      μ.innerContent U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
Tactic: rcases le_or_gt (μ.innerContent U) ε with h | h