mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Term.TermElabM
/-- Wraps the trees returned from `getInfoTrees`, if any, in an `InfoTree.context` node based on the
current monadic context and state. This is mainly used to report info trees early via
`Snapshot.infoTree?`. The trees are not removed from the `getInfoTrees` state as the final info tree
of the elaborated command should be complete and not depend on whether parts have been reported
early.

As `InfoTree.context` can have only one child, this function panics if `trees` contains more than 1
tree. Also, `PartialContextInfo.parentDeclCtx` is not currently generated as that information is not
available in the monadic context and only needed for the final info tree.
 -/
Lean.Elab.Term.getInfoTreeWithContext? : Lean.Elab.TermElabM (Option Lean.Elab.InfoTree)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.instAddGroup : {α : Type u} → AddGroup (FreeAddGroup α)
-- Init.Tactics
/-- If true, collect all successful lemmas instead of stopping at the first complete solution.
Use `+all` to enable this behavior.  -/
Lean.Parser.Tactic.LibrarySearchConfig.all : Lean.Parser.Tactic.LibrarySearchConfig → Bool
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.containsKey_alterKey_self : ∀ {α : Type u} [inst : BEq α] {β : Type v} [EquivBEq α] {a : α} {f : Option β → Option β} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.containsKey a (Std.Internal.List.Const.alterKey a f l) =
      (f (Std.Internal.List.getValue? a l)).isSome
-- Mathlib.Analysis.Calculus.Deriv.Slope
hasDerivAt_iff_tendsto_slope : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜},
  HasDerivAt f f' x ↔ Filter.Tendsto (slope f x) (nhdsWithin x {x}ᶜ) (nhds f')
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.mul_top' : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] (a : WithTop α), a * ⊤ = if a = 0 then 0 else ⊤
-- Mathlib.Tactic.CategoryTheory.ToApp
/-- Adding `@[to_app]` to a lemma named `F` of shape `∀ .., η = θ`, where `η θ : f ⟶ g` are 2-morphisms
in some bicategory, create a new lemma named `F_app`. This lemma is obtained by first specializing
the bicategory in which the equality is taking place to `Cat`, then applying `toNatTrans_congr` and
`NatTrans.congr_app` to obtain a proof of `∀ ... (X : Cat), η.app X = θ.app X`, and finally
simplifying the conclusion using some basic lemmas in the bicategory `Cat` (see `catAppSimp` for
the list of these).

So, for example, if the conclusion of `F` is `f ◁ η = θ` then the conclusion of `F_app` will be
`η.app (f.obj X) = θ.app X`.

This is useful for automatically generating lemmas that can be applied to expressions of 1-morphisms
in `Cat` which contain components of 2-morphisms.

Note that if you want both the lemma and the new lemma to be `simp` lemmas, you should tag the lemma
`@[to_app (attr := simp)]`. The variant `@[simp, to_app]` on a lemma `F` will tag `F` with
`@[simp]`, but not `F_app` (this is sometimes useful).
 -/
Mathlib.Tactic.CategoryTheory.ToApp.to_app : Lean.ParserDescr
-- Mathlib.CategoryTheory.Grothendieck
/-- Every morphism `f : X ⟶ Y` in the base category induces a natural transformation from the fiber
inclusion `ι F X` to the composition `F.map f ⋙ ι F Y`.  -/
CategoryTheory.Grothendieck.ιNatTrans : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C CategoryTheory.Cat} →
      {X Y : C} →
        (f : X ⟶ Y) → CategoryTheory.Grothendieck.ι F X ⟶ (F.map f).toFunctor.comp (CategoryTheory.Grothendieck.ι F Y)
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.toPresentation_comp : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (Q : Algebra.PreSubmersivePresentation S T ι' σ')
  (P : Algebra.PreSubmersivePresentation R S ι σ), (Q.comp P).toPresentation = Q.comp P.toPresentation
