mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.CochainComplexOpposite
CochainComplex.homotopyOp.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {f g : K ⟶ L} (h : Homotopy f g),
  CochainComplex.homotopyOp h = { hom := fun p q => (h.hom (-q) (-p)).op, zero := ⋯, comm := ⋯ }
-- Mathlib.LinearAlgebra.FreeModule.PID
/-- If `S` a finite-dimensional ring extension of a PID `R` which is free as an `R`-module,
then any nonzero `S`-ideal `I` is free as an `R`-submodule of `S`, and we can
find a basis for `S` and `I` such that the inclusion map is a square diagonal
matrix.
 -/
Ideal.selfBasis_def : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R]
  {S : Type u_4} [inst_3 : CommRing S] [inst_4 : IsDomain S] [inst_5 : Algebra R S] [inst_6 : Finite ι]
  (b : Module.Basis ι R S) (I : Ideal S) (hI : I ≠ ⊥) (i : ι),
  ↑((Ideal.selfBasis b I hI) i) = Ideal.smithCoeffs b I hI i • (Ideal.ringBasis b I hI) i
-- Mathlib.Algebra.Group.Action.Opposite
MulOpposite.instIsCentralScalar : ∀ {M : Type u_1} {α : Type u_3} [inst : SMul M α] [inst_1 : SMul Mᵐᵒᵖ α] [IsCentralScalar M α], IsCentralScalar M αᵐᵒᵖ
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
/-- Given maps `f`, `g` from a manifold into a field `𝕜` and `𝕜`-vector space `V`, respectively, the
formula for the `mfderiv` (differential) of their scalar multiplication `f • g` in the direction of
the tangent vector `v`.

Mathematically speaking the formula is `d(f • g)(v) = f • dg(v) + df(v) • g`, but to get it to
typecheck we need a phrasing involving the canonical identification `NormedSpace.fromTangentSpace`
between the vector space `V` and the tangent space to this vector space at any point. This is
because two different tangent spaces (at `(f • g) x` and `g x`) appear in the equation.  -/
_private.Mathlib.Geometry.Manifold.MFDeriv.NormedSpace.0.fromTangentSpace_mfderiv_smul_apply : ∀ {𝕜 : 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] {x : M} {V : Type u_18} [inst_6 : NormedAddCommGroup V]
  [inst_7 : NormedSpace 𝕜 V] {f : M → 𝕜} {g : M → V},
  MDiffAt f x →
    MDiffAt g x →
      ∀ (v : TangentSpace I x),
        (NormedSpace.fromTangentSpace ((f • g) x)) ((mfderiv% (f • g) x) v) =
          f x • (NormedSpace.fromTangentSpace (g x)) ((mfderiv% g x) v) +
            (NormedSpace.fromTangentSpace (f x)) ((mfderiv% f x) v) • g x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.isSome_minKey?_modify_eq_isSome : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF → ∀ {k : α} {f : β → β}, (Std.DTreeMap.Internal.Impl.Const.modify k f t).minKey?.isSome = t.minKey?.isSome
-- Mathlib.InformationTheory.Hamming
hammingNorm.eq_1 : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)]
  [inst_2 : (i : ι) → Zero (β i)] (x : (i : ι) → β i), hammingNorm x = {i | x i ≠ 0}.card
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
AlgHom.compLeftContinuous.congr_simp : ∀ (R : Type u_2) [inst : CommSemiring R] {A : Type u_3} [inst_1 : TopologicalSpace A] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : IsTopologicalSemiring A] {A₂ : Type u_4} [inst_5 : TopologicalSpace A₂]
  [inst_6 : Semiring A₂] [inst_7 : Algebra R A₂] [inst_8 : IsTopologicalSemiring A₂] {α : Type u_5}
  [inst_9 : TopologicalSpace α] (g g_1 : A →ₐ[R] A₂) (e_g : g = g_1) (hg : Continuous ⇑g),
  AlgHom.compLeftContinuous R g hg = AlgHom.compLeftContinuous R g_1 ⋯
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.self_mem_span_image : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) [Nontrivial R] {i : ι} {s : Set ι}, b i ∈ Submodule.span R (⇑b '' s) ↔ i ∈ s
-- Mathlib.Order.Basic
le_of_subsingleton : ∀ {α : Type u_2} [inst : Preorder α] {a b : α} [Subsingleton α], a ≤ b
-- Mathlib.Order.GaloisConnection.Basic
GaloisCoinsertion.u_iSup_of_l_u_eq_self : ∀ {α : Type u} {β : Type v} {u : α → β} {l : β → α} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  (gi : GaloisCoinsertion l u) {ι : Sort x} (f : ι → α), (∀ (i : ι), l (u (f i)) = f i) → u (⨆ i, f i) = ⨆ i, u (f i)
-- Std.Sync.Channel
/-- Create a new channel. If:
- `capacity` is `none` it will be unbounded (the default)
- `capacity` is `some 0` it will always force a rendezvous between sender and receiver
- `capacity` is `some n` with `n > 0` it will use a buffer of size `n` and begin blocking once it
  is filled
 -/
