mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_multiset_prod : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (m : Multiset (Polynomial R)),
  0 ∉ m → m.prod.roots = m.bind Polynomial.roots
-- Lean.Parser.Term
Lean.Parser.Term.letIdLhs.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- **Alias** of `zero_apply`. -/
MultilinearMap.zero_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Zero β}
  {inst_2 : Zero F} [self : IsZeroApply F α β] (x : α), 0 x = 0
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.neg_range' : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {ι : Type u_5} {f : ι → α}, -Set.range f = Set.range (-f)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- An auxiliary structure used to define `IsRankLeOne`.  -/
ValuativeRel.RankLeOneStruct : (R : Type u_1) → [inst : Semiring R] → [ValuativeRel R] → Type u_1
-- Mathlib.Order.Filter.CardinalInter
/-- Assuming `2 < c`, `Filter.cardinalGenerate c g` is the greatest `CardinalInterFilter c`
containing `g`.  -/
Filter.cardinalGenerate : {α : Type u} → {c : Cardinal.{u}} → Set (Set α) → 2 < c → Filter α
-- Init.Data.Ord.Basic
Ordering.isGE_left_of_isGE_then : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isGE = true → o₁.isGE = true
-- Mathlib.Algebra.Opposites
MulOpposite.op_inj : ∀ {α : Type u_1} {x y : α}, MulOpposite.op x = MulOpposite.op y ↔ x = y
-- Std.Data.DTreeMap.Basic
/-- Transforms a list of mappings into a tree map.  -/
Std.DTreeMap.Const.ofArray : {α : Type u} →
  {β : Type v} →
    Array (α × β) →
      (cmp : autoParam (α → α → Ordering) Std.DTreeMap.Const.ofArray._auto_1) → Std.DTreeMap α (fun x => β) cmp
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
IsPrimitiveRoot.minpoly_eq_cyclotomic_of_irreducible : ∀ {K : Type u_2} [inst : Field K] {R : Type u_3} [inst_1 : CommRing R] [IsDomain R] {μ : R} {n : ℕ}
  [inst_3 : Algebra K R],
  IsPrimitiveRoot μ n → Irreducible (Polynomial.cyclotomic n K) → ∀ [NeZero ↑n], Polynomial.cyclotomic n K = minpoly K μ
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.toOplax_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (η : F.StrongTrans G) {a b : B} (f : a ⟶ b),
  η.toOplax.naturality f = η.naturality f
-- Mathlib.Algebra.Group.Basic
mul_div_mul_comm : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b c d : α), a * b / (c * d) = a / c * (b / d)
-- Mathlib.Topology.Bases
/-- In a second countable topological space, any open set is a countable union of elements in a
given topological basis.  -/
TopologicalSpace.IsTopologicalBasis.exists_countable_biUnion_of_isOpen : ∀ {α : Type u} [t : TopologicalSpace α] [SecondCountableTopology α] {t_1 : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis t_1 → ∀ {u : Set α}, IsOpen u → ∃ s ⊆ t_1, s.Countable ∧ u = ⋃ a ∈ s, a
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_le_of_le_one_of_le : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulRightMono α] {a b c : α}, a ≤ 1 → b ≤ c → a * b ≤ c
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_natCast_add : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (n : ℕ) (a : R),
  ⌊↑n + a⌋ = ↑n + ⌊a⌋
-- Std.Http.Data.Extensions
_private.Std.Http.Data.Extensions.0.Std.Http.Extensions.mk : Std.TreeMap Lean.Name Dynamic Std.Http.Extensions.compareName → Std.Http.Extensions
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
spectrumRestricts_iff : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : Semifield R] [inst_1 : Semifield S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] {a : A} {f : S → R},
  SpectrumRestricts a f ↔ Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a) ∧ Function.LeftInverse f ⇑(algebraMap R S)
-- Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic
/-- Any graph on a subsingleton vertex type has a unit-distance embedding, provided the metric space
is nonempty.  -/
SimpleGraph.UnitDistEmbedding.subsingleton : {V : Type u_1} →
  (G : SimpleGraph V) → {E : Type u_3} → [inst : MetricSpace E] → [Subsingleton V] → E → G.UnitDistEmbedding E
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- **Alias** of `MonoidAlgebra.coeff_uniqueRingEquiv_symm`. -/
MonoidAlgebra.uniqueRingEquiv_symm_apply_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Monoid M] [inst_2 : Subsingleton M] (r : R) (m : M),
  ((MonoidAlgebra.uniqueRingEquiv M).symm r).coeff m = r
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lt_wf : WellFounded fun x1 x2 => x1 < x2
-- Mathlib.NumberTheory.Padics.AddChar
AddChar.tendsto_eval_one_sub_pow : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : NormedRing R] [inst_2 : Algebra ℤ_[p] R]
  [IsBoundedSMul ℤ_[p] R] [IsUltrametricDist R] {κ : AddChar ℤ_[p] R},
  Continuous ⇑κ → Filter.Tendsto (fun n => (κ 1 - 1) ^ n) Filter.atTop (nhds 0)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.Pure.thm : ∀ {σs : List (Type u)} {P Q T : Std.Do.SPred σs} {φ : Prop} [Std.Do.SPred.Tactic.IsPure Q φ], (φ → P ⊢ₛ T) → P ∧ Q ⊢ₛ T
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.measure_of_measure_compl_eq_zero : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}, μ sᶜ = 0 → μ s = μ Set.univ
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
MvPolynomial.leadingCoeff_esymmAlgHomMonomial : ∀ {R : Type u_3} {n m : ℕ} [inst : CommSemiring R] {r : R} (t : Fin n →₀ ℕ),
  n ≤ m → AddMonoidAlgebra.leadingCoeff (⇑toLex) (MvPolynomial.esymmAlgHomMonomial (Fin m) t r) = r
-- Mathlib.Tactic.ClickSuggestions.ApplyAt
Mathlib.Tactic.ClickSuggestions.ApplyAtLemma.mk.sizeOf_spec : ∀ (name : Mathlib.Tactic.ClickSuggestions.Premise), sizeOf { name := name } = 1 + sizeOf name
-- Lean.Meta.Tactic.Injection
/-- `injections` closed the input goal.  -/
Lean.Meta.InjectionsResult.solved : Lean.Meta.InjectionsResult
-- Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
_private.Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs.0.SimpleGraph.binomialRandom_map_ncard_edgeSet_singleton : {V : Type u_1} →
  {p : ↑unitInterval} →
    [Finite V] →
      (n : ℕ) →
        ProofWanted
          ((MeasureTheory.Measure.map (fun G => G.edgeSet.ncard) (SimpleGraph.binomialRandom V p)) {n} =
            ↑(((Nat.card V).choose 2).choose n) * ↑(unitInterval.toNNReal p) ^ n *
              ↑(unitInterval.toNNReal (unitInterval.symm p)) ^ ((Nat.card V).choose 2 - n))
-- Std.Http.Data.Chunk
Std.Http.Chunk.instReprExtensionName.repr : Std.Http.Chunk.ExtensionName → ℕ → Std.Format
-- Init.Data.Vector.Basic
Vector.mapIdxM : {n : ℕ} → {α : Type u} → {β : Type v} → {m : Type v → Type w} → [Monad m] → (ℕ → α → m β) → Vector α n → m (Vector β n)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
/-- `Prod.fst` as a `ContinuousLinearMap`.  -/
ContinuousLinearMap.fst : (R : Type u_1) →
  [inst : Semiring R] →
    (M₁ : Type u_2) →
      [inst_1 : TopologicalSpace M₁] →
        [inst_2 : AddCommMonoid M₁] →
          [inst_3 : Module R M₁] →
            (M₂ : Type u_3) →
              [inst_4 : TopologicalSpace M₂] → [inst_5 : AddCommMonoid M₂] → [inst_6 : Module R M₂] → M₁ × M₂ →L[R] M₁
-- Mathlib.Algebra.Order.Archimedean.Defs
exists_nat_gt : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] (x : R),
  ∃ n, x < ↑n
-- Mathlib.Data.Prod.Basic
Prod.map_rightInverse : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Nonempty α] [Nonempty γ] {f₁ : α → β} {g₁ : γ → δ}
  {f₂ : β → α} {g₂ : δ → γ},
  Function.RightInverse (Prod.map f₁ g₁) (Prod.map f₂ g₂) ↔ Function.RightInverse f₁ f₂ ∧ Function.RightInverse g₁ g₂
-- Mathlib.RingTheory.FreeCommRing
FreeCommRing.isSupported_upwards : ∀ {α : Type u} {x : FreeCommRing α} {s t : Set α}, x.IsSupported s → s ⊆ t → x.IsSupported t
-- Mathlib.Analysis.Normed.Group.Bounded
tendsto_norm_atTop_iff_cobounded' : ∀ {α : Type u_1} {E : Type u_2} [inst : SeminormedGroup E] {f : α → E} {l : Filter α},
  Filter.Tendsto (fun x => ‖f x‖) l Filter.atTop ↔ Filter.Tendsto f l (Bornology.cobounded E)
