awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
s : Set α
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
hs : NullMeasurableSet s (comap f μ)
⊢ NullMeasurableSet (f '' toMeasurable (comap f μ) s) μ

Tactic:
hf _ (measurableSet_toMeasurable _ _)

Premises used: MeasureTheory.measurableSet_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
s : Set α
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
hs : NullMeasurableSet s (comap f μ)
⊢ NullMeasurableSet (f '' toMeasurable (comap f μ) s) μ

Tactic:
exact hf _ (measurableSet_toMeasurable _ _)

Premises used: MeasureTheory.measurableSet_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
s : Set α
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
hs : NullMeasurableSet s (comap f μ)
⊢ toMeasurable (comap f μ) s =ᶠ[ae (F := Measure α) (comap f μ)] s

Tactic:
have h : toMeasurable (comap f μ) s =ᵐ[comap f μ] s :=
    NullMeasurableSet.toMeasurable_ae_eq hs
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
s : Set α
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
hs : NullMeasurableSet s (comap f μ)
h : toMeasurable (comap f μ) s =ᶠ[ae (F := Measure α) (comap f μ)] s
⊢ f '' s =ᶠ[ae μ] f '' toMeasurable (comap f μ) s

Tactic:
ae_eq_image_of_ae_eq_comap f μ hfi hf h.symm

Premises used: MeasureTheory.Measure.ae_eq_image_of_ae_eq_comap, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
s : Set α
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
hs : NullMeasurableSet s (comap f μ)
h : toMeasurable (comap f μ) s =ᶠ[ae (F := Measure α) (comap f μ)] s
⊢ f '' s =ᶠ[ae μ] f '' toMeasurable (comap f μ) s

Tactic:
exact ae_eq_image_of_ae_eq_comap f μ hfi hf h.symm

Premises used: MeasureTheory.Measure.ae_eq_image_of_ae_eq_comap, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hf : Injective f
hf' : Measurable f
h : ∀ (t : Set α), MeasurableSet t → NullMeasurableSet (f '' t) μ
s : Set β
hs : MeasurableSet s
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    ((μ : (a : Set β) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)

Tactic:
rw [comap_apply₀ _ _ hf h (hf' hs).nullMeasurableSet, image_preimage_eq_inter_range]

Premises used: MeasurableSet.nullMeasurableSet, Set.image_preimage_eq_inter_range, MeasureTheory.Measure.comap_apply₀
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
pos :
  ∀ (hf : Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) 0),
    Eq (α := Measure α) (comap f 0) 0
neg :
  ∀ (hf : ¬(Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) 0)),
    Eq (α := Measure α) (comap f 0) 0
⊢ Eq (α := Measure α) (comap f 0) 0

Tactic:
by_cases hf : Injective f ∧ ∀ s, MeasurableSet s → NullMeasurableSet (f '' s) (0 : Measure β)

Premises used: Function.Injective
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) 0
⊢ Eq (α := Measure α) (comap f 0) 0

Tactic:
simp [comap, hf]

Premises used: MeasureTheory.Measure.comap
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : ¬(Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) 0)
⊢ Eq (α := Measure α) (comap f 0) 0

Tactic:
simp [comap, hf]

