mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_C_mul_X : ∀ {R : Type u} [inst : Semiring R] (a : R), a ≠ 0 → (Polynomial.C a * Polynomial.X).natDegree = 1
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestRevMatchAt.eq : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {startPos startPos' endPos : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAt pat startPos endPos →
    String.Slice.Pattern.Model.IsLongestRevMatchAt pat startPos' endPos → startPos = startPos'
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.CommRing.mk.sizeOf_spec : ∀ (toRing : Lean.Meta.Sym.Arith.Ring) (invFn? : Option Lean.Expr) (semiringId? : Option ℕ)
  (commSemiringInst commRingInst : Lean.Expr) (noZeroDivInst? fieldInst? : Option Lean.Expr),
  sizeOf
      { toRing := toRing, invFn? := invFn?, semiringId? := semiringId?, commSemiringInst := commSemiringInst,
        commRingInst := commRingInst, noZeroDivInst? := noZeroDivInst?, fieldInst? := fieldInst? } =
    1 + sizeOf toRing + sizeOf invFn? + sizeOf semiringId? + sizeOf commSemiringInst + sizeOf commRingInst +
        sizeOf noZeroDivInst? +
      sizeOf fieldInst?
-- Mathlib.GroupTheory.Congruence.Defs
/-- The quotient of an `AddCommGroup` by an additive congruence
relation is an `AddCommGroup`.  -/
AddCon.addCommGroup : {M : Type u_4} → [inst : AddCommGroup M] → (c : AddCon M) → AddCommGroup c.Quotient
-- Mathlib.RingTheory.FilteredAlgebra.Basic
IsFiltration.F_lt_le_F : ∀ {ι : Type u_1} {σ : Type u_3} [inst : Preorder ι] [inst_1 : Preorder σ] (F : ι → σ) (F_lt : outParam (ι → σ)) (i : ι)
  [IsFiltration F F_lt], F_lt i ≤ F i
-- Lean.Elab.Quotation
/-- match step that always succeeds: _, x, `($x), ...  -/
Lean.Elab.Term.Quotation.HeadCheck.unconditional : Lean.Elab.Term.Quotation.HeadCheck
-- Mathlib.Algebra.Tropical.Basic
Tropical.untrop_zpow : ∀ {R : Type u} [inst : AddGroup R] (x : Tropical R) (n : ℤ), Tropical.untrop (x ^ n) = n • Tropical.untrop x
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min?_emptyc : ∀ {α : Type u} {cmp : α → α → Ordering}, Std.TreeSet.Raw.empty.min? = none
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.mrange_inl_sup_mrange_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddMonoidHom.mrange (AddMonoidHom.inl M N) ⊔ AddMonoidHom.mrange (AddMonoidHom.inr M N) = ⊤
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_hom : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D T) (Y : T) (X : D)
  (Y_1 : CategoryTheory.StructuredArrow X (CategoryTheory.StructuredArrow.proj Y F)),
  ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor F Y X).obj Y_1).hom = Y_1.right.hom
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- **Alias** of the reverse direction of `Metric.closedBall_eq_empty`. -/
Metric.closedBall_of_neg : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, ε < 0 → Metric.closedBall x ε = ∅
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
SimpleGraph.DeleteFar.mono : ∀ {V : Type u_1} {G : SimpleGraph V} {𝕜 : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : Fintype ↑G.edgeSet] {p : SimpleGraph V → Prop} {r₁ r₂ : 𝕜}, G.DeleteFar p r₂ → r₁ ≤ r₂ → G.DeleteFar p r₁
-- Init.Data.Bool
Bool.cond_eq_if : ∀ {b : Bool} {α : Sort u_1} {x y : α}, (bif b then x else y) = if b = true then x else y
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_filter_lt_of_le_right : ∀ {α : Type u_2} {a b c : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α]
  [inst_2 : DecidablePred fun x => x < c], c ≤ b → {x ∈ Finset.Ico a b | x < c} = Finset.Ico a c
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.toComplex_def' : ∀ (x y : ℤ), GaussianInt.toComplex { re := x, im := y } = ↑x + ↑y * Complex.I
-- Std.Do.PostCond
_private.Std.Do.PostCond.0.Std.Do.ExceptConds.entails.match_1.eq_2 : ∀ (motive : (ps : Std.Do.PostShape) → Std.Do.ExceptConds ps → Std.Do.ExceptConds ps → Sort u_2) (σ : Type u_1)
  (ps : Std.Do.PostShape) (x y : Std.Do.ExceptConds (Std.Do.PostShape.arg σ ps))
  (h_1 : (x y : Std.Do.ExceptConds Std.Do.PostShape.pure) → motive Std.Do.PostShape.pure x y)
  (h_2 :
    (σ : Type u_1) →
      (ps : Std.Do.PostShape) →
        (x y : Std.Do.ExceptConds (Std.Do.PostShape.arg σ ps)) → motive (Std.Do.PostShape.arg σ ps) x y)
  (h_3 :
    (ε : Type u_1) →
      (ps : Std.Do.PostShape) →
        (x y : Std.Do.ExceptConds (Std.Do.PostShape.except ε ps)) → motive (Std.Do.PostShape.except ε ps) x y),
  (match Std.Do.PostShape.arg σ ps, x, y with
    | Std.Do.PostShape.pure, x, y => h_1 x y
    | Std.Do.PostShape.arg σ ps, x, y => h_2 σ ps x y
    | Std.Do.PostShape.except ε ps, x, y => h_3 ε ps x y) =
    h_2 σ ps x y
-- Mathlib.RingTheory.Flat.Basic
/-- `M` is flat if and only if `𝟙 M ⊗ f` is injective whenever `f` is an injective linear map
in a universe that `R` fits in.  -/
Module.Flat.iff_lTensor_preserves_injective_linearMapₛ : ∀ {R : Type u} {M : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Small.{v', u} R],
  Module.Flat R M ↔
    ∀ ⦃N N' : Type v'⦄ [inst_4 : AddCommMonoid N] [inst_5 : AddCommMonoid N'] [inst_6 : Module R N]
      [inst_7 : Module R N'] (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(LinearMap.lTensor M f)
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.closedEBall_mem_nhds`. -/
EMetric.closedBall_mem_nhds : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (x : α) {ε : ENNReal}, 0 < ε → Metric.closedEBall x ε ∈ nhds x
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rxo.Iterator.toList_eq_match : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.Rxo.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  {it : Std.Iter α},
  it.toList =
    match it.internalState.next with
    | none => []
    | some a =>
      if a < it.internalState.upperBound then
        a :: { internalState := { next := Std.PRange.succ? a, upperBound := it.internalState.upperBound } }.toList
      else []
-- Mathlib.Data.Finset.Image
/-- The `Finset` version of `Equiv.subset_symm_image`.  -/
Finset.subset_map_symm : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {f : α ≃ β},
  s ⊆ Finset.map f.symm.toEmbedding t ↔ Finset.map f.toEmbedding s ⊆ t
-- Lean.Meta.Constructions.BRecOn
/-- Constructs the `.brecOn` definition for a inductive predicate.

For example for the `List` type, it constructs,
```
@[reducible] protected def List.brecOn.go.{u} : {a : Type} →
  {motive : List a → Sort u} →
    (t : List a) → ((t : List a) → List.below t → motive t) → motive t ×' List.below t :=
fun {a} {motive} t F_1 =>
  List.rec ⟨F_1 List.nil PUnit.unit, PUnit.unit⟩ (fun a_1 a_2 a_ih => ⟨F_1 (List.cons a_1 a_2) a_ih, a_ih⟩) t

@[reducible] protected def List.brecOn.{u} : {a : Type} →
  {motive : List a → Sort u} → (t : List a) → ((t : List a) → List.below t → motive t) → motive t :=
fun {a} {motive} t F_1 => (List.brecOn.go t F_1).1

protected theorem List.brecOn.eq.{u} : ∀ {a : Type} {motive : List a → Sort u} (t : List a)
  (F_1 : (t : List a) → List.below t → motive t), List.brecOn t F_1 = F_1 t (List.brecOn.go t F_1).2
```
 -/
_private.Lean.Meta.Constructions.BRecOn.0.Lean.mkBRecOnFromRec : Lean.Name → ℕ → Array Lean.Name → Lean.Name → Lean.MetaM Unit
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.sumAux_eq : ∀ {M : Type u_4} [inst : AddMonoid M] (l : List M), FreeAddMonoid.sumAux l = l.sum
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_withDensity_iff_integrable_smul : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_8} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : α → NNReal},
  Measurable f →
    ∀ {g : α → E},
      MeasureTheory.Integrable g (μ.withDensity fun x => ↑(f x)) ↔ MeasureTheory.Integrable (fun x => f x • g x) μ
