mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionEqualizerProducts.w_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) {F_1 : C → C → Type uF}
  {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F_1 X Y) (carrier X) (carrier Y)}
  [inst_2 : CategoryTheory.ConcreteCategory C F_1] (x : carrier (F.obj (Opposite.op (iSup U)))),
  (CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.SheafConditionEqualizerProducts.leftRes F U))
      ((CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.SheafConditionEqualizerProducts.res F U)) x) =
    (CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.SheafConditionEqualizerProducts.rightRes F U))
      ((CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.SheafConditionEqualizerProducts.res F U)) x)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.HorizontalComp.brecOn.go : {motive : Mathlib.Tactic.BicategoryLike.HorizontalComp → Sort u} →
  (t : Mathlib.Tactic.BicategoryLike.HorizontalComp) →
    ((t : Mathlib.Tactic.BicategoryLike.HorizontalComp) →
        Mathlib.Tactic.BicategoryLike.HorizontalComp.below t → motive t) →
      motive t ×' Mathlib.Tactic.BicategoryLike.HorizontalComp.below t
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.insertMany_empty_list_singleton : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {k : α} {v : β k},
  ↑(Std.DTreeMap.Internal.Impl.empty.insertMany [⟨k, v⟩] ⋯) =
    (Std.DTreeMap.Internal.Impl.insert k v Std.DTreeMap.Internal.Impl.empty ⋯).impl
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.maxD_le : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {k fallback : α}, (cmp (t.maxD fallback) k).isLE = true ↔ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.Topology.ClusterPt
/-- The set of cluster points of a filter is closed. In particular, the set of limit points
of a sequence is closed.  -/
isClosed_setOfPred_clusterPt : ∀ {X : Type u} [inst : TopologicalSpace X] {f : Filter X}, IsClosed {x | ClusterPt x f}
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionAssocIso_op : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (d : D) (c c' : C),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso (Opposite.op d) (Opposite.op c)
      (Opposite.op c') =
    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c c').symm.op
-- Init.Data.List.Basic
/-- Pads `l : List α` on the left with repeated occurrences of `a : α` until it is of length `n`. If `l`
already has at least `n` elements, it is returned unmodified.

Examples:
 * `[1, 2, 3].leftpad 5 0 = [0, 0, 1, 2, 3]`
 * `["red", "green", "blue"].leftpad 4 "blank" = ["blank", "red", "green", "blue"]`
 * `["red", "green", "blue"].leftpad 3 "blank" = ["red", "green", "blue"]`
 * `["red", "green", "blue"].leftpad 1 "blank" = ["red", "green", "blue"]`
 -/
List.leftpad : {α : Type u} → ℕ → α → List α → List α
-- Lean.Meta.Sym.Offset
/-- Variant of `isOffset?` that first checks if `declName` is `Nat.succ` or `HAdd.hAdd`.  -/
Lean.Meta.Sym.isOffset' : Lean.Name → Lean.Expr → Bool
-- Mathlib.Data.Nat.Log
Nat.log_eq_zero_iff : ∀ {b n : ℕ}, Nat.log b n = 0 ↔ n < b ∨ b ≤ 1
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Reachable.mem_subgraphVerts : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {H : G.Subgraph},
  G.Reachable u v → (∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w) → u ∈ H.verts → v ∈ H.verts
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.foldlM_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} {δ : Type w}
  {m : Type w → Type w'} [Std.TransOrd α] [inst : Monad m] [LawfulMonad m],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {f : δ → (a : α) → β a → m δ} {init : δ},
          Std.DTreeMap.Internal.Impl.foldlM f init t₁ = Std.DTreeMap.Internal.Impl.foldlM f init t₂
-- Lean.Meta.Tactic.Grind.Types
/-- Returns the next element in the equivalence class of `e`
if `e` has been internalized in the given goal.
 -/
Lean.Meta.Grind.Goal.getNext? : Lean.Meta.Grind.Goal → Lean.Expr → Option Lean.Expr
-- Mathlib.Topology.Algebra.Monoid
instSeparatelyContinuousAddAdditiveOfSeparatelyContinuousMul : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Mul M] [SeparatelyContinuousMul M],
  SeparatelyContinuousAdd (Additive M)
-- Mathlib.GroupTheory.Subgroup.Center
Group.commGroupOfCenterEqTop.eq_1 : ∀ {G : Type u_1} [inst : Group G] (h : Subgroup.center G = ⊤),
  Group.commGroupOfCenterEqTop h = { toGroup := inst, mul_comm := ⋯ }
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr : Type
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Complex.Gammaℝ_eq_zero_iff : ∀ {s : ℂ}, s.Gammaℝ = 0 ↔ ∃ n, s = -(2 * ↑n)
-- Mathlib.Topology.MetricSpace.Ultra.Basic
IsUltrametricDist.isClopen_closedBall : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] [IsUltrametricDist X] (x : X) {r : ℝ},
  r ≠ 0 → IsClopen (Metric.closedBall x r)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
