mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balanceL.match_5.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (rs : ℕ) (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (l_1 : Std.DTreeMap.Internal.Impl α β) →
      l_1.Balanced →
        Std.DTreeMap.Internal.Impl.BalanceLPrecond l_1.size (Std.DTreeMap.Internal.Impl.inner rs k v l r).size →
          Sort u_3)
  (hlb : Std.DTreeMap.Internal.Impl.leaf.Balanced)
  (hlr :
    Std.DTreeMap.Internal.Impl.BalanceLPrecond Std.DTreeMap.Internal.Impl.leaf.size
      (Std.DTreeMap.Internal.Impl.inner rs k v l r).size)
  (h_1 :
    (hlb : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
      (hlr :
          Std.DTreeMap.Internal.Impl.BalanceLPrecond Std.DTreeMap.Internal.Impl.leaf.size
            (Std.DTreeMap.Internal.Impl.inner rs k v l r).size) →
        motive Std.DTreeMap.Internal.Impl.leaf hlb hlr)
  (h_2 :
    (ls : ℕ) →
      (lk : α) →
        (lv : β lk) →
          (ll lr : Std.DTreeMap.Internal.Impl α β) →
            (hlb : (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).Balanced) →
              (hlr :
                  Std.DTreeMap.Internal.Impl.BalanceLPrecond (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).size
                    (Std.DTreeMap.Internal.Impl.inner rs k v l r).size) →
                motive (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr) hlb hlr),
  (match Std.DTreeMap.Internal.Impl.leaf, hlb, hlr with
    | Std.DTreeMap.Internal.Impl.leaf, hlb, hlr => h_1 hlb hlr
    | Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr, hlb, hlr => h_2 ls lk lv ll lr hlb hlr) =
    h_1 hlb hlr
-- Mathlib.Geometry.Manifold.Submersion
/-- If `f` is a submersion at `x`, its domain chart's target `(h.domChart.extend I).target`
is mapped to its codomain chart's target `(h.domChart.extend J).target`:
see `image_target_subset_target` for a version stated using images.  -/
Manifold.IsSubmersionAtOfComplement.target_subset_preimage_target : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : TopologicalSpace H] [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace H M] [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  {x : M} (h : Manifold.IsSubmersionAtOfComplement F I J n f x),
  (h.domChart.extend I).target ⊆ Prod.fst ∘ ⇑h.equiv ⁻¹' (h.codChart.extend J).target
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_sin_sq_mul_cos : ∀ {a b : ℝ}, ∫ (x : ℝ) in a..b, Real.sin x ^ 2 * Real.cos x = (Real.sin b ^ 3 - Real.sin a ^ 3) / 3
-- Mathlib.Algebra.Tropical.Basic
Tropical.instCommMonoidTropical : {R : Type u} → [AddCommMonoid R] → CommMonoid (Tropical R)
-- Init.Data.Sum.Basic
Sum.liftRel_inr_inr : ∀ {α : Type u_1} {γ : Type u_2} {r : α → γ → Prop} {β : Type u_3} {δ : Type u_4} {s : β → δ → Prop} {b : β} {d : δ},
  Sum.LiftRel r s (Sum.inr b) (Sum.inr d) ↔ s b d
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_bot : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {l : ℕ} {v : α → M} {xs : Fin l → M},
  ⊥.Realize v xs ↔ False
-- Mathlib.RingTheory.KrullDimension.Zero
/-- A quotient `R ⧸ I` has krull dimension at most zero if and only if all minimal primes over `I`
are maximal.  -/
Ideal.krullDimLE_zero_quotient_iff_forall_minimalPrimes_isMaximal : ∀ {R : Type u_2} [inst : CommRing R] {I : Ideal R}, Ring.KrullDimLE 0 (R ⧸ I) ↔ ∀ J ∈ I.minimalPrimes, J.IsMaximal
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.support_eq_empty : ∀ {R : Type u_1} [inst : Semiring R] {p : SkewPolynomial R}, p.support = ∅ ↔ p = 0
-- Mathlib.Data.Nat.Init
_private.Mathlib.Data.Nat.Init.0.Nat.pincerRecursion.match_1.eq_2 : ∀ (motive : ℕ → ℕ → Sort u_1) (n : ℕ) (h_1 : (m : ℕ) → motive m 0) (h_2 : (n : ℕ) → motive 0 n)
  (h_3 : (n n_1 : ℕ) → motive n.succ n_1.succ),
  (n = 0 → False) →
    (match 0, n with
      | m, 0 => h_1 m
      | 0, n => h_2 n
      | n.succ, n_1.succ => h_3 n n_1) =
      h_2 n
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.instHasCokernels : CategoryTheory.Limits.HasCokernels SemiNormedGrp
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.tensor_smul_right : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] {ρ : Representation A G V} {σ : Representation A G W}
  {τ : Representation A G U} {P : Type u_6} [inst_8 : AddCommMonoid P] [inst_9 : Module A P] {π : Representation A G P}
  (f : ρ.IntertwiningMap σ) (a : A) (g : τ.IntertwiningMap π), f.tensor (a • g) = a • f.tensor g
