mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommSum_cons : ∀ {α : Type u_3} {β : Type u_4} [inst : AddMonoid β] (s : Finset α) (a : α) (f : α → β) (ha : a ∉ s)
  (comm : (↑(Finset.cons a s ha)).Pairwise (Function.onFun AddCommute f)),
  (Finset.cons a s ha).noncommSum f comm = f a + s.noncommSum f ⋯
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.instIsAddMonHomNegOfIsCommAddMonObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {G : C}
  [inst_2 : CategoryTheory.AddGrpObj G] [inst_3 : CategoryTheory.BraidedCategory C] [CategoryTheory.IsCommAddMonObj G],
  CategoryTheory.IsAddMonHom CategoryTheory.AddGrpObj.neg
-- Mathlib.Order.Filter.Pointwise
Filter.mul_top_of_one_le : ∀ {α : Type u_2} [inst : Monoid α] {f : Filter α}, 1 ≤ f → f * ⊤ = ⊤
-- Mathlib.CategoryTheory.Action.Continuous
CategoryTheory.Equivalence.mapContAction_inverse : ∀ {V : Type u_5} {W : Type u_6} [inst : CategoryTheory.Category.{v_2, u_5} V] {FV : V → V → Type u_7}
  {CV : V → Type u_8} [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
  [inst_2 : CategoryTheory.ConcreteCategory V FV] [inst_3 : CategoryTheory.HasForget₂ V TopCat]
  [inst_4 : CategoryTheory.Category.{v_3, u_6} W] {FW : W → W → Type u_9} {CW : W → Type u_10}
  [inst_5 : (X Y : W) → FunLike (FW X Y) (CW X) (CW Y)] [inst_6 : CategoryTheory.ConcreteCategory W FW]
  [inst_7 : CategoryTheory.HasForget₂ W TopCat] (G : Type u_11) [inst_8 : Monoid G] [inst_9 : TopologicalSpace G]
  (E : V ≌ W) (H₁ : ∀ (X : ContAction V G), ((E.functor.mapAction G).obj X.obj).IsContinuous)
  (H₂ : ∀ (X : ContAction W G), ((E.inverse.mapAction G).obj X.obj).IsContinuous),
  (CategoryTheory.Equivalence.mapContAction G E H₁ H₂).inverse = CategoryTheory.Functor.mapContAction G E.inverse H₂
-- Mathlib.GroupTheory.PresentedGroup
PresentedGroup.generated_by : ∀ {α : Type u_1} (rels : Set (FreeGroup α)) (H : Subgroup (PresentedGroup rels)),
  (∀ (j : α), PresentedGroup.of j ∈ H) → ∀ (x : PresentedGroup rels), x ∈ H
-- Mathlib.Algebra.Order.UpperLower
UpperSet.instAddCommMonoid.eq_1 : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedAddMonoid α],
  UpperSet.instAddCommMonoid =
    { toAddSemigroup := UpperSet.addCommSemigroup.toAddSemigroup, toZero := UpperSet.instZero, zero_add := ⋯,
      add_zero := ⋯, nsmul := nsmulRecAuto, nsmul_zero := ⋯, nsmul_succ := ⋯, add_comm := ⋯ }
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.right_inv : ∀ {X : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G X] {f : Equidecomp X G} {x : X},
  x ∈ f.target → ↑f.toPartialEquiv (↑f.symm x) = x
-- Mathlib.MeasureTheory.SetAlgebra
MeasureTheory.generateSetAlgebra.below.empty : ∀ {α : Type u_2} {𝒜 : Set (Set α)} {motive : (a : Set α) → MeasureTheory.generateSetAlgebra 𝒜 a → Prop},
  MeasureTheory.generateSetAlgebra.below ⋯
-- Mathlib.Computability.StateTransition
StateTransition.reaches₁_eq : ∀ {σ : Type u_1} {f : σ → Option σ} {a b c : σ},
  f a = f b → (StateTransition.Reaches₁ f a c ↔ StateTransition.Reaches₁ f b c)
-- Std.Time.Internal.UnitVal
Std.Time.Internal.UnitVal.instToString : {n : ℚ} → ToString (Std.Time.Internal.UnitVal n)
-- Mathlib.NumberTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.IsDedekindDomain.emultiplicity_map_eq_ramificationIdx'_mul`.

