mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.map_sup : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (S T : AddSubmonoid M) (f : F),
  AddSubmonoid.map f (S ⊔ T) = AddSubmonoid.map f S ⊔ AddSubmonoid.map f T
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.sameCycle_comm : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle x y ↔ f.SameCycle y x
-- Init.Data.String.Lemmas.Pattern.Split.Pred
String.toList_split_bool : ∀ {s : String} {p : Char → Bool},
  List.map String.Slice.copy (s.split p).toList = List.map String.ofList (List.splitOnP p s.toList)
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.smod_umod : ∀ {w : ℕ} (x y : BitVec w),
  x.smod y =
    bif x.getLsbD (w - 1) then bif y.getLsbD (w - 1) then -(-x % -y) else bif -x % y == 0#w then -x % y else y - -x % y
    else bif y.getLsbD (w - 1) then bif x % -y == 0#w then x % -y else x % -y + y else x.umod y
-- Mathlib.Tactic.TFAE
Mathlib.Tactic.TFAE.Parser.impIff.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
_private.Mathlib.CategoryTheory.Galois.IsFundamentalgroup.0.CategoryTheory.PreGaloisCategory.isoOnObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    (F : CategoryTheory.Functor C FintypeCat) →
      {G : Type u_1} → [inst_1 : Group G] → [(X : C) → MulAction G (F.obj X).obj] → G → (X : C) → F.obj X ≅ F.obj X
-- Mathlib.Tactic.InferParam
/-- Close a goal of the form `optParam α a` or `autoParam α stx` by using `a`.  -/
Mathlib.Tactic.inferOptParam : Lean.ParserDescr
-- Mathlib.Algebra.Algebra.Operations
Submodule.span_singleton_algebraMap_of_isUnit : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] {r : R},
  IsUnit r → R ∙ (algebraMap R A) r = 1
-- Mathlib.Algebra.Field.Periodic
/-- If a function `f` is `Periodic` with positive period `c`, then for all `x` there exists some
`y ∈ Ico 0 c` such that `f x = f y`.  -/
Function.Periodic.exists_mem_Ico₀ : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddCommGroup α] [inst_1 : LinearOrder α]
  [IsOrderedAddMonoid α] [Archimedean α], Function.Periodic f c → 0 < c → ∀ (x : α), ∃ y ∈ Set.Ico 0 c, f x = f y
-- Mathlib.Combinatorics.Graph.Basic
/-- The graph with vertex set `vertexSet` and no edges  -/
Graph.noEdge : {α : Type u_1} → Set α → (β : Type u_3) → Graph α β
-- Std.Data.TreeMap.Raw.Basic
/-- Check if all elements satisfy the predicate, short-circuiting if a predicate fails.  -/
Std.TreeMap.Raw.all : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → (α → β → Bool) → Bool
-- Init.Data.Vector.Lemmas
Vector.any_cast : ∀ {α : Type u_1} {n a : ℕ} {h : n = a} {f : α → Bool} {xs : Vector α n}, (Vector.cast h xs).any f = xs.any f
-- Init.Data.List.Basic
List.zipWithAll_cons_cons : ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : Option α → Option α_1 → α_2} {a : α} {as : List α} {b : α_1}
  {bs : List α_1}, List.zipWithAll f (a :: as) (b :: bs) = f (some a) (some b) :: List.zipWithAll f as bs
-- Mathlib.Analysis.Calculus.FDeriv.Norm
ContDiffAt.contDiffAt_norm_of_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {n : WithTop ℕ∞} {x : E} {t : ℝ},
  ContDiffAt ℝ n (fun x => ‖x‖) (t • x) → ContDiffAt ℝ n (fun x => ‖x‖) x