Std.CloseableChannel.new : {α : Type} → optParam (Option ℕ) none → BaseIO (Std.CloseableChannel α)
-- Std.Tactic.BVDecide.LRAT.Parser
_private.Std.Tactic.BVDecide.LRAT.Parser.0.Std.Tactic.BVDecide.LRAT.lratProofToString.serializeIdList : Array ℕ → String
-- Mathlib.Data.List.Chain
List.IsChain.left_of_append : ∀ {α : Type u_1} {R : α → α → Prop} {l₁ l₂ : List α}, List.IsChain R (l₁ ++ l₂) → List.IsChain R l₁
-- Init.MetaTypes
Lean.NameGenerator.idx : Lean.NameGenerator → ℕ
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.expSeries_apply_eq_div' : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : Field 𝕂] [inst_1 : DivisionRing 𝔸] [inst_2 : Algebra 𝕂 𝔸]
  [inst_3 : TopologicalSpace 𝔸] [inst_4 : IsTopologicalRing 𝔸] (x : 𝔸),
  (fun n => (NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x) = fun n => x ^ n / ↑n.factorial
-- Mathlib.Data.Finset.SDiff
Finset.sdiff_inter_self_left : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), s \ (s ∩ t) = s \ t
-- Mathlib.Topology.Metrizable.Basic
TopologicalSpace.MetrizableSpace.subtype : ∀ {X : Type u_2} [inst : TopologicalSpace X] [TopologicalSpace.MetrizableSpace X] (s : Set X),
  TopologicalSpace.MetrizableSpace ↑s
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.union_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ m₃ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m₁.Equiv m₂ → (m₁ ∪ m₃).Equiv (m₂ ∪ m₃)
-- Mathlib.Algebra.Order.Group.Synonym
isRegular_toColex : ∀ {α : Type u_1} [inst : Monoid α] {a : α}, IsRegular (toColex a) ↔ IsRegular a
-- Lean.Parser.Extension
Lean.Parser.builtinParserCategoriesRef : IO.Ref Lean.Parser.ParserCategories
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF → ∀ {k a : α} {v : β k}, (t.insert k v).getKey! a = if cmp k a = Ordering.eq then k else t.getKey! a
-- Init.Data.List.Count
List.count_flatten : ∀ {α : Type u_1} [inst : BEq α] {a : α} {l : List (List α)}, List.count a l.flatten = (List.map (List.count a) l).sum
-- Mathlib.Order.Atoms
IsStronglyAtomic.mk : ∀ {α : Type u_5} [inst : Preorder α], (∀ (a b : α), a < b → ∃ x, a ⋖ x ∧ x ≤ b) → IsStronglyAtomic α
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.pullbackAwayιIso_inv_fst : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m')
  (hm' : 0 < m') {x : A} (hx : x = f * g),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).inv
      (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm)
        (AlgebraicGeometry.Proj.awayι 𝒜 g g_deg hm')) =
    AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))
-- Mathlib.Topology.UniformSpace.Cauchy
SequentiallyComplete.seq_is_cauchySeq : ∀ {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α}
  (U_mem : ∀ (n : ℕ), U n ∈ uniformity α),
  (∀ s ∈ uniformity α, ∃ n, U n ⊆ s) → CauchySeq (SequentiallyComplete.seq hf U_mem)
