awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
simp :
  Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α)) t ↔
    ∃ (p : α → Set β), (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ (x : (↑(↑s : Set α) : Type u)), p (↑x : α)
refine_1 :
  ∀ (h : Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α)) t),
    ∃ (p : α → Set β), (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ (x : (↑(↑s : Set α) : Type u)), p (↑x : α)
refine_2 refine_2₁ :
  (∃ (p : α → Set β), (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ (x : (↑(↑s : Set α) : Type u)), p (↑x : α)) →
    Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α)) t
⊢ Membership.mem (γ := Filter β) (⨅ a ∈ s, f a) t ↔ ∃ (p : α → Set β), (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ a ∈ s, p a

Tactic:
classical
  simp only [← Finset.set_biInter_coe, biInter_eq_iInter, iInf_subtype']
  refine ⟨fun h => ?_, ?_⟩
  · rcases (mem_iInf_of_finite _).1 h with ⟨p, hp, rfl⟩
    refine ⟨fun a => if h : a ∈ s then p ⟨a, h⟩ else univ,
            fun a ha => by simpa [ha] using hp ⟨a, ha⟩, ?_⟩
    refine iInter_congr_of_surjective id surjective_id ?_
    rintro ⟨a, ha⟩
    simp [ha]
  · rintro ⟨p, hpf, rfl⟩
    exact iInter_mem.2 fun a => mem_iInf_of_mem a (hpf a a.2)

Premises used: Finset.set_biInter_coe, Set.biInter_eq_iInter, id, iInf_subtype', Function.surjective_id, Set.iInter_congr_of_surjective, rfl
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type w
f : ι → Set α
⊢ Eq.{u + 1} (α := Filter α) (⨅ (i : ι), ⨅ (_ : Membership.mem (γ := Finset ι) ∅ i), 𝓟 (f i))
    (𝓟 (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) ∅ i), f i))

Tactic:
simp
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type w
f : ι → Set α
i : ι
s : Finset ι
h : i ∉ s
hs : Eq.{u + 1} (α := Filter α) (⨅ i ∈ s, 𝓟 (f i)) (𝓟 (⋂ i ∈ s, f i))
insert : 𝓟 (f i) ⊓ ⨅ x ∈ s, 𝓟 (f x) = 𝓟 (⋂ i_1 ∈ Insert.insert i s, f i_1)
insert₁ : 𝓟 (f i) ⊓ ⨅ x ∈ s, 𝓟 (f x) = 𝓟 (f i ∩ ⋂ x ∈ s, f x)
insert₂ : 𝓟 (f i) ⊓ 𝓟 (⋂ i ∈ s, f i) = 𝓟 (f i ∩ ⋂ x ∈ s, f x)
insert₃ insert₄ : 𝓟 (f i ∩ ⋂ i ∈ s, f i) = 𝓟 (f i ∩ ⋂ x ∈ s, f x)
⊢ Eq.{u + 1} (α := Filter α) (⨅ i_1 ∈ Insert.insert i s, 𝓟 (f i_1)) (𝓟 (⋂ i_1 ∈ Insert.insert i s, f i_1))

Tactic:
rw [Finset.iInf_insert, Finset.set_biInter_insert, hs, inf_principal]

Premises used: Filter.inf_principal, Finset.iInf_insert, Finset.set_biInter_insert
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type w
s : Finset ι
f : ι → Set α
empty :
  Eq.{u + 1} (α := Filter α) (⨅ (i : ι), ⨅ (_ : Membership.mem (γ := Finset ι) ∅ i), 𝓟 (f i))
    (𝓟 (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) ∅ i), f i))
insert :
  ∀ (i : ι) (s : Finset ι),
    i ∉ s →
      ∀ (hs : Eq.{u + 1} (α := Filter α) (⨅ i ∈ s, 𝓟 (f i)) (𝓟 (⋂ i ∈ s, f i))),
        Eq.{u + 1} (α := Filter α) (⨅ i_1 ∈ Insert.insert i s, 𝓟 (f i_1)) (𝓟 (⋂ i_1 ∈ Insert.insert i s, f i_1))
