mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.toRingHom : {ι : 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] → {𝒜 : ι → σ} → {ℬ : ι → τ} → (𝒜 →+*ᵍ ℬ) → A →+* B
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.outerMeasure_caratheodory : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] (A : Set G),
  MeasurableSet A ↔
    ∀ (U : TopologicalSpace.Opens G), μ.outerMeasure (↑U ∩ A) + μ.outerMeasure (↑U \ A) ≤ μ.outerMeasure ↑U
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.dirichletUnitTheorem.logEmbedding_component : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : (NumberField.RingOfIntegers K)ˣ)
  (w : { w // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }),
  (NumberField.Units.logEmbedding K) (Additive.ofMul x) w =
    ↑(↑w).mult * Real.log (↑w ((algebraMap (NumberField.RingOfIntegers K) K) ↑x))
-- Mathlib.Topology.Separation.Hausdorff
T2Quotient.continuous_mk : ∀ (X : Type u_1) [inst : TopologicalSpace X], Continuous T2Quotient.mk
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.inf_map_atTop_neBot_iff : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [IsDirectedOrder α] {F : Filter β} {u : α → β} [Nonempty α],
  (F ⊓ Filter.map u Filter.atTop).NeBot ↔ ∀ U ∈ F, ∀ (N : α), ∃ n, N ≤ n ∧ u n ∈ U
-- Mathlib.Data.Fintype.Order
Finite.map_iSup_of_antitoneOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder α]
  [inst_1 : ConditionallyCompleteLattice β] [Finite ι] [Nonempty ι] {s : Set α} {f : ι → α} {g : α → β},
  AntitoneOn g s → (∀ (i : ι), f i ∈ s) → g (⨆ i, f i) = ⨅ i, g (f i)
-- Mathlib.SetTheory.Ordinal.Univ
Ordinal.type_lt_ordinal : (Ordinal.type fun x1 x2 => x1 < x2) = Ordinal.univ.{u, u + 1}
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.equivComma_inverse_obj_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (c : CategoryTheory.Comma (CategoryTheory.Functor.const C) (CategoryTheory.Functor.id (CategoryTheory.Functor C D)))
  {X Y : CategoryTheory.WithInitial C} (f : X ⟶ Y),
  (CategoryTheory.WithInitial.equivComma.inverse.obj c).map f =
    match X, Y, f with
    | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_1, f =>
      c.right.map (CategoryTheory.WithInitial.down f)
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a, x => c.hom.app a
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => CategoryTheory.CategoryStruct.id c.left
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.smul_div_smul_comm : ∀ {α : Type u_2} [inst : CommGroup α] (a : α) (s : Set α) (b : α) (t : Set α), a • s / b • t = (a / b) • (s / t)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_map_of_getKey?_eq_some : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [Inhabited γ] {f : α → β → γ} {k k' : α} {fallback : γ},
  m.getKey? k = some k' →
    Std.DHashMap.Const.getD (Std.DHashMap.map f m) k fallback =
      (Option.map (f k') (Std.DHashMap.Const.get? m k)).getD fallback
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans_obj_str : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (α : F ⟶ G)
  (V : CategoryTheory.Endofunctor.Coalgebra F),
  ((CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans α).obj V).str =
    CategoryTheory.CategoryStruct.comp V.str (α.app V.V)
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.instInhabited : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring S] →
      [inst_1 : PartialOrder S] → [inst_2 : Semiring R] → (v : AbsoluteValue R S) → Inhabited (WithAbs v)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.ElementarilyEquivalent.symm : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N],
  L.ElementarilyEquivalent M N → L.ElementarilyEquivalent N M
-- Init.Data.Nat.ToString
_private.Init.Data.Nat.ToString.0.Nat.toDigitsCore_append : ∀ {b fuel n : ℕ} {cs₁ cs₂ : List Char}, b.toDigitsCore fuel n cs₁ ++ cs₂ = b.toDigitsCore fuel n (cs₁ ++ cs₂)
-- Mathlib.Algebra.DirectSum.Module
DirectSum.single_eq_lof : ∀ (R : Type u) [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] (i : ι) (b : M i),
  (fun₀ | i => b) = (DirectSum.lof R ι M i) b
-- Mathlib.Data.Finset.Max
Finset.max_singleton : ∀ {α : Type u_2} [inst : LinearOrder α] {a : α}, {a}.max = ↑a
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_alter_eq_isEmpty_erase : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k : α} {f : Option β → Option β},
  m.WF → (m.alter k f).isEmpty = ((m.erase k).isEmpty && (f m[k]?).isNone)
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.comp_commShiftIso_hom_app : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) {A : Type u_4} [inst_3 : AddMonoid A]
  [inst_4 : CategoryTheory.HasShift C A] [inst_5 : CategoryTheory.HasShift D A] [inst_6 : CategoryTheory.HasShift E A]
  [inst_7 : F.CommShift A] [inst_8 : G.CommShift A] (a : A) (X : C),
  (CategoryTheory.Functor.commShiftIso (F.comp G) a).hom.app X =
    CategoryTheory.CategoryStruct.comp (G.map ((CategoryTheory.Functor.commShiftIso F a).hom.app X))
      ((CategoryTheory.Functor.commShiftIso G a).hom.app (F.obj X))
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K K_1 : ChainComplex C ℕ),
  K = K_1 →
    ∀ (Δ Δ_1 : SimplexCategoryᵒᵖ),
      Δ = Δ_1 →
        ∀ [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C],
          AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ K Δ = AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ K_1 Δ_1
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.coe_inv : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Inv β]
  [inst_3 : ContinuousInv β] (f : C(α, β)), ⇑f⁻¹ = (⇑f)⁻¹