-- Mathlib.Topology.Semicontinuity.Defs
upperSemicontinuousWithinAt_const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {x : α} {s : Set α} {z : β},
  UpperSemicontinuousWithinAt (fun _x => z) s x
-- Mathlib.Algebra.Group.Subgroup.Defs
NegMemClass.neg.eq_1 : ∀ {G : Type u_5} {S : Type u_6} [inst : Neg G] [inst_1 : SetLike S G] [inst_2 : NegMemClass S G] {H : S},
  NegMemClass.neg = { neg := fun a => ⟨-↑a, ⋯⟩ }
-- Mathlib.Algebra.BigOperators.GroupWithZero.Action
List.vadd_sum : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddZeroClass N] [inst_2 : AddAction M N]
  [VAddAssocClass M N N] [VAddCommClass M N N] (l : List N) (m : M),
  l.length • m +ᵥ l.sum = (List.map (fun x => m +ᵥ x) l).sum
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_map_dvd : ∀ {G : Type u_1} [inst : AddMonoid G] {H : Type u_6} [inst_1 : AddMonoid H] (ψ : G →+ H) (x : G),
  addOrderOf (ψ x) ∣ addOrderOf x
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.comp_preservesLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F]
  [CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, v₁, v₃, u₁, u₃} (F.comp G)
-- ProofWidgets.Component.Basic
ProofWidgets.InteractiveCodeProps.mk.sizeOf_spec : ∀ (fmt : Lean.Widget.CodeWithInfos), sizeOf { fmt := fmt } = 1 + sizeOf fmt
-- Mathlib.RepresentationTheory.Rep.Res
Rep.shortExact_res : ∀ {G : Type v1} {H : Type v2} [inst : Monoid G] [inst_1 : Monoid H] {k : Type u} [inst_2 : CommRing k] (φ : H →* G)
  {S : CategoryTheory.ShortComplex (Rep.{w, u, v1} k G)}, (S.map (Rep.resFunctor φ)).ShortExact ↔ S.ShortExact
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.FunctorToTypes.shrink_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w'))
  [inst_1 : CategoryTheory.FunctorToTypes.Small.{w, w', v, u} F] (X : C),
  (CategoryTheory.FunctorToTypes.shrink.{w, w', v, u} F).obj X = Shrink.{w, w'} (F.obj X)
-- Init.Data.Iterators.Basic
Std.IterM.Step.val_toPure : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {it : Std.IterM Id β} {step : it.Step},
  ↑step.toPure = Std.IterStep.mapIterator Std.IterM.toIter ↑step
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.nhds_of_ne_top : ∀ {x : ENNReal}, x ≠ ⊤ → nhds x = ⨅ ε, ⨅ (_ : ε > 0), Filter.principal (Set.Icc (x - ε) (x + ε))
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestRevMatchAtChain.nil : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} (p : s.Pos),
  String.Slice.Pattern.Model.IsLongestRevMatchAtChain pat p p
-- Init.Omega.LinearCombo
_private.Init.Omega.LinearCombo.0.Lean.Omega.instToStringInt : ToString ℤ
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.skipSuffixWhile_string_eq_skipSuffixWhile_toSlice : ∀ {pat : String} {s : String.Slice}, s.skipSuffixWhile pat = s.skipSuffixWhile pat.toSlice
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instRightCancelMonoid : {α : Type u_1} → [RightCancelMonoid α] → RightCancelMonoid (Lex α)
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
/-- The Carathéodory-measurable sets for an outer measure `m` form a Dynkin system.  -/
MeasureTheory.OuterMeasure.caratheodoryDynkin : {α : Type u} → MeasureTheory.OuterMeasure α → MeasurableSpace.DynkinSystem α
-- Mathlib.Data.Bool.Basic
Bool.eq_true_of_not_eq_false : ∀ {b : Bool}, ¬b = false → b = true
-- Mathlib.Tactic.Simproc.VecPerm
_private.Mathlib.Tactic.Simproc.VecPerm.0.Mathlib.Tactic.FinVec.eq_etaExpand : ∀ {α : Type u_1} {m : ℕ} (v : Fin m → α), v = FinVec.etaExpand v
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normalCore_eq_iInf_comap_conj : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.normalCore = ⨅ g, Subgroup.comap (↑(MulAut.conj g)) H
-- Mathlib.RepresentationTheory.Basic
/-- The additive equivalence from the `Module k[G]` to the original vector space
of the representative.

This is just the identity, but it is helpful for typechecking and keeping track of instances.
 -/
Representation.asModuleEquiv : {k : Type u_4} →
  {G : Type u_5} →
    {V : Type u_6} →
      [inst : Semiring k] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid V] → [inst_3 : Module k V] → (ρ : Representation k G V) → ρ.asModule ≃ₗ[k] V
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_iUnion_congr : ∀ {ι : Type u_1} {α : Type u_2} {M : Matroid α} (Xs Ys : ι → Set α),
  (∀ (i : ι), M.closure (Xs i) = M.closure (Ys i)) → M.closure (⋃ i, Xs i) = M.closure (⋃ i, Ys i)
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.div_opow_log_pos : ∀ (b : Ordinal.{u_1}) {o : Ordinal.{u_1}}, o ≠ 0 → 0 < o / b ^ Ordinal.log b o
-- Std.Do.WP.SimpLemmas
Std.Do.WP.StateT_run : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {σ α : Type u} {s : σ} {Q : Std.Do.PostCond (α × σ) ps}
  [inst : Std.Do.WP m ps] (x : StateT σ m α),
  (Std.Do.wp (x.run s)).apply Q = (Std.Do.wp x).apply (fun a s => Q.1 (a, s), Q.2) s
-- Lean.Declaration
Lean.DefinitionVal.mk : Lean.ConstantVal → Lean.Expr → Lean.ReducibilityHints → Lean.DefinitionSafety → List Lean.Name → Lean.DefinitionVal
-- Lean.Meta.CongrTheorems
_private.Lean.Meta.CongrTheorems.0.Lean.Meta.mkHCongrWithArity.withNewEqs.loop : {α : Type} →
  Array Lean.Expr →
    Array Lean.Expr →
      (Array Lean.Expr → Array Lean.Meta.CongrArgKind → Lean.MetaM α) →
        ℕ → Array Lean.Expr → Array Lean.Meta.CongrArgKind → Lean.MetaM α
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `HasFDerivWithinAt.const_smul` -/
HasFDerivWithinAt.fun_const_smul : ∀ {𝕜 : 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] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} {s : Set E} {R : Type u_4} [inst_5 : Monoid R] [inst_6 : DistribMulAction R F]
  [inst_7 : SMulCommClass 𝕜 R F] [inst_8 : ContinuousConstSMul R F],
  HasFDerivWithinAt f f' s x → ∀ (c : R), HasFDerivWithinAt (fun i => c • f i) (c • f') s x
