case intro.intro.intro
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
⊢ ∃ T_1 f_1,
    ↑T_1 ⊆ s ∧
      ((⋂ (b : Subtype s) (_ : b ∈ T), f b) = ⋂ (b : β) (_ : b ∈ T_1), f_1 b) ∧ ∀ (b : β), b ∈ T_1 → f_1 b ∈ g b
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
t : Set α
h_t : t ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : t ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
⊢ ∃ T f, ↑T ⊆ s ∧ (t = ⋂ (b : β) (_ : b ∈ T), f b) ∧ ∀ (b : β), b ∈ T → f b ∈ g b
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'⟩⟩⟩
case intro.intro.intro.refine'_1
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
⊢ (⋂ (b : Subtype s) (_ : b ∈ T), f b) =
    ⋂ (b : β) (_ : b ∈ Finset.image (fun x => ↑x) T), Function.extend (fun x => ↑x) f (fun x => ∅) b

case intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
⊢ ∀ (b : β), b ∈ Finset.image (fun x => ↑x) T → Function.extend (fun x => ↑x) f (fun x => ∅) b ∈ g b
case intro.intro.intro
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
⊢ ∃ T_1 f_1,
    ↑T_1 ⊆ s ∧
      ((⋂ (b : Subtype s) (_ : b ∈ T), f b) = ⋂ (b : β) (_ : b ∈ T_1), f_1 b) ∧ ∀ (b : β), b ∈ T_1 → f_1 b ∈ g b
refine'
  ⟨T.image (fun x : s => (x : β)),
    Function.extend (fun x : s => (x : β)) f fun _ : β => (∅ : Set α), by simp, _, _⟩
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
t : Set α
h_t : t ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
h1 : (⋃ (b : Subtype s), (g ∘ Subtype.val) b) = ⋃ (b : β) (_ : b ∈ s), g b
⊢ t ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)

case h1
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
t : Set α
h_t : t ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
⊢ (⋃ (b : Subtype s), (g ∘ Subtype.val) b) = ⋃ (b : β) (_ : b ∈ s), g b
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
t : Set α
h_t : t ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
⊢ t ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
suffices h1 : (⋃ b : Subtype s, (g ∘ Subtype.val) b) = ⋃ b ∈ s, g b
case h1.h
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
t : Set α
h_t : t ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
x : Set α
⊢ (x ∈ ⋃ (b : Subtype s), (g ∘ Subtype.val) b) ↔ x ∈ ⋃ (b : β) (_ : b ∈ s), g b
case h1
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
t : Set α
h_t : t ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
⊢ (⋃ (b : Subtype s), (g ∘ Subtype.val) b) = ⋃ (b : β) (_ : b ∈ s), g b
ext x
case h1.h
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
t : Set α
h_t : t ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
x : Set α
⊢ (∃ a, s a ∧ x ∈ g a) ↔ ∃ i, i ∈ s ∧ x ∈ g i
case h1.h
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
t : Set α
h_t : t ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
x : Set α
⊢ (x ∈ ⋃ (b : Subtype s), (g ∘ Subtype.val) b) ↔ x ∈ ⋃ (b : β) (_ : b ∈ s), g b
simp only [exists_prop, Set.mem_iUnion, Function.comp_apply, Subtype.exists, Subtype.coe_mk]
no goals
case h1.h
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
t : Set α
h_t : t ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
x : Set α
⊢ (∃ a, s a ∧ x ∈ g a) ↔ ∃ i, i ∈ s ∧ x ∈ g i
rfl
no goals
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
t : Set α
h_t : t ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
h1 : (⋃ (b : Subtype s), (g ∘ Subtype.val) b) = ⋃ (b : β) (_ : b ∈ s), g b
⊢ t ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
rwa [h1]
no goals
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
⊢ ↑(Finset.image (fun x => ↑x) T) ⊆ s
simp
case intro.intro.intro.refine'_1.h
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
a : α
⊢ (a ∈ ⋂ (b : Subtype s) (_ : b ∈ T), f b) ↔
    a ∈ ⋂ (b : β) (_ : b ∈ Finset.image (fun x => ↑x) T), Function.extend (fun x => ↑x) f (fun x => ∅) b
case intro.intro.intro.refine'_1
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
⊢ (⋂ (b : Subtype s) (_ : b ∈ T), f b) =
    ⋂ (b : β) (_ : b ∈ Finset.image (fun x => ↑x) T), Function.extend (fun x => ↑x) f (fun x => ∅) b
