mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- The functions whose Mellin transform we study  -/
WeakFEPair.f : {E : Type u_1} → [inst : NormedAddCommGroup E] → [inst_1 : NormedSpace ℂ E] → WeakFEPair E → ℝ → E
-- Mathlib.RingTheory.Ideal.Basic
Ring.not_isField_of_ne_of_ne : ∀ {R : Type u_5} [inst : CommSemiring R] [Nontrivial R] {I : Ideal R}, I ≠ ⊥ → I ≠ ⊤ → ¬IsField R
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
/-- The underlying ideal of `SubDPIdeal.span hI S` is generated by the elements
of the form `hI.dpow n x` with `n > 0` and `x ∈ S`.  -/
DividedPowers.SubDPIdeal.span_carrier_eq_dpow_span : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (hI : DividedPowers I) {S : Set A},
  S ⊆ ↑I →
    (DividedPowers.SubDPIdeal.span hI S).carrier =
      Ideal.span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (xs xs_1 : List ((a : α) × β a)) (e_xs : xs = xs_1)
  (h : xs.isEmpty = false), Std.Internal.List.minKey xs h = Std.Internal.List.minKey xs_1 ⋯
-- Mathlib.Algebra.Polynomial.Div
Polynomial.eq_of_monic_of_dvd_of_natDegree_le : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.Monic → q.Monic → p ∣ q → q.natDegree ≤ p.natDegree → q = p
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.ofList_nil : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering}, Std.TreeMap.Raw.ofList [] cmp = ∅
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- commutation with `f'`  -/
CategoryTheory.ShortComplex.LeftHomologyMapData.commf'_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
  (self : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) {Z : C} (h : h₂.K ⟶ Z),
  CategoryTheory.CategoryStruct.comp h₁.f' (CategoryTheory.CategoryStruct.comp self.φK h) =
    CategoryTheory.CategoryStruct.comp φ.τ₁ (CategoryTheory.CategoryStruct.comp h₂.f' h)
-- Mathlib.Data.Matrix.Reflection
Matrix.etaExpand.eq_1 : ∀ {α : Type u_1} {m n : ℕ} (A : Matrix (Fin m) (Fin n) α),
  A.etaExpand = Matrix.of (FinVec.etaExpand fun i => FinVec.etaExpand fun j => A i j)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion_surjective : ∀ {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] (v : IsDedekindDomain.HeightOneSpectrum R),
  Function.Surjective IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.isCandidate : Lean.Meta.Grind.ENode → Lean.Expr → ℕ → ℕ → Bool
-- Lean.Elab.PreDefinition.Main
_private.Lean.Elab.PreDefinition.Main.0.Lean.Elab.addSorried : Lean.LocalContext × Lean.LocalInstances → Array Lean.Elab.PreDefinition → Lean.Elab.TermElabM Unit
-- Mathlib.Topology.Separation.Basic
isClosed_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {x : X}, IsClosed {x}
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
/-- Differences of harmonic functions are harmonic.
 -/
InnerProductSpace.HarmonicOnNhd.sub : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f₁ f₂ : E → F} {s : Set E},
  InnerProductSpace.HarmonicOnNhd f₁ s →
    InnerProductSpace.HarmonicOnNhd f₂ s → InnerProductSpace.HarmonicOnNhd (f₁ - f₂) s
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
UpperHalfPlane.contMDiffAt_iff : ∀ {n : WithTop ℕ∞} {f : UpperHalfPlane → ℂ} {τ : UpperHalfPlane},
  ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) n f τ ↔
    ContDiffAt ℂ n (f ∘ ↑UpperHalfPlane.ofComplex) ↑τ
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.shiftIso_add'_inv_app : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : F.ShiftSequence M] (n m mn : M) (hnm : m + n = mn) (a a' a'' : M)
  (ha' : n + a = a') (ha'' : m + a' = a'') (X : C),
  (F.shiftIso mn a a'' ⋯).inv.app X =
    CategoryTheory.CategoryStruct.comp ((F.shiftIso m a' a'' ha'').inv.app X)
      (CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').inv.app ((CategoryTheory.shiftFunctor C m).obj X))
        ((F.shift a).map ((CategoryTheory.shiftFunctorAdd' C m n mn hnm).inv.app X)))
-- Mathlib.Algebra.Lie.Abelian
LieAlgebra.ad_ker_eq_self_module_ker : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  (LieAlgebra.ad R L).ker = LieModule.ker R L L
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_const_mul_right : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (c : ℝ),
  ProbabilityTheory.covariance X (fun ω => c * Y ω) μ = c * ProbabilityTheory.covariance X Y μ
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.toProdMulOpposite_injective : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A],
  Function.Injective DoubleCentralizer.toProdMulOpposite
-- Mathlib.Data.Quot
Quotient.lift_mk : ∀ {α : Sort u_1} {β : Sort u_2} {s : Setoid α} (f : α → β) (h : ∀ (a b : α), a ≈ b → f a = f b) (x : α),
  Quotient.lift f h ⟦x⟧ = f x
-- Mathlib.CategoryTheory.Bicategory.Coherence
/-- Auxiliary definition for `inclusionPath`.  -/
CategoryTheory.FreeBicategory.inclusionPathAux : {B : Type u} → [inst : Quiver B] → {a b : B} → Quiver.Path a b → CategoryTheory.FreeBicategory.Hom a b
-- Init.Data.Option.Lemmas
Option.pelim_guard : ∀ {α : Type u_1} {p : α → Bool} {β : Sort u_2} {b : β} {a : α} {f : (a' : α) → Option.guard p a = some a' → β},
  (Option.guard p a).pelim b f = if h : p a = true then f a ⋯ else b
-- Mathlib.RingTheory.Ideal.Prod
/-- Every ideal of the product ring is of the form `I × J`, where `I` and `J` can be explicitly
given as the image under the projection maps.  -/
Ideal.ideal_prod_eq : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (I : Ideal (R × S)),
  I = (Ideal.map (RingHom.fst R S) I).prod (Ideal.map (RingHom.snd R S) I)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
/-- The complement of a combination, as an equivariant map.  -/
Set.powersetCard.mulActionHom_compl : (G : Type u_1) →
  [inst : Group G] →
    (α : Type u_2) →
      [inst_1 : MulAction G α] →
        {n : ℕ} →
          [inst_2 : DecidableEq α] →
            [inst_3 : Fintype α] →
              {m : ℕ} → m + n = Fintype.card α → ↑(Set.powersetCard α n) →ₑ[id] ↑(Set.powersetCard α m)
-- Mathlib.Algebra.Order.GroupWithZero.Defs
mul_le_mul_iff_right₀ : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c : α} [PosMulMono α] [PosMulReflectLE α],
  0 < a → (a * b ≤ a * c ↔ b ≤ c)
-- Init.Data.Array.Zip
_private.Init.Data.Array.Zip.0.Array.getElem?_zipWithAll.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : Option α → Option β → Sort u_3) →
      (x : Option α) →
        (x_1 : Option β) →
          (Unit → motive none none) →
            ((a? : Option α) → (b? : Option β) → (a? = none → b? = none → False) → motive a? b?) → motive x x_1
-- Init.System.IO
/-- Reads up to the given number of bytes from the handle. If the returned array is empty, an
end-of-file marker (EOF) has been reached.

Encountering an EOF does not close a handle. Subsequent reads may block and return more data.
 -/
IO.FS.Handle.read : IO.FS.Handle → USize → IO ByteArray
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.BuilderOption.pattern.inj : ∀ {stx stx_1 : Lean.Term},
  Aesop.Frontend.BuilderOption.pattern stx = Aesop.Frontend.BuilderOption.pattern stx_1 → stx = stx_1
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.mkContinue : Lean.Syntax → Lean.Elab.Term.Do.CodeBlock
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp f U)
      (f.c.app (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor f).obj U))) =
    X.presheaf.map (CategoryTheory.eqToHom ⋯)
-- Mathlib.Data.Rel
/-- A relation `R` is reflexive if `a ~[R] a`.  -/
SetRel.IsRefl : {α : Type u_1} → SetRel α α → Prop
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of `SimpleGraph.Walk.isTrail_map_iff_of_injective`. -/
SimpleGraph.Walk.map_isTrail_iff_of_injective : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u v : V} {p : G.Walk u v},
  Function.Injective ⇑f → ((SimpleGraph.Walk.map f p).IsTrail ↔ p.IsTrail)
-- Init.Data.UInt.Lemmas
UInt8.toNat_ofNatTruncate_of_le : ∀ {n : ℕ}, UInt8.size ≤ n → (UInt8.ofNatClamp n).toNat = UInt8.size - 1
-- Mathlib.Algebra.Order.IsBotOne
IsBotZeroClass.toOrderBot.eq_1 : ∀ (α : Type u_1) [inst : LE α] [inst_1 : Zero α] [inst_2 : IsBotZeroClass α],
  IsBotZeroClass.toOrderBot α = { bot := 0, bot_le := ⋯ }
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
/-- See `LinearIndependent.finCons'` for an uglier version that works if you
only have a module over a semiring.  -/
LinearIndependent.finCons : ∀ {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {x : V} {n : ℕ}
  {v : Fin n → V}, LinearIndependent K v → x ∉ Submodule.span K (Set.range v) → LinearIndependent K (Fin.cons x v)
-- Mathlib.Topology.Sheaves.LocalPredicate
/-- The subsheaf of the sheaf of all dependently typed functions satisfying the local predicate `P`.
 -/
TopCat.subsheafToTypes : {X : TopCat} → {T : ↑X → Type u_1} → TopCat.LocalPredicate T → TopCat.Sheaf (Type (max u_2 u_1)) X
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
_private.Mathlib.CategoryTheory.Monoidal.Free.Coherence.0.CategoryTheory.FreeMonoidalCategory.normalizeIsoApp.match_1.eq_2 : ∀ (C : Type u_1)
  (motive :
    CategoryTheory.FreeMonoidalCategory C →
      (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C → Sort u_2)
  (x : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C)
  (h_1 :
    (a : C) →
      (x : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C) →
        motive (CategoryTheory.FreeMonoidalCategory.of a) x)
  (h_2 :
    (x : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C) →
      motive CategoryTheory.FreeMonoidalCategory.unit x)
  (h_3 :
    (X a : CategoryTheory.FreeMonoidalCategory C) →
      (n : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C) →
        motive (X.tensor a) n),
  (match CategoryTheory.FreeMonoidalCategory.unit, x with
    | CategoryTheory.FreeMonoidalCategory.of a, x => h_1 a x
    | CategoryTheory.FreeMonoidalCategory.unit, x => h_2 x
    | X.tensor a, n => h_3 X a n) =
    h_2 x
-- Mathlib.Algebra.BigOperators.Group.Finset.Interval
Finset.prod_Icc_eq_prod_Ico_mul : ∀ {α : Type u_1} [inst : CommMonoid α] (f : ℤ → α) {l u : ℤ},
  l ≤ u → ∏ m ∈ Finset.Icc l u, f m = (∏ m ∈ Finset.Ico l u, f m) * f u
-- Mathlib.Algebra.Star.LinearMap
LinearMap.intrinsicStar_id : ∀ {R : Type u_1} {E : Type u_2} [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],
  star (WithConv.toConv LinearMap.id) = WithConv.toConv LinearMap.id
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- **Alias** of `CategoryTheory.Lax.LaxTrans.comp_app`. -/
CategoryTheory.Lax.LaxTrans.vComp_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {X Y Z : CategoryTheory.LaxFunctor B C} (η : CategoryTheory.Lax.LaxTrans X Y) (θ : CategoryTheory.Lax.LaxTrans Y Z)
  (a : B), (CategoryTheory.CategoryStruct.comp η θ).app a = CategoryTheory.CategoryStruct.comp (η.app a) (θ.app a)
-- Mathlib.Data.ENNReal.Inv
ENNReal.sub_div : ∀ {a b c : ENNReal}, (0 < b → b < a → c ≠ 0) → (a - b) / c = a / c - b / c
-- Mathlib.Order.Bounds.Basic
bddAbove_Icc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, BddAbove (Set.Icc a b)
-- Mathlib.Data.Finsupp.MonomialOrder
MonomialOrder.orderBot : {σ : Type u_1} → (m : MonomialOrder σ) → OrderBot m.syn
-- Mathlib.Topology.Algebra.Module.IsWeak
/-- The coercion `(B · ·) : E → (F → 𝕜)` is an embedding.  -/
LinearMap.IsWeak.isInducing : ∀ {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace E] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [hB : B.IsWeak], Topology.IsInducing fun x1 x2 => (B x1) x2
-- Mathlib.Order.WithBot
WithTop.eq_top_iff_forall_gt : ∀ {α : Type u_1} [inst : Preorder α] {x : WithTop α}, x = ⊤ ↔ ∀ (b : α), ↑b < x
-- Lean.ParserCompiler
/-- Precondition: `α` must match `ctx.tyName`.  -/
Lean.ParserCompiler.registerParserCompiler : {α : Type} → Lean.ParserCompiler.Context α → IO Unit
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.brecOn.eq : ∀ {motive : Lean.Grind.CommRing.Mon → Sort u} (t : Lean.Grind.CommRing.Mon)
  (F_1 : (t : Lean.Grind.CommRing.Mon) → Lean.Grind.CommRing.Mon.below t → motive t),
  Lean.Grind.CommRing.Mon.brecOn t F_1 = F_1 t (Lean.Grind.CommRing.Mon.brecOn.go t F_1).2
-- Lean.ReservedNameAction
/-- Execute a registered reserved action for the given reserved name.
Note that the handler can throw an exception.
 -/
Lean.executeReservedNameAction : Lean.Name → Lean.CoreM Unit
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.GoodProducts.span_sum : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}},
  Profinite.NobelingProof.contained C (Order.succ o) →
    ∀ (ho : o < Ordinal.type fun x1 x2 => x1 < x2),
      Set.range (Profinite.NobelingProof.GoodProducts.eval C) =
        Set.range
          (Sum.elim (fun l => Profinite.NobelingProof.Products.eval C ↑l) fun l =>
            Profinite.NobelingProof.Products.eval C ↑l)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_union_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h₁ : m₁.WF)
  (h₂ : m₂.WF) {k : α}, Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.union m₂ ⋯ ⋯).getKey? k = m₂.getKey? k
