mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∀ (x : ℕ) (x_1 : β a), x_1 ∉ approx (⇑f) x a
x✝ : ℕ
⊢ b ∉ approx (⇑f) x✝ a

Tactic:
;

Goal state after:
case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∀ (x : ℕ) (x_1 : β a), x_1 ∉ approx (⇑f) x a
x✝ : ℕ
⊢ b ∉ approx (⇑f) x✝ a
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: case mk
m : Type u → Type v
α : Type u_1
ρ β : Type u
i : α
apply✝ : α → m β
⊢ goto (mkLabel ρ { apply := apply✝ }) i = monadLift (goto { apply := apply✝ } i)

Tactic:
;

Goal state after:
case mk
m : Type u → Type v
α : Type u_1
ρ β : Type u
i : α
apply✝ : α → m β
⊢ goto (mkLabel ρ { apply := apply✝ }) i = monadLift (goto { apply := apply✝ } i)
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
ρ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : ReaderT ρ m α✝
next✝ : Label ω✝ (ReaderT ρ m) γ✝ → α✝ → ReaderT ρ m ω✝
⊢ (callCC fun f ↦ cmd✝ >>= next✝ f) = do
    let x ← cmd✝
    callCC fun f ↦ next✝ f x

Tactic:
;

Goal state after:
m : Type u → Type v
ρ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : ReaderT ρ m α✝
next✝ : Label ω✝ (ReaderT ρ m) γ✝ → α✝ → ReaderT ρ m ω✝
⊢ (callCC fun f ↦ cmd✝ >>= next✝ f) = do
    let x ← cmd✝
    callCC fun f ↦ next✝ f x
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
ρ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : ReaderT ρ m α✝
next✝ : Label ω✝ (ReaderT ρ m) γ✝ → α✝ → ReaderT ρ m ω✝
⊢ (ReaderT.mk fun r ↦ do
      let x ← cmd✝.run r
      callCC fun f ↦ (next✝ (ReaderT.mkLabel ρ f) x).run r) =
    do
    let x ← cmd✝
    ReaderT.mk fun r ↦ callCC fun f' ↦ (next✝ (ReaderT.mkLabel ρ f') x).run r

Tactic:
;

Goal state after:
m : Type u → Type v
ρ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : ReaderT ρ m α✝
next✝ : Label ω✝ (ReaderT ρ m) γ✝ → α✝ → ReaderT ρ m ω✝
⊢ (ReaderT.mk fun r ↦ do
      let x ← cmd✝.run r
      callCC fun f ↦ (next✝ (ReaderT.mkLabel ρ f) x).run r) =
    do
    let x ← cmd✝
    ReaderT.mk fun r ↦ callCC fun f' ↦ (next✝ (ReaderT.mkLabel ρ f') x).run r
Module: Mathlib.Data.TypeVec

Goal state before:
pp: α : TypeVec.{u_1} 0
i : Fin2 0
x✝ : (α ⊗ α) i
⊢ α.repeatEq i x✝ = nilFun i x✝

Tactic:
;

Goal state after:
α : TypeVec.{u_1} 0
i : Fin2 0
x✝ : (α ⊗ α) i
⊢ α.repeatEq i x✝ = nilFun i x✝
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
ρ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : ReaderT ρ m α✝
next✝ : Label ω✝ (ReaderT ρ m) γ✝ → α✝ → ReaderT ρ m ω✝
ctx✝ : ρ
⊢ (ReaderT.mk fun r ↦ do
          let x ← cmd✝.run r
          callCC fun f ↦ (next✝ (ReaderT.mkLabel ρ f) x).run r).run
      ctx✝ =
    (do
          let x ← cmd✝
          ReaderT.mk fun r ↦ callCC fun f' ↦ (next✝ (ReaderT.mkLabel ρ f') x).run r).run
      ctx✝

Tactic:
;

Goal state after:
m : Type u → Type v
ρ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : ReaderT ρ m α✝
next✝ : Label ω✝ (ReaderT ρ m) γ✝ → α✝ → ReaderT ρ m ω✝
ctx✝ : ρ
⊢ (ReaderT.mk fun r ↦ do
          let x ← cmd✝.run r
          callCC fun f ↦ (next✝ (ReaderT.mkLabel ρ f) x).run r).run
      ctx✝ =
    (do
          let x ← cmd✝
          ReaderT.mk fun r ↦ callCC fun f' ↦ (next✝ (ReaderT.mkLabel ρ f') x).run r).run
      ctx✝
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
ρ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (ReaderT ρ m) β✝ → β✝ → ReaderT ρ m α✝
⊢ (callCC fun f ↦ goto f x✝ >>= dead✝ f) = pure x✝