div_le_div₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀]
  {a b c d : G₀}, 0 ≤ c → a ≤ c → 0 < d → d ≤ b → a / b ≤ c / d
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.below.add_comm : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  {motive : (a a_1 : RingCat.Colimits.Prequotient F) → RingCat.Colimits.Relation F a a_1 → Prop}
  (x y : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation.below ⋯
-- Mathlib.Data.Fintype.Basic
Fintype.univ_punit : Finset.univ = {PUnit.unit}
-- Mathlib.NumberTheory.AbelSummation
/-- A version of `sum_mul_eq_sub_integral_mul₀` where the endpoint is a `Nat`.  -/
sum_mul_eq_sub_integral_mul₀' : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (c : ℕ → 𝕜) {f : ℝ → 𝕜},
  c 0 = 0 →
    ∀ (m : ℕ),
      (∀ t ∈ Set.Icc 1 ↑m, DifferentiableAt ℝ f t) →
        MeasureTheory.IntegrableOn (deriv f) (Set.Icc 1 ↑m) MeasureTheory.volume →
          ∑ k ∈ Finset.Icc 0 m, f ↑k * c k =
            f ↑m * ∑ k ∈ Finset.Icc 0 m, c k - ∫ (t : ℝ) in Set.Ioc 1 ↑m, deriv f t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, c k
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.deriv_eq_id_of_nfp_eq_id : ∀ {f : Ordinal.{u} → Ordinal.{u}}, Ordinal.nfp f = id → Ordinal.deriv f = id
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.fold_filterMapWithPostcondition : ∀ {α β γ δ : Type w} {n : Type w → Type w''} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad n]
  [LawfulMonad n] [inst_4 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n]
  {f : β → Std.Iterators.PostconditionT n (Option γ)} {g : δ → γ → δ} {init : δ} {it : Std.Iter β},
  Std.IterM.fold g init (Std.Iter.filterMapWithPostcondition f it) =
    Std.Iter.foldM
      (fun d b => do
        let __x ← (f b).run
        match __x with
          | some c => pure (g d c)
          | x => pure d)
      init it
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.size_inter_le_size_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp], (t₁ ∩ t₂).size ≤ t₁.size
-- Mathlib.Algebra.CharP.Subring
CharP.subring : ∀ (R : Type u) [inst : Ring R] (p : ℕ) [CharP R p] (S : Subring R), CharP (↥S) p
-- Mathlib.Data.Ordmap.Invariants
Ordnode.size_balance' : ∀ {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α},
  l.Sized → r.Sized → (l.balance' x r).size = l.size + r.size + 1
-- Aesop.Frontend.Attribute
Aesop.Frontend.AttrConfig.mk.sizeOf_spec : ∀ (rules : Array Aesop.Frontend.RuleExpr), sizeOf { rules := rules } = 1 + sizeOf rules
-- Mathlib.Geometry.Convex.Cone.Face.Basic
/-- The image of a cone `F` under an injective linear map is a face of the
image of another cone `C` if and only if `F` is a face of `C`.  -/
PointedCone.isFaceOf_map_iff : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {C F : PointedCone R M} [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] {f : M →ₗ[R] N},
  Function.Injective ⇑f → ((PointedCone.map f F).IsFaceOf (PointedCone.map f C) ↔ F.IsFaceOf C)
-- Mathlib.AlgebraicGeometry.Geometrically.Basic
AlgebraicGeometry.pullback_of_geometrically : ∀ {P : CategoryTheory.ObjectProperty AlgebraicGeometry.Scheme} {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  AlgebraicGeometry.geometrically P f →
    ∀ (K : Type u) [inst : Field K] (y : AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ Y),
      P (CategoryTheory.Limits.pullback f y)
-- Mathlib.Topology.Maps.Strict.Basic
/-- Strict maps are preserved when postcomposing with a homeomorphism.  -/
Homeomorph.comp_isStrictMap_iff : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : Y ≃ₜ Z) {f : X → Y}, Topology.IsStrictMap (⇑e ∘ f) ↔ Topology.IsStrictMap f
-- Mathlib.Topology.Category.TopPair
TopPair.Homotopy.refl_fst : ∀ {X Y : TopPair} (f : X ⟶ Y), (TopPair.Homotopy.refl f).fst = TopCat.Homotopy.refl (TopPair.Hom.fst f)
-- Mathlib.Algebra.Order.Monoid.Units
AddUnits.instPartialOrderAddUnits : {α : Type u_1} → [inst : AddMonoid α] → [PartialOrder α] → PartialOrder (AddUnits α)
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.embed_comp_lift : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_4}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {I : Ideal A} (hI : DividedPowers I) {g : M →ₗ[R] A}
  (hg : ∀ (m : M), g m ∈ I), (DividedPowerAlgebra.lift hI g hg).toLinearMap ∘ₗ DividedPowerAlgebra.embed R M = g
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
/-- If `μ 1 ≤ 1` and `μ` is nonarchimedean, then `smoothingFun μ` is nonarchimedean.  -/
isNonarchimedean_smoothingFun : ∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R),
  μ 1 ≤ 1 → IsNonarchimedean ⇑μ → IsNonarchimedean (smoothingFun μ)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- If two vector measures give the same mass to the whole space and coincide on a
