mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preorder
Preorder.instHasInitialOfOrderBot : ∀ {C : Type u} [inst : Preorder C] [OrderBot C], CategoryTheory.Limits.HasInitial C
-- Mathlib.LinearAlgebra.PiTensorProduct.Finsupp
PiTensorProduct.ofFinsuppEquiv'_apply_apply : ∀ {R : Type u_1} {ι : Type u_2} {κ : ι → Type u_3} [inst : CommSemiring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι]
  [inst_3 : (i : ι) → DecidableEq (κ i)] [inst_4 : DecidableEq R] (f : (i : ι) → κ i →₀ R) (p : (i : ι) → κ i),
  (PiTensorProduct.ofFinsuppEquiv' ((PiTensorProduct.tprod R) fun i => f i)) p = ∏ i, (f i) (p i)
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.mem_range : ∀ {V₁ : Type u_3} {V₂ : Type u_4} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (f : NormedAddGroupHom V₁ V₂) (v : V₂), v ∈ f.range ↔ ∃ w, f w = v
-- Mathlib.RingTheory.Polynomial.Dickson
Polynomial.dickson_two_zero : ∀ {R : Type u_1} [inst : CommRing R] (n : ℕ), Polynomial.dickson 2 0 n = Polynomial.X ^ n
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.qsmul_def : ∀ {M : Type u_2} [inst : AddCommGroup M] (a : ℚ) (x : DivisibleHull M),
  a • x =
    ↑(SignType.sign a) •
      (have this := ⟨|a|, ⋯⟩;
        this) •
        x
-- Init.Data.Array.Lemmas
Array.map_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ} {as : Array α},
  Array.map g (Array.map f as) = Array.map (g ∘ f) as
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
/-- A map approximating a linear equivalence on a set defines a partial equivalence on this set.
Should not be used outside of this file, because it is superseded by `toOpenPartialHomeomorph`
below.