---

If `v` is an irreducible ideal of `R`, `w` is an irreducible ideal of `S` lying over `v`, and
`I` is an ideal of `R`, then the multiplicity of `w` in `I.map (algebraMap R S)` is given by
the multiplicity of `v` in `I` multiplied by the ramification index of `w` over `v`.  -/
Ideal.IsDedekindDomain.emultiplicity_map_eq_ramificationIdx_mul : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDedekindDomain S]
  [IsDedekindDomain R] [FaithfulSMul R S] {v : Ideal R} {w : Ideal S} {I : Ideal R},
  I ≠ ⊥ →
    Irreducible v →
      Irreducible w →
        w ≠ ⊥ →
          ∀ [w.LiesOver v], emultiplicity w (Ideal.map (algebraMap R S) I) = ↑(v.ramificationIdx' w) * emultiplicity v I
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.ForgetEnrichment.equiv_functor : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {D : Type u''}
  [inst_2 : CategoryTheory.Category.{v'', u''} D] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V D],
  (CategoryTheory.ForgetEnrichment.equiv V).functor = CategoryTheory.ForgetEnrichment.equivFunctor V D
-- Mathlib.Order.CompleteLattice.Basic
Prod.snd_iInf : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : InfSet α] [inst_1 : InfSet β] (f : ι → α × β),
  (iInf f).2 = ⨅ i, (f i).2
-- Mathlib.Order.Filter.Basic
Filter.inter_mem_iff : ∀ {α : Type u} {f : Filter α} {s t : Set α}, s ∩ t ∈ f ↔ s ∈ f ∧ t ∈ f
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.dec.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (n : ℕ) (check persistent : Bool) (objs? : Option ℕ)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_13),
  sizeOf (Lean.Compiler.LCNF.CodeDecl.dec fvarId n check persistent objs? h) =
    1 + sizeOf fvarId + sizeOf n + sizeOf check + sizeOf persistent + sizeOf objs? + sizeOf h
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.self_le_maxKey?_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k} {kmi : α},
  (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.maxKey?.get ⋯ = kmi → (compare k kmi).isLE = true
-- Init.Data.Nat.Basic
Nat.le_of_add_le_add_right : ∀ {a b c : ℕ}, a + b ≤ c + b → a ≤ c
-- Mathlib.Analysis.SpecificLimits.Basic
Set.Countable.exists_pos_hasSum_le : ∀ {ι : Type u_4} {s : Set ι},
  s.Countable → ∀ {ε : ℝ}, 0 < ε → ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum (fun i => ε' ↑i) c ∧ c ≤ ε
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.Approx.head'.eq_1 : ∀ {F : PFunctor.{uA, uB}} (x : ℕ) (i : F.A) (a : F.B i → PFunctor.Approx.CofixA F x),
  PFunctor.Approx.head' (PFunctor.Approx.CofixA.intro i a) = i
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_zero_one : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] [inst_3 : FloorRing α]
  (b : α), toIcoDiv ⋯ 0 b = ⌊b⌋
-- Mathlib.CategoryTheory.Yoneda
/-- The "Coyoneda evaluation" functor, which sends `X : C` and `F : C ⥤ Type`
to `F.obj X`, functorially in both `X` and `F`.
 -/
CategoryTheory.coyonedaEvaluation : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.Functor (C × CategoryTheory.Functor C (Type v₁)) (Type (max u₁ v₁))
-- Mathlib.RingTheory.IdealFilter.Topology
/-- The additive-group filter basis whose sets are the ideals belonging to the ideal filter `F`.  -/
IdealFilter.addGroupFilterBasis : {A : Type u_1} → [inst : Ring A] → IdealFilter A → AddGroupFilterBasis A
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec64_or : ∀ (a b : ISize) (h : System.Platform.numBits = 64), (a ||| b).toBitVec64 h = a.toBitVec64 h ||| b.toBitVec64 h
-- Lean.Parser.Term
Lean.Parser.Term.letConfigItem.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.TensorProduct.Basic
/-- `S ⊗[R] T` has a `T`-algebra structure. This is not a global instance or else the action of
`S` on `S ⊗[R] S` would be ambiguous.  -/
Algebra.TensorProduct.rightAlgebra : {R : Type uR} →
  {A : Type uA} →
    {B : Type uB} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] → [inst_3 : CommSemiring B] → [inst_4 : Algebra R B] → Algebra B (TensorProduct R A B)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.startsWith_slice_eq_false_iff : ∀ {pat : String.Slice} {s : String}, s.startsWith pat = false ↔ ¬pat.copy.toList <+: s.toList
