awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact ⟨⟨I, fun _ ↦ k⟩, ⟨hI, fun _ _ ↦ hk⟩, subset_rfl⟩
-- Module: Mathlib.Order.Filter.Pi
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

Tactic:
hasBasis_pi_same_index (fun _ ↦ h) (fun I k hI hk ↦ ?_)

Premises used: Filter.hasBasis_pi_same_index
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : Type u_3
κ : Type u_4
f : Filter α
p : κ → Prop
s : κ → Set α
h : f.HasBasis p s
refine : ∀ (I : Set ι) (k : ι → κ) (hI : I.Finite) (hk : ∀ i ∈ I, p (k i)), ∃ (k₀ : κ), p k₀ ∧ ∀ i ∈ I, s k₀ ⊆ s (k i)
⊢ 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

Tactic:
refine hasBasis_pi_same_index (fun _ ↦ h) (fun I k hI hk ↦ ?_)

Premises used: Filter.hasBasis_pi_same_index
-- Module: Mathlib.Order.Filter.Pi
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)
rcases : ∀ (k₀ : κ) (hk₀ : p k₀) (hk₀' : s k₀ ⊆ ⋂ i ∈ I, s (k i)), ∃ (k₀ : κ), p k₀ ∧ ∀ i ∈ I, s k₀ ⊆ 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₀'⟩

Premises used: Iff.mpr, Filter.HasBasis.mem_iff, Filter.biInter_mem, Iff.mp, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Order.Filter.Pi
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₀ : κ
hk₀ : p k₀
hk₀' : s k₀ ⊆ ⋂ i ∈ I, s (k i)
⊢ ∃ (k₀ : κ), p k₀ ∧ ∀ i ∈ I, s k₀ ⊆ s (k i)

Tactic:
⟨k₀, hk₀, fun i hi ↦ hk₀'.trans (biInter_subset_of_mem hi)⟩

Premises used: HasSubset.Subset.trans, Set.biInter_subset_of_mem, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.Pi
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₀ : κ
hk₀ : p k₀
hk₀' : s k₀ ⊆ ⋂ i ∈ I, s (k i)
⊢ ∃ (k₀ : κ), p k₀ ∧ ∀ i ∈ I, s k₀ ⊆ s (k i)

Tactic:
exact ⟨k₀, hk₀, fun i hi ↦ hk₀'.trans (biInter_subset_of_mem hi)⟩
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
s : (i : ι) → Set (α i)
⊢ 𝓟 (Set.pi (α := α) univ s) ≤ pi (α := α) fun (i : ι) ↦ 𝓟 (s i)

Tactic:
le_pi.2 fun i ↦ tendsto_principal_principal.2 fun _f hf ↦ hf i trivial

Premises used: Iff.mpr, trivial, Filter.le_pi, Filter.tendsto_principal_principal
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
s : (i : ι) → Set (α i)
⊢ (pi (α := α) fun (i : ι) ↦ 𝓟 (s i)) = 𝓟 (Set.pi (α := α) univ s)

Tactic:
simp [Filter.pi, Set.pi_def]

Premises used: Filter.pi, Set.pi_def
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
s : (i : ι) → Set (α i)
t : Set ((i : ι) → α i)
⊢ (∃ (i : Set ι × ((i : ι) → Unit)), (i.1.Finite ∧ ∀ i_1 ∈ i.1, True) ∧ (i.1.pi (α := α) fun (i : ι) ↦ s i) ⊆ t) ↔
    ∃ (I : Set ι), I.Finite ∧ I.pi (α := α) s ⊆ t

Tactic:
simp
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
s : (i : ι) → Set (α i)
⊢ HasBasis (α := (i : ι) → α i) (pi (α := α) fun (i : ι) ↦ 𝓟 (s i)) Set.Finite fun (x : Set ι) ↦ x.pi (α := α) s

Tactic:
⟨fun _ ↦ mem_pi_principal⟩

Premises used: Filter.HasBasis.mk, Filter.mem_pi_principal
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
f : (i : ι) → α i
⊢ (pi (α := α) fun (x : ι) ↦ pure (f x)) = pure f

Tactic:
simp only [← principal_singleton, pi_principal, univ_pi_singleton]

Premises used: Filter.principal_singleton, Set.univ_pi_singleton, Filter.pi_principal
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i
s : Set ((i : ι) → α i)
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
⊢ 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

Tactic:
simp only [← principal_singleton, mem_pi_principal]

Premises used: Filter.principal_singleton, Filter.mem_pi_principal
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i
s : Set ((i : ι) → α i)
⊢ (∃ (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 [subset_def]

Premises used: Set.subset_def
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i
⊢ HasBasis (α := (i : ι) → α i) (pi (α := α) fun (i : ι) ↦ pure (f i)) Set.Finite fun (I : Set ι) ↦
    {g : (i : ι) → α i | ∀ i ∈ I, g i = f i}

Tactic:
⟨fun _ ↦ mem_pi_pure⟩

Premises used: Filter.HasBasis.mk, Filter.mem_pi_pure
-- Module: Mathlib.Order.Filter.Pi
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) = ⊥
mpr : (∃ (i : ι), f i ⊓ 𝓟 (s i) = ⊥) → pi (α := α) f ⊓ 𝓟 (Set.pi (α := α) univ s) = ⊥
⊢ pi (α := α) f ⊓ 𝓟 (Set.pi (α := α) univ s) = ⊥ ↔ ∃ (i : ι), f i ⊓ 𝓟 (s i) = ⊥

Tactic:
constructor
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
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
⊢ pi (α := α) f ⊓ 𝓟 (Set.pi (α := α) univ s) = ⊥ → ∃ (i : ι), f i ⊓ 𝓟 (s i) = ⊥

Tactic:
simp only [inf_principal_eq_bot, mem_pi]

Premises used: Filter.inf_principal_eq_bot, Filter.mem_pi
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
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)ᶜ
⊢ (∃ (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:
contrapose!
-- Module: Mathlib.Order.Filter.Pi
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)ᶜ
⊢ ∀ (i : ι), (s i ∩ t i).Nonempty

Tactic:
have : ∀ i, (s i ∩ t i).Nonempty := fun i => ((hsf i).and_eventually (htf i)).exists
-- Module: Mathlib.Order.Filter.Pi
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
mp : ∀ (x : (i : ι) → α i) (hxs : ∀ (i : ι), x i ∈ s i) (hxt : ∀ (i : ι), x i ∈ t i), False
⊢ False

Tactic:
choose x hxs hxt using this
-- Module: Mathlib.Order.Filter.Pi
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)ᶜ
x : (i : ι) → α i
hxs : ∀ (i : ι), x i ∈ s i
hxt : ∀ (i : ι), x i ∈ t i
⊢ False

Tactic:
hts (fun i _ => hxt i) (mem_univ_pi.2 hxs)

Premises used: Iff.mpr, Set.mem_univ_pi
-- Module: Mathlib.Order.Filter.Pi
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)ᶜ
x : (i : ι) → α i
hxs : ∀ (i : ι), x i ∈ s i
hxt : ∀ (i : ι), x i ∈ t i
⊢ False

