mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.elabMutualDef.finishElab : Array Lean.Expr →
  Lean.Elab.Command.Scope → Array Lean.Elab.DefView → Array Lean.Elab.DefViewElabHeader → Lean.Elab.TermElabM Unit
-- Lean.Meta.Match.MatcherApp.Transform
/-- Auxiliary function for MatcherApp.addArg  -/
_private.Lean.Meta.Match.MatcherApp.Transform.0.Lean.Meta.MatcherApp.updateAlts : Lean.Expr → Lean.Expr → Array ℕ → Array Lean.Expr → Bool → ℕ → Lean.MetaM (Array Lean.Expr)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.getOfNatThm? : Lean.Meta.Grind.Arith.Cutsat.ToIntM (Option Lean.Expr)
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.coe_toSubsemiring : ∀ {R : Type u} [inst : NonAssocRing R] (s : Subring R), ↑s.toSubsemiring = ↑s
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.absNorm_pos_of_nonZeroDivisors : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] [Module.Finite ℤ S]
  (I : ↥(nonZeroDivisors (Ideal S))), 0 < Ideal.absNorm ↑I
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.finite_genWeightSpace_ne_bot : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [IsDomain R] [Module.IsTorsionFree R M] [IsNoetherian R M],
  {χ | LieModule.genWeightSpace M χ ≠ ⊥}.Finite
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.instMul : {ι : Type u_1} →
  {A : Type u_2} → {σ : Type u_6} → [inst : Semiring A] → [inst_1 : SetLike σ A] → {𝒜 : ι → σ} → Mul (𝒜 →+*ᵍ 𝒜)
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.inf_toSubmodule : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N N' : LieSubmodule R L M), ↑(N ⊓ N') = ↑N ⊓ ↑N'
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.Triangle.invRotate_mor₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C),
  T.invRotate.mor₃ =
    CategoryTheory.CategoryStruct.comp T.mor₂ ((CategoryTheory.shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app T.3)
-- Init.Data.SInt.Basic
ISize.ofUSize.injEq : ∀ (toUSize toUSize_1 : USize), ({ toUSize := toUSize } = { toUSize := toUSize_1 }) = (toUSize = toUSize_1)
-- Mathlib.Analysis.Analytic.Constructions
AnalyticOnNhd.const_smul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E}
  {R : Type u_9} [inst_5 : NormedRing R] [inst_6 : Module R F] [IsBoundedSMul R F] [SMulCommClass 𝕜 R F] {c : R},
  AnalyticOnNhd 𝕜 f s → AnalyticOnNhd 𝕜 (c • f) s
