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 μ)
rw :
  ∀
    (hs :
      NullMeasurableSet s
        (OuterMeasure.toMeasure ((OuterMeasure.comap f : (a : OuterMeasure β) → OuterMeasure α) μ.toOuterMeasure) ⋯)),
    Eq (α := ℝ≥0∞)
      (((OuterMeasure.toMeasure ((OuterMeasure.comap f : (a : OuterMeasure β) → OuterMeasure α) μ.toOuterMeasure) ⋯ :
              Measure α) :
            (a : Set α) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)

Tactic:
rw [comap, dif_pos (And.intro hfi hf)] at hs ⊢

Premises used: dif_pos, MeasureTheory.Measure.comap, And.intro
-- 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
    (OuterMeasure.toMeasure ((OuterMeasure.comap f : (a : OuterMeasure β) → OuterMeasure α) μ.toOuterMeasure) ⋯)
rw :
  Eq (α := ℝ≥0∞)
    ((((OuterMeasure.comap f : (a : OuterMeasure β) → OuterMeasure α) μ.toOuterMeasure : OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ.toOuterMeasure : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
rw₂ rw₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((OuterMeasure.toMeasure ((OuterMeasure.comap f : (a : OuterMeasure β) → OuterMeasure α) μ.toOuterMeasure) ⋯ :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)

Tactic:
rw [toMeasure_apply₀ _ _ hs, OuterMeasure.comap_apply, coe_toOuterMeasure]

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

Tactic:
dif_neg h

Premises used: dif_neg, MeasureTheory.Measure.comap
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s : Set α
rw :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((OuterMeasure.toMeasure ((OuterMeasure.comap f : (a : OuterMeasure β) → OuterMeasure α) μ.toOuterMeasure) ⋯ :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [comap, dif_pos (And.intro hfi hf)]

Premises used: dif_pos, MeasureTheory.Measure.comap, And.intro
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s : Set α
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((OuterMeasure.toMeasure ((OuterMeasure.comap f : (a : OuterMeasure β) → OuterMeasure α) μ.toOuterMeasure) ⋯ :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
le_toMeasure_apply _ _ _

Premises used: MeasureTheory.le_toMeasure_apply
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s : Set α
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((OuterMeasure.toMeasure ((OuterMeasure.comap f : (a : OuterMeasure β) → OuterMeasure α) μ.toOuterMeasure) ⋯ :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
exact le_toMeasure_apply _ _ _

Premises used: MeasureTheory.le_toMeasure_apply
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
s : Set α
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
μ : Measure β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)

Tactic:
comap_apply₀ f μ hfi (fun s hs => (hf s hs).nullMeasurableSet) hs.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.Measure.comap_apply₀
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
s : Set α
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hs : NullMeasurableSet s (comap f μ)
pos :
  ∀ (hf : Injective f ∧ ∀ (t : Set α), MeasurableSet t → NullMeasurableSet (f '' t) μ),
    LE.le (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
neg :
  ∀ (hf : ¬(Injective f ∧ ∀ (t : Set α), MeasurableSet t → NullMeasurableSet (f '' t) μ)),
    LE.le (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)

Tactic:
by_cases hf : Injective f ∧ ∀ t, MeasurableSet t → NullMeasurableSet (f '' t) μ

Premises used: Function.Injective
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
s : Set α
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hs : NullMeasurableSet s (comap f μ)
hf : Injective f ∧ ∀ (t : Set α), MeasurableSet t → NullMeasurableSet (f '' t) μ
pos pos₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)

Tactic:
rw [comap_apply₀ _ _ hf.1 hf.2 hs]

Premises used: MeasureTheory.Measure.comap_apply₀, And.right, And.left
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
s : Set α
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hs : NullMeasurableSet s (comap f μ)
hf : ¬(Injective f ∧ ∀ (t : Set α), MeasurableSet t → NullMeasurableSet (f '' t) μ)
⊢ LE.le (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)

Tactic:
simp [comap_undef hf]

Premises used: MeasureTheory.Measure.comap_undef
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
s : Set α
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
μ : Measure β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    (((((comapₗ f : LinearMap.{0, 0, u_2, u_1} (RingHom.id ℝ≥0∞) (Measure β) (Measure α)) : (a : Measure β) → Measure α)
              μ :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
(comapₗ_apply f hfi hf μ hs).trans (comap_apply f hfi hf μ hs).symm

Premises used: MeasureTheory.Measure.comapₗ_apply, MeasureTheory.Measure.comap_apply, Eq.symm, Eq.trans
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s : Set α
hs : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← nonpos_iff_eq_zero]

Premises used: nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s : Set α
hs : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
(le_comap_apply f μ hfi hf s).trans hs.le

Premises used: MeasureTheory.Measure.le_comap_apply, Eq.le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s : Set α
hs : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact (le_comap_apply f μ hfi hf s).trans hs.le

Premises used: MeasureTheory.Measure.le_comap_apply, Eq.le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : s =ᶠ[ae (F := Measure α) (comap f μ)] t
rw :
  ∀ (hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) {a : β | ¬(f '' s) a = (f '' t) a} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ f '' s =ᶠ[ae μ] f '' t

Tactic:
rw [EventuallyEq, ae_iff] at hst ⊢

Premises used: Filter.EventuallyEq, MeasureTheory.ae_iff
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
h : ∀ (x : α), Membership.mem (γ := Set α) {a : α | ¬s a = t a} x ↔ x ∈ s \ t ∪ t \ s
⊢ {a : α | ¬s a = t a} = s \ t ∪ t \ s

Tactic:
ext1 x
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
h : ¬(s x ↔ t x) ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
⊢ Membership.mem (γ := Set α) {a : α | ¬s a = t a} x ↔ x ∈ s \ t ∪ t \ s

Tactic:
simp only [eq_iff_iff, mem_setOf_eq, mem_union, mem_diff]

Premises used: Set.mem_union, Set.mem_setOf_eq, Set.mem_diff, eq_iff_iff
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
h : ¬(s x ↔ t x) → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
h₁ : x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s → ¬(s x ↔ t x)
h₂ : ¬s x → t x → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
h₃ : ¬¬s x → ¬t x → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
h₄ : ¬s x → t x → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
h₅ : ¬¬s x → ¬t x → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
h₆ : ¬s x → t x → ¬(x ∈ s ∧ x ∉ t) → x ∈ t
h₇ : ¬s x → t x → ¬(x ∈ s ∧ x ∉ t) → x ∉ s
h₈ : ¬¬s x → ¬t x → ¬(x ∈ s ∧ x ∉ t) → x ∈ t
h₉ : ¬¬s x → ¬t x → ¬(x ∈ s ∧ x ∉ t) → x ∉ s
h₁₀ : x ∈ s → x ∉ t → ¬(s x ↔ t x)
h₁₁ : x ∈ t → x ∉ s → ¬(s x ↔ t x)
h₁₂ : x ∈ s → x ∉ t → ¬(s x ↔ t x)
h₁₃ : x ∈ t → x ∉ s → ¬(s x ↔ t x)
h₁₄ : x ∈ s → x ∉ t → (s x ↔ t x) → False
h₁₅ : x ∈ t → x ∉ s → (s x ↔ t x) → False
h₁₆ : s x → ¬t x → x ∉ s → x ∈ t
h₁₇ : s x → ¬t x → ¬x ∉ t → x ∈ t
h₁₈ : s x → ¬t x → x ∈ s → x ∉ s → False
h₁₉ : s x → ¬t x → x ∈ s → ¬x ∉ t → False
h₂₀ : x ∈ s → x ∉ t → s x → t x → False
h₂₁ : x ∈ s → x ∉ t → ¬s x → ¬t x → False
h₂₂ : x ∈ t → x ∉ s → s x → t x → False
h₂₃ : x ∈ t → x ∉ s → ¬s x → ¬t x → False
⊢ ¬(s x ↔ t x) ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s

Tactic:
tauto
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ {a : α | ¬s a = t a} = s \ t ∪ t \ s

Tactic:
have h_eq_α : { a : α | ¬s a = t a } = s \ t ∪ t \ s := by
    ext1 x
    simp only [eq_iff_iff, mem_setOf_eq, mem_union, mem_diff]
    tauto
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq_α : {a : α | ¬s a = t a} = s \ t ∪ t \ s
h : ∀ (x : β), Membership.mem (γ := Set β) {a : β | ¬(f '' s) a = (f '' t) a} x ↔ x ∈ f '' s \ f '' t ∪ f '' t \ f '' s
⊢ {a : β | ¬(f '' s) a = (f '' t) a} = f '' s \ f '' t ∪ f '' t \ f '' s

Tactic:
ext1 x
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq_α : {a : α | ¬s a = t a} = s \ t ∪ t \ s
x : β
h : ¬((f '' s) x ↔ (f '' t) x) ↔ x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
⊢ Membership.mem (γ := Set β) {a : β | ¬(f '' s) a = (f '' t) a} x ↔ x ∈ f '' s \ f '' t ∪ f '' t \ f '' s

Tactic:
simp only [eq_iff_iff, mem_setOf_eq, mem_union, mem_diff]

Premises used: Set.mem_union, Set.mem_setOf_eq, Set.mem_diff, eq_iff_iff
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq_α : {a : α | ¬s a = t a} = s \ t ∪ t \ s
x : β
h : ¬((f '' s) x ↔ (f '' t) x) → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₁ : x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s → ¬((f '' s) x ↔ (f '' t) x)
h₂ : ¬(f '' s) x → (f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₃ : ¬¬(f '' s) x → ¬(f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₄ : ¬(f '' s) x → (f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₅ : ¬¬(f '' s) x → ¬(f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₆ : ¬(f '' s) x → (f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∈ f '' t
h₇ : ¬(f '' s) x → (f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∉ f '' s
h₈ : ¬¬(f '' s) x → ¬(f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∈ f '' t
h₉ : ¬¬(f '' s) x → ¬(f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∉ f '' s
h₁₀ : x ∈ f '' s → x ∉ f '' t → ¬((f '' s) x ↔ (f '' t) x)
h₁₁ : x ∈ f '' t → x ∉ f '' s → ¬((f '' s) x ↔ (f '' t) x)
h₁₂ : x ∈ f '' s → x ∉ f '' t → ¬((f '' s) x ↔ (f '' t) x)
h₁₃ : x ∈ f '' t → x ∉ f '' s → ¬((f '' s) x ↔ (f '' t) x)
h₁₄ : x ∈ f '' s → x ∉ f '' t → ((f '' s) x ↔ (f '' t) x) → False
h₁₅ : x ∈ f '' t → x ∉ f '' s → ((f '' s) x ↔ (f '' t) x) → False
h₁₆ : (f '' s) x → ¬(f '' t) x → x ∉ f '' s → x ∈ f '' t
h₁₇ : (f '' s) x → ¬(f '' t) x → ¬x ∉ f '' t → x ∈ f '' t
h₁₈ : (f '' s) x → ¬(f '' t) x → x ∈ f '' s → x ∉ f '' s → False
h₁₉ : (f '' s) x → ¬(f '' t) x → x ∈ f '' s → ¬x ∉ f '' t → False
h₂₀ : x ∈ f '' s → x ∉ f '' t → (f '' s) x → (f '' t) x → False
h₂₁ : x ∈ f '' s → x ∉ f '' t → ¬(f '' s) x → ¬(f '' t) x → False
h₂₂ : x ∈ f '' t → x ∉ f '' s → (f '' s) x → (f '' t) x → False
h₂₃ : x ∈ f '' t → x ∉ f '' s → ¬(f '' s) x → ¬(f '' t) x → False
⊢ ¬((f '' s) x ↔ (f '' t) x) ↔ x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s

Tactic:
tauto
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq_α : {a : α | ¬s a = t a} = s \ t ∪ t \ s
⊢ {a : β | ¬(f '' s) a = (f '' t) a} = f '' s \ f '' t ∪ f '' t \ f '' s

Tactic:
have h_eq_β : { a : β | ¬(f '' s) a = (f '' t) a } = f '' s \ f '' t ∪ f '' t \ f '' s := by
    ext1 x
    simp only [eq_iff_iff, mem_setOf_eq, mem_union, mem_diff]
    tauto
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq_α : {a : α | ¬s a = t a} = s \ t ∪ t \ s
h_eq_β : {a : β | ¬(f '' s) a = (f '' t) a} = f '' s \ f '' t ∪ f '' t \ f '' s
⊢ {a : β | ¬(f '' s) a = (f '' t) a} = f '' (s \ t ∪ t \ s)

Tactic:
rw [← Set.image_diff hfi, ← Set.image_diff hfi, ← Set.image_union] at h_eq_β

Premises used: Set.image_diff, Set.image_union
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq_α : {a : α | ¬s a = t a} = s \ t ∪ t \ s
h_eq_β : {a : β | ¬(f '' s) a = (f '' t) a} = f '' (s \ t ∪ t \ s)
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' (s \ t ∪ t \ s)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) {a : β | ¬(f '' s) a = (f '' t) a} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [h_eq_β]
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq_α : {a : α | ¬s a = t a} = s \ t ∪ t \ s
h_eq_β : {a : β | ¬(f '' s) a = (f '' t) a} = f '' (s \ t ∪ t \ s)
⊢ Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) (s \ t ∪ t \ s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [h_eq_α] at hst
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq_α : {a : α | ¬s a = t a} = s \ t ∪ t \ s
h_eq_β : {a : β | ¬(f '' s) a = (f '' t) a} = f '' (s \ t ∪ t \ s)
hst₁ : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) (s \ t ∪ t \ s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ {a : α | ¬s a = t a} = s \ t ∪ t \ s

Tactic:
rw [h_eq_α] at hst
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq_α : {a : α | ¬s a = t a} = s \ t ∪ t \ s
h_eq_β : {a : β | ¬(f '' s) a = (f '' t) a} = f '' (s \ t ∪ t \ s)
hst₁ : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) (s \ t ∪ t \ s) : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq_α₁ : {a : α | ¬s a = t a} = s \ t ∪ t \ s
⊢ {a : β | ¬(f '' s) a = (f '' t) a} = f '' (s \ t ∪ t \ s)

Tactic:
rw [h_eq_α] at hst
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) (s \ t ∪ t \ s) : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq_α : {a : α | ¬s a = t a} = s \ t ∪ t \ s
h_eq_β : {a : β | ¬(f '' s) a = (f '' t) a} = f '' (s \ t ∪ t \ s)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' (s \ t ∪ t \ s)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_image_eq_zero_of_comap_eq_zero f μ hfi hf hst

Premises used: MeasureTheory.Measure.measure_image_eq_zero_of_comap_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) (s \ t ∪ t \ s) : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq_α : {a : α | ¬s a = t a} = s \ t ∪ t \ s
h_eq_β : {a : β | ¬(f '' s) a = (f '' t) a} = f '' (s \ t ∪ t \ s)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' (s \ t ∪ t \ s)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact measure_image_eq_zero_of_comap_eq_zero f μ hfi hf hst

Premises used: MeasureTheory.Measure.measure_image_eq_zero_of_comap_eq_zero
-- 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 '' s) μ

Tactic:
⟨toMeasurable μ (f '' toMeasurable (μ.comap f) s), measurableSet_toMeasurable _ _, ?_⟩

Premises used: MeasurableSet, MeasureTheory.NullMeasurableSet, MeasureTheory.measurableSet_toMeasurable, MeasureTheory.Measure.comap, And.intro, Exists.intro, Set.image, MeasureTheory.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 μ)
refine : f '' s =ᶠ[ae μ] toMeasurable μ (f '' toMeasurable (comap f μ) s)
⊢ NullMeasurableSet (f '' s) μ

Tactic:
refine ⟨toMeasurable μ (f '' toMeasurable (μ.comap f) s), 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 μ)
⊢ f '' s =ᶠ[ae μ] toMeasurable μ (f '' toMeasurable (comap f μ) s)

Tactic:
EventuallyEq.trans ?_ (NullMeasurableSet.toMeasurable_ae_eq ?_).symm

Premises used: Filter.EventuallyEq.trans, MeasureTheory.NullMeasurableSet.toMeasurable_ae_eq, 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 μ)
refine_1 : f '' s =ᶠ[ae μ] f '' toMeasurable (comap f μ) s
refine_2 : NullMeasurableSet (f '' toMeasurable (comap f μ) s) μ
⊢ f '' s =ᶠ[ae μ] toMeasurable μ (f '' toMeasurable (comap f μ) s)

Tactic:
refine EventuallyEq.trans ?_ (NullMeasurableSet.toMeasurable_ae_eq ?_).symm

Premises used: Filter.EventuallyEq.trans, MeasureTheory.NullMeasurableSet.toMeasurable_ae_eq, Filter.EventuallyEq.symm