mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.ModularForms.BoundedAtCusp
UpperHalfPlane.IsBoundedAtImInfty.slash : ∀ {g : GL (Fin 2) ℝ} {f : UpperHalfPlane → ℂ} (k : ℤ),
  ↑g 1 0 = 0 → UpperHalfPlane.IsBoundedAtImInfty f → UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map k g f)
-- Mathlib.RingTheory.Valuation.Integers
Valuation.ltIdeal_mono : ∀ {R : Type u} {Γ₀ : Type v} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀),
  Monotone v.ltIdeal
-- Mathlib.Topology.Separation.Regular
RegularSpace.of_lift'_closure_le : ∀ {X : Type u_1} [inst : TopologicalSpace X], (∀ (x : X), (nhds x).lift' closure ≤ nhds x) → RegularSpace X
-- Batteries.Data.String.Lemmas
Substring.Raw.Valid.foldr : ∀ {α : Type u_1} (f : Char → α → α) (init : α) {s : Substring.Raw},
  s.Valid → Substring.Raw.Legacy.foldr f init s = List.foldr f init s.toString.toList
-- Init.Data.List.Lemmas
List.set_nil : ∀ {α : Type u_1} {i : ℕ} {a : α}, [].set i a = []
-- Lean.Declaration
/-- Reduction rule for this Constructor  -/
Lean.RecursorRule.ctor : Lean.RecursorRule → Lean.Name
-- Init.Classical
Classical.byContradiction : ∀ {p : Prop}, (¬p → False) → p
-- Mathlib.Topology.Convenient.GeneratedBy
Topology.IsGeneratedBy.le_generatedBy : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} {tY : TopologicalSpace Y}
  [Topology.IsGeneratedBy X Y], tY ≤ TopologicalSpace.generatedBy X
-- Mathlib.Tactic.Convert
/-- Configuration for the `convert` family of tactics.
This is `Congr!.Config` with different, less aggressive, defaults.

To elaborate config options for `convert`, use `Convert.elabConfig` which chooses
between `Convert.CheapConfig` and `Convert.ExpensiveConfig` based on other flags.
 -/
Convert.CheapConfig : Type
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsColimitsClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {α : Type t}
  (J : α → Type u') [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)],
  (P.colimitsClosure J).IsClosedUnderIsomorphisms
-- Batteries.Data.List.Basic
/-- Replaces the first element of the list for which `f` returns `some` with the returned value.  -/
List.replaceF : {α : Type u_1} → (α → Option α) → List α → List α
-- Lean.DocString.Types
Lean.Doc.Inline.linebreak.injEq : ∀ {i : Type u} (string string_1 : String),
  (Lean.Doc.Inline.linebreak string = Lean.Doc.Inline.linebreak string_1) = (string = string_1)
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.areaForm.congr_simp : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o o_1 : Orientation ℝ E (Fin 2)), o = o_1 → o.areaForm = o_1.areaForm
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.instMonoid : {R : Type u} →
  [inst : CommSemiring R] →
    {A : Type u_3} → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → {S : Submonoid R} → Monoid (LocalizedModule S A)
-- Lean.CoreM
Lean.Core.instNonemptySavedState : Nonempty Lean.Core.SavedState
-- Init.Data.SInt.Lemmas
Int64.two_mul : ∀ {a : Int64}, 2 * a = a + a
-- Mathlib.Order.Filter.Germ.Basic
/-- The filter product `(a : α) → ε a` at a filter `l`. This is a dependent version of
`Filter.Germ`.  -/
Filter.Product : {α : Type u_1} → Filter α → (α → Type u_5) → Type (max u_1 u_5)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis.eq_of_subset_indep : ∀ {α : Type u_1} {M : Matroid α} {I J X : Set α}, M.IsBasis I X → M.Indep J → I ⊆ J → J ⊆ X → I = J
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.mem_center_iff : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] [inst_4 : IsScalarTower R A A] [inst_5 : SMulCommClass R A A] {a : A},
  a ∈ NonUnitalStarSubalgebra.center R A ↔ ∀ (b : A), b * a = a * b
