awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
simp :
  (∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : (↑I : Type u_2) → Set α),
          (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i) ↔
    ∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : ι → Set α),
          (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ U = ⋂ (x : (↑I : Type u_2)), V (↑x : ι) ∧ U = ⋂ (i : ι), V i
simp₁ :
  (∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : (↑I : Type u_2) → Set α),
          (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i) →
    ∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : ι → Set α),
          (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ U = ⋂ (x : (↑I : Type u_2)), V (↑x : ι) ∧ U = ⋂ (i : ι), V i
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), s i) U ↔
    ∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : ι → Set α), (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ U = ⋂ i ∈ I, V i ∧ U = ⋂ (i : ι), V i
have simp₂ : ∀ (I : Set ι) (If : I.Finite) (V : (↑I : Type u_2) → Set α) (hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)),
  ∃ (I_1 : Set ι),
    I_1.Finite ∧
      ∃ (V_1 : ι → Set α),
        (∀ (i : ι), V_1 i ∈ s i) ∧
          (∀ i ∉ I_1, V_1 i = univ) ∧
            Eq.{u + 1} (α := Set α) (⋂ (i : (↑I : Type u_2)), V i) (⋂ (x : (↑I_1 : Type u_2)), V_1 (↑x : ι)) ∧
              Eq.{u + 1} (α := Set α) (⋂ (i : (↑I : Type u_2)), V i) (⋂ (i : ι), V_1 i)
Tactic: classical
  simp only [mem_iInf, biInter_eq_iInter]
  refine ⟨?_, fun ⟨I, If, V, hVs, _, hVU, _⟩ => ⟨I, If, fun i => V i, fun i => hVs i, hVU⟩⟩
  rintro ⟨I, If, V, hV, rfl⟩
  refine ⟨I, If, fun i => if hi : i ∈ I then V ⟨i, hi⟩ else univ, fun i => ?_, fun i hi => ?_, ?_⟩
  · dsimp only
    split_ifs
    exacts [hV ⟨i,_⟩, univ_mem]
  · exact dif_neg hi
  · simp only [iInter_dite, biInter_eq_iInter, dif_pos (Subtype.coe_prop _), Subtype.coe_eta,
      iInter_univ, inter_univ, true_and]
