awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Invariants (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
fa : α → α
fb : β → β
g : α → β
hg : Measurable g
hfg : Semiconj g fa fb
s : Set β
hs : MeasurableSet s
rw : g ∘ fa ⁻¹' s = g ⁻¹' s
rw₁ : fb ∘ g ⁻¹' s = g ⁻¹' s
⊢ fa ⁻¹' g ⁻¹' s = g ⁻¹' s
have rw₂ : g ⁻¹' fb ⁻¹' s = g ⁻¹' s
Tactic: rw [← preimage_comp, hfg.comp_eq, preimage_comp, hs.2]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Invariants (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
fa : α → α
fb : β → β
g : α → β
hg : Measurable g
hfg : Semiconj g fa fb
s : Set β
hs : MeasurableSet s
rw : g ∘ fa ⁻¹' s = g ⁻¹' s
rw₁ : fb ∘ g ⁻¹' s = g ⁻¹' s
rw₂ : g ⁻¹' fb ⁻¹' s = g ⁻¹' s
⊢ fa ⁻¹' g ⁻¹' s = g ⁻¹' s
have rw₃ : g ⁻¹' s = g ⁻¹' s
Tactic: rw [← preimage_comp, hfg.comp_eq, preimage_comp, hs.2]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Invariants (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
f : α → α
g : α → β
inst_2 : MeasurableSingletonClass β
h : Measurable g
⊢ g ∘ f = g
have h₁ : ∀ (x : α), (g ∘ f) x = g x
Tactic: funext x
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Invariants (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
f : α → α
g : α → β
inst_2 : MeasurableSingletonClass β
h : Measurable g
x : α
⊢ (g ∘ f) x = g x
have h₁ : x ∈ f ⁻¹' g ⁻¹' {g x}
Tactic: suffices x ∈ f ⁻¹' g ⁻¹' {g x} by simpa
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Invariants (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
f : α → α
g : α → β
inst_2 : MeasurableSingletonClass β
h : Measurable g
x : α
⊢ x ∈ f ⁻¹' g ⁻¹' {g x}
have h₁ : x ∈ g ⁻¹' {g x}
Tactic: rw [(h <| measurableSet_singleton (g x)).2, Set.mem_preimage, Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Invariants (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
f : α → α
g : α → β
inst_2 : MeasurableSingletonClass β
h : Measurable g
x : α
h₁ : x ∈ g ⁻¹' {g x}
⊢ x ∈ f ⁻¹' g ⁻¹' {g x}
have h₂ : Membership.mem (γ := Set β) {g x} (g x)
Tactic: rw [(h <| measurableSet_singleton (g x)).2, Set.mem_preimage, Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Invariants (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
f : α → α
g : α → β
inst_2 : MeasurableSingletonClass β
h : Measurable g
x : α
h₁ : x ∈ g ⁻¹' {g x}
h₂ : Membership.mem (γ := Set β) {g x} (g x)
⊢ x ∈ f ⁻¹' g ⁻¹' {g x}
have h₃ : g x = g x
Tactic: rw [(h <| measurableSet_singleton (g x)).2, Set.mem_preimage, Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
s : Set α
this : MeasurableSpace α := generateFrom {s}
⊢ Eq (α := MeasurableSpace α) (generateFrom {s}) (MeasurableSpace.comap (β := Prop) (fun (x : α) ↦ x ∈ s) ⊤)
have refine : LE.le (α := MeasurableSpace α) (MeasurableSpace.comap (β := Prop) (fun (x : α) ↦ x ∈ s) ⊤) (generateFrom {s})
Tactic: refine le_antisymm (generateFrom_le fun t ht => ⟨{True}, trivial, by simp [ht.symm]⟩) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
s : Set α
letI letI₁ letI₂ :
  Eq (α := MeasurableSpace α) (generateFrom {s}) (MeasurableSpace.comap (β := Prop) (fun (x : α) ↦ x ∈ s) ⊤)
⊢ Eq (α := MeasurableSpace α) (generateFrom {s}) (MeasurableSpace.comap (β := Prop) (fun (x : α) ↦ x ∈ s) ⊤)
have letI₃ : LE.le (α := MeasurableSpace α) (MeasurableSpace.comap (β := Prop) (fun (x : α) ↦ x ∈ s) ⊤) (generateFrom {s})
Tactic: classical
  letI : MeasurableSpace α := generateFrom {s}
  refine le_antisymm (generateFrom_le fun t ht => ⟨{True}, trivial, by simp [ht.symm]⟩) ?_
  rintro _ ⟨u, -, rfl⟩
  exact (show MeasurableSet s from GenerateMeasurable.basic _ <| mem_singleton s).mem trivial
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
s : Set α
letI letI₁ letI₂ :
  Eq (α := MeasurableSpace α) (generateFrom {s}) (MeasurableSpace.comap (β := Prop) (fun (x : α) ↦ x ∈ s) ⊤)
letI₃ : LE.le (α := MeasurableSpace α) (MeasurableSpace.comap (β := Prop) (fun (x : α) ↦ x ∈ s) ⊤) (generateFrom {s})
⊢ Eq (α := MeasurableSpace α) (generateFrom {s}) (MeasurableSpace.comap (β := Prop) (fun (x : α) ↦ x ∈ s) ⊤)
have letI₄ : ∀ (u : Set Prop), MeasurableSet.{u_1} (α := α) ((fun (x : α) ↦ x ∈ s) ⁻¹' u)
Tactic: classical
  letI : MeasurableSpace α := generateFrom {s}
  refine le_antisymm (generateFrom_le fun t ht => ⟨{True}, trivial, by simp [ht.symm]⟩) ?_
  rintro _ ⟨u, -, rfl⟩
  exact (show MeasurableSet s from GenerateMeasurable.basic _ <| mem_singleton s).mem trivial
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
s t : Set α
⊢ MeasurableSet t ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ
have simp_rw : MeasurableSet t ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ
Tactic: simp_rw +instances [MeasurableSpace.generateFrom_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
s t : Set α
⊢ ({ MeasurableSet' := fun (s_1 : Set α) ↦ ∃ (s' : Set Prop), MeasurableSet s' ∧ (fun (x : α) ↦ x ∈ s) ⁻¹' s' = s_1,
            measurableSet_empty := ⋯, measurableSet_compl := ⋯, measurableSet_iUnion := ⋯ } :
          MeasurableSpace α).1
      t ↔
    t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ
have simp_rw : (∃ (s' : Set Prop), (fun (x : α) ↦ x ∈ s) ⁻¹' s' = t) ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ
Tactic: simp_rw [MeasurableSpace.measurableSet_top, true_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
s t : Set α
⊢ (∃ (s' : Set Prop), (fun (x : α) ↦ x ∈ s) ⁻¹' s' = t) ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ
have mp : (∃ (s' : Set Prop), (fun (x : α) ↦ x ∈ s) ⁻¹' s' = t) → t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
s t : Set α
mp : (∃ (s' : Set Prop), (fun (x : α) ↦ x ∈ s) ⁻¹' s' = t) → t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ
⊢ (∃ (s' : Set Prop), (fun (x : α) ↦ x ∈ s) ⁻¹' s' = t) ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ
have mpr : t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ → ∃ (s' : Set Prop), (fun (x : α) ↦ x ∈ s) ⁻¹' s' = t
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
s : Set α
x : Set Prop
⊢ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
    (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ
have pos : ∀ (hT : True ∈ x),
  Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
    (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ
Tactic: by_cases hT : True ∈ x
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
s : Set α
x : Set Prop
pos :
  ∀ (hT : True ∈ x),
    Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
        (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ
⊢ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
    (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ
have neg : ∀ (hT : True ∉ x),
  Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
    (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ
Tactic: by_cases hT : True ∈ x
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
⊢ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
    (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ
have pos : ∀ (hF : False ∈ x),
  Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
    (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ
Tactic: by_cases hF : False ∈ x
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
pos :
  ∀ (hF : False ∈ x),
    Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
        (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ
⊢ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
    (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ
have neg : ∀ (hF : False ∉ x),
  Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
    (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ
Tactic: by_cases hF : False ∈ x
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∈ x
⊢ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
    (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ
have pos : x = univ
Tactic: suffices x = univ by grind
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
⊢ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
    (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ
have pos : ∀ (hF : False ∈ x),
  Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
    (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ
Tactic: by_cases hF : False ∈ x
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
pos :
  ∀ (hF : False ∈ x),
    Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
        (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ
⊢ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
    (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ
have neg : ∀ (hF : False ∉ x),
  Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
    (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ
Tactic: by_cases hF : False ∈ x
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
⊢ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
    (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ
have neg : x ⊆ ∅
Tactic: suffices x ⊆ ∅ by grind
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
p : Prop
hp : p ∈ x
⊢ Membership.mem (γ := Set Prop) ∅ p
have neg : ∀ (hp : True ∈ x), Membership.mem (γ := Set Prop) ∅ True
Tactic: fin_cases p
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
p : Prop
hp : p ∈ x
neg : ∀ (hp : True ∈ x), Membership.mem (γ := Set Prop) ∅ True
⊢ Membership.mem (γ := Set Prop) ∅ p
have neg₁ : ∀ (hp : False ∈ x), Membership.mem (γ := Set Prop) ∅ False
Tactic: fin_cases p
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
s : Set α
⊢ ∃ (s' : Set Prop), Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' s') ∅
have h : Eq.{u_1 + 1} (α := Set α) (preimage (β := Prop) (fun (x : α) ↦ x ∈ s) ∅) ∅
Tactic: use ∅
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
s : Set α
⊢ ∃ (s' : Set Prop), Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' s') ∅
have h : Eq.{u_1 + 1} (α := Set α) (preimage (β := Prop) (fun (x : α) ↦ x ∈ s) ∅) ∅
Tactic: on_goal 1 => use ∅
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
t : Set α
⊢ ∃ (s' : Set Prop), (fun (x : α) ↦ x ∈ t) ⁻¹' s' = t
have h : preimage (β := Prop) (fun (x : α) ↦ x ∈ t) {True} = t
Tactic: use {True}
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
t : Set α
⊢ ∃ (s' : Set Prop), (fun (x : α) ↦ x ∈ t) ⁻¹' s' = t
have h : preimage (β := Prop) (fun (x : α) ↦ x ∈ t) {True} = t
Tactic: on_goal 2 => use {True}
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
s : Set α
⊢ ∃ (s' : Set Prop), (fun (x : α) ↦ x ∈ s) ⁻¹' s' = sᶜ
have h : preimage (β := Prop) (fun (x : α) ↦ x ∈ s) {False} = sᶜ
Tactic: use {False}
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
s : Set α
⊢ ∃ (s' : Set Prop), (fun (x : α) ↦ x ∈ s) ⁻¹' s' = sᶜ
have h : preimage (β := Prop) (fun (x : α) ↦ x ∈ s) {False} = sᶜ
Tactic: on_goal 3 => use {False}
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
s : Set α
⊢ ∃ (s' : Set Prop), Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' s') univ
have h : Eq.{u_1 + 1} (α := Set α) (preimage (β := Prop) (fun (x : α) ↦ x ∈ s) univ) univ
Tactic: use Set.univ
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
s : Set α
⊢ ∃ (s' : Set Prop), Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' s') univ
have h : Eq.{u_1 + 1} (α := Set α) (preimage (β := Prop) (fun (x : α) ↦ x ∈ s) univ) univ
Tactic: on_goal 4 => use Set.univ
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
f g : Filter α
inst_1 : f.IsMeasurablyGenerated
inst_2 : g.IsMeasurablyGenerated
⊢ (f ⊓ g).IsMeasurablyGenerated
have exists_measurable_subset : ∀ ⦃s : Set α⦄, s ∈ f ⊓ g → ∃ t ∈ f ⊓ g, MeasurableSet t ∧ t ⊆ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
f g : Filter α
inst_1 : f.IsMeasurablyGenerated
inst_2 : g.IsMeasurablyGenerated
sf : Set α
hsf : sf ∈ f
sg : Set α
hsg : sg ∈ g
⊢ ∃ t ∈ f ⊓ g, MeasurableSet t ∧ t ⊆ sf ∩ sg
have exists_measurable_subset : ∀ (s'f : Set α) (hs'f : s'f ∈ f) (hmf : MeasurableSet s'f) (hs'sf : s'f ⊆ sf),
  ∃ t ∈ f ⊓ g, MeasurableSet t ∧ t ⊆ sf ∩ sg
Tactic: rcases IsMeasurablyGenerated.exists_measurable_subset hsf with ⟨s'f, hs'f, hmf, hs'sf⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
f g : Filter α
inst_1 : f.IsMeasurablyGenerated
inst_2 : g.IsMeasurablyGenerated
sf : Set α
hsf : sf ∈ f
sg : Set α
hsg : sg ∈ g
s'f : Set α
hs'f : s'f ∈ f
hmf : MeasurableSet s'f
hs'sf : s'f ⊆ sf
⊢ ∃ t ∈ f ⊓ g, MeasurableSet t ∧ t ⊆ sf ∩ sg
have exists_measurable_subset : ∀ (s'g : Set α) (hs'g : s'g ∈ g) (hmg : MeasurableSet s'g) (hs'sg : s'g ⊆ sg),
  ∃ t ∈ f ⊓ g, MeasurableSet t ∧ t ⊆ sf ∩ sg
Tactic: rcases IsMeasurablyGenerated.exists_measurable_subset hsg with ⟨s'g, hs'g, hmg, hs'sg⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
f g : Filter α
inst_1 : f.IsMeasurablyGenerated
inst_2 : g.IsMeasurablyGenerated
sf : Set α
hsf : sf ∈ f
sg : Set α
hsg : sg ∈ g
s'f : Set α
hs'f : s'f ∈ f
hmf : MeasurableSet s'f
hs'sf : s'f ⊆ sf
s'g : Set α
hs'g : s'g ∈ g
hmg : MeasurableSet s'g
hs'sg : s'g ⊆ sg
⊢ ∃ t ∈ f ⊓ g, MeasurableSet t ∧ t ⊆ sf ∩ sg
have exists_measurable_subset : s'f ∩ s'g ⊆ sf ∩ sg
Tactic: refine ⟨s'f ∩ s'g, inter_mem_inf hs'f hs'g, hmf.inter hmg, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
⊢ (𝓟 s).IsMeasurablyGenerated ↔ MeasurableSet s
have refine : (𝓟 s).IsMeasurablyGenerated → MeasurableSet s
Tactic: refine ⟨?_, fun hs => ⟨fun t ht => ⟨s, mem_principal_self s, hs, ht⟩⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
hs : ∀ ⦃s_1 : Set α⦄, s_1 ∈ 𝓟 s → ∃ t ∈ 𝓟 s, MeasurableSet t ∧ t ⊆ s_1
⊢ MeasurableSet s
have rcases : ∀ (t : Set α) (ht : t ∈ 𝓟 s) (htm : MeasurableSet t) (hts : t ⊆ s), MeasurableSet s
Tactic: rcases hs (mem_principal_self s) with ⟨t, ht, htm, hts⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
hs : ∀ ⦃s_1 : Set α⦄, s_1 ∈ 𝓟 s → ∃ t ∈ 𝓟 s, MeasurableSet t ∧ t ⊆ s_1
t : Set α
ht : t ∈ 𝓟 s
htm : MeasurableSet t
hts : t ⊆ s
⊢ MeasurableSet s
have this : t = s
Tactic: have : t = s := hts.antisymm ht
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
f : ι → Filter α
inst_1 : ∀ (i : ι), (f i).IsMeasurablyGenerated
⊢ IsMeasurablyGenerated.{u_1} (α := α) (⨅ (i : ι), f i)
have refine : ∀ (s : Set α) (hs : Membership.mem (γ := Filter α) (⨅ (i : ι), f i) s),
  ∃ (t : Set α), Membership.mem (γ := Filter α) (⨅ (i : ι), f i) t ∧ MeasurableSet t ∧ t ⊆ s
Tactic: refine ⟨fun s hs => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
f : ι → Filter α
inst_1 : ∀ (i : ι), (f i).IsMeasurablyGenerated
s : Set α
hs : Membership.mem (γ := Filter α) (⨅ (i : ι), f i) s
⊢ ∃ (t : Set α), Membership.mem (γ := Filter α) (⨅ (i : ι), f i) t ∧ MeasurableSet t ∧ t ⊆ s
have hs₁ : ∃ (I : Set (PLift ι)),
  I.Finite ∧
    ∃ (V : (↑I : Type uι) → Set α),
      (∀ (i : (↑I : Type uι)), V i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))) ∧
        s = ⋂ (i : (↑I : Type uι)), V i
Tactic: rw [← Equiv.plift.surjective.iInf_comp, mem_iInf] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
f : ι → Filter α
inst_1 : ∀ (i : ι), (f i).IsMeasurablyGenerated
s : Set α
hs :
  ∃ (I : Set (PLift ι)),
    I.Finite ∧
      ∃ (V : (↑I : Type uι) → Set α),
        (∀ (i : (↑I : Type uι)), V i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))) ∧
          s = ⋂ (i : (↑I : Type uι)), V i
⊢ ∃ (t : Set α), Membership.mem (γ := Filter α) (⨅ (i : ι), f i) t ∧ MeasurableSet t ∧ t ⊆ s
have rcases : ∀ (t : Set (PLift ι)) (ht : t.Finite) (V : (↑t : Type uι) → Set α)
  (hVf : ∀ (i : (↑t : Type uι)), V i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))),
  ∃ (t_1 : Set α),
    Membership.mem (γ := Filter α) (⨅ (i : ι), f i) t_1 ∧ MeasurableSet t_1 ∧ t_1 ⊆ ⋂ (i : (↑t : Type uι)), V i
Tactic: rcases hs with ⟨t, ht, ⟨V, hVf, rfl⟩⟩
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
f : ι → Filter α
inst_1 : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : (↑t : Type uι) → Set α
hVf : ∀ (i : (↑t : Type uι)), V i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))
⊢ ∃ (t_1 : Set α),
    Membership.mem (γ := Filter α) (⨅ (i : ι), f i) t_1 ∧ MeasurableSet t_1 ∧ t_1 ⊆ ⋂ (i : (↑t : Type uι)), V i
have choose : ∀ (U : (i : (↑t : Type uι)) → Set α)
  (hUf : ∀ (i : (↑t : Type uι)), U i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι)))
  (hU : ∀ (i : (↑t : Type uι)), MeasurableSet (U i) ∧ U i ⊆ V i),
  ∃ (t_1 : Set α),
    Membership.mem (γ := Filter α) (⨅ (i : ι), f i) t_1 ∧ MeasurableSet t_1 ∧ t_1 ⊆ ⋂ (i : (↑t : Type uι)), V i
Tactic: choose U hUf hU using fun i => IsMeasurablyGenerated.exists_measurable_subset (hVf i)
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
f : ι → Filter α
inst_1 : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : (↑t : Type uι) → Set α
hVf : ∀ (i : (↑t : Type uι)), V i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))
U : (i : (↑t : Type uι)) → Set α
hUf : ∀ (i : (↑t : Type uι)), U i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))
hU : ∀ (i : (↑t : Type uι)), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ ∃ (t_1 : Set α),
    Membership.mem (γ := Filter α) (⨅ (i : ι), f i) t_1 ∧ MeasurableSet t_1 ∧ t_1 ⊆ ⋂ (i : (↑t : Type uι)), V i
have refine_1 : Membership.mem (γ := Filter α) (⨅ (i : ι), f i) (⋂ (i : (↑t : Type uι)), U i)
Tactic: refine ⟨⋂ i : t, U i, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
f : ι → Filter α
inst_1 : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : (↑t : Type uι) → Set α
hVf : ∀ (i : (↑t : Type uι)), V i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))
U : (i : (↑t : Type uι)) → Set α
hUf : ∀ (i : (↑t : Type uι)), U i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))
hU : ∀ (i : (↑t : Type uι)), MeasurableSet (U i) ∧ U i ⊆ V i
refine_1 : Membership.mem (γ := Filter α) (⨅ (i : ι), f i) (⋂ (i : (↑t : Type uι)), U i)
⊢ ∃ (t_1 : Set α),
    Membership.mem (γ := Filter α) (⨅ (i : ι), f i) t_1 ∧ MeasurableSet t_1 ∧ t_1 ⊆ ⋂ (i : (↑t : Type uι)), V i
have refine_2 : MeasurableSet.{u_1} (α := α) (⋂ (i : (↑t : Type uι)), U i)
Tactic: refine ⟨⋂ i : t, U i, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
f : ι → Filter α
inst_1 : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : (↑t : Type uι) → Set α
hVf : ∀ (i : (↑t : Type uι)), V i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))
U : (i : (↑t : Type uι)) → Set α
hUf : ∀ (i : (↑t : Type uι)), U i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))
hU : ∀ (i : (↑t : Type uι)), MeasurableSet (U i) ∧ U i ⊆ V i
refine_1 : Membership.mem (γ := Filter α) (⨅ (i : ι), f i) (⋂ (i : (↑t : Type uι)), U i)
refine_2 : MeasurableSet.{u_1} (α := α) (⋂ (i : (↑t : Type uι)), U i)
⊢ ∃ (t_1 : Set α),
    Membership.mem (γ := Filter α) (⨅ (i : ι), f i) t_1 ∧ MeasurableSet t_1 ∧ t_1 ⊆ ⋂ (i : (↑t : Type uι)), V i
have refine_3 : Subset.{u_1} (α := Set α) (⋂ (i : (↑t : Type uι)), U i) (⋂ (i : (↑t : Type uι)), V i)
Tactic: refine ⟨⋂ i : t, U i, ?_, ?_, ?_⟩