awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.FilterProduct
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : Preorder β
h :
  ∀ (x : (↑φ : Filter α).Germ β) (f : α → β) (x : (↑φ : Filter α).Germ β) (g : α → β),
    LT.lt (α := (↑φ : Filter α).Germ β) (Quot.mk (⇑((↑φ : Filter α).germSetoid β) : (α → β) → (α → β) → Prop) f)
        (Quot.mk (⇑((↑φ : Filter α).germSetoid β) : (α → β) → (α → β) → Prop) g) ↔
      LiftRel (l := (↑φ : Filter α)) (fun (x1 x2 : β) ↦ x1 < x2)
        (Quot.mk (⇑((↑φ : Filter α).germSetoid β) : (α → β) → (α → β) → Prop) f)
        (Quot.mk (⇑((↑φ : Filter α).germSetoid β) : (α → β) → (α → β) → Prop) g)
⊢ Eq (α := (↑φ : Filter α).Germ β → (↑φ : Filter α).Germ β → Prop) (fun (x1 x2 : (↑φ : Filter α).Germ β) ↦ x1 < x2)
    (LiftRel fun (x1 x2 : β) ↦ x1 < x2)

Tactic:
ext ⟨f⟩ ⟨g⟩
-- Module: Mathlib.Order.Filter.FilterProduct
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : Preorder β
x : (↑φ : Filter α).Germ β
f : α → β
x_1 : (↑φ : Filter α).Germ β
g : α → β
⊢ LT.lt (α := (↑φ : Filter α).Germ β) (Quot.mk (⇑((↑φ : Filter α).germSetoid β) : (α → β) → (α → β) → Prop) f)
      (Quot.mk (⇑((↑φ : Filter α).germSetoid β) : (α → β) → (α → β) → Prop) g) ↔
    LiftRel (l := (↑φ : Filter α)) (fun (x1 x2 : β) ↦ x1 < x2)
      (Quot.mk (⇑((↑φ : Filter α).germSetoid β) : (α → β) → (α → β) → Prop) f)
      (Quot.mk (⇑((↑φ : Filter α).germSetoid β) : (α → β) → (α → β) → Prop) g)

Tactic:
coe_lt

Premises used: Filter.Germ.ofFun, Filter.Germ.coe_lt, Set.Mem, Filter.Eventually, setOf, Filter.Germ.LiftRel, Quotient.mk', Quotient.liftOn₂'
-- Module: Mathlib.Order.Filter.FilterProduct
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : Preorder β
x : (↑φ : Filter α).Germ β
f : α → β
x_1 : (↑φ : Filter α).Germ β
g : α → β
⊢ LT.lt (α := (↑φ : Filter α).Germ β) (Quot.mk (⇑((↑φ : Filter α).germSetoid β) : (α → β) → (α → β) → Prop) f)
      (Quot.mk (⇑((↑φ : Filter α).germSetoid β) : (α → β) → (α → β) → Prop) g) ↔
    LiftRel (l := (↑φ : Filter α)) (fun (x1 x2 : β) ↦ x1 < x2)
      (Quot.mk (⇑((↑φ : Filter α).germSetoid β) : (α → β) → (α → β) → Prop) f)
      (Quot.mk (⇑((↑φ : Filter α).germSetoid β) : (α → β) → (α → β) → Prop) g)

Tactic:
exact coe_lt

Premises used: Filter.Germ.coe_lt
-- Module: Mathlib.Order.Filter.FilterProduct
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : LE β
inst_1 : Std.Total fun (x1 x2 : β) ↦ x1 ≤ x2
⊢ Std.Total fun (x1 x2 : (↑φ : Filter α).Germ β) ↦ x1 ≤ x2

Tactic:
⟨fun f g =>
    inductionOn₂ f g fun _f _g => eventually_or.1 <| Eventually.of_forall fun _x => total_of _ _ _⟩