Cleared hypotheses: U
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
simp :
  (∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : (↑I : Type u_2) → Set α),
          (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i) ↔
    ∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : ι → Set α),
          (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ U = ⋂ (x : (↑I : Type u_2)), V (↑x : ι) ∧ U = ⋂ (i : ι), V i
simp₁ :
  (∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : (↑I : Type u_2) → Set α),
          (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i) →
    ∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : ι → Set α),
          (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ U = ⋂ (x : (↑I : Type u_2)), V (↑x : ι) ∧ U = ⋂ (i : ι), V i
simp₂ :
  ∀ (I : Set ι) (If : I.Finite) (V : (↑I : Type u_2) → Set α) (hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)),
    ∃ (I_1 : Set ι),
      I_1.Finite ∧
        ∃ (V_1 : ι → Set α),
          (∀ (i : ι), V_1 i ∈ s i) ∧
            (∀ i ∉ I_1, V_1 i = univ) ∧
              Eq.{u + 1} (α := Set α) (⋂ (i : (↑I : Type u_2)), V i) (⋂ (x : (↑I_1 : Type u_2)), V_1 (↑x : ι)) ∧
                Eq.{u + 1} (α := Set α) (⋂ (i : (↑I : Type u_2)), V i) (⋂ (i : ι), V_1 i)
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), s i) U ↔
    ∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : ι → Set α), (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ U = ⋂ i ∈ I, V i ∧ U = ⋂ (i : ι), V i
have refine_1 : ∀ (I : Set ι) (If : I.Finite) (V : (↑I : Type u_2) → Set α) (hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) (i : ι),
  (fun (i : ι) ↦ (if hi : i ∈ I then V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else univ : Set α)) i ∈ s i
Tactic: classical
  simp only [mem_iInf, biInter_eq_iInter]
  refine ⟨?_, fun ⟨I, If, V, hVs, _, hVU, _⟩ => ⟨I, If, fun i => V i, fun i => hVs i, hVU⟩⟩
  rintro ⟨I, If, V, hV, rfl⟩
  refine ⟨I, If, fun i => if hi : i ∈ I then V ⟨i, hi⟩ else univ, fun i => ?_, fun i hi => ?_, ?_⟩
  · dsimp only
    split_ifs
    exacts [hV ⟨i,_⟩, univ_mem]
  · exact dif_neg hi
  · simp only [iInter_dite, biInter_eq_iInter, dif_pos (Subtype.coe_prop _), Subtype.coe_eta,
      iInter_univ, inter_univ, true_and]
Cleared hypotheses: U
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
simp :
  (∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : (↑I : Type u_2) → Set α),
          (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i) ↔
    ∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : ι → Set α),
          (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ U = ⋂ (x : (↑I : Type u_2)), V (↑x : ι) ∧ U = ⋂ (i : ι), V i
simp₁ :
  (∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : (↑I : Type u_2) → Set α),
          (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i) →
    ∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : ι → Set α),
          (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ U = ⋂ (x : (↑I : Type u_2)), V (↑x : ι) ∧ U = ⋂ (i : ι), V i
simp₂ :
  ∀ (I : Set ι) (If : I.Finite) (V : (↑I : Type u_2) → Set α) (hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)),
    ∃ (I_1 : Set ι),
      I_1.Finite ∧
        ∃ (V_1 : ι → Set α),
          (∀ (i : ι), V_1 i ∈ s i) ∧
            (∀ i ∉ I_1, V_1 i = univ) ∧
              Eq.{u + 1} (α := Set α) (⋂ (i : (↑I : Type u_2)), V i) (⋂ (x : (↑I_1 : Type u_2)), V_1 (↑x : ι)) ∧
                Eq.{u + 1} (α := Set α) (⋂ (i : (↑I : Type u_2)), V i) (⋂ (i : ι), V_1 i)
refine_1 :
  ∀ (I : Set ι) (If : I.Finite) (V : (↑I : Type u_2) → Set α) (hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) (i : ι),
    (fun (i : ι) ↦ (if hi : i ∈ I then V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else univ : Set α)) i ∈ s i
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), s i) U ↔
    ∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : ι → Set α), (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ U = ⋂ i ∈ I, V i ∧ U = ⋂ (i : ι), V i
have refine_2 : ∀ (I : Set ι) (If : I.Finite) (V : (↑I : Type u_2) → Set α) (hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) (i : ι)
  (hi : i ∉ I),
  Eq.{u + 1} (α := Set α)
    ((fun (i : ι) ↦ (if hi : i ∈ I then V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else univ : Set α)) i) univ
Tactic: classical
  simp only [mem_iInf, biInter_eq_iInter]
  refine ⟨?_, fun ⟨I, If, V, hVs, _, hVU, _⟩ => ⟨I, If, fun i => V i, fun i => hVs i, hVU⟩⟩
  rintro ⟨I, If, V, hV, rfl⟩
  refine ⟨I, If, fun i => if hi : i ∈ I then V ⟨i, hi⟩ else univ, fun i => ?_, fun i hi => ?_, ?_⟩
  · dsimp only
    split_ifs
    exacts [hV ⟨i,_⟩, univ_mem]
  · exact dif_neg hi
  · simp only [iInter_dite, biInter_eq_iInter, dif_pos (Subtype.coe_prop _), Subtype.coe_eta,
      iInter_univ, inter_univ, true_and]
Cleared hypotheses: U
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
simp :
  (∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : (↑I : Type u_2) → Set α),
          (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i) ↔
    ∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : ι → Set α),
          (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ U = ⋂ (x : (↑I : Type u_2)), V (↑x : ι) ∧ U = ⋂ (i : ι), V i
simp₁ :
  (∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : (↑I : Type u_2) → Set α),
          (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i) →
    ∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : ι → Set α),
          (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ U = ⋂ (x : (↑I : Type u_2)), V (↑x : ι) ∧ U = ⋂ (i : ι), V i
simp₂ :
  ∀ (I : Set ι) (If : I.Finite) (V : (↑I : Type u_2) → Set α) (hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)),
    ∃ (I_1 : Set ι),
      I_1.Finite ∧
        ∃ (V_1 : ι → Set α),
          (∀ (i : ι), V_1 i ∈ s i) ∧
            (∀ i ∉ I_1, V_1 i = univ) ∧
              Eq.{u + 1} (α := Set α) (⋂ (i : (↑I : Type u_2)), V i) (⋂ (x : (↑I_1 : Type u_2)), V_1 (↑x : ι)) ∧
                Eq.{u + 1} (α := Set α) (⋂ (i : (↑I : Type u_2)), V i) (⋂ (i : ι), V_1 i)
