mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.instGrindPowIdentity : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Fintype K], Lean.Grind.PowIdentity K (Fintype.card K)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.mkOfAlgebra : ∀ {R : Type u_6} {S : Type u_7} {S' : Type u_8} [inst : CommSemiring R] [inst_1 : Ring S] [inst_2 : Ring S']
  [inst_3 : Algebra R S] [inst_4 : Algebra R S'] (M : Submonoid R) (f : S →ₐ[R] S'),
  (∀ x ∈ M, IsUnit ((algebraMap R S') x)) →
    (∀ (y : S'), ∃ x, x.2 • y = f x.1) → (∀ (x : S), f x = 0 → ∃ m, m • x = 0) → IsLocalizedModule M f.toLinearMap
-- Mathlib.Algebra.Group.Subsemigroup.Membership
/-- The supremum of a directed family of commutative subsemigroups is commutative.  -/
Subsemigroup.isMulCommutative_iSup : ∀ {ι : Sort u_1} {M : Type u_2} [inst : Mul M] {S : ι → Subsemigroup M} [hS : ∀ (i : ι), IsMulCommutative ↥(S i)],
  Directed (fun x1 x2 => x1 ≤ x2) S → IsMulCommutative ↥(⨆ i, S i)
-- Mathlib.Combinatorics.Configuration
Configuration.ProjectivePlane.toHasPoints : {P : Type u_1} →
  {L : Type u_2} → {inst : Membership P L} → [self : Configuration.ProjectivePlane P L] → Configuration.HasPoints P L
-- Std.Data.TreeMap.Raw.WF
Std.TreeMap.Raw.WF.diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {t₁ t₂ : Std.TreeMap.Raw α β cmp},
  t₁.WF → (t₁ \ t₂).WF
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁_shortExact : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ)
  (hn₁ :
    autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁_shortExact._auto_1)
  (hn₂ :
    autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁_shortExact._auto_3),
  (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ hn₁ hn₂).ShortExact
-- Mathlib.GroupTheory.IsSubnormal
/-- The trivial additive subgroup is subnormal.  -/
AddSubgroup.IsSubnormal.bot : ∀ {G : Type u_1} [inst : AddGroup G], ⊥.IsSubnormal
-- Mathlib.GroupTheory.GroupExtension.Basic
AddGroupExtension.surjInvRightHom.eq_1 : ∀ {N : Type u_1} {G : Type u_2} [inst : AddGroup N] [inst_1 : AddGroup G] {E : Type u_3} [inst_2 : AddGroup E]
  (S : AddGroupExtension N E G), S.surjInvRightHom = { toFun := Function.surjInv ⋯, rightInverse_rightHom := ⋯ }
-- Aesop.RuleSet
Aesop.BaseRuleSet.trace : Aesop.BaseRuleSet → Aesop.TraceOption → Lean.CoreM Unit
-- Std.Async.Signal
Std.Async.Signal.ofNat_ctorIdx : ∀ (x : Std.Async.Signal), Std.Async.Signal.ofNat x.ctorIdx = x
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_surjective_eq_arrow_of_lift_le : ∀ {α : Type u} {β' : Type v} [Infinite α],
  Cardinal.lift.{u, v} (Cardinal.mk β') ≤ Cardinal.lift.{v, u} (Cardinal.mk α) →
    Cardinal.mk ↑{f | Function.Surjective f} = Cardinal.mk (α → β')
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.ofPrime_top : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K), A.ofPrime (IsLocalRing.maximalIdeal ↥A) = A
-- Mathlib.LinearAlgebra.Projectivization.Basic
/-- Two nonzero vectors go to the same point in projective space if and only if one is
a scalar multiple of the other.  -/
Projectivization.mk_eq_mk_iff' : ∀ (K : Type u_1) {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (v w : V)
  (hv : v ≠ 0) (hw : w ≠ 0), Projectivization.mk K v hv = Projectivization.mk K w hw ↔ ∃ a, a • w = v
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.ofArrows_surj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {ι : Type u_1} {Y : ι → C} (f : (i : ι) → Y i ⟶ X)
  {Z : C} (g : Z ⟶ X),
  CategoryTheory.Presieve.ofArrows Y f g →
    ∃ i, ∃ (h : Y i = Z), g = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (f i)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.triangle_assoc_comp_left : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.id b) g).hom
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor g).hom) =
    CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor f).hom g
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.one_rpow : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] {x : ℝ}, 1 ^ x = 1
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.meas_iInter : ∀ {Ω : Type u_1} {ι : Type u_2} {κ : ι → Type u_5} {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ι → Set Ω}
  [inst : Fintype ι] {m : (i : ι) → MeasurableSpace (κ i)} {f : (x : ι) → Ω → κ x},
  ProbabilityTheory.iIndepFun f μ → (∀ (i : ι), MeasurableSet (s i)) → μ (⋂ i, s i) = ∏ i, μ (s i)