generating π-system, then they coincide.  -/
MeasureTheory.VectorMeasure.ext_of_generateFrom : ∀ {M : Type u_4} [inst : AddCommGroup M] [inst_1 : TopologicalSpace M] [T2Space M] {X : Type u_5}
  {mX : MeasurableSpace X} {μ ν : MeasureTheory.VectorMeasure X M} (C : Set (Set X)),
  (∀ s ∈ C, μ s = ν s) → mX = MeasurableSpace.generateFrom C → IsPiSystem C → μ Set.univ = ν Set.univ → μ = ν
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.Hom.mk' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] →
      {X Y : CategoryTheory.CatEnrichedOrdinary C} →
        {f g : X ⟶ Y} →
          (CategoryTheory.CatEnrichedOrdinary.homEquiv f ⟶ CategoryTheory.CatEnrichedOrdinary.homEquiv g) →
            CategoryTheory.CatEnrichedOrdinary.Hom f g
-- Init.Grind.Util
Lean.Grind.nestedProof_congr : ∀ (p q : Prop), p = q → ∀ (hp : p) (hq : q), ⋯ ≍ ⋯
-- Mathlib.Algebra.Group.Subsemigroup.Membership
Subsemigroup.mem_sSup_of_directed_on : ∀ {M : Type u_2} [inst : Mul M] {S : Set (Subsemigroup M)},
  DirectedOn (fun x1 x2 => x1 ≤ x2) S → ∀ {x : M}, x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_Ici_eq_integral_Ioi' : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} [inst_2 : PartialOrder X] {x : X},
  μ {x} = 0 → ∫ (t : X) in Set.Ici x, f t ∂μ = ∫ (t : X) in Set.Ioi x, f t ∂μ
