mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.SimpleModule.Isotypic
IsIsotypic.eq_1 : ∀ (R : Type u_2) (M : Type u) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  IsIsotypic R M = ∀ (m : Submodule R M) [IsSimpleModule R ↥m], IsIsotypicOfType R M ↥m
-- Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
CategoryTheory.Functor.IsLocallyFull.functorPushforward_imageSieve_mem : ∀ {C : Type uC} {inst : CategoryTheory.Category.{vC, uC} C} {D : Type uD} {inst_1 : CategoryTheory.Category.{vD, uD} D}
  {G : CategoryTheory.Functor C D} {K : CategoryTheory.GrothendieckTopology D} [self : G.IsLocallyFull K] {U V : C}
  (f : G.obj U ⟶ G.obj V), CategoryTheory.Sieve.functorPushforward G (G.imageSieve f) ∈ K (G.obj U)
-- Mathlib.LinearAlgebra.Dimension.Free
Module.finite_iff_of_rank_eq_nsmul : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  [StrongRankCondition R] {W : Type v} [inst_5 : AddCommMonoid W] [inst_6 : Module R W] [Module.Free R W] {n : ℕ},
  n ≠ 0 → Module.rank R M = n • Module.rank R W → (Module.Finite R M ↔ Module.Finite R W)
-- Lean.Data.Lsp.Basic
Lean.Lsp.PartialResultParams.mk.sizeOf_spec : ∀ (partialResultToken? : Option Lean.Lsp.ProgressToken),
  sizeOf { partialResultToken? := partialResultToken? } = 1 + sizeOf partialResultToken?
-- Lean.Elab.DefView
Lean.Elab.BodyProcessedSnapshot.mk.inj : ∀ {toSnapshot : Lean.Language.Snapshot} {state : Lean.Elab.Term.SavedState} {value : Lean.Expr}
  {moreSnaps : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)} {toSnapshot_1 : Lean.Language.Snapshot}
  {state_1 : Lean.Elab.Term.SavedState} {value_1 : Lean.Expr}
  {moreSnaps_1 : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)},
  { toSnapshot := toSnapshot, state := state, value := value, moreSnaps := moreSnaps } =
      { toSnapshot := toSnapshot_1, state := state_1, value := value_1, moreSnaps := moreSnaps_1 } →
    toSnapshot = toSnapshot_1 ∧ state = state_1 ∧ value = value_1 ∧ moreSnaps = moreSnaps_1
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.State.importAll : Lean.ParseImports.State → Bool
-- Mathlib.LinearAlgebra.Matrix.Invertible
/-- The conjugate transpose of an invertible matrix is invertible.  -/
Matrix.invertibleConjTranspose : {n : Type u_2} →
  {α : Type u_3} →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] →
        [inst_2 : Semiring α] → [inst_3 : StarRing α] → (A : Matrix n n α) → [Invertible A] → Invertible A.conjTranspose
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonPlainTermGoal.toJson : Lean.Lsp.PlainTermGoal → Lean.Json
-- Mathlib.Probability.Moments.CovarianceBilin
ProbabilityTheory.covarianceBilin.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] (μ : MeasureTheory.Measure E),
  ProbabilityTheory.covarianceBilin μ =
    (ProbabilityTheory.covarianceBilinDual μ).bilinearComp (InnerProductSpace.toDualMap ℝ E).toContinuousLinearMap
      (InnerProductSpace.toDualMap ℝ E).toContinuousLinearMap
-- Lean.Meta.Tactic.Simp.Types
/-- A simplification procedure. Recall that we have `pre` and `post` procedures.
See `Step`.
 -/
Lean.Meta.Simp.Simproc : Type
-- Lean.Meta.Tactic.Simp.Types
/-- The simplified version of `e`  -/
Lean.Meta.Simp.Result.expr : Lean.Meta.Simp.Result → Lean.Expr
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.Reduced.eq_1 : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  (φ : (i : ι) → H →* G i) (w : Monoid.CoprodI.Word G),
  Monoid.PushoutI.Reduced φ w = ∀ g ∈ w.toList, g.snd ∉ (φ g.fst).range
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.lipschitz : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂), LipschitzWith 1 ⇑e
-- Mathlib.Topology.ContinuousOn
continuousWithinAt_compl_self : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {x : α},
  ContinuousWithinAt f {x}ᶜ x ↔ ContinuousAt f x