-- Mathlib.Algebra.Lie.UniversalEnveloping
/-- The quotient by the ideal generated by this relation is the universal enveloping algebra.

Note that we have avoided using the more natural expression:
```
| lie_compat (x y : L) : rel (ιₜ ⁅x, y⁆) ⁅ιₜ x, ιₜ y⁆
```
so that our construction needs only the semiring structure of the tensor algebra.  -/
UniversalEnvelopingAlgebra.Rel : (R : Type u₁) →
  (L : Type u₂) →
    [inst : CommRing R] →
      [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → TensorAlgebra R L → TensorAlgebra R L → Prop
-- Init.Data.Array.Find
Array.getElem?_zero_flatten : ∀ {α : Type u_1} (xss : Array (Array α)), xss.flatten[0]? = Array.findSome? (fun xs => xs[0]?) xss
-- Init.Data.List.Lex
List.cons_le_cons_iff : ∀ {α : Type u_1} [inst : LT α] [i₁ : Std.Asymm fun x1 x2 => x1 < x2] [i₂ : Std.Trichotomous fun x1 x2 => x1 < x2]
  {a b : α} {l₁ l₂ : List α}, a :: l₁ ≤ b :: l₂ ↔ a < b ∨ a = b ∧ l₁ ≤ l₂
-- Std.Time.Zoned.TimeZone
/-- Represents a timezone offset as a total number of seconds from UTC.
 -/
Std.Time.TimeZone.Offset : Type
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.ReflexiveRelation.reflexivity₁_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X}
  (self : CategoryTheory.ReflexiveRelation p₁ p₂) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.r (CategoryTheory.CategoryStruct.comp p₁ h) = h
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_zero : ∀ (x : NNReal), x ^ 0 = 1
-- Aesop.Search.Queue.Class
Aesop.Queue.init' : {Q : Type} → [Aesop.Queue Q] → Array Aesop.GoalRef → BaseIO Q
-- Mathlib.GroupTheory.Exponent
neg_eq_self_of_addOrderOf_eq_two : ∀ {G : Type u} [inst : AddGroup G] {x : G}, addOrderOf x = 2 → -x = x
-- Mathlib.NumberTheory.LSeries.ZMod
/-- Relation between the completed L-function and the usual one (even case).
We state it this way around so it holds at the poles of the gamma factor as well
(except at `s = 0`, where it is genuinely false if `N > 1` and `Φ 0 ≠ 0`).
 -/
ZMod.LFunction_eq_completed_div_gammaFactor_even : ∀ {N : ℕ} [inst : NeZero N] {Φ : ZMod N → ℂ},
  Function.Even Φ → ∀ (s : ℂ), s ≠ 0 ∨ Φ 0 = 0 → ZMod.LFunction Φ s = ZMod.completedLFunction Φ s / s.Gammaℝ
