mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
ContinuousOn.clog : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℂ} {s : Set α},
  ContinuousOn f s → (∀ x ∈ s, f x ∈ Complex.slitPlane) → ContinuousOn (fun t => Complex.log (f t)) s
-- Std.Internal.UV.Signal
_private.Std.Internal.UV.Signal.0.Std.Internal.UV.SignalImpl : NonemptyType
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_insertMany_list : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α},
  k ∈ t.insertMany l ↔ k ∈ t ∨ (List.map Prod.fst l).contains k = true
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.coe_mulₗᵢ : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (R : Type u_3) [inst_1 : NonUnitalSeminormedRing R]
  [inst_2 : NormedSpace 𝕜 R] [inst_3 : IsScalarTower 𝕜 R R] [inst_4 : SMulCommClass 𝕜 R R]
  [inst_5 : RegularNormedAlgebra 𝕜 R], ⇑(ContinuousLinearMap.mulₗᵢ 𝕜 R) = ⇑(ContinuousLinearMap.mul 𝕜 R)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness
/-- Bird's principal minor `f[α, α]`.  -/
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness.0.BirdDet.pminor : {R : Type u_1} → [CommRing R] → {n : ℕ} → Matrix (Fin n) (Fin n) R → {p : ℕ} → (Fin p → Fin n) → R
-- Init.Data.UInt.Lemmas
UInt8.toUInt16_ofNatClamp_of_le : ∀ {n : ℕ},
  UInt8.size ≤ n →
    (UInt8.ofNatClamp n).toUInt16 = UInt16.ofNatLT (UInt8.size - 1) UInt8.toUInt16_ofNatClamp_of_le._proof_1
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
/-- Given the existence of the appropriate (possibly finite) products and equalizers,
we can construct a limit cone for `F`.
(This assumes the existence of all equalizers, which is technically stronger than needed.)
 -/
CategoryTheory.Limits.limitConeOfEqualizerAndProduct : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.SmallCategory J] →
        (F : CategoryTheory.Functor J C) →
          [CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor F.obj)] →
            [CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor fun f => F.obj f.fst.2)] →
              [CategoryTheory.Limits.HasEqualizers C] → CategoryTheory.Limits.LimitCone F
-- Mathlib.RingTheory.Filtration
Ideal.stableFiltration_stable : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R)
  (N : Submodule R M), (I.stableFiltration N).Stable
