mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.Nat.TakeDrop
List.take_eq_take_min : ∀ {α : Type u_1} {l : List α} {i : ℕ}, List.take i l = List.take (min i l.length) l
-- Mathlib.MeasureTheory.Group.Arithmetic
measurableSMul₂_opposite_of_add : ∀ {M : Type u_2} [inst : Add M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M], MeasurableVAdd₂ Mᵃᵒᵖ M
-- Aesop.Builder.Basic
Aesop.elabInductiveRuleIdent : Aesop.BuilderName → Lean.Term → Lean.Meta.TransparencyMode → Lean.Elab.TermElabM (Lean.Name × Lean.InductiveVal)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.DoIfView.mk.sizeOf_spec : ∀ (ref optIdent cond thenBranch elseBranch : Lean.Syntax),
  sizeOf { ref := ref, optIdent := optIdent, cond := cond, thenBranch := thenBranch, elseBranch := elseBranch } =
    1 + sizeOf ref + sizeOf optIdent + sizeOf cond + sizeOf thenBranch + sizeOf elseBranch
-- Mathlib.Analysis.Convex.Gauge
gauge_zero' : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E], gauge 0 = 0
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.ReflQuiv.forgetToQuiv_map : ∀ {X Y : CategoryTheory.ReflQuiv} (F : X ⟶ Y), CategoryTheory.ReflQuiv.forgetToQuiv.map F = F.toPrefunctor
-- Init.Data.UInt.Lemmas
UInt16.toNat_ofNatTruncate_of_le : ∀ {n : ℕ}, UInt16.size ≤ n → (UInt16.ofNatClamp n).toNat = UInt16.size - 1
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicofork.isoOfπ_hom_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  {I : CategoryTheory.Limits.MultispanIndex J C} (t : CategoryTheory.Limits.Multicofork I),
  t.isoOfπ.hom.hom = CategoryTheory.CategoryStruct.id t.pt
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.instUniqueI₀SchemeCover : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {X S : AlgebraicGeometry.Scheme} →
    (f : X ⟶ S) →
      (hf : P f) → [inst : AlgebraicGeometry.Surjective f] → Unique (AlgebraicGeometry.Scheme.Hom.cover f hf).I₀
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.coe_mker : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F), ↑(AddMonoidHom.mker f) = ⇑f ⁻¹' {0}
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
/-- The fudge factor that appears in the formula for the volume of `convexBodyLT`.  -/
NumberField.mixedEmbedding.convexBodyLTFactor : (K : Type u_1) → [inst : Field K] → [NumberField K] → NNReal
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.δ_comp_zero_cocycle : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G K : CochainComplex C ℤ} {n : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n)
  (z₂ : CochainComplex.HomComplex.Cocycle G K 0) (m : ℤ),
  CochainComplex.HomComplex.δ n m (z₁.comp ↑z₂ ⋯) = (CochainComplex.HomComplex.δ n m z₁).comp ↑z₂ ⋯
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.comp_id : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂), f.comp LinearIsometry.id = f
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
fderivWithin_continuousAlternatingMap_apply_const : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {s : Set E} {ι : Type u_5} {c : E → F [⋀^ι]→L[𝕜] G}
  [inst_7 : Fintype ι],
  UniqueDiffWithinAt 𝕜 s x →
    DifferentiableWithinAt 𝕜 c s x →
      ∀ (u : ι → F), fderivWithin 𝕜 (fun y => (c y) u) s x = (fderivWithin 𝕜 c s x).flipAlternating u
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.codRestrict_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {S : Type u_5} [inst_2 : SetLike S N]
  [inst_3 : AddSubmonoidClass S N] (f : M →+ N) (s : S) (h : ∀ (x : M), f x ∈ s) (n : M),
  (f.codRestrict s h) n = ⟨f n, ⋯⟩
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.Hereditarily.mem : ∀ {p : ZFSet.{u} → Prop} {x y : ZFSet.{u}}, ZFSet.Hereditarily p x → y ∈ x → ZFSet.Hereditarily p y
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.step_filterMapWithPostcondition.match_3.splitter : {α β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    [inst : Std.Iterator α m β] →
      {it : Std.IterM m β} →
        (motive : it.Step → Sort u_3) →
          (x : it.Step) →
            ((it' : Std.IterM m β) →
                (out : β) →
                  (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
              ((it' : Std.IterM m β) →
                  (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
                ((h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Functor.sheafPushforwardContinuousId_inv_app_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (A : Type u) [inst_1 : CategoryTheory.Category.{t, u} A]
  (J : CategoryTheory.GrothendieckTopology C) (X : CategoryTheory.Sheaf J A) (X_1 : Cᵒᵖ),
  ((CategoryTheory.Functor.sheafPushforwardContinuousId A J).inv.app X).hom.app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj.obj X_1)
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.arrowCongr_comp : ∀ {R₁ : Type u_9} {R₂ : Type u_10} {R₁' : Type u_12} {R₂' : Type u_13} {R₁'' : Type u_15} {R₂'' : Type u_16}
  {M₁ : Type u_17} {M₂ : Type u_18} {M₁' : Type u_20} {M₂' : Type u_21} {M₁'' : Type u_23} {M₂'' : Type u_24}
  [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : CommSemiring R₁'] [inst_3 : CommSemiring R₂']
  [inst_4 : CommSemiring R₁''] [inst_5 : CommSemiring R₂''] [inst_6 : AddCommMonoid M₁] [inst_7 : AddCommMonoid M₂]
  [inst_8 : AddCommMonoid M₁'] [inst_9 : AddCommMonoid M₂'] [inst_10 : AddCommMonoid M₁'']
  [inst_11 : AddCommMonoid M₂''] [inst_12 : Module R₁ M₁] [inst_13 : Module R₂ M₂] [inst_14 : Module R₁' M₁']
  [inst_15 : Module R₂' M₂'] [inst_16 : Module R₁'' M₁''] [inst_17 : Module R₂'' M₂''] {σ₁₂ : R₁ →+* R₂}
  {σ₂₁ : R₂ →+* R₁} {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} {σ₁''₂'' : R₁'' →+* R₂''} {σ₂''₁'' : R₂'' →+* R₁''}
  {σ₁₁' : R₁ →+* R₁'} {σ₂₂' : R₂ →+* R₂'} {σ₁'₁'' : R₁' →+* R₁''} {σ₂'₂'' : R₂' →+* R₂''} {σ₁₁'' : R₁ →+* R₁''}
  {σ₂₂'' : R₂ →+* R₂''} {σ₂₁' : R₂ →+* R₁'} {σ₁₂' : R₁ →+* R₂'} {σ₂'₁'' : R₂' →+* R₁''} {σ₁'₂'' : R₁' →+* R₂''}
  {σ₂₁'' : R₂ →+* R₁''} {σ₁₂'' : R₁ →+* R₂''} [inst_18 : RingHomInvPair σ₁₂ σ₂₁] [inst_19 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_20 : RingHomInvPair σ₁'₂' σ₂'₁'], ⋯
-- Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
instBorelSpaceSubtypeMemOpens : ∀ {M : Type u_4} [inst : TopologicalSpace M] [inst_1 : MeasurableSpace M] [BorelSpace M] (U : TopologicalSpace.Opens M),
  BorelSpace ↥U
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeff_sum : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {k' : Type u_3} {G' : Type u_4} [inst_1 : AddCommMonoid k']
  {f : SkewMonoidAlgebra k G} {g : G → k → SkewMonoidAlgebra k' G'} {a₂ : G'},
  (f.sum g).coeff a₂ = f.sum fun a₁ b => (g a₁ b).coeff a₂
-- Mathlib.Data.Finset.Sups
Finset.Nonempty.of_disjSups_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] [inst_2 : OrderBot α]
  [inst_3 : DecidableRel Disjoint] {s t : Finset α}, (s.disjSups t).Nonempty → s.Nonempty
-- Mathlib.Order.Interval.Lex
NonemptyInterval.instDecidableLTLexOfDecidableEq : {α : Type u_1} →
  [inst : LT α] → [inst_1 : LE α] → [DecidableEq α] → [DecidableLT α] → DecidableLT (Lex (NonemptyInterval α))
-- Mathlib.CategoryTheory.Sites.Subcanonical
CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_naturality_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] {X X' : C} (f : X' ⟶ X) (F : CategoryTheory.Sheaf J (Type (max v v')))
  (x : F.obj.obj (Opposite.op X)),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).map f)
      (J.uliftYonedaEquiv.symm x) =
    J.uliftYonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.obj.map f.op)) x)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_eq_fallback : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} {fallback : β}, a ∉ m → Std.ExtDHashMap.Const.getD m a fallback = fallback
-- Batteries.Tactic.Alias
/-- Get the alias information for a name  -/
Batteries.Tactic.Alias.getAliasInfo? : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m (Option Batteries.Tactic.Alias.AliasInfo)
-- Mathlib.Analysis.Normed.Group.Basic
mem_ball_iff_norm_neg_add_lt' : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {a b : E} {r : ℝ}, b ∈ Metric.ball a r ↔ ‖-a + b‖ < r
-- Mathlib.Topology.Neighborhoods
IsOpen.mem_nhds_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X}, IsOpen s → (s ∈ nhds x ↔ x ∈ s)
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.integrable_densityProcess : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ},
  κ.fst ≤ ν →
    ∀ [ProbabilityTheory.IsFiniteKernel ν] (n : ℕ) (a : α) {s : Set β},
      MeasurableSet s → MeasureTheory.Integrable (fun x => κ.densityProcess ν n a x s) (ν a)
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
/-- A verbose specialization of `threeAPFree.le_addRothNumber`, sometimes convenient in
practice.  -/
ThreeAPFree.le_rothNumberNat : ∀ {k n : ℕ} (s : Finset ℕ), ThreeAPFree ↑s → (∀ x ∈ s, x < n) → s.card = k → k ≤ rothNumberNat n
-- Mathlib.MeasureTheory.Constructions.HaarToSphere
MeasureTheory.Measure.toSphere_eq_zero_iff_finrank : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  (μ : MeasureTheory.Measure E) [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure],
  μ.toSphere = 0 ↔ Module.finrank ℝ E = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.toNormalizedChainComplex_normalizedChainComplexMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] {X Y : SSet} (f : X ⟶ Y) (R : C),
  CategoryTheory.CategoryStruct.comp (X.toNormalizedChainComplex R) (SSet.normalizedChainComplexMap f R) =
    CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap f R) (Y.toNormalizedChainComplex R)
-- Mathlib.Order.MinMax
min_le_max : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, min a b ≤ max a b
-- Std.Time.Date.PlainDate
/-- Adds `Year.Offset` to a `PlainDate`, rolling over excess days to the next month, or next year.
 -/
Std.Time.PlainDate.addYearsRollOver : Std.Time.PlainDate → Std.Time.Year.Offset → Std.Time.PlainDate
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.forInStep.match_1.eq_2 : ∀ {δ : Type u_1} (motive : ForInStep δ → Sort u_2) (d : δ) (h_1 : (d : δ) → motive (ForInStep.done d))
  (h_2 : (d : δ) → motive (ForInStep.yield d)),
  (match ForInStep.yield d with
    | ForInStep.done d => h_1 d
    | ForInStep.yield d => h_2 d) =
    h_2 d
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.neg_modEq_neg : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a b : G}, -a ≡ -b [PMOD p] ↔ a ≡ b [PMOD p]
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.abs_cos_eq_abs_sin_of_two_zsmul_add_two_zsmul_eq_pi : ∀ {θ ψ : Real.Angle}, 2 • θ + 2 • ψ = ↑Real.pi → |θ.cos| = |ψ.sin|
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.GoalContext : Type
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Pos.apply_skipWhile_bool_eq_false : ∀ {p : Char → Bool} {s : String} {pos : s.Pos} {h : pos.skipWhile p ≠ s.endPos}, p ((pos.skipWhile p).get h) = false
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.orbitRel.Quotient.nonempty_orbit : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (x : AddAction.orbitRel.Quotient G α),
  x.orbit.Nonempty
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.isComplete_image_iff : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [inst : Semiring R]
  [inst_1 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂]
  [inst_4 : Module R E] [inst_5 : Module R₂ E₂] [inst_6 : FunLike 𝓕 E E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕)
  {s : Set E}, IsComplete (⇑f '' s) ↔ IsComplete s