This is a first step towards the inverse function.  -/
ApproximatesLinearOn.toPartialEquiv : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_3} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                {f : E → F} →
                  {f' : E ≃L[𝕜] F} →
                    {s : Set E} →
                      {c : NNReal} →
                        ApproximatesLinearOn f (↑f') s c → Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹ → PartialEquiv E F
-- Init.Data.String.Basic
String.Pos.Raw.get!_eq_get : ∀ (s : String) (p : String.Pos.Raw), String.Pos.Raw.get! s p = String.Pos.Raw.get s p
-- Mathlib.Topology.ContinuousMap.Defs
/-- Copy of a `ContinuousMap` with a new `toFun` equal to the old one. Useful to fix definitional
equalities.  -/
ContinuousMap.copy : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → (f : C(X, Y)) → (f' : X → Y) → f' = ⇑f → C(X, Y)
-- Lean.Meta.Tactic.Simp.Types
/-- `wellBehavedDischarge` must **not** be set to `true` IF `discharge?`
access local declarations with index >= `Context.lctxInitIndices` when
`contextual := false`.
Reason: it would prevent us from aggressively caching `simp` results.
 -/
Lean.Meta.Simp.Methods.wellBehavedDischarge : Lean.Meta.Simp.Methods → Bool
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.rid_comp_map : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {M' : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : AddCommMonoid M']
  [inst_6 : Module R M'] (f : M →ₗ[R] M') (g : N →ₗ[R] R),
  ↑(TensorProduct.rid R M') ∘ₗ TensorProduct.map f g = f ∘ₗ ↑(TensorProduct.rid R M) ∘ₗ TensorProduct.map LinearMap.id g
-- Mathlib.AlgebraicGeometry.Sites.Fpqc
AlgebraicGeometry.Scheme.fppfPrecoverage_le_fpqcPrecoverage : AlgebraicGeometry.Scheme.fppfPrecoverage ≤ AlgebraicGeometry.Scheme.fpqcPrecoverage
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKeyD_insertManyIfNewUnit!_list_of_not_mem_of_mem : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α],
  t.WF →
    ∀ {l : List α} {k k' fallback : α},
      compare k k' = Ordering.eq →
        k ∉ t →
          List.Pairwise (fun a b => ¬compare a b = Ordering.eq) l →
            k ∈ l → (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l)).getKeyD k' fallback = k
-- Init.Data.Array.MapIdx
_private.Init.Data.Array.MapIdx.0.Array.mapFinIdxM.map.match_1.eq_2 : ∀ {α : Type u_1} (as : Array α) (j : ℕ) (motive : (i : ℕ) → i + j = as.size → Sort u_2) (i : ℕ)
  (inv : i + 1 + j = as.size) (h_1 : (x : 0 + j = as.size) → motive 0 x)
  (h_2 : (i : ℕ) → (inv : i + 1 + j = as.size) → motive i.succ inv),
  (match i.succ, inv with
    | 0, x => h_1 x
    | i.succ, inv => h_2 i inv) =
    h_2 i inv
-- Mathlib.RingTheory.LocalProperties.IntegrallyClosed
IsIntegrallyClosed.of_localization_submonoid : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {ι : Type u_3} (S : ι → Submonoid R)
  (h : ∀ (i : ι), S i ≤ nonZeroDivisors R),
  (∀ (i : ι), IsIntegrallyClosed (Localization (S i))) →
    ⨅ i, Localization.subalgebra (FractionRing R) (S i) ⋯ = ⊥ → IsIntegrallyClosed R
-- Mathlib.Algebra.Group.Finsupp
/-- If `M` is the trivial monoid, then the monoid of finitely supported functions `ι →₀ M` is
is isomorphic to `M`.  -/
AddEquiv.finsuppUnique : {M : Type u_3} → [inst : AddZeroClass M] → {ι : Type u_8} → [Unique ι] → (ι →₀ M) ≃+ M
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
/-- The chosen terminal object in `Cat`.  -/
CategoryTheory.Cat.chosenTerminal : CategoryTheory.Cat
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.eval.eq_3 : Turing.ToPartrec.Code.tail.eval = fun v => pure v.tail
-- Lean.Meta.Tactic.LibrarySearch
Lean.Meta.LibrarySearch.DeclMod.ofNat : ℕ → Lean.Meta.LibrarySearch.DeclMod
-- Mathlib.LinearAlgebra.Dual.Defs
LinearMap.dualMap_def : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] (f : M₁ →ₗ[R] M₂),
  f.dualMap = Module.Dual.transpose f
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instSub : {G : Type u_1} → [inst : TopologicalSpace G] → [inst_1 : Sub G] → [ContinuousSub G] → Sub (SeparationQuotient G)
-- Init.System.IOError
/-- Some error not covered by the other constructors of `IO.Error` occurred.

This also includes POSIX error `EFAULT`.
 -/
IO.Error.otherError : UInt32 → String → IO.Error
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKeyD_modifyKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  [inst_4 : Std.LawfulEqOrd α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : β k → β k} {fallback : α},
      Std.Internal.List.maxKeyD (Std.Internal.List.modifyKey k f l) fallback = Std.Internal.List.maxKeyD l fallback
-- Mathlib.Topology.Order
induced_inf : ∀ {α : Type u_1} {β : Type u_2} {t₁ t₂ : TopologicalSpace α} {g : β → α},
  TopologicalSpace.induced g (t₁ ⊓ t₂) = TopologicalSpace.induced g t₁ ⊓ TopologicalSpace.induced g t₂
-- Mathlib.Order.Interval.Set.OrderIso
OrderIso.preimage_Iio : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) (b : β),
  ⇑e ⁻¹' Set.Iio b = Set.Iio (e.symm b)
-- Mathlib.CategoryTheory.Sites.Plus
CategoryTheory.GrothendieckTopology.diagramFunctor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w)
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  (X : C) (P : CategoryTheory.Functor Cᵒᵖ D), (J.diagramFunctor D X).obj P = J.diagram P X
-- Mathlib.Data.Finset.Sym
Finset.diag_mem_sym2_mem_iff : ∀ {α : Type u_1} {s : Finset α} {a : α}, (∀ b ∈ Sym2.diag a, b ∈ s) ↔ a ∈ s
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- The map from the third isomorphism theorem for additive groups:
`(A / N) / (M / N) → A / M`.  -/
QuotientAddGroup.quotientQuotientEquivQuotientAux : {G : Type u} →
  [inst : AddGroup G] →
    (N : AddSubgroup G) →
      [nN : N.Normal] →
        (M : AddSubgroup G) → [nM : M.Normal] → N ≤ M → (G ⧸ N) ⧸ AddSubgroup.map (QuotientAddGroup.mk' N) M →+ G ⧸ M
-- Mathlib.Analysis.Complex.Basic
RCLike.normSq_to_complex : ∀ {x : ℂ}, RCLike.normSq x = Complex.normSq x
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- Circle integrability is invariant when taking negative radius.
 -/
circleIntegrable_neg_radius : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {c : ℂ} {R : ℝ} {f : ℂ → E},
  CircleIntegrable f c (-R) ↔ CircleIntegrable f c R
-- Mathlib.Analysis.Convex.Topology
Convex.openSegment_closure_interior_subset_interior : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E},
  Convex 𝕜 s → ∀ {x y : E}, x ∈ closure s → y ∈ interior s → openSegment 𝕜 x y ⊆ interior s
