mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsSubgraph.isLink_eqOn : ∀ {α : Type u_1} {β : Type u_2} {G H : Graph α β}, H ≤ G → Set.EqOn H.IsLink G.IsLink H.edgeSet
-- Mathlib.Algebra.Star.MonoidHom
/-- If a star monoid morphism has an inverse, it is an isomorphism of star monoids.  -/
StarMulEquiv.ofStarMonoidHom : {A : Type u_2} →
  {B : Type u_3} →
    [inst : Monoid A] →
      [inst_1 : Monoid B] →
        [inst_2 : Star A] →
          [inst_3 : Star B] →
            (f : A →⋆* B) → (g : B →⋆* A) → g.comp f = StarMonoidHom.id A → f.comp g = StarMonoidHom.id B → A ≃⋆* B
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.mk.injEq : ∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R) (monic_f : f.Monic) (g : Polynomial R)
  (cond : ∃ p₁ p₂ n, Polynomial.derivative f * p₁ + f * p₂ = g ^ n) (f_1 : Polynomial R) (monic_f_1 : f_1.Monic)
  (g_1 : Polynomial R) (cond_1 : ∃ p₁ p₂ n, Polynomial.derivative f_1 * p₁ + f_1 * p₂ = g_1 ^ n),
  ({ f := f, monic_f := monic_f, g := g, cond := cond } =
      { f := f_1, monic_f := monic_f_1, g := g_1, cond := cond_1 }) =
    (f = f_1 ∧ g = g_1)
-- Mathlib.RingTheory.ClassGroup.Basic
/-- The class number of a principal ideal domain is `1`.  -/
card_classGroup_eq_one : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R],
  Fintype.card (ClassGroup R) = 1
-- Mathlib.CategoryTheory.Yoneda
/-- Variant of the Coyoneda embedding which allows a raise in the universe level
for the category of types.  -/
CategoryTheory.uliftCoyoneda : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C (Type (max w v₁)))
-- Mathlib.Order.BooleanGenerators
IsCompactlyGenerated.BooleanGenerators.sSup_le_sSup_iff_of_atoms : ∀ {α : Type u_1} [inst : CompleteLattice α] {S : Set α} [IsCompactlyGenerated α],
  IsCompactlyGenerated.BooleanGenerators S → ∀ (X Y : Set α), X ⊆ S → Y ⊆ S → (sSup X ≤ sSup Y ↔ X ⊆ Y)
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- Equivalence between the homotopy group of X and the fundamental group of
`Ω^{j // j ≠ i} x`.  -/
homotopyGroupEquivFundamentalGroup : {N : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] →
      {x : X} →
        [DecidableEq N] → (i : N) → HomotopyGroup N X x ≃ FundamentalGroup (↑(GenLoop { j // j ≠ i } X x)) GenLoop.const
-- Mathlib.Analysis.Calculus.Deriv.Basic
differentiableWithinAt_Ioi_iff_Ici : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} [inst_3 : PartialOrder 𝕜],
  DifferentiableWithinAt 𝕜 f (Set.Ioi x) x ↔ DifferentiableWithinAt 𝕜 f (Set.Ici x) x
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.realize_bot : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {v : α → M}, ⊥.Realize v ↔ False
-- Mathlib.Data.Set.Lattice.Image
Set.biUnion_image2 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (s : Set α) (t : Set β) (f : α → β → γ) (g : γ → Set δ),
  ⋃ c ∈ Set.image2 f s t, g c = ⋃ a ∈ s, ⋃ b ∈ t, g (f a b)
-- Mathlib.Topology.UniformSpace.UniformConvergence
tendstoUniformly_congr : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι}
  {F' : ι → α → β}, F =ᶠ[p] F' → (TendstoUniformly F f p ↔ TendstoUniformly F' f p)
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
CategoryTheory.Limits.coneOfDiagramInitial_π_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {X : J} (tX : CategoryTheory.Limits.IsInitial X) (F : CategoryTheory.Functor J C) (j : J),
  (CategoryTheory.Limits.coneOfDiagramInitial tX F).π.app j = F.map (tX.to j)
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.val.injEq : ∀ (e e_1 : Lean.Expr), (Lean.Meta.Match.Pattern.val e = Lean.Meta.Match.Pattern.val e_1) = (e = e_1)
-- Mathlib.Analysis.Calculus.Deriv.Abs
HasStrictFDerivAt.abs_of_neg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E},
  HasStrictFDerivAt f f' x → f x < 0 → HasStrictFDerivAt (fun x => |f x|) (-f') x
-- Mathlib.Topology.Constructions
IsClosed.isClosedMap_inclusion : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsClosed s → ∀ (h : s ⊆ t), IsClosedMap (Set.inclusion h)
-- Mathlib.Topology.MetricSpace.Contracting
/-- Banach fixed-point theorem, contraction mapping theorem, `EMetricSpace` version.
A contracting map on a complete metric space has a fixed point.
We include more conclusions in this theorem to avoid proving them again later.

The main API for this theorem are the functions `efixedPoint` and `fixedPoint`,
and lemmas about these functions.  -/
ContractingWith.exists_fixedPoint : ∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α} [CompleteSpace α],
  ContractingWith K f →
    ∀ (x : α),
      edist x (f x) ≠ ⊤ →
        ∃ y,
          Function.IsFixedPt f y ∧
            Filter.Tendsto (fun n => f^[n] x) Filter.atTop (nhds y) ∧
              ∀ (n : ℕ), edist (f^[n] x) y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
