mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Category.DeltaGenerated
/-- The adjunction between the forgetful functor `DeltaGenerated ⥤ TopCat` and its coreflector.  -/
DeltaGenerated.coreflectorAdjunction : DeltaGenerated.deltaGeneratedToTop ⊣ TopCat.toDeltaGenerated
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.Γevaluation_naturality_apply : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↥X) (a : ↑(Y.presheaf.obj (Opposite.op ⊤))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x))
      ((CategoryTheory.ConcreteCategory.hom (Y.Γevaluation (f x))) a) =
    (CategoryTheory.ConcreteCategory.hom (X.Γevaluation x))
      ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop f)) a)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.div_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Div β] (f g : MeasureTheory.SimpleFunc α β)
  (x : α), (f / g) x = f x / g x
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- A sheaf of A is a presheaf `P : Cᵒᵖ ⥤ A` such that for every `E : A`, the
presheaf of types given by sending `U : C` to `Hom_{A}(E, P U)` is a sheaf of types.  -/
CategoryTheory.Presheaf.IsSheaf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        CategoryTheory.GrothendieckTopology C → CategoryTheory.Functor Cᵒᵖ A → Prop
-- Mathlib.Topology.Germ
Germ.coe_sum : ∀ {α : Type u_4} (l : Filter α) (R : Type u_5) [inst : AddCommMonoid R] {ι : Type u_6} (f : ι → α → R) (s : Finset ι),
  ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.natDegree_Ψ₂Sq : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), 4 ≠ 0 → W.Ψ₂Sq.natDegree = 3
-- Mathlib.Algebra.Category.MonCat.Basic
_private.Mathlib.Algebra.Category.MonCat.Basic.0.CommMonCat.Hom.mk.inj : ∀ {A B : CommMonCat} {hom' hom'_1 : ↑A →* ↑B}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
/-- Left homotopy is closed under composition.  -/
CategoryTheory.Arrow.LeftHomotopy.comp : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {u v w : CategoryTheory.Arrow V} →
        {f₁ g₁ : u ⟶ v} →
          {f₂ g₂ : v ⟶ w} →
            CategoryTheory.Arrow.LeftHomotopy f₁ g₁ →
              CategoryTheory.Arrow.LeftHomotopy f₂ g₂ →
                CategoryTheory.Arrow.LeftHomotopy (CategoryTheory.CategoryStruct.comp f₁ f₂)
                  (CategoryTheory.CategoryStruct.comp g₁ g₂)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