-- Mathlib.CategoryTheory.Groupoid
CategoryTheory.instIsGroupoid : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C], CategoryTheory.IsGroupoid C
-- Mathlib.Algebra.GradedMonoid
/-- A graded version of `One`, which must be of grade 0.  -/
GradedMonoid.GOne : {ι : Type u_1} → (ι → Type u_2) → [Zero ι] → Type u_2
-- Mathlib.Analysis.Convex.Join
convexJoin_singleton_right : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] (s : Set E) (y : E), convexJoin 𝕜 s {y} = ⋃ x ∈ s, segment 𝕜 x y
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.insertMany_list : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ (l : List (α × β)), (t₁.insertMany l).Equiv (t₂.insertMany l)
-- Mathlib.LinearAlgebra.Alternating.Curry
/-- `AlternatingMap.curryLeft` as a `LinearMap`. This is a separate definition as dot notation
does not work for this version.  -/
AlternatingMap.curryLeftLinearMap : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module R M] →
              [inst_4 : Module R N] → {n : ℕ} → M [⋀^Fin n.succ]→ₗ[R] N →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
-- Mathlib.MeasureTheory.Integral.Layercake
MeasureTheory.Integrable.integral_eq_integral_meas_le : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.Integrable f μ → 0 ≤ᵐ[μ] f → ∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Set.Ioi 0, μ.real {a | t ≤ f a}
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
intervalIntegral.continuousOn_primitive : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ}
  {f : ℝ → E} [MeasureTheory.NullSingletonClass μ],
  MeasureTheory.IntegrableOn f (Set.Icc a b) μ → ContinuousOn (fun x => ∫ (t : ℝ) in Set.Ioc a x, f t ∂μ) (Set.Icc a b)
-- Mathlib.Tactic.Ring.NamePolyVars
/-- The command `name_poly_vars` names variables in
`MvPolynomial (Fin n) R` for the appropriate value of `n`.
The notation introduced by this command is local.

Usage:

```lean
variable (R : Type) [CommRing R]

name_poly_vars X, Y, Z over R

#check Y -- Y : MvPolynomial (Fin 3) R
```
 -/
Mathlib.Tactic.elabNameVariablesOver : Lean.Elab.Command.CommandElab
-- Mathlib.NumberTheory.RatFunc.Ostrowski
RatFunc.adicValuation_not_isEquiv_infty_valuation : ∀ {K : Type u_1} [inst : Field K] [inst_1 : DecidableEq (RatFunc K)]
  (p : IsDedekindDomain.HeightOneSpectrum (Polynomial K)),
  ¬(IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) p).IsEquiv (RatFunc.inftyValuation K)
-- Mathlib.Tactic.FunProp.FunctionData
Mathlib.Meta.FunProp.MaybeFunctionData.letE.sizeOf_spec : ∀ (f : Lean.Expr), sizeOf (Mathlib.Meta.FunProp.MaybeFunctionData.letE f) = 1 + sizeOf f
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.logOrderIso_apply : ∀ {G : Type u_3} [inst : Preorder G] [inst_1 : AddGroup G] (a : (WithZero (Multiplicative G))ˣ),
  WithZero.logOrderIso a = Multiplicative.toAdd (WithZero.unzero ⋯)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyOutgoingCallsParams.item : Lean.Lsp.CallHierarchyOutgoingCallsParams → Lean.Lsp.CallHierarchyItem