AEMeasurable.csin : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℂ},
  AEMeasurable f μ → AEMeasurable (fun x => Complex.sin (f x)) μ
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.ofClass_carrier : ∀ {S : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : Star A] [inst_4 : SetLike S A] [inst_5 : NonUnitalSubsemiringClass S A]
  [inst_6 : SMulMemClass S R A] [inst_7 : StarMemClass S A] (s : S), ↑(NonUnitalStarSubalgebra.ofClass s) = ↑s
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.negY_smul : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R) (u : R),
  W'.negY (u • P) = u * W'.negY P
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.cancel_var_cert : ℤ → Lean.Grind.CommRing.Var → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Bool
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
SimpleGraph.top_le_span_range_lapMatrix_ker_basis_aux : ∀ {V : Type u_1} [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj] [inst_2 : DecidableEq V]
  [inst_3 : DecidableEq G.ConnectedComponent], ⊤ ≤ Submodule.span ℝ (Set.range G.lapMatrix_ker_basis_aux)
-- Mathlib.Data.List.ModifyLast
List.modifyLast.eq_1 : ∀ {α : Type u_1} (f : α → α) (l : List α), List.modifyLast f l = List.modifyLast.go f l #[]
-- Lean.Elab.InfoTree.Types
/-- Text to use to override the docstring. The string may be dynamic text. It is an `IO` action
so that it can be computed only when it is used. The action receives a `PPContext` so that the
action does not need to create a closure with the meta state.  -/
Lean.Elab.DelabTermInfo.mkDocString? : Lean.Elab.DelabTermInfo → Option (Lean.PPContext → IO String)
-- Mathlib.Data.Holor
Holor.CPRankMax1.brecOn : ∀ {α : Type} [inst : Mul α] {motive : {ds : List ℕ} → (a : Holor α ds) → a.CPRankMax1 → Prop} {ds : List ℕ}
  {a : Holor α ds} (t : a.CPRankMax1),
  (∀ {ds : List ℕ} (a : Holor α ds) (t : a.CPRankMax1), Holor.CPRankMax1.below t → motive a t) → motive a t
-- Mathlib.Data.Ordmap.Invariants
Ordnode.findMin'_dual : ∀ {α : Type u_1} (t : Ordnode α) (x : α), t.dual.findMin' x = Ordnode.findMax' x t
-- Mathlib.Algebra.GroupWithZero.Opposite
AddOpposite.instGroupWithZero : {α : Type u_1} → [GroupWithZero α] → GroupWithZero αᵃᵒᵖ
-- Init.Data.UInt.Basic
instSubUInt64 : Sub UInt64
-- Mathlib.Topology.Compactness.DeltaGeneratedSpace
/-- **Alias** of `Quotient.isGeneratedBy`. -/
Quotient.deltaGeneratedSpace : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y]
  [Topology.IsGeneratedBy X Y] {s : Setoid Y}, Topology.IsGeneratedBy X (Quotient s)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.coe_trans : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {V₃ : Type u_6} {P : Type u_10} {P₂ : Type u_11} {P₃ : Type u_12}
  [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] [inst_9 : SeminormedAddCommGroup V₃]
  [inst_10 : NormedSpace 𝕜 V₃] [inst_11 : PseudoMetricSpace P₃] [inst_12 : NormedAddTorsor V₃ P₃] (e₁ : P ≃ᵃⁱ[𝕜] P₂)
  (e₂ : P₂ ≃ᵃⁱ[𝕜] P₃), ⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
