mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
CategoryTheory.LocallyDiscrete.mkPseudofunctor_map : ∀ {B₀ : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} B₀] [inst_1 : CategoryTheory.Bicategory C]
  (obj : B₀ → C) (map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b'))
  (mapId : (b : B₀) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b))
  (mapComp :
    {b₀ b₁ b₂ : B₀} →
      (f : b₀ ⟶ b₁) →
        (g : b₁ ⟶ b₂) →
          map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g))
  (map₂_associator :
    autoParam
      (∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
        CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h))
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv)
                  (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.LocallyDiscrete.mkPseudofunctor._auto_1)
  (map₂_left_unitor :
    autoParam
      (∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁),
        CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f))
              (CategoryTheory.Bicategory.leftUnitor (map f)).hom) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.LocallyDiscrete.mkPseudofunctor._auto_3)
  (map₂_right_unitor :
    autoParam
      (∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁),
        CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom)
              (CategoryTheory.Bicategory.rightUnitor (map f)).hom) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.LocallyDiscrete.mkPseudofunctor._auto_5)
  {X Y : CategoryTheory.LocallyDiscrete B₀} (f : X ⟶ Y),
  (CategoryTheory.LocallyDiscrete.mkPseudofunctor obj map mapId mapComp map₂_associator map₂_left_unitor
          map₂_right_unitor).map
      f =
    map f.as
-- Lean.Meta.SynthInstance
Lean.Meta.synthInstance : Lean.Expr → optParam (Option ℕ) none → Lean.MetaM Lean.Expr
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.norm_eq_of_normAtPlace_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x y : NumberField.mixedEmbedding.mixedSpace K},
  (∀ (w : NumberField.InfinitePlace K),
      (NumberField.mixedEmbedding.normAtPlace w) x = (NumberField.mixedEmbedding.normAtPlace w) y) →
    NumberField.mixedEmbedding.norm x = NumberField.mixedEmbedding.norm y
-- Mathlib.Data.Fin.SuccPred
Fin.succAbove_last_apply : ∀ {n : ℕ} (i : Fin n), (Fin.last n).succAbove i = i.castSucc
-- Mathlib.Analysis.BoxIntegral.Partition.Split
/-- Given a box `I` and `x ∈ (I.lower i, I.upper i)`, the hyperplane `{y : ι → ℝ | y i = x}` splits
`I` into two boxes. `BoxIntegral.Box.splitUpper I i x` is the box `I ∩ {y | x < y i}`
(if it is nonempty). As usual, we represent a box that may be empty as
`WithBot (BoxIntegral.Box ι)`.  -/
BoxIntegral.Box.splitUpper : {ι : Type u_1} → BoxIntegral.Box ι → ι → ℝ → WithBot (BoxIntegral.Box ι)
-- Mathlib.Order.Lattice
sup_eq_right : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, a ⊔ b = b ↔ a ≤ b
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
SimpleGraph.chromaticNumber_le_two_iff_isBipartite : ∀ {V : Type u_1} {G : SimpleGraph V}, G.chromaticNumber ≤ 2 ↔ G.IsBipartite
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
/-- If a `LocalizerMorphism` becomes a fully faithful after localization, then any compatible
functor between the localized categories is fully faithful.  -/
CategoryTheory.LocalizerMorphism.fullyFaithful : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {D₁ : Type u₄} →
      {D₂ : Type u₅} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₄, u₄} D₁] →
              [inst_3 : CategoryTheory.Category.{v₅, u₅} D₂] →
                {W₁ : CategoryTheory.MorphismProperty C₁} →
                  {W₂ : CategoryTheory.MorphismProperty C₂} →
                    (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) →
                      (L₁ : CategoryTheory.Functor C₁ D₁) →
                        [L₁.IsLocalization W₁] →
                          (L₂ : CategoryTheory.Functor C₂ D₂) →
                            [L₂.IsLocalization W₂] →
                              (G : CategoryTheory.Functor D₁ D₂) →
                                [h : Φ.IsLocalizedFullyFaithful] →
                                  [CategoryTheory.CatCommSq Φ.functor L₁ L₂ G] → G.FullyFaithful