/-- Unit monomial, represented as a list of its exponents. `[e₁, e₂, ..., eₙ]` corresponds to
`basis[0] ^ e₁ * ... * basis[n] ^ eₙ` where `basis` is the basis of functions.  -/
Tactic.ComputeAsymptotics.UnitMonomial : Type
-- Mathlib.RingTheory.Localization.Defs
/-- If `CommSemiring` homs `g : R →+* P, l : P →+* A` induce maps of localizations, the composition
of the induced maps equals the map of localizations induced by `l ∘ g`.  -/
IsLocalization.map_map : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {g : R →+* P}
  {T : Submonoid P} {Q : Type u_4} [inst_5 : CommSemiring Q] [inst_6 : Algebra P Q] [inst_7 : IsLocalization T Q]
  (hy : M ≤ Submonoid.comap g T) {A : Type u_5} [inst_8 : CommSemiring A] {U : Submonoid A} {W : Type u_6}
  [inst_9 : CommSemiring W] [inst_10 : Algebra A W] [inst_11 : IsLocalization U W] {l : P →+* A}
  (hl : T ≤ Submonoid.comap l U) (x : S),
  (IsLocalization.map W l hl) ((IsLocalization.map Q g hy) x) = (IsLocalization.map W (l.comp g) ⋯) x
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.isValue : Lean.Parser.Parser
-- Mathlib.Data.DFinsupp.Submonoid
dfinsuppSum_mem : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : AddCommMonoid γ] {S : Type u_1} [inst_4 : SetLike S γ]
  [AddSubmonoidClass S γ] (s : S) (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → γ),
  (∀ (c : ι), f c ≠ 0 → g c (f c) ∈ s) → f.sum g ∈ s
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.isCauSeq_iff_lift : ∀ {f : ℕ → ℚ}, IsCauSeq abs f ↔ IsCauSeq abs fun i => ↑(f i)
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sinh_add_cosh : ∀ (x : ℂ), Complex.sinh x + Complex.cosh x = Complex.exp x
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.BitVec.sub_eq_iff_eq_add : ∀ {w : ℕ} (a b c : BitVec w), (a + (~~~b + 1#w) == c) = (a == c + b)
-- Lean.Data.AssocList
Lean.AssocList.cons.injEq : ∀ {α : Type u} {β : Type v} (key : α) (value : β) (tail : Lean.AssocList α β) (key_1 : α) (value_1 : β)
  (tail_1 : Lean.AssocList α β),
  (Lean.AssocList.cons key value tail = Lean.AssocList.cons key_1 value_1 tail_1) =
    (key = key_1 ∧ value = value_1 ∧ tail = tail_1)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Pos.skip?_prop_eq_some_iff : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String} {pos res : s.Pos},
  pos.skip? P = some res ↔ ∃ (h : pos ≠ s.endPos), res = pos.next h ∧ P (pos.get h)
-- Lean.MetavarContext
/-- Index mapping user-friendly names to ids.  -/
Lean.MetavarContext.userNames : Lean.MetavarContext → Lean.PersistentHashMap Lean.Name Lean.MVarId
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonWorkspaceEdit : Lean.ToJson Lean.Lsp.WorkspaceEdit
-- Lean.Meta.Tactic.Subst
Lean.Meta.substCore : Lean.MVarId →
  Lean.FVarId →
    optParam Bool false →
      optParam Lean.Meta.FVarSubst { } →
        optParam Bool true → optParam Bool false → Lean.MetaM (Lean.Meta.FVarSubst × Lean.MVarId)
-- Mathlib.Analysis.Polynomial.Order
Polynomial.zero_lt_negOnePow_mul_eval_of_lt_roots_of_leadingCoeff_nonneg : ∀ {P : Polynomial ℝ} {x : ℝ},
  (∀ (y : ℝ), P.IsRoot y → x < y) → 0 ≤ P.leadingCoeff → 0 < ↑↑(↑P.natDegree).negOnePow * Polynomial.eval x P
-- Mathlib.RingTheory.Polynomial.Hermite.Basic
Polynomial.hermite_monic : ∀ (n : ℕ), (Polynomial.hermite n).Monic
-- Mathlib.Data.Set.Countable
Set.Finite.countable : ∀ {α : Type u} {s : Set α}, s.Finite → s.Countable
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey_insertEntry_le_minKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {v : β k} {he : l.isEmpty = false},
      (compare (Std.Internal.List.minKey (Std.Internal.List.insertEntry k v l) ⋯)
            (Std.Internal.List.minKey l he)).isLE =
        true
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.FineSubfamilyOn.measurableSet_u : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  {v : VitaliFamily μ} {f : X → Set (Set X)} {s : Set X} (h : v.FineSubfamilyOn f s) {p : X × Set X},
  p ∈ h.index → MeasurableSet (h.covering p)
-- Mathlib.Analysis.Convex.Quasiconvex
Monotone.quasilinearOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β] [inst_6 : Module 𝕜 E] [PosSMulMono 𝕜 E]
  {f : E → β}, Monotone f → QuasilinearOn 𝕜 Set.univ f
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
CovariantDerivative.torsion_apply : ∀ {𝕜 : 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] {x : M} [inst_6 : CompleteSpace 𝕜]
  [inst_7 : CompleteSpace E] [inst_8 : FiniteDimensional 𝕜 E] [inst_9 : IsManifold I 2 M]
  (cov : CovariantDerivative I E (TangentSpace I)) {X Y : (x : M) → TangentSpace I x},
  MDiffAt (T% X) x →
    MDiffAt (T% Y) x →
      ((cov.torsion x) (X x)) (Y x) = (↑cov Y x) (X x) - (↑cov X x) (Y x) - VectorField.mlieBracket I X Y x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.map_toUnit_comp_terminalComparison : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) (A : C),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A))
      (CategoryTheory.CartesianMonoidalCategory.terminalComparison F) =
    CategoryTheory.SemiCartesianMonoidalCategory.toUnit (F.obj A)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.foldrM_eq_foldrM_toList : ∀ {α : Type u} {δ : Type w} {m : Type w → Type w'} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [inst : Monad m] [LawfulMonad m] {f : α → β → δ → m δ} {init : δ},
  Std.DTreeMap.Internal.Impl.foldrM f init t =
    List.foldrM (fun a b => f a.1 a.2 b) init (Std.DTreeMap.Internal.Impl.Const.toList t)
-- Mathlib.Data.PNat.Factors
PrimeMultiset.ofPrime.eq_1 : ∀ (p : Nat.Primes), PrimeMultiset.ofPrime p = {p}
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.map_smul_left : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R M] [inst_7 : Module R N]
  [inst_8 : Module R₂ M₂] [inst_9 : Module R₂ N₂] (r : R₂) (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂),
  TensorProduct.map (r • f) g = r • TensorProduct.map f g
