mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.Prod
DifferentiableAt.finCons : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {n : ℕ} {F' : Fin n.succ → Type u_6}
  [inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_4 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ},
  DifferentiableAt 𝕜 φ x → DifferentiableAt 𝕜 φs x → DifferentiableAt 𝕜 (fun x => Fin.cons (φ x) (φs x)) x
-- Batteries.Data.List.Lemmas
List.append_eq_of_isSuffixOf?_eq_some : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {xs ys zs : List α}, xs.isSuffixOf? ys = some zs → zs ++ xs = ys
-- Mathlib.Algebra.GroupWithZero.Basic
mul_right_eq_self₀ : ∀ {M₀ : Type u_1} {a b : M₀} [inst : MulZeroOneClass M₀] [IsLeftCancelMulZero M₀], a * b = a ↔ b = 1 ∨ a = 0
-- Std.Http.Protocol.H1.Writer
/-- Closed; no further data can be written.
 -/
Std.Http.Protocol.H1.Writer.State.closed : Std.Http.Protocol.H1.Writer.State
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.decomposition_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C] (Δ : SimplexCategoryᵒᵖ),
  CategoryTheory.CategoryStruct.id (X.obj Δ) =
    ∑ A, CategoryTheory.CategoryStruct.comp (s.πSummand A) ((s.cofan Δ).inj A)
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
/-- The embedding from the smaller algebra into the new larger one.  -/
CliffordAlgebra.toEven : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (Q : QuadraticForm R M) → CliffordAlgebra Q →ₐ[R] ↥(CliffordAlgebra.even (CliffordAlgebra.EquivEven.Q' Q))
-- Mathlib.GroupTheory.Congruence.Defs
/-- The quotient of an `AddGroup` by an additive congruence relation is
an `AddGroup`.  -/
AddCon.addGroup : {M : Type u_1} → [inst : AddGroup M] → (c : AddCon M) → AddGroup c.Quotient
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.DeclValue.mapCode : {pu : Lean.Compiler.LCNF.Purity} →
  (Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Code pu) →
    Lean.Compiler.LCNF.DeclValue pu → Lean.Compiler.LCNF.DeclValue pu
-- Mathlib.Algebra.GroupWithZero.Divisibility
isRelPrime_zero_right : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] {x : α}, IsRelPrime x 0 ↔ IsUnit x
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.LambdaTheorems.mk : Std.HashMap (Lean.Name × Mathlib.Meta.FunProp.LambdaTheoremType) (Array Mathlib.Meta.FunProp.LambdaTheorem) →
  Mathlib.Meta.FunProp.LambdaTheorems
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.tensorUnit_src : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C],
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Dial C)).src = ⊤_ C
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
/-- `ofMatrix` bundled as a continuous linear equivalence.  -/
CStarMatrix.ofMatrixL : {m : Type u_1} →
  {n : Type u_2} → {A : Type u_3} → [inst : NonUnitalCStarAlgebra A] → Matrix m n A ≃L[ℂ] CStarMatrix m n A
-- Aesop.Builder.Basic
Aesop.RuleBuilderOptions.mk.sizeOf_spec : ∀ (immediatePremises? : Option (Array Lean.Name)) (indexingMode? : Option Aesop.IndexingMode)
  (casesPatterns? : Option (Array Aesop.CasesPattern)) (pattern? : Option Lean.Term)
  (transparency? indexTransparency? : Option Lean.Meta.TransparencyMode),
  sizeOf
      { immediatePremises? := immediatePremises?, indexingMode? := indexingMode?, casesPatterns? := casesPatterns?,
        pattern? := pattern?, transparency? := transparency?, indexTransparency? := indexTransparency? } =
    1 + sizeOf immediatePremises? + sizeOf indexingMode? + sizeOf casesPatterns? + sizeOf pattern? +
        sizeOf transparency? +
      sizeOf indexTransparency?
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.equivProd_counitIso_hom_app : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1}))
  (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A × B),
  (CategoryTheory.Comma.equivProd L R).counitIso.hom.app X =
    CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1) (CategoryTheory.CategoryStruct.id X.2)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