-- Init.Meta.Defs
Lean.Meta.instReprEtaStructMode : Repr Lean.Meta.EtaStructMode
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instReprEMatchTheoremKind.repr : Lean.Meta.Grind.EMatchTheoremKind → ℕ → Std.Format
-- Lean.Elab.InfoTree.Types
Lean.Elab.CustomInfo.stx : Lean.Elab.CustomInfo → Lean.Syntax
-- Mathlib.LinearAlgebra.Basis.Exact
/-- **Alias** of `Submodule.projectionOnto_comp_bijective_of_exact`. -/
Submodule.linearProjOfIsCompl_comp_bijective_of_exact : ∀ {R : Type u_1} {M : Type u_2} {K : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup K] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R K] [inst_6 : Module R P]
  {f : K →ₗ[R] M} {g : M →ₗ[R] P},
  Function.Exact ⇑f ⇑g →
    Function.Injective ⇑f →
      ∀ {p q : Submodule R M} (hpq : IsCompl p q),
        Disjoint g.ker q → Submodule.map g q = ⊤ → Function.Bijective ⇑(p.projectionOnto q hpq ∘ₗ f)
-- Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
Algebra.TensorProduct.distribBaseChange_includeLeftSubRight_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : Ring S] [inst_2 : Algebra R S] (T : Type u_3)
  [inst_3 : CommRing T] [inst_4 : Algebra R T] (x : TensorProduct R T S),
  (TensorProduct.AlgebraTensorModule.distribBaseChange R T S S)
      ((LinearMap.lTensor T (Algebra.TensorProduct.includeLeftSubRight R S)) x) =
    (Algebra.TensorProduct.includeLeftSubRight T (TensorProduct R T S)) x
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.eq_succMany?_of_toList_eq_append_cons : ∀ {α : Type u} {r : Std.Rci α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxi.IsAlwaysFinite α] {pref suff : List α} {cur : α} (h : r.toList = pref ++ cur :: suff),
  cur = (Std.PRange.succMany? pref.length r.lower).get ⋯
-- Lean.Meta.Tactic.Grind.Types
/-- Records that `parent` is a parent of `child`. This function actually stores the
information in the root (aka canonical representative) of `child`.
 -/
Lean.Meta.Grind.registerParent : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Topology.Closure
subset_closure_inter_union_closure_compl_left : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, closure t ⊆ closure (s ∩ t) ∪ closure sᶜ
-- Mathlib.Data.Sym.Sym2
Sym2.fromRel_mono_iff : ∀ {α : Type u_1} {r₁ r₂ : α → α → Prop} (sym₁ : Std.Symm r₁) (sym₂ : Std.Symm r₂),
  Sym2.fromRel sym₁ ⊆ Sym2.fromRel sym₂ ↔ r₁ ≤ r₂
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.density_mono_set : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ},
  κ.fst ≤ ν → ∀ (a : α) (x : γ) {s s' : Set β}, s ⊆ s' → κ.density ν a x s ≤ κ.density ν a x s'
-- Mathlib.NumberTheory.Transcendental.Liouville.Basic
/-- A Liouville number is a real number `x` such that for every natural number `n`, there exist
`a, b ∈ ℤ` with `1 < b` such that `0 < |x - a/b| < 1/bⁿ`.
In the implementation, the condition `x ≠ a/b` replaces the traditional equivalent `0 < |x - a/b|`.
 -/
Liouville : ℝ → Prop
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MCasesPat.alts.inj : ∀ {args args_1 : List Lean.Parser.Tactic.MCasesPat},
  Lean.Parser.Tactic.MCasesPat.alts args = Lean.Parser.Tactic.MCasesPat.alts args_1 → args = args_1
-- Mathlib.SetTheory.Ordinal.Family
/-- Converts a family indexed by a `Type u` to one indexed by an `Ordinal.{u}` using a specified
well-ordering.  -/
Ordinal.bfamilyOfFamily' : {α : Type u_1} →
  {ι : Type u} → (r : ι → ι → Prop) → [inst : IsWellOrder ι r] → (ι → α) → (a : Ordinal.{u}) → a < Ordinal.type r → α
-- Mathlib.Analysis.Normed.Module.Bases
/-- The projections `b.proj A x` converge to `x` along the summation filter.  -/
GeneralSchauderBasis.tendsto_proj : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] {β : Type u_3} {L : SummationFilter β} (b : GeneralSchauderBasis β 𝕜 X L) (x : X),
  Filter.Tendsto (fun A => (b.proj A) x) L.filter (nhds x)