-- Init.Internal.Order.Lemmas
Lean.Order.Array.monotone_anyM : ∀ {γ : Type w} [inst : Lean.Order.PartialOrder γ] {m : Type → Type v} [inst_1 : Monad m]
  [inst_2 : (α : Type) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m] {α : Type u} (f : γ → α → m Bool)
  (xs : Array α) (start stop : ℕ), Lean.Order.monotone f → Lean.Order.monotone fun x => Array.anyM (f x) xs start stop
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.toBitVec_val_assemble₁ : ∀ {w : UInt8} {h : ByteArray.utf8DecodeChar?.parseFirstByte w = ByteArray.utf8DecodeChar?.FirstByte.done} {c : Char},
  ByteArray.utf8DecodeChar?.assemble₁ w h = some c → c.val.toBitVec = BitVec.setWidth 32 w.toBitVec
-- Mathlib.AlgebraicTopology.TopologicalSimplex
SimplexCategory.toTop₀_map : ∀ {X Y : SimplexCategory} (f : X ⟶ Y),
  SimplexCategory.toTop₀.map f =
    TopCat.ofHom { toFun := stdSimplex.map ⇑(CategoryTheory.ConcreteCategory.hom f), continuous_toFun := ⋯ }
-- Mathlib.RingTheory.Localization.NumDen
IsFractionRing.isUnit_den_iff : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : UniqueFactorizationMonoid A] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] (x : K),
  IsUnit ↑(IsFractionRing.den A x) ↔ IsLocalization.IsInteger A x
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.coveringNumber_subset_le : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {A B : Set X} {ε : NNReal},
  A ⊆ B → Metric.coveringNumber ε A ≤ Metric.coveringNumber (ε / 2) B
-- Mathlib.Algebra.Order.Ring.Basic
Odd.pow_nonpos_iff : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : ℕ} [ExistsAddOfLE R],
  Odd n → (a ^ n ≤ 0 ↔ a ≤ 0)
-- Mathlib.FieldTheory.JacobsonNoether
/-- If `D` is a purely inseparable extension of `k` with characteristic `p`,
then for every element `a` of `D \ k`, there exists a natural number `n`
**greater than 0** such that `a ^ (p ^ n)` is contained in `k`.  -/
JacobsonNoether.exists_pow_mem_center_of_inseparable' : ∀ {D : Type u_1} [inst : DivisionRing D] [Algebra.IsAlgebraic (↥(Subring.center D)) D] (p : ℕ) [ExpChar D p] {a : D},
  a ∉ Subring.center D →
    (∀ (x : D), IsSeparable (↥(Subring.center D)) x → x ∈ Subring.center D) → ∃ n, 1 ≤ n ∧ a ^ p ^ n ∈ Subring.center D
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reverse_mul_of_domain : ∀ {R : Type u_2} [inst : Semiring R] [NoZeroDivisors R] (f g : Polynomial R), (f * g).reverse = f.reverse * g.reverse
-- Lean.Language.Basic
/-- Applies the transformation to the given syntax tree.  -/
Lean.Language.SnapshotTreeTransform.transformSyntax : Lean.Language.SnapshotTreeTransform → Lean.Syntax → Lean.Syntax
-- Mathlib.GroupTheory.Nilpotent
Subgroup.upperCentralSeries.card_image_eq_of_le_nilpotencyClass : ∀ {G : Type u_1} [inst : Group G] {a : ℕ},
  a ≤ Group.nilpotencyClass G → (Subgroup.upperCentralSeries G '' Set.Iic a).ncard = a + 1
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- The short complex `Fun(G, A) --d₁₂--> Fun(G × G, A) --d₂₃--> Fun(G × G × G, A)`.  -/
groupCohomology.shortComplexH2 : {k G : Type u} →
  [inst : CommRing k] → [inst_1 : Group G] → Rep.{u_1, u, u} k G → CategoryTheory.ShortComplex (ModuleCat k)
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.InitializedParams : Type
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey!_modify : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α] {k k' : α} {f : β → β},
  m.WF →
    (Std.DHashMap.Raw.Const.modify m k f).getKey! k' =
      if (k == k') = true then if k ∈ m then k else default else m.getKey! k'
-- Mathlib.Algebra.Category.ModuleCat.EpiMono
ModuleCat.mono_as_hom'_subtype : ∀ {R : Type u} [inst : Ring R] {X : ModuleCat R} (U : Submodule R ↑X), CategoryTheory.Mono (ModuleCat.ofHom U.subtype)
-- Mathlib.Data.Fin.Basic
Fin.nontrivial_iff_two_le : ∀ {n : ℕ}, Nontrivial (Fin n) ↔ 2 ≤ n
-- Mathlib.Order.WithBot
Equiv.withTopCongr_trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e₁ : α ≃ β) (e₂ : β ≃ γ),
  (e₁.trans e₂).withTopCongr = e₁.withTopCongr.trans e₂.withTopCongr
-- Mathlib.LinearAlgebra.AffineSpace.Restrict
AffineMap.restrict.congr_simp : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (φ φ_1 : P₁ →ᵃ[k] P₂) (e_φ : φ = φ_1) {E : AffineSubspace k P₁}
  {F : AffineSubspace k P₂} [inst_7 : Nonempty ↥E] [inst_8 : Nonempty ↥F] (hEF : AffineSubspace.map φ E ≤ F),
  φ.restrict hEF = φ_1.restrict ⋯
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.enorm : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f : ℝ → ε} {a b : ℝ}
  {μ : MeasureTheory.Measure ℝ}, IntervalIntegrable f μ a b → IntervalIntegrable (fun x => ‖f x‖ₑ) μ a b