-- Mathlib.NumberTheory.NumberField.ClassNumber
NumberField.exists_ideal_in_class_of_norm_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (C : ClassGroup (NumberField.RingOfIntegers K)),
  ∃ I,
    ClassGroup.mk0 I = C ∧
      ↑(Ideal.absNorm ↑I) ≤
        (4 / Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K *
          (↑(Module.finrank ℚ K).factorial / ↑(Module.finrank ℚ K) ^ Module.finrank ℚ K * √|↑(NumberField.discr K)|)
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
_private.Mathlib.CategoryTheory.Monoidal.Free.Coherence.0.CategoryTheory.FreeMonoidalCategory.inclusionObj.match_1.eq_2 : ∀ {C : Type u_1} (motive : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C → Sort u_2)
  (n : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) (a : C)
  (h_1 : Unit → motive CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject.unit)
  (h_2 : (n : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) → (a : C) → motive (n.tensor a)),
  (match n.tensor a with
    | CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject.unit => h_1 ()
    | n.tensor a => h_2 n a) =
    h_2 n a
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.instGeometricallyIntegralOverSchemeInferInstanceOverClass : ∀ {n : Type u} (S : AlgebraicGeometry.Scheme),
  AlgebraicGeometry.GeometricallyIntegral (AlgebraicGeometry.AffineSpace n S ↘ S)
-- Mathlib.Algebra.Group.Submonoid.Basic
AddMonoidHom.coe_ofClosureMEqTopRight : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N] {s : Set M} (f : M → N)
  (hs : AddSubmonoid.closure s = ⊤) (h1 : f 0 = 0) (hadd : ∀ (x y : M), y ∈ s → f (x + y) = f x + f y),
  ⇑(AddMonoidHom.ofClosureMEqTopRight f hs h1 hadd) = f
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
FiberBundle.chartedSpace'_chartAt : ∀ {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace F]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : TopologicalSpace B] [inst_4 : FiberBundle F E] (x : Bundle.TotalSpace F E),
  chartAt (B × F) x = (trivializationAt F E x.proj).toOpenPartialHomeomorph
-- Mathlib.Logic.Equiv.Defs
/-- `PUnit` sorts in any two universes are equivalent.  -/
Equiv.punitEquivPUnit : PUnit.{v} ≃ PUnit.{w}
-- Mathlib.Combinatorics.Configuration
Configuration.HasLines.mkLine_ax : ∀ {P : Type u_1} {L : Type u_2} {inst : Membership P L} [self : Configuration.HasLines P L] {p₁ p₂ : P} (h : p₁ ≠ p₂),
  p₁ ∈ Configuration.HasLines.mkLine h ∧ p₂ ∈ Configuration.HasLines.mkLine h
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instSMulCommClass : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {R : Type u_2}
  [inst_2 : Semiring R] [inst_3 : NonUnitalNonAssocSemiring β] [inst_4 : IsTopologicalSemiring β] [inst_5 : Module R β]
  [inst_6 : ContinuousConstSMul R β] [SMulCommClass R β β],
  SMulCommClass R (ZeroAtInftyContinuousMap α β) (ZeroAtInftyContinuousMap α β)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.link.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (szl : ℕ) (k' : α) (v' : β k') (l' r' l'' : Std.DTreeMap.Internal.Impl α β)
  (motive :
    Std.DTreeMap.Internal.Impl.Tree α β ((Std.DTreeMap.Internal.Impl.inner szl k' v' l' r').size + 1 + l''.size) →
      Sort u_3)
  (ℓ : Std.DTreeMap.Internal.Impl α β) (hℓ₁ : ℓ.Balanced)
  (hℓ₂ : ℓ.size = (Std.DTreeMap.Internal.Impl.inner szl k' v' l' r').size + 1 + l''.size)
  (h_1 :
    (ℓ : Std.DTreeMap.Internal.Impl α β) →
      (hℓ₁ : ℓ.Balanced) →
        (hℓ₂ : ℓ.size = (Std.DTreeMap.Internal.Impl.inner szl k' v' l' r').size + 1 + l''.size) →
          motive { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ }),
  (match { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } with
    | { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } => h_1 ℓ hℓ₁ hℓ₂) =
    h_1 ℓ hℓ₁ hℓ₂
-- Mathlib.Order.Filter.Bases.Basic
Filter.inf_principal_neBot_iff : ∀ {α : Type u_1} {l : Filter α} {s : Set α}, (l ⊓ Filter.principal s).NeBot ↔ ∀ U ∈ l, (U ∩ s).Nonempty
-- Mathlib.Order.Defs.Unbundled
refl_of : ∀ {α : Sort u_1} (r : α → α → Prop) [Std.Refl r] (a : α), r a a
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFiniteAt.of_le : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P Q : Ideal S}
  [inst_3 : P.IsPrime] [inst_4 : Q.IsPrime], P ≤ Q → ∀ [Algebra.QuasiFiniteAt R Q], Algebra.QuasiFiniteAt R P