-- Mathlib.Analysis.Calculus.ContDiff.Deriv
ContDiffOn.derivWithin : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {m n : WithTop ℕ∞} {f : 𝕜 → F} {s : Set 𝕜},
  ContDiffOn 𝕜 n f s → UniqueDiffOn 𝕜 s → m + 1 ≤ n → ContDiffOn 𝕜 m (derivWithin f s) s
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k fallback : α}, k ∉ m₂ → (m₁ ∩ m₂).getKeyD k fallback = fallback
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_eq_getD_getKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {a fallback : α},
  t.getKeyD a fallback = (t.getKey? a).getD fallback
-- Mathlib.FieldTheory.FinTrdeg
trdeg_lt_aleph0 : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [FinTrdeg K L],
  Algebra.trdeg K L < Cardinal.aleph0
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toArray_ric_eq_self : ∀ {n i : ℕ}, i ≤ n → (*...=n).toArray[i]! = i
-- Mathlib.Algebra.Algebra.Operations
Submodule.instSMulCommClass : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] {α : Type u_1}
  [inst_3 : Monoid α] [inst_4 : DistribMulAction α A] [inst_5 : SMulCommClass α R A] [SMulCommClass α A A],
  SMulCommClass α (Submodule R A) (Submodule R A)
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
/-- Given a matrix with non-zero determinant over a field, we get an element of `GL n K`.  -/
Matrix.GeneralLinearGroup.mkOfDetNeZero : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] → {K : Type u_1} → [inst_2 : Field K] → (A : Matrix n n K) → A.det ≠ 0 → GL n K
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
HasProd.tprod_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β} {f : β → α}
  {a : α} [T2Space α] [L.NeBot], HasProd f a L → ∏'[L] (b : β), f b = a
-- Lean.Declaration
/-- Right hand side of the reduction rule  -/
Lean.RecursorRule.rhs : Lean.RecursorRule → Lean.Expr
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.neg_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} {n : ℕ} [inst_3 : HasDerivedCategory C]
  (α : CategoryTheory.Abelian.Ext X Y n), (-α).hom = -α.hom
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.toPiLocalization_surjective_of_discreteTopology : ∀ (R : Type u) [inst : CommSemiring R] [DiscreteTopology (PrimeSpectrum R)],
  Function.Surjective ⇑(PrimeSpectrum.toPiLocalization R)
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
/-- A `1`-approximate subgroup is the same thing as a subgroup.  -/
isApproximateAddSubgroup_zero : ∀ {G : Type u_1} [inst : AddGroup G] {A : Set G}, IsApproximateAddSubgroup 1 A ↔ ∃ H, ↑H = A
-- Std.Data.DTreeMap.Raw.Lemmas
/-- Simpler variant of `get!_filterMap` when `LawfulEqCmp` is available.  -/
Std.DTreeMap.Raw.Const.get!_filterMap' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [inst : Inhabited γ] {f : α → β → Option γ} {k : α},
  t.WF →
    Std.DTreeMap.Raw.Const.get! (Std.DTreeMap.Raw.filterMap f t) k = ((Std.DTreeMap.Raw.Const.get? t k).bind (f k)).get!
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.ext : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOne M] [inst_1 : MulOne N] ⦃f g : M →* N⦄, (∀ (x : M), f x = g x) → f = g
-- Mathlib.Topology.Instances.ENNReal.Lemmas
/-- Characterization of neighborhoods for `ℝ≥0∞` numbers. See also `tendsto_order`
for a version with strict inequalities.  -/
ENNReal.tendsto_nhds : ∀ {α : Type u_1} {f : Filter α} {u : α → ENNReal} {a : ENNReal},
  a ≠ ⊤ → (Filter.Tendsto u f (nhds a) ↔ ∀ ε > 0, ∀ᶠ (x : α) in f, u x ∈ Set.Icc (a - ε) (a + ε))