-- Mathlib.LinearAlgebra.Alternating.Curry
/-- Given an alternating map `f` in `n+1` variables, split the first variable to obtain
a linear map into alternating maps in `n` variables, given by `x ↦ (m ↦ f (Matrix.vecCons x m))`.
It can be thought of as a map $Hom(\bigwedge^{n+1} M, N) \to Hom(M, Hom(\bigwedge^n M, N))$.

This is `MultilinearMap.curryLeft` for `AlternatingMap`. See also
`AlternatingMap.curryLeftLinearMap`.  -/
AlternatingMap.curryLeft : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module R M] →
              [inst_4 : Module R N] → {n : ℕ} → M [⋀^Fin n.succ]→ₗ[R] N → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
-- Mathlib.Data.Finset.Lattice.Prod
/-- See also `Finset.prodMk_inf'_inf'`.  -/
Finset.inf'_prodMap : ∀ {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β]
  {s : Finset ι} {t : Finset κ} (hst : (s ×ˢ t).Nonempty) (f : ι → α) (g : κ → β),
  (s ×ˢ t).inf' hst (Prod.map f g) = (s.inf' ⋯ f, t.inf' ⋯ g)
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.FlatMap.0.Std.Iter.step_flatMapAfterM.match_5.eq_2 : ∀ {α₂ γ : Type u_1} {m : Type u_1 → Type u_2} (motive : Option (Std.IterM m γ) → Sort u_3) (it₂ : Std.IterM m γ)
  (h_1 : some it₂ = none → motive none) (h_2 : (it₂_1 : Std.IterM m γ) → some it₂ = some it₂_1 → motive (some it₂_1)),
  (match hit : some it₂ with
    | none => h_1 hit
    | some it₂_1 => h_2 it₂_1 hit) =
    h_2 it₂ ⋯
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.spanningCoeEquivCoeOfSpanning_apply_coe : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (h : G'.IsSpanning) (v : V),
  ↑((G'.spanningCoeEquivCoeOfSpanning h) v) = v
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_add_mul₀ : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [inst : Add β]
  [MeasurableAdd₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ)) →
      ∀ (i j k l : ι), i ≠ k → i ≠ l → j ≠ k → j ≠ l → ProbabilityTheory.Kernel.IndepFun (f i + f j) (f k + f l) κ μ
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.singletonOneHom.eq_1 : ∀ {α : Type u_2} [inst : One α], Finset.singletonOneHom = { toFun := singleton, map_one' := ⋯ }
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueD_filter_not_contains_map_fst_of_contains_map_fst_right : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α} {fallback : β},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₂ = true →
      Std.Internal.List.getValueD k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) fallback =
        fallback
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.Λ'.go.injEq : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (k : K) (a : Turing.TM2to1.StAct K Γ σ k)
  (a_1 : Turing.TM2.Stmt Γ Λ σ) (k_1 : K) (a_2 : Turing.TM2to1.StAct K Γ σ k_1) (a_3 : Turing.TM2.Stmt Γ Λ σ),
  (Turing.TM2to1.Λ'.go k a a_1 = Turing.TM2to1.Λ'.go k_1 a_2 a_3) = (k = k_1 ∧ a ≍ a_2 ∧ a_1 = a_3)
-- Lean.Meta.Tactic.Grind.Cases
/-- The `grind` tactic includes an auxiliary `cases` tactic that is not intended for direct use by users.
This method implements it.
This tactic is automatically applied when introducing local declarations with a type tagged with `[grind_cases]`.
It is also used for "case-splitting" on terms during the search.

It differs from the user-facing Lean `cases` tactic in the following ways:

- It avoids unnecessary `revert` and `intro` operations.

- It does not introduce new local declarations for each minor premise. Instead, the `grind` tactic preprocessor is responsible for introducing them.

- If the major premise type is an indexed family, auxiliary declarations and (heterogeneous) equalities are introduced.
  However, these equalities are not resolved using `unifyEqs`. Instead, the `grind` tactic employs union-find and
  congruence closure to process these auxiliary equalities. This approach avoids applying substitution to propositions
  that have already been internalized by `grind`.
 -/
Lean.Meta.Grind.cases : Lean.MVarId → Lean.Expr → Lean.MetaM (List Lean.MVarId)
-- Mathlib.Algebra.Ring.BooleanRing
ofBoolAlg_top : ∀ {α : Type u_1} [inst : BooleanRing α], ofBoolAlg ⊤ = 1
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.InjectiveInfo : Type
-- Init.Data.Int.DivMod.Lemmas
Int.neg_tdiv : ∀ (a b : ℤ), (-a).tdiv b = -a.tdiv b
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.vanishingIdeal_anti_mono_iff : ∀ {R : Type u} [inst : CommSemiring R] {s t : Set (PrimeSpectrum R)},
  IsClosed t → (s ⊆ t ↔ PrimeSpectrum.vanishingIdeal t ≤ PrimeSpectrum.vanishingIdeal s)
-- Lean.Data.KVMap
/-- Update an `Int` entry based on its current value.  -/
Lean.KVMap.updateInt : Lean.KVMap → Lean.Name → (ℤ → ℤ) → Lean.KVMap
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.natDegree_iterate_comp : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R} [NoZeroDivisors R] (k : ℕ),
  (p.comp^[k] q).natDegree = p.natDegree ^ k * q.natDegree