-- Mathlib.RepresentationTheory.Coinvariants
Rep.quotientToCoinvariantsFunctor_obj_V : ∀ (k : Type u) {G : Type v} [inst : CommRing k] [inst_1 : Group G] (S : Subgroup G) [inst_2 : S.Normal]
  (X : Rep.{w, u, v} k G),
  ↑((Rep.quotientToCoinvariantsFunctor k S).obj X) = Representation.Coinvariants (MonoidHom.comp X.ρ S.subtype)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_inverse_obj_a : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (adj : F ⊣ G)
  (V : CategoryTheory.Endofunctor.Coalgebra G),
  ((CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv adj).inverse.obj V).a = V.V
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.contains_iff : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x : α} [Std.TransCmp cmp] {t : RBTree.RBSet α cmp},
  t.contains x = true ↔ x ∈ t
-- Mathlib.Order.RelClasses
InvImage.asymm : ∀ {α : Type u} {β : Type v} {r : α → α → Prop} [Std.Asymm r] (f : β → α), Std.Asymm (InvImage r f)
-- Init.Data.Slice.Array.Lemmas
Subarray.forIn_eq_forIn_toList : ∀ {α : Type u} {s : Subarray α} {m : Type v → Type w} [inst : Monad m] [LawfulMonad m] {γ : Type v} {init : γ}
  {f : α → γ → m (ForInStep γ)}, forIn s init f = forIn (Std.Slice.toList s) init f
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] [inst_3 : SizeOf C] (X : C) [grp : CategoryTheory.GrpObj X]
  [comm : CategoryTheory.IsCommMonObj X],
  sizeOf { X := X, grp := grp, comm := comm } = 1 + sizeOf X + sizeOf grp + sizeOf comm
-- Mathlib.Algebra.Homology.ModelCategory.Injective
/-- The fibrations in the category `CochainComplex.Plus C` of bounded
below cochain complexes are the morphisms that are degreewise epi with
an injective kernel.  -/
CochainComplex.Plus.modelCategoryQuillen.instCategoryWithFibrations : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → HomotopicalAlgebra.CategoryWithFibrations (CochainComplex.Plus C)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The canonical map from the multiequalizer to the objects on the left.  -/
CategoryTheory.Limits.Multicoequalizer.π : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MultispanShape} →
      (I : CategoryTheory.Limits.MultispanIndex J C) →
        [inst_1 : CategoryTheory.Limits.HasMulticoequalizer I] →
          (b : J.R) → I.right b ⟶ CategoryTheory.Limits.multicoequalizer I
-- Mathlib.RingTheory.Kaehler.Basic
/-- Derivations into `Ω[S⁄R]` is equivalent to derivations
into `(KaehlerDifferential.ideal R S).cotangentIdeal`.  -/
KaehlerDifferential.endEquivDerivation' : (R : Type u) →
  (S : Type v) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          Derivation R S Ω[S⁄R] ≃ₗ[S] Derivation R S ↥(KaehlerDifferential.ideal R S).cotangentIdeal
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.formatBuilder.go : Std.Time.DateFormat → String → (format : Std.Time.FormatString) → Std.Time.FormatType String format
-- Mathlib.RingTheory.LocalRing.RingHom.Basic
/-- The image of the maximal ideal of the source is contained within the maximal ideal of the target.
 -/
map_nonunit : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : IsLocalRing R] [inst_2 : CommSemiring S]
  [inst_3 : IsLocalRing S] (f : R →+* S) [IsLocalHom f],
  ∀ a ∈ IsLocalRing.maximalIdeal R, f a ∈ IsLocalRing.maximalIdeal S
-- Std.Internal.Do.Triple.SpecLemmas
_private.Std.Internal.Do.Triple.SpecLemmas.0.Lean.Loop.forIn.match_1.splitter : {β : Type u_1} →
  (motive : ForInStep β → Sort u_2) →
    (__do_lift : ForInStep β) →
      ((b' : β) → motive (ForInStep.done b')) → ((b' : β) → motive (ForInStep.yield b')) → motive __do_lift