-- Lean.Meta.SizeOf
Lean.Meta.genSizeOf : Lean.Option Bool
-- Mathlib.NumberTheory.Padics.WithVal
/-- The `p`-adic numbers are isomorphic as a field to the completion of the rationals at
the `p`-adic valuation.  -/
Padic.withValRingEquiv : {p : ℕ} → [inst : Fact (Nat.Prime p)] → (Rat.padicValuation p).Completion ≃+* ℚ_[p]
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- Converts a 1-morphism into a list of its components.  -/
Mathlib.Tactic.BicategoryLike.Mor₁.toList : Mathlib.Tactic.BicategoryLike.Mor₁ → List Mathlib.Tactic.BicategoryLike.Atom₁
-- Mathlib.RingTheory.Smooth.Fiber
Algebra.IsEtaleAt.of_isUnramifiedAt_of_flat : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Module.Flat R S]
  [Algebra.FinitePresentation R S] (q : Ideal S) [inst_5 : q.IsPrime] [Algebra.IsUnramifiedAt R q],
  Algebra.IsEtaleAt R q
-- Mathlib.Data.PFunctor.Univariate.Basic
/-- `x.iget i` takes the component of `x` designated by `i` if any is or returns a default value  -/
PFunctor.Obj.iget : {P : PFunctor.{uA, uB}} → [DecidableEq P.A] → {α : Type u_1} → [Inhabited α] → ↑P α → P.Idx → α
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.inv_hom_id_tensor'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {V W X Y Z : C}
  (f : V ⟶ W) [inst_2 : CategoryTheory.IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z) {Z_1 : C}
  (h_1 : CategoryTheory.MonoidalCategoryStruct.tensorObj W Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.inv f) g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f h) h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id W) g)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id W) h) h_1)
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.mono_right : ∀ {α : Type u_1} [inst : Preorder α] {x y : α},
  x ≤ y → ∀ {t : Ordnode α} {o : WithBot α}, Ordnode.Valid' o t ↑x → Ordnode.Valid' o t ↑y
-- Mathlib.RingTheory.NoetherNormalization
/-- `T` maps `f` into some polynomial in `X_0` such that the leading coefficient is invertible.  -/
_private.Mathlib.RingTheory.NoetherNormalization.0.NoetherNormalization.T_leadingcoeff_isUnit : ∀ {k : Type u_1} [inst : Field k] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) k),
  f ≠ 0 → IsUnit ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T✝ f) f)).leadingCoeff
-- Aesop.Forward.State
Aesop.instInhabitedInstMap : Inhabited Aesop.InstMap
-- Mathlib.RingTheory.Localization.Ideal
IsLocalization.disjoint_under_iff : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] (J : Ideal S), Disjoint ↑M ↑(Ideal.under R J) ↔ J ≠ ⊤
-- Init.Coe
instCoeTC : {α : Sort u_1} → CoeTC α α
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getElem?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.Equiv t₂ → t₁[k]? = t₂[k]?
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuous_sum : ∀ {α : Type u_1} [inst : TopologicalSpace α] {ι : Type u_4} {γ : Type u_5} [inst_1 : AddCommMonoid γ]
  [inst_2 : LinearOrder γ] [IsOrderedAddMonoid γ] [inst_4 : TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ]
  {f : ι → α → γ} {a : Finset ι}, (∀ i ∈ a, LowerSemicontinuous (f i)) → LowerSemicontinuous fun z => ∑ i ∈ a, f i z
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.instOne : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {X : Type u_2} → [inst_2 : MulAction R X] → [One X] → One (OreLocalization S X)
-- Mathlib.Data.List.Shortlex
List.Shortlex.wf : ∀ {α : Type u_1} {r : α → α → Prop}, WellFounded r → WellFounded (List.Shortlex r)
-- Init.Data.UInt.Lemmas
USize.ofNat_le_iff_le : ∀ {a b : ℕ}, a < USize.size → b < USize.size → (USize.ofNat a ≤ USize.ofNat b ↔ a ≤ b)
-- Mathlib.Data.Set.Subset
Set.subset_of_image_val_subset_image_val : ∀ {α : Type u_2} {A : Set α} {D E : Set ↑A}, Subtype.val '' D ⊆ Subtype.val '' E → D ⊆ E
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.ordCompare_minKey_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] {t : Std.TreeMap α β compare} {k : α} {f : β → β}
  {he : (t.modify k f).isEmpty = false}, compare ((t.modify k f).minKey he) (t.minKey ⋯) = Ordering.eq
