awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
t : Set α
h_t : Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ b ∈ s, g b)) t
have : Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val (p := s)) b)) t
have₁ :
  ∀ (this : Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val (p := s)) b)) t),
    ∃ (T : Finset β) (f : β → Set α), (↑T : Set β) ⊆ s ∧ t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
have₂ : Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val (p := s)) b)) t
have₃ have₄ :
  ∀ (this : Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val (p := s)) b)) t),
    ∃ (T : Finset β) (f : β → Set α), (↑T : Set β) ⊆ s ∧ t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
⊢ ∃ (T : Finset β) (f : β → Set α), (↑T : Set β) ⊆ s ∧ t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
have have₅ : ∀ (T : Finset (Subtype s)) (f : Subtype s → Set α) (h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val (p := s)) b)
  (h_t : Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ b ∈ s, g b)) (⋂ b ∈ T, f b))
  (this :
    Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val (p := s)) b))
      (⋂ b ∈ T, f b)),
  ∃ (T_1 : Finset β) (f_1 : β → Set α),
    (↑T_1 : Set β) ⊆ s ∧ Eq.{u_3 + 1} (α := Set α) (⋂ b ∈ T, f b) (⋂ b ∈ T_1, f_1 b) ∧ ∀ b ∈ T_1, f_1 b ∈ g b
Tactic: classical
  have : t ∈ generatePiSystem (⋃ b : Subtype s, (g ∘ Subtype.val) b) := by
    suffices h1 : ⋃ b : Subtype s, (g ∘ Subtype.val) b = ⋃ b ∈ s, g b by rwa [h1]
    ext x
    simp only [exists_prop, Set.mem_iUnion, Function.comp_apply, Subtype.exists]
    rfl
  rcases @mem_generatePiSystem_iUnion_elim α (Subtype s) (g ∘ Subtype.val)
      (fun b => h_pi b.val b.property) t this with
    ⟨T, ⟨f, ⟨rfl, h_t'⟩⟩⟩
  refine
    ⟨T.image (fun x : s => (x : β)),
      Function.extend (fun x : s => (x : β)) f fun _ : β => (∅ : Set α), by simp, ?_, ?_⟩
  · ext a
    constructor <;>
      · simp -proj only
          [Set.mem_iInter, Subtype.forall, Finset.set_biInter_finset_image]
        intro h1 b h_b h_b_in_T
        have h2 := h1 b h_b h_b_in_T
        revert h2
        rw [Subtype.val_injective.extend_apply]
        apply id
  · intro b h_b
    simp_rw [Finset.mem_image, Subtype.exists, exists_and_right, exists_eq_right]
      at h_b
    obtain ⟨h_b_w, h_b_h⟩ := h_b
    have h_b_alt : b = (Subtype.mk b h_b_w).val := rfl
    rw [h_b_alt, Subtype.val_injective.extend_apply]
    apply h_t'
    apply h_b_h
Cleared hypotheses: t, h_t
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
⊢ piiUnionInter π {i} = π i ∪ {univ}
have h : ∀ (s : Set α), s ∈ piiUnionInter π {i} ↔ s ∈ π i ∪ {univ}
Tactic: ext1 s
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
⊢ s ∈ piiUnionInter π {i} ↔ s ∈ π i ∪ {univ}
have h : Membership.mem (γ := Set (Set α))
    {s : Set α | ∃ (t : Finset ι), (↑t : Set ι) ⊆ {i} ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x} s ↔
  s ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} s
Tactic: simp only [piiUnionInter, exists_prop, mem_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
⊢ Membership.mem (γ := Set (Set α))
      {s : Set α | ∃ (t : Finset ι), (↑t : Set ι) ⊆ {i} ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x}
      s ↔
    s ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} s
have h : Membership.mem (γ := Set (Set α))
    {s : Set α | ∃ (t : Finset ι), (↑t : Set ι) ⊆ {i} ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x} s →
  s ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} s
Tactic: refine ⟨?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
h :
  Membership.mem (γ := Set (Set α))
      {s : Set α | ∃ (t : Finset ι), (↑t : Set ι) ⊆ {i} ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x}
      s →
    s ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} s
⊢ Membership.mem (γ := Set (Set α))
      {s : Set α | ∃ (t : Finset ι), (↑t : Set ι) ⊆ {i} ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x}
      s ↔
    s ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} s