-- Mathlib.Analysis.Convex.Strict.Extreme
StrictConvex.sdiff_interior_subset_extremePoints : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid A]
  [inst_3 : Module 𝕜 A] [inst_4 : TopologicalSpace A] {C : Set A},
  StrictConvex 𝕜 C → C \ interior C ⊆ Set.extremePoints 𝕜 C
-- Mathlib.Tactic.DuplicateDecls
/-- Search for duplicate instances that aren't theorems.  -/
Mathlib.Tactic.DuplicateDecls.Target.instances : Mathlib.Tactic.DuplicateDecls.Target
-- Mathlib.Algebra.Star.Basic
/-- A commutative star monoid is a star module over its opposite via
`Monoid.toOppositeMulAction`.  -/
StarSemigroup.toOpposite_starModule : ∀ {R : Type u} [inst : CommMonoid R] [inst_1 : StarMul R], StarModule Rᵐᵒᵖ R
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.smul_bdd : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {𝕜 : Type u_8} [inst_1 : NormedRing 𝕜] [inst_2 : Module 𝕜 β] [IsBoundedSMul 𝕜 β] {f : α → β} {φ : α → 𝕜},
  MeasureTheory.Integrable φ μ →
    ∀ (C : ℝ), MeasureTheory.AEStronglyMeasurable f μ → (∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ C) → MeasureTheory.Integrable (φ • f) μ
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- The angle between two nonzero vectors is `θ` if and only if the second vector is the first
rotated by `θ` and scaled by a positive real.  -/
Orientation.oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V},
  x ≠ 0 → y ≠ 0 → ∀ (θ : Real.Angle), o.oangle x y = θ ↔ ∃ r, 0 < r ∧ y = r • (o.rotation θ) x
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
/-- An auxiliary definition for `liftHomotopyZero`.  -/
CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {Y Z : C} →
        {P : CategoryTheory.ProjectiveResolution Y} →
          {Q : CategoryTheory.ProjectiveResolution Z} →
            (f : P.complex ⟶ Q.complex) → CategoryTheory.CategoryStruct.comp f Q.π = 0 → (P.complex.X 0 ⟶ Q.complex.X 1)
-- Mathlib.Topology.Algebra.Affine
ContinuousWithinAt.lineMap : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : AddCommGroup V] [inst_1 : TopologicalSpace V]
  [inst_2 : AddTorsor V P] [inst_3 : TopologicalSpace P] [IsTopologicalAddTorsor P] [inst_5 : Ring R]
  [inst_6 : Module R V] [inst_7 : TopologicalSpace R] [ContinuousSMul R V] {X : Type u_6} [inst_9 : TopologicalSpace X]
  {f₁ f₂ : X → P} {g : X → R} {s : Set X} {x : X},
  ContinuousWithinAt f₁ s x →
    ContinuousWithinAt f₂ s x →
      ContinuousWithinAt g s x → ContinuousWithinAt (fun x => (AffineMap.lineMap (f₁ x) (f₂ x)) (g x)) s x
