awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.PiSystem
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
suffices : Eq.{u_3 + 1} (α := Set (Set α)) (⋃ (b : Subtype s), (g ∘ Subtype.val (p := s)) b) (⋃ b ∈ s, g b)
⊢ Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val (p := s)) b)) t

Tactic:
suffices h1 : ⋃ b : Subtype s, (g ∘ Subtype.val) b = ⋃ b ∈ s, g b by rwa [h1]
-- Module: Mathlib.MeasureTheory.PiSystem
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
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
⊢ Eq.{u_3 + 1} (α := Set (Set α)) (⋃ (b : Subtype s), (g ∘ Subtype.val (p := s)) b) (⋃ b ∈ s, g b)

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.PiSystem
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 α
h : (∃ (a : β), s a ∧ x ∈ g a) ↔ ∃ i ∈ s, x ∈ g i
⊢ Membership.mem (γ := Set (Set α)) (⋃ (b : Subtype s), (g ∘ Subtype.val (p := s)) b) x ↔
    Membership.mem (γ := Set (Set α)) (⋃ b ∈ s, g b) x

Tactic:
simp only [exists_prop, Set.mem_iUnion, Function.comp_apply, Subtype.exists]

Premises used: Set.mem_iUnion, Subtype.exists, exists_prop, Function.comp_apply
-- Module: Mathlib.MeasureTheory.PiSystem
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 α
⊢ (∃ (a : β), s a ∧ x ∈ g a) ↔ ∃ i ∈ s, x ∈ g i

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.PiSystem
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

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
-- Module: Mathlib.MeasureTheory.PiSystem
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
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
⊢ ∃ (T : Finset β) (f : β → Set α), (↑T : Set β) ⊆ s ∧ t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f 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'⟩⟩⟩

Premises used: mem_generatePiSystem_iUnion_elim, Subtype.val, rfl, Subtype.property
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
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)
⊢ (↑(Finset.image (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) T) : Set β) ⊆ s

Tactic:
simp
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
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)
refine_1 :
  Eq.{u_3 + 1} (α := Set α) (⋂ b ∈ T, f b)
    (⋂ (b : β),
      ⋂ (_ : Membership.mem (γ := Finset β) (Finset.image (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) T) b),
        Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅) b)
refine_2 :
  ∀ (b : β),
    Membership.mem (γ := Finset β) (Finset.image (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) T) b →
      Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅) b ∈ g 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:
refine
    ⟨T.image (fun x : s => (x : β)),
      Function.extend (fun x : s => (x : β)) f fun _ : β => (∅ : Set α), by simp, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
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)
refine_1 :
  ∀ (a : α),
    Membership.mem (γ := Set α) (⋂ b ∈ T, f b) a ↔
      Membership.mem (γ := Set α)
        (⋂ (b : β),
          ⋂ (_ : Membership.mem (γ := Finset β) (Finset.image (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) T) b),
            Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅) b)
        a
⊢ Eq.{u_3 + 1} (α := Set α) (⋂ b ∈ T, f b)
    (⋂ (b : β),
      ⋂ (_ : Membership.mem (γ := Finset β) (Finset.image (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) T) b),
        Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅) b)

Tactic:
ext a
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
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)
a : α
refine_1 :
  Membership.mem (γ := Set α) (⋂ b ∈ T, f b) a →
    Membership.mem (γ := Set α)
      (⋂ (b : β),
        ⋂ (_ : Membership.mem (γ := Finset β) (Finset.image (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) T) b),
          Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅) b)
      a
refine_1₁ :
  Membership.mem (γ := Set α)
      (⋂ (b : β),
        ⋂ (_ : Membership.mem (γ := Finset β) (Finset.image (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) T) b),
          Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅) b)
      a →
    Membership.mem (γ := Set α) (⋂ b ∈ T, f b) a
