mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.SimpleModule.Isotypic
/-- The endomorphism ring of a semisimple module is the direct product of the endomorphism rings
of its isotypic components.  -/
IsSemisimpleModule.endRingEquiv : (R : Type u_2) →
  (M : Type u) →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          [IsSemisimpleModule R M] →
            [DecidableEq ↑(isotypicComponents R M)] →
              Module.End R M ≃+* ((c : ↑(isotypicComponents R M)) → Module.End R ↥↑c)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Adj.support_toWalk : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v), h.toWalk.support = [u, v]
-- Lean.Meta.Tactic.Grind.Intro
_private.Lean.Meta.Tactic.Grind.Intro.0.Lean.Meta.Grind.IntroResult.newHyp.sizeOf_spec : ∀ (fvarId : Lean.FVarId) (goal : Lean.Meta.Grind.Goal),
  sizeOf (Lean.Meta.Grind.IntroResult.newHyp✝ fvarId goal) = 1 + sizeOf fvarId + sizeOf goal
-- Mathlib.GroupTheory.GroupAction.Period
/-- If the action is periodic, then a lower bound for its period can be computed.  -/
MulAction.le_period : ∀ {α : Type v} {M : Type u} [inst : Monoid M] [inst_1 : MulAction M α] {m : M} {a : α} {n : ℕ},
  0 < MulAction.period m a → (∀ (k : ℕ), 0 < k → k < n → m ^ k • a ≠ a) → n ≤ MulAction.period m a
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- If `X : T` is initial, then the under category of `X` is equivalent to `T`.  -/
CategoryTheory.Under.equivalenceOfIsInitial : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {X : T} → CategoryTheory.Limits.IsInitial X → (CategoryTheory.Under X ≌ T)
-- Mathlib.Topology.Sequences
IsCompact.tendsto_subseq' : ∀ {X : Type u_1} [inst : TopologicalSpace X] [FirstCountableTopology X] {s : Set X} {x : ℕ → X},
  IsCompact s →
    (∃ᶠ (n : ℕ) in Filter.atTop, x n ∈ s) → ∃ a ∈ s, ∃ φ, StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (nhds a)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
/-- A version of **Markov's inequality** with elements of Lp.  -/
MeasureTheory.Lp.pow_mul_meas_ge_le_enorm : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f : ↥(MeasureTheory.Lp E p μ)),
  p ≠ 0 → p ≠ ⊤ → ∀ (ε : ENNReal), (ε * μ {x | ε ≤ ‖↑↑f x‖ₑ ^ p.toReal}) ^ (1 / p.toReal) ≤ ENNReal.ofReal ‖f‖
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.IsG2.exists_pairingIn_neg_three : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} {inst : CommRing R} {inst_1 : AddCommGroup M}
  {inst_2 : Module R M} {inst_3 : AddCommGroup N} {inst_4 : Module R N} {P : RootPairing ι R M N} [self : P.IsG2],
  ∃ i j, P.pairingIn ℤ i j = -3
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_left_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] {G : CategoryTheory.Functor C D} [inst_3 : G.IsCoverDense K]
  [inst_4 : G.IsLocallyFull K] {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A}
  {𝒢 : CategoryTheory.Functor Dᵒᵖ A} (f : 𝒢 ⟶ ℱ) (g : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) {Z : CategoryTheory.Functor Dᵒᵖ A}
  (h : ℱ'.obj ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom
        (CategoryTheory.CategoryStruct.comp (G.op.whiskerLeft f) g))
      h =
    CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom g) h)
-- Mathlib.Analysis.Seminorm
Seminorm.sub_mem_closedBall : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E]
  (p : Seminorm 𝕜 E) (x₁ x₂ y : E) (r : ℝ), x₁ - x₂ ∈ p.closedBall y r ↔ x₁ ∈ p.closedBall (x₂ + y) r