-- Init.Data.Ord.Basic
Ordering.eq_then : ∀ {o : Ordering}, Ordering.eq.then o = o
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.instModuleSubtypeMem_1 : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          {S : IntermediateField K L} →
            {E : Type u_4} → [inst_3 : Field E] → [inst_4 : Algebra L E] → (T : IntermediateField (↥S) E) → Module ↥S ↥T
-- Std.Data.TreeMap.Raw.AdditionalOperations
/-- Updates the values of the map by applying the given function to all mappings.  -/
Std.TreeMap.Raw.map : {α : Type u} →
  {β : Type v} →
    {γ : Type w} → {cmp : α → α → Ordering} → (α → β → γ) → Std.TreeMap.Raw α β cmp → Std.TreeMap.Raw α γ cmp
-- Lean.Declaration
/-- The inductive type of the major argument of the recursor.  -/
Lean.RecursorVal.getMajorInduct : Lean.RecursorVal → Lean.Name
-- Mathlib.Data.Finset.Insert
Finset.coe_eq_singleton : ∀ {α : Type u_1} {s : Finset α} {a : α}, ↑s = {a} ↔ s = {a}
-- Mathlib.Data.Set.Lattice.Image
Set.sUnion_prod_const : ∀ {α : Type u_1} {β : Type u_2} {C : Set (Set α)} {t : Set β}, ⋃₀ C ×ˢ t = ⋃₀ ((fun s => s ×ˢ t) '' C)
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
/-- The relationship between `IsPrimitiveRoot.autToPow` and
`modularCyclotomicCharacter`. Note that `IsPrimitiveRoot.autToPow`
needs an explicit root of unity, and also an auxiliary "base ring" `R`.  -/
IsPrimitiveRoot.autToPow_eq_modularCyclotomicCharacter : ∀ {L : Type u} [inst : CommRing L] [inst_1 : IsDomain L] (n : ℕ) [inst_2 : NeZero n] (R : Type u_1)
  [inst_3 : CommRing R] [inst_4 : Algebra R L] {μ : L} (hμ : IsPrimitiveRoot μ n) (g : L ≃ₐ[R] L),
  (IsPrimitiveRoot.autToPow R hμ) g = (modularCyclotomicCharacter L ⋯) g.toRingEquiv
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiffWithinAt.clm_comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {X : Type u_5} [inst_7 : NormedAddCommGroup X]
  [inst_8 : NormedSpace 𝕜 X] {n : WithTop ℕ∞} {g : X → F →L[𝕜] G} {f : X → E →L[𝕜] F} {s : Set X} {x : X},
  ContDiffWithinAt 𝕜 n g s x → ContDiffWithinAt 𝕜 n f s x → ContDiffWithinAt 𝕜 n (fun x => g x ∘SL f x) s x
-- Mathlib.Algebra.Divisibility.Basic
/-- **Alias** of `RightDvd.of_eq`. -/
Eq.rightDvd : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, a = b → a ∣ᵣ b
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
/-- The `r` coefficient of an admissible linear change of variables.  -/
WeierstrassCurve.VariableChange.r : {R : Type u} → [inst : CommRing R] → WeierstrassCurve.VariableChange R → R
-- Mathlib.Order.CountableSupClosed
CountableSupClosed.sInter : ∀ {α : Type u_2} {S : Set (Set α)} [inst : LE α], (∀ s ∈ S, CountableSupClosed s) → CountableSupClosed (⋂₀ S)
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.symm.eq_1 : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S),
  e.symm = { toEquiv := e.toMulEquiv.symm.toEquiv, map_mul' := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.Notation.Support
Function.support.eq_1 : ∀ {ι : Type u_1} {M : Type u_3} [inst : Zero M] (f : ι → M), Function.support f = {x | f x ≠ 0}
-- Mathlib.Algebra.Group.Center
Set.mem_centralizer_iff : ∀ {M : Type u_1} {S : Set M} [inst : Mul M] {c : M}, c ∈ S.centralizer ↔ ∀ m ∈ S, m * c = c * m
-- Mathlib.Algebra.DualQuaternion
Quaternion.fst_re_dualNumberEquiv_symm : ∀ {R : Type u_1} [inst : CommRing R] (d : DualNumber (Quaternion R)),
  TrivSqZeroExt.fst (Quaternion.dualNumberEquiv.symm d).re = (TrivSqZeroExt.fst d).re
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
OpenPartialHomeomorph.restr_trans : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) (s : Set X),
  (e.restr s).trans e' = (e.trans e').restr s
