awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F G : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
inst_4 : Applicative G
inst_5 : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
x : t α
⊢ traverse (Comp.mk ∘ map h ∘ g) x = (Comp.mk ∘ map (traverse h) ∘ traverse g) x

Tactic:
comp_traverse _ _ _

Premises used: LawfulTraversable.comp_traverse, Functor.Comp.mk
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F G : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
inst_4 : Applicative G
inst_5 : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
x : t α
⊢ traverse (Comp.mk ∘ map h ∘ g) x = (Comp.mk ∘ map (traverse h) ∘ traverse g) x

Tactic:
exact comp_traverse _ _ _

Premises used: LawfulTraversable.comp_traverse
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
β γ : Type u
f : β → γ
h : ∀ (x : t β), Id.run (traverse (pure ∘ f) x) = Id.run ((pure ∘ map f) x)
⊢ Eq (α := t β → Id (t γ)) (traverse (pure ∘ f)) (pure ∘ map f)

Tactic:
ext
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
β γ : Type u
f : β → γ
x : t β
⊢ Id.run (traverse (pure ∘ f) x) = Id.run ((pure ∘ map f) x)

Tactic:
traverse_eq_map_id _ _

Premises used: Id, LawfulTraversable.traverse_eq_map_id
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
β γ : Type u
f : β → γ
x : t β
⊢ Id.run (traverse (pure ∘ f) x) = Id.run ((pure ∘ map f) x)

Tactic:
exact traverse_eq_map_id _ _

Premises used: LawfulTraversable.traverse_eq_map_id
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
G : Type u → Type u
inst_2 : Applicative G
inst_3 : LawfulApplicative G
α β γ : Type u
g : α → β
h : β → G γ
h₁ : ∀ (x : t α), traverse (h ∘ g) x = (traverse h ∘ map g) x
⊢ Eq (α := t α → G (t γ)) (traverse (h ∘ g)) (traverse h ∘ map g)

Tactic:
ext
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
G : Type u → Type u
inst_2 : Applicative G
inst_3 : LawfulApplicative G
α β γ : Type u
g : α → β
h : β → G γ
x : t α
h₁ : traverse (h ∘ g) x = traverse h (g <$> x)
h₂ h₃ : traverse (h ∘ g) x = traverse (h ∘ g) x
⊢ traverse (h ∘ g) x = (traverse h ∘ map g) x

Tactic:
rw [comp_apply, traverse_map]

Premises used: Traversable.traverse_map, Function.comp_apply
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
G : Type u → Type u
inst_2 : Applicative G
inst_3 : LawfulApplicative G
α β γ : Type u
g : α → G β
h : β → γ
h₁ : ∀ (x : t α), traverse (map h ∘ g) x = (map (map h) ∘ traverse g) x
⊢ Eq (α := t α → G (t γ)) (traverse (map h ∘ g)) (map (map h) ∘ traverse g)

Tactic:
ext
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
G : Type u → Type u
inst_2 : Applicative G
inst_3 : LawfulApplicative G
α β γ : Type u
g : α → G β
h : β → γ
x : t α
h₁ : traverse (map h ∘ g) x = map h <$> traverse g x
h₂ h₃ : traverse (map h ∘ g) x = traverse (map h ∘ g) x
⊢ traverse (map h ∘ g) x = (map (map h) ∘ traverse g) x

Tactic:
rw [comp_apply, map_traverse]

Premises used: Traversable.map_traverse, Function.comp_apply
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F G : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
inst_4 : Applicative G
inst_5 : LawfulApplicative G
α β : Type u
η : ApplicativeTransformation F G
f : α → F β
h :
  ∀ (x : t α),
    Eq (α := G (t β)) (traverse ((fun {α : Type u} ↦ η.app α) ∘ f) x) (((fun {α : Type u} ↦ η.app α) ∘ traverse f) x)
⊢ Eq (α := t α → G (t β)) (traverse ((fun {α : Type u} ↦ η.app α) ∘ f)) ((fun {α : Type u} ↦ η.app α) ∘ traverse f)