Std.Iterators.Types.Flatten.IsPlausibleStep.outerYield_flatMapM : ∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [inst_3 : Std.Iterator α m β] [inst_4 : Std.Iterator α₂ m γ] {f : β → m (Std.IterM m γ)} {it₁ it₁' : Std.IterM m β}
  {it₂' : Std.IterM m γ} {b : β},
  it₁.IsPlausibleStep (Std.IterStep.yield it₁' b) →
    MonadAttach.CanReturn (f b) it₂' →
      (Std.IterM.flatMapAfterM f it₁ none).IsPlausibleStep
        (Std.IterStep.skip (Std.IterM.flatMapAfterM f it₁' (some it₂')))
-- Mathlib.Util.Notation3
/-- Matcher for expressions produced by `foldl`.  -/
Mathlib.Notation3.matchFoldl : Lean.Name → Lean.Name → Lean.Name → Mathlib.Notation3.Matcher → Mathlib.Notation3.Matcher → Mathlib.Notation3.Matcher
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α}, a ∈ t.erase k ↔ cmp k a ≠ Ordering.eq ∧ a ∈ t
-- Mathlib.Probability.UniformOn
ProbabilityTheory.uniformOn_empty_meas : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω], ProbabilityTheory.uniformOn ∅ = 0
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.symm_comp_ofMulEquivOfLocalizations_apply' : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {k : P ≃* N} (x : M),
  k ((f.ofMulEquivOfLocalizations k.symm) x) = f x
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.map_one : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddMonoid M]
  (f : R →+* S), AddMonoidAlgebra.map (↑f) 1 = 1
-- Mathlib.Order.Filter.Extr
isMaxOn_dual_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsMaxOn (⇑OrderDual.toDual ∘ f) s a ↔ IsMinOn f s a
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.func.inj : ∀ {L : FirstOrder.Language} {α : Type u'} {l : ℕ} {_f : L.Functions l} {_ts : Fin l → L.Term α} {l_1 : ℕ}
  {_f_1 : L.Functions l_1} {_ts_1 : Fin l_1 → L.Term α},
  FirstOrder.Language.func _f _ts = FirstOrder.Language.func _f_1 _ts_1 → l = l_1 ∧ _f ≍ _f_1 ∧ _ts ≍ _ts_1
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] [inst_3 : CategoryTheory.BraidedCategory D]
  (A : CategoryTheory.CommMon (CategoryTheory.Functor C D)) (X : C),
  CategoryTheory.MonObj.one = CategoryTheory.MonObj.one.app X
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.symm_dual_id : ∀ {α : Type u_2} [inst : Max α] [inst_1 : Bot α], SupBotHom.dual.symm (InfTopHom.id αᵒᵈ) = SupBotHom.id α
-- Mathlib.Topology.Algebra.FilterBasis
ModuleFilterBasis.smul_left : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : TopologicalSpace R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] (B : ModuleFilterBasis R M) (x₀ : R) {U : Set M}, U ∈ B → ∃ V ∈ B, V ⊆ (fun x => x₀ • x) ⁻¹' U
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.of_discrete : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [Countable α] [MeasurableSingletonClass α], MeasureTheory.AEStronglyMeasurable f μ
-- Mathlib.AlgebraicTopology.DoldKan.NCompGamma
/-- The unit isomorphism of the Dold-Kan equivalence.  -/
AlgebraicTopology.DoldKan.Γ₂N₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] →
        CategoryTheory.Functor.id (CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)) ≅
          AlgebraicTopology.DoldKan.N₂.comp AlgebraicTopology.DoldKan.Γ₂
-- Mathlib.Data.EReal.Basic
EReal.coe_ennreal_ofReal : ∀ {x : ℝ}, ↑(ENNReal.ofReal x) = ↑(max x 0)
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.GrowsPolynomially.const_mul : ∀ {f : ℝ → ℝ} {c : ℝ}, AkraBazziRecurrence.GrowsPolynomially f → AkraBazziRecurrence.GrowsPolynomially fun x => c * f x
-- Mathlib.RepresentationTheory.Basic
Representation.smul_ofModule_asModule : ∀ {k : Type u_1} {G : Type u_2} [inst : CommSemiring k] [inst_1 : Monoid G] (M : Type u_4) [inst_2 : AddCommMonoid M]
  [inst_3 : Module (MonoidAlgebra k G) M] (r : MonoidAlgebra k G) (m : (Representation.ofModule M).asModule),
  (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) ((Representation.ofModule M).asModuleEquiv (r • m)) =
    r • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) ((Representation.ofModule M).asModuleEquiv m)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_inter_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₂.contains k = false → (m₁.inter m₂).getKey? k = none