-- Mathlib.Data.WSeq.Basic
/-- membership for weak sequences  -/
Stream'.WSeq.Mem : {α : Type u} → Stream'.WSeq α → α → Prop
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.foldl : {α : Type u} → {β : α → Type v} → {δ : Type w} → (δ → (α : α) → β α → δ) → δ → Std.DHashMap.Internal.AssocList α β → δ
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.ι_tensorHom_assoc : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] {X₁ X₂ Y₁ Y₂ : CategoryTheory.GradedObject I C} (f : X₁ ⟶ X₂)
  (g : Y₁ ⟶ Y₂) [inst_3 : X₁.HasTensor Y₁] [inst_4 : X₂.HasTensor Y₂] (i₁ i₂ i₁₂ : I) (h : i₁ + i₂ = i₁₂) {Z : C}
  (h_1 : CategoryTheory.GradedObject.Monoidal.tensorObj X₂ Y₂ i₁₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ Y₁ i₁ i₂ i₁₂ h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.tensorHom f g i₁₂) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (f i₁) (g i₂))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₂ Y₂ i₁ i₂ i₁₂ h) h_1)
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.lsmul.congr_simp : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (R : Type u_3) [inst_3 : SeminormedRing R] [inst_4 : NormedAlgebra 𝕜 R]
  [inst_5 : Module R E] [inst_6 : IsBoundedSMul R E] [inst_7 : IsScalarTower 𝕜 R E],
  ContinuousLinearMap.lsmul 𝕜 R = ContinuousLinearMap.lsmul 𝕜 R