-- Mathlib.RingTheory.Regular.IsSMulRegular
isSMulRegular_of_isSMulRegular_on_submodule_on_quotient : ∀ {R : Type u_1} {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Submodule R M}
  {r : R}, IsSMulRegular (↥N) r → IsSMulRegular (M ⧸ N) r → IsSMulRegular M r
-- Lean.Linter.Deprecated
Lean.Linter.linter.deprecated : Lean.Option Bool
-- Mathlib.RingTheory.Extension.Basic
/-- The cotangent space of an extension.
This is a type synonym so that `P.Ring` can act on it through the action of `S` without creating
a diamond.  -/
Algebra.Extension.Cotangent : {R : Type u} →
  {S : Type v} → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Algebra.Extension R S → Type w
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.ofCoeff_add`. -/
SkewMonoidAlgebra.ofFinsupp_add : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] {a b : G →₀ k},
  { coeff := a + b } = { coeff := a } + { coeff := b }
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.coe_sub : ∀ (x y : ℝ), ↑(x - y) = ↑x - ↑y
-- Mathlib.CategoryTheory.Category.Basic
/-- The composition of epimorphisms is again an epimorphism. This version takes `Epi f` and `Epi g`
as typeclass arguments. For a version taking them as explicit arguments, see `epi_comp'`.  -/
CategoryTheory.epi_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) [CategoryTheory.Epi f] (g : Y ⟶ Z)
  [CategoryTheory.Epi g], CategoryTheory.Epi (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.restrictₛₗ_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M : PresheafOfModules R) {X Y : Cᵒᵖ} (f : X ⟶ Y) (m : ↑(M.obj X)),
  (M.restrictₛₗ f) m = (CategoryTheory.ConcreteCategory.hom (M.map f)) m