⊢ Membership.mem (γ := Set α) (⋂ b ∈ T, f b) a ↔
    Membership.mem (γ := Set α)
      (⋂ (b : β),
        ⋂ (_ : Membership.mem (γ := Finset β) (Finset.image (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) T) b),
          Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅) b)
      a

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
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)
a : α
refine_1 :
  (∀ (a_1 : β) (b : s a_1) (i : Subtype.mk (p := fun (a : β) ↦ s a) a_1 b ∈ T),
      a ∈ f (Subtype.mk (p := fun (a : β) ↦ s a) a_1 b)) →
    ∀ (a_2 : β) (b : a_2 ∈ s) (i : Subtype.mk (p := fun (a : β) ↦ a ∈ s) a_2 b ∈ T),
      a ∈
        Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅)
          (↑(Subtype.mk (p := fun (a : β) ↦ a ∈ s) a_2 b) : β)
⊢ Membership.mem (γ := Set α) (⋂ b ∈ T, f b) a →
    Membership.mem (γ := Set α)
      (⋂ (b : β),
        ⋂ (_ : Membership.mem (γ := Finset β) (Finset.image (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) T) b),
          Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅) b)
      a

Tactic:
simp -proj only
          [Set.mem_iInter, Subtype.forall, Finset.set_biInter_finset_image]

Premises used: Finset.set_biInter_finset_image, Subtype.forall, Set.mem_iInter
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
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)
a : α
h1 :
  ∀ (a_1 : β) (b : s a_1) (i : Subtype.mk (p := fun (a : β) ↦ s a) a_1 b ∈ T),
    a ∈ f (Subtype.mk (p := fun (a : β) ↦ s a) a_1 b)
b : β
h_b : b ∈ s
h_b_in_T : Subtype.mk (p := fun (a : β) ↦ a ∈ s) b h_b ∈ T
⊢ a ∈ f (Subtype.mk (p := fun (a : β) ↦ s a) b h_b)

Tactic:
have h2 := h1 b h_b h_b_in_T
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
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)
a : α
h1 :
  ∀ (a_1 : β) (b : s a_1) (i : Subtype.mk (p := fun (a : β) ↦ s a) a_1 b ∈ T),
    a ∈ f (Subtype.mk (p := fun (a : β) ↦ s a) a_1 b)
b : β
h_b : b ∈ s
h_b_in_T : Subtype.mk (p := fun (a : β) ↦ a ∈ s) b h_b ∈ T
h2 : a ∈ f (Subtype.mk (p := fun (a : β) ↦ s a) b h_b)
refine_1 :
  ∀ (h2 : a ∈ f (Subtype.mk (p := fun (a : β) ↦ s a) b h_b)),
    a ∈
      Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅)
        (↑(Subtype.mk (p := fun (a : β) ↦ a ∈ s) b h_b) : β)
⊢ a ∈
    Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅)
      (↑(Subtype.mk (p := fun (a : β) ↦ a ∈ s) b h_b) : β)

Tactic:
revert h2
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
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)
a : α
h1 :
  ∀ (a_1 : β) (b : s a_1) (i : Subtype.mk (p := fun (a : β) ↦ s a) a_1 b ∈ T),
    a ∈ f (Subtype.mk (p := fun (a : β) ↦ s a) a_1 b)
b : β
h_b : b ∈ s
h_b_in_T : Subtype.mk (p := fun (a : β) ↦ a ∈ s) b h_b ∈ T
refine_1 :
  ∀ (h2 : a ∈ f (Subtype.mk (p := fun (a : β) ↦ s a) b h_b)), a ∈ f (Subtype.mk (p := fun (a : β) ↦ a ∈ s) b h_b)
⊢ ∀ (h2 : a ∈ f (Subtype.mk (p := fun (a : β) ↦ s a) b h_b)),
    a ∈
      Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅)
        (↑(Subtype.mk (p := fun (a : β) ↦ a ∈ s) b h_b) : β)

Tactic:
rw [Subtype.val_injective.extend_apply]

Premises used: Subtype.val_injective, Function.Injective.extend_apply
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
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)
a : α
h1 :
  ∀ (a_1 : β) (b : s a_1) (i : Subtype.mk (p := fun (a : β) ↦ s a) a_1 b ∈ T),
    a ∈ f (Subtype.mk (p := fun (a : β) ↦ s a) a_1 b)
b : β
h_b : b ∈ s
h_b_in_T : Subtype.mk (p := fun (a : β) ↦ a ∈ s) b h_b ∈ T
⊢ ∀ (h2 : a ∈ f (Subtype.mk (p := fun (a : β) ↦ s a) b h_b)), a ∈ f (Subtype.mk (p := fun (a : β) ↦ a ∈ s) b h_b)