-- Mathlib.Topology.EMetricSpace.Defs
Metric.eball_subset : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {ε₁ ε₂ : ENNReal},
  edist x y + ε₁ ≤ ε₂ → edist x y ≠ ⊤ → Metric.eball x ε₁ ⊆ Metric.eball y ε₂
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] [inst_1 : Inhabited α] {f : (a : α) → β a → Option (γ a)} {k : α},
  (Std.ExtDHashMap.filterMap f m).getKey! k = ((m.getKey? k).pfilter fun x_2 h' => (f x_2 (m.get x_2 ⋯)).isSome).get!
-- Mathlib.Tactic.FieldSimp
Mathlib.Tactic.FieldSimp.DenomCondition.positive.inj : ∀ {v : Lean.Level} {M : Q(Type v)} {iM : Q(GroupWithZero «$M»)} {iM' : Q(PartialOrder «$M»)}
  {iM'' : Q(PosMulStrictMono «$M»)} {iM''' : Q(PosMulReflectLT «$M»)} {iM'''' : Q(ZeroLEOneClass «$M»)}
  {iM'_1 : Q(PartialOrder «$M»)} {iM''_1 : Q(PosMulStrictMono «$M»)} {iM'''_1 : Q(PosMulReflectLT «$M»)}
  {iM''''_1 : Q(ZeroLEOneClass «$M»)},
  Mathlib.Tactic.FieldSimp.DenomCondition.positive iM' iM'' iM''' iM'''' =
      Mathlib.Tactic.FieldSimp.DenomCondition.positive iM'_1 iM''_1 iM'''_1 iM''''_1 →
    iM' = iM'_1 ∧ iM'' = iM''_1 ∧ iM''' = iM'''_1 ∧ iM'''' = iM''''_1
-- Mathlib.Probability.Kernel.WithDensity
ProbabilityTheory.Kernel.withDensity_add_left : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ η : ProbabilityTheory.Kernel α β)
  [inst : ProbabilityTheory.IsSFiniteKernel κ] [inst_1 : ProbabilityTheory.IsSFiniteKernel η] (f : α → β → ENNReal),
  (κ + η).withDensity f = κ.withDensity f + η.withDensity f
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- Shortcut lemma for `Matrix.toLin_mul` and `LinearMap.comp_apply`.  -/
Matrix.toLin_mul_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {l : Type u_2} {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n]
  [inst_2 : DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : Module R M₁] [inst_6 : Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂)
  [inst_7 : Fintype m] {M₃ : Type u_7} [inst_8 : AddCommMonoid M₃] [inst_9 : Module R M₃] (v₃ : Module.Basis l R M₃)
  [inst_10 : Finite l] [inst_11 : DecidableEq m] (A : Matrix l m R) (B : Matrix m n R) (x : M₁),
  ((Matrix.toLin v₁ v₃) (A * B)) x = ((Matrix.toLin v₂ v₃) A) (((Matrix.toLin v₁ v₂) B) x)
-- Mathlib.Order.BooleanAlgebra.Defs
BooleanAlgebra.toTop : {α : Type u} → [self : BooleanAlgebra α] → Top α
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.coe_top : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G], ↑⊤ = Set.univ
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.canonical_right_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
  (CategoryTheory.ShortComplex.HomologyData.canonical S).right.ι = S.homologyι
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.property_pure : ∀ {m : Type w → Type w'} [inst : Monad m] {α : Type w} {x : α}, (pure x).Property = fun x_1 => x = x_1
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toLinearMap_neg : ∀ {R : Type u_1} [inst : Ring R] {R₂ : Type u_2} [inst_1 : Ring R₂] {M : Type u_4} [inst_2 : TopologicalSpace M]
  [inst_3 : AddCommGroup M] {M₂ : Type u_5} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommGroup M₂]
  [inst_6 : Module R M] [inst_7 : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst_8 : IsTopologicalAddGroup M₂]
  (f : M →SL[σ₁₂] M₂), ↑(-f) = -↑f
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.toCone_π_app : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F)
  (j : CategoryTheory.Discrete J), B.toCone.π.app j = B.π j.as
-- Mathlib.Algebra.Lie.Basic
LieHom.instFunLike : {R : Type u} →
  {L₁ : Type v} →
    {L₂ : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L₁] →
          [inst_2 : LieAlgebra R L₁] → [inst_3 : LieRing L₂] → [inst_4 : LieAlgebra R L₂] → FunLike (L₁ →ₗ⁅R⁆ L₂) L₁ L₂
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key in the tree map, returning `fallback` if
the tree map is empty.
 -/
Std.ExtDTreeMap.Const.minEntryD : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → [Std.TransCmp cmp] → Std.ExtDTreeMap α (fun x => β) cmp → α × β → α × β
-- Mathlib.Analysis.Convolution
MeasureTheory.support_convolution_subset_swap : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : NormedSpace ℝ F]
  [inst_9 : AddGroup G], Function.support (MeasureTheory.convolution f g L μ) ⊆ Function.support g + Function.support f
-- Mathlib.Algebra.Group.TypeTags.Basic
Multiplicative.commMonoid : {α : Type u} → [AddCommMonoid α] → CommMonoid (Multiplicative α)
-- Lean.Elab.PreDefinition.TerminationHint
/-- A single `decreasing_by` clause  -/
Lean.Elab.DecreasingBy : Type
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- Each local frame `{sᵢ} ∈ Γ(E)` of a `C^k` vector bundle, defined by a local trivialisation `e`,
is `C^k` on `e.baseSet`.  -/
Bundle.Trivialization.contMDiffOn_localFrame_baseSet : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] (n : WithTop ℕ∞) {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V]
  [ContMDiffVectorBundle n F V I] {ι : Type u_7} (e : Bundle.Trivialization F Bundle.TotalSpace.proj)
  [inst_15 : MemTrivializationAtlas e] (b : Module.Basis ι 𝕜 F) (i : ι),
  ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, e.localFrame b i x⟩) e.baseSet
-- Mathlib.Topology.VectorBundle.Riemannian
Bundle.RiemannianBundle.mk : {B : Type u_4} →
  {E : B → Type u_6} →
    [inst : (b : B) → TopologicalSpace (E b)] →
      [inst_1 : (b : B) → AddCommGroup (E b)] →
        [inst_2 : (b : B) → Module ℝ (E b)] → Bundle.RiemannianMetric E → Bundle.RiemannianBundle E
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  [inst_1 : Inhabited α] {k k' : α} {f : β k → β k},
  (m.modify k f).getKey! k' = if (k == k') = true then if k ∈ m then k else default else m.getKey! k'
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroupClass.sub.eq_1 : ∀ {G : Type u_5} {S : Type u_6} [inst : SubNegMonoid G] [inst_1 : SetLike S G] [inst_2 : AddSubgroupClass S G] {H : S},
  AddSubgroupClass.sub = { sub := fun a b => ⟨↑a - ↑b, ⋯⟩ }
-- Mathlib.Order.Hom.PowersetCard
Set.powersetCard.ofFinEmbEquiv_apply : ∀ {n : ℕ} {I : Type u_1} [inst : LinearOrder I] (f : Fin n ↪o I),
  Set.powersetCard.ofFinEmbEquiv f = Set.powersetCard.ofFinEmb n I f.toEmbedding
-- Init.Data.Iterators.Lemmas.Combinators.Attach
Std.Iter.attachWith.congr_simp : ∀ {α β : Type w} [inst : Std.Iterator α Id β] (it it_1 : Std.Iter β) (e_it : it = it_1) (P : β → Prop)
  (h : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out), it.attachWith P h = it_1.attachWith P ⋯
-- Mathlib.LinearAlgebra.BilinearMap
/-- **Alias** of `LinearMap.lsmul_eq_distribSMultoLinearMap`. -/
LinearMap.lsmul_eq_DistribMulAction_toLinearMap : ∀ {R : Type u_2} [inst : CommSemiring R] (M : Type u_5) [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (r : R),
  (LinearMap.lsmul R M) r = DistribSMul.toLinearMap R M r
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.coe_toBoundedContinuousFunction : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞} (f : TestFunction Ω F n),
  ⇑{ toFun := ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ } = ⇑f
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)),
  CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor.obj P =
    CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj P
-- Mathlib.Data.Finset.Lattice.Fold
/-- **Alias** of `Finset.apply_inf_eq_inf_comp`. -/
Finset.comp_inf_eq_inf_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeInf α] [inst_1 : OrderTop α]
  [inst_2 : SemilatticeInf γ] [inst_3 : OrderTop γ] {s : Finset β} {f : β → α} (g : α → γ),
  (∀ (x y : α), g (x ⊓ y) = g x ⊓ g y) → g ⊤ = ⊤ → g (s.inf f) = s.inf (g ∘ f)
-- Mathlib.Analysis.Convex.Deriv
bddAbove_slope_gt_of_mem_interior : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} {x : 𝕜}
  [inst_3 : TopologicalSpace 𝕜] [OrderTopology 𝕜],
  ConvexOn 𝕜 s f → x ∈ interior s → BddAbove (slope f x '' {y | y ∈ s ∧ y < x})
-- Init.System.CancelToken
IO.instNonemptyCancelToken : Nonempty IO.CancelToken
-- Mathlib.LinearAlgebra.Matrix.Rank
/-- The rank of a matrix is the rank of the space spanned by its rows.  -/
Matrix.rank_eq_finrank_span_row : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Fintype n] [inst_1 : Field R] [Finite m] (A : Matrix m n R),
  A.rank = Module.finrank R ↥(Submodule.span R (Set.range A.row))
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
Std.IterM.toArray_flatMapAfter : ∀ {α α₂ β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α m β] [inst_5 : Std.Iterator α₂ m γ] [Std.Iterators.Finite α m]
  [Std.Iterators.Finite α₂ m] {f : β → Std.IterM m γ} {it₁ : Std.IterM m β} {it₂ : Option (Std.IterM m γ)},
  (Std.IterM.flatMapAfter f it₁ it₂).toArray =
    match it₂ with
    | none => Array.flatten <$> (Std.IterM.mapM (fun b => (f b).toArray) it₁).toArray
    | some it₂ => do
      let __do_lift ← it₂.toArray
      let __do_lift_1 ← Array.flatten <$> (Std.IterM.mapM (fun b => (f b).toArray) it₁).toArray
      pure (__do_lift ++ __do_lift_1)
-- Init.Data.BitVec.Lemmas
BitVec.toInt_signExtend_eq_toInt_bmod_of_le : ∀ {w v : ℕ} (x : BitVec w), v ≤ w → (BitVec.signExtend v x).toInt = x.toInt.bmod (2 ^ v)
-- Mathlib.Topology.Algebra.Module.Equiv
/-- Continuous linear equivalence between dependent functions `(i : Fin 2) → M i` and `M 0 × M 1`.
 -/
ContinuousLinearEquiv.piFinTwo : (R : Type u_2) →
  [inst : Semiring R] →
    (M : Fin 2 → Type u_4) →
      [inst_1 : (i : Fin 2) → AddCommMonoid (M i)] →
        [inst_2 : (i : Fin 2) → Module R (M i)] →
          [inst_3 : (i : Fin 2) → TopologicalSpace (M i)] → ((i : Fin 2) → M i) ≃L[R] M 0 × M 1
-- Mathlib.RingTheory.Perfectoid.FontaineTheta
WittVector.quotEquivOfEq_ghostComponentModPPow : ∀ {R : Type u} [inst : CommRing R] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] (x : WittVector p (R ⧸ Ideal.span {↑p}))
  (h : Ideal.span {↑p} ^ (0 + 1) = Ideal.span {↑p}),
  (Ideal.quotEquivOfEq h) ((WittVector.ghostComponentModPPow 0) x) = (WittVector.ghostComponent 0) x
-- Init.Data.Int.Order
Int.le_sub_one_of_lt : ∀ {a b : ℤ}, a < b → a ≤ b - 1
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.Except.toBool.match_1.eq_1 : ∀ {ε : Type u_1} {α : Type u_2} (motive : Except ε α → Sort u_3) (a : α) (h_1 : (a : α) → motive (Except.ok a))
  (h_2 : (a : ε) → motive (Except.error a)),
  (match Except.ok a with
    | Except.ok a => h_1 a
    | Except.error a => h_2 a) =
    h_1 a
-- Std.Data.TreeMap.Basic
/-- Returns a list of all values present in the tree map in ascending  order.  -/
Std.TreeMap.values : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → List β
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.minKey!_modify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {f : β → β},
  Std.ExtDTreeMap.Const.modify t k f ≠ ∅ →
    (Std.ExtDTreeMap.Const.modify t k f).minKey! = if cmp t.minKey! k = Ordering.eq then k else t.minKey!
-- Init.Data.UInt.Lemmas
UInt8.toBitVec_toUSize : ∀ (n : UInt8), n.toUSize.toBitVec = BitVec.setWidth System.Platform.numBits n.toBitVec
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_rco_append_toArray_rco : ∀ {l m n : ℤ}, l ≤ m → m ≤ n → (l...m).toArray ++ (m...n).toArray = (l...n).toArray
-- Init.Data.SInt.Lemmas
Int16.toNatClampNeg_ofNat_of_lt : ∀ {n : ℕ}, n < 2 ^ 15 → (Int16.ofNat n).toNatClampNeg = n
-- Mathlib.RingTheory.DualNumber
DualNumber.instIsLocalRing : ∀ {K : Type u_2} [inst : DivisionRing K], IsLocalRing (DualNumber K)
-- Mathlib.LinearAlgebra.Projection
Submodule.projectionOnto_apply_left : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (h : IsCompl p q) (x : ↥p), (p.projectionOnto q h) ↑x = x
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.semilinearMapAddEquiv_symm_apply_apply : ∀ {R : Type u₁} {S : Type u₂} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) (M : ModuleCat R) (N : ModuleCat S)
  (g : M ⟶ (ModuleCat.restrictScalars f).obj N) (a : ↑M),
  ((ModuleCat.semilinearMapAddEquiv f M N).symm g) a = (CategoryTheory.ConcreteCategory.hom g) a
-- Mathlib.GroupTheory.Congruence.Hom
/-- The kernel of the natural homomorphism from an `AddMonoid` to its
quotient by an additive congruence relation `c` equals `c`.  -/
AddCon.mk'_ker : ∀ {M : Type u_1} [inst : AddZeroClass M] (c : AddCon M), AddCon.ker c.mk' = c
-- Mathlib.Order.Nucleus
Nucleus.mk.inj : ∀ {X : Type u_2} {inst : SemilatticeInf X} {toInfHom : InfHom X X}
  {idempotent' : ∀ (x : X), toInfHom.toFun (toInfHom.toFun x) ≤ toInfHom.toFun x}
  {le_apply' : ∀ (x : X), x ≤ toInfHom.toFun x} {toInfHom_1 : InfHom X X}
  {idempotent'_1 : ∀ (x : X), toInfHom_1.toFun (toInfHom_1.toFun x) ≤ toInfHom_1.toFun x}
  {le_apply'_1 : ∀ (x : X), x ≤ toInfHom_1.toFun x},
  { toInfHom := toInfHom, idempotent' := idempotent', le_apply' := le_apply' } =
      { toInfHom := toInfHom_1, idempotent' := idempotent'_1, le_apply' := le_apply'_1 } →
    toInfHom = toInfHom_1
-- Lean.Data.Options
Lean.Option.name : {α : Type} → Lean.Option α → Lean.Name
-- Mathlib.Topology.Defs.Filter
/-- We say that a topological space is a *weakly locally compact space*,
if each point of this space admits a compact neighborhood.  -/
WeaklyLocallyCompactSpace : (X : Type u_3) → [TopologicalSpace X] → Prop
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.leftUnitor.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.Center C),
  X.leftUnitor =
    CategoryTheory.Center.isoMk { f := (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.fst).hom, comm := ⋯ }
-- Mathlib.Topology.Algebra.IsUniformGroup.Constructions
Pi.instIsUniformGroup : ∀ {ι : Type u_4} {G : ι → Type u_5} [inst : (i : ι) → UniformSpace (G i)] [inst_1 : (i : ι) → Group (G i)]
  [∀ (i : ι), IsUniformGroup (G i)], IsUniformGroup ((i : ι) → G i)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.instLinearOrderedCommMonoidWithZero : {α : Type u_1} →
  [inst : CommMonoid α] →
    [inst_1 : LinearOrder α] → [IsOrderedCancelMonoid α] → LinearOrderedCommMonoidWithZero (WithZero α)
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.mem_set_normalizer_iff' : ∀ {G : Type u_1} [inst : Group G] {S : Set G} {g : G}, g ∈ Subgroup.normalizer S ↔ ∀ (h : G), h * g ∈ S ↔ g * h ∈ S
-- Std.Data.TreeMap.Raw.Basic
Std.TreeMap.Raw.empty_eq_emptyc : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering}, Std.TreeMap.Raw.empty = ∅
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.dimension.eq_1 : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Presentation R S ι σ), P.dimension = Nat.card ι - Nat.card σ
-- Mathlib.Data.ENat.Basic
ENat.natCast_toNat_le_self : ∀ (n : ℕ∞), ↑n.toNat ≤ n
-- Mathlib.GroupTheory.QuotientGroup.Defs
/-- Note: `range_mk'` is a lemma about the primed constructor `QuotientGroup.mk'`, not a
modified version of some `range_mk`.  -/
QuotientGroup.range_mk' : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [nN : N.Normal], (QuotientGroup.mk' N).range = ⊤
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.colimIsoFlipCompWhiskerColim_hom_app_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C]
  (X : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X_1 : K),
  (CategoryTheory.Limits.colimIsoFlipCompWhiskerColim.hom.app X).app X_1 =
    (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation X X_1).hom
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Presieve.CoverByImageStructure.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {G : CategoryTheory.Functor C D} →
          {V U : D} →
            {f : V ⟶ U} →
              (obj : C) →
                (lift : V ⟶ G.obj obj) →
                  (map : G.obj obj ⟶ U) →
                    autoParam (CategoryTheory.CategoryStruct.comp lift map = f)
                        CategoryTheory.Presieve.CoverByImageStructure.fac._autoParam →
                      CategoryTheory.Presieve.CoverByImageStructure G f
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkCoyonedaObjObjEquiv_symm_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X Y Y' : C}
  (g : Y' ⟶ Y) (f : Y ⟶ X),
  CategoryTheory.shrinkCoyonedaObjObjEquiv.symm (CategoryTheory.CategoryStruct.comp g f) =
    (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkCoyoneda.{w, v, u}.obj (Opposite.op Y')).map f))
      (CategoryTheory.shrinkCoyonedaObjObjEquiv.symm g)
-- Mathlib.AlgebraicGeometry.Gluing
/-- The gluing as sheafed spaces is isomorphic to the gluing as presheafed spaces.  -/
AlgebraicGeometry.Scheme.GlueData.isoLocallyRingedSpace : (D : AlgebraicGeometry.Scheme.GlueData) → D.glued.toLocallyRingedSpace ≅ D.toLocallyRingedSpaceGlueData.glued
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.vadd_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {R : Type u_4} [inst_1 : VAdd R Y] (r : R)
  (f : LocallyConstant X Y) (x : X), (r +ᵥ f) x = r +ᵥ f x
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- The multiplicity of `p : ℕ` in `a : ℤ` is finite exactly when `a ≠ 0`.  -/
padicValRat.finite_int_prime_iff : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {a : ℤ}, FiniteMultiplicity (↑p) a ↔ a ≠ 0
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.fromArrowArrowFunctor_obj_f₁₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)),
  (CategoryTheory.Square.fromArrowArrowFunctor.obj f).f₁₂ = CategoryTheory.Arrow.Hom.left f.hom
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.Zipper.step.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β) → Sort u_3)
  (k : α) (v : β) (h_1 : Unit → motive Lean.PersistentHashMap.Entry.null)
  (h_2 : (k : α) → (v : β) → motive (Lean.PersistentHashMap.Entry.entry k v))
  (h_3 : (node : Lean.PersistentHashMap.Node α β) → motive (Lean.PersistentHashMap.Entry.ref node)),
  (match Lean.PersistentHashMap.Entry.entry k v with
    | Lean.PersistentHashMap.Entry.null => h_1 ()
    | Lean.PersistentHashMap.Entry.entry k v => h_2 k v
    | Lean.PersistentHashMap.Entry.ref node => h_3 node) =
    h_2 k v
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.singleton_X : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T) (x : PUnit.{w + 1}),
  (CategoryTheory.PreZeroHypercover.singleton f).X x = S
-- Lean.Parser.Command
Lean.Parser.Command.partial.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.instNonUnitalCommRing : {R : Type u} →
  [inst : CommSemiring R] →
    {A : Type u_1} →
      [inst_1 : NonUnitalRing A] →
        [inst_2 : StarRing A] →
          [inst_3 : Module R A] →
            [inst_4 : IsScalarTower R A A] →
              [inst_5 : SMulCommClass R A A] → NonUnitalCommRing ↥(NonUnitalStarSubalgebra.center R A)