-- Mathlib.RingTheory.Etale.Locus
Algebra.etaleLocus_eq_univ_iff : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Algebra.etaleLocus R A = Set.univ ↔ Algebra.FormallyEtale R A
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.isStrictValue : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.AdditiveFunctor.forget_obj : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (F : C ⥤+ D), (CategoryTheory.AdditiveFunctor.forget C D).obj F = F.obj
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.radius_logSizeBallSeq_zero : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [inst_1 : DecidableEq T]
  (hJ : J.Nonempty),
  (PairReduction.logSizeBallSeq J hJ a c 0).radius = PairReduction.logSizeRadius (Exists.choose hJ) J a c
-- Mathlib.Tactic.Observe
/-- `observe hp : p` asserts the proposition `p` as a hypothesis named `hp`, and tries to prove it
using `exact?`.
If no proof is found, the tactic fails.
In other words, this tactic is equivalent to `have hp : p := by exact?`.

* `observe : p` uses the name `this` for the new hypothesis.
* `observe? hp : p` will emit a trace message of the form `have hp : p := proof_term`.
  This may be particularly useful to speed up proofs.
 -/
Mathlib.Tactic.LibrarySearch.«tacticObserve?__:_Using__,,» : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKeyD_insertMany!_list_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : BEq α] [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {l : List (α × β)} {k fallback : α},
      (List.map Prod.fst l).contains k = false →
        (↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l)).getKeyD k fallback = t.getKeyD k fallback
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.mem_closure : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {x : α} {t : Set β}, ContinuousWithinAt f s x → x ∈ closure s → Set.MapsTo f s t → f x ∈ closure t
-- Mathlib.Algebra.Homology.Single
HomologicalComplex.single_obj_d : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : V) (k l : ι), ((HomologicalComplex.single V c j).obj A).d k l = 0
-- Mathlib.CategoryTheory.Monoidal.Category
/-- Auxiliary structure to carry only the data fields of (and provide notation for)
`MonoidalCategory`.  -/
CategoryTheory.MonoidalCategoryStruct : (C : Type u) → [𝒞 : CategoryTheory.Category.{v, u} C] → Type (max u v)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_filterMap! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w}
  [inst : Std.TransOrd α] [inst_1 : Std.LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} {k : α} (h : t.WF)
  {h' : k ∈ Std.DTreeMap.Internal.Impl.filterMap! f t},
  (Std.DTreeMap.Internal.Impl.filterMap! f t).get k h' = (f k (t.get k ⋯)).get ⋯
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.get!ₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Hashable α]
  (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) [inst_3 : Inhabited (β a)], m.get!ₘ a = (m.get?ₘ a).get!