-- Mathlib.Data.Int.Order.Basic
Int.mul_nonneg_of_nonneg_or_nonpos : ∀ {a b : ℤ}, 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 → 0 ≤ a * b
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.fieldId : Lean.Syntax → Option Lean.Name → Lean.LocalContext → Lean.Name → Lean.Elab.CompletionInfo
-- Mathlib.Computability.Encoding
/-- Deprecated: Use `Encoding α Γ` along with `[Fintype Γ]` instead.  -/
Computability.FinEncoding : Type u → {Γ : Type v} → [Fintype Γ] → Type (max u v)
-- Mathlib.CategoryTheory.Category.Basic
/-- A tactic for discharging easy category theory goals, widely used as an autoparameter.
Currently this defaults to the `aesop_cat` wrapper around `aesop`, but by setting
the option `mathlib.tactic.category.grind` to `true`, it will use the `grind` tactic instead.
 -/
CategoryTheory.categoryTheoryDischarger : Lean.Elab.Tactic.TacticM Unit
-- Mathlib.RingTheory.Smooth.AdicCompletion
AdicCompletion.kerProj.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {A : Type u_4} [inst_2 : CommRing A]
  [inst_3 : Algebra R A] [inst_4 : Algebra R S] {f : S →ₐ[R] A} (hf : Function.Surjective ⇑f),
  AdicCompletion.kerProj hf = AdicCompletion.kerProj hf
-- Mathlib.GroupTheory.CosetCover
AddSubgroup.finiteIndex_of_leftCoset_cover_const : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_2} {s : Finset ι} {H : AddSubgroup G} {g : ι → G},
  ⋃ i ∈ s, g i +ᵥ ↑H = Set.univ → H.FiniteIndex
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Matrix.trace_eq_neg_charpoly_nextCoeff : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R),
  M.trace = -M.charpoly.nextCoeff
-- Mathlib.Data.Set.Lattice
iInf_sUnion : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice β] (S : Set (Set α)) (f : α → β),
  ⨅ x ∈ ⋃₀ S, f x = ⨅ s ∈ S, ⨅ x ∈ s, f x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_map_of_getKey?_eq_some : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [Std.TransOrd α] {f : α → β → γ} {k k' : α},
  t.WF →
    t.getKey? k = some k' →
      Std.DTreeMap.Internal.Impl.Const.get? (Std.DTreeMap.Internal.Impl.map f t) k =
        Option.map (f k') (Std.DTreeMap.Internal.Impl.Const.get? t k)
-- Mathlib.Data.Finsupp.Defs
Finsupp.card_support_eq_zero : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] {f : α →₀ M}, f.support.card = 0 ↔ f = 0
-- Mathlib.Data.Multiset.ZeroCons
Multiset.cons_coe : ∀ {α : Type u_1} (a : α) (l : List α), a ::ₘ ↑l = ↑(a :: l)
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
/-- The fiber of addition at `x`: all pairs `(a, b)` with `a + b = x`.  -/
DiscreteConvolution.addFiber : {M : Type u_1} → [AddMonoid M] → M → Set (M × M)
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.FinitaryExtensive.isPullback_initial_to_binaryCofan : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.FinitaryExtensive C]
  {c : CategoryTheory.Limits.BinaryCofan X Y} (hc : CategoryTheory.Limits.IsColimit c),
  CategoryTheory.IsPullback
    (CategoryTheory.Limits.initial.to
      ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left }))
    (CategoryTheory.Limits.initial.to
      ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right }))
    c.inl c.inr