-- Mathlib.CategoryTheory.Limits.Creates
/-- The lifted cocone is a colimit.  -/
CategoryTheory.liftedColimitIsColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                [inst_3 : CategoryTheory.CreatesColimit K F] →
                  {c : CategoryTheory.Limits.Cocone (K.comp F)} →
                    (t : CategoryTheory.Limits.IsColimit c) →
                      CategoryTheory.Limits.IsColimit (CategoryTheory.liftColimit t)
-- Mathlib.RingTheory.Congruence.BigOperators
/-- Congruence relation of a ring preserves finite sum indexed by a multiset.  -/
RingCon.multisetSum : ∀ {ι : Type u_1} {S : Type u_2} [inst : AddCommMonoid S] [inst_1 : Mul S] (t : RingCon S) (s : Multiset ι)
  {f g : ι → S}, (∀ i ∈ s, t (f i) (g i)) → t (Multiset.map f s).sum (Multiset.map g s).sum
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
/-- The canonical map from the subalgebra generated by an algebraic independent family
into the polynomial ring.  -/
AlgebraicIndependent.repr : {ι : Type u_1} →
  {R : Type u_3} →
    {A : Type u_5} →
      {x : ι → A} →
        [inst : CommRing R] →
          [inst_1 : CommRing A] →
            [inst_2 : Algebra R A] → AlgebraicIndependent R x → ↥(Algebra.adjoin R (Set.range x)) →ₐ[R] MvPolynomial ι R
-- Init.Data.Int.DivMod.Lemmas
_private.Init.Data.Int.DivMod.Lemmas.0.Int.fdiv.match_1.eq_1 : ∀ (motive : ℤ → ℤ → Sort u_1) (x : ℤ) (h_1 : (x : ℤ) → motive 0 x)
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n)) (h_3 : (m n : ℕ) → motive (Int.ofNat m.succ) (Int.negSucc n))
  (h_4 : (a : ℕ) → motive (Int.negSucc a) 0) (h_5 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n.succ))
  (h_6 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match 0, x with
    | 0, x => h_1 x
    | Int.ofNat m, Int.ofNat n => h_2 m n
    | Int.ofNat m.succ, Int.negSucc n => h_3 m n
    | Int.negSucc a, 0 => h_4 a
    | Int.negSucc m, Int.ofNat n.succ => h_5 m n
    | Int.negSucc m, Int.negSucc n => h_6 m n) =
    h_1 x
-- Init.Prelude
/-- The homogeneous version of `HAppend`: `a ++ b : α` where `a b : α`.  -/
Append : Type u → Type u
-- Std.Data.DHashMap.Internal.AssocList.Iterator
/-- Internal implementation detail of the hash map. Returns a finite iterator on an associative list.
 -/
Std.DHashMap.Internal.AssocList.iter : {α : Type u} → {β : α → Type v} → Std.DHashMap.Internal.AssocList α β → Std.Iter ((a : α) × β a)
-- Mathlib.RingTheory.Ideal.IsPrincipal
Ideal.associatesEquivIsPrincipal_symm_apply : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {I : Ideal R} (hI : Submodule.IsPrincipal I),
  (Ideal.associatesEquivIsPrincipal R).symm ⟨I, hI⟩ = Associates.mk (Submodule.IsPrincipal.generator I)
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.map_zero : ∀ {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] (f : α →*₀ β), f 0 = 0
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleConfig : Type
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- **Alias** of `MonoidAlgebra.coeff_mapAddEquiv`. -/
MonoidAlgebra.mapAddEquiv_apply : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Mul M] (e : R ≃+ S)
  (x : MonoidAlgebra R M) (m : M), ((MonoidAlgebra.mapAddEquiv M e) x).coeff m = e (x.coeff m)
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.rotCompInvRot_inv_app_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  (CategoryTheory.Pretriangulated.rotCompInvRot.inv.app X).hom₃ = CategoryTheory.CategoryStruct.id X.obj₃
-- Init.Data.Array.Lemmas
Array.back?_push : ∀ {α : Type u_1} {xs : Array α} {x : α}, (xs.push x).back? = some x
-- Init.Data.Int.Pow
Int.natAbs_pow : ∀ (n : ℤ) (k : ℕ), (n ^ k).natAbs = n.natAbs ^ k
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.codExtend_baseSet : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace Z] {s : Set B} (hs : IsOpen s) (nonempty : s.Nonempty) {proj : Z → ↑s}
  (e : Bundle.Trivialization F proj),
  (Bundle.Trivialization.codExtend hs nonempty e).baseSet = Subtype.val '' e.toPretrivialization.baseSet