-- Lean.DocString.Syntax
/-- Unordered List  -/
Lean.Doc.Syntax.ul : Lean.ParserDescr
-- Mathlib.Analysis.InnerProductSpace.PiL2
Matrix.toEuclideanLin_eq_toLin : ∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {m : Type u_7} {n : Type u_8} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  [inst_3 : Finite m], Matrix.toEuclideanLin = Matrix.toLin (PiLp.basisFun 2 𝕜 n) (PiLp.basisFun 2 𝕜 m)
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
_private.Mathlib.CategoryTheory.Limits.Shapes.Reflexive.0.CategoryTheory.Limits.reflexivePair.match_1.splitter : (motive : CategoryTheory.Limits.WalkingReflexivePair → Sort u_1) →
  (x : CategoryTheory.Limits.WalkingReflexivePair) →
    (Unit → motive CategoryTheory.Limits.WalkingReflexivePair.zero) →
      (Unit → motive CategoryTheory.Limits.WalkingReflexivePair.one) → motive x
-- Mathlib.Data.Erased
Erased.map_def : ∀ {α β : Type u_1}, (fun x1 x2 => x1 <$> x2) = Erased.map
-- Mathlib.Data.EReal.Basic
EReal.toENNReal_of_nonpos : ∀ {x : EReal}, x ≤ 0 → x.toENNReal = 0
-- Mathlib.CategoryTheory.Adjunction.Triple
/-- For an adjoint triple `F ⊣ G ⊣ H` where `F` and `H` are fully faithful, whiskering `G` with the
natural transformation `F ⟶ H` yields the composition of the counit of the first adjunction with
the unit of the second adjunction.  -/
CategoryTheory.Adjunction.Triple.whiskerLeft_leftToRight_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [inst_2 : F.Full] [inst_3 : F.Faithful]
  {Z : CategoryTheory.Functor D D} (h : G.comp H ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.whiskerLeft t.leftToRight) h =
    CategoryTheory.CategoryStruct.comp t.adj₁.counit (CategoryTheory.CategoryStruct.comp t.adj₂.unit h)
-- Lean.Parser.Basic
/-- Parses the `#`'s and `"` at the beginning of the raw string.
The `num` variable counts the number of `#`s after the `r`.
 -/
_private.Lean.Parser.Basic.0.Lean.Parser.rawStrLitFnAux.initState : String.Pos.Raw → ℕ → Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- **Alias** of `FunLike.coe_sub`. -/
QuadraticMap.coeFn_sub : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Sub F] [inst_2 : Sub β]
  [IsSubApply F α β] (f g : F), ⇑(f - g) = ⇑f - ⇑g
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey!_eq_head!_keys : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  List.Pairwise (fun a b => compare a.fst b.fst = Ordering.lt) l →
    Std.Internal.List.minKey! l = (Std.Internal.List.keys l).head!
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.psi_le_primeCounting_mul_log' : ∀ (x : ℝ), Chebyshev.psi x ≤ ↑⌊x⌋₊.primeCounting * Real.log x
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- In the presence of zero morphisms, projections into a product are (split) epimorphisms.  -/
CategoryTheory.Limits.isSplitEpi_prod_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  [inst_2 : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.pair X Y)],
  CategoryTheory.IsSplitEpi CategoryTheory.Limits.prod.snd