-- Mathlib.Algebra.Colimit.Ring
/-- Every element of the direct limit corresponds to some element in
some component of the directed system.  -/
Ring.DirectLimit.exists_of : ∀ {ι : Type u_1} [inst : Preorder ι] {G : ι → Type u_2} [inst_1 : (i : ι) → CommRing (G i)]
  {f : (i j : ι) → i ≤ j → G i → G j} [Nonempty ι] [IsDirectedOrder ι] (z : Ring.DirectLimit G f),
  ∃ i x, (Ring.DirectLimit.of G f i) x = z
-- Mathlib.Tactic.DeriveFintype
/-- Derive a `Fintype` instance for enum types. These come with a `ctorIdx` function.

We generate a more optimized instance than the one produced by `mkFintype`.
The strategy is to (1) create a list `enumList` of all the constructors, (2) prove that this
is in `ctorIdx` order, (3) show that `ctorIdx` maps `enumList` to `List.range numCtors` to show
the list has no duplicates, and (4) give the `Fintype` instance, using 2 for completeness.

The proofs are all linear complexity, and the main computation is that
`enumList.map ctorIdx = List.range numCtors`, which is true by `refl`.  -/
Mathlib.Deriving.Fintype.mkFintypeEnum : Lean.Name → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Data.List.ReduceOption
List.reduceOption_length_eq : ∀ {α : Type u_1} {l : List (Option α)}, l.reduceOption.length = (List.filter Option.isSome l).length
-- Mathlib.FieldTheory.Extension
IntermediateField.exists_algHom_adjoin_of_splits_of_aeval : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] {S : Set E},
  (∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits) →
    ∀ {x : E} {y : K} (hx : x ∈ IntermediateField.adjoin F S),
      (Polynomial.aeval y) (minpoly F x) = 0 → ∃ φ, φ ⟨x, hx⟩ = y
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.exp_eq_tsum_rat : ∀ {𝔸 : Type u_2} [inst : Ring 𝔸] [inst_1 : TopologicalSpace 𝔸] [inst_2 : IsTopologicalRing 𝔸] [inst_3 : Algebra ℚ 𝔸],
  NormedSpace.exp = fun x => ∑' (n : ℕ), (↑n.factorial)⁻¹ • x ^ n
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Comonad.forget_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C), G.forget.Faithful
-- Init.Data.Vector.Range
Vector.count_range_1' : ∀ {a s n : ℕ}, Vector.count a (Vector.range' s n) = if s ≤ a ∧ a < s + n then 1 else 0
-- Mathlib.Order.Completion
DedekindCut.principal_inj : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, DedekindCut.principal a = DedekindCut.principal b ↔ a = b
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
totallyBounded_inv : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {s : Set α},
  TotallyBounded s⁻¹ ↔ TotallyBounded s
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Subgraph.connected_iff' : ∀ {V : Type u} {G : SimpleGraph V} {H : G.Subgraph}, H.Connected ↔ H.coe.Connected
-- Mathlib.Topology.Order.SuccPred
SuccOrder.isOpen_iff : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] [SuccOrder α] [NoMaxOrder α]
  {s : Set α}, IsOpen s ↔ ∀ o ∈ s, Order.IsSuccLimit o → ∃ a < o, Set.Ioo a o ⊆ s
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
/-- The Riesz measure induced by a positive linear functional on `C_c(X, ℝ)` is regular.  -/
RealRMK.regular_rieszMeasure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] [inst_2 : MeasurableSpace X] [inst_3 : BorelSpace X]
  (Λ : CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ) [inst_4 : LocallyCompactSpace X], (RealRMK.rieszMeasure Λ).Regular
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.coe_mul : ∀ {𝕜 : 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'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {G : Type u_10} [inst_9 : Mul G] [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H' G]
  [inst_12 : ContMDiffMul I' n G] (f g : ContMDiffMap I I' N G n), ⇑(f * g) = ⇑f * ⇑g
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- On the translated support, `p.mulShift v` agrees with `p.config` at the preimage.