-- Mathlib.GroupTheory.OrderOfElement
card_nsmul_eq_zero : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Fintype G] {x : G}, Fintype.card G • x = 0
-- Mathlib.Order.Types.Defs
OrderType.type_eq_zero : ∀ {α : Type u} [inst : LinearOrder α], OrderType.type α = 0 ↔ IsEmpty α
-- Init.Data.Nat.Div.Lemmas
Nat.lt_of_div_eq_zero : ∀ {k x : ℕ}, 0 < k → x / k = 0 → x < k
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.congr_refl : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀),
  WithVal.congr v v (RingEquiv.refl R) = RingEquiv.refl (WithVal v)
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.colimitsOfShape_congr : ∀ {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] {J' : Type u''} [inst_2 : CategoryTheory.Category.{v'', u''} J']
  (e : J ≌ J'), P.colimitsOfShape J = P.colimitsOfShape J'
-- Lean.Meta.Sym.Arith.Poly
Lean.Grind.CommRing.Poly.length : Lean.Grind.CommRing.Poly → ℕ
-- Lean.Meta.KAbstract
_private.Lean.Meta.KAbstract.0.Lean.Meta.kabstract.visit : Lean.Expr → Lean.Meta.Occurrences → Lean.HeadIndex → ℕ → Lean.Expr → ℕ → StateRefT' IO.RealWorld ℕ Lean.MetaM Lean.Expr
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.toComplex_im_div : ∀ (x y : GaussianInt),
  (GaussianInt.toComplex (x / y)).im = ↑(round (GaussianInt.toComplex x / GaussianInt.toComplex y).im)
-- Aesop.RuleSet.Filter
Aesop.RuleFilter.mk.sizeOf_spec : ∀ (name : Lean.Name) (scope : Aesop.ScopeName) (builders : Array Aesop.BuilderName) (phases : Array Aesop.PhaseName),
  sizeOf { name := name, scope := scope, builders := builders, phases := phases } =
    1 + sizeOf name + sizeOf scope + sizeOf builders + sizeOf phases
-- Mathlib.Topology.Connected.Basic
mem_connectedComponentIn : ∀ {α : Type u} [inst : TopologicalSpace α] {x : α} {F : Set α}, x ∈ F → x ∈ connectedComponentIn F x
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_fun_smul_iff : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {𝕜 : Type u_8} [inst_1 : NormedDivisionRing 𝕜] [inst_2 : MulActionWithZero 𝕜 β] [IsBoundedSMul 𝕜 β] {c : 𝕜},
  c ≠ 0 → ∀ (f : α → β), MeasureTheory.Integrable (fun x => c • f x) μ ↔ MeasureTheory.Integrable f μ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- **Alias** of `CategoryTheory.Limits.pushout.desc'`.

---

A pair of morphisms `h : Y ⟶ W` and `k : Z ⟶ W` satisfying `f ≫ h = g ≫ k` induces a morphism
`l : pushout f g ⟶ W` such that `pushout.inl _ _ ≫ l = h` and `pushout.inr _ _ ≫ l = k`.  -/
CategoryTheory.Limits.pullback.desc' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} →
      {f : X ⟶ Y} →
        {g : X ⟶ Z} →
          [inst_1 : CategoryTheory.Limits.HasPushout f g] →
            (h : Y ⟶ W) →
              (k : Z ⟶ W) →
                CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k →
                  { l //
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g) l = h ∧
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g) l = k }
-- Mathlib.Analysis.Normed.Ring.Basic
SeminormedRing.toRing : {α : Type u_5} → [self : SeminormedRing α] → Ring α
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.symm_addMonoidHomCongrRightEquiv : ∀ {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [inst : AddZeroClass M] [inst_1 : AddMonoid N₁]
  [inst_2 : AddMonoid N₂] (e : N₁ ≃+ N₂), e.addMonoidHomCongrRightEquiv.symm = e.symm.addMonoidHomCongrRightEquiv
-- Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
abs_integral_sub_setIntegral_mulExpNegMulSq_comp_lt : ∀ {E : Type u_1} [inst : TopologicalSpace E] [inst_1 : MeasurableSpace E] [BorelSpace E] {P : MeasureTheory.Measure E}
  [MeasureTheory.IsFiniteMeasure P] {ε : ℝ} (f : C(E, ℝ)) {K : Set E},
  MeasurableSet K →
    0 < ε → P Kᶜ < ↑ε.toNNReal → |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P| < √ε
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.minKeyD_modifyKey_eq_minKeyD : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] [Std.LawfulEqOrd α]
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : β → β} {fallback : α},
      Std.Internal.List.minKeyD (Std.Internal.List.Const.modifyKey k f l) fallback =
        Std.Internal.List.minKeyD l fallback
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.assoc_comp_map_comm_comp_comul_comp_comul_assoc : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {Q : Type u_9} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : AddCommMonoid Q]
  [inst_6 : Module R Q] [inst_7 : Coalgebra R M] (f : M →ₗ[R] N) (h : Q →ₗ[R] M),
  ↑(TensorProduct.assoc R M M N) ∘ₗ
      TensorProduct.map (↑(TensorProduct.comm R M M) ∘ₗ CoalgebraStruct.comul) f ∘ₗ CoalgebraStruct.comul ∘ₗ h =
    TensorProduct.map LinearMap.id (TensorProduct.map LinearMap.id f ∘ₗ ↑(TensorProduct.comm R M M)) ∘ₗ
      ↑(TensorProduct.assoc R M M M) ∘ₗ
        TensorProduct.map CoalgebraStruct.comul LinearMap.id ∘ₗ
          ↑(TensorProduct.comm R M M) ∘ₗ CoalgebraStruct.comul ∘ₗ h
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Prod.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.CategoryStruct.{v₁, u₁} C] {D : Type u₂}
  [inst_1 : CategoryTheory.CategoryStruct.{v₂, u₂} D] {X Y : C × D} {f g : X ⟶ Y}, f.1 = g.1 → f.2 = g.2 → f = g