-- Mathlib.LinearAlgebra.Prod
Submodule.prod_eq_top_iff : ∀ (R : Type u) (M : Type v) (M₂ : Type w) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] {p₁ : Submodule R M} {p₂ : Submodule R M₂},
  p₁.prod p₂ = ⊤ ↔ p₁ = ⊤ ∧ p₂ = ⊤
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey?_eq_head?_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.minKey? = t.keys.head?
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.mem_ofFinEmb_iff_mem_range : ∀ (n : ℕ) (β : Type u_2) (f : Fin n ↪ β) (b : β), b ∈ Set.powersetCard.ofFinEmb n β f ↔ b ∈ Set.range ⇑f
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.mk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : CategoryTheory.Functor C MonCat}
  (obj obj_1 : (U : C) → Submonoid ↑(M.obj U)) (e_obj : obj = obj_1)
  (map : ∀ {U V : C} (i : U ⟶ V), obj U ≤ Submonoid.comap (MonCat.Hom.hom (M.map i)) (obj V)),
  { obj := obj, map := map } = { obj := obj_1, map := ⋯ }
-- Mathlib.SetTheory.ZFC.Rank
_private.Mathlib.SetTheory.ZFC.Rank.0.PSet.rank.match_1.eq_1 : ∀ (motive : PSet.{u_1} → Sort u_2) (α : Type u_1) (A : α → PSet.{u_1})
  (h_1 : (α : Type u_1) → (A : α → PSet.{u_1}) → motive (PSet.mk α A)),
  (match PSet.mk α A with
    | PSet.mk α A => h_1 α A) =
    h_1 α A
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey?_ofList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (Std.DTreeMap.Raw.Const.ofList l cmp).getKey? k = none
-- Lean.Meta.Tactic.Grind.Ctor
/-- Given constructors `a` and `b`, propagate equalities if they are the same,
and close goal if they are different.
 -/
Lean.Meta.Grind.propagateCtor : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Init.Data.Int.Order
Int.le_add_of_neg_add_le_left : ∀ {a b c : ℤ}, -b + a ≤ c → a ≤ b + c
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
StarAlgebra.elemental.instCommCStarAlgebraSubtypeMemStarSubalgebraComplexOfIsStarNormal : {A : Type u_1} → [inst : CStarAlgebra A] → (a : A) → [IsStarNormal a] → CommCStarAlgebra ↥(StarAlgebra.elemental ℂ a)
-- Mathlib.Algebra.Polynomial.Mirror
Polynomial.natDegree_mul_mirror : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) [NoZeroDivisors R], (p * p.mirror).natDegree = 2 * p.natDegree
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_comp_monomial : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ), PowerSeries.coeff n ∘ₗ PowerSeries.monomial n = LinearMap.id
-- Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
/-- Given any commuting diagram
```
Z' --→ X
|      |
↓      ↓
Z  --→ Y
```
With `X ⟶ Y` formally unramified and `Z' ⟶ Z` an infinitesimal thickening, there exists at most
one arrow `Z ⟶ X` making the diagram commute.
 -/
AlgebraicGeometry.FormallyUnramified.hom_ext : ∀ {X Y Z' Z : AlgebraicGeometry.Scheme} (i : Z' ⟶ Z),
  IsNilpotent (AlgebraicGeometry.Scheme.Hom.ker i) →
    ∀ [AlgebraicGeometry.IsClosedImmersion i] (f : X ⟶ Y) [AlgebraicGeometry.FormallyUnramified f] {g₁ g₂ : Z ⟶ X},
      CategoryTheory.CategoryStruct.comp i g₁ = CategoryTheory.CategoryStruct.comp i g₂ →
        CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f → g₁ = g₂