-- Std.Net.Addr
Std.Net.instInhabitedSocketAddressV6 : Inhabited Std.Net.SocketAddressV6
-- Mathlib.FieldTheory.AlgebraicClosure
/-- If `K / E / F` is a field extension tower, such that `K / E` has no non-trivial algebraic
subextensions (this means that it is purely transcendental),
then the image of `algebraicClosure F E` in `K` is equal to `algebraicClosure F K`.  -/
algebraicClosure.map_eq_of_algebraicClosure_eq_bot : ∀ (F : Type u_1) {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u_3}
  [inst_3 : Field K] [inst_4 : Algebra F K] [inst_5 : Algebra E K] [inst_6 : IsScalarTower F E K],
  algebraicClosure E K = ⊥ →
    IntermediateField.map (IsScalarTower.toAlgHom F E K) (algebraicClosure F E) = algebraicClosure F K
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.tendsto_toNNReal_iff' : ∀ {α : Type u_1} {f : α → ENNReal} {u : Filter α} {a : NNReal},
  (∀ (x : α), f x ≠ ⊤) → (Filter.Tendsto (ENNReal.toNNReal ∘ f) u (nhds a) ↔ Filter.Tendsto f u (nhds ↑a))
-- Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
CategoryTheory.ObjectProperty.inverseImage_opEquivalence_inverse_trW_inverseImage_ι_op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (A B : CategoryTheory.ObjectProperty C)
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.Preadditive C] [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_5 : CategoryTheory.Pretriangulated C] [inst_6 : A.IsTriangulated] [B.IsTriangulated]
  [B.IsClosedUnderIsomorphisms],
  (B.op.inverseImage A.op.ι).trW.inverseImage A.opEquivalence.inverse = (B.inverseImage A.ι).op.trW
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instBraidedCategory : {k : Type u} →
  {G : Type v} → [inst : CommRing k] → [inst_1 : Monoid G] → CategoryTheory.BraidedCategory (Rep.{u, u, v} k G)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
IsMax.withZero : ∀ {α : Type u_1} [inst : LE α] {a : α}, IsMax a → IsMax ↑a
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.mulOneClass.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : MulOneClass α],
  Finset.mulOneClass = Function.Injective.mulOneClass SetLike.coe ⋯ ⋯ ⋯
