mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.EReal.Operations
EReal.neg_nonneg : ∀ {a : EReal}, 0 ≤ -a ↔ a ≤ 0
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.evariance.eq_1 : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.evariance X μ = ∫⁻ (ω : Ω), ‖X ω - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2 ∂μ
-- Lean.DocString.Types
Lean.Doc.Block.brecOn_7.eq : ∀ {i : Type u} {b : Type v} {motive_1 : Lean.Doc.Block i b → Sort u_1}
  {motive_2 : Array (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1}
  {motive_3 : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1}
  {motive_4 : Array (Lean.Doc.Block i b) → Sort u_1}
  {motive_5 : List (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1}
  {motive_6 : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1}
  {motive_7 : List (Lean.Doc.Block i b) → Sort u_1} {motive_8 : Lean.Doc.ListItem (Lean.Doc.Block i b) → Sort u_1}
  {motive_9 : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b) → Sort u_1}
  (t : Lean.Doc.ListItem (Lean.Doc.Block i b)) (F_1 : (t : Lean.Doc.Block i b) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.Doc.ListItem (Lean.Doc.Block i b))) → Lean.Doc.Block.below_1 t → motive_2 t)
  (F_3 :
    (t : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) → Lean.Doc.Block.below_2 t → motive_3 t)
  (F_4 : (t : Array (Lean.Doc.Block i b)) → Lean.Doc.Block.below_3 t → motive_4 t)
  (F_5 : (t : List (Lean.Doc.ListItem (Lean.Doc.Block i b))) → Lean.Doc.Block.below_4 t → motive_5 t)
  (F_6 :
    (t : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) → Lean.Doc.Block.below_5 t → motive_6 t)
  (F_7 : (t : List (Lean.Doc.Block i b)) → Lean.Doc.Block.below_6 t → motive_7 t)
  (F_8 : (t : Lean.Doc.ListItem (Lean.Doc.Block i b)) → Lean.Doc.Block.below_7 t → motive_8 t)
  (F_9 : (t : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Lean.Doc.Block.below_8 t → motive_9 t),
  Lean.Doc.Block.brecOn_7 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 =
    F_8 t (Lean.Doc.Block.brecOn_7.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9).2
-- Init.Data.Int.Lemmas
_private.Init.Data.Int.Lemmas.0.Int.negSucc_mul_ofNat' : ∀ (m n : ℕ), Int.negSucc m * ↑n = Int.negOfNat (m.succ * n)
-- Mathlib.Analysis.SpecialFunctions.Bernstein
/-- Send `k : Fin (n+1)` to the equally spaced points `k/n` in the unit interval.
 -/
bernstein.z : {n : ℕ} → Fin (n + 1) → ↑unitInterval
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.normalizer_commutator_ge_right : ∀ {G : Type u_1} [inst : Group G] (H₁ H₂ : Subgroup G), H₂ ≤ Subgroup.normalizer ↑⁅H₁, H₂⁆
-- Mathlib.Topology.Constructible
IsRetrocompact.biInter : ∀ {X : Type u_2} [inst : TopologicalSpace X] [T2Space X] {ι : Type u_4} {f : ι → Set X} {t : Set ι},
  t.Finite → (∀ i ∈ t, IsRetrocompact (f i)) → IsRetrocompact (⋂ i ∈ t, f i)
-- Mathlib.Topology.EMetricSpace.Basic
EMetric.subsingleton_iff_indiscreteTopology : ∀ {α : Type u_2} [inst : EMetricSpace α], Subsingleton α ↔ IndiscreteTopology α
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.support_nonempty : ∀ {α : Type u_1} (p : PMF α), p.support.Nonempty
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The negative of a `C^n` function is `C^n`.  -/
ContDiff.neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {f : E → F}, ContDiff 𝕜 n f → ContDiff 𝕜 n fun x => -f x
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_filter_eq_false_iff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {f : α → β → Bool}, (Std.HashMap.filter f m).isEmpty = false ↔ ∃ k, ∃ (h : k ∈ m), f (m.getKey k h) m[k] = true
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.monic_of_isUnit_leadingCoeff_inv_smul : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} (h : IsUnit p.leadingCoeff), (h.unit⁻¹ • p).Monic
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toList_rco : ∀ {m n : ℤ} {i : ℕ}, (m...n).toList[i]! = if i < (n - m).toNat then m + ↑i else 0
-- Mathlib.Algebra.Lie.Weights.Basic
/-- See also the more useful form `LieModule.zero_genWeightSpace_eq_top_of_nilpotent`.  -/
LieModule.zero_genWeightSpace_eq_top_of_nilpotent' : ∀ {R : Type u_2} {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [LieModule.IsNilpotent L M], LieModule.genWeightSpace M 0 = ⊤
-- Init.Data.SInt.Lemmas
ISize.lt_irrefl : ∀ {a : ISize}, ¬a < a
-- Init.Data.Vector.Lex
Vector.lex_eq_false_iff_ge : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] [LawfulBEq α] [inst_2 : LT α] [inst_3 : DecidableLT α] {xs ys : Vector α n},
  (xs.lex ys fun x1 x2 => decide (x1 < x2)) = false ↔ ys ≤ xs