-- Mathlib.Data.Vector3
_private.Mathlib.Data.Vector3.0.Fin2.insertPerm.match_1.splitter : (motive : (x : ℕ) → Fin2 x → Fin2 x → Sort u_1) →
  (x : ℕ) →
    (x_1 x_2 : Fin2 x) →
      ((n : ℕ) → motive (n + 1) Fin2.fz Fin2.fz) →
        ((n : ℕ) → (j : Fin2 n) → motive (n + 1) Fin2.fz j.fs) →
          ((a : ℕ) → (a_1 : Fin2 a.succ) → motive (a.succ + 1) a_1.fs Fin2.fz) →
            ((a : ℕ) → (i : Fin2 a.succ) → (j : Fin2 (a + 1)) → motive (a.succ + 1) i.fs j.fs) → motive x x_1 x_2
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
/-- the chain complex must be degreewise projective  -/
CategoryTheory.ProjectiveResolution.projective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (self : CategoryTheory.ProjectiveResolution Z) (n : ℕ),
  CategoryTheory.Projective (self.complex.X n)
-- Mathlib.GroupTheory.Congruence.Defs
AddConGen.Rel.below.add : ∀ {M : Type u_1} [inst : Add M] {r : M → M → Prop} {motive : (a a_1 : M) → AddConGen.Rel r a a_1 → Prop} {w x y z : M}
  (a : AddConGen.Rel r w x) (a_1 : AddConGen.Rel r y z),
  AddConGen.Rel.below a → motive w x a → AddConGen.Rel.below a_1 → motive y z a_1 → AddConGen.Rel.below ⋯