-- Mathlib.RepresentationTheory.Continuous.TopRep
/-- The top rep induced by the coinduced representation.  -/
TopRep.coind₁ : {k : Type u} →
  [inst : TopologicalSpace k] →
    [inst_1 : Ring k] →
      {G : Type v} →
        [inst_2 : Group G] → [inst_3 : TopologicalSpace G] → [IsTopologicalGroup G] → TopRep k G → TopRep k G
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
CategoryTheory.Limits.coconeOfCoconeFiberwiseColimit_ι_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {H : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} H]
  {G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H}
  [inst_2 :
    ∀ {X Y : C} (f : X ⟶ Y),
      CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))]
  (c : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.fiberwiseColimit G)) (X : CategoryTheory.Grothendieck F),
  (CategoryTheory.Limits.coconeOfCoconeFiberwiseColimit c).ι.app X =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Grothendieck.ι F X.base).comp G) X.fiber) (c.ι.app X.base)
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- In a complete space `E`, the projection maps onto a complete subspace `K` and its orthogonal
complement sum to the identity.  -/
Submodule.id_eq_sum_starProjection_self_orthogonalComplement : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection],
  ContinuousLinearMap.id 𝕜 E = K.starProjection + Kᗮ.starProjection
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.homogenize_smul : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : Semiring S] [inst_2 : Module S R] (c : S)
  (p : Polynomial R) (n : ℕ), (c • p).homogenize n = c • p.homogenize n
-- Mathlib.Combinatorics.Colex
/-- `𝒜` is an initial segment of the colexicographic order on sets of `r`, and that if `t` is below
`s` in colex where `t` has size `r` and `s` is in `𝒜`, then `t` is also in `𝒜`. In effect, `𝒜` is
downwards closed with respect to colex among sets of size `r`.  -/
Finset.Colex.IsInitSeg : {α : Type u_1} → [LinearOrder α] → Finset (Finset α) → ℕ → Prop
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.beqModel_eq_true_of_perm : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] [inst_2 : BEq β] [ReflBEq β] {l₁ l₂ : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l₁ → l₁.Perm l₂ → Std.Internal.List.Const.beqModel l₁ l₂ = true
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : Add α] [inst_4 : Add β] [inst_5 : Add γ] {g : α ≃+o β} {f₁ f₂ : β ≃+o γ},
  Function.Surjective ⇑g → (g.trans f₁ = g.trans f₂ ↔ f₁ = f₂)
-- Mathlib.NumberTheory.NumberField.Ideal.Basic
/-- If the norm of the (nonzero) prime ideal `P` is coprime with the order of the torsion of `K`, then
the norm of `P` is congruent to `1` modulo `torsionOrder K`.
 -/
NumberField.torsionOrder_dvd_absNorm_sub_one : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {P : Ideal (NumberField.RingOfIntegers K)},
  P ≠ ⊥ →
    P.IsPrime →
      (Ideal.absNorm P).Coprime (NumberField.Units.torsionOrder K) →
        NumberField.Units.torsionOrder K ∣ Ideal.absNorm P - 1