-- Mathlib.Analysis.CStarAlgebra.Multiplier
/-- The canonical map `DoubleCentralizer.toProd` as an additive group homomorphism.  -/
DoubleCentralizer.toProdHom : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : SMulCommClass 𝕜 A A] →
            [inst_4 : IsScalarTower 𝕜 A A] → DoubleCentralizer 𝕜 A →+ (A →L[𝕜] A) × (A →L[𝕜] A)
-- Mathlib.Algebra.Algebra.Subalgebra.Centralizer
Subalgebra.centralizer_tensorProduct_eq_center_tensorProduct_left : ∀ (R : Type u_1) [inst : CommSemiring R] (A : Type u_2) [inst_1 : Semiring A] [inst_2 : Algebra R A] (B : Type u_3)
  [inst_3 : Semiring B] [inst_4 : Algebra R B] [Module.Free R B],
  Subalgebra.centralizer R ↑(Algebra.TensorProduct.map (AlgHom.id R A) (Algebra.ofId R B)).range =
    (Algebra.TensorProduct.map (Subalgebra.center R A).val (AlgHom.id R B)).range
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
CategoryTheory.additive_yonedaObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (X : C),
  (CategoryTheory.preadditiveYonedaObj X).Additive
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.nullHomotopic_τ₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S₁ S₂ : CategoryTheory.ShortComplex C) (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0)
  (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃)
  (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0),
  (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃ = CategoryTheory.CategoryStruct.comp h₂ S₂.g + h₃
-- Mathlib.Order.Filter.AtTopBot.Prod
Filter.prod_map_atTop_eq : ∀ {α₁ : Type u_6} {α₂ : Type u_7} {β₁ : Type u_8} {β₂ : Type u_9} [inst : Preorder β₁] [inst_1 : Preorder β₂]
  (u₁ : β₁ → α₁) (u₂ : β₂ → α₂),
  Filter.map u₁ Filter.atTop ×ˢ Filter.map u₂ Filter.atTop = Filter.map (Prod.map u₁ u₂) Filter.atTop
-- Mathlib.Data.List.ToFinsupp
List.toFinsupp_apply : ∀ {M : Type u_1} [inst : Zero M] (l : List M) [inst_1 : DecidablePred fun x => l.getD x 0 ≠ 0] (i : ℕ),
  l.toFinsupp i = l.getD i 0
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.map_eq_iff : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂) {x y : E}, e x = e y ↔ x = y
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.symm_comp_self : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), ⇑e.symm ∘ ⇑e = id
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.MemLp.toLp_eq_toLp_iff : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f g : α → E} (hf : MeasureTheory.MemLp f p μ) (hg : MeasureTheory.MemLp g p μ),
  MeasureTheory.MemLp.toLp f hf = MeasureTheory.MemLp.toLp g hg ↔ f =ᵐ[μ] g