-- Mathlib.Combinatorics.SimpleGraph.Dart
SimpleGraph.Dart.mk.sizeOf_spec : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : SizeOf V] (toProd : V × V) (adj : G.Adj toProd.1 toProd.2),
  sizeOf { toProd := toProd, adj := adj } = 1 + sizeOf toProd + sizeOf adj
-- Mathlib.Algebra.Homology.LeftResolution.Reduced
CategoryTheory.Abelian.LeftResolution.karoubi_π : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive A] [inst_4 : ι.Additive],
  Λ.karoubi.π = CategoryTheory.Abelian.LeftResolution.karoubi.π Λ
-- Mathlib.CategoryTheory.Presentable.Directed
/-- the unique map to the terminal object in the diagram  -/
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.lift : {J : Type w} →
  [inst : CategoryTheory.SmallCategory J] →
    {κ : Cardinal.{w}} →
      {D : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ} →
        {e : J} → D.IsTerminal e → {j : J} → D.P j → (j ⟶ e)
-- Mathlib.Analysis.Convex.Between
Sbtw.trans_left : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] [IsDomain R] [Module.IsTorsionFree R V]
  {w x y z : P}, Sbtw R w y z → Sbtw R w x y → Sbtw R w x z
-- Mathlib.Data.TypeVec
/-- `prod α β` is the pointwise product of the components of `α` and `β`  -/
TypeVec.prod : {n : ℕ} → TypeVec.{u} n → TypeVec.{u} n → TypeVec.{u} n
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
/-- The rightmost object of the fork diagram of the Stacks entry, which
contains the data used to check a family of elements for a presieve is compatible.
 -/