-- Std.Do.PostCond
/-- Entailment of exception assertions is defined as pointwise entailment of the assertions for each
potential exception.

While implication of exception conditions (`ExceptConds.imp`) is itself an exception condition,
entailment is an ordinary proposition.
 -/
Std.Do.ExceptConds.entails : {ps : Std.Do.PostShape} → Std.Do.ExceptConds ps → Std.Do.ExceptConds ps → Prop
-- Mathlib.Order.Shrink
instOrderBotShrink.eq_1 : ∀ {α : Type u_1} [inst : Small.{u, u_1} α] [inst_1 : Preorder α] [inst_2 : OrderBot α],
  instOrderBotShrink = { toBot := instBotShrink, bot_le := ⋯ }
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.instBEqSimpCacheKey : BEq Lean.Elab.Tactic.Grind.SimpCacheKey
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.piCongrRight_symm : ∀ {η : Type u_16} {Ms : η → Type u_17} {Ns : η → Type u_18} [inst : (j : η) → Add (Ms j)]
  [inst_1 : (j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j),
  (AddEquiv.piCongrRight es).symm = AddEquiv.piCongrRight fun i => (es i).symm
-- Mathlib.SetTheory.ZFC.Class
/-- The union of a class is the class of all members of ZFC sets in the class. Uses `⋃₀` notation,
scoped under the `Class` namespace.  -/
Class.sUnion : Class.{u_1} → Class.{u_1}
-- Mathlib.Algebra.Ring.Subsemiring.Defs
RingHom.mem_eqLocusS : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {f g : R →+* S} {x : R},
  x ∈ f.eqLocusS g ↔ f x = g x
-- Mathlib.Analysis.Complex.RemovableSingularity
Complex.differentiableOn_compl_singleton_and_continuousAt_iff : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {s : Set ℂ}
  {c : ℂ}, s ∈ nhds c → (DifferentiableOn ℂ f (s \ {c}) ∧ ContinuousAt f c ↔ DifferentiableOn ℂ f s)
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
/-- Note that equality need not hold: consider `ι := Bool, p := (·), α := ℤ, f := fun _ ↦ -1`,
then the LHS is `-1` but the RHS is `-1 ⊔ sSup ∅ = -1 ⊔ 0 = 0`.  -/
ciSup_exists_le : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {p : ι → Prop} {f : Exists p → α},
  ⨆ (ih : Exists p), f ih ≤ ⨆ i, ⨆ (h : p i), f ⋯
-- Mathlib.Topology.IsLocalHomeomorph
/-- The function `f` is injective on the target of `localInverseAt x`.  -/
IsLocalHomeomorph.injOn_localInverseAt_target : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}
  (hf : IsLocalHomeomorph f) {x : X}, Set.InjOn f (hf.localInverseAt x).target