Tactic:
exact hts (fun i _ => hxt i) (mem_univ_pi.2 hxs)

Premises used: Iff.mpr, Set.mem_univ_pi
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
mpr : (∃ (i : ι), (s i)ᶜ ∈ f i) → (Set.pi (α := α) univ s)ᶜ ∈ pi (α := α) f
⊢ (∃ (i : ι), f i ⊓ 𝓟 (s i) = ⊥) → pi (α := α) f ⊓ 𝓟 (Set.pi (α := α) univ s) = ⊥

Tactic:
simp only [inf_principal_eq_bot]

Premises used: Filter.inf_principal_eq_bot
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
i : ι
hi : (s i)ᶜ ∈ f i
x : (i : ι) → α i
⊢ x ∈ eval (β := α) i ⁻¹' (s i)ᶜ → x ∈ (Set.pi (α := α) univ s)ᶜ

Tactic:
mt fun h => h i trivial

Premises used: trivial, Set.Mem, setOf, mt, Set.preimage, Not
-- Module: Mathlib.Order.Filter.Pi
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
h₁ h₂ : ∀ x ∈ eval (β := α) i ⁻¹' (s i)ᶜ, x ∈ (Set.pi (α := α) univ s)ᶜ
⊢ (Set.pi (α := α) univ s)ᶜ ∈ pi (α := α) f