-- Lean.Parser.Syntax
Lean.Parser.Syntax.binary : Lean.Parser.Parser
-- Lean.Meta.PProdN
/-- Given types `tᵢ`, produces `t₁ ×' t₂ ×' t₃`  -/
Lean.Meta.PProdN.pack : Lean.Level → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
/-- The clifford algebra over a 1-dimensional vector space with 0 quadratic form is isomorphic to
the dual numbers.  -/
CliffordAlgebraDualNumber.equiv : {R : Type u_1} → [inst : CommRing R] → CliffordAlgebra 0 ≃ₐ[R] DualNumber R
-- Mathlib.Algebra.Algebra.Shrink
Shrink.instAlgebra : {R : Type u_1} →
  {α : Type u_2} →
    [inst : Small.{v, u_2} α] →
      [inst_1 : CommSemiring R] → [inst_2 : Semiring α] → [Algebra R α] → Algebra R (Shrink.{v, u_2} α)
-- Std.Internal.Do.WP.Lemmas
_private.Std.Internal.Do.WP.Lemmas.0.EStateM.adaptExcept.match_1.eq_1 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (e : ε) (s : σ)
  (h_1 : (e : ε) → (s : σ) → motive (EStateM.Result.error e s))
  (h_2 : (a : α) → (s : σ) → motive (EStateM.Result.ok a s)),
  (match EStateM.Result.error e s with
    | EStateM.Result.error e s => h_1 e s
    | EStateM.Result.ok a s => h_2 a s) =
    h_1 e s
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.substInvFun.eq_2 : ∀ {R : Type u_2} [inst : CommRing R] (P : PowerSeries R) [inst_1 : Invertible ((PowerSeries.coeff 1) P)],
  P.substInvFun 1 = ⅟((PowerSeries.coeff 1) P)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get!_inter_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited α] {k : α}, k ∉ m₁ → (m₁ ∩ m₂).get! k = default