-- Init.Data.Nat.Coprime
Nat.Coprime.mul_dvd_of_dvd_of_dvd : ∀ {m n a : ℕ}, m.Coprime n → m ∣ a → n ∣ a → m * n ∣ a
-- Mathlib.Algebra.Homology.Bifunctor
HomologicalComplex.mapBifunctor.hom_ext : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂}
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)} [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] {c : ComplexShape J} [inst_8 : TotalComplexShape c₁ c₂ c]
  [inst_9 : K₁.HasMapBifunctor K₂ F c] [inst_10 : DecidableEq J] {Y : D} {j : J}
  {f g : (K₁.mapBifunctor K₂ F c).X j ⟶ Y},
  (∀ (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c (i₁, i₂) = j),
      CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h) f =
        CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h) g) →
    f = g
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_neg_mul : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} {x y : F} (h : W.Nonsingular x y),
  (ClassGroup.mk W.FunctionField) (WeierstrassCurve.Affine.CoordinateRing.XYIdeal' ⋯) *
      (ClassGroup.mk W.FunctionField) (WeierstrassCurve.Affine.CoordinateRing.XYIdeal' h) =
    1
-- Mathlib.RingTheory.Polynomial.Basic
/-- The first `n` coefficients on `degreeLT n` form a linear equivalence with `Fin n → R`.  -/
Polynomial.degreeLTEquiv : (R : Type u) → [inst : Semiring R] → (n : ℕ) → ↥(Polynomial.degreeLT R n) ≃ₗ[R] Fin n → R
-- Mathlib.Order.Antichain
/-- A set which is simultaneously a chain and antichain is subsingleton.  -/
subsingleton_of_isChain_of_isAntichain : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, IsChain r s → IsAntichain r s → s.Subsingleton
-- Lean.Elab.Match
Lean.Elab.Term.PatternElabException.ex : Lean.Elab.Term.PatternElabException → Lean.Exception
-- Mathlib.Logic.Equiv.Basic
Equiv.sigmaSigmaSubtype.congr_simp : ∀ {α : Type u_9} {β : α → Type u_10} {γ : (a : α) → β a → Type u_11} (p : (a : α) × β a → Prop)
  [uniq : Unique { ab // p ab }] {a : α} {b : β a} (h : p ⟨a, b⟩),
  Equiv.sigmaSigmaSubtype p h = Equiv.sigmaSigmaSubtype p h
-- Mathlib.Data.Multiset.Powerset
Multiset.powersetCard_eq_empty : ∀ {α : Type u_2} (n : ℕ) {s : Multiset α}, s.card < n → Multiset.powersetCard n s = 0
-- Mathlib.Algebra.Ring.Basic
neg_inv : ∀ {R : Type u_1} [inst : DivisionMonoid R] [inst_1 : HasDistribNeg R] {a : R}, -a⁻¹ = (-a)⁻¹
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.HasEval.mul_right : ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : TopologicalSpace S] [IsLinearTopology S S] (c : S) {x : S},
  PowerSeries.HasEval x → PowerSeries.HasEval (x * c)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
/-- If `x : L` is an integral element in a field extension `L` over `K`, then the degree of the
minimal polynomial of `x` over `K` divides `[L : K]`.  -/
minpoly.degree_dvd : ∀ {K : Type u} [inst : Field K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] {x : L},
  IsIntegral K x → (minpoly K x).natDegree ∣ Module.finrank K L
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
_private.Mathlib.LinearAlgebra.ExteriorPower.Basic.0.exteriorPower.presentation.relations.match_1.eq_2 : ∀ (R : Type u_1) (ι : Type u_2) (M : Type u_3) (motive : exteriorPower.presentation.Rels R ι M → Sort u_4) (m : ι → M)
  (i : ι) (r : R) (x : M)
  (h_1 : (m : ι → M) → (i : ι) → (x y : M) → motive (exteriorPower.presentation.Rels.add m i x y))
  (h_2 : (m : ι → M) → (i : ι) → (r : R) → (x : M) → motive (exteriorPower.presentation.Rels.smul m i r x))
  (h_3 :
    (m : ι → M) →
      (i j : ι) → (hm : m i = m j) → (hij : i ≠ j) → motive (exteriorPower.presentation.Rels.alt m i j hm hij)),
  (match exteriorPower.presentation.Rels.smul m i r x with
    | exteriorPower.presentation.Rels.add m i x y => h_1 m i x y
    | exteriorPower.presentation.Rels.smul m i r x => h_2 m i r x
    | exteriorPower.presentation.Rels.alt m i j hm hij => h_3 m i j hm hij) =
    h_2 m i r x
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.erase_add : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)] (i : ι)
  (f₁ f₂ : Π₀ (i : ι), β i), DFinsupp.erase i (f₁ + f₂) = DFinsupp.erase i f₁ + DFinsupp.erase i f₂
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roc_eq_nil_iff : ∀ {m n : ℤ}, (m<...=n).toArray = #[] ↔ n ≤ m
-- Mathlib.RingTheory.Smooth.NoetherianDescent
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux.vars : {A : Type u} →
  {B : Type u_2} →
    [inst : CommRing A] → [inst_1 : CommRing B] → [inst_2 : Algebra A B] → Algebra.Smooth.DescentAux✝ A B → Type
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.instInhabited : Inhabited CategoryTheory.Cat
-- Mathlib.Tactic.Ring.Common
/-- A sum of monomials.  -/
Mathlib.Tactic.Ring.Common.ExBaseNat.sum : {e : Q(ℕ)} → Mathlib.Tactic.Ring.Common.ExSumNat e → Mathlib.Tactic.Ring.Common.ExBaseNat e
-- Mathlib.RepresentationTheory.Basic
Representation.asModuleEquiv_symm_map_rho : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring k] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ : Representation k G V) (g : G) (x : V),
  ρ.asModuleEquiv.symm ((ρ g) x) = (MonoidAlgebra.of k G) g • ρ.asModuleEquiv.symm x
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.Pass.mk.injEq : ∀ (toConfig : Mathlib.TacticAnalysis.Config) (opt : Option (Lean.Option Bool))
  (toConfig_1 : Mathlib.TacticAnalysis.Config) (opt_1 : Option (Lean.Option Bool)),
  ({ toConfig := toConfig, opt := opt } = { toConfig := toConfig_1, opt := opt_1 }) =
    (toConfig = toConfig_1 ∧ opt = opt_1)