-- Mathlib.Algebra.Field.Subfield.Defs
/-- A subfield contains the field's 0.  -/
Subfield.zero_mem : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K), 0 ∈ s
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.compl_singleton : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (a : α), {a}ᶜ = Finset.univ.erase a
-- Mathlib.Geometry.Euclidean.Sphere.SecondInter
/-- If the vector passed to `secondInter` is given by a subtraction involving the point in
`secondInter`, and the second point is inside the sphere, the second point is strictly between
the first point and the result of `secondInter`.  -/
EuclideanGeometry.Sphere.sbtw_secondInter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p p' : P},
  p ∈ s → dist p' s.center < s.radius → Sbtw ℝ p p' (s.secondInter p (p' -ᵥ p))
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.trailingDegree_one_le : ∀ {R : Type u} [inst : Semiring R], 0 ≤ Polynomial.trailingDegree 1
-- Mathlib.Tactic.Linter.Header
/-- The text required by `linter.style.header` as the second line of the header.  -/
Mathlib.Linter.linter.style.header.license : Lean.Option String
-- Init.Meta.Defs
/-- Syntax that represents a universe level.
 -/
Lean.Syntax.Level : Type
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.exists_iso_binaryBiproduct_of_distTriang : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    T.mor₃ = 0 →
      ∃ e,
        CategoryTheory.CategoryStruct.comp T.mor₁ e.hom = CategoryTheory.Limits.biprod.inl ∧
          T.mor₂ = CategoryTheory.CategoryStruct.comp e.hom CategoryTheory.Limits.biprod.snd
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.subset_closure_iff_forall_subset_isFlat : ∀ {α : Type u_2} {M : Matroid α} {Y : Set α} (X : Set α),
  autoParam (X ⊆ M.E) Matroid.subset_closure_iff_forall_subset_isFlat._auto_1 →
    (Y ⊆ M.closure X ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → Y ⊆ F)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.entails_5 : ∀ {σ₁ σ₂ σ₃ σ₄ σ₅ : Type u_1} {P Q : Std.Do.SPred [σ₁, σ₂, σ₃, σ₄, σ₅]},
  P ⊢ₛ Q ↔ ∀ (s₁ : σ₁) (s₂ : σ₂) (s₃ : σ₃) (s₄ : σ₄) (s₅ : σ₅), (P s₁ s₂ s₃ s₄ s₅).down → (Q s₁ s₂ s₃ s₄ s₅).down
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
ModelWithCorners.mdifferentiable : ∀ {𝕜 : 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), MDiff ↑I
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
AnalyticOnNhd.fderiv_of_isOpen : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E}, AnalyticOnNhd 𝕜 f s → IsOpen s → AnalyticOnNhd 𝕜 (fderiv 𝕜 f) s
-- Lean.Language.Basic
Lean.Language.SnapshotTask.ReportingRange.skip.sizeOf_spec : sizeOf Lean.Language.SnapshotTask.ReportingRange.skip = 1
-- Mathlib.Algebra.Star.LinearMap
/-- A star-preserving linear map is self-adjoint (with respect to the intrinsic star).  -/
IntrinsicStar.StarHomClass.isSelfAdjoint : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring R] [inst_1 : InvolutiveStar R]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : StarAddMonoid E] [inst_5 : StarModule R E]
  [inst_6 : AddCommMonoid F] [inst_7 : Module R F] [inst_8 : StarAddMonoid F] [inst_9 : StarModule R F] {S : Type u_4}
  [inst_10 : FunLike S E F] [inst_11 : LinearMapClass S R E F] [StarHomClass S E F] {f : S},
  IsSelfAdjoint (WithConv.toConv ↑f)
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.lift_t : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {φ : ↥A ≃* ↥B} {H : Type u_2} [inst_1 : Group H] (f : G →* H)
  (x : H) (hx : ∀ (a : ↥A), x * f ↑a = f ↑(φ a) * x), (HNNExtension.lift f x hx) HNNExtension.t = x
-- Init.Data.SInt.Lemmas
ISize.toInt64_mod : ∀ (a b : ISize), (a % b).toInt64 = a.toInt64 % b.toInt64
-- Mathlib.Order.SuccPred.Relation
/-- For `m < n`, `(n, m)` is in the transitive closure of a relation `~` if `succ i ~ i`
for all `i` between `n` and `m`.  -/
transGen_of_succ_of_gt : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] (r : α → α → Prop) {n m : α},
  (∀ i ∈ Set.Ico m n, r (Order.succ i) i) → m < n → Relation.TransGen r n m