-- Mathlib.Algebra.Lie.Subalgebra
/-- The embedding of a Lie subalgebra into the ambient space as a morphism of Lie modules.  -/
LieSubalgebra.incl' : {R : Type u} →
  {L : Type v} →
    [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → (L' : LieSubalgebra R L) → ↥L' →ₗ⁅R,↥L'⁆ L
-- Mathlib.NumberTheory.HeckeRing.Defs
HeckeCosetModule.instAddCommMonoid : {G : Type u_1} →
  [inst : Group G] →
    (Δ : Submonoid G) →
      (H₁ H₂ : Subgroup G) → (Z : Type u_2) → [inst_1 : AddCommMonoid Z] → AddCommMonoid (HeckeCosetModule Δ H₁ H₂ Z)
-- Mathlib.Data.List.Chain
List.IsChain.concat_induction : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α} (p : α → Prop) (l : List α),
  List.IsChain r (l ++ [b]) → (l ++ [b]).head ⋯ = a → (∀ ⦃x y : α⦄, r x y → p x → p y) → p a → ∀ i ∈ l ++ [b], p i
-- Mathlib.Algebra.Order.Group.Equiv
symm_toLexAddEquiv : ∀ (α : Type u_1) [inst : Add α], (toLexAddEquiv α).symm = ofLexAddEquiv α
-- Mathlib.Topology.MetricSpace.Bounded
Bornology.IsBounded.subset_closedBall_lt : ∀ {α : Type u} {s : Set α} [inst : PseudoMetricSpace α],
  Bornology.IsBounded s → ∀ (a : ℝ) (c : α), ∃ r, a < r ∧ s ⊆ Metric.closedBall c r
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.lift_extend : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F] (c : CategoryTheory.Limits.Cone F)
  {X : C} (f : X ⟶ c.pt),
  CategoryTheory.Limits.limit.lift F (c.extend f) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.limit.lift F c)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.forMUncurried_eq_forM_toList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m' : Type w → Type w'} {β : Type v} {m : Std.DHashMap α fun x => β}
  [inst : Monad m'] [LawfulMonad m'] {f : α × β → m' PUnit.{w + 1}},
  Std.DHashMap.Const.forMUncurried f m = (Std.DHashMap.Const.toList m).forM f
-- Lean.Meta.Tactic.FVarSubst
Lean.Meta.instInhabitedFVarSubst : Inhabited Lean.Meta.FVarSubst
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.map_rightUnitor_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X : C),
  F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.LaxMonoidal.ε F))
        (CategoryTheory.Functor.LaxMonoidal.μ F X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
_private.Mathlib.Analysis.SpecialFunctions.Gamma.Basic.0.Complex.GammaAux.eq_2 : ∀ (n : ℕ), Complex.GammaAux✝ n.succ = fun s => Complex.GammaAux✝ n (s + 1) / s
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.zero_bind : ∀ {α β : Type u} (f : α → FreeAbelianGroup β), 0 >>= f = 0
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- In a topological vector space, the addition of a simple function and a measurable function is
measurable.  -/
Measurable.simpleFunc_add : ∀ {α : Type u_1} {E : Type u_5} {x : MeasurableSpace α} [inst : MeasurableSpace E] [inst_1 : AddCancelMonoid E]
  [MeasurableAdd E] {g : α → E}, Measurable g → ∀ (f : MeasureTheory.SimpleFunc α E), Measurable (⇑f + g)
-- Init.Data.Vector.Lemmas
Vector.toList_eraseIdx! : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ}, i < n → (xs.eraseIdx! i).toList = xs.toList.eraseIdx i
-- Mathlib.Topology.Path
Path.ofLine_mem : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {f : ℝ → X} (hf : ContinuousOn f unitInterval) (h₀ : f 0 = x)
  (h₁ : f 1 = y) (t : ↑unitInterval), (Path.ofLine hf h₀ h₁) t ∈ f '' unitInterval
-- Mathlib.CategoryTheory.Adjunction.Reflective
/-- The description of the inverse of the bijection `unitCompPartialBijectiveAux`.  -/
CategoryTheory.unitCompPartialBijectiveAux_symm_apply : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {i : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Reflective i] {A : C} {B : D}
  (f : i.obj ((CategoryTheory.reflector i).obj A) ⟶ i.obj B),
  (CategoryTheory.unitCompPartialBijectiveAux A B).symm f =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.reflectorAdjunction i).unit.app A) f
-- Mathlib.CategoryTheory.Limits.ExactFunctor
/-- `C ⥤ₑ D` denotes exact functors `C ⥤ D`  -/
CategoryTheory.«term_⥤ₑ_» : Lean.TrailingParserDescr
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
/-- A bounded continuous function is in `L∞`.  -/
BoundedContinuousFunction.memLp_top : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace α]
  [BorelSpace α] [inst_2 : NormedAddCommGroup E] [SecondCountableTopologyEither α E]
  (f : BoundedContinuousFunction α E), MeasureTheory.MemLp ⇑f ⊤ μ
-- Lean.Elab.Tactic.Conv.Basic
Lean.Elab.Tactic.Conv.evalZeta : Lean.Elab.Tactic.Tactic
-- Mathlib.Algebra.Polynomial.RingDivision
/-- The multiplicity of `a` as root of `(X - a) ^ n` is `n`.  -/
Polynomial.rootMultiplicity_X_sub_C_pow : ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] (a : R) (n : ℕ),
  Polynomial.rootMultiplicity a ((Polynomial.X - Polynomial.C a) ^ n) = n