-- Mathlib.Analysis.Fourier.AddCircle
hasDerivAt_fourier : ∀ (T : ℝ) (n : ℤ) (x : ℝ), HasDerivAt (fun y => (fourier n) ↑y) (2 * ↑Real.pi * Complex.I * ↑n / ↑T * (fourier n) ↑x) x
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonLeanModuleHierarchyImportedByParams : Lean.ToJson Lean.Lsp.LeanModuleHierarchyImportedByParams
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- In the specific case of continuous alternating maps on spaces indexed by `Fin (n+1)`, where one
can build an element of `Π(i : Fin (n+1)), M i` using `cons`, one can express directly the
multiplicativity of an alternating map along the first variable.  -/
ContinuousAlternatingMap.cons_smul : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N] [inst_6 : TopologicalSpace N] {n : ℕ}
  (f : M [⋀^Fin (n + 1)]→L[R] N) (m : Fin n → M) (c : R) (x : M), f (Fin.cons (c • x) m) = c • f (Fin.cons x m)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_eq_zero_iff_of_pos : ∀ {x : ENNReal} {y : ℝ}, 0 < y → (x ^ y = 0 ↔ x = 0)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.State.mk.injEq : ∀ (congrThms : Lean.PHashMap Lean.Meta.Grind.CongrTheoremCacheKey Lean.Meta.CongrTheorem) (simp : Lean.Meta.Simp.State)
  (lastTag : Lean.Name) (counters : Lean.Meta.Grind.Counters) (splitDiags : Lean.PArray Lean.Meta.Grind.SplitDiagInfo)
  (ematchDiags : Lean.PArray Lean.Meta.Grind.EMatchDiagInfo)
  (lawfulEqCmpMap reflCmpMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option Lean.Expr))
  (anchors : Lean.PHashMap Lean.Meta.Sym.ExprPtr UInt64)
  (instanceMap : Std.HashMap Lean.Name Lean.Meta.Grind.EMatchTheorem)
  (congrThms_1 : Lean.PHashMap Lean.Meta.Grind.CongrTheoremCacheKey Lean.Meta.CongrTheorem)
  (simp_1 : Lean.Meta.Simp.State) (lastTag_1 : Lean.Name) (counters_1 : Lean.Meta.Grind.Counters)
  (splitDiags_1 : Lean.PArray Lean.Meta.Grind.SplitDiagInfo)
  (ematchDiags_1 : Lean.PArray Lean.Meta.Grind.EMatchDiagInfo)
  (lawfulEqCmpMap_1 reflCmpMap_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option Lean.Expr))
  (anchors_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr UInt64)
  (instanceMap_1 : Std.HashMap Lean.Name Lean.Meta.Grind.EMatchTheorem),
  ({ congrThms := congrThms, simp := simp, lastTag := lastTag, counters := counters, splitDiags := splitDiags,
        ematchDiags := ematchDiags, lawfulEqCmpMap := lawfulEqCmpMap, reflCmpMap := reflCmpMap, anchors := anchors,
        instanceMap := instanceMap } =
      { congrThms := congrThms_1, simp := simp_1, lastTag := lastTag_1, counters := counters_1,
        splitDiags := splitDiags_1, ematchDiags := ematchDiags_1, lawfulEqCmpMap := lawfulEqCmpMap_1,
        reflCmpMap := reflCmpMap_1, anchors := anchors_1, instanceMap := instanceMap_1 }) =
    (congrThms = congrThms_1 ∧
      simp = simp_1 ∧
        lastTag = lastTag_1 ∧
          counters = counters_1 ∧
            splitDiags = splitDiags_1 ∧
              ematchDiags = ematchDiags_1 ∧
                lawfulEqCmpMap = lawfulEqCmpMap_1 ∧
                  reflCmpMap = reflCmpMap_1 ∧ anchors = anchors_1 ∧ instanceMap = instanceMap_1)
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.ofMonoidHom.inj : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {inst : Monoid G} {inst_1 : Ring R} {inst_2 : AddCommGroup V}
  {inst_3 : TopologicalSpace V} {inst_4 : IsTopologicalAddGroup V} {inst_5 : Module R V}
  {toMonoidHom toMonoidHom_1 : G →* V →L[R] V},
  { toMonoidHom := toMonoidHom } = { toMonoidHom := toMonoidHom_1 } → toMonoidHom = toMonoidHom_1