Tactic:
ext
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F G : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
inst_4 : Applicative G
inst_5 : LawfulApplicative G
α β : Type u
η : ApplicativeTransformation F G
f : α → F β
x : t α
h : Eq (α := G (t β)) (traverse ((fun {α : Type u} ↦ η.app α) ∘ f) x) ((fun {α : Type u} ↦ η.app α) (traverse f x))
h₁ h₂ :
  Eq (α := G (t β)) (traverse ((fun {α : Type u} ↦ η.app α) ∘ f) x) (traverse ((fun {α : Type u} ↦ η.app α) ∘ f) x)
⊢ Eq (α := G (t β)) (traverse ((fun {α : Type u} ↦ η.app α) ∘ f) x) (((fun {α : Type u} ↦ η.app α) ∘ traverse f) x)

Tactic:
rw [comp_apply, naturality]

Premises used: LawfulTraversable.naturality, Function.comp_apply
-- Module: Mathlib.Control.ULift
Goal:
α : Sort u
β : Sort v
f : α → β
a : α
⊢ PLift.map f { down := a : PLift α } = { down := f a }

Tactic:
rfl

Premises used: PLift.map, rfl
-- Module: Mathlib.Control.ULift
Goal:
α : Sort u
β : Sort v
f : α → β
x : α
⊢ ({ down := f : PLift (α → β) }.seq fun (x_1 : Unit) ↦ { down := x : PLift α }) = { down := f x }

Tactic:
rfl

Premises used: PLift.seq, rfl
-- Module: Mathlib.Control.ULift
Goal:
α : Sort u
β : Sort v
a : α
f : α → PLift β
⊢ { down := a : PLift α }.bind f = f a

Tactic:
rfl