-- Init.Data.Range.Polymorphic.Basic
Std.Rxi.LawfulHasSize.mk : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.Rxi.HasSize α],
  (∀ (lo : α), Std.PRange.succ? lo = none → Std.Rxi.HasSize.size lo = 1) →
    (∀ (lo lo' : α), Std.PRange.succ? lo = some lo' → Std.Rxi.HasSize.size lo = Std.Rxi.HasSize.size lo' + 1) →
      Std.Rxi.LawfulHasSize α
-- Lean.Meta.LazyDiscrTree
/-- Extract entries at the given keys and also drop them from the tree.  -/
Lean.Meta.LazyDiscrTree.extractKeys : {α : Type} →
  Lean.Meta.LazyDiscrTree α → List (List Lean.Meta.LazyDiscrTree.Key) → Lean.MetaM (Array α × Lean.Meta.LazyDiscrTree α)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_norm_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {f' : α → E'} {l : Filter α}, (fun x => ‖f' x‖) =O[l] g ↔ f' =O[l] g
-- Init.Prelude
/-- Unpacks a `UInt64` into a `BitVec 64`. This function is overridden with a native implementation.
 -/
UInt64.toBitVec : UInt64 → BitVec 64
-- Mathlib.Computability.DFA
DFA.reindex_apply_step : ∀ {α : Type u} {σ : Type v} {σ' : Type u_2} (g : σ ≃ σ') (M : DFA α σ) (s : σ') (a : α),
  ((DFA.reindex g) M).step s a = g (M.step (g.symm s) a)
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
/-- A normal epi category is a category in which every epimorphism is normal.  -/
CategoryTheory.IsNormalEpiCategory.normalEpiOfEpi : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  [self : CategoryTheory.IsNormalEpiCategory C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f],
  Nonempty (CategoryTheory.NormalEpi f)
-- Mathlib.Analysis.Polynomial.Norm
Polynomial.supNorm_monomial : ∀ {A : Type u_1} [inst : SeminormedRing A] (n : ℕ) {a : A}, ((Polynomial.monomial n) a).supNorm = ‖a‖
-- Mathlib.Topology.Baire.LocallyCompactRegular
/-- **Alias** of `IsGδ.baireSpace_of_t2Space_locallyCompactSpace`.

---

A Gδ subset of a locally compact R₁ space is Baire.  -/
IsGδ.of_t2Space_locallyCompactSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} [R1Space X] [LocallyCompactSpace X], IsGδ s → BaireSpace ↑s
-- Mathlib.Algebra.Group.Subgroup.Ker
AddEquiv.map_range_nsmulAddMonoidHom : ∀ {M : Type u_5} {N : Type u_6} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] (e : M ≃+ N) (n : ℕ),
  AddSubgroup.map (↑e) (nsmulAddMonoidHom n).range = (nsmulAddMonoidHom n).range
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.instIsProbabilityMeasureProdVolume : ∀ {α : Type u_4} {β : Type u_5} [inst : MeasureTheory.MeasureSpace α] [inst_1 : MeasureTheory.MeasureSpace β]
  [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume],
  MeasureTheory.IsProbabilityMeasure MeasureTheory.volume
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.get?_eq_get?ₘ : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (l : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.get? l k = Std.DTreeMap.Internal.Impl.Const.get?ₘ l k
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get!_eq_default : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : Inhabited α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, a ∉ m → m.get! a = default
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Presentation.ofLinearEquiv_toRelations : ∀ {A : Type u} [inst : Ring A] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module A M]
  (pres : Module.Presentation A M) {N : Type v'} [inst_3 : AddCommGroup N] [inst_4 : Module A N] (e : M ≃ₗ[A] N),
  (pres.ofLinearEquiv e).toRelations = pres.toRelations
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.instHasQuotientWeakEquivalencesHomRel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.CofibrantObject C)).HasQuotient
    (HomotopicalAlgebra.CofibrantObject.homRel C)
-- Mathlib.LinearAlgebra.Dimension.Basic
rank_range_of_surjective : ∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M'),
  Function.Surjective ⇑f → Module.rank R ↥f.range = Module.rank R M'
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.toCoweightBasis.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : P.IsRootSystem], b.toCoweightBasis = b.toCoweightBasis
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.stronglyMeasurable : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f : ↥(MeasureTheory.Lp E p μ)), MeasureTheory.StronglyMeasurable ↑↑f
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
IsBaseChange.linearMapLeftRightHom.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_4} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {P : Type u_5} [inst_7 : AddCommMonoid P] [inst_8 : Module R P] {Q : Type u_6} [inst_9 : AddCommMonoid Q]
  [inst_10 : Module R Q] [inst_11 : Module S P] [inst_12 : IsScalarTower R S P] [inst_13 : Module S Q]
  [inst_14 : IsScalarTower R S Q] {α α_1 : M →ₗ[R] P} (e_α : α = α_1) (j : IsBaseChange S α) (β β_1 : N →ₗ[R] Q),
  β = β_1 → j.linearMapLeftRightHom β = ⋯.linearMapLeftRightHom β_1
-- Init.Data.AC
Lean.Data.AC.insert : ℕ → List ℕ → List ℕ
-- Std.Async.Process
/-- Retrieves resource usage statistics.
 -/