refine_1 :
  ∀ (I : Set ι) (If : I.Finite) (V : (↑I : Type u_2) → Set α) (hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) (i : ι),
    (fun (i : ι) ↦ (if hi : i ∈ I then V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else univ : Set α)) i ∈ s i
refine_2 :
  ∀ (I : Set ι) (If : I.Finite) (V : (↑I : Type u_2) → Set α) (hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) (i : ι)
    (hi : i ∉ I),
    Eq.{u + 1} (α := Set α)
      ((fun (i : ι) ↦ (if hi : i ∈ I then V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else univ : Set α)) i) univ
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), s i) U ↔
    ∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : ι → Set α), (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ U = ⋂ i ∈ I, V i ∧ U = ⋂ (i : ι), V i
have refine_3 : ∀ (I : Set ι) (If : I.Finite) (V : (↑I : Type u_2) → Set α) (hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)),
  Eq.{u + 1} (α := Set α) (⋂ (i : (↑I : Type u_2)), V i)
      (⋂ (x : (↑I : Type u_2)),
        (fun (i : ι) ↦ (if hi : i ∈ I then V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else univ : Set α))
          (↑x : ι)) ∧
    Eq.{u + 1} (α := Set α) (⋂ (i : (↑I : Type u_2)), V i)
      (⋂ (i : ι),
        (fun (i : ι) ↦ (if hi : i ∈ I then V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else univ : Set α)) i)
Tactic: classical
  simp only [mem_iInf, biInter_eq_iInter]
  refine ⟨?_, fun ⟨I, If, V, hVs, _, hVU, _⟩ => ⟨I, If, fun i => V i, fun i => hVs i, hVU⟩⟩
  rintro ⟨I, If, V, hV, rfl⟩
  refine ⟨I, If, fun i => if hi : i ∈ I then V ⟨i, hi⟩ else univ, fun i => ?_, fun i hi => ?_, ?_⟩
  · dsimp only
    split_ifs
    exacts [hV ⟨i,_⟩, univ_mem]
  · exact dif_neg hi
  · simp only [iInter_dite, biInter_eq_iInter, dif_pos (Subtype.coe_prop _), Subtype.coe_eta,
      iInter_univ, inter_univ, true_and]