-- Mathlib.Analysis.Polynomial.MahlerMeasure
/-- The Mahler measure for polynomials on rings other than `ℂ`. Most theorems
will require `A` to be a `NormedRing` and `v` to be an isometry. See, e.g.,
`mapMahlerMeasure_const`  -/
Polynomial.mapMahlerMeasure : {A : Type u_1} → [inst : Semiring A] → Polynomial A → (A →+* ℂ) → ℝ
-- Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
CompleteLattice.MulticoequalizerDiagram.mk : ∀ {T : Type u} [inst : CompleteLattice T] {ι : Type u_1} {x : T} {u : ι → T} {v : ι → ι → T},
  ⨆ i, u i = x → (∀ (i j : ι), v i j = u i ⊓ u j) → CompleteLattice.MulticoequalizerDiagram x u v
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Reinterpreting an `F`-costructured arrow `F.obj A ⟶ X` as an arrow over `X`.  -/
CategoryTheory.MorphismProperty.CostructuredArrow.toOver : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{u_3, u_1} C] →
      [inst_1 : CategoryTheory.Category.{u_4, u_2} D] →
        (P : CategoryTheory.MorphismProperty D) →
          (F : CategoryTheory.Functor C D) → (X : D) → CategoryTheory.Functor (P.CostructuredArrow ⊤ F X) (P.Over ⊤ X)