Tactic:
filter_upwards [mem_pi_of_mem i hi] with x using mt fun h => h i trivial

Premises used: mt, Filter.mem_pi_of_mem
-- 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 ι
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) = ⊥

Tactic:
rw [← univ_pi_piecewise_univ I, pi_inf_principal_univ_pi_eq_bot]

Premises used: Filter.pi_inf_principal_univ_pi_eq_bot, Set.univ_pi_piecewise_univ
-- 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 ι
⊢ (∃ (i : ι), f i ⊓ 𝓟 (I.piecewise (β := fun (i : ι) ↦ Set (α i)) s (fun (x : ι) ↦ univ) i) = ⊥) ↔
    ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥

Tactic:
exists_congr fun i => ?_

Premises used: exists_congr
-- 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 ι
refine :
  ∀ (i : ι),
    f i ⊓ 𝓟 (I.piecewise (β := fun (i : ι) ↦ Set (α i)) s (fun (x : ι) ↦ univ) i) = ⊥ ↔ i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥
⊢ (∃ (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 => ?_

Premises used: exists_congr
-- 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 ι
i : ι
pos :
  ∀ (hi : i ∈ I),
    f i ⊓ 𝓟 (I.piecewise (β := fun (i : ι) ↦ Set (α i)) s (fun (x : ι) ↦ univ) i) = ⊥ ↔ i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥
neg :
  ∀ (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) = ⊥

Tactic:
by_cases hi : i ∈ 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 ι
i : ι
hi : i ∈ I
⊢ f i ⊓ 𝓟 (I.piecewise (β := fun (i : ι) ↦ Set (α i)) s (fun (x : ι) ↦ univ) i) = ⊥ ↔ i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥

Tactic:
simp [hi, NeBot.ne']

Premises used: Filter.NeBot.ne'
-- 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 ι
i : ι
hi : i ∉ I
⊢ f i ⊓ 𝓟 (I.piecewise (β := fun (i : ι) ↦ Set (α i)) s (fun (x : ι) ↦ univ) i) = ⊥ ↔ i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥

Tactic:
simp [hi, NeBot.ne']

Premises used: Filter.NeBot.ne'
-- 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 ι
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) = ⊥
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) = ⊥

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']

Premises used: Filter.pi_inf_principal_univ_pi_eq_bot, Set.univ_pi_piecewise_univ, exists_congr, Filter.NeBot.ne'
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ (pi (α := α) f ⊓ 𝓟 (Set.pi (α := α) univ s)).NeBot ↔ ∀ (i : ι), (f i ⊓ 𝓟 (s i)).NeBot

Tactic:
simp [neBot_iff]

Premises used: Filter.neBot_iff
-- 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 ι
⊢ (pi (α := α) f ⊓ 𝓟 (I.pi (α := α) s)).NeBot ↔ ∀ i ∈ I, (f i ⊓ 𝓟 (s i)).NeBot

Tactic:
simp [neBot_iff]

Premises used: Filter.neBot_iff
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
p : (i : ι) → α i → Prop
h : ∀ (i : ι), (f i ⊓ 𝓟 (s i)).NeBot
I : Set ι
⊢ (pi (α := α) f ⊓ 𝓟 (I.pi (α := α) s)).NeBot

Tactic:
(pi_inf_principal_univ_pi_neBot.2 ‹_›).mono <|
    inf_le_inf_left _ <| principal_mono.2 fun _ hx i _ => hx i trivial

Premises used: Iff.mpr, trivial, Filter.NeBot.mono, Filter.principal_mono, inf_le_inf_left, Filter.pi_inf_principal_univ_pi_neBot
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
⊢ pi (α := α) f = ⊥ ↔ ∃ (i : ι), f i = ⊥

Tactic:
simpa using @pi_inf_principal_univ_pi_eq_bot ι α f fun _ => univ

Premises used: Filter.pi_inf_principal_univ_pi_eq_bot
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
⊢ (pi (α := α) f).NeBot ↔ ∀ (i : ι), (f i).NeBot

Tactic:
simp [neBot_iff]

Premises used: Filter.neBot_iff
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
p : (i : ι) → α i → Prop
inst : ∀ (i : ι), (f i).NeBot
⊢ (pi (α := α) f).NeBot

Tactic:
pi_neBot.2 ‹_›

Premises used: Iff.mpr, Filter.pi_neBot
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst : ∀ (i : ι), (f i).NeBot
i : ι
⊢ map (eval (β := α) i) (pi (α := α) f) = f i

Tactic:
le_antisymm (tendsto_eval_pi f i) fun s hs => ?_

Premises used: le_antisymm, Filter.tendsto_eval_pi
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst : ∀ (i : ι), (f i).NeBot
i : ι
refine : ∀ (s : Set (α i)) (hs : s ∈ map (eval (β := α) i) (pi (α := α) f)), s ∈ f i
⊢ map (eval (β := α) i) (pi (α := α) f) = f i

Tactic:
refine le_antisymm (tendsto_eval_pi f i) fun s hs => ?_

Premises used: le_antisymm, Filter.tendsto_eval_pi
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst : ∀ (i : ι), (f i).NeBot
i : ι
s : Set (α i)
hs : s ∈ map (eval (β := α) i) (pi (α := α) f)
rcases :
  ∀ (I : Set ι) (hIf : I.Finite) (t : (i : ι) → Set (α i)) (htf : ∀ (i : ι), t i ∈ f i)
    (hI : I.pi (α := α) t ⊆ eval (β := α) i ⁻¹' s), s ∈ f i
⊢ s ∈ f i

Tactic:
rcases mem_pi.1 (mem_map.1 hs) with ⟨I, hIf, t, htf, hI⟩

Premises used: Iff.mp, Filter.mem_pi, Filter.mem_map
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst : ∀ (i : ι), (f i).NeBot
i : ι
s : Set (α i)
hs : s ∈ map (eval (β := α) i) (pi (α := α) f)
I : Set ι
hIf : I.Finite
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : I.pi (α := α) t ⊆ eval (β := α) i ⁻¹' s
⊢ eval (β := α) i '' I.pi (α := α) t ⊆ s

Tactic:
rw [← image_subset_iff] at hI

Premises used: Set.image_subset_iff
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst : ∀ (i : ι), (f i).NeBot
i : ι
s : Set (α i)
hs : s ∈ map (eval (β := α) i) (pi (α := α) f)
I : Set ι
hIf : I.Finite
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : eval (β := α) i '' I.pi (α := α) t ⊆ s
⊢ s ∈ f i

Tactic:
mem_of_superset (htf i) ((subset_eval_image_pi ?_ _).trans hI)

Premises used: HasSubset.Subset.trans, Set.subset_eval_image_pi, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst : ∀ (i : ι), (f i).NeBot
i : ι
s : Set (α i)
hs : s ∈ map (eval (β := α) i) (pi (α := α) f)
I : Set ι
hIf : I.Finite
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : eval (β := α) i '' I.pi (α := α) t ⊆ s
refine : (I.pi (α := α) t).Nonempty
⊢ s ∈ f i

Tactic:
refine mem_of_superset (htf i) ((subset_eval_image_pi ?_ _).trans hI)

Premises used: HasSubset.Subset.trans, Set.subset_eval_image_pi, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst : ∀ (i : ι), (f i).NeBot
i : ι
s : Set (α i)
hs : s ∈ map (eval (β := α) i) (pi (α := α) f)
I : Set ι
hIf : I.Finite
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : eval (β := α) i '' I.pi (α := α) t ⊆ s
⊢ (I.pi (α := α) t).Nonempty

Tactic:
nonempty_of_mem (pi_mem_pi hIf fun i _ => htf i)

Premises used: Filter.nonempty_of_mem, Filter.pi_mem_pi
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst : ∀ (i : ι), (f i).NeBot
i : ι
s : Set (α i)
hs : s ∈ map (eval (β := α) i) (pi (α := α) f)
I : Set ι
hIf : I.Finite
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : eval (β := α) i '' I.pi (α := α) t ⊆ s
⊢ (I.pi (α := α) t).Nonempty

Tactic:
exact nonempty_of_mem (pi_mem_pi hIf fun i _ => htf i)

Premises used: Filter.nonempty_of_mem, Filter.pi_mem_pi
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f₁ f₂ : (i : ι) → Filter (α i)
inst : ∀ (i : ι), (f₁ i).NeBot
⊢ pi (α := α) f₁ ≤ pi (α := α) f₂ ↔ ∀ (i : ι), f₁ i ≤ f₂ i

Tactic:
⟨fun h i => map_eval_pi f₁ i ▸ (tendsto_eval_pi _ _).mono_left h, pi_mono⟩

Premises used: Eq.rec, Iff.intro, Filter.pi_mono, Filter.Tendsto.mono_left, Filter.map_eval_pi, Filter.tendsto_eval_pi
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f₁ f₂ : (i : ι) → Filter (α i)
inst : ∀ (i : ι), (f₁ i).NeBot
⊢ pi (α := α) f₁ = pi (α := α) f₂ ↔ f₁ = f₂

Tactic:
⟨fun h => ?_, congr_arg pi⟩

Premises used: congr_arg, Iff.intro, Filter.pi
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f₁ f₂ : (i : ι) → Filter (α i)
inst : ∀ (i : ι), (f₁ i).NeBot
refine : ∀ (h : pi (α := α) f₁ = pi (α := α) f₂), f₁ = f₂
⊢ pi (α := α) f₁ = pi (α := α) f₂ ↔ f₁ = f₂

Tactic:
refine ⟨fun h => ?_, congr_arg pi⟩
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f₁ f₂ : (i : ι) → Filter (α i)
inst : ∀ (i : ι), (f₁ i).NeBot
h : pi (α := α) f₁ = pi (α := α) f₂
⊢ f₁ ≤ f₂

Tactic:
have hle : f₁ ≤ f₂ := pi_le_pi.1 h.le
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f₁ f₂ : (i : ι) → Filter (α i)
inst : ∀ (i : ι), (f₁ i).NeBot
h : pi (α := α) f₁ = pi (α := α) f₂
hle : f₁ ≤ f₂
⊢ ∀ (i : ι), (f₂ i).NeBot

Tactic:
haveI : ∀ i, NeBot (f₂ i) := fun i => neBot_of_le (hle i)
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f₁ f₂ : (i : ι) → Filter (α i)
inst : ∀ (i : ι), (f₁ i).NeBot
h : pi (α := α) f₁ = pi (α := α) f₂
hle : f₁ ≤ f₂
this : ∀ (i : ι), (f₂ i).NeBot
⊢ f₁ = f₂

Tactic:
hle.antisymm (pi_le_pi.1 h.ge)

Premises used: Filter.pi_le_pi, Eq.ge, LE.le.antisymm, Iff.mp
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f₁ f₂ : (i : ι) → Filter (α i)
inst : ∀ (i : ι), (f₁ i).NeBot
h : pi (α := α) f₁ = pi (α := α) f₂
hle : f₁ ≤ f₂
this : ∀ (i : ι), (f₂ i).NeBot
⊢ f₁ = f₂

Tactic:
exact hle.antisymm (pi_le_pi.1 h.ge)

Premises used: Filter.pi_le_pi, Eq.ge, LE.le.antisymm, Iff.mp
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
f : (i : ι) → α i → β i
l : (i : ι) → Filter (α i)
l' : (i : ι) → Filter (β i)
h : ∀ (i : ι), Tendsto (f i) (l i) (l' i)
⊢ Tendsto (Pi.map (α := α) (β := β) f) (pi (α := α) l) (pi (α := β) l')

Tactic:
tendsto_pi.2 fun i ↦ (h i).comp (tendsto_eval_pi _ _)

Premises used: Iff.mpr, Filter.tendsto_pi, Filter.Tendsto.comp, Filter.tendsto_eval_pi
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
f : (i : ι) → α i → β i
l : (i : ι) → Filter (β i)
⊢ (pi (α := α) fun (i : ι) ↦ comap (f i) (l i)) = comap (Pi.map (α := α) (β := β) f) (pi (α := β) l)

Tactic:
simp [Filter.pi, Filter.comap_comap, Function.comp_def]

Premises used: Function.comp_def, Filter.comap_comap, Filter.pi
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
⊢ s ∈ Filter.coprodᵢ (α := α) f ↔ ∀ (i : ι), ∃ t₁ ∈ f i, eval (β := α) i ⁻¹' t₁ ⊆ s

Tactic:
simp [Filter.coprodᵢ]

Premises used: Filter.coprodᵢ
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
⊢ sᶜ ∈ Filter.coprodᵢ (α := α) f ↔ ∀ (i : ι), (eval (β := α) i '' s)ᶜ ∈ f i

Tactic:
simp only [Filter.coprodᵢ, mem_iSup, compl_mem_comap]

Premises used: Filter.coprodᵢ, Filter.mem_iSup, Filter.compl_mem_comap
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
⊢ (Filter.coprodᵢ (α := α) f).NeBot ↔ (∀ (i : ι), Nonempty.{u_2 + 1} (α i)) ∧ ∃ (d : ι), (f d).NeBot

Tactic:
simp only [Filter.coprodᵢ, iSup_neBot, ← exists_and_left, ← comap_eval_neBot_iff']

Premises used: Filter.coprodᵢ, exists_and_left, Filter.iSup_neBot, Filter.comap_eval_neBot_iff'
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
⊢ (Filter.coprodᵢ (α := α) f).NeBot ↔ ∃ (d : ι), (f d).NeBot

Tactic:
simp [coprodᵢ_neBot_iff', *]

Premises used: Filter.coprodᵢ_neBot_iff'
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
⊢ Filter.coprodᵢ (α := α) f = ⊥ ↔ (∃ (i : ι), IsEmpty.{u_2 + 1} (α i)) ∨ f = ⊥

Tactic:
simpa only [not_neBot, not_and_or, funext_iff, not_forall, not_exists, not_nonempty_iff]
    using coprodᵢ_neBot_iff'.not

Premises used: funext_iff, not_exists, Iff.not, not_nonempty_iff, not_and_or, Filter.not_neBot, Filter.coprodᵢ_neBot_iff', Classical.not_forall
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
⊢ Filter.coprodᵢ (α := α) f = ⊥ ↔ f = ⊥

Tactic:
simpa [funext_iff] using coprodᵢ_neBot_iff.not

Premises used: funext_iff, Filter.coprodᵢ_neBot_iff, Iff.not
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
⊢ Eq (α := Filter ((i : ι) → α i)) (Filter.coprodᵢ (α := α) ⊥) ⊥

Tactic:
coprodᵢ_eq_bot_iff'.2 (Or.inr rfl)

Premises used: Iff.mpr, Filter.coprodᵢ_eq_bot_iff', Or.inr, rfl