-- Batteries.Tactic.Lint.Basic
/-- Returns true if `decl` is a private or automatically generated declaration.

Also returns true if `decl` is an internal name or created during macro expansion.

See `Lean.Environment.isPrivateOrAutoDecl` for an identical pure version of this function on the
environment.
 -/
Batteries.Tactic.Lint.isPrivateOrAutoDecl : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m Bool
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolInformation.location : Lean.Lsp.SymbolInformation → Lean.Lsp.Location
-- Mathlib.RingTheory.WittVector.MulCoeff
WittVector.polyOfInterest_vars : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ), (WittVector.polyOfInterest p n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Replicate
Std.Tactic.BVDecide.BVExpr.bitblast.ReplicateTarget.inner : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {combined : ℕ} → (self : Std.Tactic.BVDecide.BVExpr.bitblast.ReplicateTarget aig combined) → aig.RefVec self.w
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
CategoryTheory.Limits.comp_lim_obj_ext_iff : ∀ {J : Type u₁} {K : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} J] [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  [inst_2 : Small.{v, u₂} K] {j : J} {G : CategoryTheory.Functor J (CategoryTheory.Functor K (Type v))}
  {x y : (G.comp CategoryTheory.Limits.lim).obj j},
  x = y ↔
    ∀ (k : K),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π (G.obj j) k)) x =
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π (G.obj j) k)) y
-- Mathlib.NumberTheory.Height.NumberField
/-- This is the familiar definition of the multiplicative height on (nonzero) tuples
of number field elements.  -/
NumberField.mulHeight_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {ι : Type u_2} {x : ι → K},
  x ≠ 0 → Height.mulHeight x = (∏ v, (⨆ i, v (x i)) ^ v.mult) * ∏ᶠ (v : NumberField.FinitePlace K), ⨆ i, v (x i)
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.continuous_toLp : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [inst : (i : ι) → TopologicalSpace (β i)], Continuous (WithLp.toLp p)
-- Lean.Expr
Lean.Expr.letType! : Lean.Expr → Lean.Expr
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- **Alias** of the reverse direction of `hasMFDerivWithinAt_insert`. -/
HasMFDerivWithinAt.insert' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M}
  {f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)} {y : M}, HasMFDerivAt[s] f x f' → HasMFDerivAt[insert y s] f x f'
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs
/-- The roots of the characteristic polynomial are in the spectrum of the matrix.  -/
Matrix.mem_spectrum_of_isRoot_charpoly : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_2} [inst_2 : CommRing R] {B : Matrix n n R}
  [Nontrivial R] {r : R}, B.charpoly.IsRoot r → r ∈ spectrum R B