-- Mathlib.Algebra.Polynomial.Degree.Domain
Polynomial.degree_le_of_dvd : ∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R] {p q : Polynomial R}, p ∣ q → q ≠ 0 → p.degree ≤ q.degree
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.FlatMap.0.Std.Iter.step_filterMapWithPostcondition.match_3.eq_3 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it : Std.Iter β} (motive : it.Step → Sort u_2)
  (h : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.Iter β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.done, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_3 h
-- Lean.Elab.Parallel
/-- Runs a list of TermElabM computations in parallel and returns the first successful result
(by completion order, not list order).

If `cancel := true` (the default), cancels all remaining tasks after the first success.
 -/
Lean.Elab.Term.TermElabM.parFirst : {α : Type} → List (Lean.Elab.TermElabM α) → optParam Bool true → Lean.Elab.TermElabM α
-- Mathlib.Data.Finset.Pi
Finset.Pi.cons_ne : ∀ {α : Type u_1} {δ : α → Sort v} [inst : DecidableEq α] {s : Finset α} {a a' : α} {b : δ a} {f : (a : α) → a ∈ s → δ a}
  {h : a' ∈ insert a s} (ha : a ≠ a'), Finset.Pi.cons s a b f a' h = f a' ⋯
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.equivHomotopy_symm_apply_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ₁ φ₂ : F ⟶ G)
  (z :
    { z //
      CochainComplex.HomComplex.Cochain.ofHom φ₁ =
        CochainComplex.HomComplex.δ (-1) 0 z + CochainComplex.HomComplex.Cochain.ofHom φ₂ })
  (i j : ℤ),
  ((CochainComplex.HomComplex.Cochain.equivHomotopy φ₁ φ₂).symm z).hom i j =
    if hij : i + -1 = j then (↑z).v i j hij else 0
-- Mathlib.Combinatorics.SetFamily.Shadow
/-- `t` is in the upper shadow of `𝒜` iff there is a `s ∈ 𝒜` from which we can remove one element
to get `t`.  -/
Finset.mem_upShadow_iff : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {𝒜 : Finset (Finset α)} {t : Finset α},
  t ∈ 𝒜.upShadow ↔ ∃ s ∈ 𝒜, ∃ a ∉ s, insert a s = t
-- Init.Data.Slice.Array.Lemmas
Subarray.toArray_mkSlice_ric : ∀ {α : Type u_1} {xs : Subarray α} {hi : ℕ},
  Std.Slice.toArray (Std.Ric.Sliceable.mkSlice xs *...=hi) = (Std.Slice.toArray xs).extract 0 (hi + 1)
-- Mathlib.GroupTheory.Congruence.Basic
Con.instIsScalarTower : ∀ {α : Type u_4} {β : Type u_5} {M : Type u_6} [inst : MulOneClass M] [inst_1 : SMul α β] [inst_2 : SMul α M]
  [inst_3 : SMul β M] [inst_4 : IsScalarTower α M M] [inst_5 : IsScalarTower β M M] [IsScalarTower α β M] (c : Con M),
  IsScalarTower α β c.Quotient
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.infPrepartition_toPrepartition : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) (π' : BoxIntegral.Prepartition I),
  (π.infPrepartition π').toPrepartition = π.toPrepartition ⊓ π'
-- Mathlib.GroupTheory.Coprod.Basic
AddEquiv.coprodComm_symm_apply : ∀ (M : Type u_1) (N : Type u_2) [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  ⇑(AddEquiv.coprodComm M N).symm = ⇑(AddMonoid.Coprod.swap N M)
-- Mathlib.CategoryTheory.Limits.Yoneda
/-- The yoneda embeddings jointly reflect limits.  -/
CategoryTheory.yonedaJointlyReflectsLimits : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{t, w} J] →
        (F : CategoryTheory.Functor J Cᵒᵖ) →
          (c : CategoryTheory.Limits.Cone F) →
            ((X : C) → CategoryTheory.Limits.IsLimit ((CategoryTheory.yoneda.obj X).mapCone c)) →
              CategoryTheory.Limits.IsLimit c
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- Copy of a `QuadraticMap` with a new `toFun` equal to the old one. Useful to fix definitional
equalities.  -/
QuadraticMap.copy : {R : Type u_3} →
  {M : Type u_4} →
    {N : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] → (Q : QuadraticMap R M N) → (Q' : M → N) → Q' = ⇑Q → QuadraticMap R M N
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.im_inv : ∀ {K : Type u_1} [inst : Field K] {a b : K} (z : QuadraticAlgebra K a b), z⁻¹.im = -((QuadraticAlgebra.norm z)⁻¹ * z.im)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- If we can partition a product into subsets that cancel out, then the whole product cancels.  -/
Finset.prod_cancels_of_partition_cancels : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : CommMonoid M] {f : ι → M} (R : Setoid ι)
  [inst_1 : DecidableRel ⇑R], (∀ x ∈ s, ∏ a ∈ s with R a x, f a = 1) → ∏ x ∈ s, f x = 1
-- Mathlib.MeasureTheory.Integral.Prod
/-- Integrals commute with subtraction inside a lower Lebesgue integral.
`F` can be any function.  -/
MeasureTheory.lintegral_fn_integral_sub : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [inst_4 : NormedSpace ℝ E] [MeasureTheory.SFinite μ] ⦃f g : α × β → E⦄ (F : E → ENNReal),
  MeasureTheory.Integrable f (μ.prod ν) →
    MeasureTheory.Integrable g (μ.prod ν) →
      ∫⁻ (x : α), F (∫ (y : β), f (x, y) - g (x, y) ∂ν) ∂μ =
        ∫⁻ (x : α), F (∫ (y : β), f (x, y) ∂ν - ∫ (y : β), g (x, y) ∂ν) ∂μ
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instRightCancelMonoid.eq_1 : ∀ {α : Type u_1} [inst : LeftCancelMonoid α],
  MulOpposite.instRightCancelMonoid = { toMonoid := MulOpposite.instMonoid, toIsRightCancelMul := ⋯ }
-- Init.Data.Array.Sort.Lemmas
_private.Init.Data.List.Sort.Basic.0.List.mergeSort.match_1.congr_eq_1 : ∀ {α : Type u_1} (motive : List α → (α → α → Bool) → Sort u_2) (x : List α) (x_1 : α → α → Bool)
  (h_1 : (x : α → α → Bool) → motive [] x) (h_2 : (a : α) → (x : α → α → Bool) → motive [a] x)
  (h_3 : (a b : α) → (xs : List α) → (le : α → α → Bool) → motive (a :: b :: xs) le) (x_2 : α → α → Bool),
  x = [] →
    x_1 = x_2 →
      (match x, x_1 with
        | [], x => h_1 x
        | [a], x => h_2 a x
        | a :: b :: xs, le => h_3 a b xs le) ≍
        h_1 x_2
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.lTensor_id_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) (N : Type u_8) [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (x : TensorProduct R M N),
  (LinearMap.lTensor M LinearMap.id) x = x