Premises used: MeasureTheory.Measure.comap
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
h :
  ∀ (s : Set β) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((comap (fun (x : β) ↦ x) μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((μ : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ comap (fun (x : β) ↦ x) μ = μ

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
h : Injective (β := β) fun (x : β) ↦ x
h₁ : ∀ (s : Set β), MeasurableSet s → MeasurableSet (α := β) ((fun (x : β) ↦ x) '' s)
h₂ : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((comap (fun (x : β) ↦ x) μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [comap_apply, image_id']

Premises used: Set.image_id', MeasureTheory.Measure.comap_apply
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ Injective (β := β) fun (x : β) ↦ x

Tactic:
injective_id

Premises used: Function.injective_id
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ Injective (β := β) fun (x : β) ↦ x

Tactic:
exact injective_id

Premises used: Function.injective_id
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ ∀ (s : Set β), MeasurableSet s → MeasurableSet (α := β) ((fun (x : β) ↦ x) '' s)

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet s

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Measure.Comap
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 γ
pos : ∀ (hf : Injective f), Eq (α := Measure α) (comap f (comap g μ)) (comap (g ∘ f) μ)
neg : ∀ (hf : ¬Injective f), Eq (α := Measure α) (comap f (comap g μ)) (comap (g ∘ f) μ)
⊢ Eq (α := Measure α) (comap f (comap g μ)) (comap (g ∘ f) μ)

Tactic:
by_cases hf : Injective f

Premises used: Function.Injective
-- Module: Mathlib.MeasureTheory.Measure.Comap
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
pos :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((comap f (comap g μ) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((comap (g ∘ f) μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Measure α) (comap f (comap g μ)) (comap (g ∘ f) μ)

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.Comap
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
s : Set α
hs : MeasurableSet s
pos :
  Eq (α := ℝ≥0∞) (((comap g μ : Measure β) : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((comap (g ∘ f) μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
pos₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set γ) → ℝ≥0∞) (g '' f '' s) : ℝ≥0∞)
    (((comap (g ∘ f) μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
pos₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set γ) → ℝ≥0∞) (g '' f '' s) : ℝ≥0∞) ((μ : (a : Set γ) → ℝ≥0∞) (g ∘ f '' s) : ℝ≥0∞)
pos₃ pos₄ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set γ) → ℝ≥0∞) (g '' f '' s) : ℝ≥0∞) ((μ : (a : Set γ) → ℝ≥0∞) (g '' f '' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((comap f (comap g μ) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((comap (g ∘ f) μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [comap_apply _ hf hf' _ hs, comap_apply _ hg hg' _ (hf' _ hs),
      comap_apply _ (hg.comp hf) (fun t ht ↦ image_comp g f _ ▸ hg' _ <| hf' _ ht) _ hs, image_comp]

Premises used: MeasureTheory.Measure.comap_apply, Function.Injective.comp, Set.image_comp
-- Module: Mathlib.MeasureTheory.Measure.Comap
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)
neg₃ neg₄ : Eq.{u_1 + 1} (α := Measure α) 0 0
⊢ Eq (α := Measure α) (comap f (comap g μ)) (comap (g ∘ f) μ)

Tactic:
rw [comap, dif_neg <| mt And.left hf, comap, dif_neg fun h ↦ hf h.1.of_comp]

Premises used: mt, dif_neg, And.left, MeasureTheory.Measure.comap
-- Module: Mathlib.MeasureTheory.Measure.Comap
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 μ)
inr : ∀ (hc : c ≠ 0), comap f (c • μ) = HSMul.hSMul (β := Measure α) c (comap f μ)
⊢ comap f (c • μ) = HSMul.hSMul (β := Measure α) c (comap f μ)

Tactic:
obtain rfl | hc := eq_or_ne c 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
⊢ comap f (HSMul.hSMul (α := ℝ≥0∞) 0 μ) = HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) 0 (comap f μ)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Comap
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 μ)
neg :
  ∀ (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 μ)

Tactic:
by_cases h : Function.Injective f ∧ ∀ s : Set α, MeasurableSet s → NullMeasurableSet (f '' s) μ

Premises used: Function.Injective
-- Module: Mathlib.MeasureTheory.Measure.Comap
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) μ
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∞)
⊢ comap f (c • μ) = HSMul.hSMul (β := Measure α) c (comap f μ)

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.Comap
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
rw : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) (c • μ)
⊢ Eq (α := ℝ≥0∞) (((comap f (c • μ) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (β := Measure α) c (comap f μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [comap_apply₀ f _ h.1 _ hs.nullMeasurableSet, smul_apply, smul_apply,
      comap_apply₀ f μ h.1 h.2 hs.nullMeasurableSet]

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.Measure.comap_apply₀, And.right, And.left, MeasureTheory.Measure.smul_apply
-- Module: Mathlib.MeasureTheory.Measure.Comap
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
⊢ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) (c • μ)

Tactic:
simpa [nullMeasurableSet_smul_measure_iff hc] using h.2

Premises used: MeasureTheory.nullMeasurableSet_smul_measure_iff, And.right
-- Module: Mathlib.MeasureTheory.Measure.Comap
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) μ)
⊢ ¬(Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) (c • μ))

Tactic:
simpa [nullMeasurableSet_smul_measure_iff hc] using h

Premises used: MeasureTheory.nullMeasurableSet_smul_measure_iff
-- Module: Mathlib.MeasureTheory.Measure.Comap
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) μ)
⊢ ¬(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
-- Module: Mathlib.MeasureTheory.Measure.Comap
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) μ)
h' : ¬(Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) (c • μ))
⊢ comap f (c • μ) = HSMul.hSMul (β := Measure α) c (comap f μ)

Tactic:
simp [comap_undef, h, h']

Premises used: MeasureTheory.Measure.comap_undef
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
ma : MeasurableSpace α
mb : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure β
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∞)
⊢ Measure.comap f (μ + ν) = HAdd.hAdd (α := Measure α) (Measure.comap f μ) (Measure.comap f ν)

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
ma : MeasurableSpace α
mb : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure β
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:
simp only [← comapₗ_eq_comap _ hf.injective (fun _ ↦ hf.measurableSet_image.mpr) _ hs,
    map_add, add_apply]

Premises used: Iff.mpr, MeasurableEmbedding.measurableSet_image, MeasureTheory.Measure.comapₗ_eq_comap, map_add, MeasureTheory.Measure.add_apply, MeasurableEmbedding.injective
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
ma : MeasurableSpace α
mb : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
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∞)
⊢ Eq.{u_2 + 1} (α := Measure β) (Measure.comap (⇑e.symm : (a : β) → α) μ) (Measure.map (⇑e : (a : α) → β) μ)

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
ma : MeasurableSpace α
mb : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
s : Set β
hs : MeasurableSet s
rw : ∀ (s : Set β), MeasurableSet s → MeasurableSet.{u_1} (α := α) ((⇑e.symm : (a : β) → α) '' 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:
rw [e.map_apply, Measure.comap_apply _ e.symm.injective _ _ hs, image_symm]

Premises used: MeasurableEquiv.injective, MeasurableEquiv.map_apply, MeasurableEquiv.symm, MeasureTheory.Measure.comap_apply, MeasurableEquiv.image_symm
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
ma : MeasurableSpace α
mb : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
s : Set β
hs : MeasurableSet s
⊢ ∀ (s : Set β), MeasurableSet s → MeasurableSet.{u_1} (α := α) ((⇑e.symm : (a : β) → α) '' s)

Tactic:
fun t ht ↦ e.symm.measurableSet_image.mpr ht

Premises used: Iff.mpr, MeasurableEquiv.measurableSet_image, MeasurableEquiv.symm
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
ma : MeasurableSpace α
mb : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
s : Set β
hs : MeasurableSet s
⊢ ∀ (s : Set β), MeasurableSet s → MeasurableSet.{u_1} (α := α) ((⇑e.symm : (a : β) → α) '' s)

Tactic:
exact fun t ht ↦ e.symm.measurableSet_image.mpr ht

Premises used: Iff.mpr, MeasurableEquiv.measurableSet_image, MeasurableEquiv.symm
-- Module: Mathlib.MeasureTheory.Measure.Comap
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 : β) → α) μ)
rw₁ rw₂ : Eq.{u_2 + 1} (α := Measure β) (Measure.comap (⇑e : (a : β) → α) μ) (Measure.comap (⇑e : (a : β) → α) μ)
⊢ Eq.{u_2 + 1} (α := Measure β) (Measure.map (⇑e.symm : (a : α) → β) μ) (Measure.comap (⇑e : (a : β) → α) μ)

Tactic:
rw [← comap_symm, symm_symm]

Premises used: MeasurableEquiv.symm_symm, MeasurableEquiv.comap_symm
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
ma : MeasurableSpace α
mb : MeasurableSpace β
μ : Measure (α × β)
⊢ Eq (α := Measure (β × α)) (comap Prod.swap μ) (map Prod.swap μ)

Tactic:
(MeasurableEquiv.prodComm ..).comap_symm

Premises used: MeasurableEquiv.comap_symm, MeasurableEquiv.prodComm, Prod.swap
-- Module: Mathlib.MeasureTheory.Measure.Complex
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
rw : { re := 0, im := 0 : ℂ } = 0
⊢ { re := (↑s : Set α → ℝ) ∅, im := (↑t : Set α → ℝ) ∅ : ℂ } = 0

Tactic:
rw [s.empty, t.empty]

Premises used: MeasureTheory.VectorMeasure.empty
-- Module: Mathlib.MeasureTheory.Measure.Complex
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
⊢ { re := 0, im := 0 : ℂ } = 0

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.Complex
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
i : Set α
hi : ¬MeasurableSet i
rw : { re := 0, im := 0 : ℂ } = 0
⊢ { re := (↑s : Set α → ℝ) i, im := (↑t : Set α → ℝ) i : ℂ } = 0

Tactic:
rw [s.not_measurable hi, t.not_measurable hi]

Premises used: MeasureTheory.VectorMeasure.not_measurable
-- Module: Mathlib.MeasureTheory.Measure.Complex
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
i : Set α
hi : ¬MeasurableSet i
⊢ { re := 0, im := 0 : ℂ } = 0

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.Complex
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
i : Set α
⊢ (↑(s.toComplexMeasure t) : Set α → ℂ) i = { re := (↑s : Set α → ℝ) i, im := (↑t : Set α → ℝ) i }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.Complex
Goal:
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
⊢ SignedMeasure.toComplexMeasure ((re : (a : ComplexMeasure α) → SignedMeasure α) c)
      ((im : (a : ComplexMeasure α) → SignedMeasure α) c) =
    c

Tactic:
rfl

Premises used: MeasureTheory.SignedMeasure.toComplexMeasure, rfl
-- Module: Mathlib.MeasureTheory.Measure.Complex
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
⊢ (re : (a : ComplexMeasure α) → SignedMeasure α) (s.toComplexMeasure t) = s

Tactic:
rfl

Premises used: MeasureTheory.VectorMeasure.mapRange, rfl
-- Module: Mathlib.MeasureTheory.Measure.Complex
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
⊢ (im : (a : ComplexMeasure α) → SignedMeasure α) (s.toComplexMeasure t) = t

Tactic:
rfl

Premises used: MeasureTheory.VectorMeasure.mapRange, rfl
-- Module: Mathlib.MeasureTheory.Measure.Complex
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 ℂ
c d : ComplexMeasure α
⊢ Equiv.toFun equivSignedMeasure (c + d) = Equiv.toFun equivSignedMeasure c + Equiv.toFun equivSignedMeasure d

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.Complex
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 α
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)
⊢ Equiv.toFun equivSignedMeasure (r • c) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (Equiv.toFun equivSignedMeasure c)

Tactic:
dsimp
-- Module: Mathlib.MeasureTheory.Measure.Complex
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
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
⊢ (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:
ext
-- Module: Mathlib.MeasureTheory.Measure.Complex
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 α
i : Set α
h : 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:
simp [Complex.smul_re]

Premises used: Complex.smul_re