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
s_1 : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
μ : Measure β
hf : Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s : Set α
hs : MeasurableSet s
t : Set α
⊢ (((OuterMeasure.comap f : (a : OuterMeasure β) → OuterMeasure α) μ.toOuterMeasure : OuterMeasure α) :
        (a : Set α) → ℝ≥0∞)
      t =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((OuterMeasure.comap f : (a : OuterMeasure β) → OuterMeasure α) μ.toOuterMeasure : OuterMeasure α) :
            (a : Set α) → ℝ≥0∞)
          (t ∩ s) :
        ℝ≥0∞)
      ((((OuterMeasure.comap f : (a : OuterMeasure β) → OuterMeasure α) μ.toOuterMeasure : OuterMeasure α) :
            (a : Set α) → ℝ≥0∞)
          (t \ s) :
        ℝ≥0∞)
have simp : (μ.toOuterMeasure : (a : Set β) → ℝ≥0∞) (f '' t) =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.toOuterMeasure : (a : Set β) → ℝ≥0∞) (f '' t ∩ f '' s) : ℝ≥0∞)
    ((μ.toOuterMeasure : (a : Set β) → ℝ≥0∞) (f '' t \ f '' s) : ℝ≥0∞)
Tactic: simp only [OuterMeasure.comap_apply, image_inter hf.1, image_diff hf.1]
-- 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 μ)
⊢ Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
have rw : ∀
  (hs :
    NullMeasurableSet s
      (OuterMeasure.toMeasure ((OuterMeasure.comap f : (a : OuterMeasure β) → OuterMeasure α) μ.toOuterMeasure) sorry)),
  Eq (α := ℝ≥0∞)
    (((OuterMeasure.toMeasure ((OuterMeasure.comap f : (a : OuterMeasure β) → OuterMeasure α) μ.toOuterMeasure) sorry :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
Tactic: rw [comap, dif_pos (And.intro hfi hf)] at hs ⊢
Cleared hypotheses: hs
-- 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
    (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∞)
have rw : Eq (α := ℝ≥0∞)
  ((((OuterMeasure.comap f : (a : OuterMeasure β) → OuterMeasure α) μ.toOuterMeasure : OuterMeasure α) :
        (a : Set α) → ℝ≥0∞)
      s :
    ℝ≥0∞)
  ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
Tactic: rw [toMeasure_apply₀ _ _ hs, OuterMeasure.comap_apply, coe_toOuterMeasure]
-- 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
    (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∞)
⊢ Eq (α := ℝ≥0∞)
    (((OuterMeasure.toMeasure ((OuterMeasure.comap f : (a : OuterMeasure β) → OuterMeasure α) μ.toOuterMeasure) ⋯ :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ.toOuterMeasure : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
Tactic: rw [toMeasure_apply₀ _ _ hs, OuterMeasure.comap_apply, coe_toOuterMeasure]
-- 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
    (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∞)
⊢ Eq (α := ℝ≥0∞)
    (((OuterMeasure.toMeasure ((OuterMeasure.comap f : (a : OuterMeasure β) → OuterMeasure α) μ.toOuterMeasure) ⋯ :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
Tactic: rw [toMeasure_apply₀ _ _ hs, OuterMeasure.comap_apply, coe_toOuterMeasure]
-- 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 : Set α
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
  (((OuterMeasure.toMeasure ((OuterMeasure.comap f : (a : OuterMeasure β) → OuterMeasure α) μ.toOuterMeasure) sorry :
          Measure α) :
        (a : Set α) → ℝ≥0∞)
      s :
    ℝ≥0∞)
Tactic: rw [comap, dif_pos (And.intro hfi hf)]
-- 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 β
hs : NullMeasurableSet s (comap f μ)
⊢ LE.le (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
have 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∞)
Tactic: by_cases hf : Injective f ∧ ∀ t, MeasurableSet t → NullMeasurableSet (f '' t) μ
-- 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 β
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∞)
⊢ LE.le (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
have 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∞)
Tactic: by_cases hf : Injective f ∧ ∀ t, MeasurableSet t → NullMeasurableSet (f '' t) μ
-- 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 β
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∞)
have pos : LE.le (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
Tactic: rw [comap_apply₀ _ _ hf.1 hf.2 hs]
-- 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 : Set α
hs : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← nonpos_iff_eq_zero]
-- 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 : s =ᶠ[ae (F := Measure α) (comap f μ)] t
⊢ f '' s =ᶠ[ae μ] f '' t
have 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∞)
Tactic: rw [EventuallyEq, ae_iff] at hst ⊢
Cleared hypotheses: hst
-- 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∞)
⊢ {a : α | ¬s a = t a} = s \ t ∪ t \ s
have h : ∀ (x : α), Membership.mem (γ := Set α) {a : α | ¬s a = t a} x ↔ x ∈ s \ t ∪ t \ s
Tactic: ext1 x
-- 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∞)
x : α
⊢ Membership.mem (γ := Set α) {a : α | ¬s a = t a} x ↔ x ∈ s \ t ∪ t \ s
have h : ¬(s x ↔ t x) ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
Tactic: simp only [eq_iff_iff, mem_setOf_eq, mem_union, mem_diff]
-- 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∞)
x : α
⊢ ¬(s x ↔ t x) ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have h : ¬(s x ↔ t x) → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
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∞)
x : α
h : ¬(s x ↔ t x) → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
⊢ ¬(s x ↔ t x) ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have h₁ : x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s → ¬(s x ↔ t x)
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∞)
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)
⊢ ¬(s x ↔ t x) ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have h₂ : ¬s x → t x → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
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∞)
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
⊢ ¬(s x ↔ t x) ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have h₃ : ¬¬s x → ¬t x → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
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∞)
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
⊢ ¬(s x ↔ t x) ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have h₆ : ¬s x → t x → ¬(x ∈ s ∧ x ∉ t) → x ∈ t
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∞)
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
⊢ ¬(s x ↔ t x) ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have h₇ : ¬s x → t x → ¬(x ∈ s ∧ x ∉ t) → x ∉ s
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∞)
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
⊢ ¬(s x ↔ t x) ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have h₈ : ¬¬s x → ¬t x → ¬(x ∈ s ∧ x ∉ t) → x ∈ t
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∞)
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
⊢ ¬(s x ↔ t x) ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have h₉ : ¬¬s x → ¬t x → ¬(x ∈ s ∧ x ∉ t) → x ∉ s
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∞)
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
⊢ ¬(s x ↔ t x) ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have h₁₀ : x ∈ s → x ∉ t → ¬(s x ↔ t x)
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∞)
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)
⊢ ¬(s x ↔ t x) ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have h₁₁ : x ∈ t → x ∉ s → ¬(s x ↔ t x)
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∞)
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
⊢ ¬(s x ↔ t x) ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have h₁₆ : s x → ¬t x → x ∉ s → x ∈ t
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∞)
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
⊢ ¬(s x ↔ t x) ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have h₁₇ : s x → ¬t x → ¬x ∉ t → x ∈ t
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∞)
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
⊢ ¬(s x ↔ t x) ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have h₁₈ : s x → ¬t x → x ∈ s → x ∉ s → 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∞)
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
⊢ ¬(s x ↔ t x) ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have h₁₉ : s x → ¬t x → x ∈ s → ¬x ∉ t → 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∞)
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
⊢ ¬(s x ↔ t x) ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have h₂₀ : x ∈ s → x ∉ t → s x → t x → False
Tactic: tauto