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 : 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
have 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)
Tactic: refine
    ⟨T.image (fun x : s => (x : β)),
      Function.extend (fun x : s => (x : β)) f fun _ : β => (∅ : Set α), by simp, ?_, ?_⟩
-- 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 : 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)
⊢ ∃ (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
have 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
Tactic: refine
    ⟨T.image (fun x : s => (x : β)),
      Function.extend (fun x : s => (x : β)) f fun _ : β => (∅ : Set α), by simp, ?_, ?_⟩
-- 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 : 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)
⊢ 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)
have 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
Tactic: ext a
-- 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 : 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 : α
⊢ 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
have 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
Tactic: constructor
-- 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 : 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
⊢ 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
have 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
Tactic: constructor
-- 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 : 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 : α
⊢ 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
have 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) : β)
Tactic: simp -proj only
          [Set.mem_iInter, Subtype.forall, Finset.set_biInter_finset_image]
-- 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 : 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 ∈
    Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅)
      (↑(Subtype.mk (p := fun (a : β) ↦ a ∈ s) b h_b) : β)
have h2 : a ∈ f (Subtype.mk (p := fun (a : β) ↦ s a) b h_b)
Tactic: have h2 := h1 b h_b h_b_in_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 : 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 ∈
    Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅)
      (↑(Subtype.mk (p := fun (a : β) ↦ a ∈ s) b h_b) : β)
have 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) : β)
Tactic: revert h2
Cleared hypotheses: h2
-- 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 : 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 ∈
      Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅)
        (↑(Subtype.mk (p := fun (a : β) ↦ a ∈ s) b h_b) : β)
have 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)
Tactic: rw [Subtype.val_injective.extend_apply]
-- 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 : 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 : α
⊢ 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
have 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)
Tactic: simp -proj only
          [Set.mem_iInter, Subtype.forall, Finset.set_biInter_finset_image]
-- 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 : 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 ∈ f (Subtype.mk (p := fun (a : β) ↦ s a) b h_b)
have h2 : 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
-- 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 : 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) : β)
⊢ a ∈ f (Subtype.mk (p := fun (a : β) ↦ s a) b h_b)
have 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)
Tactic: revert h2
Cleared hypotheses: h2
-- 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 : 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) : β)),
    a ∈ f (Subtype.mk (p := fun (a : β) ↦ s a) b h_b)
have 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)
Tactic: rw [Subtype.val_injective.extend_apply]
-- 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 : 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
⊢ Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅) b ∈ g b
have h_b₁ : ∃ (x : b ∈ s), Subtype.mk (p := fun (a : β) ↦ a ∈ s) b sorry ∈ T
Tactic: simp_rw [Finset.mem_image, Subtype.exists, exists_and_right, exists_eq_right]
      at h_b
Cleared hypotheses: h_b
-- 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 : 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
⊢ Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅) b ∈ g b
have h_b_w : b ∈ s
Tactic: obtain ⟨h_b_w, h_b_h⟩ := h_b
Cleared hypotheses: h_b
-- 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 : 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
⊢ Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅) b ∈ g b
have h_b_h : Subtype.mk (p := fun (a : β) ↦ a ∈ s) b sorry ∈ T
Tactic: obtain ⟨h_b_w, h_b_h⟩ := h_b
Cleared hypotheses: h_b
-- 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 : 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
⊢ Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅) b ∈ g b
have h_b_alt : 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
-- 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 : 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) : β)
⊢ Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅) b ∈ g b
have refine_2 : f (Subtype.mk (p := Membership.mem s) b h_b_w) ∈ g (↑(Subtype.mk (p := Membership.mem s) b h_b_w) : β)
Tactic: rw [h_b_alt, Subtype.val_injective.extend_apply]
-- 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 : 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) : β)
⊢ f (Subtype.mk (p := Membership.mem s) b h_b_w) ∈ g (↑(Subtype.mk (p := Membership.mem s) b h_b_w) : β)
have refine_2 : Subtype.mk (p := Membership.mem s) b h_b_w ∈ T
Tactic: apply 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
⊢ ∃ (T : Finset β) (f : β → Set α), (↑T : Set β) ⊆ s ∧ t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
have have : Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val (p := s)) b)) t
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
-- 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
⊢ ∃ (T : Finset β) (f : β → Set α), (↑T : Set β) ⊆ s ∧ t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
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
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