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 α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t s : Set α
h_s : Membership.mem (γ := Set (Set α)) (⋃ (b : β), g b) s
⊢ ∃ (T : Finset β) (f : β → Set α), s = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
have base : ∀ (b : β) (h_s_in_t' : Membership.mem (γ := Set (Set α)) ((fun (b : β) ↦ g b) b) s),
  ∃ (T : Finset β) (f : β → Set α), s = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
Tactic: rcases h_s with ⟨t', ⟨⟨b, rfl⟩, h_s_in_t'⟩⟩
Cleared hypotheses: h_s
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t s : Set α
b : β
h_s_in_t' : Membership.mem (γ := Set (Set α)) ((fun (b : β) ↦ g b) b) s
⊢ ∃ (T : Finset β) (f : β → Set α), s = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
have base : s = ⋂ (b_1 : β), ⋂ (_ : Membership.mem (γ := Finset β) {b} b_1), (fun (x : β) ↦ s) b_1 ∧
  ∀ (b_1 : β), Membership.mem (γ := Finset β) {b} b_1 → (fun (x : β) ↦ s) b_1 ∈ g b_1
Tactic: refine ⟨{b}, fun _ => s, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t s t_1 : Set α
h_gen_s : generatePiSystem (⋃ (b : β), g b) s
h_gen_t' : generatePiSystem (⋃ (b : β), g b) t_1
h_nonempty : (s ∩ t_1).Nonempty
h_s : ∃ (T : Finset β) (f : β → Set α), s = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
h_t' : ∃ (T : Finset β) (f : β → Set α), t_1 = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
⊢ ∃ (T : Finset β) (f : β → Set α), s ∩ t_1 = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
have inter : ∀ (T_t' : Finset β) (f_t' : β → Set α) (h_t' : ∀ b ∈ T_t', f_t' b ∈ g b)
  (h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b))
  (h_nonempty : (s ∩ ⋂ b ∈ T_t', f_t' b).Nonempty),
  ∃ (T : Finset β) (f : β → Set α), s ∩ ⋂ b ∈ T_t', f_t' b = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
Tactic: rcases h_t' with ⟨T_t', ⟨f_t', ⟨rfl, h_t'⟩⟩⟩
Cleared hypotheses: t_1, h_gen_t', h_nonempty, h_t'
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t s : Set α
h_gen_s : generatePiSystem (⋃ (b : β), g b) s
h_s : ∃ (T : Finset β) (f : β → Set α), s = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
h_nonempty : (s ∩ ⋂ b ∈ T_t', f_t' b).Nonempty
⊢ ∃ (T : Finset β) (f : β → Set α), s ∩ ⋂ b ∈ T_t', f_t' b = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
have inter : ∀ (T_s : Finset β) (f_s : β → Set α) (h_s : ∀ b ∈ T_s, f_s b ∈ g b)
  (h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b))
  (h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)),
  ∃ (T : Finset β) (f : β → Set α),
    Eq.{u_3 + 1} (α := Set α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b) (⋂ b ∈ T, f b) ∧ ∀ b ∈ T, f b ∈ g b
Tactic: rcases h_s with ⟨T_s, ⟨f_s, ⟨rfl, h_s⟩⟩⟩
Cleared hypotheses: s, h_gen_s, h_s, h_nonempty
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
⊢ ∃ (T : Finset β) (f : β → Set α),
    Eq.{u_3 + 1} (α := Set α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b) (⋂ b ∈ T, f b) ∧ ∀ b ∈ T, f b ∈ g b