-- Mathlib.Algebra.Homology.TotalComplex
/-- The vertical differential in the total complex.  -/
HomologicalComplex₂.D₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {I₁ : Type u_2} →
        {I₂ : Type u_3} →
          {I₁₂ : Type u_4} →
            {c₁ : ComplexShape I₁} →
              {c₂ : ComplexShape I₂} →
                (K : HomologicalComplex₂ C c₁ c₂) →
                  (c₁₂ : ComplexShape I₁₂) →
                    [inst_2 : TotalComplexShape c₁ c₂ c₁₂] →
                      [DecidableEq I₁₂] →
                        [inst_4 : K.HasTotal c₁₂] →
                          (i₁₂ i₁₂' : I₁₂) →
                            K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instIsEquivalenceActionModuleCatActionToRep : ∀ (k : Type u) (G : Type v) [inst : Ring k] [inst_1 : Monoid G], (Rep.ActionToRep k G).IsEquivalence
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
SimpleGraph.CliqueFree.not_farFromTriangleFree : ∀ {α : Type u_1} {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {G : SimpleGraph α}
  {ε : 𝕜} [inst_3 : Fintype α] [inst_4 : DecidableRel G.Adj] [Nonempty α],
  G.CliqueFree 3 → 0 < ε → ¬G.FarFromTriangleFree ε
-- Mathlib.Combinatorics.Additive.CauchyDavenport
_private.Mathlib.Combinatorics.Additive.CauchyDavenport.0.devosAddRel_of_le_of_le : ∀ {α : Type u_2} [inst : AddGroup α] [inst_1 : DecidableEq α] {x y : Finset α × Finset α},
  (x.1 + x.2).card ≤ (y.1 + y.2).card →
    y.1.card + y.2.card ≤ x.1.card + x.2.card → x.1.card < y.1.card → DevosAddRel✝ x y
-- Mathlib.CategoryTheory.Galois.EssSurj
_private.Mathlib.CategoryTheory.Galois.EssSurj.0.CategoryTheory.PreGaloisCategory.functorToAction_map_quotientToEndObjectHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat}
  [inst_1 : CategoryTheory.GaloisCategory C] [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F]
  (V : OpenSubgroup (CategoryTheory.Aut F)) {U : OpenSubgroup (CategoryTheory.Aut F)} (h : (↑U).Normal) {A : C}
  (u :
    (CategoryTheory.PreGaloisCategory.functorToAction F).obj A ≅
      Action.FintypeCat.ofMulAction (CategoryTheory.Aut F) (FintypeCat.of (CategoryTheory.Aut F ⧸ ↑U)))
  (m :
    CategoryTheory.SingleObj.star (↥V ⧸ (↑U).subgroupOf ↑V) ⟶ CategoryTheory.SingleObj.star (↥V ⧸ (↑U).subgroupOf ↑V)),
  (CategoryTheory.PreGaloisCategory.functorToAction F).map
      ((CategoryTheory.PreGaloisCategory.quotientToEndObjectHom✝ V h u) m) =
    CategoryTheory.CategoryStruct.comp u.hom
      (CategoryTheory.CategoryStruct.comp ((Action.FintypeCat.quotientToEndHom ↑V ↑U) m) u.inv)
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- An `AddSubmonoid` of a unital additive magma inherits a unital additive magma structure.  -/
AddSubmonoid.toAddZeroClass : {M : Type u_5} → [inst : AddZeroClass M] → (S : AddSubmonoid M) → AddZeroClass ↥S
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.processInstImplicitArg.mkInstMVar : Lean.Name → Lean.Expr → Lean.Elab.Term.ElabAppArgs.M Lean.Expr
-- Mathlib.RingTheory.ZMod.UnitsCyclic
ZMod.orderOf_one_add_mul_prime_pow : ∀ {p : ℕ},
  Nat.Prime p → ∀ (m : ℕ), m ≠ 0 → m + 2 ≤ p * m → ∀ (a : ℤ), ¬↑p ∣ a → ∀ (n : ℕ), orderOf (1 + ↑p ^ m * ↑a) = p ^ n
-- Mathlib.Analysis.Normed.Algebra.Unitization
Unitization.splitMul_apply : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : IsScalarTower 𝕜 A A] [inst_4 : SMulCommClass 𝕜 A A] (x : Unitization 𝕜 A),
  (Unitization.splitMul 𝕜 A) x =
    (x.toProd.1, (algebraMap 𝕜 (A →L[𝕜] A)) x.toProd.1 + (ContinuousLinearMap.mul 𝕜 A) x.toProd.2)