Tactic:
;

Goal state after:
m : Type u → Type v
ρ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (ReaderT ρ m) β✝ → β✝ → ReaderT ρ m α✝
⊢ (callCC fun f ↦ goto f x✝ >>= dead✝ f) = pure x✝
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
ρ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (ReaderT ρ m) β✝ → β✝ → ReaderT ρ m α✝
ctx✝ : ρ
⊢ (ReaderT.mk fun r ↦ pure x✝).run ctx✝ = (pure x✝).run ctx✝

Tactic:
;

Goal state after:
m : Type u → Type v
ρ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (ReaderT ρ m) β✝ → β✝ → ReaderT ρ m α✝
ctx✝ : ρ
⊢ (ReaderT.mk fun r ↦ pure x✝).run ctx✝ = (pure x✝).run ctx✝
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
ρ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ReaderT ρ m α✝
⊢ (callCC fun x ↦ dummy✝) = dummy✝

Tactic:
;

Goal state after:
m : Type u → Type v
ρ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ReaderT ρ m α✝
⊢ (callCC fun x ↦ dummy✝) = dummy✝
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
ρ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ReaderT ρ m α✝
⊢ (ReaderT.mk fun r ↦ dummy✝.run r) = dummy✝

Tactic:
;

Goal state after:
m : Type u → Type v
ρ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ReaderT ρ m α✝
⊢ (ReaderT.mk fun r ↦ dummy✝.run r) = dummy✝
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
ρ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ReaderT ρ m α✝
ctx✝ : ρ
⊢ (ReaderT.mk fun r ↦ dummy✝.run r).run ctx✝ = dummy✝.run ctx✝

Tactic:
;

Goal state after:
m : Type u → Type v
ρ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ReaderT ρ m α✝
ctx✝ : ρ
⊢ (ReaderT.mk fun r ↦ dummy✝.run r).run ctx✝ = dummy✝.run ctx✝
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
m₁ : Type u₀ → Type v₀
m₂ : Type u₁ → Type v₁
α₁ r₁ : Type u₀
α₂ r₂ : Type u₁
F : m₁ r₁ ≃ m₂ r₂
G : α₁ ≃ α₂
f : ContT r₁ m₁ α₁
r : α₁ → m₁ r₁
⊢ (fun f r ↦ F.symm (f fun x ↦ F (r (G.symm x)))) ((fun f r ↦ F (f fun x ↦ F.symm (r (G x)))) f) r = f r

Tactic:
;

Goal state after:
m : Type u → Type v
m₁ : Type u₀ → Type v₀
m₂ : Type u₁ → Type v₁
α₁ r₁ : Type u₀
α₂ r₂ : Type u₁
F : m₁ r₁ ≃ m₂ r₂
G : α₁ ≃ α₂
f : ContT r₁ m₁ α₁
r : α₁ → m₁ r₁
⊢ (fun f r ↦ F.symm (f fun x ↦ F (r (G.symm x)))) ((fun f r ↦ F (f fun x ↦ F.symm (r (G x)))) f) r = f r
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
m₁ : Type u₀ → Type v₀
m₂ : Type u₁ → Type v₁
α₁ r₁ : Type u₀
α₂ r₂ : Type u₁
F : m₁ r₁ ≃ m₂ r₂
G : α₁ ≃ α₂
f : ContT r₂ m₂ α₂
r : α₂ → m₂ r₂
⊢ (fun f r ↦ F (f fun x ↦ F.symm (r (G x)))) ((fun f r ↦ F.symm (f fun x ↦ F (r (G.symm x)))) f) r = f r

Tactic:
;