-- Mathlib.Data.Quot
/-- A version of `Quotient.ind` taking `{s : Setoid α}` as an implicit argument instead of an
instance argument.  -/
Quotient.ind' : ∀ {α : Sort u_1} {s₁ : Setoid α} {p : Quotient s₁ → Prop}, (∀ (a : α), p (Quotient.mk'' a)) → ∀ (q : Quotient s₁), p q
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.NatTrans.isIso_app_iff_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {F G : CategoryTheory.Functor C D} (α : F ⟶ G) {X Y : C} (e : X ≅ Y),
  CategoryTheory.IsIso (α.app X) ↔ CategoryTheory.IsIso (α.app Y)
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- If `f` is multilinear, then `f (Σ_{j₁ ∈ A₁} g₁ j₁, ..., Σ_{jₙ ∈ Aₙ} gₙ jₙ)` is the sum of
`f (g₁ (r 1), ..., gₙ (r n))` where `r` ranges over all functions with `r 1 ∈ A₁`, ...,
`r n ∈ Aₙ`. This follows from multilinearity by expanding successively with respect to each
coordinate.  -/
MultilinearMap.map_sum_finset : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) {α : ι → Type u_1} (g : (i : ι) → α i → M₁ i)
  (A : (i : ι) → Finset (α i)) [inst_5 : DecidableEq ι] [inst_6 : Fintype ι],
  (f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ Fintype.piFinset A, f fun i => g i (r i)
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.δ_comp_σ_self' : ∀ {n : ℕ} {j : Fin (n + 2)} {i : Fin (n + 1)},
  j = i.castSucc →
    CategoryTheory.CategoryStruct.comp (SimplexCategory.δ j) (SimplexCategory.σ i) =
      CategoryTheory.CategoryStruct.id { len := n }
-- Lean.Linter.UnusedVariables
/-- Gets the status of `linter.unusedVariables.funArgs`  -/
Lean.Linter.getLinterUnusedVariablesFunArgs : Lean.Linter.LinterOptions → Bool
-- Init.NotationExtra
unexpandTSyntax : Lean.PrettyPrinter.Unexpander
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.uliftYonedaIsoYoneda_hom_app_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{max w v₁, u₁} C] (X : C) (X_1 : Cᵒᵖ),
  (CategoryTheory.uliftYonedaIsoYoneda.hom.app X).app X_1 = Equiv.ulift.toIso.hom
-- Init.Data.String.Basic
/-- Constructs a valid position on `s` from a position, returning `none` if the position is not valid.  -/
String.Slice.pos? : (s : String.Slice) → String.Pos.Raw → Option s.Pos
-- Mathlib.Order.CompleteLattice.Basic
iInf_const : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {a : α} [Nonempty ι], ⨅ x, a = a
-- Mathlib.Topology.ApproximateUnit
/-- The filter is not `⊥`.  -/
Filter.IsApproximateUnit.neBot : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Mul α] {l : Filter α}, l.IsApproximateUnit → l.NeBot
-- Std.Http.Protocol.H1.Parser
/-- Parses a single header field line, or returns `none` when it sees the blank line that
terminates the header section.

```
field-line = field-name ":" OWS field-value OWS CRLF
```
 -/