-- Mathlib.Topology.UniformSpace.Ultra.Completion
IsUltraUniformity.cauchyFilter_iff : ∀ {X : Type u_1} [inst : UniformSpace X], IsUltraUniformity (CauchyFilter X) ↔ IsUltraUniformity X
-- Mathlib.NumberTheory.LucasLehmer
mersenne_succ : ∀ (n : ℕ), mersenne (n + 1) = 2 * mersenne n + 1
-- Mathlib.Logic.Equiv.Finset
Denumerable.lower'.eq_2 : ∀ (x m : ℕ) (l : List ℕ), Denumerable.lower' (m :: l) x = (m - x) :: Denumerable.lower' l (m + 1)
-- Mathlib.Analysis.Calculus.Deriv.Inv
HasDerivAt.inv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_1} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {c : 𝕜 → 𝕜'} {c' : 𝕜'}, HasDerivAt c c' x → c x ≠ 0 → HasDerivAt c⁻¹ (-c' / c x ^ 2) x
-- Mathlib.Order.Heyting.Basic
PUnit.bot_eq : ⊥ = PUnit.unit
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.instFunLike : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] → [inst_2 : AddZeroClass α] → [inst_3 : AddZeroClass β] → FunLike (α →+o β) α β
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.alterKey : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] →
      [LawfulBEq α] → (k : α) → (Option (β k) → Option (β k)) → List ((a : α) × β a) → List ((a : α) × β a)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