-- Mathlib.RingTheory.RingHom.LocallyStandardSmooth
/-- A ring homomorphism is smooth if and only if it is locally standard smooth.  -/
RingHom.smooth_iff_locally_isStandardSmooth : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  f.Smooth ↔ RingHom.Locally (fun {R S} [CommRing R] [CommRing S] => RingHom.IsStandardSmooth) f
-- Mathlib.Topology.Order.Basic
nhdsGE_eq_iInf_principal : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [OrderTopology α] {a : α},
  (∃ u, a < u) → nhdsWithin a (Set.Ici a) = ⨅ u, ⨅ (_ : a < u), Filter.principal (Set.Ico a u)
-- Mathlib.Topology.Order.LocalExtr
IsLocalMinOn.comp_continuousOn : ∀ {α : Type u} {β : Type v} {δ : Type x} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β}
  [inst_2 : TopologicalSpace δ] {t : Set α} {s : Set δ} {g : δ → α} {b : δ},
  IsLocalMinOn f t (g b) → s ⊆ g ⁻¹' t → ContinuousOn g s → b ∈ s → IsLocalMinOn (f ∘ g) s b
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- The relationship between the unit and hom set equivalence of an adjunction  -/
CategoryTheory.Adjunction.CoreHomEquivUnitCounit.homEquiv_unit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (self : CategoryTheory.Adjunction.CoreHomEquivUnitCounit F G) {X : C} {Y : D} {f : F.obj X ⟶ Y},
  (self.homEquiv X Y) f = CategoryTheory.CategoryStruct.comp (self.unit.app X) (G.map f)
-- Init.Data.AC
_private.Init.Data.AC.0.Lean.Data.AC.removeNeutrals.loop.match_3.splitter : (motive : List ℕ → Sort u_1) →
  (x : List ℕ) → ((x : ℕ) → (xs : List ℕ) → motive (x :: xs)) → (Unit → motive []) → motive x
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.lt_iff : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {hI : DividedPowers I} {J J' : hI.SubDPIdeal},
  J < J' ↔ J.carrier < J'.carrier
-- Batteries.Recycling.RBTree.Basic
/-- Asserts that `t₁` and `t₂` have the same set of keys (up to equality).  -/
RBTree.RBMap.eqKeys : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → {γ : Type u_1} → RBTree.RBMap α β cmp → RBTree.RBMap α γ cmp → Bool
-- Lean.Parser.Term
Lean.Parser.Term.letConfig.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_atTop_mul_right_of_le' : ∀ {α : Type u_1} {G : Type u_2} [inst : CommGroup G] [inst_1 : PartialOrder G] [IsOrderedMonoid G] (l : Filter α)
  {f g : α → G} (C : G),
  Filter.Tendsto f l Filter.atTop → (∀ᶠ (x : α) in l, C ≤ g x) → Filter.Tendsto (fun x => f x * g x) l Filter.atTop
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.openCell_subset_skeleton : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D] (n : ℕ)
  (j : Topology.RelCWComplex.cell C n), Topology.RelCWComplex.openCell n j ⊆ ↑(Topology.RelCWComplex.skeleton C ↑n)
-- Mathlib.Algebra.Homology.Double
/-- The isomorphism `(double f hi₀₁).X i₁ ≅ X₁`.  -/
HomologicalComplex.doubleXIso₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        {X₀ X₁ : C} →
          (f : X₀ ⟶ X₁) →
            {ι : Type u_2} →
              {c : ComplexShape ι} →
                {i₀ i₁ : ι} → (hi₀₁ : c.Rel i₀ i₁) → i₀ ≠ i₁ → ((HomologicalComplex.double f hi₀₁).X i₁ ≅ X₁)