-- Mathlib.Analysis.Convex.Segment
mem_segment_translate : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [AddRightMono 𝕜] [inst_3 : AddCommGroup E]
  [inst_4 : Module 𝕜 E] (a : E) {x b c : E}, a + x ∈ segment 𝕜 (a + b) (a + c) ↔ x ∈ segment 𝕜 b c
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.ofUnits_right_inverse : ∀ {M : Type u_1} [inst : Monoid M], Function.RightInverse Subgroup.ofUnits Submonoid.units
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.instRingHomClass : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ}, RingHomClass (𝒜 →+*ᵍ ℬ) A B
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.embedding_valueGroupOrderIso : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  (g : (MonoidWithZeroHom.ofClass (IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuation K v)).ValueGroup₀),
  MonoidWithZeroHom.ValueGroup₀.embedding
      ((IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderIso K v) g) =
    MonoidWithZeroHom.ValueGroup₀.embedding g
-- Mathlib.Topology.Covering.Basic
IsCoveringMapOn.of_isCoveringMap_subtype : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {s : Set X},
  IsOpen s → ∀ {f : E → X} (h : ∀ (x : E), f x ∈ s), (IsCoveringMap fun x => ⟨f x, ⋯⟩) → IsCoveringMapOn f s
-- Mathlib.Geometry.Convex.ConvexSpace.Prod
Prod.snd_iConvexComb : ∀ {I : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  {X : Type u_3} {Y : Type u_4} [inst_3 : Convexity.ConvexSpace R X] [inst_4 : Convexity.ConvexSpace R Y]
  (w : Convexity.StdSimplex R I) (f : I → X × Y),
  (Convexity.iConvexComb w f).2 = Convexity.iConvexComb w fun i => (f i).2
-- Mathlib.Algebra.Lie.DirectSum
/-- The projection map onto one component, as a morphism of Lie algebras.  -/
DirectSum.lieAlgebraComponent : (R : Type u) →
  (ι : Type v) →
    [inst : CommRing R] →
      (L : ι → Type w) →
        [inst_1 : (i : ι) → LieRing (L i)] →
          [inst_2 : (i : ι) → LieAlgebra R (L i)] → (j : ι) → (DirectSum ι fun i => L i) →ₗ⁅R⁆ L j
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.denseRange_coe₂ : ∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β], DenseRange fun x => (↑x.1, ↑x.2)
-- Mathlib.Data.List.Chain
/-- If there is a non-empty `r`-chain, its head and last element are related by the
reflexive transitive closure of `r`.
 -/
List.relationReflTransGen_of_exists_isChain : ∀ {α : Type u_1} {r : α → α → Prop} (l : List α),
  List.IsChain r l → ∀ (hne : l ≠ []), Relation.ReflTransGen r (l.head hne) (l.getLast hne)
-- Mathlib.CategoryTheory.Adjunction.Comma
/-- If each costructured arrow category on `G` has a terminal object, construct a right adjoint to `G`.
It is shown that it is a right adjoint in `adjunctionOfCostructuredArrowTerminals`.
 -/
CategoryTheory.rightAdjointOfCostructuredArrowTerminals : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor D C) →
          [∀ (A : C), CategoryTheory.Limits.HasTerminal (CategoryTheory.CostructuredArrow G A)] →
            CategoryTheory.Functor C D
-- Mathlib.LinearAlgebra.AffineSpace.Centroid
/-- The weights for the centroid of some points.  -/
Finset.centroidWeights : (k : Type u_1) → [DivisionRing k] → {ι : Type u_4} → Finset ι → ι → k
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- Construct an affine scheme from a scheme and the information that it is affine.
Also see `AffineScheme.of` for a typeclass version.  -/
AlgebraicGeometry.AffineScheme.mk : (X : AlgebraicGeometry.Scheme) → AlgebraicGeometry.IsAffine X → AlgebraicGeometry.AffineScheme
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_zero : CategoryTheory.Limits.walkingParallelPairOpEquiv.unitIso.app CategoryTheory.Limits.WalkingParallelPair.zero =
  CategoryTheory.Iso.refl CategoryTheory.Limits.WalkingParallelPair.zero