CategoryTheory.Equalizer.Presieve.SecondObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor Cᵒᵖ (Type (max v u)) →
      {X : C} → (R : CategoryTheory.Presieve X) → [R.HasPairwisePullbacks] → Type (max v u)
-- Lean.Compiler.IR.Format
_private.Lean.Compiler.IR.Format.0.Lean.IR.formatExpr : Lean.IR.Expr → Std.Format
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.instIsCodirectedOrderElemOpensOpenNhds : ∀ {α : Type u_1} [inst : TopologicalSpace α] (K : TopologicalSpace.Compacts α), IsCodirectedOrder ↑K.openNhds
-- Mathlib.RingTheory.PowerSeries.Order
/-- The order of the `0` power series is infinite.  -/
PowerSeries.order_zero : ∀ {R : Type u_1} [inst : Semiring R], PowerSeries.order 0 = ⊤
-- Mathlib.Algebra.Group.Commute.Defs
Commute.one_left : ∀ {M : Type u_2} [inst : MulOneClass M] (a : M), Commute 1 a
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.equivAddSubgroupOrbitsSetoidComap.eq_1 : ∀ {G : Type u} {X : Type v} [inst : AddGroup G] [inst_1 : AddAction G X] (H : AddSubgroup G)
  (ω : Quotient (AddAction.orbitRel G X)),
  AddAction.equivAddSubgroupOrbitsSetoidComap H ω =
    { toFun := fun q => Quotient.liftOn' q (fun x => ⟦⟨↑x, ⋯⟩⟧) ⋯, invFun := fun q => q.liftOn' (fun x => ⟦⟨↑x, ⋯⟩⟧) ⋯,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.of_natCast : ∀ {ι : Type u_1} [inst : DecidableEq ι] (A : ι → Type u_2) [inst_1 : (i : ι) → AddCommMonoid (A i)]
  [inst_2 : AddMonoid ι] [inst_3 : DirectSum.GSemiring A] (n : ℕ), (DirectSum.of A 0) ↑n = ↑n
-- Mathlib.CategoryTheory.Comma.Over.Pullback
/-- If `F` is a left adjoint and its source category has pullbacks, then so is
`post F : Over Y ⥤ Over (G Y)`.

If the right adjoint of `F` is `G`, then the right adjoint of `post F` is given by
`(Y ⟶ F X) ↦ (G Y ⟶ X ×_{G F X} G Y ⟶ X)`.  -/
CategoryTheory.Over.postAdjunctionLeft : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.Limits.HasPullbacks C] →
          {X : C} →
            {F : CategoryTheory.Functor C D} →
              {G : CategoryTheory.Functor D C} →
                (a : F ⊣ G) →
                  CategoryTheory.Over.post F ⊣
                    (CategoryTheory.Over.post G).comp (CategoryTheory.Over.pullback (a.unit.app X))