-- Init.Data.Array.Attach
Array.map_attachWith_eq_pmap : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {P : α → Prop} {H : ∀ a ∈ xs, P a} {f : { x // P x } → β},
  Array.map f (xs.attachWith P H) = Array.pmap (fun a h => f ⟨a, ⋯⟩) xs ⋯
-- Mathlib.AlgebraicTopology.ModelCategory.Over
HomotopicalAlgebra.instCategoryWithCofibrationsOver : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (S : C) →
      [HomotopicalAlgebra.CategoryWithCofibrations C] →
        HomotopicalAlgebra.CategoryWithCofibrations (CategoryTheory.Over S)
-- Init.Data.SInt.Basic
instInhabitedInt8 : Inhabited Int8
-- Init.Data.Rat.Basic
Rat.instIntCast : IntCast ℚ
-- Mathlib.Data.Nat.Factorial.Basic
Nat.ascFactorial.eq_1 : ∀ (n : ℕ), n.ascFactorial 0 = 1
-- Mathlib.Order.Lattice
Monotone.of_map_sup : ∀ {α : Type u} {β : Type v} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] {f : α → β},
  (∀ (x y : α), f (x ⊔ y) = f x ⊔ f y) → Monotone f
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCountableLimits C],
  CategoryTheory.Limits.HasFiniteLimits C
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.left_triangle : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight adj.unit F)
      (CategoryTheory.CategoryStruct.comp (F.associator G F).hom (F.whiskerLeft adj.counit)) =
    CategoryTheory.CategoryStruct.comp F.leftUnitor.hom F.rightUnitor.inv
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  {S : CategoryTheory.ShortComplex C},
  S.ShortExact →
    ∀ (n : ℕ),
      CategoryTheory.HasProjectiveDimensionLT S.X₁ n →
        CategoryTheory.HasProjectiveDimensionLT S.X₂ (n + 1) → CategoryTheory.HasProjectiveDimensionLT S.X₃ (n + 1)
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
CategoryTheory.Preadditive.RightFreyd.Candidate.instEpiMapArrowQuotientπ : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts V] {u v : CategoryTheory.Arrow V} (f : u ⟶ v),
  CategoryTheory.Epi
    ((CategoryTheory.Preadditive.RightFreyd.quotient V).map (CategoryTheory.Preadditive.RightFreyd.Candidate.π f))
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.WF.diff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α}, m₁.WF → m₂.WF → (m₁ \ m₂).WF
-- Mathlib.LinearAlgebra.Finsupp.VectorSpace
/-- For any `r : R`, `s : S`, we have
`B.repr ((algebra_map R S r) * s) i = r * (B.repr s i) `.  -/
Module.Basis.repr_smul' : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {ι : Type u_3}
  (B : Module.Basis ι R S) (i : ι) (r : R) (s : S), (B.repr ((algebraMap R S) r * s)) i = r * (B.repr s) i
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.mem_ker : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {f : M →ₛₗ[τ₁₂] M₂} {y : M}, y ∈ f.ker ↔ f y = 0
-- Mathlib.CategoryTheory.Sites.Whiskering
/-- Mapping the multifork associated to a cover `S : J.Cover X` and a presheaf `P` with
respect to a functor `F` is isomorphic (upto a natural isomorphism of the underlying functors)
to the multifork associated to `S` and `P ⋙ F`.  -/
CategoryTheory.GrothendieckTopology.Cover.mapMultifork : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        {B : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} B] →
            {J : CategoryTheory.GrothendieckTopology C} →
              (F : CategoryTheory.Functor A B) →
                (P : CategoryTheory.Functor Cᵒᵖ A) →
                  {X : C} →
                    (S : J.Cover X) →
                      F.mapCone (S.multifork P) ≅
                        (CategoryTheory.Limits.Cone.postcompose
                              (CategoryTheory.GrothendieckTopology.Cover.multicospanComp F P S).hom).obj
                          (S.multifork (P.comp F))