Goal state after:
m : Type u → Type v
m₁ : Type u₀ → Type v₀
m₂ : Type u₁ → Type v₁
α₁ r₁ : Type u₀
α₂ r₂ : Type u₁
F : m₁ r₁ ≃ m₂ r₂
G : α₁ ≃ α₂
f : ContT r₂ m₂ α₂
r : α₂ → m₂ r₂
⊢ (fun f r ↦ F (f fun x ↦ F.symm (r (G x)))) ((fun f r ↦ F.symm (f fun x ↦ F (r (G.symm x)))) f) r = f r
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α α' β β' : TypeVec.{u_1} n
f : α ⟹ β
g : α' ⟹ β'
i : Fin2 n
⊢ (prod.fst ⊚ (f ⊗' g)) i = (f ⊚ prod.fst) i

Tactic:
;

Goal state after:
n : ℕ
α α' β β' : TypeVec.{u_1} n
f : α ⟹ β
g : α' ⟹ β'
i : Fin2 n
⊢ (prod.fst ⊚ (f ⊗' g)) i = (f ⊚ prod.fst) i
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α α' β β' : TypeVec.{u_1} n
f : α ⟹ β
g : α' ⟹ β'
i : Fin2 n
⊢ (prod.snd ⊚ (f ⊗' g)) i = (g ⊚ prod.snd) i

Tactic:
;

Goal state after:
n : ℕ
α α' β β' : TypeVec.{u_1} n
f : α ⟹ β
g : α' ⟹ β'
i : Fin2 n
⊢ (prod.snd ⊚ (f ⊗' g)) i = (g ⊚ prod.snd) i
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} n
i : Fin2 n
⊢ (prod.fst ⊚ prod.diag) i = id i

Tactic:
;

Goal state after:
n : ℕ
α : TypeVec.{u_1} n
i : Fin2 n
⊢ (prod.fst ⊚ prod.diag) i = id i
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} n
i : Fin2 n
⊢ (prod.snd ⊚ prod.diag) i = id i

Tactic:
;

Goal state after:
n : ℕ
α : TypeVec.{u_1} n
i : Fin2 n
⊢ (prod.snd ⊚ prod.diag) i = id i
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz.mk
n✝¹ n✝ : ℕ
α✝ β✝ : TypeVec.{u} (n✝ + 1)
fst✝ : α✝.last
snd✝ : β✝.last
⊢ (id ⊗' id) Fin2.fz (fst✝, snd✝) = id Fin2.fz (fst✝, snd✝)

Tactic:
;

Goal state after:
case fz.mk
n✝¹ n✝ : ℕ
α✝ β✝ : TypeVec.{u} (n✝ + 1)
fst✝ : α✝.last
snd✝ : β✝.last
⊢ (id ⊗' id) Fin2.fz (fst✝, snd✝) = id Fin2.fz (fst✝, snd✝)
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : Part α → Part α
hc : ωScottContinuous f
⊢ (toUnitMono { toFun := f, monotone' := ⋯ }) (Part.fix ⇑(toUnitMono { toFun := f, monotone' := ⋯ })) () = f (Fix.fix f)

Tactic:
;

Goal state after:
α : Type u_1
β : α → Type u_2
f : Part α → Part α
hc : ωScottContinuous f
⊢ (toUnitMono { toFun := f, monotone' := ⋯ }) (Part.fix ⇑(toUnitMono { toFun := f, monotone' := ⋯ })) () = f (Fix.fix f)
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
p : α ⟹ «repeat» n Prop
f : β ⟹ Subtype_ p
⊢ id ⊚ f = f

Tactic:
;

Goal state after:
n : ℕ
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
p : α ⟹ «repeat» n Prop
f : β ⟹ Subtype_ p
⊢ id ⊚ f = f
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
α β : Type u
f : α → β
x : t' α
⊢ ⇑(eqv β) <$> pure (f <$> (eqv α).symm x) = pure (Equiv.map eqv f x)

Tactic:
;

Goal state after:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
α β : Type u
f : α → β
x : t' α
⊢ ⇑(eqv β) <$> pure (f <$> (eqv α).symm x) = pure (Equiv.map eqv f x)
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: R : Type
inst✝ : CommRing R
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
⊢ Continuous
    (Sum.elim (fun t ↦ ⟨(t, t), ⋯⟩) fun xy ↦
      ⟨((LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})).hom.hom' (↑xy).1,
          (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})).hom.hom' (↑xy).2),
        ⋯⟩)

Tactic:
;

Goal state after:
R : Type
inst✝ : CommRing R
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
⊢ Continuous
    (Sum.elim (fun t ↦ ⟨(t, t), ⋯⟩) fun xy ↦
      ⟨((LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})).hom.hom' (↑xy).1,
          (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})).hom.hom' (↑xy).2),
        ⋯⟩)
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁶ : Traversable t
inst✝⁵ : LawfulTraversable t
inst✝⁴ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
x✝² : β✝ → F✝ γ✝
x✝¹ : α✝ → G✝ β✝
x✝ : t' α✝
⊢ Comp.mk (Equiv.traverse eqv x✝² <$> Equiv.traverse eqv x✝¹ x✝) = Comp.mk (Equiv.traverse eqv x✝² <$> traverse x✝¹ x✝)

