mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.LeftHomotopy.mk.injEq : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v : CategoryTheory.Arrow V} {f g : u ⟶ v} (hom : u.right ⟶ v.left)
  (comm :
    autoParam
      (CategoryTheory.Arrow.Hom.left f - CategoryTheory.Arrow.Hom.left g = CategoryTheory.CategoryStruct.comp u.hom hom)
      CategoryTheory.Arrow.LeftHomotopy.comm._autoParam)
  (hom_1 : u.right ⟶ v.left)
  (comm_1 :
    autoParam
      (CategoryTheory.Arrow.Hom.left f - CategoryTheory.Arrow.Hom.left g =
        CategoryTheory.CategoryStruct.comp u.hom hom_1)
      CategoryTheory.Arrow.LeftHomotopy.comm._autoParam),
  ({ hom := hom, comm := comm } = { hom := hom_1, comm := comm_1 }) = (hom = hom_1)
-- Mathlib.MeasureTheory.Category.MeasCat
/-- The Borel functor, the canonical embedding of topological spaces into measurable spaces.  -/
Borel : CategoryTheory.Functor TopCat MeasCat
-- Lean.DocString.Markdown
_private.Lean.DocString.Markdown.0.Lean.Doc.MarkdownM.State.footnotes : Lean.Doc.MarkdownM.State → Array (String × String)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.leibnizPullback_obj_obj : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) [inst_3 : CategoryTheory.Limits.HasPullbacks C₂]
  (f₁ : (CategoryTheory.Arrow C₁)ᵒᵖ) (f₃ : CategoryTheory.Arrow C₃),
  (G.leibnizPullback.obj f₁).obj f₃ =
    CategoryTheory.Arrow.mk (CategoryTheory.Functor.PullbackObjObj.ofHasPullback G (Opposite.unop f₁).hom f₃.hom).π