-- Mathlib.Data.Rat.BigOperators
Rat.cast_sum : ∀ {ι : Type u_1} {α : Type u_2} [inst : DivisionRing α] [CharZero α] (s : Finset ι) (f : ι → ℚ),
  ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
-- Mathlib.Algebra.Order.Module.Defs
/-- Do not use this. Use `lt_of_smul_lt_smul_right` instead.  -/
SMulPosReflectLT.lt_of_smul_lt_smul_right : ∀ {α : Type u_1} {β : Type u_2} {inst : SMul α β} {inst_1 : Preorder α} {inst_2 : Preorder β} {inst_3 : Zero β}
  [self : SMulPosReflectLT α β] ⦃b : β⦄, 0 ≤ b → ∀ ⦃a₁ a₂ : α⦄, a₁ • b < a₂ • b → a₁ < a₂
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
/-- Construct a morphism in the free groupoid on `C` by providing a morphism in `C`.  -/
CategoryTheory.FreeGroupoid.homMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → (X ⟶ Y) → (CategoryTheory.FreeGroupoid.mk X ⟶ CategoryTheory.FreeGroupoid.mk Y)
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.taylorAlgHom_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (r : R) (a : Polynomial R),
  (Polynomial.taylorAlgHom r) a = (Polynomial.taylor r) a
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBiconeMorphism.mk.sizeOf_spec : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} {A B : CategoryTheory.Limits.BinaryBicone P Q} [inst_2 : SizeOf C] (hom : A.pt ⟶ B.pt)
  (wfst :
    autoParam (CategoryTheory.CategoryStruct.comp hom B.fst = A.fst)
      CategoryTheory.Limits.BinaryBiconeMorphism.wfst._autoParam)
  (wsnd :
    autoParam (CategoryTheory.CategoryStruct.comp hom B.snd = A.snd)
      CategoryTheory.Limits.BinaryBiconeMorphism.wsnd._autoParam)
  (winl :
    autoParam (CategoryTheory.CategoryStruct.comp A.inl hom = B.inl)
      CategoryTheory.Limits.BinaryBiconeMorphism.winl._autoParam)
  (winr :
    autoParam (CategoryTheory.CategoryStruct.comp A.inr hom = B.inr)
      CategoryTheory.Limits.BinaryBiconeMorphism.winr._autoParam),
  sizeOf { hom := hom, wfst := wfst, wsnd := wsnd, winl := winl, winr := winr } =
    1 + sizeOf hom + sizeOf wfst + sizeOf wsnd + sizeOf winl + sizeOf winr
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.NullMeasurableSet.addFundamentalFrontier : ∀ (G : Type u_1) {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] (s : Set α) [Countable G]
  [inst_3 : MeasurableSpace α] [MeasurableConstVAdd G α] {μ : MeasureTheory.Measure α}
  [MeasureTheory.VAddInvariantMeasure G α μ],
  MeasureTheory.NullMeasurableSet s μ → MeasureTheory.NullMeasurableSet (MeasureTheory.addFundamentalFrontier G s) μ