Premises used: Filter.Germ.inductionOn₂, Std.Total.mk
-- Module: Mathlib.Order.Filter.FilterProduct
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : LinearOrder β
x y : (↑φ : Filter α).Germ β
a b : α → β
inl :
  ∀ (h : LE.le (α := (↑φ : Filter α).Germ β) (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β)),
    Eq (α := (↑φ : Filter α).Germ β) (max (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
      (map₂ max (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
inr :
  ∀ (h : LE.le (α := (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β) (↑a : (↑φ : Filter α).Germ β)),
    Eq (α := (↑φ : Filter α).Germ β) (max (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
      (map₂ max (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
⊢ Eq (α := (↑φ : Filter α).Germ β) (max (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
    (map₂ max (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))

Tactic:
rcases le_total (a : β*) b with h | h
-- Module: Mathlib.Order.Filter.FilterProduct
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : LinearOrder β
x y : (↑φ : Filter α).Germ β
a b : α → β
h : LE.le (α := (↑φ : Filter α).Germ β) (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β)
inl : b =ᶠ[(↑φ : Filter α)] fun (x : α) ↦ max (a x) (b x)
⊢ Eq (α := (↑φ : Filter α).Germ β) (max (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
    (map₂ max (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))

Tactic:
rw [max_eq_right h, map₂_coe, coe_eq]

Premises used: Filter.Germ.map₂_coe, Filter.Germ.coe_eq, max_eq_right
-- Module: Mathlib.Order.Filter.FilterProduct
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : LinearOrder β
x y : (↑φ : Filter α).Germ β
a b : α → β
h : LE.le (α := (↑φ : Filter α).Germ β) (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β)
⊢ b =ᶠ[(↑φ : Filter α)] fun (x : α) ↦ max (a x) (b x)

Tactic:
h.mono fun i hi => (max_eq_right hi).symm

Premises used: Filter.EventuallyEq, Filter.Eventually.mono, max_eq_right, Eq.symm
-- Module: Mathlib.Order.Filter.FilterProduct
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : LinearOrder β
x y : (↑φ : Filter α).Germ β
a b : α → β
h : LE.le (α := (↑φ : Filter α).Germ β) (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β)
⊢ b =ᶠ[(↑φ : Filter α)] fun (x : α) ↦ max (a x) (b x)

Tactic:
exact h.mono fun i hi => (max_eq_right hi).symm

Premises used: Filter.Eventually.mono, max_eq_right, Eq.symm
-- Module: Mathlib.Order.Filter.FilterProduct
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : LinearOrder β
x y : (↑φ : Filter α).Germ β
a b : α → β
h : LE.le (α := (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β) (↑a : (↑φ : Filter α).Germ β)
inr : a =ᶠ[(↑φ : Filter α)] fun (x : α) ↦ max (a x) (b x)
⊢ Eq (α := (↑φ : Filter α).Germ β) (max (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
    (map₂ max (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))

Tactic:
rw [max_eq_left h, map₂_coe, coe_eq]

Premises used: Filter.Germ.map₂_coe, Filter.Germ.coe_eq, max_eq_left
-- Module: Mathlib.Order.Filter.FilterProduct
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : LinearOrder β
x y : (↑φ : Filter α).Germ β
a b : α → β
h : LE.le (α := (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β) (↑a : (↑φ : Filter α).Germ β)
⊢ a =ᶠ[(↑φ : Filter α)] fun (x : α) ↦ max (a x) (b x)

Tactic:
h.mono fun i hi => (max_eq_left hi).symm

Premises used: Filter.EventuallyEq, max_eq_left, Filter.Eventually.mono, Eq.symm
-- Module: Mathlib.Order.Filter.FilterProduct
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : LinearOrder β
x y : (↑φ : Filter α).Germ β
a b : α → β
h : LE.le (α := (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β) (↑a : (↑φ : Filter α).Germ β)
⊢ a =ᶠ[(↑φ : Filter α)] fun (x : α) ↦ max (a x) (b x)

Tactic:
exact h.mono fun i hi => (max_eq_left hi).symm

Premises used: max_eq_left, Filter.Eventually.mono, Eq.symm
-- Module: Mathlib.Order.Filter.FilterProduct
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : (↑φ : Filter α).Germ β
a b : α → β
inl :
  ∀ (h : LE.le (α := (↑φ : Filter α).Germ β) (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β)),
    Eq (α := (↑φ : Filter α).Germ β) (min (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
      (map₂ min (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
inr :
  ∀ (h : LE.le (α := (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β) (↑a : (↑φ : Filter α).Germ β)),
    Eq (α := (↑φ : Filter α).Germ β) (min (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
      (map₂ min (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
⊢ Eq (α := (↑φ : Filter α).Germ β) (min (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
    (map₂ min (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))

Tactic:
rcases le_total (a : β*) b with h | h
-- Module: Mathlib.Order.Filter.FilterProduct
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : (↑φ : Filter α).Germ β
a b : α → β
h : LE.le (α := (↑φ : Filter α).Germ β) (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β)
inl : a =ᶠ[(↑φ : Filter α)] fun (x : α) ↦ min (a x) (b x)
⊢ Eq (α := (↑φ : Filter α).Germ β) (min (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
    (map₂ min (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))

Tactic:
rw [min_eq_left h, map₂_coe, coe_eq]

Premises used: Filter.Germ.map₂_coe, Filter.Germ.coe_eq, min_eq_left
-- Module: Mathlib.Order.Filter.FilterProduct
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : (↑φ : Filter α).Germ β
a b : α → β
h : LE.le (α := (↑φ : Filter α).Germ β) (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β)
⊢ a =ᶠ[(↑φ : Filter α)] fun (x : α) ↦ min (a x) (b x)

Tactic:
h.mono fun i hi => (min_eq_left hi).symm

Premises used: Filter.EventuallyEq, Filter.Eventually.mono, min_eq_left, Eq.symm
-- Module: Mathlib.Order.Filter.FilterProduct
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : (↑φ : Filter α).Germ β
a b : α → β
h : LE.le (α := (↑φ : Filter α).Germ β) (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β)
⊢ a =ᶠ[(↑φ : Filter α)] fun (x : α) ↦ min (a x) (b x)

Tactic:
exact h.mono fun i hi => (min_eq_left hi).symm

Premises used: Filter.Eventually.mono, min_eq_left, Eq.symm
-- Module: Mathlib.Order.Filter.FilterProduct
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : (↑φ : Filter α).Germ β
a b : α → β
h : LE.le (α := (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β) (↑a : (↑φ : Filter α).Germ β)
inr : b =ᶠ[(↑φ : Filter α)] fun (x : α) ↦ min (a x) (b x)
⊢ Eq (α := (↑φ : Filter α).Germ β) (min (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
    (map₂ min (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))

Tactic:
rw [min_eq_right h, map₂_coe, coe_eq]

Premises used: Filter.Germ.map₂_coe, Filter.Germ.coe_eq, min_eq_right
-- Module: Mathlib.Order.Filter.FilterProduct
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : (↑φ : Filter α).Germ β
a b : α → β
h : LE.le (α := (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β) (↑a : (↑φ : Filter α).Germ β)
⊢ b =ᶠ[(↑φ : Filter α)] fun (x : α) ↦ min (a x) (b x)

Tactic:
h.mono fun i hi => (min_eq_right hi).symm

Premises used: Filter.EventuallyEq, min_eq_right, Filter.Eventually.mono, Eq.symm
-- Module: Mathlib.Order.Filter.FilterProduct
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : (↑φ : Filter α).Germ β
a b : α → β
h : LE.le (α := (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β) (↑a : (↑φ : Filter α).Germ β)
⊢ b =ᶠ[(↑φ : Filter α)] fun (x : α) ↦ min (a x) (b x)

Tactic:
exact h.mono fun i hi => (min_eq_right hi).symm

Premises used: min_eq_right, Filter.Eventually.mono, Eq.symm
-- Module: Mathlib.Order.Filter.FilterProduct
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : AddCommGroup β
inst_1 : LinearOrder β
x : (↑φ : Filter α).Germ β
⊢ |x| = map abs x

Tactic:
inductionOn x fun _a => rfl

Premises used: Filter.Germ.inductionOn
-- Module: Mathlib.Order.Filter.FilterProduct
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : LinearOrder β
x y : β
rw :
  Eq (α := (↑φ : Filter α).Germ β) (↑(max x y) : (↑φ : Filter α).Germ β)
    (map₂ max (↑x : (↑φ : Filter α).Germ β) (↑y : (↑φ : Filter α).Germ β))
rw₁ rw₂ : Eq (α := (↑φ : Filter α).Germ β) (↑(max x y) : (↑φ : Filter α).Germ β) (↑(max x y) : (↑φ : Filter α).Germ β)
⊢ Eq (α := (↑φ : Filter α).Germ β) (↑(max x y) : (↑φ : Filter α).Germ β)
    (max (↑x : (↑φ : Filter α).Germ β) (↑y : (↑φ : Filter α).Germ β))

Tactic:
rw [max_def, map₂_const]

Premises used: Filter.Germ.map₂_const, Filter.Germ.max_def
-- Module: Mathlib.Order.Filter.FilterProduct
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : LinearOrder β
x y : β
rw :
  Eq (α := (↑φ : Filter α).Germ β) (↑(min x y) : (↑φ : Filter α).Germ β)
    (map₂ min (↑x : (↑φ : Filter α).Germ β) (↑y : (↑φ : Filter α).Germ β))
rw₁ rw₂ : Eq (α := (↑φ : Filter α).Germ β) (↑(min x y) : (↑φ : Filter α).Germ β) (↑(min x y) : (↑φ : Filter α).Germ β)
⊢ Eq (α := (↑φ : Filter α).Germ β) (↑(min x y) : (↑φ : Filter α).Germ β)
    (min (↑x : (↑φ : Filter α).Germ β) (↑y : (↑φ : Filter α).Germ β))

Tactic:
rw [min_def, map₂_const]

Premises used: Filter.Germ.map₂_const, Filter.Germ.min_def
-- Module: Mathlib.Order.Filter.FilterProduct
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : AddCommGroup β
inst_1 : LinearOrder β
x : β
rw : Eq (α := (↑φ : Filter α).Germ β) (↑|x| : (↑φ : Filter α).Germ β) (map abs (↑x : (↑φ : Filter α).Germ β))
rw₁ rw₂ : Eq (α := (↑φ : Filter α).Germ β) (↑|x| : (↑φ : Filter α).Germ β) (↑|x| : (↑φ : Filter α).Germ β)
⊢ Eq (α := (↑φ : Filter α).Germ β) (↑|x| : (↑φ : Filter α).Germ β) |(↑x : (↑φ : Filter α).Germ β)|

Tactic:
rw [abs_def, map_const]

Premises used: Filter.Germ.map_const, Filter.Germ.abs_def
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
f : Filter α
β : Type v
s : β → Set α
is : Set β
⊢ ⋂ (i : β), ⋂ (_ : Membership.mem (γ := Set β) ∅ i), s i ∈ f ↔ ∀ (i : β), Membership.mem (γ := Set β) ∅ i → s i ∈ f

Tactic:
simp
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
f : Filter α
β : Type v
s : β → Set α
is : Set β
a : β
s_1 : Set β
h : a ∉ s_1
hs_1 : s_1.Finite
hs : ⋂ i ∈ s_1, s i ∈ f ↔ ∀ i ∈ s_1, s i ∈ f
⊢ ⋂ i ∈ insert a s_1, s i ∈ f ↔ ∀ i ∈ insert a s_1, s i ∈ f

Tactic:
simp [hs]
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
f : Filter α
β : Type v
s : β → Set α
is : Set β
hf : is.Finite
empty :
  ⋂ (i : β), ⋂ (_ : Membership.mem (γ := Set β) ∅ i), s i ∈ f ↔ ∀ (i : β), Membership.mem (γ := Set β) ∅ i → s i ∈ f
insert :
  ∀ {a : β} {s_1 : Set β},
    a ∉ s_1 →
      s_1.Finite →
        ∀ (hs : ⋂ i ∈ s_1, s i ∈ f ↔ ∀ i ∈ s_1, s i ∈ f),
          ⋂ i ∈ Insert.insert a s_1, s i ∈ f ↔ ∀ i ∈ Insert.insert a s_1, s i ∈ f
⊢ ⋂ i ∈ is, s i ∈ f ↔ ∀ i ∈ is, s i ∈ f

Tactic:
induction is, hf using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ hs => simp [hs]

Premises used: Insert.insert
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
f : Filter α
β : Type v
s : β → Set α
is : Finset β
⊢ ⋂ i ∈ is, s i ∈ f ↔ ∀ i ∈ is, s i ∈ f

Tactic:
biInter_mem is.finite_toSet

Premises used: Set.Mem, Filter.biInter_mem, Finset.finite_toSet
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
f : Filter α
s : Set (Set α)
hfin : s.Finite
rw : ⋂ i ∈ s, i ∈ f ↔ ∀ U ∈ s, U ∈ f
rw₁ rw₂ : (∀ i ∈ s, i ∈ f) ↔ ∀ U ∈ s, U ∈ f
⊢ ⋂₀ s ∈ f ↔ ∀ U ∈ s, U ∈ f

Tactic:
rw [sInter_eq_biInter, biInter_mem hfin]

Premises used: Set.sInter_eq_biInter, Filter.biInter_mem
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
f : Filter α
β : Sort v
s : β → Set α
inst : Finite β
⊢ ⋂ (i : β), s i ∈ f ↔ ∀ (i : β), s i ∈ f

Tactic:
(sInter_mem (finite_range _)).trans forall_mem_range

Premises used: iInf, Set.forall_mem_range, Set.Mem, Set.iInter, Set.finite_range, Iff.trans, Filter.sInter_mem
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
s : Set (Set α)
U : Set α
mp : U ∈ generate s → ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U
mpr : (∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U) → U ∈ generate s
⊢ U ∈ generate s ↔ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U

Tactic:
constructor
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
s : Set (Set α)
U V : Set α
V_in : V ∈ s
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ V

Tactic:
⟨{V}, singleton_subset_iff.2 V_in, finite_singleton _, (sInter_singleton _).subset⟩

Premises used: Iff.mpr, Set.singleton_subset_iff, Eq.subset, And.intro, Set.sInter_singleton, Exists.intro, Singleton.singleton, Set.finite_singleton
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
s : Set (Set α)
U V : Set α
V_in : V ∈ s
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ V

Tactic:
exact ⟨{V}, singleton_subset_iff.2 V_in, finite_singleton _, (sInter_singleton _).subset⟩
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
s : Set (Set α)
U : Set α
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ univ

Tactic:
⟨∅, empty_subset _, finite_empty, subset_univ _⟩

Premises used: Set.finite_empty, Set.subset_univ, And.intro, Set.empty_subset, Exists.intro, EmptyCollection.emptyCollection
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
s : Set (Set α)
U : Set α
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ univ

Tactic:
exact ⟨∅, empty_subset _, finite_empty, subset_univ _⟩
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
s : Set (Set α)
U s_1 t : Set α
h : GenerateSets s s_1
hVW : s_1 ⊆ t
hV : ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ s_1
mp : ∀ (t_1 : Set (Set α)) (hts : t_1 ⊆ s) (ht : t_1.Finite) (htV : ⋂₀ t_1 ⊆ s_1), ∃ t_2 ⊆ s, t_2.Finite ∧ ⋂₀ t_2 ⊆ t
⊢ ∃ t_1 ⊆ s, t_1.Finite ∧ ⋂₀ t_1 ⊆ t

Tactic:
rcases hV with ⟨t, hts, ht, htV⟩
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
s : Set (Set α)
U s_1 t_1 : Set α
h : GenerateSets s s_1
hVW : s_1 ⊆ t_1
t : Set (Set α)
hts : t ⊆ s
ht : t.Finite
htV : ⋂₀ t ⊆ s_1
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ t_1

Tactic:
⟨t, hts, ht, htV.trans hVW⟩

Premises used: HasSubset.Subset.trans, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
s : Set (Set α)
U s_1 t_1 : Set α
h : GenerateSets s s_1
hVW : s_1 ⊆ t_1
t : Set (Set α)
hts : t ⊆ s
ht : t.Finite
htV : ⋂₀ t ⊆ s_1
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ t_1

Tactic:
exact ⟨t, hts, ht, htV.trans hVW⟩
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
s : Set (Set α)
U s_1 t : Set α
h : GenerateSets s s_1
h_1 : GenerateSets s t
hV : ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ s_1
hW : ∃ t_1 ⊆ s, t_1.Finite ∧ ⋂₀ t_1 ⊆ t
mp :
  ∀ (t_1 : Set (Set α)) (hts : t_1 ⊆ s) (ht : t_1.Finite) (htV : ⋂₀ t_1 ⊆ s_1) (u : Set (Set α)) (hus : u ⊆ s)
    (hu : u.Finite) (huW : ⋂₀ u ⊆ t), ∃ t_2 ⊆ s, t_2.Finite ∧ ⋂₀ t_2 ⊆ s_1 ∩ t
⊢ ∃ t_1 ⊆ s, t_1.Finite ∧ ⋂₀ t_1 ⊆ s_1 ∩ t

Tactic:
rcases hV, hW with ⟨⟨t, hts, ht, htV⟩, u, hus, hu, huW⟩
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
s : Set (Set α)
U s_1 t_1 : Set α
h : GenerateSets s s_1
h_1 : GenerateSets s t_1
t : Set (Set α)
hts : t ⊆ s
ht : t.Finite
htV : ⋂₀ t ⊆ s_1
u : Set (Set α)
hus : u ⊆ s
hu : u.Finite
huW : ⋂₀ u ⊆ t_1
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ s_1 ∩ t_1

Tactic:
⟨t ∪ u, union_subset hts hus, ht.union hu,
          (sInter_union _ _).subset.trans <| inter_subset_inter htV huW⟩

Premises used: Set.Finite.union, HasSubset.Subset.trans, Set.inter_subset_inter, Set.sInter_union, Set.union_subset, Eq.subset, And.intro, Exists.intro, Union.union
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
s : Set (Set α)
U s_1 t_1 : Set α
h : GenerateSets s s_1
h_1 : GenerateSets s t_1
t : Set (Set α)
hts : t ⊆ s
ht : t.Finite
htV : ⋂₀ t ⊆ s_1
u : Set (Set α)
hus : u ⊆ s
hu : u.Finite
huW : ⋂₀ u ⊆ t_1
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ s_1 ∩ t_1

Tactic:
exact
        ⟨t ∪ u, union_subset hts hus, ht.union hu,
          (sInter_union _ _).subset.trans <| inter_subset_inter htV huW⟩
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
s : Set (Set α)
U : Set α
h : U ∈ generate s
mp : ∀ {V : Set α} (V_in : V ∈ s), ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ V
mp₁ : ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ univ
mp₂ :
  ∀ {s_1 t : Set α},
    GenerateSets s s_1 → ∀ (hVW : s_1 ⊆ t) (hV : ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ s_1), ∃ t_1 ⊆ s, t_1.Finite ∧ ⋂₀ t_1 ⊆ t
mp₃ :
  ∀ {s_1 t : Set α},
    GenerateSets s s_1 →
      GenerateSets s t →
        ∀ (hV : ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ s_1) (hW : ∃ t_1 ⊆ s, t_1.Finite ∧ ⋂₀ t_1 ⊆ t),
          ∃ t_1 ⊆ s, t_1.Finite ∧ ⋂₀ t_1 ⊆ s_1 ∩ t
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U

Tactic:
induction h with
    | @basic V V_in =>
      exact ⟨{V}, singleton_subset_iff.2 V_in, finite_singleton _, (sInter_singleton _).subset⟩
    | univ => exact ⟨∅, empty_subset _, finite_empty, subset_univ _⟩
    | superset _ hVW hV =>
      rcases hV with ⟨t, hts, ht, htV⟩
      exact ⟨t, hts, ht, htV.trans hVW⟩
    | inter _ _ hV hW =>
      rcases hV, hW with ⟨⟨t, hts, ht, htV⟩, u, hus, hu, huW⟩
      exact
        ⟨t ∪ u, union_subset hts hus, ht.union hu,
          (sInter_union _ _).subset.trans <| inter_subset_inter htV huW⟩

Premises used: Set.univ
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
s : Set (Set α)
U : Set α
h : ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U
mpr : ∀ (t : Set (Set α)) (hts : t ⊆ s) (tfin : t.Finite) (h : ⋂₀ t ⊆ U), U ∈ generate s
⊢ U ∈ generate s

Tactic:
rcases h with ⟨t, hts, tfin, h⟩
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
s : Set (Set α)
U : Set α
t : Set (Set α)
hts : t ⊆ s
tfin : t.Finite
h : ⋂₀ t ⊆ U
⊢ U ∈ generate s

Tactic:
mem_of_superset ((sInter_mem tfin).2 fun V hV => GenerateSets.basic <| hts hV) h

Premises used: Iff.mpr, Filter.sInter_mem, Filter.GenerateSets.basic, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
s : Set (Set α)
U : Set α
t : Set (Set α)
hts : t ⊆ s
tfin : t.Finite
h : ⋂₀ t ⊆ U
⊢ U ∈ generate s

Tactic:
exact mem_of_superset ((sInter_mem tfin).2 fun V hV => GenerateSets.basic <| hts hV) h

Premises used: Iff.mpr, Filter.sInter_mem, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
I_fin : I.Finite
V : (↑I : Type u_2) → Set α
hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)
hU : ⋂ (i : (↑I : Type u_2)), V i ⊆ U
haveI : ∀ (this : Fintype (↑I : Type u_2)), Membership.mem (γ := Filter α) (⨅ (i : ι), s i) U
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), s i) U

Tactic:
haveI := I_fin.fintype
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
I_fin : I.Finite
V : (↑I : Type u_2) → Set α
hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)
hU : ⋂ (i : (↑I : Type u_2)), V i ⊆ U
this : Fintype (↑I : Type u_2)
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), s i) U

Tactic:
mem_of_superset (iInter_mem.2 fun i => ?_) hU

Premises used: Iff.mpr, Filter.iInter_mem, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
I_fin : I.Finite
V : (↑I : Type u_2) → Set α
hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)
hU : ⋂ (i : (↑I : Type u_2)), V i ⊆ U
this : Fintype (↑I : Type u_2)
refine : ∀ (i : (↑I : Type u_2)), Membership.mem (γ := Filter α) (⨅ (i : ι), s i) (V i)
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), s i) U

Tactic:
refine mem_of_superset (iInter_mem.2 fun i => ?_) hU

Premises used: Iff.mpr, Filter.iInter_mem, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
I_fin : I.Finite
V : (↑I : Type u_2) → Set α
hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)
hU : ⋂ (i : (↑I : Type u_2)), V i ⊆ U
this : Fintype (↑I : Type u_2)
i : (↑I : Type u_2)
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), s i) (V i)

Tactic:
mem_iInf_of_mem (i : ι) (hV _)

Premises used: Filter.mem_iInf_of_mem, Subtype.val
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
I_fin : I.Finite
V : (↑I : Type u_2) → Set α
hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)
hU : ⋂ (i : (↑I : Type u_2)), V i ⊆ U
this : Fintype (↑I : Type u_2)
i : (↑I : Type u_2)
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), s i) (V i)

Tactic:
exact mem_iInf_of_mem (i : ι) (hV _)

Premises used: Filter.mem_iInf_of_mem, Subtype.val
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
mp :
  Membership.mem (γ := Filter α) (⨅ (i : ι), s i) U →
    ∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : (↑I : Type u_2) → Set α), (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i
mpr :
  (∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : (↑I : Type u_2) → Set α),
          (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i) →
    Membership.mem (γ := Filter α) (⨅ (i : ι), s i) U
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), s i) U ↔
    ∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : (↑I : Type u_2) → Set α), (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i

Tactic:
constructor
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
mp :
  (∃ t ⊆ ⋃ (i : ι), (s i).sets, t.Finite ∧ ⋂₀ t ⊆ U) →
    ∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : (↑I : Type u_2) → Set α), (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), s i) U →
    ∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : (↑I : Type u_2) → Set α), (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i

Tactic:
rw [iInf_eq_generate, mem_generate_iff]

Premises used: Filter.mem_generate_iff, Filter.iInf_eq_generate