mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.forget_obj : ∀ (R : Type u) [inst : Ring R] {M : ModuleCat R}, (CategoryTheory.forget (ModuleCat R)).obj M = ↑M
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.liftCycles_leftHomologyπ_eq_zero_of_boundary : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) {A : C} (k : A ⟶ S.X₂) [inst_2 : S.HasLeftHomology] (x : A ⟶ S.X₁)
  (hx : k = CategoryTheory.CategoryStruct.comp x S.f),
  CategoryTheory.CategoryStruct.comp (S.liftCycles k ⋯) S.leftHomologyπ = 0
-- Mathlib.Order.RelSeries
RelSeries.cons_cast_succ : ∀ {α : Type u_1} {r : SetRel α α} (s : RelSeries r) (a : α) (h : (a, s.head) ∈ r) (i : Fin (s.length + 1)),
  (s.cons a h).toFun (Fin.cast ⋯ i.succ) = s.toFun i
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.mk_bot : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L : BooleanSubalgebra α}, ⟨⊥, ⋯⟩ = ⊥
-- Mathlib.Computability.StateTransition
_private.Mathlib.Computability.StateTransition.0.StateTransition.Respects.match_1.eq_1 : ∀ {σ₁ : Type u_1} (motive : Option σ₁ → Sort u_2) (b₁ : σ₁) (h_1 : (b₁ : σ₁) → motive (some b₁))
  (h_2 : Unit → motive none),
  (match some b₁ with
    | some b₁ => h_1 b₁
    | none => h_2 ()) =
    h_1 b₁
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy.h_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject.Augmented C}
  (ed : X.ExtraDegeneracy) {n : ℕ} (i : Fin (n + 1)) (j : ℕ)
  (hj : autoParam (j = ↑i.rev) CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy.h_eq._auto_1),
  CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy.h ed i =
    CategoryTheory.CategoryStruct.comp (X.left.δ₀Iter ↑i ⋯)
      (CategoryTheory.CategoryStruct.comp (ed.s j) (X.left.σ₀Iter ↑i ⋯))
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α} {fallback : β}, (m.erase k).getD a fallback = if (k == a) = true then fallback else m.getD a fallback
-- Lean.Meta.AbstractMVars
Lean.Meta.AbstractMVars.mkFreshFVarId : Lean.Meta.AbstractMVars.M Lean.FVarId
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.congr_simp : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  {S : AlgebraicGeometry.Scheme} {J : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} J]
  (D D_1 : CategoryTheory.Functor J (P.Over ⊤ S)),
  D = D_1 →
    ∀ (𝒰 : S.OpenCover) [inst_2 : CategoryTheory.Category.{v_3, u_2} 𝒰.I₀]
      [inst_3 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰],
      AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰 = AlgebraicGeometry.Scheme.Cover.ColimitGluingData D_1 𝒰
-- Mathlib.Topology.ContinuousOn
continuousOn_to_generateFrom_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {β : Type u_5} {T : Set (Set β)} {f : α → β},
  ContinuousOn f s ↔ ∀ x ∈ s, ∀ t ∈ T, f x ∈ t → f ⁻¹' t ∈ nhdsWithin x s
-- Init.System.IOError
IO.Error.mkResourceVanished : UInt32 → String → IO.Error
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.isLongestMatchAt_iff_extract : ∀ {pat : String} {s : String.Slice} {pos₁ pos₂ : s.Pos},
  pat ≠ "" →
    (String.Slice.Pattern.Model.IsLongestMatchAt pat pos₁ pos₂ ↔
      s.copy.toByteArray.extract pos₁.offset.byteIdx pos₂.offset.byteIdx = pat.toByteArray)
-- Lean.Meta.Basic
Lean.Meta.instInhabitedDefEqCacheKey.default : Lean.Meta.DefEqCacheKey
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_subtype_eq_of_mulSupport_subset : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {s : Set β},
  Function.mulSupport f ⊆ s → ∏' (x : ↑s), f ↑x = ∏' (x : β), f x