-- Mathlib.Data.Finsupp.Defs
Finsupp.ne_iff : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] {f g : α →₀ M}, f ≠ g ↔ ∃ a, f a ≠ g a
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.neg_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Neg β]
  [inst_3 : ContinuousNeg β] (f : C(α, β)) (x : α), (-f) x = -f x
-- Mathlib.FieldTheory.Finite.GaloisField
galois_poly_separable : ∀ {K : Type u_1} [inst : CommRing K] (p q : ℕ) [CharP K p], p ∣ q → (Polynomial.X ^ q - Polynomial.X).Separable
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- A variant of `app_inv_app` that gives an `eqToHom` instead of `homOfLe`.  -/
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace)
  (hU : ↑U ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.hom.base)),
  CategoryTheory.CategoryStruct.comp (f.hom.c.app (Opposite.op U))
      (AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp f ((TopologicalSpace.Opens.map f.hom.base).obj U)) =
    Y.presheaf.map (CategoryTheory.eqToHom ⋯).op
-- Mathlib.RingTheory.Localization.Module
/-- An `R`-linear isomorphism between `S⁻¹R`-modules is actually `S⁻¹R`-linear.  -/
LinearEquiv.extendScalarsOfIsLocalization : {R : Type u_3} →
  [inst : CommSemiring R] →
    (S : Submonoid R) →
      (A : Type u_4) →
        [inst_1 : CommSemiring A] →
          [inst_2 : Algebra R A] →
            [IsLocalization S A] →
              {M : Type u_5} →
                {N : Type u_6} →
                  [inst_4 : AddCommMonoid M] →
                    [inst_5 : Module R M] →
                      [inst_6 : Module A M] →
                        [IsScalarTower R A M] →
                          [inst_8 : AddCommMonoid N] →
                            [inst_9 : Module R N] →
                              [inst_10 : Module A N] → [IsScalarTower R A N] → (M ≃ₗ[R] N) → M ≃ₗ[A] N
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
Complex.radius_regularizedGaussHGFunSeries_eq_top_of_right : ∀ (a c : ℂ) (k : ℕ), (a.regularizedGaussHGFunSeries (-↑k) c).radius = ⊤
-- Mathlib.Data.Prod.Lex
Prod.Lex.instOrdLexProd : {α : Type u_1} → {β : Type u_2} → [Ord α] → [Ord β] → Ord (Lex (α × β))
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Cotangent.val_of : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  (w : P.ker.Cotangent), (Algebra.Extension.Cotangent.of w).val = w
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.isoLimit_hom_π : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
  [inst_1 : CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] [inst_2 : CategoryTheory.Limits.HasLimit X]
  (j : α),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.isoLimit X).hom
      (CategoryTheory.Limits.limit.π X { as := j }) =
    CategoryTheory.Limits.Pi.π (fun j => X.obj { as := j }) j