-- Std.Http.Data.Headers
/-- Removes a header with the given name.
 -/
Std.Http.Headers.erase : Std.Http.Headers → Std.Http.Header.Name → Std.Http.Headers
-- Std.Data.Iterators.Lemmas.Producers.Array
Array.toList_iter : ∀ {β : Type w} {array : Array β}, array.iter.toList = array.toList
-- Mathlib.Topology.Homotopy.Equiv
ContinuousMap.HomotopyEquiv.trans_apply : ∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (h₁ : ContinuousMap.HomotopyEquiv X Y) (h₂ : ContinuousMap.HomotopyEquiv Y Z) (a : X),
  (h₁.trans h₂).toFun a = h₂.toFun (h₁.toFun a)
-- Mathlib.Logic.Equiv.Basic
Equiv.piCongr'_symm_apply_symm_apply : ∀ {α : Sort u_1} {β : Sort u_4} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : (b : β) → W (h₁.symm b) ≃ Z b)
  (f : (b : β) → Z b) (b : β), (h₁.piCongr' h₂).symm f (h₁.symm b) = (h₂ b).symm (f b)
-- Mathlib.ModelTheory.Substructures
/-- Substructure closure of a set is monotone in its argument: if `s ⊆ t`,
then `closure L s ≤ closure L t`.  -/
FirstOrder.Language.Substructure.closure_mono : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] ⦃s t : Set M⦄,
  s ⊆ t → (FirstOrder.Language.Substructure.closure L).toFun s ≤ (FirstOrder.Language.Substructure.closure L).toFun t
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.BitVec.rotateRight_congr : ∀ (n w : ℕ) (x x' : BitVec w), x = x' → x'.rotateRight n = x.rotateRight n
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
/-- A convenience class, for a completely pseudometrizable space endowed with a complete
pseudometric. No instance of this class should be registered: It should be used as
`letI := upgradeIsCompletelyPseudoMetrizable X` to endow a completely pseudometrizable
space with a complete pseudometric.  -/
TopologicalSpace.UpgradedIsCompletelyPseudoMetrizableSpace : Type u_3 → Type u_3
-- Lean.Meta.WHNF
Lean.Meta.ReduceMatcherResult.stuck.inj : ∀ {val val_1 : Lean.Expr},
  Lean.Meta.ReduceMatcherResult.stuck val = Lean.Meta.ReduceMatcherResult.stuck val_1 → val = val_1
-- Mathlib.GroupTheory.ResiduallyFinite
AddGroup.residuallyFinite_iff_exists_finiteIndex : ∀ {G : Type u_1} [inst : AddGroup G], AddGroup.ResiduallyFinite G ↔ ∀ (g : G), g ≠ 0 → ∃ H, H.FiniteIndex ∧ g ∉ H
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_eq_some : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : LawfulBEq α] {k : α},
  k ∈ m → m.get? k = some k
-- Mathlib.Analysis.Analytic.Binomial
/-- `∑ (ai + b) zⁱ = (b - a) / (1 - z) + a / (1 - z)²`  -/
Complex.hasFPowerSeriesOnBall_ofScalars_mul_add_zero : ∀ (a b : ℂ),
  HasFPowerSeriesOnBall (fun x => (b - a) / (1 - x) + a / (1 - x) ^ 2)
    (FormalMultilinearSeries.ofScalars ℂ fun n => a * ↑n + b) 0 1
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.trans_iterate_Ico : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f : ℝ → ε} {μ : MeasureTheory.Measure ℝ}
  [TopologicalSpace.PseudoMetrizableSpace ε] {a : ℕ → ℝ} {m n : ℕ},
  m ≤ n → (∀ k ∈ Set.Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))) → IntervalIntegrable f μ (a m) (a n)