-- Mathlib.Algebra.Homology.TotalComplexSymmetry
HomologicalComplex₂.instHasTotalFlip : ∀ {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  (K : HomologicalComplex₂ C c₁ c₂) (c : ComplexShape J) [inst_2 : TotalComplexShape c₁ c₂ c]
  [inst_3 : TotalComplexShape c₂ c₁ c] [TotalComplexShapeSymmetry c₁ c₂ c] [K.HasTotal c], K.flip.HasTotal c
-- Mathlib.LinearAlgebra.Matrix.Basis
Module.Basis.toMatrix_self : ∀ {ι : Type u_1} {R : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (e : Module.Basis ι R M) [inst_3 : DecidableEq ι], e.toMatrix ⇑e = 1
-- Init.Data.Array.Bootstrap
Array.toList_empty : ∀ {α : Type u_1}, #[].toList = []
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.zeroLocus_minimalPrimes : ∀ (R : Type u) [inst : CommSemiring R],
  PrimeSpectrum.zeroLocus ∘ SetLike.coe '' minimalPrimes R = irreducibleComponents (PrimeSpectrum R)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.MethodsRef : Type
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_trunc : ∀ {M : Type u_2} [inst : AddCommMonoid M] {a b : ℕ} (f : Fin (a + b) → M),
  (∀ (j : Fin b), f (Fin.natAdd a j) = 0) → ∑ i, f i = ∑ i, f (Fin.castAdd b i)
-- Mathlib.SetTheory.Lists
_private.Mathlib.SetTheory.Lists.0.Lists.Subset.decidable.match_1.splitter : {α : Type u_1} →
  (motive : Lists' α true → Lists' α true → Sort u_2) →
    (x x_1 : Lists' α true) →
      ((x : Lists' α true) → motive Lists'.nil x) →
        ((b : Bool) → (a : Lists' α b) → (l₁ l₂ : Lists' α true) → motive (a.cons' l₁) l₂) → motive x x_1
-- Mathlib.CategoryTheory.Monoidal.Closed.Types
CategoryTheory.instMonoidalClosedFunctorType_1 : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.MonoidalClosed (CategoryTheory.Functor C (Type (max u₁ v₁)))
-- Mathlib.RingTheory.Extension.Basic
/-- A hom between two extensions induces a map between cotangent spaces.  -/
Algebra.Extension.Cotangent.map : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {P : Algebra.Extension R S} →
            {R' : Type u_1} →
              {S' : Type u_2} →
                [inst_3 : CommRing R'] →
                  [inst_4 : CommRing S'] →
                    [inst_5 : Algebra R' S'] →
                      {P' : Algebra.Extension R' S'} →
                        [inst_6 : Algebra R R'] →
                          [inst_7 : Algebra S S'] →
                            [inst_8 : Algebra R S'] →
                              [IsScalarTower R R' S'] → P.Hom P' → P.Cotangent →ₗ[S] P'.Cotangent
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_lt_of_lt_mul : ∀ {a b c : ENNReal}, a < b * c → a / c < b
-- Mathlib.Tactic.Tauto
/-- Matches propositions where we want to apply the `constructor` tactic in the
finishing stage of `tauto`.  -/
Mathlib.Tactic.Tauto.finishingConstructorMatcher : Q(Prop) → Lean.MetaM Bool
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
CategoryTheory.MorphismProperty.instIsIsoMapS_2 : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] {X Y : C} (z : W.RightFraction₂ X Y),
  CategoryTheory.IsIso (L.map z.s)
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.eq_of_forall_toMeasure_apply_eq_iff : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {μ ν : MeasureTheory.FiniteMeasure Ω},
  μ = ν ↔ ∀ (s : Set Ω), MeasurableSet s → ↑μ s = ↑ν s
-- Lean.Meta.Eqns
Lean.Meta.isEqnLikeSuffix : String → Bool
-- Mathlib.Algebra.Order.Group.Lattice
/-- Every lattice ordered commutative group is a distributive lattice.  -/
CommGroup.toDistribLattice : (α : Type u_2) → [inst : Lattice α] → [inst_1 : CommGroup α] → [MulLeftMono α] → DistribLattice α
-- Mathlib.Condensed.Discrete.Colimit
Condensed.lanPresheafExt.eq_1 : ∀ {F G : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))}
  (i : FintypeCat.toProfinite.op.comp F ≅ FintypeCat.toProfinite.op.comp G),
  Condensed.lanPresheafExt i =
    (FintypeCat.toProfinite.op.pointwiseLeftKanExtension (FintypeCat.toProfinite.op.comp F)).leftKanExtensionUniqueOfIso
      (FintypeCat.toProfinite.op.pointwiseLeftKanExtensionUnit (FintypeCat.toProfinite.op.comp F)) i
      (Condensed.lanPresheaf G)
      (FintypeCat.toProfinite.op.pointwiseLeftKanExtensionUnit (FintypeCat.toProfinite.op.comp G))
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.pos_eq_of_eq_right : ∀ {s : String} {p q : s.Pos} {s_1 s' t : String}, p.Splits s_1 t → q.Splits s' t → p = q
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.extendComp_inv_hom : ∀ {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).inv.hom = CategoryTheory.CategoryStruct.id X
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The second part of the third cosimplicial identity  -/
CategoryTheory.CosimplicialObject.δ_comp_σ_succ_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
  {i : Fin (n + 1)} {Z : C} (h : X.obj { len := n } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.δ i.succ) (CategoryTheory.CategoryStruct.comp (X.σ i) h) = h
-- Mathlib.NumberTheory.Modular
ModularGroup.coe_T_zpow_smul_eq : ∀ (z : UpperHalfPlane) {n : ℤ}, ↑(ModularGroup.T ^ n • z) = ↑z + ↑n
-- Mathlib.GroupTheory.Congruence.Basic
/-- The `AddSubmonoid` of `M × M` defined by an additive congruence
relation on an `AddMonoid` `M`.  -/
AddCon.addSubmonoid : {M : Type u_1} → [inst : AddZeroClass M] → AddCon M → AddSubmonoid (M × M)
-- Mathlib.Analysis.Calculus.VectorField
/-- The differentiation operator along `[W, V]`
is the commutator of the differentiation operators along `W` and `V`.  -/
VectorField.fderivWithin_apply_lieBracket_of_isSymmSndFDerivWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {V W : E → E}
  {s : Set E} {x : E} {f : E → F},
  ContDiffWithinAt 𝕜 2 f s x →
    IsSymmSndFDerivWithinAt 𝕜 f s x →
      UniqueDiffOn 𝕜 s →
        x ∈ s →
          DifferentiableWithinAt 𝕜 W s x →
            DifferentiableWithinAt 𝕜 V s x →
              (fderivWithin 𝕜 f s x) (VectorField.lieBracketWithin 𝕜 V W s x) =
                (fderivWithin 𝕜 (fun x => (fderivWithin 𝕜 f s x) (W x)) s x) (V x) -
                  (fderivWithin 𝕜 (fun x => (fderivWithin 𝕜 f s x) (V x)) s x) (W x)
-- Std.Data.TreeSet.Raw.Slice
Std.TreeSet.Raw.toList_rco : ∀ {α : Type u} (cmp : autoParam (α → α → Ordering) Std.TreeSet.Raw.toList_rco._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeSet.Raw α cmp},
  t.WF →
    ∀ {lowerBound upperBound : α},
      Std.Slice.toList (Std.Rco.Sliceable.mkSlice t lowerBound...upperBound) =
        List.filter (fun e => decide ((cmp e lowerBound).isGE = true ∧ (cmp e upperBound).isLT = true)) t.toList
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.whiskerLeft_sum : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (P : C) {Q R : C} {J : Type u_2}
  (s : Finset J) (g : J → (Q ⟶ R)),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (∑ j ∈ s, g j) =
    ∑ j ∈ s, CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (g j)
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.comap_sup_map_of_injective : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂},
  Function.Injective ⇑f → ∀ (p q : Submodule R M), Submodule.comap f (Submodule.map f p ⊔ Submodule.map f q) = p ⊔ q
-- Mathlib.RingTheory.ClassGroup.Basic
ClassGroup.equiv.eq_1 : ∀ {R : Type u_1} (K : Type u_2) [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDomain R],
  ClassGroup.equiv K =
    QuotientGroup.congr (toPrincipalIdeal R (FractionRing R)).range (toPrincipalIdeal R K).range
      (Units.mapEquiv (FractionalIdeal.canonicalEquiv (nonZeroDivisors R) (FractionRing R) K).toMulEquiv) ⋯
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.isSFiniteKernel_prodMkLeft_unit : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β},
  ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.Kernel.prodMkLeft Unit κ) ↔ ProbabilityTheory.IsSFiniteKernel κ
-- Mathlib.Topology.Category.UniformSpace
UniformSpaceCat.coe_of : ∀ (X : Type u) [inst : UniformSpace X], { carrier := X, str := inst }.carrier = X
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_ite_eq : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] {s : Finset ι} [inst_2 : DecidableEq ι]
  (i : ι) (f : ι → M), (s.expect fun j => if i = j then f j else 0) = if i ∈ s then (↑s.card)⁻¹ • f i else 0
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.IsInt.of_raw : ∀ (α : Type u_1) [inst : Ring α] (n : ℤ), Mathlib.Meta.NormNum.IsInt n.rawCast n
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.cRank.eq_1 : ∀ {α : Type u} (M : Matroid α), M.cRank = ⨆ B, Cardinal.mk ↑↑B
-- Mathlib.Algebra.Category.Ring.Constructions
/-- The trivial ring is the (strict) terminal object of `CommRingCat`.  -/
CommRingCat.punitIsTerminal : CategoryTheory.Limits.IsTerminal (CommRingCat.of PUnit.{u + 1})
-- Mathlib.CategoryTheory.Sites.Monoidal
CategoryTheory.Sheaf.instMonoidalFunctorOppositePresheafToSheaf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (A : Type u₃) →
        [inst_1 : CategoryTheory.Category.{v₃, u₃} A] →
          [inst_2 : CategoryTheory.MonoidalCategory A] →
            [inst_3 : J.W.IsMonoidal] →
              [inst_4 : CategoryTheory.HasWeakSheafify J A] → (CategoryTheory.presheafToSheaf J A).Monoidal
-- Init.Data.Array.Lex.Lemmas
Array.lt_iff_exists : ∀ {α : Type u_1} [inst : LT α] {xs ys : Array α},
  xs < ys ↔
    xs = ys.take xs.size ∧ xs.size < ys.size ∨
      ∃ i, ∃ (h₁ : i < xs.size) (h₂ : i < ys.size), (∀ (j : ℕ) (hj : j < i), xs[j] = ys[j]) ∧ xs[i] < ys[i]
-- Mathlib.Data.PFunctor.Multivariate.Basic
MvPFunctor.comp_map : ∀ {n : ℕ} (P : MvPFunctor.{u} n) {α β γ : TypeVec.{u} n} (f : α.Arrow β) (g : β.Arrow γ) (x : ↑P α),
  MvFunctor.map (TypeVec.comp g f) x = MvFunctor.map g (MvFunctor.map f x)
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B}
  (f : a ⟶ b) (X : ↑(F.obj a)),
  (F.map f).toFunctor.map ((F.mapId a).inv.toNatTrans.app X) =
    CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.leftUnitor f).inv).toNatTrans.app X)
      ((F.mapComp (CategoryTheory.CategoryStruct.id a) f).hom.toNatTrans.app X)
-- Mathlib.Algebra.Group.Subgroup.Actions
Subgroup.mk_smul : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {S : Subgroup G} (g : G) (hg : g ∈ S) (a : α),
  ⟨g, hg⟩ • a = g • a
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.get?.match_1.eq_2 : ∀ {α : Type u_2} {β : Type u_1} (motive : (Std.DHashMap.Internal.AssocList α fun x => β) → Sort u_3) (k : α) (v : β)
  (es : Std.DHashMap.Internal.AssocList α fun x => β) (h_1 : Unit → motive Std.DHashMap.Internal.AssocList.nil)
  (h_2 :
    (k : α) →
      (v : β) →
        (es : Std.DHashMap.Internal.AssocList α fun x => β) → motive (Std.DHashMap.Internal.AssocList.cons k v es)),
  (match Std.DHashMap.Internal.AssocList.cons k v es with
    | Std.DHashMap.Internal.AssocList.nil => h_1 ()
    | Std.DHashMap.Internal.AssocList.cons k v es => h_2 k v es) =
    h_2 k v es
-- Mathlib.Data.Finmap
Finmap.instInhabited : {α : Type u} → {β : α → Type v} → Inhabited (Finmap β)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ColorInformation.mk.injEq : ∀ (range : Lean.Lsp.Range) (color : Lean.Lsp.Color) (range_1 : Lean.Lsp.Range) (color_1 : Lean.Lsp.Color),
  ({ range := range, color := color } = { range := range_1, color := color_1 }) = (range = range_1 ∧ color = color_1)
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.neg_pi_lt_log_im : ∀ (x : ℂ), -Real.pi < (Complex.log x).im
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instNonUnitalSemiring : {k : Type u_1} →
  {G : Type u_2} →
    [inst : Semiring k] → [inst_1 : Monoid G] → [MulSemiringAction G k] → NonUnitalSemiring (SkewMonoidAlgebra k G)
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MCasesPat.alts : List Lean.Parser.Tactic.MCasesPat → Lean.Parser.Tactic.MCasesPat
-- Mathlib.CategoryTheory.Linear.Basic
/-- compatibility of the scalar multiplication with the post-composition  -/
CategoryTheory.Linear.smul_comp : ∀ {R : Type w} {inst : Semiring R} {C : Type u} {inst_1 : CategoryTheory.Category.{v, u} C}
  {inst_2 : CategoryTheory.Preadditive C} [self : CategoryTheory.Linear R C] (X Y Z : C) (r : R) (f : X ⟶ Y)
  (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (r • f) g = r • CategoryTheory.CategoryStruct.comp f g
-- Init.Data.String.Basic
String.Pos.Raw.isValid_iff_isSome_utf8DecodeChar? : ∀ {s : String} {p : String.Pos.Raw},
  String.Pos.Raw.IsValid s p ↔ p = s.rawEndPos ∨ (s.toByteArray.utf8DecodeChar? p.byteIdx).isSome = true
-- Mathlib.Order.Category.LinOrd
/-- The underlying `OrderHom`.  -/
LinOrd.Hom.hom' : {X Y : LinOrd} → X.Hom Y → ↑X →o ↑Y
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map_equiv_top : ∀ {N : Type u_2} [inst : MulOneClass N] {M : Type u_5} [inst_1 : MulOneClass M] (f : M ≃* N), Submonoid.map f ⊤ = ⊤
-- Init.Data.UInt.Lemmas
UInt16.ofNat_uInt32ToNat : ∀ (n : UInt32), UInt16.ofNat n.toNat = n.toUInt16
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.equivUnitsAffineMap_symm_apply_toFun : ∀ {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (u : (P₁ →ᵃ[k] P₁)ˣ) (a : P₁), (AffineEquiv.equivUnitsAffineMap.symm u) a = ↑u a
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.instConcreteCategoryAddMonoidHomCarrier : CategoryTheory.ConcreteCategory AddGrpCat fun x1 x2 => ↑x1 →+ ↑x2
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothBumpCovering.mk.injEq : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] [inst_5 : FiniteDimensional ℝ E] {s : Set M} (c : ι → M)
  (toFun : (i : ι) → SmoothBumpFunction I (c i)) (c_mem' : ∀ (i : ι), c i ∈ s)
  (locallyFinite' : LocallyFinite fun i => Function.support ↑(toFun i))
  (eventuallyEq_one' : ∀ x ∈ s, ∃ i, ↑(toFun i) =ᶠ[nhds x] 1) (c_1 : ι → M)
  (toFun_1 : (i : ι) → SmoothBumpFunction I (c_1 i)) (c_mem'_1 : ∀ (i : ι), c_1 i ∈ s)
  (locallyFinite'_1 : LocallyFinite fun i => Function.support ↑(toFun_1 i))
  (eventuallyEq_one'_1 : ∀ x ∈ s, ∃ i, ↑(toFun_1 i) =ᶠ[nhds x] 1),
  ({ c := c, toFun := toFun, c_mem' := c_mem', locallyFinite' := locallyFinite',
        eventuallyEq_one' := eventuallyEq_one' } =
      { c := c_1, toFun := toFun_1, c_mem' := c_mem'_1, locallyFinite' := locallyFinite'_1,
        eventuallyEq_one' := eventuallyEq_one'_1 }) =
    (c = c_1 ∧ toFun ≍ toFun_1)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.continuousOn_rpowIntegrand₀₁_uncurry : ∀ {p : ℝ}, p ∈ Set.Ioo 0 1 → ∀ s ⊆ Set.Ici 0, ContinuousOn (Function.uncurry p.rpowIntegrand₀₁) (Set.Ioi 0 ×ˢ s)
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.instFiniteQuotientIdealHSMulTop : ∀ {R : Type u_1} [inst : CommRing R] (M : Type u_3) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Finite R M]
  (I : Ideal R), Module.Finite (R ⧸ I) (M ⧸ I • ⊤)
-- Mathlib.Analysis.Normed.Group.Constructions
Prod.norm_mk : ∀ {E : Type u_2} {F : Type u_3} [inst : Norm E] [inst_1 : Norm F] (x : E) (y : F), ‖(x, y)‖ = max ‖x‖ ‖y‖
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.equalizer_as_kernel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f],
  CategoryTheory.Limits.equalizer.ι f 0 = CategoryTheory.Limits.kernel.ι f
-- Mathlib.Order.Hom.Bounded
/-- The type of bounded order homomorphisms from `α` to `β`.  -/
BoundedOrderHom : (α : Type u_6) →
  (β : Type u_7) →
    [inst : Preorder α] → [inst_1 : Preorder β] → [BoundedOrder α] → [BoundedOrder β] → Type (max u_6 u_7)
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
/-- As the thickening radius δ tends to 0, the δ-thickened indicator of a set E (in α) tends
pointwise (i.e., w.r.t. the product topology on `α → ℝ≥0∞`) to the indicator function of the
closure of E.

This statement is for the unbundled `ℝ≥0∞`-valued functions `thickenedIndicatorAux δ E`, see
`thickenedIndicator_tendsto_indicator_closure` for the version for bundled `ℝ≥0`-valued
bounded continuous functions.  -/
thickenedIndicatorAux_tendsto_indicator_closure : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {δseq : ℕ → ℝ},
  Filter.Tendsto δseq Filter.atTop (nhds 0) →
    ∀ (E : Set α),
      Filter.Tendsto (fun n => thickenedIndicatorAux (δseq n) E) Filter.atTop (nhds ((closure E).indicator fun x => 1))
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.single_ne_zero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {a : Γ} {r : R},
  r ≠ 0 → (HahnSeries.single a) r ≠ 0
-- Mathlib.Data.Set.SMulAntidiagonal
Set.SMulAntidiagonal.eq_of_fst_eq_fst : ∀ {G : Type u_1} {P : Type u_2} {s : Set G} {t : Set P} {a : P} [inst : SMul G P] {x y : ↑(s.smulAntidiagonal t a)}
  [IsLeftCancelSMul G P], (↑x).1 = (↑y).1 → x = y
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.rename_comp_rename : ∀ {σ : Type u_1} {τ : Type u_2} {α : Type u_3} {R : Type u_4} [inst : CommSemiring R] (f : σ → τ) (g : τ → α),
  (MvPolynomial.rename g).comp (MvPolynomial.rename f) = MvPolynomial.rename (g ∘ f)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup'_cons : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : β → α) {b : β}
  {hb : b ∉ s}, (Finset.cons b s hb).sup' ⋯ f = f b ⊔ s.sup' H f
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `IsDedekindDomain.HeightOneSpectrum.ext`. -/
IsDedekindDomain.HeightOneSpectrum.asIdeal_inj : ∀ {R : Type u_1} {inst : CommRing R} {x y : IsDedekindDomain.HeightOneSpectrum R}, x.asIdeal = y.asIdeal → x = y
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegular.map_of_continuous : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [BorelSpace α] [inst_3 : MeasurableSpace β] [inst_4 : TopologicalSpace β] [BorelSpace β] [h : μ.InnerRegular]
  {f : α → β}, Continuous f → (MeasureTheory.Measure.map f μ).InnerRegular
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.instIsRepresentableCompOppositeOpObjTypeYonedaObjRightAdjointObjIsDefined : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (Y : F.PartialRightAdjointSource),
  (F.op.comp (CategoryTheory.yoneda.obj Y.obj)).IsRepresentable
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.length_toListRev_eq_length : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β}, it.toListRev.length = it.length