-- Lean.Data.Position
Lean.Position : Type
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- The right fraction in the opposite category corresponding to a left fraction.  -/
CategoryTheory.MorphismProperty.LeftFraction.op : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {X Y : C} → W.LeftFraction X Y → W.op.RightFraction (Opposite.op Y) (Opposite.op X)
-- Lean.Meta.LitValues
/-- Return `some s` if `e` is of the form `.lit (.strVal s)`.  -/
Lean.Meta.getStringValue? : Lean.Expr → Option String
-- Lean.Elab.DeclModifiers
Lean.Elab.instToFormatModifiers : Std.ToFormat Lean.Elab.Modifiers
-- Mathlib.Algebra.Algebra.Subalgebra.Pi
Subalgebra.pi_toSubmodule : ∀ {ι : Type u_1} {R : Type u_2} {S : ι → Type u_3} [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (S i)]
  [inst_2 : (i : ι) → Algebra R (S i)] {s : Set ι} {t : (i : ι) → Subalgebra R (S i)},
  Subalgebra.toSubmodule (Subalgebra.pi s t) = Submodule.pi s fun i => Subalgebra.toSubmodule (t i)
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Adjunction.adjToComonadIso_inv_toNatTrans_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) (X : C),
  (CategoryTheory.Adjunction.adjToComonadIso G).inv.app X = CategoryTheory.CategoryStruct.id (G.obj X)
-- Mathlib.GroupTheory.Complement
/-- `H` and `K` are complements if `(+) : H × K → G` is a bijection  -/
AddSubgroup.IsComplement' : {G : Type u_1} → [inst : AddGroup G] → AddSubgroup G → AddSubgroup G → Prop
-- Mathlib.Data.List.Cycle
Cycle.instDecidableEq : {α : Type u_1} → [DecidableEq α] → DecidableEq (Cycle α)
-- Aesop.RuleSet.Member
Aesop.GlobalRuleSetMember.base.injEq : ∀ (m m_1 : Aesop.BaseRuleSetMember), (Aesop.GlobalRuleSetMember.base m = Aesop.GlobalRuleSetMember.base m_1) = (m = m_1)
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.homologyFunctorSingleIso_inv_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  [inst_4 : CategoryTheory.CategoryWithHomology C] (X : C),
  (HomologicalComplex.homologyFunctorSingleIso C c j).inv.app X =
    (HomologicalComplex.singleObjHomologySelfIso c j X).inv
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.id_base : ∀ (X : AlgebraicGeometry.Scheme),
  (CategoryTheory.CategoryStruct.id X).base = CategoryTheory.CategoryStruct.id ↑X.toPresheafedSpace
-- Init.Data.BitVec.Lemmas
BitVec.cpopNatRec_le_of_acc_le : ∀ {w : ℕ} {x : BitVec w} {pos acc acc' : ℕ}, acc ≤ acc' → x.cpopNatRec pos acc ≤ x.cpopNatRec pos acc'
-- Mathlib.Logic.Basic
ite_prop_iff_and : ∀ {P Q R : Prop} [inst : Decidable P], (if P then Q else R) ↔ (P → Q) ∧ (¬P → R)
-- Mathlib.Order.Hom.Basic
OrderIso.ofRelIsoLT_symm : ∀ {α : Type u_6} {β : Type u_7} [inst : PartialOrder α] [inst_1 : PartialOrder β]
  (e : (fun x1 x2 => x1 < x2) ≃r fun x1 x2 => x1 < x2), (OrderIso.ofRelIsoLT e).symm = OrderIso.ofRelIsoLT e.symm
-- Mathlib.Data.Nat.MaxPowDiv
Nat.divMaxPow.eq_1 : ∀ (n p : ℕ), n.divMaxPow p = (p.maxPowDvdDiv n).2
-- Mathlib.Topology.Order.MonotoneContinuity
/-- If a function `f` is strictly monotone on a neighborhood of `a` and the image of this
neighborhood under `f` meets every interval `[b, f a)`, `b < f a`, and every interval
`(f a, b]`, `b > f a`, then `f` is continuous at `a`.  -/
StrictMonoOn.continuousAt_of_exists_between : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] {f : α → β} {s : Set α} {a : α},
  StrictMonoOn f s →
    s ∈ nhds a →
      (∀ b < f a, ∃ c ∈ s, f c ∈ Set.Ico b (f a)) → (∀ b > f a, ∃ c ∈ s, f c ∈ Set.Ioc (f a) b) → ContinuousAt f a
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
FixedDetMatrices.reduceStep.eq_1 : ∀ {m : ℤ} (A : FixedDetMatrix (Fin 2) ℤ m),
  FixedDetMatrices.reduceStep A = ModularGroup.S • ModularGroup.T ^ (-(↑A 0 0 / ↑A 1 0)) • A