-- Mathlib.Algebra.Divisibility.Basic
/-- **Alias** of `dvd_mul_of_dvd_right`. -/
Dvd.dvd.mul_left : ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α}, a ∣ b → ∀ (c : α), a ∣ c * b
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.compr₂ₛₗ_comp : ∀ {R : Type u_2} [inst : CommSemiring R] {R₂ : Type u_14} {R₃ : Type u_15} {R₄ : Type u_16} {M : Type u_17}
  {N : Type u_18} {P : Type u_19} {Q : Type u_20} [inst_1 : CommSemiring R₂] [inst_2 : CommSemiring R₃]
  [inst_3 : CommSemiring R₄] [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P]
  [inst_7 : AddCommMonoid Q] [inst_8 : Module R M] [inst_9 : Module R₂ N] [inst_10 : Module R₃ P]
  [inst_11 : Module R₄ Q] {σ₁₃ : R →+* R₃} {σ₁₄ : R →+* R₄} {σ₂₃ : R₂ →+* R₃} {σ₂₄ : R₂ →+* R₄} {σ₃₄ : R₃ →+* R₄}
  [inst_12 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [inst_13 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] {Q' : Type u_21} {R₅ : Type u_22}
  [inst_14 : CommSemiring R₅] [inst_15 : AddCommMonoid Q'] [inst_16 : Module R₅ Q'] {σ₁₅ : R →+* R₅} {σ₂₅ : R₂ →+* R₅}
  {σ₃₅ : R₃ →+* R₅} {σ₄₅ : R₄ →+* R₅} [inst_17 : RingHomCompTriple σ₁₃ σ₃₅ σ₁₅]
  [inst_18 : RingHomCompTriple σ₁₄ σ₄₅ σ₁₅] [inst_19 : RingHomCompTriple σ₂₃ σ₃₅ σ₂₅]
  [inst_20 : RingHomCompTriple σ₂₄ σ₄₅ σ₂₅] [inst_21 : RingHomCompTriple σ₃₄ σ₄₅ σ₃₅] (f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P)
  (g : P →ₛₗ[σ₃₄] Q) (h : Q →ₛₗ[σ₄₅] Q'), f.compr₂ₛₗ (h ∘ₛₗ g) = (f.compr₂ₛₗ g).compr₂ₛₗ h
-- Std.Data.ByteSlice
/-- The ending index of the region of interest (exclusive).
 -/
Std.Slice.Internal.ByteSliceData.stop : Std.Slice.Internal.ByteSliceData → ℕ
-- Mathlib.RingTheory.MvPowerSeries.Equiv
MvPowerSeries.HasSubst.toMvPowerSeries : ∀ {σ : Type u_2} {R : Type u_4} [inst : CommRing R] {f : PowerSeries R},
  PowerSeries.constantCoeff f = 0 → MvPowerSeries.HasSubst fun x => (PowerSeries.toMvPowerSeries x) f
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
Mathlib.Tactic.Linarith.SimplexAlgorithm.Tableau.mk.inj : ∀ {matType : ℕ → ℕ → Type} {inst : Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType}
  {basic free : Array ℕ} {mat : matType basic.size free.size} {basic_1 free_1 : Array ℕ}
  {mat_1 : matType basic_1.size free_1.size},
  { basic := basic, free := free, mat := mat } = { basic := basic_1, free := free_1, mat := mat_1 } →
    basic = basic_1 ∧ free = free_1 ∧ mat ≍ mat_1
-- Mathlib.Topology.Separation.Profinite
/-- In a totally disconnected compact Hausdorff space `X`, if `Z ⊆ U` are subsets with `Z` closed
and `U` open, there exists a clopen `C` with `Z ⊆ C ⊆ U`.  -/
exists_clopen_of_closed_subset_open : ∀ {X : Type u_4} [inst : TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] {Z U : Set X},
  IsClosed Z → IsOpen U → Z ⊆ U → ∃ C, IsClopen C ∧ Z ⊆ C ∧ C ⊆ U
-- Mathlib.Topology.Sheaves.Sheaf
/-- A `TopCat.Sheaf C X` is a presheaf of objects from `C` over a (bundled) topological space `X`,
satisfying the sheaf condition.
 -/
TopCat.Sheaf : (C : Type u) → [CategoryTheory.Category.{v, u} C] → TopCat → Type (max u v w)
-- Mathlib.LinearAlgebra.Matrix.Swap
/-- Multiplying with `swap R i j` on the left swaps the `j`-th row with the `i`-th row.  -/
Matrix.swap_mul_apply_right : ∀ {R : Type u_1} {n : Type u_2} {m : Type u_3} [inst : Semiring R] [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  (i j : n) (a : m) (g : Matrix n m R), (Matrix.swap R i j * g) j a = g i a
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_diff_of_contains_eq_false_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k : α} {fallback : β},
        m₁.contains k = false → Std.DHashMap.Internal.Raw₀.Const.getD (m₁.diff m₂) k fallback = fallback
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbolAux.selectionRange : {Self : Type} → Lean.Lsp.DocumentSymbolAux Self → Lean.Lsp.Range
-- Mathlib.Order.WithBot
WithBot.coe_top : ∀ {α : Type u_1} [inst : Top α], ↑⊤ = ⊤
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.eval₂_eq_tsum : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : UniformSpace R] {S : Type u_3} [inst_2 : CommRing S]
  [inst_3 : UniformSpace S] {φ : R →+* S} {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R]
  [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S],
  Continuous ⇑φ →
    MvPowerSeries.HasEval a →
      ∀ (f : MvPowerSeries σ R),
        MvPowerSeries.eval₂ φ a f = ∑' (d : σ →₀ ℕ), φ ((MvPowerSeries.coeff d) f) * d.prod fun s e => a s ^ e
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubMulAction.notMem_val_image : ∀ (G : Type u_1) [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] {a : α}
  (t : Set ↥(SubMulAction.ofStabilizer G a)), a ∉ Subtype.val '' t
-- Mathlib.Topology.Algebra.Monoid.Defs
/-- Basic hypothesis to talk about a topological monoid or a topological semigroup.
A topological monoid over `M`, for example, is obtained by requiring both the instances `Monoid M`
and `ContinuousMul M`.

Continuity in each argument separately can be stated using `SeparatelyContinuousMul α`. If one wants
only continuity in either the left or right argument, but not both one can use
`ContinuousConstSMul α α`/`ContinuousConstSMul αᵐᵒᵖ α`.  -/
ContinuousMul : (M : Type u_1) → [TopologicalSpace M] → [Mul M] → Prop
-- Mathlib.Logic.Equiv.Basic
Equiv.Perm.extendDomain.eq_1 : ∀ {α' : Type u_9} {β' : Type u_10} (e : Equiv.Perm α') {p : β' → Prop} [inst : DecidablePred p] (f : α' ≃ Subtype p),
  e.extendDomain f = (f.permCongr e).subtypeCongr (Equiv.refl { a // ¬p a })
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
aemeasurable_coe_nnreal_ennreal_iff : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → NNReal} {μ : MeasureTheory.Measure α},
  AEMeasurable (fun x => ↑(f x)) μ ↔ AEMeasurable f μ
-- Mathlib.RingTheory.Ideal.Maps
/-- The `Ideal` version of `Set.preimage_subset_image_of_inverse`.  -/
Ideal.comap_le_map_of_inverse : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  {G : Type u_2} [inst_3 : FunLike G S R] [inst_4 : RingHomClass F R S] (g : G) (I : Ideal S),
  Function.LeftInverse ⇑g ⇑f → Ideal.comap f I ≤ Ideal.map g I
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightIso_counitIso_hom_app_right : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) (X : CategoryTheory.Comma L R₂),
  ((CategoryTheory.Comma.mapRightIso L i).counitIso.hom.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.LinearAlgebra.Span.Basic
/-- **Alias** of `Submodule.map_span`. -/
LinearMap.map_span : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂]
  [inst_6 : RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (s : Set M),
  Submodule.map f (Submodule.span R s) = Submodule.span R₂ (⇑f '' s)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
IsSMulRegular.skewMonoidAlgebra : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] {S : Type u_3} [inst_1 : Monoid S] [inst_2 : DistribMulAction S k]
  {a : S}, IsSMulRegular k a → IsSMulRegular (SkewMonoidAlgebra k G) a
-- Mathlib.Tactic.FunProp.Core
/-- Cache for failed goals such that `fun_prop` can fail fast next time.  -/
Mathlib.Meta.FunProp.cacheFailure : Lean.Expr → Mathlib.Meta.FunProp.FunPropM Unit
-- Mathlib.Algebra.Category.Ring.FilteredColimits
CommSemiRingCat.FilteredColimits.forget₂SemiRing_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ CommSemiRingCat SemiRingCat)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.extendComp.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cocone F) {X Y : C} (g : s.pt ⟶ Y) (f : Y ⟶ X),
  s.extendComp g f =
    CategoryTheory.Limits.Cocone.extInv (CategoryTheory.Iso.refl (s.extend (CategoryTheory.CategoryStruct.comp g f)).pt)
      ⋯