More precisely, if `w ∈ p.support`, then at the translated site `v * w`,
the configuration `p.mulShift v` takes the value `p.config w`.

This uses `[IsLeftCancelMul G]` to identify the unique preimage of `v * w`
under left-multiplication by `v`.  -/
SymbolicDynamics.FullShift.Pattern.mulShift_apply_mul_left_of_mem : ∀ {A : Type u_1} [inst : Inhabited A] {G : Type u_2} [inst_1 : Monoid G] [IsLeftCancelMul G]
  (p : SymbolicDynamics.FullShift.Pattern A G) (v w : G), w ∈ p.support → p.mulShift v (v * w) = p.config w
-- Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
/-- Any inner product space has smooth bump functions.  -/
hasContDiffBump_of_innerProductSpace : ∀ (E : Type u_1) [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E], HasContDiffBump E
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalRingHom.mem_eqLocus : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] {f g : R →ₙ+* S}
  {x : R}, x ∈ f.eqLocus g ↔ f x = g x
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.OplaxLeftLinear.δₗ_unitality_inv_assoc : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'} [self : F.OplaxLeftLinear C] (d : D) {Z : D'}
  (h :
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (F.obj d) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso (F.obj d)).inv h =
    CategoryTheory.CategoryStruct.comp
      (F.map (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OplaxLeftLinear.δₗ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) d) h)
-- Mathlib.Computability.Language
Symbol.nonterminal.injEq : ∀ {T : Type u_4} {N : Type u_5} (n n_1 : N), (Symbol.nonterminal n = Symbol.nonterminal n_1) = (n = n_1)
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.dual_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Lattice α] [inst_1 : BoundedOrder α] [inst_2 : Lattice β]
  [inst_3 : BoundedOrder β] [inst_4 : Lattice γ] [inst_5 : BoundedOrder γ] (g : BoundedLatticeHom β γ)
  (f : BoundedLatticeHom α β),
  BoundedLatticeHom.dual (g.comp f) = (BoundedLatticeHom.dual g).comp (BoundedLatticeHom.dual f)
-- Lean.Parser.Command
Lean.Parser.Command.deprecated_module.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFinite.mk : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  autoParam (∀ (P : Ideal R) [inst_3 : P.IsPrime], Module.Finite P.ResidueField (P.Fiber S))
      Algebra.QuasiFinite.finite_fiber._autoParam →
    Algebra.QuasiFinite R S
-- Mathlib.Analysis.Matrix.Normed
/-- This applies to the sup norm of sup norm.  -/
Matrix.normSMulClass : ∀ {R : Type u_1} {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedRing R] [inst_3 : SeminormedAddCommGroup α] [inst_4 : Module R α] [NormSMulClass R α],
  NormSMulClass R (Matrix m n α)
-- Lean.Elab.App
/-- whnfCore + implicit consumption.
Example: given `e` with `eType := {α : Type} → (fun β => List β) α `, it produces `(e ?m, List ?m)` where `?m` is fresh metavariable.  -/
_private.Lean.Elab.App.0.Lean.Elab.Term.consumeImplicits : Lean.Syntax → Lean.Expr → Lean.Expr → Bool → Lean.Elab.TermElabM (Lean.Expr × Lean.Expr)
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
/-- In a Noetherian ring, the height of a principal ideal spanned by a non-unit is at most one.  -/
Ideal.height_span_singleton_le_one : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {x : R}, ¬IsUnit x → (Ideal.span {x}).height ≤ 1
-- Mathlib.RingTheory.Algebraic.Integral
rank_mvPolynomial_mvPolynomial : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [NoZeroDivisors R]
  (σ : Type u), Module.rank (MvPolynomial σ R) (MvPolynomial σ S) = Cardinal.lift.{u, u_2} (Module.rank R S)