-- Init.Data.SInt.Bitwise
Int64.not_eq_neg_add : ∀ (a : Int64), ~~~a = -a - 1
-- Mathlib.RingTheory.PicardGroup
/-- The image of an invertible `R`-submodule `I ⊆ A` under `unitsToPic` is isomorphic to `I`.  -/
Submodule.unitsToPicEquiv : {R : Type u} →
  {A : Type u_4} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] →
          [inst_3 : FaithfulSMul R A] → (I : (Submodule R A)ˣ) → ((Submodule.unitsToPic R A) I).AsModule ≃ₗ[R] ↥↑I
-- Mathlib.FieldTheory.Normal.Defs
AlgEquiv.restrictNormal_eq_one_iff : ∀ {F : Type u_1} [inst : Field F] {K₁ : Type u_3} [inst_1 : Field K₁] [inst_2 : Algebra F K₁]
  (L : IntermediateField F K₁) [inst_3 : Normal F ↥L] (σ : Gal(K₁/F)), σ.restrictNormal ↥L = 1 ↔ ∀ x ∈ L, σ x = x
-- Mathlib.CategoryTheory.Filtered.OfColimitCommutesFiniteLimit
/-- A converse to `colimitLimitIso`: if colimits of shape `K` commute with finite
limits, then `K` is filtered.  -/
CategoryTheory.isFiltered_of_nonempty_limit_colimit_to_colimit_limit : ∀ {K : Type v} [inst : CategoryTheory.SmallCategory K],
  (∀ {J : Type v} [inst_1 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J]
      (F : CategoryTheory.Functor J (CategoryTheory.Functor K (Type v))),
      Nonempty
        (CategoryTheory.Limits.limit (CategoryTheory.Limits.colimit F.flip) ⟶
          CategoryTheory.Limits.colimit (CategoryTheory.Limits.limit F))) →
    CategoryTheory.IsFiltered K