-- Mathlib.Order.SupIndep
Finset.SupIndep.mono : ∀ {α : Type u_1} {ι : Type u_3} [inst : Lattice α] [inst_1 : OrderBot α] {s : Finset ι} {f g : ι → α},
  s.SupIndep f → (∀ i ∈ s, g i ≤ f i) → s.SupIndep g
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.constantCoeff_divXPowOrder_eq_zero_iff : ∀ {R : Type u_1} [inst : Semiring R] {f : PowerSeries R}, PowerSeries.constantCoeff f.divXPowOrder = 0 ↔ f = 0
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.extendScalars_le_iff : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {F E : IntermediateField K L}
  (h : F ≤ E) (E' : IntermediateField (↥F) L),
  IntermediateField.extendScalars h ≤ E' ↔ E ≤ IntermediateField.restrictScalars K E'
-- Mathlib.Order.Partition.Finpartition
/-- A `Finpartition` constructor of `parts.sup id` from a finset `parts` of pairwise disjoint
elements. Any `⊥` elements in `parts` are erased.  -/
Finpartition.ofPairwiseDisjoint : {α : Type u_1} →
  [inst : DistribLattice α] →
    [inst_1 : OrderBot α] →
      [DecidableEq α] → (parts : Finset α) → (↑parts).PairwiseDisjoint id → Finpartition (parts.sup id)
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
/-- The product of the sections of a presheaf over the pairwise intersections of
a family of open sets.
 -/
TopCat.Presheaf.SheafConditionEqualizerProducts.piInters : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasProducts C] →
      {X : TopCat} → TopCat.Presheaf C X → {ι : Type v'} → (ι → TopologicalSpace.Opens ↑X) → C
-- Mathlib.Topology.Homotopy.Basic
/-- If two maps are homotopic relative to a set, then they agree on it.  -/
ContinuousMap.HomotopicRel.fst_eq_snd : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {S : Set X} ⦃f₀ f₁ : C(X, Y)⦄,
  f₀.HomotopicRel f₁ S → ∀ {x : X}, x ∈ S → f₀ x = f₁ x
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_insertList_of_contains_left_of_contains_right_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α}
  {m : Std.Internal.List.containsKey k (Std.Internal.List.insertList l toInsert) = true},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys toInsert →
      ∀ (mem : Std.Internal.List.containsKey k l = true),
        (∃ (mem₂ : Std.Internal.List.containsKey k toInsert = true),
            Std.Internal.List.getKey k (Std.Internal.List.insertList l toInsert) m =
              Std.Internal.List.getKey k toInsert mem₂) ∨
          Std.Internal.List.getKey k (Std.Internal.List.insertList l toInsert) m = Std.Internal.List.getKey k l mem
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- **Alias** of `one_apply_eq_self`. -/
ContinuousLinearMap.one_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {inst : FunLike F α α} {inst_1 : One F} [self : IsOneApplyEqSelf F α]
  (x : α), 1 x = x
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
MulChar.subgroupOrderIsoSubgroupMulChar.congr_simp : ∀ (M : Type u_1) (R : Type u_2) [inst : CommMonoid M] [inst_1 : CommRing R] [inst_2 : Finite M]
  [inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)],
  MulChar.subgroupOrderIsoSubgroupMulChar M R = MulChar.subgroupOrderIsoSubgroupMulChar M R
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.isZero_single_obj_homology : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : C) (i : ι), i ≠ j → CategoryTheory.Limits.IsZero (((HomologicalComplex.single C c j).obj A).homology i)
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.IsOrtho.inl_inr : ∀ {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid P] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} (m₁ : M₁) (m₂ : M₂),
  (Q₁.prod Q₂).IsOrtho (m₁, 0) (0, m₂)
