awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
mp :
  s ∈ pi (α := α) f →
    ∃ (I : Set ι), I.Finite ∧ ∃ (t : (i : ι) → Set (α i)), (∀ (i : ι), t i ∈ f i) ∧ I.pi (α := α) t ⊆ s
⊢ s ∈ pi (α := α) f ↔
    ∃ (I : Set ι), I.Finite ∧ ∃ (t : (i : ι) → Set (α i)), (∀ (i : ι), t i ∈ f i) ∧ I.pi (α := α) t ⊆ s
have mpr : (∃ (I : Set ι), I.Finite ∧ ∃ (t : (i : ι) → Set (α i)), (∀ (i : ι), t i ∈ f i) ∧ I.pi (α := α) t ⊆ s) →
  s ∈ pi (α := α) f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
⊢ s ∈ pi (α := α) f →
    ∃ (I : Set ι), I.Finite ∧ ∃ (t : (i : ι) → Set (α i)), (∀ (i : ι), t i ∈ f i) ∧ I.pi (α := α) t ⊆ s
have mp : (∃ (I : Set ι),
    I.Finite ∧
      ∃ (V : ι → Set ((i : ι) → α i)),
        (∀ (i : ι), ∃ t ∈ f i, eval (β := α) i ⁻¹' t ⊆ V i) ∧
          (∀ i ∉ I, V i = univ) ∧ s = ⋂ i ∈ I, V i ∧ s = ⋂ (i : ι), V i) →
  ∃ (I : Set ι), I.Finite ∧ ∃ (t : (i : ι) → Set (α i)), (∀ (i : ι), t i ∈ f i) ∧ ⋂ a ∈ I, eval (β := α) a ⁻¹' t a ⊆ s
Tactic: simp only [pi, mem_iInf', mem_comap, pi_def]
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
I : Set ι
If : I.Finite
V : ι → Set ((i : ι) → α i)
hVf : ∀ (i : ι), ∃ t ∈ f i, eval (β := α) i ⁻¹' t ⊆ V i
⊢ ∃ (I_1 : Set ι),
    I_1.Finite ∧
      ∃ (t : (i : ι) → Set (α i)),
        (∀ (i : ι), t i ∈ f i) ∧ Subset (α := Set ((i : ι) → α i)) (⋂ a ∈ I_1, eval (β := α) a ⁻¹' t a) (⋂ i ∈ I, V i)
have mp : ∀ (t : (i : ι) → Set (α i)) (htf : ∀ (i : ι), t i ∈ f i) (htV : ∀ (i : ι), eval (β := α) i ⁻¹' t i ⊆ V i),
  ∃ (I_1 : Set ι),
    I_1.Finite ∧
      ∃ (t : (i : ι) → Set (α i)),
        (∀ (i : ι), t i ∈ f i) ∧ Subset (α := Set ((i : ι) → α i)) (⋂ a ∈ I_1, eval (β := α) a ⁻¹' t a) (⋂ i ∈ I, V i)
Tactic: choose t htf htV using hVf
Cleared hypotheses: hVf
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst : ∀ (i : ι), (f i).NeBot
I : Set ι
h : I.pi (α := α) s ∈ pi (α := α) f
i : ι
hi : i ∈ I
⊢ s i ∈ f i
have rcases : ∀ (I' : Set ι) (t : (i : ι) → Set (α i)) (htf : ∀ (i : ι), t i ∈ f i) (hts : I'.pi (α := α) t ⊆ I.pi (α := α) s),
  s i ∈ f i
Tactic: rcases mem_pi.1 h with ⟨I', -, t, htf, hts⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst : ∀ (i : ι), (f i).NeBot
I : Set ι
h : I.pi (α := α) s ∈ pi (α := α) f
i : ι
hi : i ∈ I
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : I'.pi (α := α) t ⊆ I.pi (α := α) s
⊢ s i ∈ f i
have refine : ∀ (x : α i) (hx : x ∈ t i), x ∈ s i
Tactic: refine mem_of_superset (htf i) fun x hx => ?_
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst : ∀ (i : ι), (f i).NeBot
I : Set ι
h : I.pi (α := α) s ∈ pi (α := α) f
i : ι
hi : i ∈ I
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : I'.pi (α := α) t ⊆ I.pi (α := α) s
x : α i
hx : x ∈ t i
⊢ x ∈ s i
have this : ∀ (i : ι), (t i).Nonempty
Tactic: have : ∀ i, (t i).Nonempty := fun i => nonempty_of_mem (htf i)
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst : ∀ (i : ι), (f i).NeBot
I : Set ι
h : I.pi (α := α) s ∈ pi (α := α) f
i : ι
hi : i ∈ I
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : I'.pi (α := α) t ⊆ I.pi (α := α) s
x : α i
hx : x ∈ t i
this : ∀ (i : ι), (t i).Nonempty
⊢ x ∈ s i
have choose : ∀ (g : (i : ι) → α i) (hg : ∀ (i : ι), g i ∈ t i), x ∈ s i
Tactic: choose g hg using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst : ∀ (i : ι), (f i).NeBot
I : Set ι
h : I.pi (α := α) s ∈ pi (α := α) f
i : ι
hi : i ∈ I
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : I'.pi (α := α) t ⊆ I.pi (α := α) s
x : α i
hx : x ∈ t i
g : (i : ι) → α i
hg : ∀ (i : ι), g i ∈ t i
j : ι
h_1 : j ∈ I'
⊢ update (β := α) g i x j ∈ t j
have inl : ∀ (hi : j ∈ I) (x : α j) (hx : x ∈ t j), update (β := α) g j x j ∈ t j
Tactic: rcases eq_or_ne j i with (rfl | hne)
Cleared hypotheses: i, hi, x, hx
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst : ∀ (i : ι), (f i).NeBot
I : Set ι
h : I.pi (α := α) s ∈ pi (α := α) f
i : ι
hi : i ∈ I
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : I'.pi (α := α) t ⊆ I.pi (α := α) s
x : α i
hx : x ∈ t i
g : (i : ι) → α i
hg : ∀ (i : ι), g i ∈ t i
j : ι
h_1 : j ∈ I'
inl : ∀ (hi : j ∈ I) (x : α j) (hx : x ∈ t j), update (β := α) g j x j ∈ t j
⊢ update (β := α) g i x j ∈ t j
have inr : ∀ (hne : j ≠ i), update (β := α) g i x j ∈ t j
Tactic: rcases eq_or_ne j i with (rfl | hne)
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst : ∀ (i : ι), (f i).NeBot
I : Set ι
h : I.pi (α := α) s ∈ pi (α := α) f
i : ι
hi : i ∈ I
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : I'.pi (α := α) t ⊆ I.pi (α := α) s
x : α i
hx : x ∈ t i
g : (i : ι) → α i
hg : ∀ (i : ι), g i ∈ t i
⊢ x ∈ s i
have this : update (β := α) g i x ∈ I'.pi (α := α) t
Tactic: have : update g i x ∈ I'.pi t := fun j _ => by
    rcases eq_or_ne j i with (rfl | hne) <;> simp [*]
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst : ∀ (i : ι), (f i).NeBot
I : Set ι
h : I.pi (α := α) s ∈ pi (α := α) f
i : ι
hi : i ∈ I
⊢ s i ∈ f i
have rcases : ∀ (I' : Set ι) (t : (i : ι) → Set (α i)) (htf : ∀ (i : ι), t i ∈ f i) (hts : I'.pi (α := α) t ⊆ I.pi (α := α) s),
  s i ∈ f i
Tactic: classical
  rcases mem_pi.1 h with ⟨I', -, t, htf, hts⟩
  refine mem_of_superset (htf i) fun x hx => ?_
  have : ∀ i, (t i).Nonempty := fun i => nonempty_of_mem (htf i)
  choose g hg using this
  have : update g i x ∈ I'.pi t := fun j _ => by
    rcases eq_or_ne j i with (rfl | hne) <;> simp [*]
  simpa using hts this i hi
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst : ∀ (i : ι), (f i).NeBot
I : Set ι
h : I.pi (α := α) s ∈ pi (α := α) f
i : ι
hi : i ∈ I
rcases :
  ∀ (I' : Set ι) (t : (i : ι) → Set (α i)) (htf : ∀ (i : ι), t i ∈ f i) (hts : I'.pi (α := α) t ⊆ I.pi (α := α) s),
    s i ∈ f i
⊢ s i ∈ f i
have rcases₁ : ∀ (I' : Set ι) (t : (i : ι) → Set (α i)) (htf : ∀ (i : ι), t i ∈ f i) (hts : I'.pi (α := α) t ⊆ I.pi (α := α) s)
  (x : α i) (hx : x ∈ t i), x ∈ s i
Tactic: classical
  rcases mem_pi.1 h with ⟨I', -, t, htf, hts⟩
  refine mem_of_superset (htf i) fun x hx => ?_
  have : ∀ i, (t i).Nonempty := fun i => nonempty_of_mem (htf i)
  choose g hg using this
  have : update g i x ∈ I'.pi t := fun j _ => by
    rcases eq_or_ne j i with (rfl | hne) <;> simp [*]
  simpa using hts this i hi
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst : ∀ (i : ι), (f i).NeBot
I : Set ι
h : I.pi (α := α) s ∈ pi (α := α) f
i : ι
hi : i ∈ I
rcases :
  ∀ (I' : Set ι) (t : (i : ι) → Set (α i)) (htf : ∀ (i : ι), t i ∈ f i) (hts : I'.pi (α := α) t ⊆ I.pi (α := α) s),
    s i ∈ f i
rcases₁ :
  ∀ (I' : Set ι) (t : (i : ι) → Set (α i)) (htf : ∀ (i : ι), t i ∈ f i) (hts : I'.pi (α := α) t ⊆ I.pi (α := α) s)
    (x : α i) (hx : x ∈ t i), x ∈ s i
⊢ s i ∈ f i
have rcases₂ : ∀ (I' : Set ι) (t : (i : ι) → Set (α i)) (htf : ∀ (i : ι), t i ∈ f i) (hts : I'.pi (α := α) t ⊆ I.pi (α := α) s)
  (x : α i) (hx : x ∈ t i) (this : ∀ (i : ι), (t i).Nonempty), x ∈ s i
Tactic: classical
  rcases mem_pi.1 h with ⟨I', -, t, htf, hts⟩
  refine mem_of_superset (htf i) fun x hx => ?_
  have : ∀ i, (t i).Nonempty := fun i => nonempty_of_mem (htf i)
  choose g hg using this
  have : update g i x ∈ I'.pi t := fun j _ => by
    rcases eq_or_ne j i with (rfl | hne) <;> simp [*]
  simpa using hts this i hi
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst : ∀ (i : ι), (f i).NeBot
I : Set ι
h : I.pi (α := α) s ∈ pi (α := α) f
i : ι
hi : i ∈ I
rcases :
  ∀ (I' : Set ι) (t : (i : ι) → Set (α i)) (htf : ∀ (i : ι), t i ∈ f i) (hts : I'.pi (α := α) t ⊆ I.pi (α := α) s),
    s i ∈ f i
rcases₁ :
  ∀ (I' : Set ι) (t : (i : ι) → Set (α i)) (htf : ∀ (i : ι), t i ∈ f i) (hts : I'.pi (α := α) t ⊆ I.pi (α := α) s)
    (x : α i) (hx : x ∈ t i), x ∈ s i
rcases₂ :
  ∀ (I' : Set ι) (t : (i : ι) → Set (α i)) (htf : ∀ (i : ι), t i ∈ f i) (hts : I'.pi (α := α) t ⊆ I.pi (α := α) s)
    (x : α i) (hx : x ∈ t i) (this : ∀ (i : ι), (t i).Nonempty), x ∈ s i
⊢ s i ∈ f i
have rcases₃ : ∀ (I' : Set ι) (t : (i : ι) → Set (α i)) (htf : ∀ (i : ι), t i ∈ f i) (hts : I'.pi (α := α) t ⊆ I.pi (α := α) s)
  (x : α i) (hx : x ∈ t i) (g : (i : ι) → α i) (hg : ∀ (i : ι), g i ∈ t i), x ∈ s i
Tactic: classical
  rcases mem_pi.1 h with ⟨I', -, t, htf, hts⟩
  refine mem_of_superset (htf i) fun x hx => ?_
  have : ∀ i, (t i).Nonempty := fun i => nonempty_of_mem (htf i)
  choose g hg using this
  have : update g i x ∈ I'.pi t := fun j _ => by
    rcases eq_or_ne j i with (rfl | hne) <;> simp [*]
  simpa using hts this i hi
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst : ∀ (i : ι), (f i).NeBot
I : Set ι
h : I.pi (α := α) s ∈ pi (α := α) f
i : ι
hi : i ∈ I
rcases :
  ∀ (I' : Set ι) (t : (i : ι) → Set (α i)) (htf : ∀ (i : ι), t i ∈ f i) (hts : I'.pi (α := α) t ⊆ I.pi (α := α) s),
    s i ∈ f i
rcases₁ :
  ∀ (I' : Set ι) (t : (i : ι) → Set (α i)) (htf : ∀ (i : ι), t i ∈ f i) (hts : I'.pi (α := α) t ⊆ I.pi (α := α) s)
    (x : α i) (hx : x ∈ t i), x ∈ s i
rcases₂ :
  ∀ (I' : Set ι) (t : (i : ι) → Set (α i)) (htf : ∀ (i : ι), t i ∈ f i) (hts : I'.pi (α := α) t ⊆ I.pi (α := α) s)
    (x : α i) (hx : x ∈ t i) (this : ∀ (i : ι), (t i).Nonempty), x ∈ s i
rcases₃ :
  ∀ (I' : Set ι) (t : (i : ι) → Set (α i)) (htf : ∀ (i : ι), t i ∈ f i) (hts : I'.pi (α := α) t ⊆ I.pi (α := α) s)
    (x : α i) (hx : x ∈ t i) (g : (i : ι) → α i) (hg : ∀ (i : ι), g i ∈ t i), x ∈ s i
⊢ s i ∈ f i
have rcases₄ : ∀ (I' : Set ι) (t : (i : ι) → Set (α i)) (htf : ∀ (i : ι), t i ∈ f i) (hts : I'.pi (α := α) t ⊆ I.pi (α := α) s)
  (x : α i) (hx : x ∈ t i) (g : (i : ι) → α i) (hg : ∀ (i : ι), g i ∈ t i)
  (this : update (β := α) g i x ∈ I'.pi (α := α) t), x ∈ s i
Tactic: classical
  rcases mem_pi.1 h with ⟨I', -, t, htf, hts⟩
  refine mem_of_superset (htf i) fun x hx => ?_
  have : ∀ i, (t i).Nonempty := fun i => nonempty_of_mem (htf i)
  choose g hg using this
  have : update g i x ∈ I'.pi t := fun j _ => by
    rcases eq_or_ne j i with (rfl | hne) <;> simp [*]
  simpa using hts this i hi
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
κ : Type u_3
p : κ → Prop
s : (i : ι) → κ → Set (α i)
h : ∀ (i : ι), (f i).HasBasis p (s i)
h_dir : ∀ (I : Set ι) (k : ι → κ), I.Finite → (∀ i ∈ I, p (k i)) → ∃ (k₀ : κ), p k₀ ∧ ∀ i ∈ I, s i k₀ ⊆ s i (k i)
⊢ (pi (α := α) f).HasBasis (fun (Ik : Prod.{u_1, u_3} (Set ι) κ) ↦ Ik.1.Finite ∧ p Ik.2)
    fun (Ik : Prod.{u_1, u_3} (Set ι) κ) ↦ Ik.1.pi (α := α) fun (i : ι) ↦ s i Ik.2
have refine_1 : ∀ (i : Set ι × ((i : ι) → κ)),
  (i.1.Finite ∧ ∀ i_1 ∈ i.1, p (i.2 i_1)) →
    ∃ (i' : Prod.{u_1, u_3} (Set ι) κ),
      (i'.1.Finite ∧ p i'.2) ∧
        Subset (α := Set ((i : ι) → α i)) (i'.1.pi (α := α) fun (i : ι) ↦ s i i'.2)
          (i.1.pi (α := α) fun (i_1 : ι) ↦ s i_1 (i.2 i_1))
Tactic: refine hasBasis_pi h |>.to_hasBasis ?_ ?_
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
κ : Type u_3
p : κ → Prop
s : (i : ι) → κ → Set (α i)
h : ∀ (i : ι), (f i).HasBasis p (s i)
h_dir : ∀ (I : Set ι) (k : ι → κ), I.Finite → (∀ i ∈ I, p (k i)) → ∃ (k₀ : κ), p k₀ ∧ ∀ i ∈ I, s i k₀ ⊆ s i (k i)
refine_1 :
  ∀ (i : Set ι × ((i : ι) → κ)),
    (i.1.Finite ∧ ∀ i_1 ∈ i.1, p (i.2 i_1)) →
      ∃ (i' : Prod.{u_1, u_3} (Set ι) κ),
        (i'.1.Finite ∧ p i'.2) ∧
          Subset (α := Set ((i : ι) → α i)) (i'.1.pi (α := α) fun (i : ι) ↦ s i i'.2)
            (i.1.pi (α := α) fun (i_1 : ι) ↦ s i_1 (i.2 i_1))
⊢ (pi (α := α) f).HasBasis (fun (Ik : Prod.{u_1, u_3} (Set ι) κ) ↦ Ik.1.Finite ∧ p Ik.2)
    fun (Ik : Prod.{u_1, u_3} (Set ι) κ) ↦ Ik.1.pi (α := α) fun (i : ι) ↦ s i Ik.2
have refine_2 : ∀ (i' : Prod.{u_1, u_3} (Set ι) κ),
  i'.1.Finite ∧ p i'.2 →
    ∃ (i : Set ι × ((i : ι) → κ)),
      (i.1.Finite ∧ ∀ i_1 ∈ i.1, p (i.2 i_1)) ∧
        Subset (α := Set ((i : ι) → α i)) (i.1.pi (α := α) fun (i_1 : ι) ↦ s i_1 (i.2 i_1))
          (i'.1.pi (α := α) fun (i : ι) ↦ s i i'.2)
Tactic: refine hasBasis_pi h |>.to_hasBasis ?_ ?_
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
κ : Type u_3
p : κ → Prop
s : (i : ι) → κ → Set (α i)
h : ∀ (i : ι), (f i).HasBasis p (s i)
h_dir : ∀ (I : Set ι) (k : ι → κ), I.Finite → (∀ i ∈ I, p (k i)) → ∃ (k₀ : κ), p k₀ ∧ ∀ i ∈ I, s i k₀ ⊆ s i (k i)
I : Set ι
k : (i : ι) → κ
hI : (I, k).1.Finite
hk : ∀ i ∈ (I, k).1, p ((I, k).2 i)
⊢ ∃ (i' : Prod.{u_1, u_3} (Set ι) κ),
    (i'.1.Finite ∧ p i'.2) ∧
      Subset (α := Set ((i : ι) → α i)) (i'.1.pi (α := α) fun (i : ι) ↦ s i i'.2)
        ((I, k).1.pi (α := α) fun (i : ι) ↦ s i ((I, k).2 i))
have refine_1 : ∀ (k₀ : κ) (hk₀ : p k₀) (hk₀' : ∀ i ∈ I, s i k₀ ⊆ s i (k i)),
  ∃ (i' : Prod.{u_1, u_3} (Set ι) κ),
    (i'.1.Finite ∧ p i'.2) ∧
      Subset (α := Set ((i : ι) → α i)) (i'.1.pi (α := α) fun (i : ι) ↦ s i i'.2)
        ((I, k).1.pi (α := α) fun (i : ι) ↦ s i ((I, k).2 i))
Tactic: rcases h_dir I k hI hk with ⟨k₀, hk₀, hk₀'⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : Type u_3
κ : Type u_4
f : Filter α
p : κ → Prop
s : κ → Set α
h : f.HasBasis p s
⊢ HasBasis (α := (i : ι) → α) (pi (α := fun (x : ι) ↦ α) fun (x : ι) ↦ f)
    (fun (Ik : Prod.{u_1, u_4} (Set ι) κ) ↦ Ik.1.Finite ∧ p Ik.2) fun (Ik : Prod.{u_1, u_4} (Set ι) κ) ↦
    Ik.1.pi (α := fun (i : ι) ↦ α) fun (x : ι) ↦ s Ik.2
have refine : ∀ (I : Set ι) (k : ι → κ) (hI : I.Finite) (hk : ∀ i ∈ I, p (k i)), ∃ (k₀ : κ), p k₀ ∧ ∀ i ∈ I, s k₀ ⊆ s (k i)
Tactic: refine hasBasis_pi_same_index (fun _ ↦ h) (fun I k hI hk ↦ ?_)
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : Type u_3
κ : Type u_4
f : Filter α
p : κ → Prop
s : κ → Set α
h : f.HasBasis p s
I : Set ι
k : ι → κ
hI : I.Finite
hk : ∀ i ∈ I, p (k i)
⊢ ∃ (k₀ : κ), p k₀ ∧ ∀ i ∈ I, s k₀ ⊆ s (k i)
have rcases : ∀ (k₀ : κ) (hk₀ : p k₀) (hk₀' : s k₀ ⊆ ⋂ i ∈ I, s (k i)), ∃ (k₀ : κ), p k₀ ∧ ∀ i ∈ I, s k₀ ⊆ s (k i)
Tactic: rcases h.mem_iff.mp (biInter_mem hI |>.mpr fun i hi ↦ h.mem_of_mem (hk i hi))
    with ⟨k₀, hk₀, hk₀'⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i
s : Set ((i : ι) → α i)
⊢ Membership.mem (γ := Filter ((i : ι) → α i)) (pi (α := α) fun (i : ι) ↦ pure (f i)) s ↔
    ∃ (I : Set ι), I.Finite ∧ ∀ (g : (i : ι) → α i), (∀ i ∈ I, g i = f i) → g ∈ s
have simp : (∃ (I : Set ι), I.Finite ∧ (I.pi (α := α) fun (i : ι) ↦ {f i}) ⊆ s) ↔
  ∃ (I : Set ι), I.Finite ∧ ∀ (g : (i : ι) → α i), (∀ i ∈ I, g i = f i) → g ∈ s
Tactic: simp only [← principal_singleton, mem_pi_principal]
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ pi (α := α) f ⊓ 𝓟 (Set.pi (α := α) univ s) = ⊥ ↔ ∃ (i : ι), f i ⊓ 𝓟 (s i) = ⊥
have mp : pi (α := α) f ⊓ 𝓟 (Set.pi (α := α) univ s) = ⊥ → ∃ (i : ι), f i ⊓ 𝓟 (s i) = ⊥
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
mp : pi (α := α) f ⊓ 𝓟 (Set.pi (α := α) univ s) = ⊥ → ∃ (i : ι), f i ⊓ 𝓟 (s i) = ⊥
⊢ pi (α := α) f ⊓ 𝓟 (Set.pi (α := α) univ s) = ⊥ ↔ ∃ (i : ι), f i ⊓ 𝓟 (s i) = ⊥
have mpr : (∃ (i : ι), f i ⊓ 𝓟 (s i) = ⊥) → pi (α := α) f ⊓ 𝓟 (Set.pi (α := α) univ s) = ⊥
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ pi (α := α) f ⊓ 𝓟 (Set.pi (α := α) univ s) = ⊥ → ∃ (i : ι), f i ⊓ 𝓟 (s i) = ⊥
have mp : (∃ (I : Set ι),
    I.Finite ∧ ∃ (t : (i : ι) → Set (α i)), (∀ (i : ι), t i ∈ f i) ∧ I.pi (α := α) t ⊆ (Set.pi (α := α) univ s)ᶜ) →
  ∃ (i : ι), (s i)ᶜ ∈ f i
Tactic: simp only [inf_principal_eq_bot, mem_pi]
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ (∃ (I : Set ι),
      I.Finite ∧ ∃ (t : (i : ι) → Set (α i)), (∀ (i : ι), t i ∈ f i) ∧ I.pi (α := α) t ⊆ (Set.pi (α := α) univ s)ᶜ) →
    ∃ (i : ι), (s i)ᶜ ∈ f i
have mp : (∀ (i : ι), (s i)ᶜ ∉ f i) →
  ∀ (I : Set ι) (_ : I.Finite) (t : (i : ι) → Set (α i)) (_ : ∀ (i : ι), t i ∈ f i),
    ¬I.pi (α := α) t ⊆ (Set.pi (α := α) univ s)ᶜ
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
hsf : ∀ (i : ι), ∃ᶠ (x : α i) in f i, x ∈ s i
I : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : I.pi (α := α) t ⊆ (Set.pi (α := α) univ s)ᶜ
⊢ False
have this : ∀ (i : ι), (s i ∩ t i).Nonempty
Tactic: have : ∀ i, (s i ∩ t i).Nonempty := fun i => ((hsf i).and_eventually (htf i)).exists
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
hsf : ∀ (i : ι), ∃ᶠ (x : α i) in f i, x ∈ s i
I : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : I.pi (α := α) t ⊆ (Set.pi (α := α) univ s)ᶜ
this : ∀ (i : ι), (s i ∩ t i).Nonempty
⊢ False
have mp : ∀ (x : (i : ι) → α i) (hxs : ∀ (i : ι), x i ∈ s i) (hxt : ∀ (i : ι), x i ∈ t i), False
Tactic: choose x hxs hxt using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ (∃ (i : ι), f i ⊓ 𝓟 (s i) = ⊥) → pi (α := α) f ⊓ 𝓟 (Set.pi (α := α) univ s) = ⊥
have mpr : (∃ (i : ι), (s i)ᶜ ∈ f i) → (Set.pi (α := α) univ s)ᶜ ∈ pi (α := α) f
Tactic: simp only [inf_principal_eq_bot]
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
i : ι
hi : (s i)ᶜ ∈ f i
⊢ (Set.pi (α := α) univ s)ᶜ ∈ pi (α := α) f
have h : ∀ (a : (i : ι) → α i),
  Membership.mem (γ := Set ((i : ι) → α i))
    {x : (i : ι) → α i | x ∈ eval (β := α) i ⁻¹' (s i)ᶜ → x ∈ (Set.pi (α := α) univ s)ᶜ} a
Tactic: filter_upwards [mem_pi_of_mem i hi] with x using mt fun h => h i trivial
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
i : ι
hi : (s i)ᶜ ∈ f i
h :
  ∀ (a : (i : ι) → α i),
    Membership.mem (γ := Set ((i : ι) → α i))
      {x : (i : ι) → α i | x ∈ eval (β := α) i ⁻¹' (s i)ᶜ → x ∈ (Set.pi (α := α) univ s)ᶜ} a
⊢ (Set.pi (α := α) univ s)ᶜ ∈ pi (α := α) f
have h₁ : ∀ a ∈ eval (β := α) i ⁻¹' (s i)ᶜ, a ∈ (Set.pi (α := α) univ s)ᶜ
Tactic: filter_upwards [mem_pi_of_mem i hi] with x using mt fun h => h i trivial
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst : ∀ (i : ι), (f i).NeBot
I : Set ι
⊢ pi (α := α) f ⊓ 𝓟 (I.pi (α := α) s) = ⊥ ↔ ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥
have rw : (∃ (i : ι), f i ⊓ 𝓟 (I.piecewise (β := fun (i : ι) ↦ Set (α i)) s (fun (x : ι) ↦ univ) i) = ⊥) ↔
  ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥
Tactic: rw [← univ_pi_piecewise_univ I, pi_inf_principal_univ_pi_eq_bot]
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst : ∀ (i : ι), (f i).NeBot
I : Set ι
⊢ (∃ (i : ι), f i ⊓ 𝓟 (I.piecewise (β := fun (i : ι) ↦ Set (α i)) s (fun (x : ι) ↦ univ) i) = ⊥) ↔
    ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥
have refine : ∀ (i : ι), f i ⊓ 𝓟 (I.piecewise (β := fun (i : ι) ↦ Set (α i)) s (fun (x : ι) ↦ univ) i) = ⊥ ↔ i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥
Tactic: refine exists_congr fun i => ?_
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst : ∀ (i : ι), (f i).NeBot
I : Set ι
i : ι
⊢ f i ⊓ 𝓟 (I.piecewise (β := fun (i : ι) ↦ Set (α i)) s (fun (x : ι) ↦ univ) i) = ⊥ ↔ i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥
have pos : ∀ (hi : i ∈ I),
  f i ⊓ 𝓟 (I.piecewise (β := fun (i : ι) ↦ Set (α i)) s (fun (x : ι) ↦ univ) i) = ⊥ ↔ i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥
Tactic: by_cases hi : i ∈ I
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst : ∀ (i : ι), (f i).NeBot
I : Set ι
i : ι
pos :
  ∀ (hi : i ∈ I),
    f i ⊓ 𝓟 (I.piecewise (β := fun (i : ι) ↦ Set (α i)) s (fun (x : ι) ↦ univ) i) = ⊥ ↔ i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥
⊢ f i ⊓ 𝓟 (I.piecewise (β := fun (i : ι) ↦ Set (α i)) s (fun (x : ι) ↦ univ) i) = ⊥ ↔ i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥
have neg : ∀ (hi : i ∉ I),
  f i ⊓ 𝓟 (I.piecewise (β := fun (i : ι) ↦ Set (α i)) s (fun (x : ι) ↦ univ) i) = ⊥ ↔ i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥
Tactic: by_cases hi : i ∈ I
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst : ∀ (i : ι), (f i).NeBot
I : Set ι
⊢ pi (α := α) f ⊓ 𝓟 (I.pi (α := α) s) = ⊥ ↔ ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥
have rw : pi (α := α) f ⊓ 𝓟 (Set.pi (α := α) univ (I.piecewise (β := fun (i : ι) ↦ Set (α i)) s fun (x : ι) ↦ univ)) = ⊥ ↔
  ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥
Tactic: classical
  rw [← univ_pi_piecewise_univ I, pi_inf_principal_univ_pi_eq_bot]
  refine exists_congr fun i => ?_
  by_cases hi : i ∈ I <;> simp [hi, NeBot.ne']
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst : ∀ (i : ι), (f i).NeBot
I : Set ι
rw :
  pi (α := α) f ⊓ 𝓟 (Set.pi (α := α) univ (I.piecewise (β := fun (i : ι) ↦ Set (α i)) s fun (x : ι) ↦ univ)) = ⊥ ↔
    ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥
⊢ pi (α := α) f ⊓ 𝓟 (I.pi (α := α) s) = ⊥ ↔ ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥
have rw₁ : (∃ (i : ι), f i ⊓ 𝓟 (I.piecewise (β := fun (i : ι) ↦ Set (α i)) s (fun (x : ι) ↦ univ) i) = ⊥) ↔
  ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥
Tactic: classical
  rw [← univ_pi_piecewise_univ I, pi_inf_principal_univ_pi_eq_bot]
  refine exists_congr fun i => ?_
  by_cases hi : i ∈ I <;> simp [hi, NeBot.ne']
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst : ∀ (i : ι), (f i).NeBot
I : Set ι
rw :
  pi (α := α) f ⊓ 𝓟 (Set.pi (α := α) univ (I.piecewise (β := fun (i : ι) ↦ Set (α i)) s fun (x : ι) ↦ univ)) = ⊥ ↔
    ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥
rw₁ rw₂ rw₃ :
  (∃ (i : ι), f i ⊓ 𝓟 (I.piecewise (β := fun (i : ι) ↦ Set (α i)) s (fun (x : ι) ↦ univ) i) = ⊥) ↔
    ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥
⊢ pi (α := α) f ⊓ 𝓟 (I.pi (α := α) s) = ⊥ ↔ ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥
have rw₄ : ∀ (i : ι), f i ⊓ 𝓟 (I.piecewise (β := fun (i : ι) ↦ Set (α i)) s (fun (x : ι) ↦ univ) i) = ⊥ ↔ i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥
Tactic: classical
  rw [← univ_pi_piecewise_univ I, pi_inf_principal_univ_pi_eq_bot]
  refine exists_congr fun i => ?_
  by_cases hi : i ∈ I <;> simp [hi, NeBot.ne']
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst : ∀ (i : ι), (f i).NeBot
i : ι
⊢ map (eval (β := α) i) (pi (α := α) f) = f i
have refine : ∀ (s : Set (α i)) (hs : s ∈ map (eval (β := α) i) (pi (α := α) f)), s ∈ f i
Tactic: refine le_antisymm (tendsto_eval_pi f i) fun s hs => ?_