-- Mathlib.Tactic.Simproc.ExistsAndEq
ExistsAndEq.GoTo.right.sizeOf_spec : sizeOf ExistsAndEq.GoTo.right = 1
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k k' fallback : α}, cmp k k' = Ordering.eq → t.getKeyD k fallback = t.getKeyD k' fallback
-- Mathlib.Topology.Compactness.Compact
/-- **Tychonoff's theorem**: product of compact sets is compact.  -/
isCompact_pi_infinite : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {s : (i : ι) → Set (X i)},
  (∀ (i : ι), IsCompact (s i)) → IsCompact {x | ∀ (i : ι), x i ∈ s i}
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.smul_basis_eq_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} {p q : Polynomial R},
  p • 1 + q • (WeierstrassCurve.Affine.CoordinateRing.mk W') Polynomial.X = 0 → p = 0 ∧ q = 0
-- Init.Data.Slice.Array.Lemmas
Subarray.mkSlice_roc_eq_mkSlice_rco : ∀ {α : Type u_1} {xs : Subarray α} {lo hi : ℕ},
  (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = Std.Rco.Sliceable.mkSlice xs (lo + 1)...hi + 1
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.sum_sum_index : ∀ {R : Type u_1} [inst : Semiring R] {R' : Type u_5} {P : Type u_6} [inst_1 : AddCommMonoid P] [inst_2 : Semiring R']
  {f : SkewPolynomial R} {g : ℕ → R → SkewPolynomial R'} {h : ℕ → R' → P},
  (∀ (a : ℕ), h a 0 = 0) →
    (∀ (a : ℕ) (b₁ b₂ : R'), h a (b₁ + b₂) = h a b₁ + h a b₂) → (f.sum g).sum h = f.sum fun a b => (g a b).sum h
-- Lean.Elab.AssertExists
/-- `assert_not_imported m₁ m₂ ... mₙ` checks that each one of the modules `m₁ m₂ ... mₙ` is not
among the transitive imports of the current file.

The command does not currently check whether the modules `m₁ m₂ ... mₙ` actually exist.
 -/
Lean.Elab.Command.elabAssertNotImported : Lean.Elab.Command.CommandElab
-- Mathlib.Logic.Embedding.Basic
/-- If `e₁` and `e₂` are embeddings,
then so is `fun ⟨a, b⟩ ↦ ⟨e₁ a, e₂ b⟩ : PProd α γ → PProd β δ`.  -/
Function.Embedding.pprodMap : {α : Sort u_1} → {β : Sort u_2} → {γ : Sort u_3} → {δ : Sort u_4} → (α ↪ β) → (γ ↪ δ) → α ×' γ ↪ β ×' δ
-- Mathlib.Algebra.GroupWithZero.Defs
/-- Zero is a right absorbing element for multiplication  -/
MulZeroClass.mul_zero : ∀ {M₀ : Type u} [self : MulZeroClass M₀] (a : M₀), a * 0 = 0
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) AlgebraicGeometry.Scheme.forgetToTop
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- The image of `R` in `S` is linearly disjoint with any other submodules.  -/
Submodule.LinearDisjoint.one_right : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (M : Submodule R S),
  M.LinearDisjoint 1
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.XXIsoOfEq_rfl : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (K : HomologicalComplex₂ C c₁ c₂)
  (i₁ : I₁) (i₂ : I₂), HomologicalComplex₂.XXIsoOfEq C c₁ c₂ K ⋯ ⋯ = CategoryTheory.Iso.refl ((K.X i₁).X i₂)
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
/-- The map `p : P ⟶ image f` is an epimorphism  -/
CategoryTheory.NonPreadditiveAbelian.instEpiFactorThruImage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {P Q : C}
  (f : P ⟶ Q), CategoryTheory.Epi (CategoryTheory.Abelian.factorThruImage f)
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.instIsCentralScalarSubtypePreLpMemAddSubgroup : ∀ {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)]
  [inst_1 : NormedRing 𝕜] [inst_2 : (i : α) → Module 𝕜 (E i)] [inst_3 : ∀ (i : α), IsBoundedSMul 𝕜 (E i)]
  [inst_4 : (i : α) → Module 𝕜ᵐᵒᵖ (E i)] [inst_5 : ∀ (i : α), IsCentralScalar 𝕜 (E i)], IsCentralScalar 𝕜 ↥(lp E p)
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.MorphismProperty.regularEpi.respectsIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C], (CategoryTheory.MorphismProperty.regularEpi C).RespectsIso
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_filterMap_le_size : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [Std.TransCmp cmp] {f : (a : α) → β a → Option (γ a)}, (Std.ExtDTreeMap.filterMap f t).size ≤ t.size
-- Std.Async.Signal
Std.Async.Signal.sigtstp.sizeOf_spec : sizeOf Std.Async.Signal.sigtstp = 1
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.decomp_to : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {i : ℤ} {A : C}
  (f : A ⟶ (CochainComplex.mappingCone φ).X i) (j : ℤ) (hij : i + 1 = j),
  ∃ a b,
    f =
      CategoryTheory.CategoryStruct.comp a ((CochainComplex.mappingCone.inl φ).v j i ⋯) +
        CategoryTheory.CategoryStruct.comp b ((CochainComplex.mappingCone.inr φ).f i)
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.NatTrans.toCatHom₂_id : ∀ {C D : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v, u} D]
  (F : CategoryTheory.Functor C D),
  CategoryTheory.NatTrans.toCatHom₂ (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id F.toCatHom
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.HomotopyEquiv.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (hom : S₁ ⟶ S₂) →
          (inv : S₂ ⟶ S₁) →
            CategoryTheory.ShortComplex.Homotopy (CategoryTheory.CategoryStruct.comp hom inv)
                (CategoryTheory.CategoryStruct.id S₁) →
              CategoryTheory.ShortComplex.Homotopy (CategoryTheory.CategoryStruct.comp inv hom)
                  (CategoryTheory.CategoryStruct.id S₂) →
                S₁.HomotopyEquiv S₂
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
/-- If `P` is a submersive presentation of `S` as an `R`-algebra and `S` is nontrivial,
`Ω[S⁄R]` is free of rank the dimension of `P`, i.e. the number of generators minus the number
of relations.  -/
Algebra.SubmersivePresentation.rank_kaehlerDifferential : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] [Nontrivial S] [Finite ι] (P : Algebra.SubmersivePresentation R S ι σ),
  Module.rank S Ω[S⁄R] = ↑P.dimension
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransformMorphism.mk.injEq : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (left : ψ.left ⟶ ψ'.left) (right : ψ.right ⟶ ψ'.right)
  (base : ψ.base ⟶ ψ'.base)
  (left_coherence :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom
          (CategoryTheory.Functor.whiskerRight left F') =
        CategoryTheory.CategoryStruct.comp (F.whiskerLeft base) (CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom)
      CategoryTheory.Limits.CatCospanTransformMorphism.left_coherence._autoParam)
  (right_coherence :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom
          (CategoryTheory.Functor.whiskerRight right G') =
        CategoryTheory.CategoryStruct.comp (G.whiskerLeft base)
          (CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom)
      CategoryTheory.Limits.CatCospanTransformMorphism.right_coherence._autoParam)
  (left_1 : ψ.left ⟶ ψ'.left) (right_1 : ψ.right ⟶ ψ'.right) (base_1 : ψ.base ⟶ ψ'.base)
  (left_coherence_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom
          (CategoryTheory.Functor.whiskerRight left_1 F') =
        CategoryTheory.CategoryStruct.comp (F.whiskerLeft base_1)
          (CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom)
      CategoryTheory.Limits.CatCospanTransformMorphism.left_coherence._autoParam)
  (right_coherence_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom
          (CategoryTheory.Functor.whiskerRight right_1 G') =
        CategoryTheory.CategoryStruct.comp (G.whiskerLeft base_1)
          (CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom)
      CategoryTheory.Limits.CatCospanTransformMorphism.right_coherence._autoParam),
  ({ left := left, right := right, base := base, left_coherence := left_coherence,
        right_coherence := right_coherence } =
      { left := left_1, right := right_1, base := base_1, left_coherence := left_coherence_1,
        right_coherence := right_coherence_1 }) =
    (left = left_1 ∧ right = right_1 ∧ base = base_1)
-- Init.Data.Vector.Lex
Vector.instDecidableLTOfDecidableEq : {α : Type u_1} → {n : ℕ} → [DecidableEq α] → [inst : LT α] → [DecidableLT α] → DecidableLT (Vector α n)