Tactic:
apply id

Premises used: id
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
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)
a : α
refine_1 :
  (∀ (a_1 : β) (b : a_1 ∈ s) (i : Subtype.mk (p := fun (a : β) ↦ a ∈ s) a_1 b ∈ T),
      a ∈
        Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅)
          (↑(Subtype.mk (p := fun (a : β) ↦ a ∈ s) a_1 b) : β)) →
    ∀ (a_2 : β) (b : s a_2) (i : Subtype.mk (p := fun (a : β) ↦ s a) a_2 b ∈ T),
      a ∈ f (Subtype.mk (p := fun (a : β) ↦ s a) a_2 b)
⊢ Membership.mem (γ := Set α)
      (⋂ (b : β),
        ⋂ (_ : Membership.mem (γ := Finset β) (Finset.image (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) T) b),
          Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅) b)
      a →
    Membership.mem (γ := Set α) (⋂ b ∈ T, f b) a

Tactic:
simp -proj only
          [Set.mem_iInter, Subtype.forall, Finset.set_biInter_finset_image]

Premises used: Finset.set_biInter_finset_image, Subtype.forall, Set.mem_iInter
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
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)
a : α
h1 :
  ∀ (a_1 : β) (b : a_1 ∈ s) (i : Subtype.mk (p := fun (a : β) ↦ a ∈ s) a_1 b ∈ T),
    a ∈
      Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅)
        (↑(Subtype.mk (p := fun (a : β) ↦ a ∈ s) a_1 b) : β)
b : β
h_b : s b
h_b_in_T : Subtype.mk (p := fun (a : β) ↦ s a) b h_b ∈ T
⊢ a ∈
    Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅)
      (↑(Subtype.mk (p := fun (a : β) ↦ a ∈ s) b h_b) : β)

Tactic:
have h2 := h1 b h_b h_b_in_T
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
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)
a : α
h1 :
  ∀ (a_1 : β) (b : a_1 ∈ s) (i : Subtype.mk (p := fun (a : β) ↦ a ∈ s) a_1 b ∈ T),
    a ∈
      Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅)
        (↑(Subtype.mk (p := fun (a : β) ↦ a ∈ s) a_1 b) : β)
b : β
h_b : s b
h_b_in_T : Subtype.mk (p := fun (a : β) ↦ s a) b h_b ∈ T
h2 :
  a ∈
    Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅)
      (↑(Subtype.mk (p := fun (a : β) ↦ a ∈ s) b h_b) : β)
refine_1 :
  ∀
    (h2 :
      a ∈
        Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅)
          (↑(Subtype.mk (p := fun (a : β) ↦ a ∈ s) b h_b) : β)),
    a ∈ f (Subtype.mk (p := fun (a : β) ↦ s a) b h_b)
⊢ a ∈ f (Subtype.mk (p := fun (a : β) ↦ s a) b h_b)

Tactic:
revert h2
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
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)
a : α
h1 :
  ∀ (a_1 : β) (b : a_1 ∈ s) (i : Subtype.mk (p := fun (a : β) ↦ a ∈ s) a_1 b ∈ T),
    a ∈
      Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅)
        (↑(Subtype.mk (p := fun (a : β) ↦ a ∈ s) a_1 b) : β)
b : β
h_b : s b
h_b_in_T : Subtype.mk (p := fun (a : β) ↦ s a) b h_b ∈ T
refine_1 :
  ∀ (h2 : a ∈ f (Subtype.mk (p := fun (a : β) ↦ a ∈ s) b h_b)), a ∈ f (Subtype.mk (p := fun (a : β) ↦ s a) b h_b)
⊢ ∀
    (h2 :
      a ∈
        Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅)
          (↑(Subtype.mk (p := fun (a : β) ↦ a ∈ s) b h_b) : β)),
    a ∈ f (Subtype.mk (p := fun (a : β) ↦ s a) b h_b)

Tactic:
rw [Subtype.val_injective.extend_apply]

Premises used: Subtype.val_injective, Function.Injective.extend_apply
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
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)
a : α
h1 :
  ∀ (a_1 : β) (b : a_1 ∈ s) (i : Subtype.mk (p := fun (a : β) ↦ a ∈ s) a_1 b ∈ T),
    a ∈
      Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅)
        (↑(Subtype.mk (p := fun (a : β) ↦ a ∈ s) a_1 b) : β)