-- Lean.Meta.Tactic.Grind.Cases
Lean.Meta.Grind.CasesEntry : Type
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- Equality holds when `a ≠ 0`. See `inv_mul_cancel`.  -/
inv_mul_le_one : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : Preorder G₀] [ZeroLEOneClass G₀] {a : G₀}, a⁻¹ * a ≤ 1
-- Mathlib.NumberTheory.LSeries.Convergence
LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable' : ∀ {f : ℕ → ℂ} {x : EReal}, (∀ (y : ℝ), x < ↑y → LSeriesSummable f ↑y) → LSeries.abscissaOfAbsConv f ≤ x
-- Mathlib.Analysis.Analytic.Binomial
/-- The radius of convergence of `binomialSeries 𝔸 a` is `⊤` for natural `a`.  -/
binomialSeries_radius_eq_top_of_nat : ∀ {𝕂 : Type v} [inst : RCLike 𝕂] {𝔸 : Type u} [inst_1 : NormedDivisionRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸] {a : ℕ},
  (binomialSeries 𝔸 ↑a).radius = ⊤
-- Mathlib.RingTheory.FiniteType
RingHom.FiniteType.id : ∀ (A : Type u_1) [inst : CommRing A], (RingHom.id A).FiniteType
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.contract_ground_subset_ground : ∀ {α : Type u_1} (M : Matroid α) (C : Set α), (M.contract C).E ⊆ M.E
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
/-- The identity arrows of the walking span.  -/
CategoryTheory.Limits.WalkingSpan.Hom.id : (X : CategoryTheory.Limits.WalkingSpan) → X ⟶ X
-- Mathlib.CategoryTheory.Linear.Basic
CategoryTheory.Linear.inducedCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {R : Type w} →
        [inst_2 : Semiring R] →
          [CategoryTheory.Linear R C] →
            {D : Type u'} → (F : D → C) → CategoryTheory.Linear R (CategoryTheory.InducedCategory C F)
-- Lean.Elab.MutualInductive
/-- View of a constructor. Only `ref`, `modifiers`, `declName`, and `declId` are required by the mutual inductive elaborator itself.  -/
Lean.Elab.Command.CtorView : Type
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.le_comap_mk' : ∀ {G : Type u} [inst : AddGroup G] (N : AddSubgroup G) [inst_1 : N.Normal] (H : AddSubgroup (G ⧸ N)),
  N ≤ AddSubgroup.comap (QuotientAddGroup.mk' N) H
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
/-- The CoGrothendieck construction is functorial: a strong natural transformation `α : F ⟶ G`
induces a functor `CoGrothendieck.map : ∫ᶜ F ⥤ ∫ᶜ G`.  -/
CategoryTheory.Pseudofunctor.CoGrothendieck.map : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {F G : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} →
      (F ⟶ G) → CategoryTheory.Functor F.CoGrothendieck G.CoGrothendieck
-- Mathlib.Algebra.Ring.Opposite
AddOpposite.instCommRing : {R : Type u_1} → [CommRing R] → CommRing Rᵃᵒᵖ
-- Mathlib.Topology.MetricSpace.Lipschitz
LipschitzWith.const_max : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {f : α → ℝ} {Kf : NNReal},
  LipschitzWith Kf f → ∀ (a : ℝ), LipschitzWith Kf fun x => max a (f x)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- Given two morphisms `f : X ⟶ Z` and `g : Y ⟶ Z`, given pullback in `C` over each component,
construct the pullback in `FormalCategory.{w} C`.  -/
CategoryTheory.Limits.FormalCoproduct.pullbackCone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : CategoryTheory.Limits.FormalCoproduct C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) →
          ((i : Function.Pullback f.f g.f) →
              CategoryTheory.Limits.PullbackCone
                (CategoryTheory.CategoryStruct.comp (f.φ (↑i).1) (CategoryTheory.eqToHom ⋯)) (g.φ (↑i).2)) →
            CategoryTheory.Limits.PullbackCone f g
-- Lean.Meta.Tactic.Grind.EMatchTheoremParam
_private.Lean.Meta.Tactic.Grind.EMatchTheoremParam.0.Lean.Meta.Grind.getLocalTheoremAnchors.go : Std.HashSet Lean.Meta.Grind.Origin →
  Array Lean.Meta.Grind.ExprWithAnchor →
    Lean.PArray Lean.Meta.Grind.EMatchTheorem →
      Lean.Meta.Grind.GrindM (Std.HashSet Lean.Meta.Grind.Origin × Array Lean.Meta.Grind.ExprWithAnchor)
-- Mathlib.Data.List.Defs
_private.Mathlib.Data.List.Defs.0.List.permutationsAux.rec.match_1.splitter : {α : Type u_1} →
  (motive : List α → List α → Sort u_2) →
    (x x_1 : List α) →
      ((is : List α) → motive [] is) → ((t : α) → (ts is : List α) → motive (t :: ts) is) → motive x x_1
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_insert_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited β],
  (↑m).WF → ∀ {k : α} {v : β}, Std.DHashMap.Internal.Raw₀.Const.get! (m.insert k v) k = v