-- Mathlib.Data.Set.Function
Set.MapsTo.inter_bijOn : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} {f : α → β},
  Set.MapsTo f s₁ t₁ → Set.BijOn f s₂ t₂ → s₂ ∩ f ⁻¹' t₁ ⊆ s₁ → Set.BijOn f (s₁ ∩ s₂) (t₁ ∩ t₂)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackProdFstIsoProd_hom_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct Y Z] [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Z]
  [inst_3 : CategoryTheory.Limits.HasPullback f CategoryTheory.Limits.prod.fst],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdFstIsoProd f Z).hom
      CategoryTheory.Limits.prod.snd =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f CategoryTheory.Limits.prod.fst)
      CategoryTheory.Limits.prod.snd
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
SimpleGraph.bipartiteDoubleCover.match_1.congr_eq_2 : ∀ {V : Type u_1} (motive : V ⊕ V → V ⊕ V → Sort u_2) (x x_1 : V ⊕ V)
  (h_1 : (v' w' : V) → motive (Sum.inl v') (Sum.inr w')) (h_2 : (v' w' : V) → motive (Sum.inr v') (Sum.inl w'))
  (h_3 : (x x_2 : V ⊕ V) → motive x x_2) (v' w' : V),
  x = Sum.inr v' →
    x_1 = Sum.inl w' →
      (match x, x_1 with
        | Sum.inl v', Sum.inr w' => h_1 v' w'
        | Sum.inr v', Sum.inl w' => h_2 v' w'
        | x, x_2 => h_3 x x_2) ≍
        h_2 v' w'
-- Mathlib.Combinatorics.Configuration
Configuration.ProjectivePlane.order.eq_1 : ∀ (P : Type u_1) (L : Type u_2) [inst : Membership P L] [inst_1 : Configuration.ProjectivePlane P L],
  Configuration.ProjectivePlane.order P L = Configuration.lineCount L (Classical.choose ⋯) - 1
-- Init.Data.List.Erase
List.eraseP_of_forall_not : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, (∀ a ∈ l, ¬p a = true) → List.eraseP p l = l
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.hom_comp : ∀ {M N T : AddMonCat} (f : M ⟶ N) (g : N ⟶ T),
  AddMonCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (AddMonCat.Hom.hom g).comp (AddMonCat.Hom.hom f)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- The seminorm controls the Schwartz estimate for any fixed `x`.

Variant for functions `𝓢(ℝ, F)`.  -/
SchwartzMap.le_seminorm' : ∀ (𝕜 : Type u_2) {F : Type u_6} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] [inst_2 : NormedField 𝕜]
  [inst_3 : NormedSpace 𝕜 F] [inst_4 : SMulCommClass ℝ 𝕜 F] (k n : ℕ) (f : SchwartzMap ℝ F) (x : ℝ),
  |x| ^ k * ‖iteratedDeriv n (⇑f) x‖ ≤ (SchwartzMap.seminorm 𝕜 k n) f
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DeclarationParams : Type
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.alterₘ.match_1.eq_2 : ∀ {α : Type u_3} {β : α → Type u_1} (a : α) (motive : Option (β a) → Sort u_2) (b : β a) (h_1 : Unit → motive none)
  (h_2 : (b : β a) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.Topology.Order.Monotone
/-- An antitone map has a limit to the right of any point `x`, equal to `sSup (f '' (Ioi x))`.  -/
Antitone.tendsto_nhdsGT : ∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Antitone f → ∀ (x : α), Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhds (sSup (f '' Set.Ioi x)))
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.instInhabitedCont'.default : Turing.PartrecToTM2.Cont'
-- Mathlib.Algebra.Lie.Basic
/-- Consider an equivalence of Lie algebras as a linear equivalence.  -/
LieEquiv.toLinearEquiv : {R : Type u} →
  {L₁ : Type v} →
    {L₂ : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L₁] →
          [inst_2 : LieRing L₂] → [inst_3 : LieAlgebra R L₁] → [inst_4 : LieAlgebra R L₂] → (L₁ ≃ₗ⁅R⁆ L₂) → L₁ ≃ₗ[R] L₂