-- Mathlib.Logic.Basic
Classical.choose_eq' : ∀ {α : Sort u_1} (a : α), ⋯.choose = a
-- Mathlib.RingTheory.IsPrimary
Submodule.IsPrimary.radical_colon_singleton_of_notMem : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {S : Submodule R M}, S.IsPrimary → ∀ {m : M}, m ∉ S → (S.colon {m}).radical = (S.colon Set.univ).radical
-- Mathlib.RingTheory.Algebraic.Basic
Algebra.transcendental_of_subsingleton : ∀ (R : Type u) (A : Type v) [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] [Subsingleton R],
  Algebra.Transcendental R A
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.monoidalCategoryOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.MonoidalCategory C] → CategoryTheory.MonoidalCategory Cᵒᵖ
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageDirection.serverToClient : Lean.JsonRpc.MessageDirection
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMultispan.left : {J : CategoryTheory.Limits.MultispanShape} → J.L → CategoryTheory.Limits.WalkingMultispan J
-- Init.GrindInstances.ToInt
Lean.Grind.instZeroUInt32UintOfNatNat : Lean.Grind.ToInt.Zero UInt32 (Lean.Grind.IntInterval.uint 32)
-- Mathlib.Data.Finsupp.SMul
IsSMulRegular.finsupp : ∀ {α : Type u_1} {M : Type u_3} {R : Type u_6} [inst : Zero M] [inst_1 : SMulZeroClass R M] {k : R},
  IsSMulRegular M k → IsSMulRegular (α →₀ M) k
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0to1.Λ'.act : {Γ : Type u_1} → {Λ : Type u_2} → Turing.TM0.Stmt Γ → Λ → Turing.TM0to1.Λ' Γ Λ
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.instIsScalarTower_closedBall_closedBall : IsScalarTower Complex.UnitClosedDisc Complex.UnitClosedDisc Complex.UnitDisc
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.whisker_right : ∀ {B : Type u} [inst : Quiver B] {a b c : B} (f g : CategoryTheory.FreeBicategory.Hom a b)
  (h : CategoryTheory.FreeBicategory.Hom b c) (η η' : CategoryTheory.FreeBicategory.Hom₂ f g),
  CategoryTheory.FreeBicategory.Rel η η' →
    CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.whisker_right h η)
      (CategoryTheory.FreeBicategory.Hom₂.whisker_right h η')
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_eq_of_forall_row_eq_smul_add_const_aux : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {A B : Matrix n n R}
  {s : Finset n} (c : n → R), (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
-- Batteries.Lean.EStateM
_private.Batteries.Lean.EStateM.0.EStateM.run_bind.match_1.splitter : {ε σ α : Type u_1} →
  (motive : EStateM.Result ε σ α → Sort u_2) →
    (x : EStateM.Result ε σ α) →
      ((x : α) → (s : σ) → motive (EStateM.Result.ok x s)) →
        ((e : ε) → (s : σ) → motive (EStateM.Result.error e s)) → motive x
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.pointReflection_apply : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] (x y : P),
  (AffineIsometryEquiv.pointReflection 𝕜 x) y = (x -ᵥ y) +ᵥ x
-- Mathlib.Algebra.Free
instReprFreeMagma.eq_1 : ∀ {α : Type u} [inst : Repr α], instReprFreeMagma = { reprPrec := fun o x => o.repr }
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone_cocone_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type w}
  [inst_1 : CategoryTheory.Limits.HasFiniteCoproducts C]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape (Finset (CategoryTheory.Discrete α)) C]
  (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C),
  (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone F).cocone.pt =
    CategoryTheory.Limits.colimit (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj F)