-- Mathlib.Data.Nat.Prime.Defs
Nat.minFac_prime_iff : ∀ {n : ℕ}, Nat.Prime n.minFac ↔ n ≠ 1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.insertManyIfNewUnit_list_eq_foldl : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α (fun x => Unit) cmp} [inst : Std.TransCmp cmp]
  {l : List α}, Std.ExtDTreeMap.Const.insertManyIfNewUnit t l = List.foldl (fun acc a => acc.insertIfNew a ()) t l
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.val_logOrderIso_symm_apply : ∀ {G : Type u_3} [inst : Preorder G] [inst_1 : AddGroup G] (a : G),
  ↑((RelIso.symm WithZero.logOrderIso) a) = ↑(Multiplicative.ofAdd a)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.paramSet.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.fundamentalCone.paramSet K =
    Set.univ.pi fun w => if w = NumberField.Units.dirichletUnitTheorem.w₀ then Set.Iic 0 else Set.Ico 0 1
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.isRestriction_iff_exists_eq_delete : ∀ {α : Type u_1} {M N : Matroid α}, N.IsRestriction M ↔ ∃ D ⊆ M.E, N = M.delete D
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.and_assoc : ∀ {σs : List (Type u)} {P Q R : Std.Do.SPred σs}, (P ∧ Q) ∧ R ⊣⊢ₛ P ∧ Q ∧ R
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Comma.coconeOfPreserves_ι_app_right : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {A : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  {B : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃}
  [inst_3 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
  (F : CategoryTheory.Functor J (CategoryTheory.Comma L R))
  [inst_4 : CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L]
  {c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁)
  (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))) (j : J),
  ((CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).ι.app j).right = c₂.ι.app j
-- Mathlib.Probability.Process.Adapted
MeasureTheory.IsProgressive.neg : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} {u : ι → Ω → β} {mi : MeasurableSpace ι} {mβ : MeasurableSpace β} [inst_1 : AddGroup β]
  [MeasurableNeg β], MeasureTheory.IsProgressive f u → MeasureTheory.IsProgressive f fun i ω => -u i ω
-- Lean.Elab.Open
Lean.Elab.OpenDecl.State.openDecls : Lean.Elab.OpenDecl.State → List Lean.OpenDecl
-- Mathlib.Algebra.BigOperators.Pi
prod_indicator : ∀ {ι : Type u_1} {κ : Type u_2} {R : Type u_5} [inst : CommSemiring R] (s : Finset ι) (f : ι → Set κ) (g : ι → κ → R),
  ∏ i ∈ s, (f i).indicator (g i) = (⋂ x ∈ s, f x).indicator (∏ i ∈ s, g i)
-- Mathlib.Algebra.Free
/-- Associativity relations for an additive magma.  -/
AddMagma.AssocRel : (α : Type u) → [Add α] → α → α → Prop
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndependent.repr.eq_1 : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (hv : LinearIndependent R v), hv.repr = ↑hv.linearCombinationEquiv.symm
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_alter_le_size : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, (t.alter k f).size ≤ t.size + 1
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.tendsto_atTop_r : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r) (i : α), Filter.Tendsto (r i) Filter.atTop Filter.atTop
-- Mathlib.Analysis.Normed.Group.Uniform
AntilipschitzWith.le_mul_norm_div : ∀ {F : Type u_3} [inst : SeminormedCommGroup F] {E : Type u_5} [inst_1 : SeminormedCommGroup E] {K : NNReal}
  {f : E → F}, AntilipschitzWith K f → ∀ (x y : E), ‖x⁻¹ * y‖ ≤ ↑K * ‖(f x)⁻¹ * f y‖
-- Mathlib.Analysis.Complex.CanonicalDecomposition
/-- A proof that `g` does not vanish on the closed ball.  -/
Complex.ECanonicalDecomp.ne_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : ℂ → E} {R : ℝ},
  Complex.ECanonicalDecomp f g R → ∀ u ∈ Metric.closedBall 0 R, g u ≠ 0
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.neg_add_cancel_left : ∀ {α : Type u} [inst : SubtractionMonoid α] {a : α}, IsAddUnit a → ∀ (b : α), -a + (a + b) = b
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mfderiv_add : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {z : M} {f g : M → E'},
  MDiffAt f z → MDiffAt g z → mfderiv% (f + g) z = mfderiv% f z + mfderiv% g z
-- Mathlib.NumberTheory.LegendreSymbol.Basic
ZMod.mod_four_ne_three_of_sq_eq_neg_sq : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {x y : ZMod p}, x ≠ 0 → x ^ 2 = -y ^ 2 → p % 4 ≠ 3
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_out : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M]
  (A : ArchimedeanClass M), ArchimedeanClass.mk A.out = A