-- Mathlib.Data.Fin.SuccPred
Fin.pred_le_iff : ∀ {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ 0), i.pred hi ≤ j ↔ i ≤ j.succ
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.mapRingHom_comp_includeLeftRingHom : ∀ {R : Type u_3} {S : Type u_4} {T : Type u_5} {R' : Type u_6} {S' : Type u_7} {T' : Type u_8} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : CommSemiring T] [inst_3 : Algebra R S] [inst_4 : Algebra R T]
  [inst_5 : CommSemiring R'] [inst_6 : CommSemiring S'] [inst_7 : CommSemiring T'] [inst_8 : Algebra R' S']
  [inst_9 : Algebra R' T'] (fR : R →+* R') (fS : S →+* S') (fT : T →+* T')
  (HS : fS.comp (algebraMap R S) = (algebraMap R' S').comp fR)
  (HT : fT.comp (algebraMap R T) = (algebraMap R' T').comp fR),
  (Algebra.TensorProduct.mapRingHom fR fS fT HS HT).comp Algebra.TensorProduct.includeLeftRingHom =
    Algebra.TensorProduct.includeLeftRingHom.comp fS
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
_private.Mathlib.Algebra.Homology.ShortComplex.ModuleCat.0.exact_conj_of_exact : ∀ {R : Type u} [inst : Ring R] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type v}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {L : Type v} [inst_5 : AddCommGroup L] [inst_6 : Module R L]
  {M' : Type u_1} {N' : Type u_2} {L' : Type u_3} [inst_7 : AddCommGroup M'] [inst_8 : AddCommGroup N']
  [inst_9 : AddCommGroup L'] [inst_10 : Module R M'] [inst_11 : Module R N'] [inst_12 : Module R L'] (eM : M ≃ₗ[R] M')
  (eN : N ≃ₗ[R] N') (eL : L ≃ₗ[R] L') (f : M' →ₗ[R] N') (g : N' →ₗ[R] L'),
  Function.Exact ⇑f ⇑g → Function.Exact ⇑((↑eN.symm ∘ₗ f) ∘ₗ ↑eM) ⇑(↑eL.symm ∘ₗ g ∘ₗ ↑eN)
-- Mathlib.RingTheory.Jacobson.Ring
/-- If `f : R →+* S` is a ring homomorphism from a Jacobson ring to a field,
then it is finite if and only if it is finite type.
 -/
RingHom.finite_iff_finiteType_of_isJacobsonRing : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [IsJacobsonRing R] [inst_2 : Field S] {f : R →+* S},
  f.Finite ↔ f.FiniteType
-- Lean.Data.Lsp.Internal
/-- Shortened representation of `RefIdent.const` for more compact serialization.  -/
Lean.Lsp.RefIdent.RefIdentJsonRepr.c : String → String → Lean.Lsp.RefIdent.RefIdentJsonRepr
-- Std.Data.Iterators.Lemmas.Combinators.Drop
Std.Iter.toListRev_drop : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {n : ℕ} [Std.Iterators.Finite α Id] {it : Std.Iter β},
  (Std.Iter.drop n it).toListRev = List.take (it.toList.length - n) it.toList.reverse
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.reverse_reverse : ∀ {n : ℕ} (c : Composition n), c.reverse.reverse = c
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tan_add_nat_mul_pi : ∀ (x : ℝ) (n : ℕ), Real.tan (x + ↑n * Real.pi) = Real.tan x
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Adjunction.map_η_comp_η_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [inst_4 : F.Monoidal]
  [inst_5 : G.Monoidal] [adj.IsMonoidal] {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Functor.OplaxMonoidal.η G))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η F) h) =
    CategoryTheory.CategoryStruct.comp (adj.counit.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) h
-- Init.Data.List.Monadic
/-- We can express a for loop over a list as a fold,
in which whenever we reach `.done b` we keep that value through the rest of the fold.
 -/
List.forIn'_eq_foldlM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {l : List α}
  (f : (a : α) → a ∈ l → β → m (ForInStep β)) (init : β),
  forIn' l init f =
    ForInStep.value <$>
      List.foldlM
        (fun b x =>
          match x with
          | ⟨a, m_1⟩ =>
            match b with
            | ForInStep.yield b => f a m_1 b
            | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l.attach
-- Mathlib.Algebra.Opposites
MulOpposite.op_sub : ∀ {α : Type u_1} [inst : Sub α] (x y : α), MulOpposite.op (x - y) = MulOpposite.op x - MulOpposite.op y
-- Lean.Elab.DeclModifiers
/-- Input syntax, used for adjusting declaration range (unless missing)  -/
Lean.Elab.Modifiers.stx : Lean.Elab.Modifiers → Lean.TSyntax `Lean.Parser.Command.declModifiers
-- Mathlib.RingTheory.MvPolynomial.Groebner
MonomialOrder.degree_sub_LTerm_lt : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] {f : MvPolynomial σ R},
  m.degree f ≠ 0 → m.toSyn (m.degree (m.subLTerm f)) < m.toSyn (m.degree f)
-- Mathlib.Geometry.Manifold.Instances.Sphere
stereoInvFun_apply : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {v : E} (hv : ‖v‖ = 1) (w : ↥(ℝ ∙ v)ᗮ),
  ↑(stereoInvFun hv w) = (‖w‖ ^ 2 + 4)⁻¹ • (4 • ↑w + (‖w‖ ^ 2 - 4) • v)
-- Init.Control.Basic
forIn_eq_forIn' : ∀ {α : Type u_1} {ρ : Type u_2} {m : Type u_3 → Type u_4} [d : Membership α ρ] [inst : ForIn' m ρ α d] {β : Type u_3}
  (x : ρ) (b : β) (f : α → β → m (ForInStep β)),
  forIn x b f = forIn' x b fun x_1 h => binderNameHint x_1 f (binderNameHint h () (f x_1))
-- Mathlib.Probability.Kernel.Basic
/-- Constant kernel, which always returns the same measure.  -/
ProbabilityTheory.Kernel.const : (α : Type u_4) →
  {β : Type u_5} →
    [inst : MeasurableSpace α] → {x : MeasurableSpace β} → MeasureTheory.Measure β → ProbabilityTheory.Kernel α β
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
StarAlgEquiv.ofLeftInverse'_symm_apply : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A]
  [inst_2 : Module R A] [inst_3 : Star A] [inst_4 : NonUnitalSemiring B] [inst_5 : Module R B] [inst_6 : Star B]
  [inst_7 : FunLike F A B] [inst_8 : NonUnitalAlgHomClass F R A B] [inst_9 : StarHomClass F A B] {g : B → A} {f : F}
  (h : Function.LeftInverse g ⇑f) (x : ↥(NonUnitalStarAlgHom.range f)), (StarAlgEquiv.ofLeftInverse' h).symm x = g ↑x
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minEntry!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Inhabited ((a : α) × β a)],
  Std.DTreeMap.Internal.Impl.leaf.minEntry! =
    panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.minEntry!" 367 13
      "Map is empty"
-- Mathlib.Combinatorics.Tiling.Tile
/-- A `Prototile G X` describes a tile in `X`, copies of which under elements of `G` may be used in
tilings. Two copies related by an element of `symmetries` are considered the same; two copies not so
related, even if they have the same points, are considered distinct.  -/
DiscreteTiling.Prototile : (G : Type u_1) → (X : Type u_2) → [inst : Group G] → [MulAction G X] → Type (max u_1 u_2)
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
QuadraticMap.tensorDistrib_tmul : ∀ {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} {N₁ : Type uN₁} {N₂ : Type uN₂} [inst : CommRing R]
  [inst_1 : CommRing A] [inst_2 : AddCommGroup M₁] [inst_3 : AddCommGroup M₂] [inst_4 : AddCommGroup N₁]
  [inst_5 : AddCommGroup N₂] [inst_6 : Algebra R A] [inst_7 : Module R M₁] [inst_8 : Module A M₁] [inst_9 : Module R N₁]
  [inst_10 : Module A N₁] [inst_11 : SMulCommClass R A M₁] [inst_12 : IsScalarTower R A M₁]
  [inst_13 : IsScalarTower R A N₁] [inst_14 : Module R M₂] [inst_15 : Module R N₂] [inst_16 : Invertible 2]
  (Q₁ : QuadraticMap A M₁ N₁) (Q₂ : QuadraticMap R M₂ N₂) (m₁ : M₁) (m₂ : M₂),
  ((QuadraticMap.tensorDistrib R A) (Q₁ ⊗ₜ[R] Q₂)) (m₁ ⊗ₜ[R] m₂) = Q₁ m₁ ⊗ₜ[R] Q₂ m₂
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pseudofunctor.ofOplaxFunctorToLocallyGroupoid_mapIdIso_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {B' : Type u₂} [inst_1 : CategoryTheory.Bicategory B']
  [inst_2 : CategoryTheory.Bicategory.IsLocallyGroupoid B] (F : CategoryTheory.OplaxFunctor B' B) (x : B'),
  ((CategoryTheory.Bicategory.Pseudofunctor.ofOplaxFunctorToLocallyGroupoid F).mapIdIso x).inv =
    CategoryTheory.inv (F.mapId x)
-- Mathlib.Order.Filter.Pointwise
Filter.inv.instNeBot : ∀ {α : Type u_2} [inst : Inv α] {f : Filter α} [f.NeBot], f⁻¹.NeBot
-- Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
/-- The (semi-)inner product space whose elements are the elements of `A`, but which has an
inner product-induced norm that is different from the norm on `A` and which is induced by `f`.
 -/
PositiveLinearMap.preGNSpreInnerProdSpace : {A : Type u_1} →
  [inst : NonUnitalCStarAlgebra A] →
    [inst_1 : PartialOrder A] → (f : A →ₚ[ℂ] ℂ) → [StarOrderedRing A] → PreInnerProductSpace.Core ℂ f.PreGNS
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
/-- The line polynomial `ℓ(X - x) + y` associated to the line `Y = ℓ(X - x) + y` that passes through
a nonsingular affine point `(x, y)` on a Weierstrass curve `W` with a slope of `ℓ`.

This does not depend on `W`, and has argument order: `x`, `y`, `ℓ`.  -/
WeierstrassCurve.Affine.linePolynomial : {R : Type r} → [inst : CommRing R] → R → R → R → Polynomial R
-- Mathlib.Data.Finset.Lattice.Basic
Finset.inter_subset_inter : ∀ {α : Type u_1} [inst : DecidableEq α] {x y s t : Finset α}, x ⊆ y → s ⊆ t → x ∩ s ⊆ y ∩ t
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_17.eq_2 : ∀ (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) (w : ℕ) (val : BitVec w)
  (h_1 : (w a : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var a))
  (h_2 : (w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val))
  (h_3 :
    (w : ℕ) →
      (lhsExpr : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinOp) →
          (rhsExpr : Std.Tactic.BVDecide.BVExpr w) → motive w (lhsExpr.bin op rhsExpr))
  (h_4 :
    (w : ℕ) →
      (op : Std.Tactic.BVDecide.BVUnOp) →
        (expr : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op expr))
  (h_5 :
    (w l r : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr l) →
        (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h))
  (h_6 :
    (w w_1 n : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w_1) →
        (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h))
  (h_7 :
    (len w start : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr))
  (h_8 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs))
  (h_9 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs))
  (h_10 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)),
  (match w, Std.Tactic.BVDecide.BVExpr.const val with
    | w, Std.Tactic.BVDecide.BVExpr.var a => h_1 w a
    | w, Std.Tactic.BVDecide.BVExpr.const val => h_2 w val
    | w, lhsExpr.bin op rhsExpr => h_3 w lhsExpr op rhsExpr
    | w, Std.Tactic.BVDecide.BVExpr.un op expr => h_4 w op expr
    | w, lhs.append rhs h => h_5 w l r lhs rhs h
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h => h_6 w w_1 n expr h
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr => h_7 len w start expr
    | w, lhs.shiftLeft rhs => h_8 w n lhs rhs
    | w, lhs.shiftRight rhs => h_9 w n lhs rhs
    | w, lhs.arithShiftRight rhs => h_10 w n lhs rhs) =
    h_2 w val
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.MeasurePreserving.setIntegral_image_emb : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure X} {Y : Type u_5} {x : MeasurableSpace Y} {f : X → Y} {ν : MeasureTheory.Measure Y},
  MeasureTheory.MeasurePreserving f μ ν →
    MeasurableEmbedding f → ∀ (g : Y → E) (s : Set X), ∫ (y : Y) in f '' s, g y ∂ν = ∫ (x : X) in s, g (f x) ∂μ
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.single_add : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)] (i : ι) (b₁ b₂ : β i),
  (fun₀ | i => b₁ + b₂) = (fun₀ | i => b₁) + fun₀ | i => b₂
-- Mathlib.GroupTheory.OrderOfElement
/-- Every finite right cancellative monoid is a group.  -/
RightCancelMonoid.groupOfFinite : {H : Type u_6} → [RightCancelMonoid H] → [Finite H] → Group H
-- Mathlib.Algebra.Order.CompleteField
/-- **Alias** of `ConditionallyCompleteLinearOrderedField.exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self`.

---

Preparatory lemma for `inducedOrderRingHom`.  -/
LinearOrderedField.exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self : ∀ {α : Type u_2} {β : Type u_3} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Field β]
  [inst_4 : ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] {a : α},
  0 < a →
    ∀
      b <
        ConditionallyCompleteLinearOrderedField.inducedMap α β a *
          ConditionallyCompleteLinearOrderedField.inducedMap α β a,
      ∃ c ∈ LinearOrderedField.cutMap β (a * a), b < c
-- Std.Http.Data.URI.Encoding
_private.Std.Http.Data.URI.Encoding.0.Std.Http.URI.EncodedString.mk : {r : UInt8 → Bool} →
  (toByteArray : ByteArray) → Std.Http.URI.IsAllowedEncodedChars r toByteArray → Std.Http.URI.EncodedString r
-- Init.Grind.Interactive
/-- `fail msg` is a tactic that always fails, and produces an error using the given message.  -/
Lean.Parser.Tactic.Grind.fail : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- If `i` is an isomorphism such that `l ≫ i.hom = f`, any kernel of `f` is a kernel of `l`.  -/
CategoryTheory.Limits.IsKernel.ofCompIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          {Z : C} →
            (l : X ⟶ Z) →
              (i : Z ≅ Y) →
                (h : CategoryTheory.CategoryStruct.comp l i.hom = f) →
                  {s : CategoryTheory.Limits.KernelFork f} →
                    CategoryTheory.Limits.IsLimit s →
                      CategoryTheory.Limits.IsLimit
                        (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.Fork.ι s) ⋯)
-- Mathlib.Data.Set.Semiring
SetSemiring.down_one : ∀ {α : Type u_1} [inst : One α], SetSemiring.down 1 = 1
-- Mathlib.Algebra.Homology.Additive
CategoryTheory.Functor.mapHomologicalComplexIdIso_inv_app_f : ∀ {ι : Type u_1} (W₁ : Type u_3) [inst : CategoryTheory.Category.{v_2, u_3} W₁]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms W₁] (c : ComplexShape ι) (X : HomologicalComplex W₁ c) (i : ι),
  ((CategoryTheory.Functor.mapHomologicalComplexIdIso W₁ c).inv.app X).f i = CategoryTheory.CategoryStruct.id (X.X i)
-- Mathlib.Analysis.Convex.Function
/-- A concave function on a segment is lower-bounded by the min of its endpoints.  -/
ConcaveOn.ge_on_segment : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  [PosSMulStrictMono 𝕜 β] {s : Set E} {f : E → β},
  ConcaveOn 𝕜 s f → ∀ {x y z : E}, x ∈ s → y ∈ s → z ∈ segment 𝕜 x y → min (f x) (f y) ≤ f z
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
PolynormableSpace.inf : ∀ {𝕜 : Type u_2} {E : Type u_6} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {t₁ t₂ : TopologicalSpace E}, PolynormableSpace 𝕜 E → PolynormableSpace 𝕜 E → PolynormableSpace 𝕜 E
-- Mathlib.RingTheory.PowerBasis
Module.Basis.PowerBasis_gen : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {ι : Type u_7}
  [inst_3 : Fintype ι] (B : Module.Basis ι R S) {x : S} (e : ι ≃ Fin (Fintype.card ι))
  (hx : ∀ (i : ι), B i = x ^ ↑(e i)), (B.PowerBasis e hx).gen = x
-- Mathlib.Data.ENNReal.Operations
ENNReal.add_lt_add_of_le_of_lt : ∀ {a b c d : ENNReal}, a ≠ ⊤ → a ≤ b → c < d → a + c < b + d
-- Mathlib.Algebra.CharZero.Defs
Nat.cast_eq_one : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharZero R] {n : ℕ}, ↑n = 1 ↔ n = 1
-- Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
InnerProductSpace.HarmonicContOnCl.add_const : ∀ {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 : E → F} {s : Set E},
  InnerProductSpace.HarmonicContOnCl f s → ∀ (c : F), InnerProductSpace.HarmonicContOnCl (f + fun x => c) s
-- Mathlib.Analysis.Convex.Segment
mem_openSegment_add_sub : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [Invertible 2] (x y : E), x ∈ openSegment 𝕜 (x + y) (x - y)
-- Mathlib.Data.Finsupp.SMul
/-- When `G` is a group, `Finsupp.comapSMul` acts by precomposition with the action of `g⁻¹`.
 -/
Finsupp.comapSMul_apply : ∀ {α : Type u_1} {M : Type u_3} {G : Type u_5} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : AddCommMonoid M]
  (g : G) (f : α →₀ M) (a : α), (g • f) a = f (g⁻¹ • a)
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.not_endPos_lt : ∀ {s : String.Slice} {p : s.Pos}, ¬s.endPos < p
-- Batteries.Recycling.MonadSatisfying.Array
_private.Batteries.Recycling.MonadSatisfying.Array.0.Array.forIn'.loop.match_3.eq_2 : ∀ {α : Type u_1} (as : Array α) (motive : (i : ℕ) → i ≤ as.size → Sort u_2) (i : ℕ) (h : i + 1 ≤ as.size)
  (h_1 : (x : 0 ≤ as.size) → motive 0 x) (h_2 : (i : ℕ) → (h : i + 1 ≤ as.size) → motive i.succ h),
  (match i.succ, h with
    | 0, x => h_1 x
    | i.succ, h => h_2 i h) =
    h_2 i h
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.iso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} (D : F.DescentData f) ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁)
  (f₂ : Y ⟶ X i₂)
  (_hf₁ :
    autoParam (CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q) CategoryTheory.Pseudofunctor.DescentData.iso._auto_1)
  (_hf₂ :
    autoParam (CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q) CategoryTheory.Pseudofunctor.DescentData.iso._auto_3),
  (D.iso q f₁ f₂ _hf₁ _hf₂).inv = D.hom q f₂ f₁ ⋯ ⋯
-- Init.Data.Repr
instReprAtomUInt16 : ReprAtom UInt16
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.addSubgroupOf_sup : ∀ {G : Type u_1} [inst : AddGroup G] {A A' B : AddSubgroup G},
  A ≤ B → A' ≤ B → (A ⊔ A').addSubgroupOf B = A.addSubgroupOf B ⊔ A'.addSubgroupOf B
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.sInf_toSubsemigroup : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (s : Set (NonUnitalSubsemiring R)),
  (sInf s).toSubsemigroup = ⨅ t ∈ s, t.toSubsemigroup
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instSMul.eq_1 : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} {G : Type u_6} [inst : SMul M G],
  Filter.Germ.instSMul = { smul := fun n f => Filter.Germ.map (fun x => n • x) f }
-- Mathlib.Data.ENNReal.Inv
/-- See `ENNReal.inv_mul_cancel_left` for a simpler version assuming `a ≠ 0`, `a ≠ ∞`.  -/
ENNReal.inv_mul_cancel_left' : ∀ {a b : ENNReal}, (a = 0 → b = 0) → (a = ⊤ → b = 0) → a⁻¹ * (a * b) = b
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_filterMap : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {γ : α → Type w} [inst_2 : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α} {fallback : γ k},
  (↑m).WF → (Std.DHashMap.Internal.Raw₀.filterMap f m).getD k fallback = ((m.get? k).bind (f k)).getD fallback
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiffOn.snd : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {f : E → F × G} {s : Set E},
  ContDiffOn 𝕜 n f s → ContDiffOn 𝕜 n (fun x => (f x).2) s
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The canonical equivalence between over and under categories by reversing structure arrows.  -/
CategoryTheory.Over.opEquivOpUnder : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    (X : T) → CategoryTheory.Over (Opposite.op X) ≌ (CategoryTheory.Under X)ᵒᵖ
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- If an intermediate field of `E / F` is both purely inseparable and separable, then it is equal
to `F`.  -/
IntermediateField.eq_bot_of_isPurelyInseparable_of_isSeparable : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (L : IntermediateField F E)
  [IsPurelyInseparable F ↥L] [Algebra.IsSeparable F ↥L], L = ⊥