-- Mathlib.CategoryTheory.Limits.Pi
/-- Given a family of colimit cocones over the `F ⋙ Pi.eval C i`,
assembling them together as a `Cocone F` produces a colimit cocone.
 -/
CategoryTheory.pi.coconeOfCoconeEvalIsColimit : {I : Type v₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {J : Type v₁} →
        [inst_1 : CategoryTheory.SmallCategory J] →
          {F : CategoryTheory.Functor J ((i : I) → C i)} →
            {c : (i : I) → CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Pi.eval C i))} →
              ((i : I) → CategoryTheory.Limits.IsColimit (c i)) →
                CategoryTheory.Limits.IsColimit (CategoryTheory.pi.coconeOfCoconeCompEval c)
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.adjoin_map : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [inst_3 : IsGalois k K]
  (f : K →ₐ[k] K) (s : Set K) [inst_4 : Finite ↑s],
  FiniteGaloisIntermediateField.adjoin k (⇑f '' s) = FiniteGaloisIntermediateField.adjoin k s
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.isSome_succMany?_of_lt_size_toArray : ∀ {α : Type u} {r : Std.Ric α} [inst : Std.PRange.Least? α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [inst_6 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxc.IsAlwaysFinite α] {i : ℕ},
  i < r.toArray.size → (Std.PRange.succMany? i Std.PRange.UpwardEnumerable.least).isSome = true
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
CategoryTheory.MorphismProperty.IsStableUnderBraiding.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {P : CategoryTheory.MorphismProperty C}
  [toIsMonoidalStable : P.IsMonoidalStable],
  (∀ (c c' : C), P (β_ c c').hom) → (∀ (c c' : C), P (β_ c c').inv) → P.IsStableUnderBraiding
-- Mathlib.RingTheory.Artinian.Module
LinearMap.isArtinian_iff_of_bijective : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_5}
  {P : Type u_6} [inst_3 : Semiring S] [inst_4 : AddCommMonoid P] [inst_5 : Module S P] {σ : R →+* S}
  [RingHomSurjective σ] (l : M →ₛₗ[σ] P), Function.Bijective ⇑l → (IsArtinian R M ↔ IsArtinian S P)
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : Cᵒᵖ ⥤ D` creates limits of `K.op : Jᵒᵖ ⥤ Cᵒᵖ`, then `F.rightOp : C ⥤ Dᵒᵖ` creates
colimits of `K : J ⥤ C`.  -/
CategoryTheory.Limits.createsColimitRightOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (K : CategoryTheory.Functor J C) →
              (F : CategoryTheory.Functor Cᵒᵖ D) →
                [CategoryTheory.CreatesLimit K.op F] → CategoryTheory.CreatesColimit K F.rightOp
-- Mathlib.Tactic.FieldSimp
/-- Basic meta-code "normal form" object of the `field_simp` tactic: a type synonym
for a list of ordered triples comprising an expression representing a term of a type `M` (where
typically `M` is a field), together with an integer "power" and a natural number "index".

The natural number represents the index of the `M` term in the `AtomM` monad: this is not enforced,
but is sometimes assumed in operations.  Thus when items `((a₁, x₁), k)` and `((a₂, x₂), k)`
appear in two different `FieldSimp.qNF` objects (i.e. with the same `ℕ`-index `k`), it is expected
that the expressions `x₁` and `x₂` are the same.  It is also expected that the items in a
`FieldSimp.qNF` list are in strictly decreasing order by natural-number index.

By forgetting the natural number indices, an expression representing a `Mathlib.Tactic.FieldSimp.NF`
object can be built from a `FieldSimp.qNF` object; this construction is provided as
`Mathlib.Tactic.FieldSimp.qNF.toNF`.  -/
Mathlib.Tactic.FieldSimp.qNF : {v : Lean.Level} → Q(Type v) → Type
-- Mathlib.Topology.Algebra.Group.Extension
/-- Construct a short exact sequence of topological groups from a closed normal subgroup.  -/
TopologicalGroup.IsSES.ofClosedSubgroup : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] (H : Subgroup G)
  [inst_3 : H.Normal], IsClosed ↑H → TopologicalGroup.IsSES H.subtype (QuotientGroup.mk' H)
-- Mathlib.Order.Fin.Basic
Fin.castSuccOrderEmb_apply : ∀ {n : ℕ} (a : Fin n), Fin.castSuccOrderEmb a = a.castSucc
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.mul_comm_of_mem_isMulCommutative : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [IsMulCommutative ↥H] {a b : G}, a ∈ H → b ∈ H → a * b = b * a
-- Init.Data.List.Pairwise
List.Nodup.eq_1 : ∀ {α : Type u}, List.Nodup = List.Pairwise fun x1 x2 => x1 ≠ x2
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndepSet.meas_biInter : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {f : ι → Set Ω},
  ProbabilityTheory.Kernel.iIndepSet f κ μ →
    ∀ (s : Finset ι), ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ s, f i) = ∏ i ∈ s, (κ a) (f i)
-- Mathlib.Probability.Kernel.MeasurableIntegral
MeasureTheory.StronglyMeasurable.integral_kernel_prod_right' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  {E : Type u_4} [inst : NormedAddCommGroup E] [ProbabilityTheory.IsSFiniteKernel κ] [inst_2 : NormedSpace ℝ E]
  ⦃f : α × β → E⦄,
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun x => ∫ (y : β), f (x, y) ∂κ x
-- Mathlib.Data.Semiquot
Semiquot.eq_pure : ∀ {α : Type u_1} {q : Semiquot α} (p : q.IsPure), q = pure (q.get p)
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoidClass.coe_subtype : ∀ {M : Type u_1} {A : Type u_3} [inst : AddZeroClass M] [inst_1 : SetLike A M] [hA : AddSubmonoidClass A M] (S' : A),
  ⇑(AddSubmonoidClass.subtype S') = Subtype.val
-- Mathlib.Analysis.Calculus.Deriv.Linear
LinearMap.deriv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} (e : 𝕜 →ₗ[𝕜] F), deriv (⇑e) x = e 1
-- Mathlib.Data.Num.Lemmas
PosNum.succ_to_nat : ∀ (n : PosNum), ↑n.succ = ↑n + 1
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
CliffordAlgebraQuaternion.equiv_symm_apply : ∀ {R : Type u_1} [inst : CommRing R] {c₁ c₂ : R} (a : QuaternionAlgebra R c₁ 0 c₂),
  CliffordAlgebraQuaternion.equiv.symm a = CliffordAlgebraQuaternion.ofQuaternion a
-- Aesop.Tree.TreeM
/-- Union of the mvars introduced by all rapps.
 -/
Aesop.Tree.allIntroducedMVars : Aesop.Tree → Std.HashSet Lean.MVarId
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey?_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {f : β k → β k}, (t.modify k f).maxKey? = t.maxKey?
-- Init.Data.Int.DivMod.Lemmas
Int.mul_le_mul_right_of_neg : ∀ {a b c : ℤ}, a < 0 → (b * a ≤ c * a ↔ c ≤ b)
-- Mathlib.Order.BoundedOrder.Basic
OrderDual.instBotOfTop.eq_1 : ∀ (α : Type u) [h : Top α], OrderDual.instBotOfTop α = { bot := ⊤ }
-- Mathlib.SetTheory.ZFC.Ordinal
/-- An ordinal is a transitive set, well-ordered under membership.  -/
ZFSet.isOrdinal_iff_isWellOrder : ∀ {x : ZFSet.{u}}, x.IsOrdinal ↔ x.IsTransitive ∧ IsWellOrder (↥x) (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_right_le_size_union : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m₂.size ≤ (m₁ ∪ m₂).size
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.RightExtension.w_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  {s t : CategoryTheory.Bicategory.RightExtension f g} (η : s ⟶ t) {Z : a ⟶ c} (h : g ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η.left)
      (CategoryTheory.CategoryStruct.comp t.counit h) =
    CategoryTheory.CategoryStruct.comp s.counit h
-- Mathlib.Topology.Constructions
instWeaklyLocallyCompactSpaceAdditive : ∀ {X : Type u} [inst : TopologicalSpace X] [WeaklyLocallyCompactSpace X], WeaklyLocallyCompactSpace (Additive X)
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
IsIntegral.of_mem_closure'' : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_5} [inst_1 : CommRing S] {f : R →+* S} (G : Set S),
  (∀ x ∈ G, f.IsIntegralElem x) → ∀ x ∈ Subring.closure G, f.IsIntegralElem x
-- Mathlib.Order.Lattice
Prod.snd_inf : ∀ (α : Type u) (β : Type v) [inst : Min α] [inst_1 : Min β] (p q : α × β), (p ⊓ q).2 = p.2 ⊓ q.2
-- Mathlib.Data.Rat.Lemmas
Rat.intCast_add_den : ∀ (n : ℤ) (q : ℚ), (↑n + q).den = q.den
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.algebraMap_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (I : Ideal R) [inst_2 : Algebra S R] (s : S),
  (algebraMap S (AdicCompletion I R)) s = (AdicCompletion.of I R) ((algebraMap S R) s)
-- Lean.Meta.Basic
/-- When `trackZetaDelta = true`, we track all free variables that have been zetaDelta-expanded.
That is, suppose the local context contains
the declaration `x : t := v`, and we reduce `x` to `v`, then we insert `x` into `State.zetaDeltaFVarIds`.
We use `trackZetaDelta` to discover which let-declarations `let x := v; e` can be represented as `have x := v; e`.
When we find these declarations we set their `nondep` flag with `true`.
To find these let-declarations in a given term `s`, we
1- Reset `State.zetaDeltaFVarIds`
2- Set `trackZetaDelta := true`
3- Type-check `s`.

Note that, we do not include this field in the `Config` structure because this field is not
taken into account while caching results. See also field `zetaDeltaSet`.
 -/
Lean.Meta.Context.trackZetaDelta : Lean.Meta.Context → Bool
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.norm_eq_zero : ∀ {d : ℤ}, (∀ (n : ℤ), d ≠ n * n) → ∀ (a : ℤ√d), a.norm = 0 ↔ a = 0
-- Mathlib.Analysis.Analytic.Order
/-- A version of **Taylor's theorem** for analytic functions in one variable, with the error
term of the form `z ^ n` times a function analytic at 0.

(See `AnalyticAt.exists_eq_sum_add_pow_mul` for a version asserting global equality rather than
just on a neighbourhood of 0.)  -/
AnalyticAt.exists_eventuallyEq_sum_add_pow_mul : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CharZero 𝕜] [CompleteSpace E] {f : 𝕜 → E},
  AnalyticAt 𝕜 f 0 →
    ∀ (n : ℕ),
      ∃ F,
        AnalyticAt 𝕜 F 0 ∧
          ∀ᶠ (z : 𝕜) in nhds 0, f z = ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 + z ^ n • F z
-- Mathlib.Geometry.Manifold.Algebra.SMul
/-- Basic typeclass stating that the action of `G` on `M` is Cⁿ as a function `G × M → M`.
Unlike with `ContMDiffMul` (the class stating that multiplication `G × G → G` within a single type
`G` is Cⁿ), we do not extend `IsManifold` because `ContMDiffSMul` contains more
explicit arguments than `IsManifold` and so `ContMDiffSMul.toIsManifold` could not be an instance
anyway: this means that in order for `ContMDiffSMul` to be meaningful, smoothness of `G` and `M`
have to be required separately. For example, to state that `G` is a Cⁿ Lie group with a Cⁿ action on
a Cⁿ manifold `M`, one can use the typeclasses
`[LieGroup I n G] [IsManifold I' n M] [ContMDiffSMul I I' n G M]`.  -/
ContMDiffSMul : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {H : Type u_2} →
      [inst_1 : TopologicalSpace H] →
        {E : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : NormedSpace 𝕜 E] →
              ModelWithCorners 𝕜 E H →
                {H' : Type u_4} →
                  [inst_4 : TopologicalSpace H'] →
                    {E' : Type u_5} →
                      [inst_5 : NormedAddCommGroup E'] →
                        [inst_6 : NormedSpace 𝕜 E'] →
                          ModelWithCorners 𝕜 E' H' →
                            WithTop ℕ∞ →
                              (G : Type u_6) →
                                [inst : TopologicalSpace G] →
                                  [ChartedSpace H G] →
                                    (M : Type u_7) →
                                      [inst : TopologicalSpace M] → [ChartedSpace H' M] → [SMul G M] → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
/-- For a functor `F : J ⥤ C`, if `J` has a terminal object then the image of it is isomorphic
to the colimit of `F`.  -/
CategoryTheory.Limits.colimitOfTerminal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} J] →
        (F : CategoryTheory.Functor J C) →
          [inst_2 : CategoryTheory.Limits.HasTerminal J] → CategoryTheory.Limits.colimit F ≅ F.obj (⊤_ J)
-- Mathlib.RingTheory.Unramified.LocalRing
Localization.localRingHom_surjective_of_primesOver_eq_singleton : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R}
  [inst_3 : p.IsPrime] {q : Ideal S} [inst_4 : q.IsPrime],
  p.primesOver S = {q} →
    ∀ [Module.Finite R S] [inst_6 : q.LiesOver p] [Algebra.IsUnramifiedAt R q]
      [inst_8 : Algebra (Localization.AtPrime p) (Localization.AtPrime q)]
      [inst_9 : Localization.AtPrime.IsLiesOverAlgebra p q],
      Function.Surjective ⇑(algebraMap p.ResidueField q.ResidueField) →
        Function.Surjective ⇑(Localization.localRingHom p q (algebraMap R S) ⋯)
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.toLinearMap : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → RootPairing ι R M N → M →ₗ[R] N →ₗ[R] R
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Formula.imp_iff_not_sup : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (φ ψ : L.Formula α), T.Iff (φ.imp ψ) (φ.not ⊔ ψ)
-- ImportGraph.Tools.FindHome
GoToModuleLinkProps : Type
-- Aesop.Rule.Name
Aesop.RuleName.instHashable : Hashable Aesop.RuleName
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.nonsingular_of_Z_eq_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P : Fin 3 → R},
  P 2 = 0 → (W'.Nonsingular P ↔ W'.Equation P ∧ (3 * P 0 ^ 2 ≠ 0 ∨ 2 * P 1 ≠ 0 ∨ W'.a₁ * P 0 * P 1 ≠ 0))
-- Mathlib.Algebra.Ring.Prod
NonUnitalRingHom.coe_fst : ∀ {R : Type u_1} {S : Type u_3} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S],
  ⇑(NonUnitalRingHom.fst R S) = Prod.fst
-- Mathlib.AlgebraicTopology.SimplicialSet.Op
SSet.op_σ : ∀ (X : SSet) {n : ℕ} (i : Fin (n + 1)) (x : X.op.obj (Opposite.op { len := n })),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ X.op i)) x =
    SSet.opObjEquiv.symm
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ X i.rev)) (SSet.opObjEquiv x))