⊢ Eq.{u + 1} (α := Filter α) (⨅ i ∈ s, 𝓟 (f i)) (𝓟 (⋂ i ∈ s, f i))

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert i s _ hs => rw [Finset.iInf_insert, Finset.set_biInter_insert, hs, inf_principal]

Premises used: Filter.inf_principal, Finset.iInf_insert, Insert.insert, Finset.set_biInter_insert
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type w
s : Finset ι
f : ι → Set α
empty :
  Eq.{u + 1} (α := Filter α) (⨅ (i : ι), ⨅ (_ : Membership.mem (γ := Finset ι) ∅ i), 𝓟 (f i))
    (𝓟 (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) ∅ i), f i))
insert :
  ∀ (i : ι) (s : Finset ι),
    i ∉ s →
      ∀ (hs : Eq.{u + 1} (α := Filter α) (⨅ i ∈ s, 𝓟 (f i)) (𝓟 (⋂ i ∈ s, f i))),
        Eq.{u + 1} (α := Filter α) (⨅ i_1 ∈ Insert.insert i s, 𝓟 (f i_1)) (𝓟 (⋂ i_1 ∈ Insert.insert i s, f i_1))
⊢ Eq.{u + 1} (α := Filter α) (⨅ i ∈ s, 𝓟 (f i)) (𝓟 (⋂ i ∈ s, f i))

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s _ hs => rw [Finset.iInf_insert, Finset.set_biInter_insert, hs, inf_principal]

Premises used: Filter.inf_principal, Finset.iInf_insert, Insert.insert, Finset.set_biInter_insert
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Sort w
inst : Finite ι
f : ι → Set α
intro : ∀ (val : Fintype (PLift ι)), Eq.{u + 1} (α := Filter α) (⨅ (i : ι), 𝓟 (f i)) (𝓟 (⋂ (i : ι), f i))
⊢ Eq.{u + 1} (α := Filter α) (⨅ (i : ι), 𝓟 (f i)) (𝓟 (⋂ (i : ι), f i))

Tactic:
cases nonempty_fintype (PLift ι)

Premises used: PLift, nonempty_fintype
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Sort w
inst : Finite ι
f : ι → Set α
val : Fintype (PLift ι)
intro : Eq.{u + 1} (α := Filter α) (⨅ (i : PLift ι), 𝓟 (f i.down)) (𝓟 (⋂ (i : PLift ι), f i.down))
⊢ Eq.{u + 1} (α := Filter α) (⨅ (i : ι), 𝓟 (f i)) (𝓟 (⋂ (i : ι), f i))

Tactic:
rw [← iInf_plift_down, ← iInter_plift_down]

Premises used: Set.iInter_plift_down, iInf_plift_down
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Sort w
inst : Finite ι
f : ι → Set α
val : Fintype (PLift ι)
⊢ Eq.{u + 1} (α := Filter α) (⨅ (i : PLift ι), 𝓟 (f i.down)) (𝓟 (⋂ (i : PLift ι), f i.down))

Tactic:
simpa using iInf_principal_finset Finset.univ (f <| PLift.down ·)

Premises used: Finset.univ, Filter.iInf_principal_finset, PLift.down
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type w
inst : Finite ι
f : ι → Set α
⊢ Eq.{u + 1} (α := Filter α) (⨅ (i : ι), 𝓟 (f i)) (𝓟 (⋂ (i : ι), f i))

Tactic:
iInf_principal _

Premises used: Filter.iInf_principal
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type w
s : Set ι
hs : s.Finite
f : ι → Set α
⊢ s.Finite