-- Batteries.Data.HashMap.Basic
Batteries.HashMap.instEmptyCollection : {α : Type u_1} → {β : Type u_2} → [inst : BEq α] → [inst_1 : Hashable α] → EmptyCollection (Batteries.HashMap α β)
-- Mathlib.Order.CompleteLattice.Defs
CompleteLattice.toSupSet : {α : Type u_8} → [self : CompleteLattice α] → SupSet α
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_surjective : ∀ {R : Type u} [inst : Semiring R] (x : R), Function.Surjective (Polynomial.eval x)
-- Mathlib.Tactic.NormNum.Core
/-- The state of the `norm_num` extension environment  -/
Mathlib.Meta.NormNum.NormNums : Type
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- If we replace a column of a matrix by a linear combination of its columns, then the determinant
is multiplied by the coefficient of that column.  -/
Matrix.det_updateCol_sum : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (A : Matrix n n R)
  (j : n) (c : n → R), (A.updateCol j fun k => ∑ i, c i • A k i).det = c j • A.det
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_filter_key : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → Bool} {k : α},
  t.WF → (k ∈ Std.DTreeMap.Raw.filter (fun a x => f a) t ↔ ∃ (h : k ∈ t), f (t.getKey k h) = true)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyMap'_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData)
  (h₃ : S₃.HomologyData),
  CategoryTheory.ShortComplex.homologyMap' (CategoryTheory.CategoryStruct.comp φ₁ φ₂) h₁ h₃ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap' φ₁ h₁ h₂)
      (CategoryTheory.ShortComplex.homologyMap' φ₂ h₂ h₃)
-- Mathlib.Tactic.Simps.Basic
Simps.instInhabitedConfig.default : Simps.Config
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
RootPairing.Base.cartanMatrix.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : P.IsCrystallographic], b.cartanMatrix = RootPairing.Base.cartanMatrixIn ℤ b
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.mem_vanishingIdeal : ∀ {R : Type u} [inst : CommSemiring R] (t : Set (PrimeSpectrum R)) (f : R),
  f ∈ PrimeSpectrum.vanishingIdeal t ↔ ∀ x ∈ t, f ∈ x.asIdeal
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.inv_zero : ∀ {α : Type u_1} [inst : Inv α], 0⁻¹ = 0
-- Mathlib.Algebra.Algebra.Unitization
Unitization.equiv_apply : ∀ {R : Type u_1} {A : Type u_2} (self : Unitization R A), Unitization.equiv self = self.toProd
-- Mathlib.CategoryTheory.Limits.Opposites
/-- If `F.leftOp : Jᵒᵖ ⥤ C` has a limit, we can construct a colimit for `F : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.hasColimit_of_hasLimit_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J Cᵒᵖ) [CategoryTheory.Limits.HasLimit F.leftOp], CategoryTheory.Limits.HasColimit F
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.nodup_keys : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α],
  m.keys.Nodup
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_hom_app_comp_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X : C} (g : Z ⟶ X)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g] (T : CategoryTheory.Over X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left ((CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback g).hom.app T))
      (CategoryTheory.Limits.pullback.fst T.hom g) =
    CategoryTheory.ChosenPullbacksAlong.fst T.hom g
-- Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits
_private.Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits.0.SimpleGraph.ErdosStone.filter.congr_simp : ∀ {n : ℕ} {G : SimpleGraph (Fin n)} {inst : DecidableRel G.Adj} [inst_1 : DecidableRel G.Adj] {r t' : ℕ}
  (K K_1 : G.CompleteEquipartiteSubgraph r t'),
  K = K_1 → ∀ (t t_1 : ℕ), t = t_1 → SimpleGraph.ErdosStone.filter✝ K t = SimpleGraph.ErdosStone.filter✝ K_1 t_1
-- Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
MeasureTheory.eLpNorm_star : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {R : Type u_5} [inst : NormedAddCommGroup R]
  [inst_1 : StarAddMonoid R] [NormedStarGroup R] {p : ENNReal} {f : α → R},
  MeasureTheory.eLpNorm (star f) p μ = MeasureTheory.eLpNorm f p μ
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.densityProcess_fst_univ_ae : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × β))
  [ProbabilityTheory.IsFiniteKernel κ] (n : ℕ) (a : α), ∀ᵐ (x : γ) ∂κ.fst a, κ.densityProcess κ.fst n a x Set.univ = 1
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
_private.Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.0.CategoryTheory.Limits.mapPair.match_1.splitter : (motive : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair → Sort u_1) →
  (x : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) →
    (Unit → motive { as := CategoryTheory.Limits.WalkingPair.left }) →
      (Unit → motive { as := CategoryTheory.Limits.WalkingPair.right }) → motive x
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.Ordinal.instDecidableEqOfDay : DecidableEq Std.Time.Nanosecond.Ordinal.OfDay
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
PresheafOfModules.ModuleColimit.jointly_surjective₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C]
  [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {cR : CategoryTheory.Limits.Cocone R} {hcR : CategoryTheory.Limits.IsColimit cR} {M : PresheafOfModules R}
  {cM : CategoryTheory.Limits.Cocone M.presheaf} {hcM : CategoryTheory.Limits.IsColimit cM} (r : ↑cR.pt)
  (m : PresheafOfModules.ModuleColimit hcR hcM),
  ∃ U a x, (PresheafOfModules.ModuleColimit.ιR cR) a = r ∧ PresheafOfModules.ModuleColimit.ιM x = m
-- Mathlib.Data.Vector.MapLemmas
List.Vector.map₂_map_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ζ : Type u_4} {n : ℕ} (xs : List.Vector α n) (ys : List.Vector β n)
  (f₁ : α → γ → ζ) (f₂ : β → γ),
  List.Vector.map₂ f₁ xs (List.Vector.map f₂ ys) = List.Vector.map₂ (fun x y => f₁ x (f₂ y)) xs ys
-- Mathlib.Logic.Nonempty
Nonempty.forall : ∀ {α : Sort u_3} {p : Nonempty α → Prop}, (∀ (h : Nonempty α), p h) ↔ ∀ (a : α), p ⋯
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_eq_getKeyD_default : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {a : α}, t.getKey! a = t.getKeyD a default
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : C ⥤ Dᵒᵖ` creates limits, then `F.leftOp : Cᵒᵖ ⥤ D` creates colimits.  -/
CategoryTheory.Limits.createsColimitsLeftOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C Dᵒᵖ) → [CategoryTheory.CreatesLimits F] → CategoryTheory.CreatesColimits F.leftOp
-- Init.Sym.Lemmas
Lean.Sym.Nat.lt_eq_true : ∀ (a b : ℕ), decide (a < b) = true → (a < b) = True
-- Mathlib.Order.Cover
WCovBy.trans_antisymm_rel : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, a ⩿ b → AntisymmRel (fun x1 x2 => x1 ≤ x2) b c → a ⩿ c
-- Batteries.Classes.RatCast
instCoeHTCTRatOfRatCast : {K : Type u_1} → [RatCast K] → CoeHTCT ℚ K
-- Mathlib.RingTheory.LocalRing.RingHom.Basic
/-- If `f : R →+* S` is a surjective local ring hom, then the induced units map is surjective.  -/
IsLocalRing.surjective_units_map_of_local_ringHom : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S),
  Function.Surjective ⇑f → IsLocalHom f → Function.Surjective ⇑(Units.map ↑f)