Std.IO.Process.getResourceUsage : IO Std.IO.Process.ResourceUsageStats
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.polynomialZ_eq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R},
  W'.polynomialZ =
    MvPolynomial.X 1 ^ 2 + MvPolynomial.C W'.a₁ * MvPolynomial.X 0 * MvPolynomial.X 1 +
        MvPolynomial.C (2 * W'.a₃) * MvPolynomial.X 1 * MvPolynomial.X 2 -
      (MvPolynomial.C W'.a₂ * MvPolynomial.X 0 ^ 2 + MvPolynomial.C (2 * W'.a₄) * MvPolynomial.X 0 * MvPolynomial.X 2 +
        MvPolynomial.C (3 * W'.a₆) * MvPolynomial.X 2 ^ 2)
-- Mathlib.RingTheory.Ideal.Height
_private.Mathlib.RingTheory.Ideal.Height.0.mem_minimalPrimes_of_primeHeight_eq_height : ∀ {R : Type u_1} [inst : CommRing R] {I J : Ideal R} [inst_1 : J.IsPrime],
  I ≤ J → Ideal.primeHeight✝ J = I.height → ∀ [J.FiniteHeight], J ∈ I.minimalPrimes
-- Std.Data.Internal.List.Associative
Std.Internal.List.replaceEntry_eq_map : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.replaceEntry k v l = List.map (fun e => if (e.fst == k) = true then ⟨k, v⟩ else e) l
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
CategoryTheory.Functor.hasPointwiseLeftDerivedFunctorAt_iff_of_mem : ∀ {C : Type u₁} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₃, u₃} H]
  (F : CategoryTheory.Functor C H) (W : CategoryTheory.MorphismProperty C) {X Y : C} (w : X ⟶ Y),
  W w → (F.HasPointwiseLeftDerivedFunctorAt W X ↔ F.HasPointwiseLeftDerivedFunctorAt W Y)
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearMap.BilinForm.comp_inj : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type w}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (B₁ B₂ : LinearMap.BilinForm R M') {l r : M →ₗ[R] M'},
  Function.Surjective ⇑l → Function.Surjective ⇑r → (B₁.comp l r = B₂.comp l r ↔ B₁ = B₂)
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinOrder.of_mem_zpowers : ∀ {G : Type u_1} [inst : Group G] {x y : G}, IsOfFinOrder x → y ∈ Subgroup.zpowers x → IsOfFinOrder y
-- Mathlib.RepresentationTheory.Rep.Basic
/-- Given a representation `A` of a finite group `G`, `norm A` is the representation morphism
`A ⟶ A` defined by `x ↦ ∑ A.ρ g x` for `g` in `G`.  -/
Rep.norm : {k : Type u} →
  [inst : Semiring k] → {G : Type v} → [inst_1 : Group G] → [Fintype G] → (A : Rep.{w, u, v} k G) → CategoryTheory.End A
-- Init.Data.Option.Lemmas
Option.toArray_some : ∀ {α : Type u_1} (a : α), (some a).toArray = #[a]
-- Init.Data.Order.PackageFactories
Std.FactoryInstances.instLawfulOrderBEqOfDecidableLE : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α], Std.LawfulOrderBEq α
-- Mathlib.Topology.Homeomorph.Defs
IsHomeomorph.injective : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsHomeomorph f → Function.Injective f
-- Mathlib.Data.Fintype.Card
Fintype.card_range : ∀ {α : Type u_4} {β : Type u_5} {F : Type u_6} [inst : FunLike F α β] [EmbeddingLike F α β] (f : F) [inst_2 : Fintype α]
  [inst_3 : Fintype ↑(Set.range ⇑f)], Fintype.card ↑(Set.range ⇑f) = Fintype.card α
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.mk.injEq : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (val : ι → S)
  (σ' : S → MvPolynomial ι R) (aeval_val_σ' : ∀ (s : S), (MvPolynomial.aeval val) (σ' s) = s)
  (algebra : Algebra (MvPolynomial ι R) S)
  (algebraMap_eq :
    autoParam (algebraMap (MvPolynomial ι R) S = ↑(MvPolynomial.aeval val)) Algebra.Generators.algebraMap_eq._autoParam)
  (val_1 : ι → S) (σ'_1 : S → MvPolynomial ι R) (aeval_val_σ'_1 : ∀ (s : S), (MvPolynomial.aeval val_1) (σ'_1 s) = s)
  (algebra_1 : Algebra (MvPolynomial ι R) S)
  (algebraMap_eq_1 :
    autoParam (algebraMap (MvPolynomial ι R) S = ↑(MvPolynomial.aeval val_1))
      Algebra.Generators.algebraMap_eq._autoParam),
  ({ val := val, σ' := σ', aeval_val_σ' := aeval_val_σ', algebra := algebra, algebraMap_eq := algebraMap_eq } =
      { val := val_1, σ' := σ'_1, aeval_val_σ' := aeval_val_σ'_1, algebra := algebra_1,
        algebraMap_eq := algebraMap_eq_1 }) =
    (val = val_1 ∧ σ' = σ'_1 ∧ algebra = algebra_1)
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  (hx : AlgebraicIndependent R x) (y : MvPolynomial (Option ι) R),
  hx.mvPolynomialOptionEquivPolynomialAdjoin y =
    Polynomial.map (↑hx.aevalEquiv)
      ((MvPolynomial.aeval fun o => o.elim Polynomial.X fun s => Polynomial.C (MvPolynomial.X s)) y)