awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
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
⊢ ¬((f '' s) x ↔ (f '' t) x) ↔ x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
have h₂₀ : x ∈ f '' s → x ∉ f '' t → (f '' s) x → (f '' t) x → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
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
⊢ ¬((f '' s) x ↔ (f '' t) x) ↔ x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
have h₂₁ : x ∈ f '' s → x ∉ f '' t → ¬(f '' s) x → ¬(f '' t) x → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
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
⊢ ¬((f '' s) x ↔ (f '' t) x) ↔ x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
have h₂₂ : x ∈ f '' t → x ∉ f '' s → (f '' s) x → (f '' t) x → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
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
⊢ ¬((f '' s) x ↔ (f '' t) x) ↔ x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
have h₂₃ : x ∈ f '' t → x ∉ f '' s → ¬(f '' s) x → ¬(f '' t) x → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (hypothesis)
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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) {a : β | ¬(f '' s) a = (f '' t) a} : ℝ≥0∞) (0 : ℝ≥0∞)
have h_eq_β : {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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (hypothesis)
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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) {a : β | ¬(f '' s) a = (f '' t) a} : ℝ≥0∞) (0 : ℝ≥0∞)
have h_eq_β₁ : {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_β
Cleared hypotheses: h_eq_β
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
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∞) ((μ : (a : Set β) → ℝ≥0∞) {a : β | ¬(f '' s) a = (f '' t) a} : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' (s \ t ∪ t \ s)) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [h_eq_β]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (hypothesis)
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∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' (s \ t ∪ t \ s)) : ℝ≥0∞) (0 : ℝ≥0∞)
have hst₁ : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) (s \ t ∪ t \ s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [h_eq_α] at hst
Cleared hypotheses: hst, h_eq_α, h_eq_β
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
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) μ
have refine : f '' s =ᶠ[ae μ] toMeasurable μ (f '' toMeasurable (comap f μ) s)
Tactic: refine ⟨toMeasurable μ (f '' toMeasurable (μ.comap f) s), measurableSet_toMeasurable _ _, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
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)
have refine_1 : f '' s =ᶠ[ae μ] f '' toMeasurable (comap f μ) s
Tactic: refine EventuallyEq.trans ?_ (NullMeasurableSet.toMeasurable_ae_eq ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
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
⊢ f '' s =ᶠ[ae μ] toMeasurable μ (f '' toMeasurable (comap f μ) s)
have refine_2 : NullMeasurableSet (f '' toMeasurable (comap f μ) s) μ
Tactic: refine EventuallyEq.trans ?_ (NullMeasurableSet.toMeasurable_ae_eq ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (hypothesis)
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 μ] f '' toMeasurable (comap f μ) s
have h : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
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
⊢ Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    ((μ : (a : Set β) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
Tactic: rw [comap_apply₀ _ _ hf h (hf' hs).nullMeasurableSet, image_preimage_eq_inter_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    ((μ : (a : Set β) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
Tactic: rw [comap_apply₀ _ _ hf h (hf' hs).nullMeasurableSet, image_preimage_eq_inter_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
⊢ Eq (α := Measure α) (comap f 0) 0
have pos : ∀ (hf : Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) 0), Eq (α := Measure α) (comap f 0) 0
Tactic: by_cases hf : Injective f ∧ ∀ s, MeasurableSet s → NullMeasurableSet (f '' s) (0 : Measure β)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
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
⊢ Eq (α := Measure α) (comap f 0) 0
have neg : ∀ (hf : ¬(Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) 0)),
  Eq (α := Measure α) (comap f 0) 0
Tactic: by_cases hf : Injective f ∧ ∀ s, MeasurableSet s → NullMeasurableSet (f '' s) (0 : Measure β)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
⊢ comap (fun (x : β) ↦ x) μ = μ
have h : ∀ (s : Set β) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((comap (fun (x : β) ↦ x) μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((comap (fun (x : β) ↦ x) μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h : Injective (β := β) fun (x : β) ↦ x
Tactic: rw [comap_apply, image_id']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
h : Injective (β := β) fun (x : β) ↦ x
⊢ Eq (α := ℝ≥0∞) (((comap (fun (x : β) ↦ x) μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : ∀ (s : Set β), MeasurableSet s → MeasurableSet (α := β) ((fun (x : β) ↦ x) '' s)
Tactic: rw [comap_apply, image_id']
-- 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 γ
⊢ Eq (α := Measure α) (comap f (comap g μ)) (comap (g ∘ f) μ)
have pos : ∀ (hf : Injective f), Eq (α := Measure α) (comap f (comap g μ)) (comap (g ∘ f) μ)
Tactic: by_cases hf : Injective f
-- 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 γ
pos : ∀ (hf : Injective f), Eq (α := Measure α) (comap f (comap g μ)) (comap (g ∘ f) μ)
⊢ Eq (α := Measure α) (comap f (comap g μ)) (comap (g ∘ f) μ)
have neg : ∀ (hf : ¬Injective f), Eq (α := Measure α) (comap f (comap g μ)) (comap (g ∘ f) μ)
Tactic: by_cases hf : Injective f
-- 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
⊢ Eq (α := Measure α) (comap f (comap g μ)) (comap (g ∘ f) μ)
have 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∞)
Tactic: ext s hs
-- 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
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∞)
have pos : Eq (α := ℝ≥0∞) (((comap g μ : Measure β) : (a : Set β) → ℝ≥0∞) (f '' 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]
-- 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
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∞)
⊢ Eq (α := ℝ≥0∞) (((comap f (comap g μ) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((comap (g ∘ f) μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have pos₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set γ) → ℝ≥0∞) (g '' f '' 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]
-- 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
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∞)
⊢ Eq (α := ℝ≥0∞) (((comap f (comap g μ) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((comap (g ∘ f) μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have pos₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set γ) → ℝ≥0∞) (g '' f '' s) : ℝ≥0∞) ((μ : (a : Set γ) → ℝ≥0∞) (g ∘ f '' 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]
-- 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
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∞)
⊢ Eq (α := ℝ≥0∞) (((comap f (comap g μ) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((comap (g ∘ f) μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have pos₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set γ) → ℝ≥0∞) (g '' f '' s) : ℝ≥0∞) ((μ : (a : Set γ) → ℝ≥0∞) (g '' f '' 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]
-- 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
⊢ Eq (α := Measure α) (comap f (comap g μ)) (comap (g ∘ f) μ)
have 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 μ)))
      sorry
  else 0)
  (comap (g ∘ f) μ)
Tactic: rw [comap, dif_neg <| mt And.left hf, comap, dif_neg fun h ↦ hf h.1.of_comp]