-- Mathlib.Data.Set.Lattice
Set.sInter_subset_sInter : ∀ {α : Type u_1} {S T : Set (Set α)}, S ⊆ T → ⋂₀ T ⊆ ⋂₀ S
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciSup_image : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {ι : Type u_5} {ι' : Type u_6} {s : Set ι} {f : ι → ι'}
  {g : ι' → α}, BddAbove (Set.range fun i => g (f ↑i)) → sSup ∅ ≤ ⨆ i, g (f ↑i) → ⨆ i ∈ f '' s, g i = ⨆ x ∈ s, g (f x)
-- Mathlib.Data.Set.Finite.Lattice
Set.finite_sdiff_iUnion_Ioo' : ∀ {α : Type u} [inst : LinearOrder α] (s : Set α), (s \ ⋃ x, Set.Ioo ↑x.1 ↑x.2).Finite
-- Mathlib.Algebra.BigOperators.Ring.Finset
Finset.sum_prod_piFinset : ∀ {ι : Type u_1} {κ : Type u_2} {R : Type u_4} [inst : CommSemiring R] [inst_1 : DecidableEq ι] [inst_2 : Fintype ι]
  (s : Finset κ) (g : ι → κ → R), ∑ f ∈ Fintype.piFinset fun x => s, ∏ i, g i (f i) = ∏ i, ∑ j ∈ s, g i j
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.row_submatrix_eq_comp : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {m₀ : Type u_10} {n₀ : Type u_11} (A : Matrix m n α) (r : m₀ → m)
  (c : n₀ → n) (i : m₀), (A.submatrix r c).row i = A.row (r i) ∘ c
-- Mathlib.Data.PSigma.Order
PSigma.Lex.noMinOrder_of_nonempty : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Preorder ι] [inst_1 : (i : ι) → Preorder (α i)] [NoMinOrder ι]
  [∀ (i : ι), Nonempty (α i)], NoMinOrder (Σₗ' (i : ι), α i)
-- Mathlib.Analysis.Convex.Basic
Set.OrdConnected.convex : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : Module 𝕜 E] [PosSMulMono 𝕜 E] {s : Set E},
  s.OrdConnected → Convex 𝕜 s
-- Mathlib.ModelTheory.Graph
/-- Any model of the theory of simple graphs represents a simple graph.  -/
FirstOrder.Language.simpleGraphOfStructure : (V : Type u) →
  [inst : FirstOrder.Language.graph.Structure V] → [V ⊨ FirstOrder.Language.Theory.simpleGraph] → SimpleGraph V