-- Mathlib.Analysis.Convex.Basic
Convex.openSegment_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {s : Set E}, Convex 𝕜 s → ∀ {x y : E}, x ∈ s → y ∈ s → openSegment 𝕜 x y ⊆ s
-- Mathlib.Analysis.Seminorm
Seminorm.mem_ball_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E]
  (p : Seminorm 𝕜 E) {y : E} {r : ℝ}, y ∈ p.ball 0 r ↔ p y < r
-- Mathlib.CategoryTheory.Monoidal.CommComon_
CategoryTheory.CommComon.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] [inst_3 : SizeOf C] (X : C) [comon : CategoryTheory.ComonObj X]
  [comm : CategoryTheory.IsCommComonObj X],
  sizeOf { X := X, comon := comon, comm := comm } = 1 + sizeOf X + sizeOf comon + sizeOf comm
-- Mathlib.CategoryTheory.Galois.Prorepresentability
/-- `obj` is Galois.  -/
CategoryTheory.PreGaloisCategory.PointedGaloisObject.isGalois : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  {F : CategoryTheory.Functor C FintypeCat} (self : CategoryTheory.PreGaloisCategory.PointedGaloisObject F),
  CategoryTheory.PreGaloisCategory.IsGalois self.obj
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.finiteDimensional_iSup_of_finset' : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {ι : Type u_5}
  {t : ι → IntermediateField K L} {s : Finset ι},
  (∀ i ∈ s, FiniteDimensional K ↥(t i)) → FiniteDimensional K ↥(⨆ i ∈ s, t i)
-- Mathlib.Data.NNReal.Basic
NNReal.iInf_mul : ∀ {ι : Sort u_3} (f : ι → NNReal) (a : NNReal), iInf f * a = ⨅ i, f i * a
-- Mathlib.Order.RelClasses
/-- **Alias** of `InvImage.trichotomous`. -/
InvImage.isTrichotomous : ∀ {α : Type u} {β : Type v} {r : α → α → Prop} [Std.Trichotomous r] {f : β → α},
  Function.Injective f → Std.Trichotomous (InvImage r f)
-- Mathlib.RingTheory.SimpleRing.Congr
IsSimpleRing.of_ringEquiv : ∀ {R : Type u_1} {S : Type u_2} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] (f : R ≃+* S),
  IsSimpleRing R → IsSimpleRing S
-- Aesop.Forward.LevelIndex
Aesop.LevelIndex.mk.inj : ∀ {toNat toNat_1 : ℕ}, { toNat := toNat } = { toNat := toNat_1 } → toNat = toNat_1
-- Mathlib.Topology.Order.CountableSeparating
Filter.EventuallyEq.of_forall_eventually_ge_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : LinearOrder X] [OrderTopology X] [SecondCountableTopology X]
  {α : Type u_2} {l : Filter α} [CountableInterFilter l] {f g : α → X},
  (∀ (x : X), ∀ᶠ (a : α) in l, x ≤ f a ↔ x ≤ g a) → f =ᶠ[l] g
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
RingNorm.apply_one : ∀ (R : Type u_1) [inst : NonUnitalRing R] [inst_1 : DecidableEq R] (x : R), 1 x = if x = 0 then 0 else 1
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- A free group basis `FreeAddGroupBasis ι G` is a structure recording the isomorphism between an
additive group `G` and the additive free group over `ι`. One may think of such a basis as a function
from `ι` to `G` (which is registered through a `FunLike` instance) together with the fact that the
morphism induced by this function from `FreeAddGroup ι` to `G` is an isomorphism.  -/
FreeAddGroupBasis : Type u_1 → (G : Type u_2) → [AddGroup G] → Type (max u_1 u_2)
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.expand_expand : ∀ {R : Type u} [inst : CommSemiring R] (p q : ℕ) (f : Polynomial R),
  (Polynomial.expand R p) ((Polynomial.expand R q) f) = (Polynomial.expand R (p * q)) f
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.interSmallerFn.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m sofar : Std.DHashMap.Internal.Raw₀ α β) (k : α),
  m.interSmallerFn sofar k =
    match m.getEntry? k with
    | some kv' => sofar.insert kv'.fst kv'.snd
    | none => sofar
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedBilinearMap.smul_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] [inst_5 : SeminormedAddCommGroup G]
  [inst_6 : Module 𝕜 G] {f : E × F → G},
  IsBoundedBilinearMap 𝕜 f → ∀ (c : 𝕜) (x : E) (y : F), f (c • x, y) = c • f (x, y)
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_rotateLeft : ∀ {w : ℕ} {x : BitVec w} {r i : ℕ},
  (x.rotateLeft r).getLsbD i =
    bif decide (i < r % w) then x.getLsbD (w - r % w + i) else decide (i < w) && x.getLsbD (i - r % w)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- A natural isomorphism `R₁ ≅ R₂` induces an equivalence of categories