-- Mathlib.Topology.Order.Lattice
ContinuousWithinAt.sup' : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] [inst_2 : Max L]
  [ContinuousSup L] {f g : X → L} {s : Set X} {x : X},
  ContinuousWithinAt f s x → ContinuousWithinAt g s x → ContinuousWithinAt (f ⊔ g) s x
-- Mathlib.Data.ENat.Basic
instOrderBotENat : OrderBot ℕ∞
-- Mathlib.RingTheory.Derivation.Basic
Derivation.instSMulCommClass : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M] {S : Type u_5}
  {T : Type u_6} [inst_6 : Monoid S] [inst_7 : DistribMulAction S M] [inst_8 : SMulCommClass R S M]
  [inst_9 : SMulCommClass S A M] [inst_10 : Monoid T] [inst_11 : DistribMulAction T M] [inst_12 : SMulCommClass R T M]
  [inst_13 : SMulCommClass T A M] [SMulCommClass S T M], SMulCommClass S T (Derivation R A M)
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
HomotopicalAlgebra.AttachCells.hm_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a}
  {X₁ X₂ : C} {f : X₁ ⟶ X₂} (self : HomotopicalAlgebra.AttachCells g f) (i : self.ι) {Z : C} (h : self.cofan₂.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.cofan₁.inj i) (CategoryTheory.CategoryStruct.comp self.m h) =
    CategoryTheory.CategoryStruct.comp (g (self.π i)) (CategoryTheory.CategoryStruct.comp (self.cofan₂.inj i) h)
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.quotEquivQuotMap_apply : ∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R) (I : Ideal R)
  (a : AdjoinRoot f ⧸ Ideal.map (AdjoinRoot.of f) I),
  (AdjoinRoot.quotEquivQuotMap f I) a = (AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot I f) a
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey_eq_getKey! : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m.WF → ∀ {a : α} {h' : a ∈ m}, m.getKey a h' = m.getKey! a
-- Mathlib.Probability.Kernel.Composition.ParallelComp
/-- Parallel product of two kernels.  -/
ProbabilityTheory.Kernel.parallelComp : {α : Type u_5} →
  {β : Type u_6} →
    {γ : Type u_7} →
      {δ : Type u_8} →
        {mα : MeasurableSpace α} →
          {mβ : MeasurableSpace β} →
            {mγ : MeasurableSpace γ} →
              {mδ : MeasurableSpace δ} →
                ProbabilityTheory.Kernel α β → ProbabilityTheory.Kernel γ δ → ProbabilityTheory.Kernel (α × γ) (β × δ)
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.enum_zero_le' : ∀ {o : Ordinal.{u_1}} (h0 : 0 < o) (a : o.ToType), (Ordinal.enum fun x1 x2 => x1 < x2) ⟨0, ⋯⟩ ≤ a
-- Mathlib.Analysis.InnerProductSpace.LinearMap
LinearEquiv.isometryOfInner_toLinearEquiv : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {E' : Type u_7} [inst_3 : SeminormedAddCommGroup E'] [inst_4 : InnerProductSpace 𝕜 E'] (f : E ≃ₗ[𝕜] E')
  (h : ∀ (x y : E), inner 𝕜 (f x) (f y) = inner 𝕜 x y), (f.isometryOfInner h).toLinearEquiv = f
-- Mathlib.FieldTheory.Minpoly.Field
IsOfFinOrder.unit.congr_simp : ∀ {M : Type u_6} [inst : Monoid M] {x x_1 : M} (e_x : x = x_1) (hx : IsOfFinOrder x), hx.unit = ⋯.unit