-- Mathlib.Topology.Spectral.Hom
SpectralMap.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {g₁ g₂ : SpectralMap β γ} {f : SpectralMap α β},
  Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.instInvolutiveStar : InvolutiveStar Complex.UnitClosedDisc
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
_private.Mathlib.CategoryTheory.Monoidal.Free.Basic.0.CategoryTheory.FreeMonoidalCategory.projectMapAux.match_1.splitter : {C : Type u_1} →
  (motive : (x x_1 : CategoryTheory.FreeMonoidalCategory C) → x.Hom x_1 → Sort u_2) →
    (x x_1 : CategoryTheory.FreeMonoidalCategory C) →
      (x_2 : x.Hom x_1) →
        ((x : CategoryTheory.FreeMonoidalCategory C) → motive x x (CategoryTheory.FreeMonoidalCategory.Hom.id x)) →
          ((X Y Z : CategoryTheory.FreeMonoidalCategory C) →
              motive ((X.tensor Y).tensor Z) (X.tensor (Y.tensor Z))
                (CategoryTheory.FreeMonoidalCategory.Hom.α_hom X Y Z)) →
            ((X Y Z : CategoryTheory.FreeMonoidalCategory C) →
                motive (X.tensor (Y.tensor Z)) ((X.tensor Y).tensor Z)
                  (CategoryTheory.FreeMonoidalCategory.Hom.α_inv X Y Z)) →
              ((a : CategoryTheory.FreeMonoidalCategory C) →
                  motive (CategoryTheory.FreeMonoidalCategory.unit.tensor a) a
                    (CategoryTheory.FreeMonoidalCategory.Hom.l_hom a)) →
                ((a : CategoryTheory.FreeMonoidalCategory C) →
                    motive a (CategoryTheory.FreeMonoidalCategory.unit.tensor a)
                      (CategoryTheory.FreeMonoidalCategory.Hom.l_inv a)) →
                  ((a : CategoryTheory.FreeMonoidalCategory C) →
                      motive (a.tensor CategoryTheory.FreeMonoidalCategory.unit) a
                        (CategoryTheory.FreeMonoidalCategory.Hom.ρ_hom a)) →
                    ((a : CategoryTheory.FreeMonoidalCategory C) →
                        motive a (a.tensor CategoryTheory.FreeMonoidalCategory.unit)
                          (CategoryTheory.FreeMonoidalCategory.Hom.ρ_inv a)) →
                      ((x x_3 Y : CategoryTheory.FreeMonoidalCategory C) →
                          (f : x.Hom Y) → (g : Y.Hom x_3) → motive x x_3 (f.comp g)) →
                        ((X Y₁ Y₂ : CategoryTheory.FreeMonoidalCategory C) →
                            (p : Y₁.Hom Y₂) →
                              motive (X.tensor Y₁) (X.tensor Y₂)
                                (CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft X p)) →
                          ((X₁ X₂ : CategoryTheory.FreeMonoidalCategory C) →
                              (p : X₁.Hom X₂) →
                                (X : CategoryTheory.FreeMonoidalCategory C) →
                                  motive (X₁.tensor X) (X₂.tensor X) (p.whiskerRight X)) →
                            ((W X Y Z : CategoryTheory.FreeMonoidalCategory C) →
                                (f : W.Hom Y) → (g : X.Hom Z) → motive (W.tensor X) (Y.tensor Z) (f.tensor g)) →
                              motive x x_1 x_2
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
_private.Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctor_obj_distinguished : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (A : C),
  (CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctor✝ t n).obj A ∈
    CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.Topology.Continuous