-- Mathlib.Algebra.Category.ModuleCat.Basic
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
ModuleCat.Hom.Simps.hom : {R : Type u} → [inst : Ring R] → (A B : ModuleCat R) → A.Hom B → ↑A →ₗ[R] ↑B
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.mapDomainOfBialgHom_id : ∀ {R : Type u_1} {G : Type u_5} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : Group G],
  MonoidAlgebra.mapDomainOfBialgHom (BialgHom.id R (MonoidAlgebra R G)) = MonoidHom.id G
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.freeAddGroupEmptyEquivAddUnit.eq_1 : FreeAddGroup.freeAddGroupEmptyEquivAddUnit = Equiv.ofUnique (FreeAddGroup Empty) Unit
-- Mathlib.MeasureTheory.Measure.Hausdorff
AntilipschitzWith.le_hausdorffMeasure_image : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] [inst_2 : MeasurableSpace X]
  [inst_3 : BorelSpace X] [inst_4 : MeasurableSpace Y] [inst_5 : BorelSpace Y] {f : X → Y} {K : NNReal} {d : ℝ},
  AntilipschitzWith K f →
    0 ≤ d →
      ∀ (s : Set X),
        (MeasureTheory.Measure.hausdorffMeasure d) s ≤ ↑K ^ d * (MeasureTheory.Measure.hausdorffMeasure d) (f '' s)
-- Lean.Data.JsonRpc
Lean.JsonRpc.Request.mk.injEq : ∀ {α : Type u} (id : Lean.JsonRpc.RequestID) (method : String) (param : α) (id_1 : Lean.JsonRpc.RequestID)
  (method_1 : String) (param_1 : α),
  ({ id := id, method := method, param := param } = { id := id_1, method := method_1, param := param_1 }) =
    (id = id_1 ∧ method = method_1 ∧ param = param_1)
-- Init.Data.SInt.Lemmas
Int32.toInt64_ne_minValue : ∀ (a : Int32), a.toInt64 ≠ Int64.minValue
-- Mathlib.Analysis.Complex.Trigonometric
Complex.tanh_neg : ∀ (x : ℂ), Complex.tanh (-x) = -Complex.tanh x
-- Std.Time.Format.Modifier
/-- `q`: Stand-alone quarter of year as number or text (e.g., 3, 03, Q3, 3rd quarter).
Stand-alone means the value is used independently (e.g., a calendar header) rather than as part of a full date phrase.
In practice the output is the same as `Q`; the distinction is meaningful only in locale-aware contexts.
 -/
Std.Time.Modifier.q : Std.Time.Number ⊕ Std.Time.Text → Std.Time.Modifier
-- Mathlib.Order.FixedPoints
OrderHom.map_sInf_subset_fixedPoints_le : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α), ∀ A ⊆ Function.fixedPoints ⇑f, f (sInf A) ≤ sInf A
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.map_eq_one_iff : ∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R ≃+* S) {x : R},
  f x = 1 ↔ x = 1
-- Mathlib.Topology.Category.TopCat.Basic
/-- Turn a morphism in `TopCat` back into a `ContinuousMap`.  -/
TopCat.Hom.hom : {X Y : TopCat} → X.Hom Y → C(↑X, ↑Y)
-- Mathlib.Data.List.Basic
List.reverse_perm' : ∀ {α : Type u} {l₁ l₂ : List α}, l₁.reverse.Perm l₂ ↔ l₁.Perm l₂
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.basis_singleton : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {v : ι → F} (i : ι),
  Lagrange.basis {i} v i = 1
-- Mathlib.Data.List.PeriodicityLemma
List.hasPeriod_empty : ∀ {α : Type u_1} (p : ℕ), [].HasPeriod p
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.C_addPolynomial_slope : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ x₂ y₁ y₂ : F},
  W.Equation x₁ y₁ →
    W.Equation x₂ y₂ →
      ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂) →
        (WeierstrassCurve.Affine.CoordinateRing.mk W) (Polynomial.C (W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) =
          -(WeierstrassCurve.Affine.CoordinateRing.XClass W x₁ * WeierstrassCurve.Affine.CoordinateRing.XClass W x₂ *
              WeierstrassCurve.Affine.CoordinateRing.XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)))