/-- Given `L/K` finite and Galois, and `x : Lˣ`, this essentially says
`(∏ σ) • x = N_{L/K}(x)`, where the product is over `σ ∈ Gal(L/K)`.  -/
groupCohomology.norm_ofAlgebraAutOnUnits_eq : ∀ {K L : Type} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [inst_3 : FiniteDimensional K L]
  [IsGalois K L] (x : Lˣ),
  ↑(Additive.toMul
        (Rep.toAdditive ((Rep.Hom.hom (Rep.ofAlgebraAutOnUnits K L).norm) (Rep.toAdditive.symm (Additive.ofMul x))))) =
    (algebraMap K L) ((Algebra.norm K) ↑x)
-- Mathlib.CategoryTheory.FintypeCat
/-- `FintypeCat.Skeleton` is a skeleton of `FintypeCat`.  -/
FintypeCat.isSkeleton : CategoryTheory.IsSkeletonOf FintypeCat FintypeCat.Skeleton FintypeCat.Skeleton.incl
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpExtension.getTheorems : Lean.Meta.SimpExtension → Lean.CoreM Lean.Meta.SimpTheorems
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.not_neg'' : ∀ {w : ℕ} (x : BitVec w), ~~~(1#w + x) = ~~~x + -1#w
-- Init.Data.Int.Order
_private.Init.Data.Int.Order.0.Int.neg.match_1.eq_1 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n)) (h_2 : (n : ℕ) → motive (Int.negSucc n)),
  (match Int.ofNat n with
    | Int.ofNat n => h_1 n
    | Int.negSucc n => h_2 n) =
    h_1 n
-- Mathlib.CategoryTheory.Subobject.NoetherianObject
CategoryTheory.instWellFoundedGTSubobjectOfIsNoetherianObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.IsNoetherianObject X],
  WellFoundedGT (CategoryTheory.Subobject X)
-- Init.System.IO
IO.FS.instReprDirEntry : Repr IO.FS.DirEntry
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_map_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X)
  {c c' : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)} (f : c ⟶ c'),
  ((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor F U).map f).hom = f.hom
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.isPosSemidef_def : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M} [inst_3 : LE R], B.IsPosSemidef ↔ B.IsSymm ∧ B.IsNonneg
-- Mathlib.Order.Max
noBotOrder_iff' : ∀ (α : Type u_3) [inst : LE α], NoBotOrder α ↔ ∀ (a : α), ∃ b, ¬a ≤ b
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.addMonoidal_rightUnitor : ∀ (M : Type u) [inst : AddMonoid M] (X : CategoryTheory.Discrete M),
  CategoryTheory.MonoidalCategoryStruct.rightUnitor X = CategoryTheory.Discrete.eqToIso ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.assocInv_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {sXY : CategoryTheory.Limits.BinaryFan X Y}
  {sYZ : CategoryTheory.Limits.BinaryFan Y Z} (P : CategoryTheory.Limits.IsLimit sXY)
  (s : CategoryTheory.Limits.BinaryFan X sYZ.pt),
  (CategoryTheory.Limits.BinaryFan.assocInv P s).snd = CategoryTheory.CategoryStruct.comp s.snd sYZ.snd
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.commute_add_int : ∀ (f : CircleDeg1Lift) (n : ℤ), Function.Commute ⇑f fun x => x + ↑n
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
TangentBundle.trivializationAt_fst : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] (x : M) (z : TangentBundle I M),
  (↑(trivializationAt E (TangentSpace I) x) z).1 = z.proj
