awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
l : Filter α
s : Set α
f : α → β
t : Set β
⊢ sᶜ ∪ f ⁻¹' t ∈ l ↔ {x : α | x ∉ s ∨ x ∈ f ⁻¹' t} ∈ l

Tactic:
rfl
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
l₁ : Filter α
l₂ : Filter β
s : Set α
f : α → β
⊢ Tendsto f (l₁ ⊓ 𝓟 s) l₂ ↔ PTendsto (PFun.res f s) l₁ l₂

Tactic:
simp only [Tendsto, PTendsto, pmap_res]

Premises used: Filter.Tendsto, Filter.pmap_res, Filter.PTendsto
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
l₁ : Filter α
l₂ : Filter β
f : α → β
rw : Tendsto f l₁ l₂ ↔ Tendsto f (l₁ ⊓ 𝓟 Set.univ) l₂
⊢ Tendsto f l₁ l₂ ↔ PTendsto (PFun.res f Set.univ) l₁ l₂

Tactic:
rw [← tendsto_iff_ptendsto]

Premises used: Filter.tendsto_iff_ptendsto
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
l₁ : Filter α
l₂ : Filter β
f : α → β
⊢ Tendsto f l₁ l₂ ↔ Tendsto f (l₁ ⊓ 𝓟 Set.univ) l₂

Tactic:
simp [principal_univ]

Premises used: Filter.principal_univ
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
f : α →. β
l₁ : Filter α
l₂ : Filter β
⊢ PTendsto' f l₁ l₂ ↔ ∀ s ∈ l₂, f.preimage s ∈ l₁

Tactic:
rtendsto'_def _ _ _

Premises used: Set.Mem, Filter.rtendsto'_def, Filter.PTendsto', PFun.preimage
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
f : α →. β
l₁ : Filter α
l₂ : Filter β
rw : (∀ s ∈ l₂, f.preimage s ∈ l₁) → ∀ s ∈ l₂, f.core s ∈ l₁
⊢ PTendsto' f l₁ l₂ → PTendsto f l₁ l₂

Tactic:
rw [ptendsto_def, ptendsto'_def]

Premises used: Filter.ptendsto_def, Filter.ptendsto'_def
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
f : α →. β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ s ∈ l₂, f.preimage s ∈ l₁) → ∀ s ∈ l₂, f.core s ∈ l₁

Tactic:
fun h s sl₂ => mem_of_superset (h s sl₂) (PFun.preimage_subset_core _ _)

Premises used: PFun.preimage_subset_core, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
f : α →. β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ s ∈ l₂, f.preimage s ∈ l₁) → ∀ s ∈ l₂, f.core s ∈ l₁

Tactic:
exact fun h s sl₂ => mem_of_superset (h s sl₂) (PFun.preimage_subset_core _ _)

Premises used: PFun.preimage_subset_core, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
f : α →. β
l₁ : Filter α
l₂ : Filter β
h : f.Dom ∈ l₁
rw : (∀ s ∈ l₂, f.core s ∈ l₁) → ∀ s ∈ l₂, f.preimage s ∈ l₁
⊢ PTendsto f l₁ l₂ → PTendsto' f l₁ l₂