Filter.Tendsto.lift'_closure : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f →
    ∀ {l : Filter X} {l' : Filter Y}, Filter.Tendsto f l l' → Filter.Tendsto f (l.lift' closure) (l'.lift' closure)
-- Mathlib.Algebra.Homology.HomologySequenceLemmas
CategoryTheory.ShortComplex.ShortExact.exactAt_X₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)},
  S.ShortExact →
    ∀ (i : ι),
      autoParam (CategoryTheory.Epi (HomologicalComplex.homologyMap S.f i))
          CategoryTheory.ShortComplex.ShortExact.exactAt_X₃._auto_1 →
        autoParam (∀ (j : ι), c.Rel i j → CategoryTheory.Mono (HomologicalComplex.homologyMap S.f j))
            CategoryTheory.ShortComplex.ShortExact.exactAt_X₃._auto_3 →
          S.X₃.ExactAt i
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_nonneg : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [ContinuousSqrt R]
  [StarOrderedRing R] [inst_8 : TopologicalSpace A] [inst_9 : Ring A] [inst_10 : StarRing A] [inst_11 : PartialOrder A]
  [StarOrderedRing A] [inst_13 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {f : R → R} {a : A},
  (∀ x ∈ spectrum R a, 0 ≤ f x) → 0 ≤ cfc f a
-- Init.Data.Array.Lemmas
Array.filterMap_some : ∀ {α : Type u_1} {xs : Array α}, Array.filterMap some xs = xs
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_singleton_mul_right_unit : ∀ {α : Type u} [inst : CommSemiring α] {a : α}, IsUnit a → ∀ (x : α), Ideal.span {x * a} = Ideal.span {x}
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.max_zero : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.HasFiniteIntegral f μ → MeasureTheory.HasFiniteIntegral (fun a => max (f a) 0) μ
-- Init.Omega.Int
Lean.Omega.Prod.fst_mk : ∀ {α : Type u_1} {x : α} {β : Type u_2} {y : β}, (x, y).1 = x
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.prodLIE_apply : ∀ (𝕜 : Type u) (E : Type wE) (F : Type wF) (G : Type wG) {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fintype ι]
  (f : E [⋀^ι]→L[𝕜] F × E [⋀^ι]→L[𝕜] G), (ContinuousAlternatingMap.prodLIE 𝕜 E F G) f = f.1.prod f.2
-- Lean.Expr
/-- Return `some lhs` if `e = mkLHSGoal e'`, where `e'` is of the form `lhs = rhs`.  -/
Lean.isLHSGoal? : Lean.Expr → Option Lean.Expr
-- Mathlib.NumberTheory.Real.Irrational
Irrational.intCast_mul : ∀ {x : ℝ}, Irrational x → ∀ {m : ℤ}, m ≠ 0 → Irrational (↑m * x)
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
isLUB_ciSup_set : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {f : β → α} {s : Set β},
  BddAbove (f '' s) → s.Nonempty → IsLUB (f '' s) (⨆ i, f ↑i)
-- Init.Data.BitVec.Bitblast
BitVec.DivModState.mk.sizeOf_spec : ∀ {w : ℕ} (wn wr : ℕ) (q r : BitVec w),
  sizeOf { wn := wn, wr := wr, q := q, r := r } = 1 + sizeOf wn + sizeOf wr + sizeOf q + sizeOf r
-- Init.Data.SInt.Lemmas
Int64.toNatClampNeg_one : Int64.toNatClampNeg 1 = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.pullbackAssoc_inv_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁)
  (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [inst_1 : CategoryTheory.Limits.HasPullback f₁ f₂]
  [inst_2 : CategoryTheory.Limits.HasPullback f₃ f₄]
  [inst_3 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃)
      f₄]
  [inst_4 :
    CategoryTheory.Limits.HasPullback f₁
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).inv
      (CategoryTheory.Limits.pullback.snd
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd f₁
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂))
      (CategoryTheory.Limits.pullback.snd f₃ f₄)
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.id_map : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} (hf : Measurable f),
  ProbabilityTheory.Kernel.id.map f = ProbabilityTheory.Kernel.deterministic f hf
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
/-- In the special case `n = 1`, `Quaternion 1` is a cyclic group (of order `4`).  -/
QuaternionGroup.quaternionGroup_one_isCyclic : IsCyclic (QuaternionGroup 1)
-- Aesop.Rule
Aesop.NormRuleInfo.mk.sizeOf_spec : ∀ (penalty : ℤ), sizeOf { penalty := penalty } = 1 + sizeOf penalty
-- Mathlib.Topology.Algebra.UniformConvergence
instCommMonoidUniformOnFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : CommMonoid β],
  instCommMonoidUniformOnFun = { toMonoid := instMonoidUniformOnFun, mul_comm := ⋯ }
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getThenInsertIfNew?_fst : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, (t.getThenInsertIfNew? k v).1 = t[k]?
-- Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
PointwiseConvergenceCLM.piEquivL_symm_apply : ∀ {𝕜 : Type u_3} [inst : NormedField 𝕜] {E : Type u_7} [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜 E] {ι : Type u_11} (F : ι → Type u_12) [inst_4 : (i : ι) → AddCommGroup (F i)]
  [inst_5 : (i : ι) → Module 𝕜 (F i)] [inst_6 : (i : ι) → TopologicalSpace (F i)]
  [inst_7 : ∀ (i : ι), IsTopologicalAddGroup (F i)] [inst_8 : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)]
  (T : E →Lₚₜ[𝕜] (i : ι) → F i) (e : E) (i : ι), ((PointwiseConvergenceCLM.piEquivL 𝕜 E F).symm T i) e = T e i
-- Init.Data.Option.Basic
/-- Converts an optional monadic computation into a monadic computation of an optional value.

This function only requires `m` to be an applicative functor.

Example:
```lean example
#eval show IO (Option String) from
  Option.sequence <| some do
    IO.println "hello"
    return "world"
```
```output
hello
```
```output
some "world"
```
 -/
Option.sequence : {m : Type u → Type u_1} → [Applicative m] → {α : Type u} → Option (m α) → m (Option α)