-- Mathlib.RingTheory.Valuation.Basic
/-- The valuation of a sum is less than or equal to the maximum of the valuations.  -/
Valuation.map_add_le_max' : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : LinearOrderedCommMonoidWithZero Γ₀] [inst_1 : Ring R] (self : Valuation R Γ₀)
  (x y : R),
  (↑self.toMonoidWithZeroHom).toFun (x + y) ≤
    max ((↑self.toMonoidWithZeroHom).toFun x) ((↑self.toMonoidWithZeroHom).toFun y)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_cons_of_true : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k},
  (k == a) = true → Std.Internal.List.getEntry? a (⟨k, v⟩ :: l) = some ⟨k, v⟩
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
/-- The canonical presentation of `universalFactorizationMap`.  -/
MvPolynomial.universalFactorizationMapPresentation : (R : Type u_1) →
  [inst : CommRing R] →
    (n m k : ℕ) →
      (hn : n = m + k) →
        Algebra.PreSubmersivePresentation (MvPolynomial (Fin n) R)
          (TensorProduct R (MvPolynomial (Fin m) R) (MvPolynomial (Fin k) R)) (Fin m ⊕ Fin k) (Fin n)
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.instFiniteIso : ∀ (X Y : FintypeCat), Finite (X ≅ Y)
-- Lean.Elab.Open
_private.Lean.Elab.Open.0.Lean.Elab.OpenDecl.addOpenDecl : {m : Type → Type} → [MonadLiftT (ST IO.RealWorld) m] → Lean.OpenDecl → Lean.Elab.OpenDecl.M Unit
-- Mathlib.Data.Finsupp.Basic
Finsupp.fst_sumFinsuppEquivProdFinsupp : ∀ {α : Type u_12} {β : Type u_13} {γ : Type u_14} [inst : Zero γ] (f : α ⊕ β →₀ γ) (x : α),
  (Finsupp.sumFinsuppEquivProdFinsupp f).1 x = f (Sum.inl x)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_eq_pow : ∀ (x y : ℝ), x.rpow y = x ^ y
-- Mathlib.Order.ScottContinuity.Complete
/-- `f` is Scott continuous if and only if it commutes with `sSup` on directed sets  -/
scottContinuous_iff_map_sSup : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] {f : α → β},
  ScottContinuous f ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → f (sSup d) = sSup (f '' d)