Premises used: PLift.bind, rfl
-- Module: Mathlib.Control.ULift
Goal:
α : Sort u
β : Type v
b : β
⊢ Eq (α := (t : PLift α) → β) (rec (motive := fun (x : PLift α) ↦ β) fun (x : α) ↦ b) fun (x : PLift α) ↦ b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Control.ULift
Goal:
α : Type u
β : Type v
f : α → β
a : α
⊢ ULift.map.{u, v, u', v'} f { down := a : ULift.{u', u} α } = { down := f a }

Tactic:
rfl

Premises used: ULift.map, rfl
-- Module: Mathlib.Control.ULift
Goal:
α : Type u
β : Type v
f : α → β
x : α
⊢ (ULift.seq.{u_1, u, v, u_2, u_3} { down := f : ULift (α → β) } fun (x_1 : Unit) ↦ { down := x : ULift.{u_3, u} α }) =
    { down := f x }

Tactic:
rfl

Premises used: ULift.seq, rfl
-- Module: Mathlib.Control.ULift
Goal:
α : Type u
β : Type v
a : α
f : α → ULift.{u_1, v} β
⊢ { down := a : ULift.{u_2, u} α }.bind f = f a

Tactic:
rfl

Premises used: ULift.bind, rfl
-- Module: Mathlib.Control.ULift
Goal:
α : Type u
β : Sort v
b : β
⊢ Eq (α := (t : ULift.{u_1, u} α) → β) (rec (motive := fun (x : ULift.{u_1, u} α) ↦ β) fun (x : α) ↦ b)
    fun (x : ULift.{u_1, u} α) ↦ b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Control.ULiftable
Goal:
f : Type u₀ → Type u₁
g : Type (max u₀ v₀) → Type v₁
inst : ULiftable f g
α : Type u₀
x : g (ULift.{v₀, u₀} α)
⊢ up (down x) = x

Tactic:
(ULiftable.congr Equiv.ulift.symm).right_inv _

Premises used: Equiv.right_inv, Equiv.ulift, ULiftable.congr, Equiv.symm
-- Module: Mathlib.Control.ULiftable
Goal:
f : Type u₀ → Type u₁
g : Type (max u₀ v₀) → Type v₁
inst : ULiftable f g
α : Type u₀
x : f α
⊢ down.{v₀, u₀, u₁, v₁} (g := g) (up x) = x

Tactic:
(ULiftable.congr Equiv.ulift.symm).left_inv _

Premises used: Equiv.ulift, ULiftable.congr, Equiv.symm, Equiv.left_inv
-- Module: Mathlib.Control.ULiftable
Goal:
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α : Type v₁
β : Type v₂
e : α ≃ β
f : Except ε α
error :
  ∀ (a : ε),
    Eq (α := Except ε α)
      (Except.map.{u₀, v₂, v₁} (α := β) (⇑e.symm : (a : β) → α)
        (Except.map.{u₀, v₁, v₂} (α := α) (⇑e : (a : α) → β) (Except.error a)))
      (Except.error a)
ok :
  ∀ (a : α),
    Eq (α := Except ε α)
      (Except.map.{u₀, v₂, v₁} (α := β) (⇑e.symm : (a : β) → α) (Except.map (⇑e : (a : α) → β) (Except.ok a)))
      (Except.ok a)
⊢ Except.map.{u₀, v₂, v₁} (α := β) (⇑e.symm : (a : β) → α) (Except.map (⇑e : (a : α) → β) f) = f

Tactic:
cases f
-- Module: Mathlib.Control.ULiftable
Goal:
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α : Type v₁
β : Type v₂
e : α ≃ β
a : ε
⊢ Eq (α := Except ε α)
    (Except.map.{u₀, v₂, v₁} (α := β) (⇑e.symm : (a : β) → α)
      (Except.map.{u₀, v₁, v₂} (α := α) (⇑e : (a : α) → β) (error a)))
    (error a)

Tactic:
simp [Except.map]

Premises used: Except.map
-- Module: Mathlib.Control.ULiftable
Goal:
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α : Type v₁
β : Type v₂
e : α ≃ β
a : α
⊢ Eq (α := Except ε α) (Except.map.{u₀, v₂, v₁} (α := β) (⇑e.symm : (a : β) → α) (Except.map (⇑e : (a : α) → β) (ok a)))
    (ok a)

Tactic:
simp [Except.map]

Premises used: Except.map
-- Module: Mathlib.Control.ULiftable
Goal:
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α : Type v₁
β : Type v₂
e : α ≃ β
f : Except ε β
error :
  ∀ (a : ε),
    Eq (α := Except ε β)
      (Except.map.{u₀, v₁, v₂} (α := α) (⇑e : (a : α) → β)
        (Except.map.{u₀, v₂, v₁} (α := β) (⇑e.symm : (a : β) → α) (Except.error a)))
      (Except.error a)
ok :
  ∀ (a : β),
    Eq (α := Except ε β)
      (Except.map.{u₀, v₁, v₂} (α := α) (⇑e : (a : α) → β) (Except.map (⇑e.symm : (a : β) → α) (Except.ok a)))
      (Except.ok a)
⊢ Except.map.{u₀, v₁, v₂} (α := α) (⇑e : (a : α) → β) (Except.map (⇑e.symm : (a : β) → α) f) = f

Tactic:
cases f
-- Module: Mathlib.Control.ULiftable
Goal:
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α : Type v₁
β : Type v₂
e : α ≃ β
a : ε
⊢ Eq (α := Except ε β)
    (Except.map.{u₀, v₁, v₂} (α := α) (⇑e : (a : α) → β)
      (Except.map.{u₀, v₂, v₁} (α := β) (⇑e.symm : (a : β) → α) (error a)))
    (error a)

Tactic:
simp [Except.map]

Premises used: Except.map
-- Module: Mathlib.Control.ULiftable
Goal:
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α : Type v₁
β : Type v₂
e : α ≃ β
a : β
⊢ Eq (α := Except ε β) (Except.map.{u₀, v₁, v₂} (α := α) (⇑e : (a : α) → β) (Except.map (⇑e.symm : (a : β) → α) (ok a)))
    (ok a)

Tactic:
simp [Except.map]

Premises used: Except.map
-- Module: Mathlib.Control.ULiftable
Goal:
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α : Type u₀
β : Type u₁
e : α ≃ β
f : Option α
none :
  Eq.{u₀ + 1} (α := Option α)
    (Option.map.{u₁, u₀} (α := β) (⇑e.symm : (a : β) → α) (Option.map.{u₀, u₁} (α := α) (⇑e : (a : α) → β) Option.none))
    Option.none
some :
  ∀ (val : α),
    Option.map.{u₁, u₀} (α := β) (⇑e.symm : (a : β) → α) (Option.map (⇑e : (a : α) → β) (Option.some val)) =
      Option.some val
⊢ Option.map.{u₁, u₀} (α := β) (⇑e.symm : (a : β) → α) (Option.map (⇑e : (a : α) → β) f) = f

Tactic:
cases f
-- Module: Mathlib.Control.ULiftable
Goal:
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α : Type u₀
β : Type u₁
e : α ≃ β
⊢ Eq.{u₀ + 1} (α := Option α)
    (Option.map.{u₁, u₀} (α := β) (⇑e.symm : (a : β) → α) (Option.map.{u₀, u₁} (α := α) (⇑e : (a : α) → β) none)) none

Tactic:
simp
-- Module: Mathlib.Control.ULiftable
Goal:
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α : Type u₀
β : Type u₁
e : α ≃ β
val : α
⊢ Option.map.{u₁, u₀} (α := β) (⇑e.symm : (a : β) → α) (Option.map (⇑e : (a : α) → β) (some val)) = some val

Tactic:
simp
-- Module: Mathlib.Control.ULiftable
Goal:
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α : Type u₀
β : Type u₁
e : α ≃ β
f : Option β
none :
  Eq.{u₁ + 1} (α := Option β)
    (Option.map.{u₀, u₁} (α := α) (⇑e : (a : α) → β) (Option.map.{u₁, u₀} (α := β) (⇑e.symm : (a : β) → α) Option.none))
    Option.none
some :
  ∀ (val : β),
    Option.map.{u₀, u₁} (α := α) (⇑e : (a : α) → β) (Option.map (⇑e.symm : (a : β) → α) (Option.some val)) =
      Option.some val
⊢ Option.map.{u₀, u₁} (α := α) (⇑e : (a : α) → β) (Option.map (⇑e.symm : (a : β) → α) f) = f

Tactic:
cases f
-- Module: Mathlib.Control.ULiftable
Goal:
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α : Type u₀
β : Type u₁
e : α ≃ β
⊢ Eq.{u₁ + 1} (α := Option β)
    (Option.map.{u₀, u₁} (α := α) (⇑e : (a : α) → β) (Option.map.{u₁, u₀} (α := β) (⇑e.symm : (a : β) → α) none)) none

Tactic:
simp
-- Module: Mathlib.Control.ULiftable
Goal:
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α : Type u₀
β : Type u₁
e : α ≃ β
val : β
⊢ Option.map.{u₀, u₁} (α := α) (⇑e : (a : α) → β) (Option.map (⇑e.symm : (a : β) → α) (some val)) = some val

Tactic:
simp
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
σ : Type u_3
inst : PartialOrder α
f : σ → α
pt : σ
inf : σ → σ → σ
h₁ : ∀ (a b : σ), f (inf a b) ≤ f a
h₂ : ∀ (a b : σ), f (inf a b) ≤ f b
a : σ
⊢ { f := f, pt := pt, inf := inf, inf_le_left := h₁, inf_le_right := h₂ : CFilter α σ }.f a = f a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst : PartialOrder α
F : CFilter α σ
E : σ ≃ τ
f : σ → α
p : σ
g : σ → σ → σ
h₁ : ∀ (a b : σ), f (g a b) ≤ f a
h₂ : ∀ (a b : σ), f (g a b) ≤ f b
a b : τ
⊢ f ((E.symm : (a : τ) → σ) ((E : (a : σ) → τ) (g ((E.symm : (a : τ) → σ) a) ((E.symm : (a : τ) → σ) b)) : τ)) ≤
    f ((E.symm : (a : τ) → σ) a)

Tactic:
simpa using h₁ (E.symm a) (E.symm b)

Premises used: Equiv.symm, DFunLike.coe
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst : PartialOrder α
F : CFilter α σ
E : σ ≃ τ
f : σ → α
p : σ
g : σ → σ → σ
h₁ : ∀ (a b : σ), f (g a b) ≤ f a
h₂ : ∀ (a b : σ), f (g a b) ≤ f b
a b : τ
⊢ f ((E.symm : (a : τ) → σ) ((E : (a : σ) → τ) (g ((E.symm : (a : τ) → σ) a) ((E.symm : (a : τ) → σ) b)) : τ)) ≤
    f ((E.symm : (a : τ) → σ) b)

Tactic:
simpa using h₂ (E.symm a) (E.symm b)

Premises used: Equiv.symm, DFunLike.coe
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
σ : Type u_3
τ : Type u_4
inst : PartialOrder α
E : σ ≃ τ
F : CFilter α σ
a : τ
mk :
  ∀ (f : σ → α) (pt : σ) (inf : σ → σ → σ) (inf_le_left : ∀ (a b : σ), f (inf a b) ≤ f a)
    (inf_le_right : ∀ (a b : σ), f (inf a b) ≤ f b),
    (ofEquiv E
            { f := f, pt := pt, inf := inf, inf_le_left := inf_le_left, inf_le_right := inf_le_right : CFilter α σ }).f
        a =
      { f := f, pt := pt, inf := inf, inf_le_left := inf_le_left, inf_le_right := inf_le_right : CFilter α σ }.f
        ((E.symm : (a : τ) → σ) a)
⊢ (ofEquiv E F).f a = F.f ((E.symm : (a : τ) → σ) a)

Tactic:
cases F
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
σ : Type u_3
τ : Type u_4
inst : PartialOrder α
E : σ ≃ τ
a : τ
f : σ → α
pt : σ
inf : σ → σ → σ
inf_le_left : ∀ (a b : σ), f (inf a b) ≤ f a
inf_le_right : ∀ (a b : σ), f (inf a b) ≤ f b
⊢ (ofEquiv E { f := f, pt := pt, inf := inf, inf_le_left := inf_le_left, inf_le_right := inf_le_right : CFilter α σ }).f
      a =
    { f := f, pt := pt, inf := inf, inf_le_left := inf_le_left, inf_le_right := inf_le_right : CFilter α σ }.f
      ((E.symm : (a : τ) → σ) a)

Tactic:
rfl
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
σ : Type u_3
F : CFilter.{u_1, u_3} (Set α) σ
a : Set α
⊢ a ∈ F.toFilter ↔ ∃ (b : σ), F.f b ⊆ a

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
f : Filter α
F : Realizer.{u_1, u_5} f
a : Set α
mk :
  ∀ (σ : Type u_5) (F : CFilter.{u_1, u_5} (Set α) σ) (eq : F.toFilter = f),
    a ∈ f ↔
      ∃ (b : { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ),
        { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f b ⊆ a
⊢ a ∈ f ↔ ∃ (b : F.σ), F.F.f b ⊆ a

Tactic:
cases F
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
f : Filter α
a : Set α
σ : Type u_5
F : CFilter.{u_1, u_5} (Set α) σ
eq : F.toFilter = f
mk :
  a ∈ F.toFilter ↔
    ∃ (b : { σ := σ, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.σ),
      { σ := σ, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.F.f b ⊆ a
⊢ a ∈ f ↔
    ∃ (b : { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ),
      { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f b ⊆ a

Tactic:
subst f
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
a : Set α
σ : Type u_5
F : CFilter.{u_1, u_5} (Set α) σ
⊢ a ∈ F.toFilter ↔
    ∃ (b : { σ := σ, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.σ),
      { σ := σ, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.F.f b ⊆ a

Tactic:
rfl
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
x : Set α
⊢ Membership.mem (γ := Set (Set α))
      (sets
        (CFilter.toFilter (σ := (↑f.sets : Type u_1))
          { f := Subtype.val (p := fun (x : Set α) ↦ x ∈ f.sets),
            pt := Subtype.mk (p := fun (x : Set α) ↦ x ∈ f.sets) univ ⋯,
            inf := fun (x x_1 : (↑f.sets : Type u_1)) ↦
              match (motive := (↑f.sets : Type u_1) → (↑f.sets : Type u_1)) x with
              | ⟨val, h₁⟩ =>
                match (motive := (↑f.sets : Type u_1) → (↑f.sets : Type u_1)) x_1 with
                | ⟨val_1, h₂⟩ => Subtype.mk (p := fun (x : Set α) ↦ x ∈ f.sets) (val ∩ val_1) ⋯,
            inf_le_left := ⋯, inf_le_right := ⋯ }))
      x ↔
    x ∈ f.sets

Tactic:
simp [exists_mem_subset_iff]

Premises used: Filter.exists_mem_subset_iff
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
F : Realizer.{u_1, u_5} f
E : Equiv.{u_5 + 1, u_4 + 1} F.σ τ
⊢ (CFilter.ofEquiv E F.F).toFilter = f

Tactic:
Eq.trans ?_ F.eq

Premises used: Filter.Realizer.eq, Eq.trans
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
F : Realizer.{u_1, u_5} f
E : Equiv.{u_5 + 1, u_4 + 1} F.σ τ
refine : (CFilter.ofEquiv E F.F).toFilter = F.F.toFilter
⊢ (CFilter.ofEquiv E F.F).toFilter = f

Tactic:
refine Eq.trans ?_ F.eq

Premises used: Filter.Realizer.eq, Eq.trans
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
F : Realizer.{u_1, u_5} f
E : Equiv.{u_5 + 1, u_4 + 1} F.σ τ
x : Set α
h_1 : x ∈ (CFilter.ofEquiv E F.F).toFilter.sets
s : τ
h : (CFilter.ofEquiv E F.F).f s ⊆ x
⊢ F.F.f ((E.symm : (a : τ) → F.σ) s) ⊆ x

Tactic:
simpa using h
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
F : Realizer.{u_1, u_5} f
E : Equiv.{u_5 + 1, u_4 + 1} F.σ τ
x : Set α
h_1 : x ∈ F.F.toFilter.sets
t : F.σ
h : F.F.f t ⊆ x
⊢ (CFilter.ofEquiv E F.F).f ((E : (a : F.σ) → τ) t) ⊆ x

Tactic:
simp [h]
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
F : Realizer.{u_1, u_5} f
E : Equiv.{u_5 + 1, u_4 + 1} F.σ τ
⊢ (CFilter.ofEquiv E F.F).toFilter = F.F.toFilter

Tactic:
exact filter_eq (Set.ext fun _ ↦
      ⟨fun ⟨s, h⟩ ↦ ⟨E.symm s, by simpa using h⟩, fun ⟨t, h⟩ ↦ ⟨E t, by simp [h]⟩⟩)
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
τ : Type u_4
f : Filter α
F : Realizer.{u_1, u_5} f
E : Equiv.{u_5 + 1, u_4 + 1} F.σ τ
⊢ (F.ofEquiv E).σ = τ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
τ : Type u_4
f : Filter α
F : Realizer.{u_1, u_5} f
E : Equiv.{u_5 + 1, u_4 + 1} F.σ τ
s : τ
⊢ (F.ofEquiv E).F.f s = F.F.f ((E.symm : (a : τ) → F.σ) s)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
s : Set α
⊢ (Realizer.principal s).σ = Unit

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
s : Set α
u : Unit
⊢ (Realizer.principal s).F.f u = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
⊢ σ.{u_1, 0} (α := α) Realizer.top = Unit

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
u : Unit
⊢ Eq.{u_1 + 1} (α := Set α) (CFilter.f (F Realizer.top) u) univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
⊢ σ.{u_1, 0} (α := α) Realizer.bot = Unit

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
u : Unit
⊢ Eq.{u_1 + 1} (α := Set α) (CFilter.f (F Realizer.bot) u) ∅

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
f : Filter α
F : Realizer.{u_1, u_5} f
x : Set β
simp : (∃ (b : F.σ), F.F.f b ⊆ m ⁻¹' x) ↔ m ⁻¹' x ∈ f
⊢ Membership.mem (γ := Set (Set β))
      (sets
        (CFilter.toFilter
          { f := fun (s : F.σ) ↦ m '' F.F.f s, pt := F.F.pt, inf := F.F.inf, inf_le_left := ⋯, inf_le_right := ⋯ :
            CFilter.{u_2, u_5} (Set β) F.σ }))
      x ↔
    x ∈ (map m f).sets

Tactic:
simp only [CFilter.toFilter, image_subset_iff, mem_setOf_eq, Filter.mem_sets, mem_map]

Premises used: CFilter.toFilter, Filter.mem_sets, Set.mem_setOf_eq, Set.image_subset_iff, Filter.mem_map
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
f : Filter α
F : Realizer.{u_1, u_5} f
x : Set β
rw rw₁ : (∃ (b : F.σ), F.F.f b ⊆ m ⁻¹' x) ↔ ∃ (b : F.σ), F.F.f b ⊆ m ⁻¹' x
⊢ (∃ (b : F.σ), F.F.f b ⊆ m ⁻¹' x) ↔ m ⁻¹' x ∈ f

Tactic:
rw [F.mem_sets]

Premises used: Filter.Realizer.mem_sets
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
m : α → β
f : Filter α
F : Realizer.{u_1, u_5} f
⊢ (Realizer.map m F).σ = F.σ

Tactic:
rfl

Premises used: Filter.map, rfl
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
m : α → β
f : Filter α
F : Realizer.{u_1, u_5} f
s : (Realizer.map m F).σ
⊢ (Realizer.map m F).F.f s = m '' F.F.f s

Tactic:
rfl

Premises used: setOf, Set.image, rfl
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
f : Filter β
F : Realizer.{u_2, u_5} f
x : Set α
mk :
  ∀ (σ : Type u_5) (F : CFilter.{u_2, u_5} (Set β) σ) (eq : F.toFilter = f),
    Membership.mem (γ := Set (Set α))
        (sets
          (CFilter.toFilter
            {
              f := fun (s : { σ := σ, F := F, eq := eq : Realizer.{u_2, u_5} f }.σ) ↦
                m ⁻¹' { σ := σ, F := F, eq := eq : Realizer.{u_2, u_5} f }.F.f s,
              pt := { σ := σ, F := F, eq := eq : Realizer.{u_2, u_5} f }.F.pt,
              inf := { σ := σ, F := F, eq := eq : Realizer.{u_2, u_5} f }.F.inf, inf_le_left := ⋯, inf_le_right := ⋯ :
              CFilter.{u_1, u_5} (Set α) { σ := σ, F := F, eq := eq : Realizer.{u_2, u_5} f }.σ }))
        x ↔
      x ∈ (comap m f).sets
⊢ Membership.mem (γ := Set (Set α))
      (sets
        (CFilter.toFilter
          { f := fun (s : F.σ) ↦ m ⁻¹' F.F.f s, pt := F.F.pt, inf := F.F.inf, inf_le_left := ⋯, inf_le_right := ⋯ :
            CFilter.{u_1, u_5} (Set α) F.σ }))
      x ↔
    x ∈ (comap m f).sets

Tactic:
cases F
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
f : Filter β
x : Set α
σ_1 : Type u_5
F : CFilter.{u_2, u_5} (Set β) σ_1
eq : F.toFilter = f
mk :
  Membership.mem (γ := Set (Set α))
      (sets
        (CFilter.toFilter
          {
            f := fun (s : { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_2, u_5} F.toFilter }.σ) ↦
              m ⁻¹' { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_2, u_5} F.toFilter }.F.f s,
            pt := { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_2, u_5} F.toFilter }.F.pt,
            inf := { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_2, u_5} F.toFilter }.F.inf, inf_le_left := ⋯,
            inf_le_right := ⋯ :
            CFilter.{u_1, u_5} (Set α) { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_2, u_5} F.toFilter }.σ }))
      x ↔
    x ∈ (comap m F.toFilter).sets
⊢ Membership.mem (γ := Set (Set α))
      (sets
        (CFilter.toFilter
          {
            f := fun (s : { σ := σ_1, F := F, eq := eq : Realizer.{u_2, u_5} f }.σ) ↦
              m ⁻¹' { σ := σ_1, F := F, eq := eq : Realizer.{u_2, u_5} f }.F.f s,
            pt := { σ := σ_1, F := F, eq := eq : Realizer.{u_2, u_5} f }.F.pt,
            inf := { σ := σ_1, F := F, eq := eq : Realizer.{u_2, u_5} f }.F.inf, inf_le_left := ⋯, inf_le_right := ⋯ :
            CFilter.{u_1, u_5} (Set α) { σ := σ_1, F := F, eq := eq : Realizer.{u_2, u_5} f }.σ }))
      x ↔
    x ∈ (comap m f).sets

Tactic:
subst f