have h₁ : ∀ (h : s ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} s),
  Membership.mem (γ := Set (Set α))
    {s : Set α | ∃ (t : Finset ι), (↑t : Set ι) ⊆ {i} ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x} s
Tactic: refine ⟨?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (hypothesis)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
hti : (↑t : Set ι) ⊆ {i}
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
⊢ ⋂ x ∈ t, f x ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} (⋂ x ∈ t, f x)
have hti₁ : ∀ y ∈ t, y = i
Tactic: simp only [subset_singleton_iff, Finset.mem_coe] at hti
Cleared hypotheses: hti
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
⊢ ⋂ x ∈ t, f x ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} (⋂ x ∈ t, f x)
have pos : ∀ (hi : i ∈ t), ⋂ x ∈ t, f x ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} (⋂ x ∈ t, f x)
Tactic: by_cases hi : i ∈ t
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
pos : ∀ (hi : i ∈ t), ⋂ x ∈ t, f x ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} (⋂ x ∈ t, f x)
⊢ ⋂ x ∈ t, f x ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} (⋂ x ∈ t, f x)
have neg : ∀ (hi : i ∉ t), ⋂ x ∈ t, f x ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} (⋂ x ∈ t, f x)
Tactic: by_cases hi : i ∈ t
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∈ t
⊢ t = {i}
have h : ∀ (x : ι), x ∈ t ↔ Membership.mem (γ := Finset ι) {i} x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∈ t
x : ι
⊢ x ∈ t ↔ Membership.mem (γ := Finset ι) {i} x
have h : x ∈ t ↔ x = i
Tactic: rw [Finset.mem_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (hypothesis)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∈ t
⊢ ⋂ x ∈ t, f x ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} (⋂ x ∈ t, f x)
have ht_eq_i : t = {i}
Tactic: have ht_eq_i : t = {i} := by
        ext1 x
        rw [Finset.mem_singleton]
        exact ⟨fun h => hti x h, fun h => h.symm ▸ hi⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∈ t
ht_eq_i : t = {i}
⊢ ⋂ x ∈ t, f x ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} (⋂ x ∈ t, f x)
have pos : f i ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} (f i)
Tactic: simp only [ht_eq_i, Finset.mem_singleton, iInter_iInter_eq_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∉ t
⊢ t = ∅
have h : ∀ (x : ι), x ∈ t ↔ Membership.mem (γ := Finset ι) ∅ x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∉ t
x : ι
⊢ x ∈ t ↔ Membership.mem (γ := Finset ι) ∅ x
have h : x ∉ t
Tactic: simp only [Finset.notMem_empty, iff_false]
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (hypothesis)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∉ t
⊢ ⋂ x ∈ t, f x ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} (⋂ x ∈ t, f x)
have ht_empty : t = ∅
Tactic: have ht_empty : t = ∅ := by
        ext1 x
        simp only [Finset.notMem_empty, iff_false]
        exact fun hx => hi (hti x hx ▸ hx)
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
h : s ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} s
⊢ Membership.mem (γ := Set (Set α))
    {s : Set α | ∃ (t : Finset ι), (↑t : Set ι) ⊆ {i} ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x} s
have h₁ : ∀ (hs : s ∈ π i),
  Membership.mem (γ := Set (Set α))
    {s : Set α | ∃ (t : Finset ι), (↑t : Set ι) ⊆ {i} ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x} s
Tactic: rcases h with hs | hs
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
h : s ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} s
h₁ :
  ∀ (hs : s ∈ π i),
    Membership.mem (γ := Set (Set α))
      {s : Set α | ∃ (t : Finset ι), (↑t : Set ι) ⊆ {i} ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x} s
⊢ Membership.mem (γ := Set (Set α))
    {s : Set α | ∃ (t : Finset ι), (↑t : Set ι) ⊆ {i} ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x} s
have h₂ : ∀ (hs : Membership.mem (γ := Set (Set α)) {univ} s),
  Membership.mem (γ := Set (Set α))
    {s : Set α | ∃ (t : Finset ι), (↑t : Set ι) ⊆ {i} ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x} s
Tactic: rcases h with hs | hs
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ Membership.mem (γ := Set (Set α))
    {s : Set α | ∃ (t : Finset ι), (↑t : Set ι) ⊆ {i} ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x} s