Std.Http.Protocol.H1.parseSingleHeader : Std.Http.Protocol.H1.Config → Std.Internal.Parsec.ByteArray.Parser (Option (String × String))
-- Init.Data.String.Slice
String.Slice.SplitIterator.PlausibleStep : Type
-- Mathlib.Algebra.Order.GroupWithZero.Basic
div_lt_div_iff₀ : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b c d : G₀},
  0 < b → 0 < d → (a / b < c / d ↔ a * d < c * b)
-- Std.Internal.Do.WP.Basic
/-- `EStateM ε σ` is a WPMonad combining state and exceptions.  -/
Std.Internal.Do.EStateM.instWPMonad : {ε σ : Type} → Std.Internal.Do.WPMonad (EStateM ε σ) (σ → Prop) (ε → σ → Prop)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_eq_default : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {a : α} [inst_2 : Inhabited (β a)], a ∉ t → t.get! a = default
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.total.mapAux.mapMap_D₂_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂}
  (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂]
  [inst_4 : K.HasTotal c₁₂] [inst_5 : L.HasTotal c₁₂] (i₁₂ i₁₂' : I₁₂) {Z : C}
  (h : L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂' ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂)
      (CategoryTheory.CategoryStruct.comp (L.D₂ c₁₂ i₁₂ i₁₂') h) =
    CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂')
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂') h)
-- Mathlib.Analysis.Analytic.CPolynomialDef
FormalMultilinearSeries.sum_of_finite : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ}, (∀ (m : ℕ), n ≤ m → p m = 0) → ∀ (x : E), p.sum x = p.partialSum n x
-- Mathlib.Algebra.CharP.Defs
CharP.CharOne.subsingleton : ∀ {R : Type u_1} [inst : NonAssocSemiring R] [CharP R 1], Subsingleton R
-- Lean.DocString.Types
/-- Emphasis, typically rendered using italic text.
 -/
Lean.Doc.Inline.emph : {i : Type u} → Array (Lean.Doc.Inline i) → Lean.Doc.Inline i
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.instSemigroup : {d : ℤ} → Semigroup (ℤ√d)
-- Lean.Parser.Term
Lean.Parser.Term.valConfigItem.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.componentComplMk_mem : ∀ {V : Type u} {K : Set V} (G : SimpleGraph V) {v : V} (vK : v ∉ K), v ∈ G.componentComplMk vK
-- Init.Data.Order.MinMaxOn
maxOn_eq_or : ∀ {β : Type u_1} {α : Sort u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {x y : α},
  maxOn f x y = x ∨ maxOn f x y = y
-- Mathlib.GroupTheory.Solvable
/-- **Alias** of `Group.isSolvable_of_surjective`. -/
solvable_of_surjective : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] {f : G →* G'},
  Function.Surjective ⇑f → ∀ [Group.IsSolvable G], Group.IsSolvable G'
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
iteratedFDerivWithin_one_apply : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E},
  UniqueDiffWithinAt 𝕜 s x → ∀ (m : Fin 1 → E), (iteratedFDerivWithin 𝕜 1 f s x) m = (fderivWithin 𝕜 f s x) (m 0)
-- Mathlib.Topology.MetricSpace.Completion
/-- The lift of an isometry to completions.  -/
Isometry.mapRingHom : {α : Type u} →
  {β : Type v} →
    [inst : PseudoMetricSpace α] →
      [inst_1 : Ring α] →
        [inst_2 : IsTopologicalRing α] →
          [inst_3 : IsUniformAddGroup α] →
            [inst_4 : Ring β] →
              [inst_5 : PseudoMetricSpace β] →
                [inst_6 : IsUniformAddGroup β] →
                  [inst_7 : IsTopologicalRing β] →
                    {f : α →+* β} → Isometry ⇑f → UniformSpace.Completion α →+* UniformSpace.Completion β
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.support_C_subset : ∀ {R : Type u_1} [inst : Semiring R] (a : R), (SkewPolynomial.C a).support ⊆ {0}
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVUnOp.rotateRight.injEq : ∀ (n n_1 : ℕ), (Std.Tactic.BVDecide.BVUnOp.rotateRight n = Std.Tactic.BVDecide.BVUnOp.rotateRight n_1) = (n = n_1)
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- Naturality of the lax functoriality constraint, on the left.  -/
CategoryTheory.LaxFunctor.mapComp_naturality_left_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.LaxFunctor B CategoryTheory.Cat)
  {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (X : ↑(self.obj a)),
  CategoryTheory.CategoryStruct.comp ((self.mapComp f g).toNatTrans.app X)
      ((self.map₂ (CategoryTheory.Bicategory.whiskerRight η g)).toNatTrans.app X) =
    CategoryTheory.CategoryStruct.comp ((self.map g).toFunctor.map ((self.map₂ η).toNatTrans.app X))
      ((self.mapComp f' g).toNatTrans.app X)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
/-- An induction principle for elements of `⨆ i, S i`.
If `C` holds for `1` and all elements of `S i` for all `i`, and is preserved under multiplication,
then it holds for all elements of the supremum of `S`.  -/
Subgroup.iSup_induction : ∀ {G : Type u_2} [inst : Group G] {ι : Sort u_5} (S : ι → Subgroup G) {C : G → Prop} {x : G},
  x ∈ ⨆ i, S i → (∀ (i : ι), ∀ x ∈ S i, C x) → C 1 → (∀ (x y : G), C x → C y → C (x * y)) → C x
-- Init.Data.Rat.Lemmas
Rat.den_mkRat : ∀ (n : ℤ) (d : ℕ), (mkRat n d).den = if d = 0 then 1 else d / d.gcd n.natAbs
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.num : ℤ → Lean.Grind.CommRing.Poly
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instHashableCtorInfo.hash : Lean.Compiler.LCNF.CtorInfo → UInt64
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.RelabelNat.State.Inv1.insert : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {n : ℕ} {map : Std.HashMap α ℕ} {x : α},
  Std.Sat.AIG.RelabelNat.State.Inv1 n map → map[x]? = none → Std.Sat.AIG.RelabelNat.State.Inv1 (n + 1) (map.insert x n)
-- Mathlib.Analysis.Seminorm
Seminorm.iSup_apply : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {ι : Sort u_12}
  {p : ι → Seminorm 𝕜 E}, BddAbove (Set.range p) → ∀ {x : E}, (⨆ i, p i) x = ⨆ i, (p i) x
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.jacobiMatrix_ofAlgEquiv : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.PreSubmersivePresentation R S ι σ) {T : Type u_1} [inst_3 : CommRing T] [inst_4 : Algebra R T]
  (e : S ≃ₐ[R] T) [inst_5 : Fintype σ] [inst_6 : DecidableEq σ], (P.ofAlgEquiv e).jacobiMatrix = P.jacobiMatrix
-- Init.Data.Range.Polymorphic.Fin
Fin.instIsAlwaysFinite_2 : ∀ {n : ℕ}, Std.Rxi.IsAlwaysFinite (Fin n)
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
CategoryTheory.StrongEpi.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : C} {f : P ⟶ Q},
  CategoryTheory.Epi f →
    (∀ ⦃X Y : C⦄ (z : X ⟶ Y) [CategoryTheory.Mono z], CategoryTheory.HasLiftingProperty f z) →
      CategoryTheory.StrongEpi f
-- Init.MetaTypes
/-- When true (default: `true`) then the simplifier caches the result of simplifying each sub-expression, if possible.
 -/
Lean.Meta.Simp.Config.memoize : Lean.Meta.Simp.Config → Bool
-- Lean.Compiler.IR.Basic
Lean.IR.instInhabitedDecl : Inhabited Lean.IR.Decl
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
lineMap_lt_lineMap_iff_of_lt : ∀ {k : Type u_1} {E : Type u_2} [inst : Ring k] [inst_1 : PartialOrder k] [IsOrderedRing k] [inst_3 : AddCommGroup E]
  [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E] [IsStrictOrderedModule k E] {a b : E}
  {r r' : k} [PosSMulReflectLT k E], r < r' → ((AffineMap.lineMap a b) r < (AffineMap.lineMap a b) r' ↔ a < b)
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousMonoidHom.instContinuousEvalConst : ∀ (A : Type u_2) (B : Type u_3) [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B], ContinuousEvalConst (A →ₜ* B) A B
-- Mathlib.Order.CompleteLattice.Defs
le_sSup : ∀ {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α} {a : α}, a ∈ s → a ≤ sSup s
-- Mathlib.CategoryTheory.ObjectProperty.Retract
CategoryTheory.ObjectProperty.retractClosure_isoClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C),
  P.isoClosure.retractClosure = P.retractClosure
-- Mathlib.CategoryTheory.Limits.MonoCoprod
CategoryTheory.Limits.MonoCoprod.instMonoInr : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B : C} [CategoryTheory.Limits.MonoCoprod C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A B], CategoryTheory.Mono CategoryTheory.Limits.coprod.inr
-- Mathlib.RingTheory.Ideal.Span
Ideal.submodule_span_eq : ∀ {α : Type u} [inst : Semiring α] {s : Set α}, Submodule.span α s = Ideal.span s
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.NullMeasurable.measure_preimage_eq_measure_restrict_preimage_of_ae_compl_eq_const : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [inst : MeasurableSpace β]
  {b : β} {f : α → β} {s : Set α},
  MeasureTheory.NullMeasurable f (μ.restrict s) →
    (f =ᵐ[μ.restrict sᶜ] fun x => b) → ∀ {t : Set β}, MeasurableSet t → b ∉ t → μ (f ⁻¹' t) = (μ.restrict s) (f ⁻¹' t)
-- Lean.Expr
/-- Given `a b : Nat`, returns `a - b`  -/
Lean.mkNatSub : Lean.Expr → Lean.Expr → Lean.Expr
-- Init.Data.Vector.Lemmas
Vector.not_mem_of_not_mem_push : ∀ {α : Type u_1} {n : ℕ} {a b : α} {xs : Vector α n}, a ∉ xs.push b → a ∉ xs
-- Lean.Data.JsonRpc
Lean.JsonRpc.instToJsonMessageKind : Lean.ToJson Lean.JsonRpc.MessageKind
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.mem_range_deriv : ∀ {f : Ordinal.{u} → Ordinal.{u}}, Order.IsNormal f → ∀ {a : Ordinal.{u}}, a ∈ Set.range (Ordinal.deriv f) ↔ f a = a
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableAt.comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M → M'} (x : M) {g : M' → M''}, MDiffAt g (f x) → MDiffAt f x → MDiffAt (g ∘ f) x
-- Mathlib.Data.Set.Function
/-- This lemma is a special case of `rightInvOn_invFunOn.image_image'`; it may make more sense
to use the other lemma directly in an application.  -/
Set.SurjOn.image_invFunOn_image_of_subset : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} [inst : Nonempty α] {r : Set β},
  Set.SurjOn f s t → r ⊆ t → f '' Function.invFunOn f s '' r = r
-- Mathlib.Topology.UniformSpace.CompactConvergence
ContinuousMap.hasBasis_compactConvergenceUniformity : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β],
  (uniformity C(α, β)).HasBasis (fun p => IsCompact p.1 ∧ p.2 ∈ uniformity β) fun p =>
    {fg | ∀ x ∈ p.1, (fg.1 x, fg.2 x) ∈ p.2}
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.comp_map_eq_const_assoc : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (s : X.PtSimplex n x) {Y : SSet}
  (φ : Y ⟶ SSet.stdSimplex.obj { len := n }) [Y.HasDimensionLT n] {Z : SSet} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp φ (CategoryTheory.CategoryStruct.comp s.map h) =
    CategoryTheory.CategoryStruct.comp (SSet.const x) h