-- Mathlib.Topology.Algebra.Polynomial
Polynomial.isClosedMap_eval : ∀ {R : Type u_2} [inst : NormedRing R] [IsAbsoluteValue norm] [ProperSpace R] (p : Polynomial R),
  IsClosedMap fun x => Polynomial.eval x p
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get_maxD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {fallback : α} {hc : t.maxD fallback ∈ t}, t.get (t.maxD fallback) hc = t.maxD fallback
-- Lean.Elab.Do.Basic
/-- Elaborate `doSeq` using `ops` for pure/bind construction.  -/
Lean.Elab.Do.elabDoWith : Lean.Elab.Do.DoOps → Lean.DoSeq → Option Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
CochainComplex.instShiftSequenceHomologicalComplexIntUpHomologyFunctorOfNat : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.CategoryWithHomology C] →
        (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).ShiftSequence ℤ
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trList.eq_2 : ∀ (n : ℕ) (ns : List ℕ),
  Turing.PartrecToTM2.trList (n :: ns) =
    Turing.PartrecToTM2.trNat n ++ Turing.PartrecToTM2.Γ'.cons :: Turing.PartrecToTM2.trList ns
-- Mathlib.AlgebraicTopology.DoldKan.Projections
AlgebraicTopology.DoldKan.map_Q : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.Preadditive D]
  (G : CategoryTheory.Functor C D) [G.Additive] (X : CategoryTheory.SimplicialObject C) (q n : ℕ),
  G.map ((AlgebraicTopology.DoldKan.Q q).f n) = (AlgebraicTopology.DoldKan.Q q).f n
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.univ_sub_univ : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SubtractionMonoid α] [inst_2 : Fintype α],
  Finset.univ - Finset.univ = Finset.univ
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- The factorisation through the zero object is an image factorisation.
 -/