Cleared hypotheses: U
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (hypothesis)
Goal:
ι : Sort u_2
α : Type u_3
f : ι → Filter α
s : Set α
hs : Membership.mem (γ := Filter α) (⨅ (i : ι), f i) s
⊢ ∃ (t : ι → Set α), (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ (i : ι), t i
have hs₁ : Membership.mem (γ := Filter α) (⨅ (b : (↑(range f) : Type u_3)), (↑b : Filter α)) s
Tactic: rw [← iInf_range' (g := (·))] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
ι : Sort u_2
α : Type u_3
f : ι → Filter α
s : Set α
hs : Membership.mem (γ := Filter α) (⨅ (b : (↑(range f) : Type u_3)), (↑b : Filter α)) s
⊢ ∃ (t : ι → Set α), (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ (i : ι), t i
have let : ∀ (w : Set (↑(range f) : Type u_3)),
  w.Finite →
    ∀ (V : (↑(range f) : Type u_3) → Set α) (hVs : ∀ (i : (↑(range f) : Type u_3)), V i ∈ (↑i : Filter α)),
      (∀ i ∉ w, V i = univ) →
        s = ⋂ i ∈ w, V i →
          ∀ (hVU' : s = ⋂ (i : (↑(range f) : Type u_3)), V i),
            ∃ (t : ι → Set α), (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ (i : ι), t i
Tactic: let ⟨_, _, V, hVs, _, _, hVU'⟩ := mem_iInf'.1 hs
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
ι : Sort u_2
α : Type u_3
f : ι → Filter α
s : Set α
hs : Membership.mem (γ := Filter α) (⨅ (b : (↑(range f) : Type u_3)), (↑b : Filter α)) s
w : Set (↑(range f) : Type u_3)
left : w.Finite
V : (↑(range f) : Type u_3) → Set α
hVs : ∀ (i : (↑(range f) : Type u_3)), V i ∈ (↑i : Filter α)
left_1 : ∀ i ∉ w, V i = univ
left_2 : s = ⋂ i ∈ w, V i
hVU' : s = ⋂ (i : (↑(range f) : Type u_3)), V i
⊢ ∃ (t : ι → Set α), (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ (i : ι), t i
have right : s = ⋂ (i : ι), (V ∘ rangeFactorization f) i
Tactic: use V ∘ rangeFactorization f, fun i ↦ hVs (rangeFactorization f i)
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
ι : Sort u_2
α : Type u_3
f : ι → Filter α
s : Set α
hs : Membership.mem (γ := Filter α) (⨅ (b : (↑(range f) : Type u_3)), (↑b : Filter α)) s
w : Set (↑(range f) : Type u_3)
left : w.Finite
V : (↑(range f) : Type u_3) → Set α
hVs : ∀ (i : (↑(range f) : Type u_3)), V i ∈ (↑i : Filter α)
left_1 : ∀ i ∉ w, V i = univ
left_2 : s = ⋂ i ∈ w, V i
hVU' : s = ⋂ (i : (↑(range f) : Type u_3)), V i
⊢ s = ⋂ (i : ι), (V ∘ rangeFactorization f) i
have right : Eq.{u_3 + 1} (α := Set α) (⋂ (i : (↑(range f) : Type u_3)), V i) (⋂ (i : ι), (V ∘ rangeFactorization f) i)
Tactic: rw [hVU', ← rangeFactorization_surjective.iInter_comp, comp_def]
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
ι : Sort u_2
α : Type u_3
f : ι → Filter α
s : Set α
hs : Membership.mem (γ := Filter α) (⨅ (b : (↑(range f) : Type u_3)), (↑b : Filter α)) s
w : Set (↑(range f) : Type u_3)
left : w.Finite
V : (↑(range f) : Type u_3) → Set α
hVs : ∀ (i : (↑(range f) : Type u_3)), V i ∈ (↑i : Filter α)
left_1 : ∀ i ∉ w, V i = univ
left_2 : s = ⋂ i ∈ w, V i
hVU' : s = ⋂ (i : (↑(range f) : Type u_3)), V i
right : Eq.{u_3 + 1} (α := Set α) (⋂ (i : (↑(range f) : Type u_3)), V i) (⋂ (i : ι), (V ∘ rangeFactorization f) i)
⊢ s = ⋂ (i : ι), (V ∘ rangeFactorization f) i
have right₁ : Eq.{u_3 + 1} (α := Set α) (⋂ (x : ι), V (rangeFactorization f x)) (⋂ (i : ι), (V ∘ rangeFactorization f) i)
Tactic: rw [hVU', ← rangeFactorization_surjective.iInter_comp, comp_def]
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
ι : Sort u_2
α : Type u_3
f : ι → Filter α
s : Set α
hs : Membership.mem (γ := Filter α) (⨅ (b : (↑(range f) : Type u_3)), (↑b : Filter α)) s
w : Set (↑(range f) : Type u_3)
left : w.Finite
V : (↑(range f) : Type u_3) → Set α
hVs : ∀ (i : (↑(range f) : Type u_3)), V i ∈ (↑i : Filter α)
left_1 : ∀ i ∉ w, V i = univ
left_2 : s = ⋂ i ∈ w, V i
hVU' : s = ⋂ (i : (↑(range f) : Type u_3)), V i
right : Eq.{u_3 + 1} (α := Set α) (⋂ (i : (↑(range f) : Type u_3)), V i) (⋂ (i : ι), (V ∘ rangeFactorization f) i)
right₁ : Eq.{u_3 + 1} (α := Set α) (⋂ (x : ι), V (rangeFactorization f x)) (⋂ (i : ι), (V ∘ rangeFactorization f) i)
⊢ s = ⋂ (i : ι), (V ∘ rangeFactorization f) i
have right₂ : Eq.{u_3 + 1} (α := Set α) (⋂ (x : ι), V (rangeFactorization f x))
  (⋂ (i : ι), (fun (x : ι) ↦ V (rangeFactorization f x)) i)
Tactic: rw [hVU', ← rangeFactorization_surjective.iInter_comp, comp_def]
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
ι : Sort u_2
inst : Finite ι
α : Type u_3
f : ι → Filter α
s : Set α
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), f i) s ↔ ∃ (t : ι → Set α), (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ (i : ι), t i
have refine : (∃ (t : ι → Set α), (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ (i : ι), t i) → Membership.mem (γ := Filter α) (⨅ (i : ι), f i) s
Tactic: refine ⟨exists_iInter_of_mem_iInf, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
t : Set α
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), ⨅ (_ : p i), 𝓟 (s i)) t ↔
    ∃ (I : Set ι), I.Finite ∧ (∀ i ∈ I, p i) ∧ ⋂ i ∈ I, s i ⊆ t
have mp : Membership.mem (γ := Filter α) (⨅ (i : ι), ⨅ (_ : p i), 𝓟 (s i)) t →
  ∃ (I : Set ι), I.Finite ∧ (∀ i ∈ I, p i) ∧ ⋂ i ∈ I, s i ⊆ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
t : Set α
mp :
  Membership.mem (γ := Filter α) (⨅ (i : ι), ⨅ (_ : p i), 𝓟 (s i)) t →
    ∃ (I : Set ι), I.Finite ∧ (∀ i ∈ I, p i) ∧ ⋂ i ∈ I, s i ⊆ t
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), ⨅ (_ : p i), 𝓟 (s i)) t ↔
    ∃ (I : Set ι), I.Finite ∧ (∀ i ∈ I, p i) ∧ ⋂ i ∈ I, s i ⊆ t
have mpr : (∃ (I : Set ι), I.Finite ∧ (∀ i ∈ I, p i) ∧ ⋂ i ∈ I, s i ⊆ t) →
  Membership.mem (γ := Filter α) (⨅ (i : ι), ⨅ (_ : p i), 𝓟 (s i)) t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
t : Set α
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), ⨅ (_ : p i), 𝓟 (s i)) t →
    ∃ (I : Set ι), I.Finite ∧ (∀ i ∈ I, p i) ∧ ⋂ i ∈ I, s i ⊆ t
have mp : (∃ (I : Set ι),
    I.Finite ∧
      ∃ (V : (↑I : Type u_2) → Set α),
        (∀ (i : (↑I : Type u_2)),
            ∃ (t : p (↑i : ι) → Set α), (∀ (i_1 : p (↑i : ι)), s (↑i : ι) ⊆ t i_1) ∧ V i = ⋂ (i : p (↑i : ι)), t i) ∧
          t = ⋂ (i : (↑I : Type u_2)), V i) →
  ∃ (I : Set ι), I.Finite ∧ (∀ i ∈ I, p i) ∧ ⋂ i ∈ I, s i ⊆ t
Tactic: simp only [mem_iInf (ι := ι), mem_iInf_of_finite, mem_principal]
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
I : Set ι
hIf : I.Finite
V : (↑I : Type u_2) → Set α
hV₁ :
  ∀ (i : (↑I : Type u_2)),
    ∃ (t : p (↑i : ι) → Set α), (∀ (i_1 : p (↑i : ι)), s (↑i : ι) ⊆ t i_1) ∧ V i = ⋂ (i : p (↑i : ι)), t i
⊢ ∃ (I_1 : Set ι),
    I_1.Finite ∧ (∀ i ∈ I_1, p i) ∧ Subset.{u} (α := Set α) (⋂ i ∈ I_1, s i) (⋂ (i : (↑I : Type u_2)), V i)
have mp : ∀ (t : (i : (↑I : Type u_2)) → p (↑i : ι) → Set α)
  (ht₁ : ∀ (i : (↑I : Type u_2)) (i_1 : p (↑i : ι)), s (↑i : ι) ⊆ t i i_1)
  (ht₂ : ∀ (i : (↑I : Type u_2)), V i = ⋂ (i_1 : p (↑i : ι)), t i i_1),
  ∃ (I_1 : Set ι),
    I_1.Finite ∧ (∀ i ∈ I_1, p i) ∧ Subset.{u} (α := Set α) (⋂ i ∈ I_1, s i) (⋂ (i : (↑I : Type u_2)), V i)
Tactic: choose! t ht₁ ht₂ using hV₁
Cleared hypotheses: hV₁
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
I : Set ι
hIf : I.Finite
V : (↑I : Type u_2) → Set α
t : (i : (↑I : Type u_2)) → p (↑i : ι) → Set α
ht₁ : ∀ (i : (↑I : Type u_2)) (i_1 : p (↑i : ι)), s (↑i : ι) ⊆ t i i_1
ht₂ : ∀ (i : (↑I : Type u_2)), V i = ⋂ (i_1 : p (↑i : ι)), t i i_1
⊢ ∃ (I_1 : Set ι),
    I_1.Finite ∧ (∀ i ∈ I_1, p i) ∧ Subset.{u} (α := Set α) (⋂ i ∈ I_1, s i) (⋂ (i : (↑I : Type u_2)), V i)
have mp : Subset.{u} (α := Set α) (⋂ i ∈ I ∩ {i : ι | p i}, s i) (⋂ (i : (↑I : Type u_2)), V i)
Tactic: refine ⟨I ∩ {i | p i}, hIf.inter_of_left _, fun i ↦ And.right, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
I : Set ι
hIf : I.Finite
V : (↑I : Type u_2) → Set α
t : (i : (↑I : Type u_2)) → p (↑i : ι) → Set α
ht₁ : ∀ (i : (↑I : Type u_2)) (i_1 : p (↑i : ι)), s (↑i : ι) ⊆ t i i_1
ht₂ : ∀ (i : (↑I : Type u_2)), V i = ⋂ (i_1 : p (↑i : ι)), t i i_1
⊢ Subset.{u} (α := Set α) (⋂ i ∈ I ∩ {i : ι | p i}, s i) (⋂ (i : (↑I : Type u_2)), V i)
have mp : Subset.{u} (α := Set α) (⋂ (x : (↑I : Type u_2)), ⋂ (_ : p (↑x : ι)), s (↑x : ι))
  (⋂ (i : (↑I : Type u_2)), ⋂ (i_1 : p (↑i : ι)), t i i_1)
Tactic: simp only [mem_inter_iff, iInter_and, biInter_eq_iInter, ht₂, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (hypothesis)
Goal:
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
t : Set α
I : Set ι
hIf : I.Finite
hpI : ∀ i ∈ I, p i
hst : ⋂ i ∈ I, s i ⊆ t
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), ⨅ (_ : p i), 𝓟 (s i)) t
have hst₁ : ⋂ (x : (↑I : Type u_2)), s (↑x : ι) ⊆ t
Tactic: rw [biInter_eq_iInter] at hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
t : Set α
I : Set ι
hIf : I.Finite
hpI : ∀ i ∈ I, p i
hst : ⋂ (x : (↑I : Type u_2)), s (↑x : ι) ⊆ t
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), ⨅ (_ : p i), 𝓟 (s i)) t
have mpr : ∀ (i : (↑I : Type u_2)), Membership.mem (γ := Filter α) (⨅ (_ : p (↑i : ι)), 𝓟 (s (↑i : ι))) (s (↑i : ι))
Tactic: refine mem_iInf_of_iInter hIf (fun i ↦ ?_) hst
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (hypothesis)
Goal:
α : Type u
ι : Type u_2
inst : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
⊢ ∃ (s : ι → Set α), (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Disjoint on s)
have this : Pairwise fun (i j : ι) ↦
  ∃ (s : { s : Set α // s ∈ l i }) (t : { t : Set α // t ∈ l j }), Disjoint (↑s : Set α) (↑t : Set α)
Tactic: have : Pairwise fun i j => ∃ (s : {s // s ∈ l i}) (t : {t // t ∈ l j}), Disjoint s.1 t.1 := by
    simpa only [Pairwise, Function.onFun, Filter.disjoint_iff, exists_prop, Subtype.exists] using hd
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
inst : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
this :
  Pairwise fun (i j : ι) ↦
    ∃ (s : { s : Set α // s ∈ l i }) (t : { t : Set α // t ∈ l j }), Disjoint (↑s : Set α) (↑t : Set α)
⊢ ∃ (s : ι → Set α), (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Disjoint on s)
have choose! : ∀ (s : ⦃i j : ι⦄ → { s : Set α // s ∈ l i }) (t : ⦃i j : ι⦄ → { t : Set α // t ∈ l j })
  (hst : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint (↑(s (j := j)) : Set α) (↑(t (i := i)) : Set α)),
  ∃ (s : ι → Set α), (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Disjoint on s)
Tactic: choose! s t hst using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
inst : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
s : ⦃i j : ι⦄ → { s : Set α // s ∈ l i }
t : ⦃i j : ι⦄ → { t : Set α // t ∈ l j }
hst : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint (↑(s (j := j)) : Set α) (↑(t (i := i)) : Set α)
⊢ ∃ (s : ι → Set α), (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Disjoint on s)
have refine_1 : ∀ (i : ι), (fun (i : ι) ↦ (⋂ (j : ι), (↑(s (j := j)) : Set α) ∩ (↑(t (i := j)) : Set α) : Set α)) i ∈ l i
Tactic: refine ⟨fun i => ⋂ j, @s i j ∩ @t j i, fun i => ?_, fun i j hij => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
inst : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
s : ⦃i j : ι⦄ → { s : Set α // s ∈ l i }
t : ⦃i j : ι⦄ → { t : Set α // t ∈ l j }
hst : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint (↑(s (j := j)) : Set α) (↑(t (i := i)) : Set α)
refine_1 : ∀ (i : ι), (fun (i : ι) ↦ (⋂ (j : ι), (↑(s (j := j)) : Set α) ∩ (↑(t (i := j)) : Set α) : Set α)) i ∈ l i
⊢ ∃ (s : ι → Set α), (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Disjoint on s)
have refine_2 : ∀ (i j : ι) (hij : i ≠ j),
  onFun.{u_2 + 1, u + 1, 1} (β := Set α) Disjoint
    (fun (i : ι) ↦ ⋂ (j : ι), (↑(s (j := j)) : Set α) ∩ (↑(t (i := j)) : Set α)) i j
Tactic: refine ⟨fun i => ⋂ j, @s i j ∩ @t j i, fun i => ?_, fun i j hij => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (hypothesis)
Goal:
α : Type u
ι : Type u_2
l : ι → Filter α
t : Set ι
hd : t.PairwiseDisjoint l
ht : t.Finite
⊢ ∃ (s : ι → Set α), (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s
have this : Finite.{u_2 + 1} (↑t : Type u_2)
Tactic: haveI := ht.to_subtype
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
l : ι → Filter α
t : Set ι
hd : t.PairwiseDisjoint l
ht : t.Finite
this : Finite.{u_2 + 1} (↑t : Type u_2)
⊢ ∃ (s : ι → Set α), (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s
have rcases : ∀ (s : (↑t : Type u_2) → Set α) (hsl : ∀ (i : (↑t : Type u_2)), s i ∈ l (↑i : ι)) (hsd : Pairwise (Disjoint on s)),
  ∃ (s : ι → Set α), (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s
Tactic: rcases (hd.subtype _ _).exists_mem_filter_of_disjoint with ⟨s, hsl, hsd⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
l : ι → Filter α
t : Set ι
hd : t.PairwiseDisjoint l
ht : t.Finite
this : Finite.{u_2 + 1} (↑t : Type u_2)
s : (↑t : Type u_2) → Set α
hsl : ∀ (i : (↑t : Type u_2)), s i ∈ l (↑i : ι)
hsd : Pairwise (Disjoint on s)
⊢ ∃ (s : ι → Set α), (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s
have lift : ∀ (s : (i : (↑t : Type u_2)) → { s : Set α // s ∈ l (↑i : ι) })
  (hsd :
    Pairwise.{u_2} (α := (↑t : Type u_2))
      (onFun.{u_2 + 1, u + 1, 1} (β := Set α) Disjoint fun (i : (↑t : Type u_2)) ↦ (↑(s i) : Set α))),
  ∃ (s : ι → Set α), (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s
Tactic: lift s to (i : t) → {s // s ∈ l i} using hsl
Cleared hypotheses: s, hsl, hsd
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
l : ι → Filter α
t : Set ι
hd : t.PairwiseDisjoint l
ht : t.Finite
this : Finite.{u_2 + 1} (↑t : Type u_2)
s : (i : (↑t : Type u_2)) → { s : Set α // s ∈ l (↑i : ι) }
hsd :
  Pairwise.{u_2} (α := (↑t : Type u_2))
    (onFun.{u_2 + 1, u + 1, 1} (β := Set α) Disjoint fun (i : (↑t : Type u_2)) ↦ (↑(s i) : Set α))
⊢ ∃ (s : ι → Set α), (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s
have rcases : ∀ (s : (i : ι) → { s : Set α // s ∈ l i })
  (hsd :
    Pairwise.{u_2} (α := (↑t : Type u_2))
      (onFun.{u_2 + 1, u + 1, 1} (β := Set α) Disjoint fun (i : (↑t : Type u_2)) ↦
        (↑((fun (i : { x : ι // x ∈ t }) ↦ (s (↑i : ι) : { s : Set α // s ∈ l (↑i : ι) })) i) : Set α))),
  ∃ (s : ι → Set α), (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s
Tactic: rcases @Subtype.exists_pi_extension ι (fun i => { s // s ∈ l i }) _ _ s with ⟨s, rfl⟩
Cleared hypotheses: s, hsd