Tactic:
;

Goal state after:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁶ : Traversable t
inst✝⁵ : LawfulTraversable t
inst✝⁴ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
x✝² : β✝ → F✝ γ✝
x✝¹ : α✝ → G✝ β✝
x✝ : t' α✝
⊢ Comp.mk (Equiv.traverse eqv x✝² <$> Equiv.traverse eqv x✝¹ x✝) = Comp.mk (Equiv.traverse eqv x✝² <$> traverse x✝¹ x✝)
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: case e_a
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁶ : Traversable t
inst✝⁵ : LawfulTraversable t
inst✝⁴ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
x✝² : β✝ → F✝ γ✝
x✝¹ : α✝ → G✝ β✝
x✝ : t' α✝
⊢ Equiv.traverse eqv x✝¹ x✝ = traverse x✝¹ x✝

Tactic:
;

Goal state after:
case e_a
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁶ : Traversable t
inst✝⁵ : LawfulTraversable t
inst✝⁴ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
x✝² : β✝ → F✝ γ✝
x✝¹ : α✝ → G✝ β✝
x✝ : t' α✝
⊢ Equiv.traverse eqv x✝¹ x✝ = traverse x✝¹ x✝
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: case mk
α : 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✝ }).f a =
    { f := f✝, pt := pt✝, inf := inf✝, inf_le_left := inf_le_left✝, inf_le_right := inf_le_right✝ }.f (E.symm a)

Tactic:
;

Goal state after:
case mk
α : 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✝ }).f a =
    { f := f✝, pt := pt✝, inf := inf✝, inf_le_left := inf_le_left✝, inf_le_right := inf_le_right✝ }.f (E.symm a)
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: case mk
α : Type u_1
f : Filter α
a : Set α
σ✝ : Type u_5
F✝ : CFilter (Set α) σ✝
eq✝ : F✝.toFilter = f
⊢ a ∈ f ↔ ∃ b, { σ := σ✝, F := F✝, eq := eq✝ }.F.f b ⊆ a

Tactic:
;

Goal state after:
case mk
α : Type u_1
f : Filter α
a : Set α
σ✝ : Type u_5
F✝ : CFilter (Set α) σ✝
eq✝ : F✝.toFilter = f
⊢ a ∈ f ↔ ∃ b, { σ := σ✝, F := F✝, eq := eq✝ }.F.f b ⊆ a
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: case mk
α : Type u_1
a : Set α
σ✝ : Type u_5
F✝ : CFilter (Set α) σ✝
⊢ a ∈ F✝.toFilter ↔ ∃ b, { σ := σ✝, F := F✝, eq := ⋯ }.F.f b ⊆ a