ext a
case intro.intro.intro.refine'_1.h.mpr
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
a : α
⊢ (∀ (a_1 : β) (b : a_1 ∈ s),
      { val := a_1, property := b } ∈ T →
        a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑{ val := a_1, property := b }) →
    ∀ (a_2 : β) (b : s a_2), { val := a_2, property := b } ∈ T → a ∈ f { val := a_2, property := b }
case intro.intro.intro.refine'_1.h.mpr
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
a : α
⊢ (a ∈ ⋂ (b : β) (_ : b ∈ Finset.image (fun x => ↑x) T), Function.extend (fun x => ↑x) f (fun x => ∅) b) →
    a ∈ ⋂ (b : Subtype s) (_ : b ∈ T), f b
simp (config := { proj := false }) only
  [Set.mem_iInter, Subtype.forall, Finset.set_biInter_finset_image]
case intro.intro.intro.refine'_1.h.mpr
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
a : α
h1 :
  ∀ (a_1 : β) (b : a_1 ∈ s),
    { val := a_1, property := b } ∈ T → a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑{ val := a_1, property := b }
b : β
h_b : s b
h_b_in_T : { val := b, property := h_b } ∈ T
⊢ a ∈ f { val := b, property := h_b }
case intro.intro.intro.refine'_1.h.mpr
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
a : α
⊢ (∀ (a_1 : β) (b : a_1 ∈ s),
      { val := a_1, property := b } ∈ T →
        a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑{ val := a_1, property := b }) →
    ∀ (a_2 : β) (b : s a_2), { val := a_2, property := b } ∈ T → a ∈ f { val := a_2, property := b }
intro h1 b h_b h_b_in_T
case intro.intro.intro.refine'_1.h.mpr
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
a : α
h1 :
  ∀ (a_1 : β) (b : a_1 ∈ s),
    { val := a_1, property := b } ∈ T → a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑{ val := a_1, property := b }
b : β
h_b : s b
h_b_in_T : { val := b, property := h_b } ∈ T
h2 : a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑{ val := b, property := h_b }
⊢ a ∈ f { val := b, property := h_b }
case intro.intro.intro.refine'_1.h.mpr
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
a : α
h1 :
  ∀ (a_1 : β) (b : a_1 ∈ s),
    { val := a_1, property := b } ∈ T → a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑{ val := a_1, property := b }
b : β
h_b : s b
h_b_in_T : { val := b, property := h_b } ∈ T
⊢ a ∈ f { val := b, property := h_b }
have h2 := h1 b h_b h_b_in_T
case intro.intro.intro.refine'_1.h.mpr
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
a : α
h1 :
  ∀ (a_1 : β) (b : a_1 ∈ s),
    { val := a_1, property := b } ∈ T → a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑{ val := a_1, property := b }
b : β
h_b : s b
h_b_in_T : { val := b, property := h_b } ∈ T
⊢ a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑{ val := b, property := h_b } → a ∈ f { val := b, property := h_b }
case intro.intro.intro.refine'_1.h.mpr
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
a : α
h1 :
  ∀ (a_1 : β) (b : a_1 ∈ s),
    { val := a_1, property := b } ∈ T → a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑{ val := a_1, property := b }
b : β
h_b : s b
h_b_in_T : { val := b, property := h_b } ∈ T
h2 : a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑{ val := b, property := h_b }
⊢ a ∈ f { val := b, property := h_b }
revert h2
case intro.intro.intro.refine'_1.h.mpr
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
a : α
h1 :
  ∀ (a_1 : β) (b : a_1 ∈ s),
    { val := a_1, property := b } ∈ T → a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑{ val := a_1, property := b }
b : β
h_b : s b
h_b_in_T : { val := b, property := h_b } ∈ T
⊢ a ∈ f { val := b, property := h_b } → a ∈ f { val := b, property := h_b }
case intro.intro.intro.refine'_1.h.mpr
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
a : α
h1 :
  ∀ (a_1 : β) (b : a_1 ∈ s),
    { val := a_1, property := b } ∈ T → a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑{ val := a_1, property := b }