Tactic:
rw [ptendsto_def, ptendsto'_def]

Premises used: Filter.ptendsto_def, Filter.ptendsto'_def
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
f : α →. β
l₁ : Filter α
l₂ : Filter β
h : f.Dom ∈ l₁
h' : ∀ s ∈ l₂, f.core s ∈ l₁
s : Set β
sl₂ : s ∈ l₂
rw : f.core s ∩ f.Dom ∈ l₁
⊢ f.preimage s ∈ l₁

Tactic:
rw [PFun.preimage_eq]

Premises used: PFun.preimage_eq
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
f : α →. β
l₁ : Filter α
l₂ : Filter β
h : f.Dom ∈ l₁
h' : ∀ s ∈ l₂, f.core s ∈ l₁
s : Set β
sl₂ : s ∈ l₂
⊢ f.core s ∩ f.Dom ∈ l₁

Tactic:
inter_mem (h' s sl₂) h

Premises used: Filter.inter_mem
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
f : α →. β
l₁ : Filter α
l₂ : Filter β
h : f.Dom ∈ l₁
h' : ∀ s ∈ l₂, f.core s ∈ l₁
s : Set β
sl₂ : s ∈ l₂
⊢ f.core s ∩ f.Dom ∈ l₁

Tactic:
exact inter_mem (h' s sl₂) h

Premises used: Filter.inter_mem
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
i : ι
⊢ Tendsto (eval (β := α) i) (pi (α := α) f) (f i)

Tactic:
tendsto_iInf' i tendsto_comap

Premises used: Filter.tendsto_comap, Filter.tendsto_iInf', Filter.pi
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
β : Type u_3
m : β → (i : ι) → α i
l : Filter β
simp : (∀ (i : ι), Tendsto (eval (β := α) i ∘ m) l (f i)) ↔ ∀ (i : ι), Tendsto (fun (x : β) ↦ m x i) l (f i)
⊢ Tendsto m l (pi (α := α) f) ↔ ∀ (i : ι), Tendsto (fun (x : β) ↦ m x i) l (f i)

Tactic:
simp only [pi, tendsto_iInf, tendsto_comap_iff]

Premises used: Filter.tendsto_comap_iff, Filter.pi, Filter.tendsto_iInf
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
β : Type u_3
m : β → (i : ι) → α i
l : Filter β
⊢ (∀ (i : ι), Tendsto (eval (β := α) i ∘ m) l (f i)) ↔ ∀ (i : ι), Tendsto (fun (x : β) ↦ m x i) l (f i)

Tactic:
rfl
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
g : Filter ((i : ι) → α i)
⊢ g ≤ pi (α := α) f ↔ ∀ (i : ι), Tendsto (eval (β := α) i) g (f i)

Tactic:
tendsto_pi

Premises used: Set.Mem, setOf, Filter.tendsto_pi, Set.preimage, Filter.Tendsto
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f₁ f₂ : (i : ι) → Filter (α i)
h : ∀ (i : ι), f₁ i ≤ f₂ i
⊢ pi (α := α) f₁ ≤ pi (α := α) f₂

Tactic:
iInf_mono fun i => comap_mono <| h i

Premises used: Set.Mem, Filter.comap_mono, iInf_mono
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
i : ι
s : Set (α i)
hs : s ∈ f i
⊢ eval (β := α) i ⁻¹' s ∈ pi (α := α) f

Tactic:
mem_iInf_of_mem i <| preimage_mem_comap hs

Premises used: Set.Mem, Filter.mem_iInf_of_mem, Filter.preimage_mem_comap
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
hI : I.Finite
h : ∀ i ∈ I, s i ∈ f i
rw : ⋂ (x : (↑I : Type u_1)), eval (β := α) (↑x : ι) ⁻¹' s (↑x : ι) ∈ pi (α := α) f
⊢ I.pi (α := α) s ∈ pi (α := α) f

Tactic:
rw [pi_def, biInter_eq_iInter]

Premises used: Set.biInter_eq_iInter, Set.pi_def
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
hI : I.Finite
h : ∀ i ∈ I, s i ∈ f i
⊢ ⋂ (x : (↑I : Type u_1)), eval (β := α) (↑x : ι) ⁻¹' s (↑x : ι) ∈ pi (α := α) f

Tactic:
mem_iInf_of_iInter hI (fun i => ?_) Subset.rfl

Premises used: Set.Mem, Filter.mem_iInf_of_iInter, Set.Subset.rfl
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
hI : I.Finite
h : ∀ i ∈ I, s i ∈ f i
refine : ∀ (i : (↑I : Type u_1)), eval (β := α) (↑i : ι) ⁻¹' s (↑i : ι) ∈ comap (eval (β := α) (↑i : ι)) (f (↑i : ι))
⊢ ⋂ (x : (↑I : Type u_1)), eval (β := α) (↑x : ι) ⁻¹' s (↑x : ι) ∈ pi (α := α) f

Tactic:
refine mem_iInf_of_iInter hI (fun i => ?_) Subset.rfl

Premises used: Filter.mem_iInf_of_iInter, Set.Subset.rfl
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
hI : I.Finite
h : ∀ i ∈ I, s i ∈ f i
i : (↑I : Type u_1)
⊢ eval (β := α) (↑i : ι) ⁻¹' s (↑i : ι) ∈ comap (eval (β := α) (↑i : ι)) (f (↑i : ι))

Tactic:
preimage_mem_comap (h i i.2)

Premises used: Filter.preimage_mem_comap, Subtype.val, Subtype.property
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
hI : I.Finite
h : ∀ i ∈ I, s i ∈ f i
i : (↑I : Type u_1)
⊢ eval (β := α) (↑i : ι) ⁻¹' s (↑i : ι) ∈ comap (eval (β := α) (↑i : ι)) (f (↑i : ι))

Tactic:
exact preimage_mem_comap (h i i.2)

Premises used: Filter.preimage_mem_comap, Subtype.val, Subtype.property
-- Module: Mathlib.Order.Filter.Pi
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
mpr :
  (∃ (I : Set ι), I.Finite ∧ ∃ (t : (i : ι) → Set (α i)), (∀ (i : ι), t i ∈ f i) ∧ I.pi (α := α) t ⊆ s) →
    s ∈ pi (α := α) f
⊢ s ∈ pi (α := α) f ↔
    ∃ (I : Set ι), I.Finite ∧ ∃ (t : (i : ι) → Set (α i)), (∀ (i : ι), t i ∈ f i) ∧ I.pi (α := α) t ⊆ s

Tactic:
constructor
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
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
⊢ s ∈ pi (α := α) f →
    ∃ (I : Set ι), I.Finite ∧ ∃ (t : (i : ι) → Set (α i)), (∀ (i : ι), t i ∈ f i) ∧ I.pi (α := α) t ⊆ s

Tactic:
simp only [pi, mem_iInf', mem_comap, pi_def]

Premises used: Filter.mem_comap, Filter.pi, Filter.mem_iInf', Set.pi_def
-- Module: Mathlib.Order.Filter.Pi
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
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)
⊢ ∃ (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
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
I : Set ι
If : I.Finite
V : ι → Set ((i : ι) → α i)
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:
⟨I, If, t, htf, iInter₂_mono fun i _ => htV i⟩

Premises used: Set.iInter₂_mono, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
I : Set ι
If : I.Finite
V : ι → Set ((i : ι) → α i)
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:
exact ⟨I, If, t, htf, iInter₂_mono fun i _ => htV i⟩
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
I : Set ι
If : I.Finite
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : I.pi (α := α) t ⊆ s
⊢ s ∈ pi (α := α) f

Tactic:
mem_of_superset (pi_mem_pi If fun i _ => htf i) hts

Premises used: Filter.pi_mem_pi, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
I : Set ι
If : I.Finite
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : I.pi (α := α) t ⊆ s
⊢ s ∈ pi (α := α) f

Tactic:
exact mem_of_superset (pi_mem_pi If fun i _ => htf i) hts

Premises used: Filter.pi_mem_pi, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
⊢ s ∈ pi (α := α) f ↔
    ∃ (I : Finset ι) (t : (i : ι) → Set (α i)), (∀ (i : ι), t i ∈ f i) ∧ (↑I : Set ι).pi (α := α) t ⊆ s

Tactic:
mem_pi.trans exists_finite_iff_finset

Premises used: Iff.trans, Set.exists_finite_iff_finset, Filter.mem_pi
-- Module: Mathlib.Order.Filter.Pi
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

Tactic:
rcases mem_pi.1 h with ⟨I', -, t, htf, hts⟩

Premises used: Iff.mp, Filter.mem_pi
-- Module: Mathlib.Order.Filter.Pi
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

Tactic:
mem_of_superset (htf i) fun x hx => ?_

Premises used: Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Pi
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
refine : ∀ (x : α i) (hx : x ∈ t i), x ∈ s i
⊢ s i ∈ f i

Tactic:
refine mem_of_superset (htf i) fun x hx => ?_

Premises used: Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Pi
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
⊢ ∀ (i : ι), (t i).Nonempty

Tactic:
have : ∀ i, (t i).Nonempty := fun i => nonempty_of_mem (htf i)
-- Module: Mathlib.Order.Filter.Pi
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
choose : ∀ (g : (i : ι) → α i) (hg : ∀ (i : ι), g i ∈ t i), x ∈ s i
⊢ x ∈ s i

Tactic:
choose g hg using this
-- Module: Mathlib.Order.Filter.Pi
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
inr : ∀ (hne : j ≠ i), update (β := α) g i x j ∈ t j
⊢ update (β := α) g i x j ∈ t j

Tactic:
rcases eq_or_ne j i with (rfl | hne)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Order.Filter.Pi
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' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : I'.pi (α := α) t ⊆ I.pi (α := α) s
g : (i : ι) → α i
hg : ∀ (i : ι), g i ∈ t i
j : ι
h_1 : j ∈ I'
hi : j ∈ I
x : α j
hx : x ∈ t j
⊢ update (β := α) g j x j ∈ t j

Tactic:
simp [*]
-- Module: Mathlib.Order.Filter.Pi
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'
hne : j ≠ i
⊢ update (β := α) g i x j ∈ t j

Tactic:
simp [*]
-- Module: Mathlib.Order.Filter.Pi
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
⊢ 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 [*]
-- Module: Mathlib.Order.Filter.Pi
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
this : update (β := α) g i x ∈ I'.pi (α := α) t
⊢ x ∈ s i

Tactic:
simpa using hts this i hi
-- Module: Mathlib.Order.Filter.Pi
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
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
⊢ 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

Premises used: Iff.mp, Filter.mem_pi
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst : ∀ (i : ι), (f i).NeBot
I : Set ι
hI : I.Finite
⊢ I.pi (α := α) s ∈ pi (α := α) f ↔ ∀ i ∈ I, s i ∈ f i

Tactic:
⟨fun h _i hi => mem_of_pi_mem_pi h hi, pi_mem_pi hI⟩

Premises used: Filter.mem_of_pi_mem_pi, Iff.intro, Filter.pi_mem_pi
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
p : (i : ι) → α i → Prop
i : ι
hf : ∀ᶠ (x : α i) in f i, p i x
⊢ ∀ᶠ (x : (i : ι) → α i) in pi (α := α) f, p i (x i)

Tactic:
(tendsto_eval_pi _ _).eventually hf

Premises used: Filter.Tendsto.eventually, Filter.tendsto_eval_pi
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
p : (i : ι) → α i → Prop
inst : Finite ι
hf : ∀ (i : ι), ∀ᶠ (x : α i) in f i, p i x
⊢ ∀ᶠ (x : (i : ι) → α i) in pi (α := α) f, ∀ (i : ι), p i (x i)

Tactic:
eventually_all.2 fun _i => (hf _).eval_pi

Premises used: Iff.mpr, Filter.Eventually.eval_pi, Filter.eventually_all
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
ι' : ι → Type u_3
s : (i : ι) → ι' i → Set (α i)
p : (i : ι) → ι' i → Prop
h : ∀ (i : ι), (f i).HasBasis (p i) (s i)
⊢ (pi (α := α) f).HasBasis (fun (If : Set ι × ((i : ι) → ι' i)) ↦ If.1.Finite ∧ ∀ i ∈ If.1, p i (If.2 i))
    fun (If : Set ι × ((i : ι) → ι' i)) ↦ If.1.pi (α := α) fun (i : ι) ↦ s i (If.2 i)

Tactic:
simpa [Set.pi_def] using HasBasis.iInf' fun i => (h i).comap (eval i : (∀ j, α j) → α i)

Premises used: Function.eval, Filter.HasBasis.comap, Filter.HasBasis.iInf', Set.pi_def
-- Module: Mathlib.Order.Filter.Pi
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

Tactic:
hasBasis_pi h |>.to_hasBasis ?_ ?_

Premises used: Filter.HasBasis.to_hasBasis, Filter.hasBasis_pi
-- Module: Mathlib.Order.Filter.Pi
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))
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)
⊢ (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

Tactic:
refine hasBasis_pi h |>.to_hasBasis ?_ ?_

Premises used: Filter.HasBasis.to_hasBasis, Filter.hasBasis_pi
-- Module: Mathlib.Order.Filter.Pi
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)
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))
⊢ ∃ (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₀'⟩
-- Module: Mathlib.Order.Filter.Pi
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)
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:
⟨⟨I, k₀⟩, ⟨hI, hk₀⟩, Set.pi_mono hk₀'⟩

Premises used: Prod.mk, And.intro, Exists.intro, Set.pi_mono
-- Module: Mathlib.Order.Filter.Pi
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)
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:
exact ⟨⟨I, k₀⟩, ⟨hI, hk₀⟩, Set.pi_mono hk₀'⟩
-- Module: Mathlib.Order.Filter.Pi
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 : κ
hI : (I, k).1.Finite
hk : p (I, k).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, k).1.pi (α := α) fun (i : ι) ↦ s i (I, k).2)

Tactic:
⟨⟨I, fun _ ↦ k⟩, ⟨hI, fun _ _ ↦ hk⟩, subset_rfl⟩

Premises used: Prod.mk, And.intro, Exists.intro, subset_rfl