`P.Comma L R₁ Q W ≌ P.Comma L R₂ Q W`.  -/
CategoryTheory.MorphismProperty.Comma.mapRightIso : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {B : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
        {T : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} T] →
            (L : CategoryTheory.Functor A T) →
              {P : CategoryTheory.MorphismProperty T} →
                {Q : CategoryTheory.MorphismProperty A} →
                  {W : CategoryTheory.MorphismProperty B} →
                    [inst_3 : Q.IsMultiplicative] →
                      [inst_4 : W.IsMultiplicative] →
                        {R₁ R₂ : CategoryTheory.Functor B T} →
                          [P.RespectsIso] →
                            [Q.RespectsIso] →
                              [W.RespectsIso] →
                                (R₁ ≅ R₂) →
                                  (CategoryTheory.MorphismProperty.Comma L R₁ P Q W ≌
                                    CategoryTheory.MorphismProperty.Comma L R₂ P Q W)
-- Mathlib.Algebra.Order.Kleene
Pi.kstar_apply : ∀ {ι : Type u_3} {π : ι → Type u_4} [inst : (i : ι) → KleeneAlgebra (π i)] (a : (i : ι) → π i) (i : ι),
  KStar.kstar a i = KStar.kstar (a i)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RocSliceData.mk.injEq : ∀ {α : Type u} {β : Type v} [inst : Ord α] (treeMap : Std.DTreeMap.Internal.Impl α fun x => β) (range : Std.Roc α)
  (treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => β) (range_1 : Std.Roc α),
  ({ treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 }) =
    (treeMap = treeMap_1 ∧ range = range_1)
-- Init.Sym.Lemmas
Lean.Sym.or_eq_right : ∀ (a b : Prop), a = False → (a ∨ b) = b
-- Lean.Elab.DefView
Lean.Elab.DefView.declId : Lean.Elab.DefView → Lean.Syntax
-- Mathlib.SetTheory.Lists
Lists'.cons' : {α : Type u} → {b : Bool} → Lists' α b → Lists' α true → Lists' α true
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.contDiff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  {n : WithTop ℕ∞} (h : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' n), ContDiff 𝕜 n ⇑h
-- Mathlib.RingTheory.MatrixAlgebra
Matrix.toAlgEquiv_kroneckerTMulStarAlgEquiv : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_5) (S : Type u_6) {A : Type u_7} {B : Type u_8} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Fintype n]
  [inst_6 : DecidableEq n] [inst_7 : CommSemiring S] [inst_8 : Algebra R S] [inst_9 : Algebra S A]
  [inst_10 : IsScalarTower R S A] [inst_11 : Fintype m] [inst_12 : DecidableEq m] [inst_13 : StarRing R]
  [inst_14 : StarAddMonoid A] [inst_15 : StarAddMonoid B] [inst_16 : StarModule R A] [inst_17 : StarModule R B],
  (Matrix.kroneckerTMulStarAlgEquiv m n R S A B).toAlgEquiv = Matrix.kroneckerTMulAlgEquiv m n R S A B
-- Mathlib.Algebra.Category.Grp.Limits
CommGrpCat.forget_createsLimitsOfShape : (J : Type v) →
  [inst : CategoryTheory.Category.{w, v} J] → CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.forget CommGrpCat)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max_eq_iff_mem_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {he : t ≠ ∅} {km : α}, t.max he = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Computability.Partrec
Computable.vector_tail : ∀ {α : Type u_1} [inst : Primcodable α] {n : ℕ}, Computable List.Vector.tail