-- Init.Data.String.OrderInstances
String.Pos.instLinearOrderPackage : {s : String} → Std.LinearOrderPackage s.Pos
-- Mathlib.FieldTheory.AbelRuffini
IsSolvableByRad.neg : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (α : E),
  IsSolvableByRad F α → IsSolvableByRad F (-α)
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.mor₁_eq_zero_iff_epi₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, T.mor₁ = 0 ↔ CategoryTheory.Epi T.mor₃
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.OneCochain.instGroup : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {G : CategoryTheory.Functor Cᵒᵖ GrpCat} →
      {I : Type w'} → {U : I → C} → Group (CategoryTheory.PresheafOfGroups.OneCochain G U)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instMulZeroClass : {α : Type u_1} → {l : Filter α} → {R : Type u_5} → [MulZeroClass R] → MulZeroClass (l.Germ R)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.size_insertMany_list_le : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {l : List α},
  (t.insertMany l).size ≤ t.size + l.length
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.IsSeparatedFor.of_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P Q : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X} (f : P ⟶ Q) [CategoryTheory.Mono f],
  CategoryTheory.Presieve.IsSeparatedFor Q R → CategoryTheory.Presieve.IsSeparatedFor P R
-- Mathlib.Topology.Algebra.Order.UpperLower
instHasUpperLowerClosureOrderDual : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α] [HasUpperLowerClosure α], HasUpperLowerClosure αᵒᵈ
-- Std.Async.Basic
/-- Lifts an `EIO` action into an `EAsync` computation.
 -/
Std.Async.EAsync.lift : {ε α : Type} → EIO ε α → Std.Async.EAsync ε α
-- Mathlib.Algebra.Polynomial.Splits
/-- **Alias** of `Polynomial.splits_mul`. -/
Polynomial.splits_mul_iff : ∀ {R : Type u_1} [inst : CommRing R] {f g : Polynomial R} [IsDomain R],
  f ≠ 0 → g ≠ 0 → ((f * g).Splits ↔ f.Splits ∧ g.Splits)
-- Mathlib.FieldTheory.SeparableClosure
/-- A separable extension has inseparable degree one.  -/
Algebra.IsSeparable.insepDegree_eq : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.IsSeparable F E],
  Field.insepDegree F E = 1
-- Mathlib.RingTheory.Binomial
Int.instBinomialRing : BinomialRing ℤ
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.cycleBypass_nil : ∀ {V : Type u} {G : SimpleGraph V} {v : V} [inst : DecidableEq V],
  SimpleGraph.Walk.nil.cycleBypass = SimpleGraph.Walk.nil