Tactic:
hs
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type w
s : Set ι
hs : s.Finite
f : ι → Set α
lift : ∀ (s : Finset ι), Eq.{u + 1} (α := Filter α) (⨅ i ∈ (↑s : Set ι), 𝓟 (f i)) (𝓟 (⋂ i ∈ (↑s : Set ι), f i))
⊢ Eq.{u + 1} (α := Filter α) (⨅ i ∈ s, 𝓟 (f i)) (𝓟 (⋂ i ∈ s, f i))

Tactic:
lift s to Finset ι using hs

Premises used: Finset
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type w
f : ι → Set α
s : Finset ι
⊢ Eq.{u + 1} (α := Filter α) (⨅ i ∈ (↑s : Set ι), 𝓟 (f i)) (𝓟 (⋂ i ∈ (↑s : Set ι), f i))

Tactic:
mod_cast iInf_principal_finset s f

Premises used: iInf, Filter.iInf_principal_finset, Iff.of_eq, congrArg, Set.iInter, cast, Finset.mem_coe._simp_1, funext, congr, iInf_congr_Prop, Filter.principal, Eq.refl, Eq.symm, Eq, Set.iInter_congr_Prop
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type w
f : ι → Set α
s : Finset ι
⊢ Eq.{u + 1} (α := Filter α) (⨅ i ∈ (↑s : Set ι), 𝓟 (f i)) (𝓟 (⋂ i ∈ (↑s : Set ι), f i))

Tactic:
exact mod_cast iInf_principal_finset s f

Premises used: Filter.iInf_principal_finset
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Sort u_2
inst : Finite ι
l : Filter α
p : ι → α → Prop
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι), p i x) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p i x

Tactic:
simpa only [Filter.Eventually, setOf_forall] using iInter_mem