-- Mathlib.Topology.Instances.Real.Lemmas
Real.uniformContinuous_mul : ∀ (s : Set (ℝ × ℝ)) {r₁ r₂ : ℝ}, (∀ x ∈ s, |x.1| < r₁ ∧ |x.2| < r₂) → UniformContinuous fun p => (↑p).1 * (↑p).2
-- Mathlib.CategoryTheory.ObjectProperty.HasCardinalLT
CategoryTheory.ObjectProperty.HasCardinalLT.sup : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P₁ P₂ : CategoryTheory.ObjectProperty C} {κ : Cardinal.{w}},
  P₁.HasCardinalLT κ → P₂.HasCardinalLT κ → Cardinal.aleph0 ≤ κ → (P₁ ⊔ P₂).HasCardinalLT κ
-- Mathlib.Analysis.LocallyConvex.AbsConvex
/-- The absolutely convex closed hull of a set `s` is the minimal absolutely convex closed set that
includes `s`.  -/
closedAbsConvexHull : (𝕜 : Type u_1) →
  {E : Type u_2} →
    [SeminormedRing 𝕜] →
      [SMul 𝕜 E] → [AddCommMonoid E] → [PartialOrder 𝕜] → [TopologicalSpace E] → ClosureOperator (Set E)
-- Mathlib.CategoryTheory.Functor.Flat
/-- If `C` is finitely complete, then `F : C ⥤ D` is representably flat iff it preserves
finite limits.
 -/
CategoryTheory.preservesFiniteLimits_iff_flat : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.Limits.HasFiniteLimits C] (F : CategoryTheory.Functor C D),
  CategoryTheory.RepresentablyFlat F ↔ CategoryTheory.Limits.PreservesFiniteLimits F
-- Init.Grind.AC
Lean.Grind.AC.Seq.insert_k.eq_1 : ∀ (x : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq),
  Lean.Grind.AC.Seq.insert_k x s =
    Lean.Grind.AC.Seq.rec
      (fun y =>
        Bool.rec (Lean.Grind.AC.Seq.cons y (Lean.Grind.AC.Seq.var x))
          (Lean.Grind.AC.Seq.cons x (Lean.Grind.AC.Seq.var y)) (Nat.blt x y))
      (fun y s ih =>
        Bool.rec (Lean.Grind.AC.Seq.cons y ih) (Lean.Grind.AC.Seq.cons x (Lean.Grind.AC.Seq.cons y s)) (Nat.blt x y))
      s
-- Init.Data.Array.MinMax
Array.max?_eq_some_iff : ∀ {α : Type u_1} {a : α} [inst : Max α] [inst_1 : LE α] {xs : Array α} [Std.IsLinearOrder α] [Std.LawfulOrderMax α],
  xs.max? = some a ↔ a ∈ xs ∧ ∀ b ∈ xs, b ≤ a
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.instSMulCommClass : ∀ {M : Type u_2} {N : Type u_3} {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Monoid M]
  [inst_2 : Monoid N] [inst_3 : DistribMulAction M α] [inst_4 : SMulCommClass M α α] [inst_5 : IsScalarTower M α α]
  [inst_6 : DistribMulAction N α] [inst_7 : SMulCommClass N α α] [inst_8 : IsScalarTower N α α] [SMulCommClass M N α],
  SMulCommClass M N (CentroidHom α)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
EisensteinSeries.e2Summand.eq_1 : ∀ (m : ℤ) (z : UpperHalfPlane), EisensteinSeries.e2Summand m z = ∑' (n : ℤ), EisensteinSeries.eisSummand 2 ![m, n] z
-- Mathlib.LinearAlgebra.StdBasis
/-- The `R`-submodule of `η → R` consisting of functions supported in the subset `s`.  -/
Pi.spanSubset : (R : Type u_2) → {η : Type u_4} → [inst : Semiring R] → [Finite η] → Set η → Submodule R (η → R)
-- Batteries.Data.AssocList
/-- Optimized version of `toList`.  -/
Batteries.AssocList.toListTR : {α : Type u_1} → {β : Type u_2} → Batteries.AssocList α β → List (α × β)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.rpow_def : ∀ {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] {a : A} {y : ℝ}, a ^ y = cfc (fun x => x ^ y) a