-- Mathlib.Algebra.Divisibility.Units
/-- In a commutative monoid, an element `a` divides an element `b` iff `a` divides all left
associates of `b`.  -/
Units.dvd_mul_left : ∀ {α : Type u_1} [inst : CommMonoid α] {a b : α} {u : αˣ}, a ∣ ↑u * b ↔ a ∣ b
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
/-- If a function is the least upper bound of countably many measurable functions on a measurable
set `s`, and coincides with a measurable function outside of `s`, then it is measurable.  -/
Measurable.isLUB_of_mem : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_5}
  [Countable ι] {f : ι → δ → α} {g g' : δ → α},
  (∀ (i : ι), Measurable (f i)) →
    ∀ {s : Set δ},
      MeasurableSet s → (∀ b ∈ s, IsLUB {a | ∃ i, f i b = a} (g b)) → Set.EqOn g g' sᶜ → Measurable g' → Measurable g
-- Mathlib.Topology.Bases
/-- A dense sequence in a non-empty separable topological space.

If `α` might be empty, then `TopologicalSpace.exists_countable_dense` is the main way to use
separability of `α`.  -/
TopologicalSpace.denseSeq : (α : Type u) → [t : TopologicalSpace α] → [TopologicalSpace.SeparableSpace α] → [Nonempty α] → ℕ → α
-- Mathlib.Algebra.Homology.HomologicalComplex
ComplexShape.up.congr_simp : ∀ (α : Type u_2) [inst : Add α] [inst_1 : IsRightCancelAdd α] [inst_2 : One α], ComplexShape.up α = ComplexShape.up α
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.mkResult : Array Lean.MVarId → Lean.Meta.Sym.UnifyM✝ Lean.Meta.Sym.MatchUnifyResult
-- Mathlib.Topology.Bornology.Basic
Bornology.isBounded_union : ∀ {α : Type u_2} {x : Bornology α} {s t : Set α},
  Bornology.IsBounded (s ∪ t) ↔ Bornology.IsBounded s ∧ Bornology.IsBounded t