b : β
h_b : s b
h_b_in_T : { val := b, property := h_b } ∈ T
⊢ a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑{ val := b, property := h_b } → a ∈ f { val := b, property := h_b }
rw [Subtype.val_injective.extend_apply]
no goals
case intro.intro.intro.refine'_1.h.mpr
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
a : α
h1 :
  ∀ (a_1 : β) (b : a_1 ∈ s),
    { val := a_1, property := b } ∈ T → a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑{ val := a_1, property := b }
b : β
h_b : s b
h_b_in_T : { val := b, property := h_b } ∈ T
⊢ a ∈ f { val := b, property := h_b } → a ∈ f { val := b, property := h_b }
apply id
case intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
b : β
h_b : b ∈ Finset.image (fun x => ↑x) T
⊢ Function.extend (fun x => ↑x) f (fun x => ∅) b ∈ g b
case intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
⊢ ∀ (b : β), b ∈ Finset.image (fun x => ↑x) T → Function.extend (fun x => ↑x) f (fun x => ∅) b ∈ g b
intros b h_b
case intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
b : β
h_b : ∃ x, { val := b, property := (_ : b ∈ s) } ∈ T
⊢ Function.extend (fun x => ↑x) f (fun x => ∅) b ∈ g b
case intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
b : β
h_b : b ∈ Finset.image (fun x => ↑x) T
⊢ Function.extend (fun x => ↑x) f (fun x => ∅) b ∈ g b
simp_rw [Finset.mem_image, Subtype.exists, exists_and_right, exists_eq_right]
  at h_b
case intro.intro.intro.refine'_2.intro
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
b : β
h_b_w : b ∈ s
h_b_h : { val := b, property := (_ : b ∈ s) } ∈ T
⊢ Function.extend (fun x => ↑x) f (fun x => ∅) b ∈ g b
case intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
b : β
h_b : ∃ x, { val := b, property := (_ : b ∈ s) } ∈ T
⊢ Function.extend (fun x => ↑x) f (fun x => ∅) b ∈ g b
cases' h_b with h_b_w h_b_h
case intro.intro.intro.refine'_2.intro
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
b : β
h_b_w : b ∈ s
h_b_h : { val := b, property := (_ : b ∈ s) } ∈ T
h_b_alt : b = ↑{ val := b, property := h_b_w }
⊢ Function.extend (fun x => ↑x) f (fun x => ∅) b ∈ g b
case intro.intro.intro.refine'_2.intro
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
b : β
h_b_w : b ∈ s
h_b_h : { val := b, property := (_ : b ∈ s) } ∈ T
⊢ Function.extend (fun x => ↑x) f (fun x => ∅) b ∈ g b
have h_b_alt : b = (Subtype.mk b h_b_w).val := rfl
case intro.intro.intro.refine'_2.intro
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
b : β
h_b_w : b ∈ s
h_b_h : { val := b, property := (_ : b ∈ s) } ∈ T
h_b_alt : b = ↑{ val := b, property := h_b_w }
⊢ f { val := b, property := h_b_w } ∈ g ↑{ val := b, property := h_b_w }
case intro.intro.intro.refine'_2.intro
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
b : β
h_b_w : b ∈ s
h_b_h : { val := b, property := (_ : b ∈ s) } ∈ T
h_b_alt : b = ↑{ val := b, property := h_b_w }
⊢ Function.extend (fun x => ↑x) f (fun x => ∅) b ∈ g b
rw [h_b_alt, Subtype.val_injective.extend_apply]
case intro.intro.intro.refine'_2.intro.a
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
b : β
h_b_w : b ∈ s
h_b_h : { val := b, property := (_ : b ∈ s) } ∈ T
h_b_alt : b = ↑{ val := b, property := h_b_w }
⊢ { val := b, property := h_b_w } ∈ T
case intro.intro.intro.refine'_2.intro
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
b : β
h_b_w : b ∈ s
h_b_h : { val := b, property := (_ : b ∈ s) } ∈ T
h_b_alt : b = ↑{ val := b, property := h_b_w }
⊢ f { val := b, property := h_b_w } ∈ g ↑{ val := b, property := h_b_w }
apply h_t'
no goals
case intro.intro.intro.refine'_2.intro.a
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : (⋂ (b : Subtype s) (_ : b ∈ T), f b) ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
b : β
h_b_w : b ∈ s
h_b_h : { val := b, property := (_ : b ∈ s) } ∈ T
h_b_alt : b = ↑{ val := b, property := h_b_w }
⊢ { val := b, property := h_b_w } ∈ T
apply h_b_h