-- Mathlib.Data.NNReal.Defs
NNReal.exists_mem_Ico_zpow : ∀ {x y : NNReal}, x ≠ 0 → 1 < y → ∃ n, x ∈ Set.Ico (y ^ n) (y ^ (n + 1))
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.leftUnitor_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C}
  {s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)} (P : CategoryTheory.Limits.IsLimit s)
  {t : CategoryTheory.Limits.BinaryFan s.pt X} (Q : CategoryTheory.Limits.IsLimit t),
  (CategoryTheory.Limits.BinaryFan.leftUnitor P Q).hom = t.snd
-- Mathlib.Analysis.Convex.Side
/-- **Alias** of `AffineSubspace.setOfPred_wSameSide_eq_image2`. -/
AffineSubspace.setOf_wSameSide_eq_image2 : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x p : P},
  x ∉ s → p ∈ s → {y | s.WSameSide x y} = Set.image2 (fun t q => t • (x -ᵥ p) +ᵥ q) (Set.Ici 0) ↑s
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.comapEq_symm : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {β γ : Type w} {f g : β → γ} (h : f = g),
  CategoryTheory.GradedObject.comapEq C ⋯ = (CategoryTheory.GradedObject.comapEq C h).symm
-- Mathlib.RingTheory.Ideal.Over
/-- If an ideal `P` of `B` is prime and lying over `p`, then it is in `primesOver p B`.  -/
Ideal.primesOver.mk : {A : Type u_2} →
  [inst : CommSemiring A] →
    (p : Ideal A) →
      {B : Type u_3} →
        [inst_1 : Semiring B] →
          [inst_2 : Algebra A B] → (P : Ideal B) → [hPp : P.IsPrime] → [hp : P.LiesOver p] → ↑(p.primesOver B)