b : β
h_b : s b
h_b_in_T : Subtype.mk (p := fun (a : β) ↦ s a) b h_b ∈ T
⊢ ∀ (h2 : a ∈ f (Subtype.mk (p := fun (a : β) ↦ a ∈ s) b h_b)), a ∈ f (Subtype.mk (p := fun (a : β) ↦ s a) b h_b)

Tactic:
apply id

Premises used: id
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
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)
b : β
h_b : Membership.mem (γ := Finset β) (Finset.image (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) T) b
⊢ ∃ (x : b ∈ s), Subtype.mk (p := fun (a : β) ↦ a ∈ s) b ⋯ ∈ T

Tactic:
simp_rw [Finset.mem_image, Subtype.exists, exists_and_right, exists_eq_right]
      at h_b

Premises used: Finset.mem_image, Subtype.exists, exists_eq_right, exists_and_right
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
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)
b : β
h_b : ∃ (x : b ∈ s), Subtype.mk (p := fun (a : β) ↦ a ∈ s) b ⋯ ∈ T
⊢ b ∈ s

Tactic:
obtain ⟨h_b_w, h_b_h⟩ := h_b
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
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)
b : β
h_b : ∃ (x : b ∈ s), Subtype.mk (p := fun (a : β) ↦ a ∈ s) b ⋯ ∈ T
h_b_w : b ∈ s
⊢ Subtype.mk (p := fun (a : β) ↦ a ∈ s) b ⋯ ∈ T

Tactic:
obtain ⟨h_b_w, h_b_h⟩ := h_b
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
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)
b : β
h_b_w : b ∈ s
h_b_h : Subtype.mk (p := fun (a : β) ↦ a ∈ s) b ⋯ ∈ T
⊢ b = (↑(Subtype.mk (p := Membership.mem s) b h_b_w) : β)

Tactic:
have h_b_alt : b = (Subtype.mk b h_b_w).val := rfl
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
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)
b : β
h_b_w : b ∈ s
h_b_h : Subtype.mk (p := fun (a : β) ↦ a ∈ s) b ⋯ ∈ T
h_b_alt : b = (↑(Subtype.mk (p := Membership.mem s) b h_b_w) : β)
refine_2 : f (Subtype.mk (p := Membership.mem s) b h_b_w) ∈ g (↑(Subtype.mk (p := Membership.mem s) b h_b_w) : β)
⊢ Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅) b ∈ g b

Tactic:
rw [h_b_alt, Subtype.val_injective.extend_apply]

Premises used: Subtype.val_injective, Function.Injective.extend_apply
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
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)
b : β
h_b_w : b ∈ s
h_b_h : Subtype.mk (p := fun (a : β) ↦ a ∈ s) b ⋯ ∈ T
h_b_alt : b = (↑(Subtype.mk (p := Membership.mem s) b h_b_w) : β)
refine_2 : Subtype.mk (p := Membership.mem s) b h_b_w ∈ T
⊢ f (Subtype.mk (p := Membership.mem s) b h_b_w) ∈ g (↑(Subtype.mk (p := Membership.mem s) b h_b_w) : β)

Tactic:
apply h_t'
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
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)
b : β
h_b_w : b ∈ s
h_b_h : Subtype.mk (p := fun (a : β) ↦ a ∈ s) b ⋯ ∈ T
h_b_alt : b = (↑(Subtype.mk (p := Membership.mem s) b h_b_w) : β)
⊢ Subtype.mk (p := Membership.mem s) b h_b_w ∈ T

Tactic:
apply h_b_h
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
h : ∀ (s : Set α), s ∈ piiUnionInter π {i} ↔ s ∈ π i ∪ {univ}
⊢ piiUnionInter π {i} = π i ∪ {univ}

Tactic:
ext1 s
-- Module: Mathlib.MeasureTheory.PiSystem
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
⊢ s ∈ piiUnionInter π {i} ↔ s ∈ π i ∪ {univ}

Tactic:
simp only [piiUnionInter, exists_prop, mem_union]

Premises used: Set.mem_union, piiUnionInter, exists_prop