Premises used: Filter.Eventually, Filter.iInter_mem, Set.setOf_forall
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
I : Set ι
hI : I.Finite
l : Filter α
p : ι → α → Prop
⊢ (∀ᶠ (x : α) in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ (x : α) in l, p i x

Tactic:
simpa only [Filter.Eventually, setOf_forall] using biInter_mem hI

Premises used: Filter.Eventually, Filter.biInter_mem, Set.setOf_forall
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
I : Finset ι
l : Filter α
p : ι → α → Prop
⊢ (∀ᶠ (x : α) in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ (x : α) in l, p i x

Tactic:
I.finite_toSet.eventually_all

Premises used: Set.Finite.eventually_all, Finset.finite_toSet
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Sort u_2
inst : Finite ι
l : Filter α
p : ι → α → Prop
rw : (¬∃ᶠ (x : α) in l, ∃ (i : ι), p i x) ↔ ¬∃ (i : ι), ∃ᶠ (x : α) in l, p i x
⊢ (∃ᶠ (x : α) in l, ∃ (i : ι), p i x) ↔ ∃ (i : ι), ∃ᶠ (x : α) in l, p i x

Tactic:
rw [← not_iff_not]

Premises used: not_iff_not
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Sort u_2
inst : Finite ι
l : Filter α
p : ι → α → Prop
⊢ (¬∃ᶠ (x : α) in l, ∃ (i : ι), p i x) ↔ ¬∃ (i : ι), ∃ᶠ (x : α) in l, p i x

Tactic:
simp
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
I : Set ι
hI : I.Finite
l : Filter α
p : ι → α → Prop
rw : (¬∃ᶠ (x : α) in l, ∃ i ∈ I, p i x) ↔ ¬∃ i ∈ I, ∃ᶠ (x : α) in l, p i x
⊢ (∃ᶠ (x : α) in l, ∃ i ∈ I, p i x) ↔ ∃ i ∈ I, ∃ᶠ (x : α) in l, p i x

Tactic:
rw [← not_iff_not]

Premises used: not_iff_not
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
I : Set ι
hI : I.Finite
l : Filter α
p : ι → α → Prop
⊢ (¬∃ᶠ (x : α) in l, ∃ i ∈ I, p i x) ↔ ¬∃ i ∈ I, ∃ᶠ (x : α) in l, p i x

Tactic:
simp [hI]
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
I : Finset ι
l : Filter α
p : ι → α → Prop
⊢ (∃ᶠ (x : α) in l, ∃ i ∈ I, p i x) ↔ ∃ i ∈ I, ∃ᶠ (x : α) in l, p i x

Tactic:
I.finite_toSet.frequently_exists

Premises used: Finset.finite_toSet, Set.Finite.frequently_exists
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
f : Filter ι
s : ι → Set α
t : Set α
ht : t.Finite
hs : ∀ a ∈ t, ∀ᶠ (i : ι) in f, a ∈ s i
⊢ ∀ᶠ (i : ι) in f, t ⊆ s i

Tactic:
simpa [Set.subset_def, eventually_all_finite ht] using hs

Premises used: Set.subset_def, Filter.eventually_all_finite
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Sort x
l : Filter α
inst : Finite ι
s t : ι → Set α
h : ∀ (i : ι), s i ≤ᶠ[l] t i
⊢ ⋃ (i : ι), s i ≤ᶠ[l] ⋃ (i : ι), t i

Tactic:
(eventually_all.2 h).mono fun _x hx hx' ↦
    let ⟨i, hi⟩ := mem_iUnion.1 hx'; mem_iUnion.2 ⟨i, hx i hi⟩

Premises used: Iff.mpr, Set.mem_iUnion, Filter.eventually_all, Filter.Eventually.mono, Exists.intro, Iff.mp, Filter.EventuallyLE, Set.iUnion, _private.0.Filter.EventuallyLE.iUnion.match_1
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Sort x
l : Filter α
inst : Finite ι
s t : ι → Set α
h : ∀ (i : ι), s i =ᶠ[l] t i
⊢ ⋃ (i : ι), s i =ᶠ[l] ⋃ (i : ι), t i

Tactic:
(EventuallyLE.iUnion fun i ↦ (h i).le).antisymm <| .iUnion fun i ↦ (h i).symm.le

Premises used: Filter.EventuallyLE.iUnion, Filter.EventuallyEq.le, Filter.EventuallyLE.antisymm, Filter.EventuallyEq.symm
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Sort x
l : Filter α
inst : Finite ι
s t : ι → Set α
h : ∀ (i : ι), s i ≤ᶠ[l] t i
⊢ ⋂ (i : ι), s i ≤ᶠ[l] ⋂ (i : ι), t i

Tactic:
(eventually_all.2 h).mono fun _x hx hx' ↦ mem_iInter.2 fun i ↦ hx i (mem_iInter.1 hx' i)

Premises used: Iff.mpr, Filter.eventually_all, Set.mem_iInter, Filter.Eventually.mono, Iff.mp, Filter.EventuallyLE
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Sort x
l : Filter α
inst : Finite ι
s t : ι → Set α
h : ∀ (i : ι), s i =ᶠ[l] t i
⊢ ⋂ (i : ι), s i =ᶠ[l] ⋂ (i : ι), t i

Tactic:
(EventuallyLE.iInter fun i ↦ (h i).le).antisymm <| .iInter fun i ↦ (h i).symm.le

Premises used: Filter.EventuallyLE.iInter, Filter.EventuallyEq.le, Filter.EventuallyLE.antisymm, Filter.EventuallyEq.symm
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
⊢ Finite.{u_2 + 1} (↑s : Type u_2)

Tactic:
have := hs.to_subtype
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
this : Finite.{u_2 + 1} (↑s : Type u_2)
rw : ⋃ (x : (↑s : Type u_2)), f (↑x : ι) ≤ᶠ[l] ⋃ (x : (↑s : Type u_2)), g (↑x : ι)
⊢ ⋃ i ∈ s, f i ≤ᶠ[l] ⋃ i ∈ s, g i

Tactic:
rw [biUnion_eq_iUnion, biUnion_eq_iUnion]

Premises used: Set.biUnion_eq_iUnion
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
this : Finite.{u_2 + 1} (↑s : Type u_2)
⊢ ⋃ (x : (↑s : Type u_2)), f (↑x : ι) ≤ᶠ[l] ⋃ (x : (↑s : Type u_2)), g (↑x : ι)

Tactic:
.iUnion fun i ↦ hle i.1 i.2

Premises used: Filter.EventuallyLE.iUnion, Subtype.val, Subtype.property
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
this : Finite.{u_2 + 1} (↑s : Type u_2)
⊢ ⋃ (x : (↑s : Type u_2)), f (↑x : ι) ≤ᶠ[l] ⋃ (x : (↑s : Type u_2)), g (↑x : ι)

Tactic:
exact .iUnion fun i ↦ hle i.1 i.2
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
heq : ∀ i ∈ s, f i =ᶠ[l] g i
⊢ ⋃ i ∈ s, f i =ᶠ[l] ⋃ i ∈ s, g i

Tactic:
(EventuallyLE.biUnion hs fun i hi ↦ (heq i hi).le).antisymm <|
    .biUnion hs fun i hi ↦ (heq i hi).symm.le

Premises used: Filter.EventuallyEq.le, Filter.EventuallyLE.biUnion, Filter.EventuallyLE.antisymm, Filter.EventuallyEq.symm
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
this : Finite.{u_2 + 1} (↑s : Type u_2)
rw : ⋂ (x : (↑s : Type u_2)), f (↑x : ι) ≤ᶠ[l] ⋂ (x : (↑s : Type u_2)), g (↑x : ι)
⊢ ⋂ i ∈ s, f i ≤ᶠ[l] ⋂ i ∈ s, g i

Tactic:
rw [biInter_eq_iInter, biInter_eq_iInter]

Premises used: Set.biInter_eq_iInter
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
this : Finite.{u_2 + 1} (↑s : Type u_2)
⊢ ⋂ (x : (↑s : Type u_2)), f (↑x : ι) ≤ᶠ[l] ⋂ (x : (↑s : Type u_2)), g (↑x : ι)

Tactic:
.iInter fun i ↦ hle i.1 i.2

Premises used: Filter.EventuallyLE.iInter, Subtype.val, Subtype.property
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
this : Finite.{u_2 + 1} (↑s : Type u_2)
⊢ ⋂ (x : (↑s : Type u_2)), f (↑x : ι) ≤ᶠ[l] ⋂ (x : (↑s : Type u_2)), g (↑x : ι)

Tactic:
exact .iInter fun i ↦ hle i.1 i.2
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
heq : ∀ i ∈ s, f i =ᶠ[l] g i
⊢ ⋂ i ∈ s, f i =ᶠ[l] ⋂ i ∈ s, g i

Tactic:
(EventuallyLE.biInter hs fun i hi ↦ (heq i hi).le).antisymm <|
    .biInter hs fun i hi ↦ (heq i hi).symm.le

Premises used: Filter.EventuallyLE.biInter, Filter.EventuallyEq.le, Filter.EventuallyLE.antisymm, Filter.EventuallyEq.symm
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
l : Filter α
ι : Type u_2
s : Finset ι
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
⊢ ⋃ i ∈ s, f i ≤ᶠ[l] ⋃ i ∈ s, g i

Tactic:
.biUnion s.finite_toSet hle

Premises used: Filter.EventuallyLE.biUnion, Finset.finite_toSet
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
l : Filter α
ι : Type u_2
s : Finset ι
f g : ι → Set α
heq : ∀ i ∈ s, f i =ᶠ[l] g i
⊢ ⋃ i ∈ s, f i =ᶠ[l] ⋃ i ∈ s, g i

Tactic:
.biUnion s.finite_toSet heq

Premises used: Filter.EventuallyEq.biUnion, Finset.finite_toSet
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
l : Filter α
ι : Type u_2
s : Finset ι
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
⊢ ⋂ i ∈ s, f i ≤ᶠ[l] ⋂ i ∈ s, g i

Tactic:
.biInter s.finite_toSet hle

Premises used: Filter.EventuallyLE.biInter, Finset.finite_toSet
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
l : Filter α
ι : Type u_2
s : Finset ι
f g : ι → Set α
heq : ∀ i ∈ s, f i =ᶠ[l] g i
⊢ ⋂ i ∈ s, f i =ᶠ[l] ⋂ i ∈ s, g i

Tactic:
.biInter s.finite_toSet heq

Premises used: Filter.EventuallyEq.biInter, Finset.finite_toSet
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : l.NeBot
a b : β
⊢ (∀ᶠ (x : α) in l, a = b) ↔ a = b

Tactic:
eventually_const

Premises used: Filter.eventually_const
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : l.NeBot
a b : β
⊢ (EventuallyEq.{u_1, u_2} (β := β) l (fun (x : α) ↦ a) fun (x : α) ↦ b) ↔ a = b

Tactic:
@const_eventuallyEq' _ _ _ _ a b

Premises used: Filter.const_eventuallyEq', Filter.EventuallyEq
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l_1 : Filter α
f g h : α → β
l : Filter α
P : l.Germ β
suffices : ∀ (f g : α → β) (b : β), f =ᶠ[l] g → (f =ᶠ[l] fun (x : α) ↦ b) → g =ᶠ[l] fun (x : α) ↦ b
⊢ ∀ (a b : α → β),
    a ≈ b →
      Eq (α := Prop) ((fun (f : α → β) ↦ ∃ (b : β), f =ᶠ[l] fun (x : α) ↦ b) a)
        ((fun (f : α → β) ↦ ∃ (b : β), f =ᶠ[l] fun (x : α) ↦ b) b)

Tactic:
suffices ∀ f g : α → β, ∀ b : β, f =ᶠ[l] g → (f =ᶠ[l] fun _ ↦ b) → (g =ᶠ[l] fun _ ↦ b) from
      fun f g h ↦ propext ⟨fun ⟨b, hb⟩ ↦ ⟨b, this f g b h hb⟩, fun ⟨b, hb⟩ ↦ ⟨b, h.trans hb⟩⟩
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l_1 : Filter α
f g h : α → β
l : Filter α
P : l.Germ β
⊢ ∀ (f g : α → β) (b : β), f =ᶠ[l] g → (f =ᶠ[l] fun (x : α) ↦ b) → g =ᶠ[l] fun (x : α) ↦ b

Tactic:
fun f g b hfg hf ↦ (hfg.symm).trans hf

Premises used: Filter.EventuallyEq.trans, Filter.EventuallyEq.symm
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l_1 : Filter α
f g h : α → β
l : Filter α
P : l.Germ β
⊢ ∀ (f g : α → β) (b : β), f =ᶠ[l] g → (f =ᶠ[l] fun (x : α) ↦ b) → g =ᶠ[l] fun (x : α) ↦ b

Tactic:
exact fun f g b hfg hf ↦ (hfg.symm).trans hf
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : Filter α
b : β
h : ∀ (x' : α), f x' = b
⊢ IsConstant (l := l) (↑f : l.Germ β)

Tactic:
⟨b, Eventually.of_forall h⟩

Premises used: Filter.Eventually.of_forall, Exists.intro, Filter.Germ.IsConstant
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
l : Filter α
b w : β
h : EventuallyEq.{u_1, u_2} (β := β) l (fun (x : α) ↦ b) fun (x : α) ↦ b
⊢ IsConstant.{u_1, u_2} (α := α) (β := β) (l := l) (↑fun (x : α) ↦ b : l.Germ β)

Tactic:
use b
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
f : α → β
g : β → γ
h : IsConstant (l := l) (↑f : l.Germ β)
obtain : ∀ (b : β) (hb : f =ᶠ[l] fun (x : α) ↦ b), IsConstant (l := l) (↑(g ∘ f) : l.Germ γ)
⊢ IsConstant (l := l) (↑(g ∘ f) : l.Germ γ)

Tactic:
obtain ⟨b, hb⟩ := h
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
f : α → β
g : β → γ
b : β
hb : f =ᶠ[l] fun (x : α) ↦ b
⊢ IsConstant (l := l) (↑(g ∘ f) : l.Germ γ)

Tactic:
⟨g b, hb.fun_comp g⟩

Premises used: Exists.intro, Filter.Germ.IsConstant, Filter.EventuallyEq.fun_comp
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
f : α → β
g : β → γ
b : β
hb : f =ᶠ[l] fun (x : α) ↦ b
⊢ IsConstant (l := l) (↑(g ∘ f) : l.Germ γ)

Tactic:
exact ⟨g b, hb.fun_comp g⟩
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
⊢ Eq (α := Quot (α := α → β) (⇑(l.germSetoid β) : (α → β) → (α → β) → Prop))
    (Quot.mk (⇑(l.germSetoid β) : (α → β) → (α → β) → Prop) f) (↑f : l.Germ β)

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Quotient.mk', rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
⊢ Eq (α := Quotient (l.germSetoid β)) (Quotient.mk' f) (↑f : l.Germ β)

Tactic:
rfl

Premises used: Filter.Germ.ofFun, rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
l : Filter α
f : l.Germ β
p : l.Germ β → Prop
h : ∀ (f : α → β), p (↑f : l.Germ β)
⊢ p f

Tactic:
Quotient.inductionOn' f h

Premises used: Quotient.inductionOn'
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
f : l.Germ β
g : l.Germ γ
p : l.Germ β → l.Germ γ → Prop
h : ∀ (f : α → β) (g : α → γ), p (↑f : l.Germ β) (↑g : l.Germ γ)
⊢ p f g

Tactic:
Quotient.inductionOn₂' f g h

Premises used: Quotient.inductionOn₂'
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f : l.Germ β
g : l.Germ γ
h : l.Germ δ
p : l.Germ β → l.Germ γ → l.Germ δ → Prop
H : ∀ (f : α → β) (g : α → γ) (h : α → δ), p (↑f : l.Germ β) (↑g : l.Germ γ) (↑h : l.Germ δ)
⊢ p f g h

Tactic:
Quotient.inductionOn₃' f g h H

Premises used: Quotient.inductionOn₃'
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
lc : Filter γ
F : (α → β) → γ → δ
hF : (l.EventuallyEq ⇒ lc.EventuallyEq) F F
f : α → β
⊢ map' F hF (↑f : l.Germ β) = (↑(F f) : lc.Germ δ)

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Quotient.mk', rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
l : Filter α
f g : α → β
⊢ Eq (α := l.Germ β) (↑f : l.Germ β) (↑g : l.Germ β) ↔ f =ᶠ[l] g

Tactic:
Quotient.eq''

Premises used: Filter.Germ.ofFun, Quotient.eq'', Quotient.mk', Filter.Germ
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
op : β → γ
f : α → β
⊢ Eq (α := l.Germ γ) (map op (↑f : l.Germ β)) (↑(op ∘ f) : l.Germ γ)

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Quotient.mk', Filter.Germ.map, rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
l : Filter α
h :
  ∀ (x : l.Germ β) (f : α → β),
    Eq (α := l.Germ β) (map id (Quot.mk (⇑(l.germSetoid β) : (α → β) → (α → β) → Prop) f))
      (id (Quot.mk (⇑(l.germSetoid β) : (α → β) → (α → β) → Prop) f))
⊢ Eq (α := l.Germ β → l.Germ β) (map id) id

Tactic:
ext ⟨f⟩
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
l : Filter α
x : l.Germ β
f : α → β
⊢ Eq (α := l.Germ β) (map id (Quot.mk (⇑(l.germSetoid β) : (α → β) → (α → β) → Prop) f))
    (id (Quot.mk (⇑(l.germSetoid β) : (α → β) → (α → β) → Prop) f))

Tactic:
rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
op₁ : γ → δ
op₂ : β → γ
f : l.Germ β
⊢ map op₁ (map op₂ f) = map (op₁ ∘ op₂) f

Tactic:
inductionOn f fun _ => rfl

Premises used: Filter.Germ.inductionOn
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g_1 h : α → β
op : β → γ → δ
f f' : α → β
Hf_1 : f ≈ f'
g g' : α → γ
Hg_1 : g ≈ g'
x : α
Hf : f x = f' x
Hg : g x = g' x
⊢ Eq.{u_4 + 1} (α := δ) ((fun (f : α → β) (g : α → γ) (x : α) ↦ op (f x) (g x)) f g x)
    ((fun (f : α → β) (g : α → γ) (x : α) ↦ op (f x) (g x)) f' g' x)

Tactic:
simp only [Hf, Hg]
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
op : β → γ → δ
f : α → β
g : α → γ
⊢ Eq (α := l.Germ δ) (map₂ op (↑f : l.Germ β) (↑g : l.Germ γ)) (↑fun (x : α) ↦ op (f x) (g x) : l.Germ δ)

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Quotient.mk', rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
lb : Filter β
⊢ Germ.Tendsto (l := l) (↑f : l.Germ β) lb ↔ Tendsto f l lb

Tactic:
Iff.rfl

Premises used: Quotient.liftOn', Filter.Germ.Tendsto, Iff.rfl, Filter.Tendsto, Filter.Germ.liftOn
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
f : α → β
lc : Filter γ
g : lc.Germ α
hg : g.Tendsto l
⊢ compTendsto' (↑f : l.Germ β) g hg = map f g

Tactic:
rfl

Premises used: Filter.Germ.compTendsto', Filter.Germ.map', Quotient.map', Filter.Germ.map, rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
f : α → β
lc : Filter γ
g : γ → α
hg : Tendsto g lc l
⊢ compTendsto (↑f : l.Germ β) g hg = (↑(f ∘ g) : lc.Germ β)

Tactic:
rfl

Premises used: Filter.Germ.compTendsto, Filter.Germ.ofFun, Filter.Germ.compTendsto', Filter.Germ.map', Quotient.mk', Filter.Germ.liftOn, Quotient.map', Filter.Germ.map, rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
f : l.Germ β
lc : Filter γ
g : γ → α
hg : Tendsto g lc l
⊢ f.compTendsto' (↑g : lc.Germ α) ⋯ = f.compTendsto g hg

Tactic:
rfl

Premises used: Filter.Germ.compTendsto, rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f g : β → γ
l : Filter α
l' : Filter β
h : f =ᶠ[l'] g
φ : α → β
hφ : Tendsto φ l l'
⊢ Eq (α := l.Germ γ) (↑(f ∘ φ) : l.Germ γ) (↑(g ∘ φ) : l.Germ γ)

Tactic:
EventuallyEq.germ_eq (h.comp_tendsto hφ)

Premises used: Filter.EventuallyEq.comp_tendsto, Filter.EventuallyEq.germ_eq
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
f : α → β
lc : Filter γ
g : γ → α
hf : IsConstant (l := l) (↑f : l.Germ β)
hg : Tendsto g lc l
rcases : ∀ (b : β) (hb : f =ᶠ[l] fun (x : α) ↦ b), IsConstant (l := lc) (↑(f ∘ g) : lc.Germ β)
⊢ IsConstant (l := lc) (↑(f ∘ g) : lc.Germ β)

Tactic:
rcases hf with ⟨b, hb⟩