-- Init.Data.Slice.List.Lemmas
ListSlice.mkSlice_ric_eq_mkSlice_rio : ∀ {α : Type u_1} {xs : ListSlice α} {hi : ℕ},
  (Std.Ric.Sliceable.mkSlice xs *...=hi) = Std.Rio.Sliceable.mkSlice xs *...hi + 1
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.op_sSup : ∀ {G : Type u_2} [inst : Group G] (S : Set (Subgroup G)), (sSup S).op = sSup (Subgroup.unop ⁻¹' S)
-- Mathlib.GroupTheory.Coset.Basic
/-- If `s` is a subgroup of the group `α`, and `t` is a subset of `α ⧸ s`, then there is a
(typically non-canonical) bijection between the preimage of `t` in `α` and the product `s × t`.  -/
QuotientGroup.preimageMkEquivSubgroupProdSet : {α : Type u_1} → [inst : Group α] → (s : Subgroup α) → (t : Set (α ⧸ s)) → ↑(QuotientGroup.mk ⁻¹' t) ≃ ↥s × ↑t
-- Lean.Meta.Sym.DSimp.DSimpM
/-- Mutable state for the definitional simplifier.  -/
Lean.Meta.Sym.DSimp.State : Type
-- Mathlib.FieldTheory.RatFunc.Degree
RatFunc.intDegree_one : ∀ {K : Type u} [inst : Field K], RatFunc.intDegree 1 = 0
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.HeightOneSpectrum.embedding_mul_absNorm`. -/
NumberField.FinitePlace.IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm : ∀ (K : Type u_1) [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R] {x : R},
  x ≠ 0 →
    ‖(NumberField.FinitePlace.embedding v) ((algebraMap R K) x)‖ *
        ↑(Ideal.absNorm (v.maxPowDividing (Ideal.span {x}))) =
      1
-- Mathlib.CategoryTheory.Sites.GlobalSections
CategoryTheory.Sheaf.coneΓ_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] [inst_2 : CategoryTheory.HasWeakSheafify J A]
  [inst_3 : CategoryTheory.HasGlobalSectionsFunctor J A] (F : CategoryTheory.Sheaf J A),
  F.coneΓ.pt = (CategoryTheory.Sheaf.Γ J A).obj F
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
/-- The set `D f K` is a complicated set constructed using countable intersections and unions. Its
main use is that, when `K` is complete, it is exactly the set of points where `f` is differentiable,
with a derivative in `K`.  -/
FDerivMeasurableAux.D : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_3} →
            [inst_3 : NormedAddCommGroup F] → [inst_4 : NormedSpace 𝕜 F] → (E → F) → Set (E →L[𝕜] F) → Set E
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.isPullback : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₃ Y₃ : C₃}
  {f₃ : X₃ ⟶ Y₃} (self : G.PullbackObjObj f₁ f₃),
  CategoryTheory.IsPullback self.fst self.snd ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃)
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The angle between a vector and a negative multiple of a vector.  -/
InnerProductGeometry.angle_smul_right_of_neg : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V) {r : ℝ},
  r < 0 → InnerProductGeometry.angle x (r • y) = InnerProductGeometry.angle x (-y)
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instNatCastCoeOfAddSubmonoidWithOneClass : {ι : Type u_1} →
  (R : ι → Type u_2) →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            [inst_1 : (i : ι) → AddMonoidWithOne (R i)] →
              [∀ (i : ι), AddSubmonoidWithOneClass (S i) (R i)] →
                NatCast (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_toIocMod : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a₁ a₂ b : α), toIcoMod hp a₁ (toIocMod hp a₂ b) = toIcoMod hp a₁ b
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z_obj_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  (data : W₁.FunctorialFactorizationData W₂) (J : Type u_3) [inst_1 : CategoryTheory.Category.{v_3, u_3} J]
  (f : CategoryTheory.Arrow (CategoryTheory.Functor J C)) {X Y : J} (φ : X ⟶ Y),
  ((CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z data J).obj f).map φ =
    data.mapZ (CategoryTheory.Arrow.homMk (f.left.map φ) (f.right.map φ) ⋯)
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.coe_sum : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂] {ι : Type u_5}
  (s : Finset ι) (f : ι → NormedAddGroupHom V₁ V₂), ⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(f i)
-- Mathlib.Algebra.Algebra.Operations
Submodule.mker_spanSingleton : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] [FaithfulSMul R A],
  MonoidHom.mker (Submodule.spanSingleton R) = Submonoid.map (algebraMap R A) (IsUnit.submonoid R)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.top_prod_top : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S], ⊤.prod ⊤ = ⊤
-- Init.Data.Int.Basic
/-- Subtraction of integers, usually accessed via the `-` operator.

This function is overridden by the compiler with an efficient implementation. This definition is
the logical model.

Examples:
* `(63 : Int) - (6 : Int) = 57`
* `(7 : Int) - (0 : Int) = 7`
* `(0 : Int) - (7 : Int) = -7`
 -/
Int.sub : ℤ → ℤ → ℤ
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.lift_one : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {c₁ c₂ c₃ : R}
  (q : QuaternionAlgebra.Basis A c₁ c₂ c₃), q.lift 1 = 1
-- Mathlib.Logic.Lemmas
dite_dite_distrib_right : ∀ {α : Sort u_1} {p q : Prop} [inst : Decidable p] [inst_1 : Decidable q] {a : p → q → α} {b : p → ¬q → α} {c : ¬p → α},
  dite p (fun hp => dite q (a hp) (b hp)) c =
    if hq : q then dite p (fun hp => a hp hq) c else dite p (fun hp => b hp hq) c
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- The type indexing the basis `stdBasis`.  -/
NumberField.mixedEmbedding.index : (K : Type u_1) → [Field K] → Type u_1
-- Lean.Data.LOption
Lean.LOption.none.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α], sizeOf Lean.LOption.none = 1
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.coe_aeval_eq_eval : ∀ {R : Type u} [inst : CommSemiring R] (r : R), ⇑(Polynomial.aeval r) = Polynomial.eval r
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.GeneratingSections.ofEpi.congr_simp : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (σ σ_1 : M.GeneratingSections),
  σ = σ_1 → ∀ (p p_1 : M ⟶ N) (e_p : p = p_1) [inst_3 : CategoryTheory.Epi p], σ.ofEpi p = σ_1.ofEpi p_1
-- Lean.Elab.Do.InferControlInfo
Lean.Elab.Do.instInhabitedControlInfo.default : Lean.Elab.Do.ControlInfo
-- Aesop.Util.Basic
Aesop.forEachExprInLDecl' : {ω : Type} →
  {m : Type → Type} → [STWorld ω m] → [MonadLiftT (ST ω) m] → [Monad m] → Lean.LocalDecl → (Lean.Expr → m Bool) → m Unit
-- Std.Time.Zoned.Database.PosixTz
_private.Std.Time.Zoned.Database.PosixTz.0.Std.Time.TimeZone.posixParseHMS : optParam ℕ 24 → Std.Internal.Parsec.String.Parser Std.Time.Second.Offset
-- Mathlib.Analysis.Calculus.DiffContOnCl
DiffContOnCl.smul : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {𝕜' : Type u_5}
  [inst_5 : NontriviallyNormedField 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F]
  {c : E → 𝕜'} {f : E → F} {s : Set E}, DiffContOnCl 𝕜 c s → DiffContOnCl 𝕜 f s → DiffContOnCl 𝕜 (fun x => c x • f x) s
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.degree_k : Lean.Grind.CommRing.Mon → ℕ
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousAddMonoidHom.instT2Space : ∀ {A : Type u_2} {B : Type u_3} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] [T2Space B], T2Space (A →ₜ+ B)
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrixAlgEquiv'_toLinAlgEquiv' : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  (M : Matrix n n R), LinearMap.toMatrixAlgEquiv' (Matrix.toLinAlgEquiv' M) = M
-- Lean.Elab.Match
Lean.Elab.Term.ToDepElimPattern.TopSort.State.visitedMVars : Lean.Elab.Term.ToDepElimPattern.TopSort.State → Lean.MVarIdSet
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
complEDS_ofNat : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (k : ℤ) (n : ℕ), complEDS b c d k ↑n = complEDS' b c d k n
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- Range of an `NonUnitalAlgHom` as a `NonUnitalStarSubalgebra`.  -/
NonUnitalStarAlgHom.range : {F : Type v'} →
  {R : Type u} →
    {A : Type v} →
      {B : Type w} →
        [inst : CommSemiring R] →
          [inst_1 : NonUnitalNonAssocSemiring A] →
            [inst_2 : Module R A] →
              [inst_3 : Star A] →
                [inst_4 : NonUnitalNonAssocSemiring B] →
                  [inst_5 : Module R B] →
                    [inst_6 : Star B] →
                      [inst_7 : FunLike F A B] →
                        [NonUnitalAlgHomClass F R A B] → [StarHomClass F A B] → F → NonUnitalStarSubalgebra R B
-- Mathlib.Algebra.Group.Action.Opposite
SMulCommClass.opposite_mid : ∀ {M : Type u_5} {N : Type u_6} [inst : Mul N] [inst_1 : SMul M N] [IsScalarTower M N N], SMulCommClass M Nᵐᵒᵖ N
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_le_measureReal_union_left : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  autoParam (μ t ≠ ⊤) MeasureTheory.measureReal_le_measureReal_union_left._auto_1 → μ.real s ≤ μ.real (s ∪ t)
-- Mathlib.LinearAlgebra.Matrix.Stochastic
/-- Every entry of a row stochastic matrix is less than or equal to 1.  -/
Matrix.le_one_of_mem_rowStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {M : Matrix n n R},
  M ∈ Matrix.rowStochastic R n → ∀ {i j : n}, M i j ≤ 1
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.ofBifunctor.Forward.secondMap₁_app_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (β : CategoryTheory.MonoidalCategory.curriedTensor C ≅ (CategoryTheory.MonoidalCategory.curriedTensor C).flip)
  (X₁ X₂ X₃ : C),
  (((CategoryTheory.BraidedCategory.ofBifunctor.Forward.secondMap₁ β).app X₁).app X₂).app X₃ =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight ((β.hom.app X₁).app X₂) X₃
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_counitIso_hom_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (adj : F ⊣ G)
  (X : CategoryTheory.Endofunctor.Coalgebra G),
  ((CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv adj).counitIso.hom.app X).f =
    CategoryTheory.CategoryStruct.id X.V
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- An object `X` has `𝟙 X = 0` if and only if it is isomorphic to the zero object.

Because `X ≅ 0` contains data (even if a subsingleton), we express this `↔` as an `≃`.
 -/
CategoryTheory.Limits.idZeroEquivIsoZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → (X : C) → CategoryTheory.CategoryStruct.id X = 0 ≃ (X ≅ 0)