-- Mathlib.MeasureTheory.Measure.Real
/-- **Alias** of `MeasureTheory.measureReal_sdiff_null`. -/
MeasureTheory.measureReal_diff_null : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α},
  μ.real s₂ = 0 → autoParam (μ s₂ ≠ ⊤) MeasureTheory.measureReal_sdiff_null._auto_1 → μ.real (s₁ \ s₂) = μ.real s₁
-- Mathlib.Order.DirSupClosed
DirSupInacc.dirSupInaccOn : ∀ {α : Type u_1} {s : Set α} {D : Set (Set α)} [inst : Preorder α], DirSupInacc s → DirSupInaccOn D s
-- Aesop.Tree.TreeM
Aesop.getRootMVarCluster : Aesop.TreeM Aesop.MVarClusterRef
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
/-- The valuation subring of a valued field is clopen.  -/
Valued.isClopen_valuationSubring : ∀ {Γ₀ : Type v} [inst : LinearOrderedCommGroupWithZero Γ₀] (K : Type u) [inst_1 : Field K] [hv : Valued K Γ₀],
  IsClopen ↑Valued.v.valuationSubring
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instNonUnitalRing : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : NonUnitalRing β] → [IsTopologicalRing β] → NonUnitalRing (ZeroAtInftyContinuousMap α β)
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- The inner product with values in `ℂ`.  -/
ComplexInnerProductSpace.«term⟪_,_⟫» : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.iso_isometry_of_normNoninc : ∀ {V W : SemiNormedGrp} (i : V ≅ W),
  (SemiNormedGrp.Hom.hom i.hom).NormNoninc →
    (SemiNormedGrp.Hom.hom i.inv).NormNoninc → Isometry ⇑(CategoryTheory.ConcreteCategory.hom i.hom)
-- Mathlib.Algebra.Central.End
Module.End.mem_subsemiringCenter_iff : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  {f : Module.End R M},
  f ∈ Subsemiring.center (Module.End R M) ↔ ∃ α, ∃ (hα : α ∈ Subsemiring.center R), f = Module.End.smulLeft α hα
-- Init.Omega.Constraint
Lean.Omega.bmod_coeffs.eq_1 : ∀ (m i : ℕ) (x : Lean.Omega.Coeffs), Lean.Omega.bmod_coeffs m i x = (x.bmod m).set i ↑m
-- Mathlib.Order.Circular
Set.cIcc.eq_1 : ∀ {α : Type u_1} [inst : CircularPreorder α] (a b : α), Set.cIcc a b = {x | btw a x b}
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.Bivariate.swap_symm : ∀ {R : Type u_1} [inst : CommSemiring R], Polynomial.Bivariate.swap.symm = Polynomial.Bivariate.swap
-- Lean.Elab.ConfigEval.Types
/-- Evaluates setting the configuration item described by `item` in `config`.
 -/
Lean.Elab.ConfigEval.EvalConfigItem.set : {α : Type} → Lean.Elab.ConfigEval.EvalConfigItem α → α → Lean.Elab.ConfigEval.ConfigItem → Lean.Elab.TermElabM α
-- Init.GetElem
getElem_congr_idx : ∀ {coll : Type u_1} {idx : Type u_2} {elem : Type u_3} {valid : coll → idx → Prop} [inst : GetElem coll idx elem valid]
  {c : coll} {i j : idx} {w : valid c i} (h' : i = j), c[i] = c[j]
-- Init.SimpLemmas
or_assoc : ∀ {a b c : Prop}, (a ∨ b) ∨ c ↔ a ∨ b ∨ c
-- Mathlib.RingTheory.Length
Module.length_prod : ∀ (R : Type u_1) (M : Type u_2) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Type u_3)
  [inst_3 : AddCommGroup N] [inst_4 : Module R N], Module.length R (M × N) = Module.length R M + Module.length R N