Tactic:
;

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

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
f : Filter β
x✝ : Set α
σ✝ : Type ?u.50
F✝ : CFilter (Set β) σ✝
eq✝ : F✝.toFilter = f
⊢ x✝ ∈
      { f := fun s ↦ m ⁻¹' { σ := σ✝, F := F✝, eq := eq✝ }.F.f s, pt := { σ := σ✝, F := F✝, eq := eq✝ }.F.pt,
            inf := { σ := σ✝, F := F✝, eq := eq✝ }.F.inf, inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ (comap m f).sets

Tactic:
;

Goal state after:
case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
f : Filter β
x✝ : Set α
σ✝ : Type ?u.50
F✝ : CFilter (Set β) σ✝
eq✝ : F✝.toFilter = f
⊢ x✝ ∈
      { f := fun s ↦ m ⁻¹' { σ := σ✝, F := F✝, eq := eq✝ }.F.f s, pt := { σ := σ✝, F := F✝, eq := eq✝ }.F.pt,
            inf := { σ := σ✝, F := F✝, eq := eq✝ }.F.inf, inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ (comap m f).sets
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
G : g.Realizer
x✝ : Set α
σ✝ : Type ?u.88
F✝ : CFilter (Set α) σ✝
eq✝ : F✝.toFilter = f
⊢ x✝ ∈
      {
            f := fun x ↦
              match x with
              | (s, t) => { σ := σ✝, F := F✝, eq := eq✝ }.F.f s ∪ G.F.f t,
            pt := ({ σ := σ✝, F := F✝, eq := eq✝ }.F.pt, G.F.pt),
            inf := fun x x_1 ↦
              match x with
              | (a, a') =>
                match x_1 with
                | (b, b') => ({ σ := σ✝, F := F✝, eq := eq✝ }.F.inf a b, G.F.inf a' b'),
            inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ (f ⊔ g).sets

Tactic:
;

Goal state after:
case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
G : g.Realizer
x✝ : Set α
σ✝ : Type ?u.88
F✝ : CFilter (Set α) σ✝
eq✝ : F✝.toFilter = f
⊢ x✝ ∈
      {
            f := fun x ↦
              match x with
              | (s, t) => { σ := σ✝, F := F✝, eq := eq✝ }.F.f s ∪ G.F.f t,
            pt := ({ σ := σ✝, F := F✝, eq := eq✝ }.F.pt, G.F.pt),
            inf := fun x x_1 ↦
              match x with
              | (a, a') =>
                match x_1 with
                | (b, b') => ({ σ := σ✝, F := F✝, eq := eq✝ }.F.inf a b, G.F.inf a' b'),
            inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ (f ⊔ g).sets
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: case mk
α : Type u_1
σ : Type u_3
τ : Type u_4
E : σ ≃ τ
a : τ
f✝ : σ → Set α
top✝ : α → σ
top_mem✝ : ∀ (x : α), x ∈ f✝ (top✝ x)
inter✝ : (a b : σ) → (x : α) → x ∈ f✝ a ∩ f✝ b → σ
inter_mem✝ : ∀ (a b : σ) (x : α) (h : x ∈ f✝ a ∩ f✝ b), x ∈ f✝ (inter✝ a b x h)
inter_sub✝ : ∀ (a b : σ) (x : α) (h : x ∈ f✝ a ∩ f✝ b), f✝ (inter✝ a b x h) ⊆ f✝ a ∩ f✝ b
⊢ (ofEquiv E
          { f := f✝, top := top✝, top_mem := top_mem✝, inter := inter✝, inter_mem := inter_mem✝,
            inter_sub := inter_sub✝ }).f
      a =
    { f := f✝, top := top✝, top_mem := top_mem✝, inter := inter✝, inter_mem := inter_mem✝, inter_sub := inter_sub✝ }.f
      (E.symm a)

Tactic:
;

Goal state after:
case mk
α : Type u_1
σ : Type u_3
τ : Type u_4
E : σ ≃ τ
a : τ
f✝ : σ → Set α
top✝ : α → σ
top_mem✝ : ∀ (x : α), x ∈ f✝ (top✝ x)
inter✝ : (a b : σ) → (x : α) → x ∈ f✝ a ∩ f✝ b → σ
inter_mem✝ : ∀ (a b : σ) (x : α) (h : x ∈ f✝ a ∩ f✝ b), x ∈ f✝ (inter✝ a b x h)
inter_sub✝ : ∀ (a b : σ) (x : α) (h : x ∈ f✝ a ∩ f✝ b), f✝ (inter✝ a b x h) ⊆ f✝ a ∩ f✝ b
⊢ (ofEquiv E
          { f := f✝, top := top✝, top_mem := top_mem✝, inter := inter✝, inter_mem := inter_mem✝,
            inter_sub := inter_sub✝ }).f
      a =
    { f := f✝, top := top✝, top_mem := top_mem✝, inter := inter✝, inter_mem := inter_mem✝, inter_sub := inter_sub✝ }.f
      (E.symm a)
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
T : TopologicalSpace α
F : Realizer α
this : TopologicalSpace.IsTopologicalBasis (range F.F.f)
⊢ TopologicalSpace.IsTopologicalBasis (range F.F.f)

Tactic:
;

Goal state after:
α : Type u_1
T : TopologicalSpace α
F : Realizer α
this : TopologicalSpace.IsTopologicalBasis (range F.F.f)
⊢ TopologicalSpace.IsTopologicalBasis (range F.F.f)
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
x✝ : Set α
σ✝¹ : Type ?u.88
F✝¹ : CFilter (Set α) σ✝¹
eq✝¹ : F✝¹.toFilter = f
σ✝ : Type ?u.92
F✝ : CFilter (Set α) σ✝
eq✝ : F✝.toFilter = g
⊢ x✝ ∈
      {
            f := fun x ↦
              match x with
              | (s, t) => { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F.f s ∪ { σ := σ✝, F := F✝, eq := eq✝ }.F.f t,
            pt := ({ σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F.pt, { σ := σ✝, F := F✝, eq := eq✝ }.F.pt),
            inf := fun x x_1 ↦
              match x with
              | (a, a') =>
                match x_1 with
                | (b, b') =>
                  ({ σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F.inf a b, { σ := σ✝, F := F✝, eq := eq✝ }.F.inf a' b'),
            inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ (f ⊔ g).sets

Tactic:
;

Goal state after:
case mk.mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
x✝ : Set α
σ✝¹ : Type ?u.88
F✝¹ : CFilter (Set α) σ✝¹
eq✝¹ : F✝¹.toFilter = f
σ✝ : Type ?u.92
F✝ : CFilter (Set α) σ✝
eq✝ : F✝.toFilter = g
⊢ x✝ ∈
      {
            f := fun x ↦
              match x with
              | (s, t) => { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F.f s ∪ { σ := σ✝, F := F✝, eq := eq✝ }.F.f t,
            pt := ({ σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F.pt, { σ := σ✝, F := F✝, eq := eq✝ }.F.pt),
            inf := fun x x_1 ↦
              match x with
              | (a, a') =>
                match x_1 with
                | (b, b') =>
                  ({ σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F.inf a b, { σ := σ✝, F := F✝, eq := eq✝ }.F.inf a' b'),
            inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ (f ⊔ g).sets
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
T : TopologicalSpace α
F : Realizer α
s : Set α
a : α
this : s ∈ 𝓝 a ↔ ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s
⊢ s ∈ 𝓝 a ↔ ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s

Tactic:
;

Goal state after:
α : Type u_1
T : TopologicalSpace α
F : Realizer α
s : Set α
a : α
this : s ∈ 𝓝 a ↔ ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s
⊢ s ∈ 𝓝 a ↔ ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
x✝ : Set α
σ✝¹ : Type ?u.88
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.92
F✝ : CFilter (Set α) σ✝
⊢ x✝ ∈
      {
            f := fun x ↦
              match x with
              | (s, t) => { σ := σ✝¹, F := F✝¹, eq := ⋯ }.F.f s ∪ { σ := σ✝, F := F✝, eq := ⋯ }.F.f t,
            pt := ({ σ := σ✝¹, F := F✝¹, eq := ⋯ }.F.pt, { σ := σ✝, F := F✝, eq := ⋯ }.F.pt),
            inf := fun x x_1 ↦
              match x with
              | (a, a') =>
                match x_1 with
                | (b, b') => ({ σ := σ✝¹, F := F✝¹, eq := ⋯ }.F.inf a b, { σ := σ✝, F := F✝, eq := ⋯ }.F.inf a' b'),
            inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ (F✝¹.toFilter ⊔ F✝.toFilter).sets

Tactic:
;

Goal state after:
case mk.mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
x✝ : Set α
σ✝¹ : Type ?u.88
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.92
F✝ : CFilter (Set α) σ✝
⊢ x✝ ∈
      {
            f := fun x ↦
              match x with
              | (s, t) => { σ := σ✝¹, F := F✝¹, eq := ⋯ }.F.f s ∪ { σ := σ✝, F := F✝, eq := ⋯ }.F.f t,
            pt := ({ σ := σ✝¹, F := F✝¹, eq := ⋯ }.F.pt, { σ := σ✝, F := F✝, eq := ⋯ }.F.pt),
            inf := fun x x_1 ↦
              match x with
              | (a, a') =>
                match x_1 with
                | (b, b') => ({ σ := σ✝¹, F := F✝¹, eq := ⋯ }.F.inf a b, { σ := σ✝, F := F✝, eq := ⋯ }.F.inf a' b'),
            inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ (F✝¹.toFilter ⊔ F✝.toFilter).sets
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
F : Realizer α
s : Set α
a : α
this : (a : Prop) → Decidable a
⊢ (a ∉ s → ∃ b, a ∈ F.F.f b ∧ ∀ z ∈ F.F.f b, z ∉ s) ↔ (∀ (b : F.σ), a ∈ F.F.f b → ∃ z, z ∈ F.F.f b ∩ s) → a ∈ s

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
F : Realizer α
s : Set α
a : α
this : (a : Prop) → Decidable a
⊢ (a ∉ s → ∃ b, a ∈ F.F.f b ∧ ∀ z ∈ F.F.f b, z ∉ s) ↔ (∀ (b : F.σ), a ∈ F.F.f b → ∃ z, z ∈ F.F.f b ∩ s) → a ∈ s