-- Mathlib.NumberTheory.Fermat
Nat.odd_fermatNumber : ∀ (n : ℕ), Odd n.fermatNumber
-- Mathlib.Topology.Order.OrderClosed
/-- The set `{ (x, y) | x ≤ y }` is a closed set.  -/
OrderClosedTopology.isClosed_le' : ∀ {α : Type u_1} {inst : TopologicalSpace α} {inst_1 : Preorder α} [self : OrderClosedTopology α],
  IsClosed {p | p.1 ≤ p.2}
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addU_of_Z_eq_zero_right : ∀ {F : Type u} [inst : Field F] {P Q : Fin 3 → F}, Q 2 = 0 → WeierstrassCurve.Jacobian.addU P Q = 0
-- Mathlib.Data.Seq.Computation
Computation.destruct_empty : ∀ {α : Type u}, (Computation.empty α).destruct = Sum.inr (Computation.empty α)
-- Mathlib.NumberTheory.Divisors
Nat.mem_properDivisors_prime_pow : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ) {x : ℕ}, x ∈ (p ^ k).properDivisors ↔ ∃ j, ∃ (_ : j < k), x = p ^ j
-- Mathlib.Order.Antisymmetrization
/-- **Alias** of the forward direction of `le_iff_lt_or_antisymmRel`. -/
LE.le.lt_or_antisymmRel : ∀ {α : Type u_1} {a b : α} [inst : Preorder α], a ≤ b → a < b ∨ AntisymmRel (fun x1 x2 => x1 ≤ x2) a b
-- Mathlib.CategoryTheory.Filtered.Small
/-- The realization function sends the abstract maxima and weak coequalizers to the corresponding
objects in `C`.  -/
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsFiltered.FilteredClosureSmall.inductiveStepRealization : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.IsFilteredOrEmpty C] →
      (n : ℕ) →
        (X : (k : ℕ) → k < n → (t : Type (max v w)) × (t → C)) →
          CategoryTheory.IsFiltered.FilteredClosureSmall.InductiveStep✝ n X → C
-- Mathlib.CategoryTheory.Types.Monomorphisms
CategoryTheory.Types.instIsStableUnderCobaseChangeMonomorphismsType : (CategoryTheory.MorphismProperty.monomorphisms (Type u)).IsStableUnderCobaseChange
-- Mathlib.Algebra.Lie.Ideal
/-- See also `LieIdeal.map_comap_eq`.  -/
LieIdeal.comap_map_le : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L},
  I ≤ LieIdeal.comap f (LieIdeal.map f I)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_of_getKey?_eq_some : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] {a a' : α},
  t.WF → t.getKey? a = some a' → a' ∈ t
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.fromRows_mul : ∀ {R : Type u_1} {m : Type u_2} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [inst : Semiring R] [inst_1 : Fintype n]
  (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (B : Matrix n m R), A₁.fromRows A₂ * B = (A₁ * B).fromRows (A₂ * B)
-- Mathlib.Data.Matrix.Diagonal
Matrix.instAddGroupWithOne : {n : Type u_3} → {α : Type v} → [DecidableEq n] → [AddGroupWithOne α] → AddGroupWithOne (Matrix n n α)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
/-- **Alias** of the reverse direction of `Units.one_le_inv`. -/
Units.one_le_inv_of_le : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulLeftMono M] (u : Mˣ), ↑u ≤ 1 → 1 ≤ ↑u⁻¹
-- Mathlib.Algebra.Group.AddChar
/-- The values of an additive character on an additive group are units.  -/
AddChar.val_isUnit : ∀ {A : Type u_1} {M : Type u_2} [inst : AddGroup A] [inst_1 : Monoid M] (φ : AddChar A M) (a : A), IsUnit (φ a)
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosSemidef.smul : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] {α : Type u_5}
  [inst_3 : CommSemiring α] [inst_4 : PartialOrder α] [inst_5 : StarRing α] [StarOrderedRing α] [inst_7 : Algebra α R]
  [StarModule α R] [PosSMulMono α R] {x : Matrix n n R}, x.PosSemidef → ∀ {a : α}, 0 ≤ a → (a • x).PosSemidef