have h : (↑{i} : Set ι) ⊆ {i}
Tactic: refine ⟨{i}, ?_, fun _ => s, ⟨fun x hx => ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
h : (↑{i} : Set ι) ⊆ {i}
⊢ Membership.mem (γ := Set (Set α))
    {s : Set α | ∃ (t : Finset ι), (↑t : Set ι) ⊆ {i} ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x} s
have h₁ : ∀ (x : ι) (hx : Membership.mem (γ := Finset ι) {i} x), (fun (x : ι) ↦ s) x ∈ π x
Tactic: refine ⟨{i}, ?_, fun _ => s, ⟨fun x hx => ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
h : (↑{i} : Set ι) ⊆ {i}
h₁ : ∀ (x : ι) (hx : Membership.mem (γ := Finset ι) {i} x), (fun (x : ι) ↦ s) x ∈ π x
⊢ Membership.mem (γ := Set (Set α))
    {s : Set α | ∃ (t : Finset ι), (↑t : Set ι) ⊆ {i} ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x} s
have h₂ : s = ⋂ (x : ι), ⋂ (_ : Membership.mem (γ := Finset ι) {i} x), (fun (x : ι) ↦ s) x
Tactic: refine ⟨{i}, ?_, fun _ => s, ⟨fun x hx => ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ (↑{i} : Set ι) ⊆ {i}
have h : Subset (α := Set ι) {i} {i}
Tactic: rw [Finset.coe_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (hypothesis)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
x : ι
hx : Membership.mem (γ := Finset ι) {i} x
⊢ (fun (x : ι) ↦ s) x ∈ π x
have hx₁ : x = i
Tactic: rw [Finset.mem_singleton] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : Membership.mem (γ := Set (Set α)) {univ} s
⊢ Membership.mem (γ := Set (Set α))
    {s : Set α | ∃ (t : Finset ι), (↑t : Set ι) ⊆ {i} ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x} s
have h : (↑∅ : Set ι) ⊆ {i} ∧
  ∃ (f : ι → Set α),
    (∀ (x : ι), Membership.mem (γ := Finset ι) ∅ x → f x ∈ π x) ∧
      s = ⋂ (x : ι), ⋂ (_ : Membership.mem (γ := Finset ι) ∅ x), f x
Tactic: refine ⟨∅, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
⊢ Eq.{u_3 + 1} (α := Set (Set α)) (piiUnionInter (fun (i : ι) ↦ {s i}) S)
    {s' : Set α | ∃ (t : Finset ι) (_ : (↑t : Set ι) ⊆ S), s' = ⋂ i ∈ t, s i}
have h : ∀ (s' : Set α),
  Membership.mem (γ := Set (Set α)) (piiUnionInter (fun (i : ι) ↦ {s i}) S) s' ↔
    Membership.mem (γ := Set (Set α)) {s' : Set α | ∃ (t : Finset ι) (_ : (↑t : Set ι) ⊆ S), s' = ⋂ i ∈ t, s i} s'
Tactic: ext1 s'
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
s' : Set α
⊢ Membership.mem (γ := Set (Set α)) (piiUnionInter (fun (i : ι) ↦ {s i}) S) s' ↔
    Membership.mem (γ := Set (Set α)) {s' : Set α | ∃ (t : Finset ι) (_ : (↑t : Set ι) ⊆ S), s' = ⋂ i ∈ t, s i} s'
have h : (∃ (t : Finset ι), (↑t : Set ι) ⊆ S ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x = s x) ∧ s' = ⋂ x ∈ t, f x) ↔
  ∃ (t : Finset ι), (↑t : Set ι) ⊆ S ∧ s' = ⋂ i ∈ t, s i
Tactic: simp_rw [piiUnionInter, Set.mem_singleton_iff, exists_prop, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
s' : Set α
⊢ (∃ (t : Finset ι), (↑t : Set ι) ⊆ S ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x = s x) ∧ s' = ⋂ x ∈ t, f x) ↔
    ∃ (t : Finset ι), (↑t : Set ι) ⊆ S ∧ s' = ⋂ i ∈ t, s i
have h : ∀ (h : ∃ (t : Finset ι), (↑t : Set ι) ⊆ S ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x = s x) ∧ s' = ⋂ x ∈ t, f x),
  ∃ (t : Finset ι), (↑t : Set ι) ⊆ S ∧ s' = ⋂ i ∈ t, s i
Tactic: refine ⟨fun h => ?_, fun ⟨t, htS, h_eq⟩ => ⟨t, htS, s, fun _ _ => rfl, h_eq⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
⊢ Eq.{u_3 + 1} (α := MeasurableSpace α) (generateFrom (piiUnionInter (fun (k : ι) ↦ {s k}) S))
    (generateFrom {t : Set α | ∃ k ∈ S, s k = t})
have refine_1 : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) (piiUnionInter (fun (k : ι) ↦ {s k}) S) t → MeasurableSet t
Tactic: refine le_antisymm (generateFrom_le ?_) (generateFrom_mono ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
refine_1 : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) (piiUnionInter (fun (k : ι) ↦ {s k}) S) t → MeasurableSet t
⊢ Eq.{u_3 + 1} (α := MeasurableSpace α) (generateFrom (piiUnionInter (fun (k : ι) ↦ {s k}) S))
    (generateFrom {t : Set α | ∃ k ∈ S, s k = t})
have refine_2 : Subset.{u_3} (α := Set (Set α)) {t : Set α | ∃ k ∈ S, s k = t} (piiUnionInter (fun (k : ι) ↦ {s k}) S)
Tactic: refine le_antisymm (generateFrom_le ?_) (generateFrom_mono ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
I : Finset ι
hI : (↑I : Set ι) ⊆ S
f : ι → Set α
hf : ∀ x ∈ I, Membership.mem (γ := Set (Set α)) ((fun (k : ι) ↦ ({s k} : Set (Set α))) x) (f x)
⊢ MeasurableSet.{u_3} (α := α) (⋂ x ∈ I, f x)
have refine_1 : ∀ (m : ι) (hm : m ∈ I), Membership.mem (γ := Set (Set α)) {t : Set α | ∃ k ∈ S, s k = t} (f m)
Tactic: refine Finset.measurableSet_biInter _ fun m hm => measurableSet_generateFrom ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
⊢ Membership.mem (γ := Set (Set α)) (piiUnionInter (fun (k : ι) ↦ {s k}) S) (s k)
have refine_2 : ∀ (m : ι) (hm : m ∈ (↑{k} : Set ι)), m ∈ S
Tactic: refine ⟨{k}, fun m hm => ?_, s, fun i _ => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
refine_2 : ∀ (m : ι) (hm : m ∈ (↑{k} : Set ι)), m ∈ S
⊢ Membership.mem (γ := Set (Set α)) (piiUnionInter (fun (k : ι) ↦ {s k}) S) (s k)
have refine_2₁ : ∀ (i : ι),
  Membership.mem (γ := Finset ι) {k} i →
    Membership.mem (γ := Set (Set α)) ((fun (k : ι) ↦ ({s k} : Set (Set α))) i) (s i)
Tactic: refine ⟨{k}, fun m hm => ?_, s, fun i _ => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
refine_2 : ∀ (m : ι) (hm : m ∈ (↑{k} : Set ι)), m ∈ S
refine_2₁ :
  ∀ (i : ι),
    Membership.mem (γ := Finset ι) {k} i →
      Membership.mem (γ := Set (Set α)) ((fun (k : ι) ↦ ({s k} : Set (Set α))) i) (s i)
⊢ Membership.mem (γ := Set (Set α)) (piiUnionInter (fun (k : ι) ↦ {s k}) S) (s k)
have refine_2₂ : s k = ⋂ (x : ι), ⋂ (_ : Membership.mem (γ := Finset ι) {k} x), s x
Tactic: refine ⟨{k}, fun m hm => ?_, s, fun i _ => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (hypothesis)
Goal:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
m : ι
hm : m ∈ (↑{k} : Set ι)
⊢ m ∈ S
have hm₁ : m = k
Tactic: rw [Finset.mem_coe, Finset.mem_singleton] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (hypothesis)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : (↑p1 : Set ι) ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : (↑p2 : Set ι) ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : (n : ι) → Set α := fun (n : ι) ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
⊢ ∃ (t : Finset ι) (_ : (↑t : Set ι) ⊆ S) (f : ι → Set α) (_ : ∀ x ∈ t, f x ∈ π x), t1 ∩ t2 = ⋂ x ∈ t, f x
have hp_union_ss : (↑(p1 ∪ p2) : Set ι) ⊆ S
Tactic: have hp_union_ss : ↑(p1 ∪ p2) ⊆ S := by
    simp only [hp1S, hp2S, Finset.coe_union, union_subset_iff, and_self_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : (↑p1 : Set ι) ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : (↑p2 : Set ι) ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : (n : ι) → Set α := fun (n : ι) ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : (↑(p1 ∪ p2) : Set ι) ⊆ S
⊢ ∃ (t : Finset ι) (_ : (↑t : Set ι) ⊆ S) (f : ι → Set α) (_ : ∀ x ∈ t, f x ∈ π x), t1 ∩ t2 = ⋂ x ∈ t, f x
have h : ∃ (_ : ∀ x ∈ p1 ∪ p2, g x ∈ π x), t1 ∩ t2 = ⋂ x ∈ p1 ∪ p2, g x
Tactic: use p1 ∪ p2, hp_union_ss, g
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : (↑p1 : Set ι) ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : (↑p2 : Set ι) ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : (n : ι) → Set α := fun (n : ι) ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : (↑(p1 ∪ p2) : Set ι) ⊆ S
⊢ t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
have rw : Eq.{u_3 + 1} (α := Set α) ((⋂ x ∈ p1, f1 x) ∩ ⋂ x ∈ p2, f2 x) (⋂ i ∈ p1 ∪ p2, g i)
Tactic: rw [ht1_eq, ht2_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : (↑p1 : Set ι) ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : (↑p2 : Set ι) ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : (n : ι) → Set α := fun (n : ι) ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : (↑(p1 ∪ p2) : Set ι) ⊆ S
⊢ Eq.{u_3 + 1} (α := Set α) ((⋂ x ∈ p1, f1 x) ⊓ ⋂ x ∈ p2, f2 x) (⋂ i ∈ p1 ∪ p2, g i)
have h : ∀ (x : α),
  Membership.mem (γ := Set α) ((⋂ x ∈ p1, f1 x) ⊓ ⋂ x ∈ p2, f2 x) x ↔ Membership.mem (γ := Set α) (⋂ i ∈ p1 ∪ p2, g i) x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : (↑p1 : Set ι) ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : (↑p2 : Set ι) ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : (n : ι) → Set α := fun (n : ι) ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : (↑(p1 ∪ p2) : Set ι) ⊆ S
x : α
⊢ Membership.mem (γ := Set α) ((⋂ x ∈ p1, f1 x) ⊓ ⋂ x ∈ p2, f2 x) x ↔ Membership.mem (γ := Set α) (⋂ i ∈ p1 ∪ p2, g i) x
have h : ((∀ (i : ι) (i_1 : i ∈ p1), x ∈ f1 i) ∧ ∀ (i : ι) (i_1 : i ∈ p2), x ∈ f2 i) ↔ ∀ (i : ι) (i_1 : i ∈ p1 ∪ p2), x ∈ g i
Tactic: simp only [inf_eq_inter, mem_inter_iff, mem_iInter]
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (hypothesis)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : (↑p1 : Set ι) ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : (↑p2 : Set ι) ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : (n : ι) → Set α := fun (n : ι) ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : (↑(p1 ∪ p2) : Set ι) ⊆ S
⊢ ∃ (_ : ∀ x ∈ p1 ∪ p2, g x ∈ π x), t1 ∩ t2 = ⋂ x ∈ p1 ∪ p2, g x
have h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
Tactic: have h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i := by
    rw [ht1_eq, ht2_eq]
    simp_rw [← Set.inf_eq_inter]
    ext1 x
    simp only [inf_eq_inter, mem_inter_iff, mem_iInter]
    grind
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : (↑p1 : Set ι) ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : (↑p2 : Set ι) ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : (n : ι) → Set α := fun (n : ι) ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : (↑(p1 ∪ p2) : Set ι) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
⊢ ∃ (_ : ∀ x ∈ p1 ∪ p2, g x ∈ π x), t1 ∩ t2 = ⋂ x ∈ p1 ∪ p2, g x
have h : ∀ (n : ι) (hn : n ∈ p1 ∪ p2), g n ∈ π n
Tactic: refine ⟨fun n hn => ?_, h_inter_eq⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : (↑p1 : Set ι) ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : (↑p2 : Set ι) ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : (n : ι) → Set α := fun (n : ι) ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : (↑(p1 ∪ p2) : Set ι) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
⊢ ((if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ) ∈ π n
have pos : ∀ (hn1 : n ∈ p1) (hn2 : n ∈ p2), f1 n ∩ f2 n ∈ π n
Tactic: split_ifs with hn1 hn2 h