CategoryTheory.Limits.imageFactorisationZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [CategoryTheory.Limits.HasZeroObject C] → (X Y : C) → CategoryTheory.Limits.ImageFactorisation 0
-- Lean.Data.Lsp.Basic
/-- The version number of this document (it will increase after each change, including undo/redo).  -/
Lean.Lsp.TextDocumentItem.version : Lean.Lsp.TextDocumentItem → ℕ
-- Mathlib.LinearAlgebra.Dual.Defs
Submodule.coe_dualCoannihilator_span : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s : Set (Module.Dual R M)), ↑(Submodule.span R s).dualCoannihilator = {x | ∀ f ∈ s, f x = 0}
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.equivalence₁UnitIso_inv_app : ∀ {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] [inst_2 : CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'}
  {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) (X : A),
  (AlgebraicTopology.DoldKan.Compatibility.equivalence₁UnitIso hF).inv.app X =
    CategoryTheory.CategoryStruct.comp (eA.inverse.map (e'.inverse.map (hF.inv.app X)))
      (CategoryTheory.CategoryStruct.comp (eA.inverse.map (e'.unitIso.inv.app (eA.functor.obj X)))
        (eA.unitIso.inv.app X))
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearIsometryEquiv.conjStarAlgEquiv_ext_iff : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {H : Type u_5} [inst_1 : NormedAddCommGroup H] [inst_2 : InnerProductSpace 𝕜 H]
  [inst_3 : CompleteSpace H] {K : Type u_6} [inst_4 : NormedAddCommGroup K] [inst_5 : InnerProductSpace 𝕜 K]
  [inst_6 : CompleteSpace K] (f g : H ≃ₗᵢ[𝕜] K), f.conjStarAlgEquiv = g.conjStarAlgEquiv ↔ ∃ α, f = α • g
-- Std.Do.WP.SimpLemmas
Std.Do.WP.restoreM_trans : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {o : Type u → Type u_1} {n : Type u → Type u_2} {α : Type u}
  {Q : Std.Do.PostCond α ps} [inst : Std.Do.WP o ps] [inst_1 : MonadControl n o] [inst_2 : MonadControlT m n]
  (x : stM m o α), (Std.Do.wp (restoreM x)).apply Q = (Std.Do.wp (MonadControl.restoreM (restoreM x))).apply Q
-- Mathlib.Algebra.Algebra.Bilinear
LinearMap.flip_mul : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocCommSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A], (LinearMap.mul R A).flip = LinearMap.mul R A
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.hom_zero : ∀ {V W : SemiNormedGrp}, SemiNormedGrp.Hom.hom 0 = 0
-- Mathlib.Tactic.Tauto
/-- Tries to apply de-Morgan-like rules on all hypotheses.
Always succeeds, regardless of whether any progress was actually made.
 -/
Mathlib.Tactic.Tauto.distribNot : Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.map_mrange : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P] (g : N →+ P) (f : M →+ N),
  AddSubmonoid.map g (AddMonoidHom.mrange f) = AddMonoidHom.mrange (g.comp f)
-- Init.Data.Iterators.Combinators.Monadic.Attach
_private.Init.Data.Iterators.Combinators.Monadic.Attach.0.Std.Iterators.Types.Attach.Monadic.modifyStep.match_1.splitter : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [inst : Std.Iterator α m β] →
        {P : β → Prop} →
          (it : Std.IterM m { out // P out }) →
            (motive : it.internalState.inner.Step → Sort u_3) →
              (step : it.internalState.inner.Step) →
                ((it' : Std.IterM m β) →
                    (out : β) →
                      (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out)) →
                        motive ⟨Std.IterStep.yield it' out, h⟩) →
                  ((it' : Std.IterM m β) →
                      (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')) →
                        motive ⟨Std.IterStep.skip it', h⟩) →
                    ((property : it.internalState.inner.IsPlausibleStep Std.IterStep.done) →
                        motive ⟨Std.IterStep.done, property⟩) →
                      motive step
-- Aesop.Forward.State
Aesop.InstMap.mk : Lean.PHashMap Aesop.SlotIndex (Aesop.EMap (Lean.PHashSet Aesop.Match × Lean.PHashSet Aesop.Hyp)) → Aesop.InstMap
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
/-- The postcomposition `Ext X Y a →+ Ext X Z b` with `β : Ext Y Z n` when `a + n = b`.  -/
CategoryTheory.Abelian.Ext.postcomp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.HasExt C] →
        {Y Z : C} →
          {n : ℕ} →
            CategoryTheory.Abelian.Ext Y Z n →
              (X : C) → {a b : ℕ} → a + n = b → CategoryTheory.Abelian.Ext X Y a →+ CategoryTheory.Abelian.Ext X Z b
-- Mathlib.Analysis.Normed.Ring.Basic
/-- The distance is induced by the norm.  -/
NonUnitalNormedRing.dist_eq : ∀ {α : Type u_5} [self : NonUnitalNormedRing α] (x y : α), dist x y = ‖-x + y‖
-- Mathlib.GroupTheory.Abelianization.Defs
/-- See note [partially-applied ext lemmas].  -/
Abelianization.hom_ext : ∀ {G : Type u} [inst : Group G] {A : Type v} [inst_1 : Monoid A] (φ ψ : Abelianization G →* A),
  φ.comp Abelianization.of = ψ.comp Abelianization.of → φ = ψ
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- A vector measure on a measurable space `α` is a σ-additive `M`-valued function (for some `M`
an additive monoid) such that the empty set and non-measurable sets are mapped to zero.  -/
MeasureTheory.VectorMeasure : (α : Type u_3) → [MeasurableSpace α] → (M : Type u_4) → [AddCommMonoid M] → [TopologicalSpace M] → Type (max u_3 u_4)
-- Mathlib.ModelTheory.Bundled
/-- The object in the category of R-algebras associated to a type equipped with the appropriate
typeclasses.  -/
FirstOrder.Language.Theory.ModelType.of : {L : FirstOrder.Language} →
  (T : L.Theory) → (M : Type w) → [inst : L.Structure M] → [M ⊨ T] → [Nonempty M] → T.ModelType
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
AlgebraicGeometry.UniversallyInjective.isStableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.UniversallyInjective
-- Mathlib.Order.SymmDiff
top_symmDiff : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] (a : α), symmDiff ⊤ a = ￢a
-- Mathlib.RingTheory.LocalProperties.Injective
/-- A variant of `Module.injective_of_localization_maximal` that accepts `IsLocalizedModule`.
 -/
Module.injective_of_localization_maximal' : ∀ {R : Type u} [inst : CommRing R] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u') [inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)]
  [∀ (P : Ideal R) [inst : P.IsMaximal], Small.{v', u'} (Rₚ P)]
  [inst_5 : (P : Ideal R) → [inst_5 : P.IsMaximal] → Algebra R (Rₚ P)]
  [∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P]
  (Mₚ : (P : Ideal R) → [P.IsMaximal] → Type v') [inst_7 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)]
  [inst_8 : (P : Ideal R) → [inst_8 : P.IsMaximal] → Module R (Mₚ P)]
  [inst_9 : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)]
  [∀ (P : Ideal R) [inst_10 : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)]
  (f : (P : Ideal R) → [inst_11 : P.IsMaximal] → M →ₗ[R] Mₚ P)
  [inst_11 : ∀ (P : Ideal R) [inst_11 : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] [Small.{v, u} R]
  [IsNoetherianRing R], (∀ (I : Ideal R) (x : I.IsMaximal), Module.Injective (Rₚ I) (Mₚ I)) → Module.Injective R M
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.all_filterMapM : ∀ {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : MonadLiftT m n] [inst_3 : Std.IteratorLoop α m m] [inst_4 : Monad m]
  [LawfulMonad m] [inst_6 : Monad n] [inst_7 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
  [LawfulMonadLiftT m n] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β} {f : β → n (Option β')} {p : β' → Bool},
  Std.IterM.all p (Std.IterM.filterMapM f it) =
    Std.IterM.allM
      (fun x => do
        let __do_lift ← f x
        match __do_lift with
          | some fx => pure { down := p fx }
          | none => pure { down := true })
      (Std.IterM.mapM pure it)
-- Init.Prelude
instPowOfHomogeneousPow : {α : Type u_1} → [HomogeneousPow α] → Pow α α
-- Lean.AddDecl
_private.Lean.AddDecl.0.Lean.registerNamePrefixes.go : Lean.Environment → Lean.Name → Lean.Environment
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.le_add_left : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν ν' : MeasureTheory.Measure α}, μ ≤ ν → μ ≤ ν' + ν
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.coe_algebraMap : ∀ {R : Type u_1} [inst : CommSemiring R],
  ⇑(algebraMap (PowerSeries R) (LaurentSeries R)) = ⇑(HahnSeries.ofPowerSeries ℤ R)
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.LaxMonoidalFunctor.hom_ext_iff : ∀ {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 G : CategoryTheory.LaxMonoidalFunctor C D} {α β : F ⟶ G}, α = β ↔ α.hom = β.hom
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instZeroAtInftyContinuousMapClass : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β],
  ZeroAtInftyContinuousMapClass (ZeroAtInftyContinuousMap α β) α β
-- Mathlib.Tactic.Attr.Register
/-- Simplification procedure  -/
Parser.Attr.ghost_simps_proc : Lean.ParserDescr
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
/-- Given an element `m : M.Elements` of a presheaf of modules `M`, this is the
free presheaf of modules on the Yoneda presheaf of types corresponding to the
underlying object of `m`.  -/
PresheafOfModules.Elements.freeYoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} → {M : PresheafOfModules R} → M.Elements → PresheafOfModules R
-- Mathlib.Algebra.Polynomial.Div
Polynomial.modByMonic_X_sub_C_eq_C_eval : ∀ {R : Type u} [inst : CommRing R] (p : Polynomial R) (a : R),
  p %ₘ (Polynomial.X - Polynomial.C a) = Polynomial.C (Polynomial.eval a p)
-- Mathlib.Topology.ContinuousMap.CompactlySupported
/-- For a positive linear functional `Λ : C_c(α, ℝ) → ℝ`, define a `ℝ≥0`-linear map.  -/
CompactlySupportedContinuousMap.toNNRealLinear : {α : Type u_2} →
  [inst : TopologicalSpace α] →
    (CompactlySupportedContinuousMap α ℝ →ₚ[ℝ] ℝ) → CompactlySupportedContinuousMap α NNReal →ₗ[NNReal] NNReal
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.comm_assoc : ∀ {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} (self : SSet.RelativeMorphism A B φ)
  {Z : SSet} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp A.ι (CategoryTheory.CategoryStruct.comp self.map h) =
    CategoryTheory.CategoryStruct.comp φ (CategoryTheory.CategoryStruct.comp B.ι h)