-- Mathlib.Topology.Defs.Induced
Topology.IsCoherentWith.isOpen_of_forall_induced : ∀ {X : Type u_1} [tX : TopologicalSpace X] {S : Set (Set X)},
  Topology.IsCoherentWith S → ∀ (u : Set X), (∀ s ∈ S, IsOpen (Subtype.val ⁻¹' u)) → IsOpen u
-- Std.Sync.CancellationContext
/-- Forks a child context from a parent. If the parent is already cancelled, returns the parent context.
Otherwise, creates a new child that will be cancelled when the parent is cancelled.
 -/
Std.CancellationContext.fork : Std.CancellationContext → BaseIO Std.CancellationContext
-- Mathlib.LinearAlgebra.Pi
LinearMap.sum_single_apply : ∀ {ι : Type x} (φ : ι → Type i) [inst : (i : ι) → AddCommMonoid (φ i)] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι]
  (v : (i : ι) → φ i), ∑ i, Pi.single i (v i) = v
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.limitsOfShape_le : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} (P : CategoryTheory.ObjectProperty C) (J : Type u')
  {inst_1 : CategoryTheory.Category.{v', u'} J} [self : P.IsClosedUnderLimitsOfShape J], P.limitsOfShape J ≤ P
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If `f` tends to infinity along a nontrivial filter,
`fun x ↦ f x / r` tends to negative infinity if and only if `r < 0`.  -/
Filter.tendsto_div_const_atBot_iff_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α} [l.NeBot],
  Filter.Tendsto f l Filter.atTop → (Filter.Tendsto (fun x => f x / r) l Filter.atBot ↔ r < 0)
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trStmts₁.match_1.eq_1 : ∀ (motive : Turing.PartrecToTM2.Λ' → Sort u_1) (p : Turing.PartrecToTM2.Γ' → Bool) (k₁ k₂ : Turing.PartrecToTM2.K')
  (q : Turing.PartrecToTM2.Λ')
  (h_1 :
    (Q : Turing.PartrecToTM2.Λ') →
      (p : Turing.PartrecToTM2.Γ' → Bool) →
        (k₁ k₂ : Turing.PartrecToTM2.K') →
          (q : Turing.PartrecToTM2.Λ') →
            Q = Turing.PartrecToTM2.Λ'.move p k₁ k₂ q → motive (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q))
  (h_2 :
    (Q : Turing.PartrecToTM2.Λ') →
      (k : Turing.PartrecToTM2.K') →
        (s : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') →
          (q : Turing.PartrecToTM2.Λ') →
            Q = Turing.PartrecToTM2.Λ'.push k s q → motive (Turing.PartrecToTM2.Λ'.push k s q))
  (h_3 :
    (Q : Turing.PartrecToTM2.Λ') →
      (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') →
        Q = Turing.PartrecToTM2.Λ'.read q → motive (Turing.PartrecToTM2.Λ'.read q))
  (h_4 :
    (Q : Turing.PartrecToTM2.Λ') →
      (p : Turing.PartrecToTM2.Γ' → Bool) →
        (k : Turing.PartrecToTM2.K') →
          (q : Turing.PartrecToTM2.Λ') →
            Q = Turing.PartrecToTM2.Λ'.clear p k q → motive (Turing.PartrecToTM2.Λ'.clear p k q))
  (h_5 : (Q q : Turing.PartrecToTM2.Λ') → Q = q.copy → motive q.copy)
  (h_6 : (Q q : Turing.PartrecToTM2.Λ') → Q = q.succ → motive q.succ)
  (h_7 : (Q q₁ q₂ : Turing.PartrecToTM2.Λ') → Q = q₁.pred q₂ → motive (q₁.pred q₂))
  (h_8 :
    (Q : Turing.PartrecToTM2.Λ') →
      (k : Turing.PartrecToTM2.Cont') → Q = Turing.PartrecToTM2.Λ'.ret k → motive (Turing.PartrecToTM2.Λ'.ret k)),
  (match Turing.PartrecToTM2.Λ'.move p k₁ k₂ q with
    | Q@h:(Turing.PartrecToTM2.Λ'.move p k₁ k₂ q) => h_1 Q p k₁ k₂ q h
    | Q@h:(Turing.PartrecToTM2.Λ'.push k s q) => h_2 Q k s q h
    | Q@h:(Turing.PartrecToTM2.Λ'.read q) => h_3 Q q h
    | Q@h:(Turing.PartrecToTM2.Λ'.clear p k q) => h_4 Q p k q h
    | Q@h:q.copy => h_5 Q q h
    | Q@h:q.succ => h_6 Q q h
    | Q@h:(q₁.pred q₂) => h_7 Q q₁ q₂ h
    | Q@h:(Turing.PartrecToTM2.Λ'.ret k) => h_8 Q k h) =
    h_1 (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q) p k₁ k₂ q ⋯
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.coe_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst_1 : Add α] [inst_2 : LE α] [inst_3 : Mul β] [inst_4 : Add β]
  [inst_5 : LE β] (e : α ≃+* β) (h : ∀ {a b : α}, e.toFun a ≤ e.toFun b ↔ a ≤ b),
  ⇑{ toRingEquiv := e, map_le_map_iff' := h } = ⇑e
-- Mathlib.Order.LiminfLimsup
Filter.blimsup_eq_iInf_biSup_of_nat : ∀ {α : Type u_1} [inst : CompleteLattice α] {p : ℕ → Prop} {u : ℕ → α},
  Filter.blimsup u Filter.atTop p = ⨅ i, ⨆ j, ⨆ (_ : p j ∧ i ≤ j), u j
-- Mathlib.Data.List.Sigma
_private.Mathlib.Data.List.Sigma.0.List.kunion.match_1.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : List (Sigma β) → List (Sigma β) → Sort u_3) (s : Sigma β)
  (l₁ : List (Sigma β)) (l₂ : List (Sigma β)) (h_1 : (l₂ : List (Sigma β)) → motive [] l₂)
  (h_2 : (s : Sigma β) → (l₁ : List (Sigma β)) → (l₂ : List (Sigma β)) → motive (s :: l₁) l₂),
  (match s :: l₁, l₂ with
    | [], l₂ => h_1 l₂
    | s :: l₁, l₂ => h_2 s l₁ l₂) =
    h_2 s l₁ l₂
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.toCommaMorphism_eq_hom : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} (f : X ⟶ Y),
  f.toCommaMorphism = CategoryTheory.MorphismProperty.Comma.Hom.hom f
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc_f : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq' pq'' : κ) (i₀' i₀ i₁ i₂ i₃ : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯)
  (hi₀ : i₀ = data.i₀ r pq' ⋯) (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯)
  (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq')
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc._auto_3),
  (CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc X data r r' hrr' hr pq' pq'' i₀' i₀ i₁ i₂ i₃
        hi₀' hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' hn₁ hn₂).f =
    CategoryTheory.CategoryStruct.comp (X.mapFourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃ ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ hn₁ ⋯)
      (CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁
          n₂ hn₁' hn₁ ⋯).inv
-- Init.Data.Nat.Lemmas
Nat.one_add : ∀ (n : ℕ), 1 + n = n.succ
-- Mathlib.Order.Copy
GeneralizedCoheytingAlgebra.copy.congr_simp : ∀ {α : Type u} (c c_1 : GeneralizedCoheytingAlgebra α) (e_c : c = c_1) (le le_1 : α → α → Prop) (e_le : le = le_1)
  (eq_le : le = LE.le) (bot bot_1 : α) (e_bot : bot = bot_1) (eq_bot : bot = ⊥) (sup sup_1 : α → α → α)
  (e_sup : sup = sup_1) (eq_sup : sup = max) (inf inf_1 : α → α → α) (e_inf : inf = inf_1) (eq_inf : inf = min)
  (sdiff sdiff_1 : α → α → α) (e_sdiff : sdiff = sdiff_1) (eq_sdiff : sdiff = SDiff.sdiff),
  c.copy le eq_le bot eq_bot sup eq_sup inf eq_inf sdiff eq_sdiff = c_1.copy le_1 ⋯ bot_1 ⋯ sup_1 ⋯ inf_1 ⋯ sdiff_1 ⋯
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.op_X₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C), S.op.X₂ = Opposite.op S.X₂
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_ne_zero : ∀ {x : ℝ}, Real.log x ≠ 0 ↔ x ≠ 0 ∧ x ≠ 1 ∧ x ≠ -1
-- Init.Data.BitVec.Lemmas
BitVec.lt_of_isSome_getElem? : ∀ {w : ℕ} (x : BitVec w) (i : ℕ), x[i]?.isSome = true → i < w
-- Mathlib.RingTheory.Valuation.Basic
/-- The type of `Γ₀`-valued valuations on `R`.

When you extend this structure, make sure to extend `ValuationClass`.  -/
Valuation : (R : Type u_3) → (Γ₀ : Type u_4) → [LinearOrderedCommMonoidWithZero Γ₀] → [Ring R] → Type (max u_3 u_4)
-- Mathlib.Topology.TietzeExtension
/-- Any retract of a `TietzeExtension` space is one itself.  -/
TietzeExtension.of_retract : ∀ {Y : Type v} {Z : Type w} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace Z] [TietzeExtension Z] (ι : C(Y, Z))
  (r : C(Z, Y)), r.comp ι = ContinuousMap.id Y → TietzeExtension Y
-- Mathlib.Analysis.Convex.Between
Function.Injective.sbtw_map_iff : ∀ {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [inst : Ring R] [inst_1 : PartialOrder R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup V']
  [inst_6 : Module R V'] [inst_7 : AddTorsor V' P'] {x y z : P} {f : P →ᵃ[R] P'},
  Function.Injective ⇑f → (Sbtw R (f x) (f y) (f z) ↔ Sbtw R x y z)
-- Init.Data.String.Lemmas.FindPos
String.offset_posLT_lt : ∀ {s : String} {p : String.Pos.Raw} {h : 0 < p}, (s.posLT p h).offset < p
-- Mathlib.Order.SuccPred.WithBot
/-- Not to be confused with `WithBot.orderSucc_bot`, which is about `Order.succ`.  -/
WithBot.succ_bot : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α] [inst_2 : SuccOrder α], ⊥.succ = ⊥
-- Lean.Parser.Basic
Lean.Parser.PrattParsingTables.leadingParsers : Lean.Parser.PrattParsingTables → List (Lean.Parser.Parser × ℕ)
-- Init.Data.String.Basic
/-- Returns the character at position `p` of a string. If `p` is not a valid position, returns `none`.

This function is overridden with an efficient implementation in runtime code. See
`String.utf8GetAux?` for the reference implementation.

This is a legacy function. The recommended alternative is `String.Pos.get`, combined with
`String.pos?` or another means of obtaining a `String.Pos`.

Examples:
* `"abc".get? ⟨1⟩ = some 'b'`
* `"abc".get? ⟨3⟩ = none`
* `"L∃∀N".get? ⟨1⟩ = some '∃'`
* `"L∃∀N".get? ⟨2⟩ = none`
 -/
String.Pos.Raw.get? : String → String.Pos.Raw → Option Char
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Iso.op_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (α : X ≅ Y), α.op.hom = α.hom.op
-- Mathlib.Data.Finset.Filter
Finset.subset_coe_filter_of_subset_forall : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s : Finset α) {t : Set α},
  t ⊆ ↑s → (∀ x ∈ t, p x) → t ⊆ ↑(Finset.filter p s)
-- Mathlib.Data.PFun
PFun.fix_fwd : ∀ {α : Type u_1} {β : Type u_2} {f : α →. β ⊕ α} {b : β} {a a' : α}, b ∈ f.fix a → Sum.inr a' ∈ f a → b ∈ f.fix a'
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallHSMul : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  CanLift (Set M) (Submodule R M) SetLike.coe fun s =>
    0 ∈ s ∧ (∀ {x y : M}, x ∈ s → y ∈ s → x + y ∈ s) ∧ ∀ (r : R) {x : M}, x ∈ s → r • x ∈ s
-- Mathlib.Algebra.Order.Field.Basic
inv_antitoneOn_Icc_right : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α},
  0 < a → AntitoneOn (fun x => x⁻¹) (Set.Icc a b)
-- Lean.Setup
Lean.ModuleArtifacts.c? : Lean.ModuleArtifacts → Option System.FilePath
-- Init.Data.BitVec.Lemmas
BitVec.append_assoc : ∀ {w₁ w₂ w₃ : ℕ} {x₁ : BitVec w₁} {x₂ : BitVec w₂} {x₃ : BitVec w₃}, x₁ ++ x₂ ++ x₃ = BitVec.cast ⋯ (x₁ ++ (x₂ ++ x₃))
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.PreservesFiniteCoproducts.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  (∀ (n : ℕ), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete (Fin n)) F) →
    CategoryTheory.Limits.PreservesFiniteCoproducts F
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisorAt.mod.eq_1 : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I)
  (f : PowerSeries A) [inst_1 : IsPrecomplete I A],
  H.mod f = (PowerSeries.trunc ((PowerSeries.map (Ideal.Quotient.mk I)) g).order.toNat) (f - g * H.div f)
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.le_hittingBtwn_of_exists : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] {u : ι → Ω → β} {s : Set β}
  {n : ι} {ω : Ω} {m : ι}, (∃ j ∈ Set.Icc n m, u j ω ∈ s) → n ≤ MeasureTheory.hittingBtwn u s n m ω
-- Init.Data.List.Nat.Range
List.erase_range : ∀ {n i : ℕ}, (List.range n).erase i = List.range (min n i) ++ List.range' (i + 1) (n - (i + 1))
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.id_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  (X : CategoryTheory.Grothendieck F),
  (CategoryTheory.CategoryStruct.id X).base = CategoryTheory.CategoryStruct.id X.base
-- Lean.ResolveName
Lean.instMonadResolveNameOfMonadLift : (m n : Type → Type) → [MonadLift m n] → [Lean.MonadResolveName m] → Lean.MonadResolveName n
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
/-- The Fourier integral of the derivative of a function is obtained by multiplying the Fourier
integral of the original function by `-L w v`.  -/
VectorFourier.fourierIntegral_fderiv : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} {W : Type u_3}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup W] [inst_5 : NormedSpace ℝ W]
  (L : V →L[ℝ] W →L[ℝ] ℝ) {f : V → E} [inst_6 : MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V]
  {μ : MeasureTheory.Measure V} [μ.IsAddHaarMeasure],
  MeasureTheory.Integrable f μ →
    Differentiable ℝ f →
      MeasureTheory.Integrable (fderiv ℝ f) μ →
        VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ L) (fderiv ℝ f) =
          VectorFourier.fourierSMulRight (-L.flip)
            (VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ L) f)
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.comap.eq_1 : ∀ {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.MonoidalLeftAction C D]
  {A B : C} [inst_4 : CategoryTheory.MonObj A] [inst_5 : CategoryTheory.MonObj B] (f : A ⟶ B)
  [inst_6 : CategoryTheory.IsMonHom f],
  CategoryTheory.Mod.comap f =
    { obj := fun M => { X := M.X, mod := CategoryTheory.Mod.scalarRestriction f M.X },
      map := fun {M N} g => { hom := g.hom, isModHom := ⋯ }, map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.sumAssoc_coe : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_5} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_9}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} {M' : Type u_13}
  [inst_6 : TopologicalSpace M'] [inst_7 : ChartedSpace H M'] {M'' : Type u_14} [inst_8 : TopologicalSpace M'']
  [inst_9 : ChartedSpace H M''], ⇑(Diffeomorph.sumAssoc I M n M' M'') = ⇑(Equiv.sumAssoc M M' M'')
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.normal_of_isMulCommutative : ∀ {G : Type u_1} [inst : Group G] [IsMulCommutative G] (H : Subgroup G), H.Normal
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
/-- When `K` is a cochain complex indexed by `ℤ` and `n < i`, this is
the isomorphism `(K.truncGE n).X i ≅ K.X i`.  -/
CochainComplex.truncGEXIso : {C : Type u_2} →
  [inst : CategoryTheory.Category.{u_3, u_2} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        (K : CochainComplex C ℤ) →
          [inst_3 : ∀ (i : ℤ), HomologicalComplex.HasHomology K i] →
            (n i : ℤ) → autoParam (n < i) CochainComplex.truncGEXIso._auto_1 → ((K.truncGE n).X i ≅ K.X i)
-- Mathlib.Analysis.Convex.Star
StarConvex.openSegment_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {x : E} {s : Set E}, StarConvex 𝕜 x s → ∀ {y : E}, y ∈ s → openSegment 𝕜 x y ⊆ s
-- Mathlib.AlgebraicTopology.ModelCategory.Homotopy
HomotopicalAlgebra.RightHomotopyRel.leftHomotopyRel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  {f g : X ⟶ Y} [HomotopicalAlgebra.IsFibrant Y],
  HomotopicalAlgebra.RightHomotopyRel f g → HomotopicalAlgebra.LeftHomotopyRel f g
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.Iterator.instIteratorLoop.match_1.splitter : {α : Type u_1} →
  [inst : Std.PRange.UpwardEnumerable α] →
    [inst_1 : LE α] →
      [inst_2 : DecidableLE α] →
        {n : Type u_1 → Type u_3} →
          (γ : Type u_1) →
            (Pl : α → γ → ForInStep γ → Prop) →
              (motive :
                  (it : Std.IterM Id α) →
                    ((b : α) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (Pl b c))) → Sort u_2) →
                (it : Std.IterM Id α) →
                  (f : (b : α) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (Pl b c))) →
                    ((next upperBound : α) →
                        (f :
                            (b : α) →
                              {
                                      internalState :=
                                        { next := some next, upperBound := upperBound } }.IsPlausibleIndirectOutput
                                  b →
                                (c : γ) → n (Subtype (Pl b c))) →
                          motive { internalState := { next := some next, upperBound := upperBound } } f) →
                      ((upperBound : α) →
                          (f :
                              (b : α) →
                                {
                                        internalState :=
                                          { next := none, upperBound := upperBound } }.IsPlausibleIndirectOutput
                                    b →
                                  (c : γ) → n (Subtype (Pl b c))) →
                            motive { internalState := { next := none, upperBound := upperBound } } f) →
                        motive it f
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.leadingCoeff_preΨ₄ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), 2 ≠ 0 → W.preΨ₄.leadingCoeff = 2
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.le_iff_nonempty_imp_le_and_iUnion_subset : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I},
  π₁ ≤ π₂ ↔ (∀ J ∈ π₁, ∀ J' ∈ π₂, (↑J ∩ ↑J').Nonempty → J ≤ J') ∧ π₁.iUnion ⊆ π₂.iUnion
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.Tendsto.pow : ∀ {α : Type u_1} {f : Filter α} {m : α → ENNReal} {a : ENNReal} {n : ℕ},
  Filter.Tendsto m f (nhds a) → Filter.Tendsto (fun x => m x ^ n) f (nhds (a ^ n))
-- Mathlib.LinearAlgebra.Dual.Lemmas
/-- Given a subspace `W` of `V` and an element of its dual `φ`, `dualLift W φ` is
an arbitrary extension of `φ` to an element of the dual of `V`.
That is, `dualLift W φ` sends `w ∈ W` to `φ x` and `x` in a chosen complement of `W` to `0`.  -/
Subspace.dualLift : {K : Type u_1} →
  {V : Type u_2} →
    [inst : Field K] →
      [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → (W : Subspace K V) → Module.Dual K ↥W →ₗ[K] Module.Dual K V
-- Mathlib.Topology.Neighborhoods
tendsto_atBot_of_eventually_const : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {ι : Type u_2} [inst_1 : Preorder ι] {u : ι → X} {i₀ : ι},
  (∀ i ≤ i₀, u i = x) → Filter.Tendsto u Filter.atBot (nhds x)
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
_private.Mathlib.RingTheory.Polynomial.UniversalFactorizationRing.0.Polynomial.term𝓡' : Lean.ParserDescr
-- Lean.Data.Lsp.Internal
/-- Named identifier. These are used in all references that are globally available.  -/
Lean.Lsp.RefIdent.const : String → String → Lean.Lsp.RefIdent
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.cospan_map_inr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z),
  (CategoryTheory.Limits.cospan f g).map CategoryTheory.Limits.WalkingCospan.Hom.inr = g
-- Mathlib.Algebra.Module.Submodule.Lattice
AddSubmonoid.coe_toNatSubmodule : ∀ {M : Type u_3} [inst : AddCommMonoid M] (S : AddSubmonoid M), ↑(AddSubmonoid.toNatSubmodule S) = ↑S
-- Mathlib.RingTheory.AdjoinRoot
/-- **Alias** of `AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapMk_symm_quotQuotMk`. -/
AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (f p : Polynomial R),
  (AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapMk I f).symm
      ((DoubleQuot.quotQuotMk (Ideal.map Polynomial.C I) (Ideal.span {f})) p) =
    (Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (Ideal.span {f})) (Ideal.map Polynomial.C I)))
      ((AdjoinRoot.mk f) p)
-- Mathlib.Computability.ContextFreeGrammar
/-- Type of nonterminals.  -/
ContextFreeGrammar.NT : {T : Type u_1} → ContextFreeGrammar T → Type
-- Std.Time.Format.Modifier
Std.Time.instReprModifier : Repr Std.Time.Modifier
-- Mathlib.Analysis.InnerProductSpace.Basic
real_inner_eq_re_inner : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E), inner ℝ x y = RCLike.re (inner 𝕜 x y)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_zero_measure : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  (f : α → G), ∫ (x : α), f x ∂0 = 0
-- Mathlib.Topology.Homotopy.Product
ContinuousMap.HomotopyRel.pi_apply : ∀ {I : Type u_1} {A : Type u_2} {X : I → Type u_3} [inst : (i : I) → TopologicalSpace (X i)]
  [inst_1 : TopologicalSpace A] {f g : (i : I) → C(A, X i)} {S : Set A}
  (homotopies : (i : I) → (f i).HomotopyRel (g i) S) (a : ↑unitInterval × A) (i : I),
  (ContinuousMap.HomotopyRel.pi homotopies) a i = (homotopies i) a
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
LeftPreLieRing.assoc_symm' : ∀ {L : Type u_1} [self : LeftPreLieRing L] (x y z : L), associator x y z = associator y x z