have h : Eq.{u_3 + 1} (α := Set α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
    (⋂ b ∈ T_s ∪ T_t',
      (fun (b : β) ↦ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅)
        b) ∧
  ∀ b ∈ T_s ∪ T_t',
    (fun (b : β) ↦ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) b ∈
      g b
Tactic: use T_s ∪ T_t', fun b : β =>
      if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b
      else if b ∈ T_t' then f_t' b else (∅ : Set α)
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
⊢ Eq.{u_3 + 1} (α := Set α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
      (⋂ b ∈ T_s ∪ T_t',
        (fun (b : β) ↦ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅)
          b) ∧
    ∀ b ∈ T_s ∪ T_t',
      (fun (b : β) ↦ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) b ∈
        g b
have h : Eq.{u_3 + 1} (α := Set α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
  (⋂ b ∈ T_s ∪ T_t', if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
h :
  Eq.{u_3 + 1} (α := Set α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
    (⋂ b ∈ T_s ∪ T_t', if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅)
⊢ Eq.{u_3 + 1} (α := Set α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
      (⋂ b ∈ T_s ∪ T_t',
        (fun (b : β) ↦ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅)
          b) ∧
    ∀ b ∈ T_s ∪ T_t',
      (fun (b : β) ↦ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) b ∈
        g b
have h₁ : ∀ b ∈ T_s ∪ T_t', (if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) ∈ g b
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
⊢ Eq.{u_3 + 1} (α := Set α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
    (⋂ b ∈ T_s ∪ T_t', if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅)
have h : ∀ (a : α),
  Membership.mem (γ := Set α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b) a ↔
    Membership.mem (γ := Set α)
      (⋂ b ∈ T_s ∪ T_t', if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅)
      a
Tactic: ext a
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
a : α
⊢ Membership.mem (γ := Set α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b) a ↔
    Membership.mem (γ := Set α)
      (⋂ b ∈ T_s ∪ T_t', if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅)
      a
have h : ((∀ (i : β) (i_1 : i ∈ T_s), a ∈ f_s i) ∧ ∀ (i : β) (i_1 : i ∈ T_t'), a ∈ f_t' i) ↔
  ∀ (i : β) (i_1 : i ∈ T_s ∨ i ∈ T_t'),
    a ∈ if i ∈ T_s then if i ∈ T_t' then f_s i ∩ f_t' i else f_s i else if i ∈ T_t' then f_t' i else ∅
Tactic: simp_rw [Set.mem_inter_iff, Set.mem_iInter, Finset.mem_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
b : β
h_b : b ∈ T_s ∪ T_t'
⊢ (if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) ∈ g b
have pos : ∀ (hbs : b ∈ T_s) (hbt : b ∈ T_t'), f_s b ∩ f_t' b ∈ g b
Tactic: split_ifs with hbs hbt hbt
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
b : β
h_b : b ∈ T_s ∪ T_t'
pos : ∀ (hbs : b ∈ T_s) (hbt : b ∈ T_t'), f_s b ∩ f_t' b ∈ g b
⊢ (if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) ∈ g b
have neg : ∀ (hbs : b ∈ T_s) (hbt : b ∉ T_t'), f_s b ∈ g b
Tactic: split_ifs with hbs hbt hbt
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
b : β
h_b : b ∈ T_s ∪ T_t'
pos : ∀ (hbs : b ∈ T_s) (hbt : b ∈ T_t'), f_s b ∩ f_t' b ∈ g b
neg : ∀ (hbs : b ∈ T_s) (hbt : b ∉ T_t'), f_s b ∈ g b
⊢ (if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) ∈ g b
have pos₁ : ∀ (hbs : b ∉ T_s) (hbt : b ∈ T_t'), f_t' b ∈ g b
Tactic: split_ifs with hbs hbt hbt
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
b : β
h_b : b ∈ T_s ∪ T_t'
pos : ∀ (hbs : b ∈ T_s) (hbt : b ∈ T_t'), f_s b ∩ f_t' b ∈ g b
neg : ∀ (hbs : b ∈ T_s) (hbt : b ∉ T_t'), f_s b ∈ g b
pos₁ : ∀ (hbs : b ∉ T_s) (hbt : b ∈ T_t'), f_t' b ∈ g b
⊢ (if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) ∈ g b
have neg₁ : ∀ (hbs : b ∉ T_s) (hbt : b ∉ T_t'), ∅ ∈ g b
Tactic: split_ifs with hbs hbt hbt
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
b : β
h_b : b ∈ T_s ∪ T_t'
hbs : b ∈ T_s
hbt : b ∈ T_t'
⊢ f_s b ∩ f_t' b ∈ g b
have pos : (⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b ⊆ f_s b ∩ f_t' b
Tactic: refine h_pi b (f_s b) (h_s b hbs) (f_t' b) (h_t' b hbt) (Set.Nonempty.mono ?_ h_nonempty)
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (hypothesis)
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
b : β
h_b : b ∈ T_s ∪ T_t'
hbs : b ∉ T_s
hbt : b ∉ T_t'
⊢ ∅ ∈ g b
have h_b₁ : b ∈ T_s ∨ b ∈ T_t'
Tactic: rw [Finset.mem_union] at h_b
Cleared hypotheses: h_b, hbs, hbt
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
h_t : Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ (b : β), g b)) t
⊢ ∃ (T : Finset β) (f : β → Set α), t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
have base : ∀ {s : Set α} (h_s : Membership.mem (γ := Set (Set α)) (⋃ (b : β), g b) s),
  ∃ (T : Finset β) (f : β → Set α), s = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
Tactic: induction h_t with
  | @base s h_s =>
    rcases h_s with ⟨t', ⟨⟨b, rfl⟩, h_s_in_t'⟩⟩
    refine ⟨{b}, fun _ => s, ?_⟩
    simpa using h_s_in_t'
  | inter h_gen_s h_gen_t' h_nonempty h_s h_t' =>
    rcases h_t' with ⟨T_t', ⟨f_t', ⟨rfl, h_t'⟩⟩⟩
    rcases h_s with ⟨T_s, ⟨f_s, ⟨rfl, h_s⟩⟩⟩
    use T_s ∪ T_t', fun b : β =>
      if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b
      else if b ∈ T_t' then f_t' b else (∅ : Set α)
    constructor
    · ext a
      simp_rw [Set.mem_inter_iff, Set.mem_iInter, Finset.mem_union]
      grind
    intro b h_b
    split_ifs with hbs hbt hbt
    · refine h_pi b (f_s b) (h_s b hbs) (f_t' b) (h_t' b hbt) (Set.Nonempty.mono ?_ h_nonempty)
      exact Set.inter_subset_inter (Set.biInter_subset_of_mem hbs) (Set.biInter_subset_of_mem hbt)
    · exact h_s b hbs
    · exact h_t' b hbt
    · rw [Finset.mem_union] at h_b
      apply False.elim (h_b.elim hbs hbt)
Cleared hypotheses: h_t
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
h_t : Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ (b : β), g b)) t
base :
  ∀ {s : Set α} (h_s : Membership.mem (γ := Set (Set α)) (⋃ (b : β), g b) s),
    ∃ (T : Finset β) (f : β → Set α), s = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
⊢ ∃ (T : Finset β) (f : β → Set α), t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
have inter : ∀ {s t : Set α} (h_gen_s : generatePiSystem (⋃ (b : β), g b) s) (h_gen_t' : generatePiSystem (⋃ (b : β), g b) t)
  (h_nonempty : (s ∩ t).Nonempty) (h_s : ∃ (T : Finset β) (f : β → Set α), s = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b)
  (h_t' : ∃ (T : Finset β) (f : β → Set α), t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b),
  ∃ (T : Finset β) (f : β → Set α), s ∩ t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
Tactic: induction h_t with
  | @base s h_s =>
    rcases h_s with ⟨t', ⟨⟨b, rfl⟩, h_s_in_t'⟩⟩
    refine ⟨{b}, fun _ => s, ?_⟩
    simpa using h_s_in_t'
  | inter h_gen_s h_gen_t' h_nonempty h_s h_t' =>
    rcases h_t' with ⟨T_t', ⟨f_t', ⟨rfl, h_t'⟩⟩⟩
    rcases h_s with ⟨T_s, ⟨f_s, ⟨rfl, h_s⟩⟩⟩
    use T_s ∪ T_t', fun b : β =>
      if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b
      else if b ∈ T_t' then f_t' b else (∅ : Set α)
    constructor
    · ext a
      simp_rw [Set.mem_inter_iff, Set.mem_iInter, Finset.mem_union]
      grind
    intro b h_b
    split_ifs with hbs hbt hbt
    · refine h_pi b (f_s b) (h_s b hbs) (f_t' b) (h_t' b hbt) (Set.Nonempty.mono ?_ h_nonempty)
      exact Set.inter_subset_inter (Set.biInter_subset_of_mem hbs) (Set.biInter_subset_of_mem hbt)
    · exact h_s b hbs
    · exact h_t' b hbt
    · rw [Finset.mem_union] at h_b
      apply False.elim (h_b.elim hbs hbt)
Cleared hypotheses: h_t
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
h_t : Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ (b : β), g b)) t
⊢ ∃ (T : Finset β) (f : β → Set α), t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
have base : ∀ {s : Set α} (h_s : Membership.mem (γ := Set (Set α)) (⋃ (b : β), g b) s),
  ∃ (T : Finset β) (f : β → Set α), s = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
Tactic: classical
  induction h_t with
  | @base s h_s =>
    rcases h_s with ⟨t', ⟨⟨b, rfl⟩, h_s_in_t'⟩⟩
    refine ⟨{b}, fun _ => s, ?_⟩
    simpa using h_s_in_t'
  | inter h_gen_s h_gen_t' h_nonempty h_s h_t' =>
    rcases h_t' with ⟨T_t', ⟨f_t', ⟨rfl, h_t'⟩⟩⟩
    rcases h_s with ⟨T_s, ⟨f_s, ⟨rfl, h_s⟩⟩⟩
    use T_s ∪ T_t', fun b : β =>
      if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b
      else if b ∈ T_t' then f_t' b else (∅ : Set α)
    constructor
    · ext a
      simp_rw [Set.mem_inter_iff, Set.mem_iInter, Finset.mem_union]
      grind
    intro b h_b
    split_ifs with hbs hbt hbt
    · refine h_pi b (f_s b) (h_s b hbs) (f_t' b) (h_t' b hbt) (Set.Nonempty.mono ?_ h_nonempty)
      exact Set.inter_subset_inter (Set.biInter_subset_of_mem hbs) (Set.biInter_subset_of_mem hbt)
    · exact h_s b hbs
    · exact h_t' b hbt
    · rw [Finset.mem_union] at h_b
      apply False.elim (h_b.elim hbs hbt)
Cleared hypotheses: h_t
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
h_t : Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ (b : β), g b)) t
base :
  ∀ {s : Set α} (h_s : Membership.mem (γ := Set (Set α)) (⋃ (b : β), g b) s),
    ∃ (T : Finset β) (f : β → Set α), s = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
⊢ ∃ (T : Finset β) (f : β → Set α), t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
have inter : ∀ {s t : Set α} (h_gen_s : generatePiSystem (⋃ (b : β), g b) s) (h_gen_t' : generatePiSystem (⋃ (b : β), g b) t)
  (h_nonempty : (s ∩ t).Nonempty) (h_s : ∃ (T : Finset β) (f : β → Set α), s = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b)
  (h_t' : ∃ (T : Finset β) (f : β → Set α), t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b),
  ∃ (T : Finset β) (f : β → Set α), s ∩ t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
Tactic: classical
  induction h_t with
  | @base s h_s =>
    rcases h_s with ⟨t', ⟨⟨b, rfl⟩, h_s_in_t'⟩⟩
    refine ⟨{b}, fun _ => s, ?_⟩
    simpa using h_s_in_t'
  | inter h_gen_s h_gen_t' h_nonempty h_s h_t' =>
    rcases h_t' with ⟨T_t', ⟨f_t', ⟨rfl, h_t'⟩⟩⟩
    rcases h_s with ⟨T_s, ⟨f_s, ⟨rfl, h_s⟩⟩⟩
    use T_s ∪ T_t', fun b : β =>
      if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b
      else if b ∈ T_t' then f_t' b else (∅ : Set α)
    constructor
    · ext a
      simp_rw [Set.mem_inter_iff, Set.mem_iInter, Finset.mem_union]
      grind
    intro b h_b
    split_ifs with hbs hbt hbt
    · refine h_pi b (f_s b) (h_s b hbs) (f_t' b) (h_t' b hbt) (Set.Nonempty.mono ?_ h_nonempty)
      exact Set.inter_subset_inter (Set.biInter_subset_of_mem hbs) (Set.biInter_subset_of_mem hbt)
    · exact h_s b hbs
    · exact h_t' b hbt
    · rw [Finset.mem_union] at h_b
      apply False.elim (h_b.elim hbs hbt)
Cleared hypotheses: h_t
-- 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
⊢ Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val (p := s)) b)) t
have suffices : Eq.{u_3 + 1} (α := Set (Set α)) (⋃ (b : Subtype s), (g ∘ Subtype.val (p := s)) b) (⋃ b ∈ s, g b)
Tactic: suffices h1 : ⋃ b : Subtype s, (g ∘ Subtype.val) b = ⋃ b ∈ s, g b by rwa [h1]
-- 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
⊢ Eq.{u_3 + 1} (α := Set (Set α)) (⋃ (b : Subtype s), (g ∘ Subtype.val (p := s)) b) (⋃ b ∈ s, g b)
have h : ∀ (x : Set α),
  Membership.mem (γ := Set (Set α)) (⋃ (b : Subtype s), (g ∘ Subtype.val (p := s)) b) x ↔
    Membership.mem (γ := Set (Set α)) (⋃ b ∈ s, g b) x
Tactic: ext x
-- 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
x : Set α
⊢ Membership.mem (γ := Set (Set α)) (⋃ (b : Subtype s), (g ∘ Subtype.val (p := s)) b) x ↔
    Membership.mem (γ := Set (Set α)) (⋃ b ∈ s, g b) x
have h : (∃ (a : β), s a ∧ x ∈ g a) ↔ ∃ i ∈ s, x ∈ g i
Tactic: simp only [exists_prop, Set.mem_iUnion, Function.comp_apply, Subtype.exists]
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (hypothesis)
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
⊢ ∃ (T : Finset β) (f : β → Set α), (↑T : Set β) ⊆ s ∧ t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
have this : Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val (p := s)) b)) t
Tactic: 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
-- 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
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 rcases : ∀ (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: 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'⟩⟩⟩
Cleared hypotheses: t, h_t, this