-- Lean.Elab.DeclModifiers
Lean.Elab.RecKind.partial.sizeOf_spec : sizeOf Lean.Elab.RecKind.partial = 1
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
CategoryTheory.Limits.IsWeakLimit.mk : {J : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} J] →
    {C : Type u_3} →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cone F} →
            (lift : (s : CategoryTheory.Limits.Cone F) → s.pt ⟶ t.pt) →
              autoParam
                  (∀ (s : CategoryTheory.Limits.Cone F) (j : J),
                    CategoryTheory.CategoryStruct.comp (lift s) (t.π.app j) = s.π.app j)
                  CategoryTheory.Limits.IsWeakLimit.fac._autoParam →
                CategoryTheory.Limits.IsWeakLimit t
-- Mathlib.LinearAlgebra.Matrix.Echelon.Basic
/-- If the row indices have a linear order, then every entry in a pivot column vanishes
except for the pivot.  -/
Matrix.IsReducedRowEchelon.eq_zero_of_ne_of_isLeadingEntry : ∀ {m : Type u_1} {n : Type u_2} {R : Type v} {A : Matrix m n R} [inst : Zero R] [inst_1 : LinearOrder m] [inst_2 : LT n]
  [inst_3 : One R] {i₁ i₂ : m} {c : n}, A.IsReducedRowEchelon → i₁ ≠ i₂ → A.IsLeadingEntry i₂ c → A i₁ c = 0
-- Mathlib.ModelTheory.ElementaryMaps
/-- The elementary diagram of an `L`-structure is the set of all sentences with parameters it
satisfies.  -/
FirstOrder.Language.elementaryDiagram : (L : FirstOrder.Language) → (M : Type u_1) → [L.Structure M] → (L.withConstants M).Theory
-- Mathlib.Analysis.SpecialFunctions.Integrability.Basic
/-- The real logarithm is interval integrable (with respect to every locally finite measure) over every
interval that does not contain zero. See `intervalIntegrable_log'` for a version without any
hypothesis on the interval, but assuming the measure is the volume.
 -/
intervalIntegral.intervalIntegrable_log : ∀ {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ],
  0 ∉ Set.uIcc a b → IntervalIntegrable Real.log μ a b
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct
SSet.prodStdSimplex.anodyneExtensions_unionProd_ι : ∀ {m : ℕ} (k : Fin (m + 2)) (n : ℕ), SSet.anodyneExtensions ((SSet.horn (m + 1) k).unionProd (SSet.boundary n)).ι
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
/-- Reindexing a simplex produces one with the same set of points.  -/
Affine.Simplex.reindex_range_points : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {m n : ℕ} (s : Affine.Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1)),
  Set.range (s.reindex e).points = Set.range s.points
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSet.compl : ∀ {α : Type u_1} {s : Set α} {m : MeasurableSpace α}, MeasurableSet s → MeasurableSet sᶜ
-- Init.Data.Array.Mem
Array.sizeOf_getElem : ∀ {α : Type u_1} [inst : SizeOf α] (as : Array α) (i : ℕ) (h : i < as.size), sizeOf as[i] < sizeOf as
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.map_univ_equiv : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (f : β ≃ α),
  Finset.map f.toEmbedding Finset.univ = Finset.univ
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
SchwartzMap.fderivCLM_apply : ∀ (𝕜 : Type u_2) {E : Type u_5} {F : Type u_8} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace ℝ F] [inst_3 : NormedSpace ℝ E] [inst_4 : RCLike 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] (f : SchwartzMap E F) (x : E), ((SchwartzMap.fderivCLM 𝕜 E F) f) x = fderiv ℝ (⇑f) x
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.BitVec.add_left_inj' : ∀ {w : ℕ} (a b c : BitVec w), (a + c == c + b) = (a == b)