-- Mathlib.Data.Finset.Functor
Finset.seqRight_def : ∀ {α β : Type u} [inst : (P : Prop) → Decidable P] (s : Finset α) (t : Finset β), s *> t = if s = ∅ then ∅ else t
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_uLift : ∀ (α : Type u), Cardinal.mk (ULift.{v, u} α) = Cardinal.lift.{v, u} (Cardinal.mk α)
-- Mathlib.Topology.Sober
/-- The irreducible component of a generic point  -/
genericPoints.component : {α : Type u_1} → [inst : TopologicalSpace α] → ↑(genericPoints α) → ↑(irreducibleComponents α)
-- Mathlib.FieldTheory.LinearDisjoint
IntermediateField.LinearDisjoint.rank_right_mul_adjoin_rank_eq_of_isAlgebraic_left : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E}
  {L : Type v} [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E],
  A.LinearDisjoint L →
    ∀ [Algebra.IsAlgebraic F ↥A],
      Module.rank F L * Module.rank (↥(IntermediateField.adjoin L ↑A)) E = Module.rank (↥A) E
-- Mathlib.FieldTheory.RatFunc.Defs
RatFunc.liftOn'_mk : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {P : Sort v} (p q : Polynomial K)
  (f : Polynomial K → Polynomial K → P),
  (∀ (p : Polynomial K), f p 0 = f 0 1) →
    ∀ (H : ∀ {p q a : Polynomial K}, q ≠ 0 → a ≠ 0 → f (a * p) (a * q) = f p q), (RatFunc.mk p q).liftOn' f H = f p q
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupNorm.funLike : {E : Type u_3} → [inst : Group E] → FunLike (GroupNorm E) E ℝ
-- Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
/-- The functor `CommGrpCat ⥤ AddCommGrpCat` by sending `X ↦ Additive X` and `f ↦ f`.
 -/
CommGrpCat.toAddCommGrp : CategoryTheory.Functor CommGrpCat AddCommGrpCat
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_map_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited γ] {f : α → β → γ} {k k' : α},
  m.getKey? k = some k' → (Std.ExtHashMap.map f m)[k]! = (Option.map (f k') m[k]?).get!
-- Mathlib.Analysis.RCLike.Basic
/-- The ℝ → K coercion, as a linear isometry  -/
RCLike.ofRealLI : {K : Type u_1} → [inst : RCLike K] → ℝ →ₗᵢ[ℝ] K
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.Gal.restrictComp.eq_1 : ∀ {F : Type u_1} [inst : Field F] (p q : Polynomial F) (hq : q.natDegree ≠ 0),
  Polynomial.Gal.restrictComp p q hq = Polynomial.Gal.restrict p (p.comp q).SplittingField
-- Std.Sat.AIG.Basic
Std.Sat.AIG.RefVec.mk : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {w : ℕ} →
          (refs : Vector Std.Sat.AIG.Fanin w) → (∀ {i : ℕ} (h : i < w), refs[i].gate < aig.decls.size) → aig.RefVec w
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.trivial_covering : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {S : CategoryTheory.Sieve X},
  S ∈ (CategoryTheory.GrothendieckTopology.trivial C) X ↔ S = ⊤
-- Mathlib.NumberTheory.ModularForms.BoundedAtCusp
OnePoint.IsBoundedAt.eq_1 : ∀ (c : OnePoint ℝ) (f : UpperHalfPlane → ℂ) (k : ℤ),
  c.IsBoundedAt f k =
    ∀ (g : GL (Fin 2) ℝ), g • OnePoint.infty = c → UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map k g f)