-- Std.Do.WP.Basic
Std.Do.Option.instWP : Std.Do.WP Option (Std.Do.PostShape.except PUnit.{u_1 + 1} Std.Do.PostShape.pure)
-- Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
IsDedekindDomain.FiniteAdeleRing.isUnit_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] {a : IsDedekindDomain.FiniteAdeleRing R K},
  IsUnit a ↔
    (∀ (v : IsDedekindDomain.HeightOneSpectrum R), a v ≠ 0) ∧
      ∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum R) in Filter.cofinite, Valued.v (a v) = 1
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.ofAlgEquiv_symm_of : ∀ {S : Type u_5} [inst : CommRing S] (I : Ideal S) [inst_1 : IsAdicComplete I S] (x : S),
  (AdicCompletion.ofAlgEquiv I).symm ((AdicCompletion.of I S) x) = x
-- Mathlib.Algebra.Category.Grp.Preadditive
AddCommGrpCat.hom_neg : ∀ {M N : AddCommGrpCat} (f : M ⟶ N), AddCommGrpCat.Hom.hom (-f) = -AddCommGrpCat.Hom.hom f
-- Mathlib.Data.Subtype
/-- Restrict a (dependent) function to a subtype  -/
Subtype.restrict : {α : Sort u_5} → {β : α → Type u_4} → (p : α → Prop) → ((x : α) → β x) → (x : Subtype p) → β ↑x
-- Mathlib.Algebra.Polynomial.Roots
/-- The multiset `nthRoots ↑n a` as a Finset. Previously `nthRootsFinset n` was defined to be
`nthRoots n (1 : R)` as a Finset. That situation can be recovered by setting `a` to be `(1 : R)`  -/
Polynomial.nthRootsFinset : ℕ → {R : Type u_1} → R → [inst : CommRing R] → [IsDomain R] → Finset R
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.containsThenInsertIfNew_eq_insertIfNewₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α)
  (b : β a), (m.containsThenInsertIfNew a b).2 = m.insertIfNewₘ a b
-- Mathlib.Tactic.Push
/-- Return `true` if `stx` is an underscore, i.e. `_` or `fun $_ => _`/`fun $_ ↦ _`.  -/
Mathlib.Tactic.Push.isUnderscore : Lean.Term → Bool
-- Mathlib.Computability.StateTransition
/-- (co-)Induction principle for `eval`. If a property `C` holds of any point `a` evaluating to `b`
which is either terminal (meaning `a = b`) or where the next point also satisfies `C`, then it
holds of any point where `eval f a` evaluates to `b`. This formalizes the notion that if
`eval f a` evaluates to `b` then it reaches terminal state `b` in finitely many steps.  -/
StateTransition.evalInduction : {σ : Type u_2} →
  {f : σ → Option σ} →
    {b : σ} →
      {C : σ → Sort u_1} →
        {a : σ} →
          b ∈ StateTransition.eval f a →
            ((a : σ) → b ∈ StateTransition.eval f a → ((a' : σ) → f a = some a' → C a') → C a) → C a
-- Std.Time.Format.Modifier
Std.Time.OffsetZ.full.sizeOf_spec : sizeOf Std.Time.OffsetZ.full = 1
-- Mathlib.Topology.UniformSpace.Equicontinuity
equicontinuousWithinAt_empty : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] [h : IsEmpty ι]
  (F : ι → X → α) (S : Set X) (x₀ : X), EquicontinuousWithinAt F S x₀
-- Init.Data.List.Basic
List.length_add_eq_lengthTRAux : ∀ {α : Type u} {as : List α} {n : ℕ}, as.length + n = as.lengthTRAux n
-- Mathlib.LinearAlgebra.BilinearForm.TensorProduct
LinearMap.BilinForm.baseChange_zero : ∀ {R : Type uR} {A : Type uA} {M₂ : Type uM₂} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Algebra R A] [inst_4 : Module R M₂], LinearMap.BilinForm.baseChange A 0 = 0