mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.GroupAction.Defs
/-- The submonoid of elements fixed under the whole action.  -/
FixedPoints.submonoid : (M : Type u) → (α : Type v) → [inst : Monoid M] → [inst_1 : Monoid α] → [MulDistribMulAction M α] → Submonoid α
-- Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
alternatingGroup.card_two_sylow_of_card_eq_four : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α],
  Nat.card α = 4 → ∀ (S : Sylow 2 ↥(alternatingGroup α)), Nat.card ↥↑S = 4
-- Mathlib.Algebra.WithConv
WithConv.equiv_apply : ∀ {A : Type u_2} (x : WithConv A), (WithConv.equiv A) x = x.ofConv
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.prodCongr_apply : ∀ {R : Type u_7} {R' : Type u_8} {S : Type u_9} {S' : Type u_10} [inst : NonUnitalNonAssocSemiring R]
  [inst_1 : NonUnitalNonAssocSemiring R'] [inst_2 : NonUnitalNonAssocSemiring S] [inst_3 : NonUnitalNonAssocSemiring S']
  (f : R ≃+* R') (g : S ≃+* S') (a : R × S), (f.prodCongr g) a = Prod.map (⇑f) (⇑g) a
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- Mapping from variable to occurrences. For example, an entry `x ↦ {y, z}` means that `x` may occur in `dvdCnstrs`, `lowers`, or `uppers` of
variables `y` and `z`.
If `x` occurs in `dvdCnstrs[y]`, `lowers[y]`, or `uppers[y]`, then `y` is in `occurs[x]`, but the reverse is not true.
If `x` is in `elimStack`, then `occurs[x]` is the empty set.
 -/
Lean.Meta.Grind.Arith.Cutsat.State.occurs : Lean.Meta.Grind.Arith.Cutsat.State → Lean.PArray Lean.Meta.Grind.Arith.Cutsat.VarSet
-- Init.Data.Array.Lex.Lemmas
Array.instIsLinearOrderOfLawfulOrderLT : ∀ {α : Type u_1} [inst : LT α] [inst_1 : LE α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α], Std.IsLinearOrder (Array α)
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal_transpose : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] (v : n → α),
  (Matrix.diagonal v).transpose = Matrix.diagonal v
-- Lean.Exception
Lean.Exception.error.sizeOf_spec : ∀ (ref : Lean.Syntax) (msg : Lean.MessageData), sizeOf (Lean.Exception.error ref msg) = 1 + sizeOf ref + sizeOf msg
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isLongestMatch_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatch pat pos ↔
    String.Slice.Pattern.Model.IsMatch pat pos ∧
      ∀ (pos' : s.Pos), pos < pos' → ¬String.Slice.Pattern.Model.IsMatch pat pos'
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.biprodXIso_hom_fst : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (K L : HomologicalComplex C c)
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] (i : ι),
  CategoryTheory.CategoryStruct.comp (K.biprodXIso L i).hom CategoryTheory.Limits.biprod.fst =
    CategoryTheory.Limits.biprod.fst.f i
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.range_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {G : Type u_7} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 F G}, Set.range ↑(I.prod J) = Set.range ↑I ×ˢ Set.range ↑J
-- Mathlib.CategoryTheory.Sites.Whiskering
_private.Mathlib.CategoryTheory.Sites.Whiskering.0.CategoryTheory.GrothendieckTopology.Cover.multicospanComp.match_1.splitter : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {X : C} →
        (S : J.Cover X) →
          (motive : CategoryTheory.Limits.WalkingMulticospan S.shape → Sort u_3) →
            (t : CategoryTheory.Limits.WalkingMulticospan S.shape) →
              ((a : S.shape.L) → motive (CategoryTheory.Limits.WalkingMulticospan.left a)) →
                ((a : S.shape.R) → motive (CategoryTheory.Limits.WalkingMulticospan.right a)) → motive t
-- Init.Data.String.Modify
String.mapAux : (Char → Char) → (s : String) → s.Pos → String
-- Batteries.Data.List.Basic
List.all₂.eq_def : ∀ {α : Type u_1} {β : Type u_2} (r : α → β → Bool) (x : List α) (x_1 : List β),
  List.all₂ r x x_1 =
    match x, x_1 with
    | [], [] => true
    | a :: as, b :: bs => if r a b = true then List.all₂ r as bs else false
    | x, x_2 => false
-- Mathlib.CategoryTheory.Equivalence.Symmetry
CategoryTheory.Equivalence.symmEquivInverse_obj_unitIso_inv : ∀ (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] (X : (D ≌ C)ᵒᵖ),
  ((CategoryTheory.Equivalence.symmEquivInverse C D).obj X).unitIso.inv = (Opposite.unop X).counitIso.hom
-- Mathlib.Analysis.Convex.AmpleSet
/-- Affine translations of ample sets are ample.  -/
AmpleSet.vadd : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousAdd E]
  {s : Set E}, AmpleSet s → ∀ {y : E}, AmpleSet (y +ᵥ s)
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.instInhabited : {α : Type u_1} → Inhabited (MeasureTheory.OuterMeasure α)
-- Init.Data.List.Sublist
List.instTransSublist : {α : Type u_1} → Trans List.Sublist List.Sublist List.Sublist
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs_ite : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] {a b : α} (p : Prop) [inst_2 : Decidable p],
  |if p then a else b| = if p then |a| else |b|
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the reverse direction of `Asymptotics.isLittleO_neg_right`. -/
Asymptotics.IsLittleO.neg_right : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
  {g' : α → F'} {l : Filter α}, f =o[l] g' → f =o[l] fun x => -g' x
-- Mathlib.CategoryTheory.Subobject.FactorThru
CategoryTheory.Subobject.factorThru_ofLE : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y Z : C} {P Q : CategoryTheory.Subobject Y} {f : Z ⟶ Y}
  (h : P ≤ Q) (w : P.Factors f), Q.factorThru f ⋯ = CategoryTheory.CategoryStruct.comp (P.factorThru f w) (P.ofLE Q h)
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.CommRingObjCat.forget₂RingObjCat_obj_X : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (R : CategoryTheory.CommRingObjCat C),
  ((CategoryTheory.CommRingObjCat.forget₂RingObjCat C).obj R).X = R.X
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
/-- The most basic case possible: two ordered points, with N = 1. This lemma is used in the proof of
the general error bound later on.  -/
_private.Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule.0.trapezoidal_error_le_of_lt' : ∀ {f : ℝ → ℝ} {ζ a b : ℝ},
  a < b →
    DifferentiableOn ℝ f (Set.Icc a b) →
      DifferentiableOn ℝ (derivWithin f (Set.Icc a b)) (Set.Icc a b) →
        (∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ) → |trapezoidal_error f 1 a b| ≤ (b - a) ^ 3 * ζ / 12
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey?_insert_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, t.isEmpty = true → (t.insert k v).minKey? = some k
-- Lean.Server.References
Lean.Server.instEmptyCollectionDirectImports : EmptyCollection Lean.Server.DirectImports
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] (f : α → β) (v : α →₀ M),
  Finsupp.mapDomain f v = v.sum fun a => Finsupp.single (f a)
-- Mathlib.Analysis.Complex.Norm
Complex.cauSeqIm.eq_1 : ∀ (f : CauSeq ℂ fun x => ‖x‖), Complex.cauSeqIm f = ⟨fun n => (↑f n).im, ⋯⟩
-- Mathlib.Order.KrullDimension
Order.coe_lt_height_iff : ∀ {α : Type u_1} [inst : Preorder α] {x : α} {n : ℕ},
  Order.height x < ⊤ → (↑n < Order.height x ↔ ∃ y < x, Order.height y = ↑n)
-- Mathlib.Order.UpperLower.CompleteLattice
/-- The complement of a lower set as an upper set.  -/
LowerSet.compl : {α : Type u_1} → [inst : LE α] → LowerSet α → UpperSet α
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.congr_refl : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S), WithAbs.congr v v (RingEquiv.refl R) = RingEquiv.refl (WithAbs v)
-- Mathlib.Topology.VectorBundle.Riemannian
/-- The continuity at `0` is automatic when `E b` is isomorphic to a normed space, but since
we are not making this assumption here we have to include it.  -/
Bundle.RiemannianMetric.continuousAt : ∀ {B : Type u_4} {E : B → Type u_6} [inst : (b : B) → TopologicalSpace (E b)] [inst_1 : (b : B) → AddCommGroup (E b)]
  [inst_2 : (b : B) → Module ℝ (E b)] (self : Bundle.RiemannianMetric E) (b : B),
  ContinuousAt (fun v => ((self.inner b) v) v) 0
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.instIsClosedUnderIsomorphismsMinus : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C), t.minus.IsClosedUnderIsomorphisms
-- Mathlib.RingTheory.Binomial
Ring.choose_smul_choose : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : Pow R ℕ] [inst_2 : BinomialRing R] [NatPowAssoc R] (r : R) {n k : ℕ},
  k ≤ n → n.choose k • Ring.choose r n = Ring.choose r k * Ring.choose (r - ↑k) (n - k)
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
/-- A vector with coprime entries, right-multiplied by a matrix in `SL(2, R)`, has
coprime entries.  -/
IsCoprime.vecMulSL : ∀ {R : Type u_1} [inst : CommRing R] {v : Fin 2 → R},
  IsCoprime (v 0) (v 1) →
    ∀ (A : Matrix.SpecialLinearGroup (Fin 2) R), IsCoprime (Matrix.vecMul v (↑A) 0) (Matrix.vecMul v (↑A) 1)
-- Mathlib.SetTheory.Cardinal.Aleph
/-- The "pre-aleph" function gives the cardinals listed by their ordinal index. `preAleph n = n`,
`preAleph ω = ℵ₀`, `preAleph (ω + 1) = succ ℵ₀`, etc.

For the more common aleph function skipping over finite cardinals, see `Cardinal.aleph`.  -/
Cardinal.preAleph : Ordinal.{u} ≃o Cardinal.{u}
-- Init.Data.Format.Basic
Std.Format.line.sizeOf_spec : sizeOf Std.Format.line = 1
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.sub_v : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} {n : ℤ} (z₁ z₂ : CochainComplex.HomComplex.Cochain F G n) (p q : ℤ) (hpq : p + n = q),
  (z₁ - z₂).v p q hpq = z₁.v p q hpq - z₂.v p q hpq
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get!_union_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ ∪ m₂).get! k = m₂.get! k
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Nat.instDecidableExistsPowEq : {n a : ℕ} → Decidable (∃ x, x ^ n = a)
-- Mathlib.Topology.MetricSpace.Snowflaking
/-- The natural uniform space equivalence between `Snowflaking X α hα hα₁`
and the underlying space.  -/
Metric.Snowflaking.uniformEquiv : {X : Type u_1} → {α : ℝ} → {hα₀ : 0 < α} → {hα₁ : α ≤ 1} → [inst : UniformSpace X] → Metric.Snowflaking X α hα₀ hα₁ ≃ᵤ X
-- Mathlib.Algebra.Order.Quantale
/-- A quantale is a semigroup distributing over a complete lattice.  -/
IsQuantale : (α : Type u_1) → [Semigroup α] → [CompleteLattice α] → Prop
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.leSigmaOfOrd_total : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.OrientedOrd α] (a b : (a : α) × β a), a ≤ b ∨ b ≤ a
-- Std.Data.ExtDTreeMap.Basic
Std.ExtDTreeMap.instInhabited : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Inhabited (Std.ExtDTreeMap α β cmp)
-- Mathlib.Analysis.Convex.GaugeRescale
gaugeRescale_smul : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] (s t : Set E) {c : ℝ},
  0 ≤ c → ∀ (x : E), gaugeRescale s t (c • x) = c • gaugeRescale s t x
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.quotNilradicalEquivPi_apply : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsArtinianRing R] (a : R ⧸ nilradical R) (I : MaximalSpectrum R),
  (IsArtinianRing.quotNilradicalEquivPi R) a I =
    (Ideal.quotientInfRingEquivPiQuotient MaximalSpectrum.asIdeal ⋯) ((Ideal.quotientEquivAlgOfEq R ⋯) a) I
-- Mathlib.Order.SuccPred.CompleteLinearOrder
csInf_mem_of_not_isPredPrelimit : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] {s : Set α},
  s.Nonempty → BddBelow s → ¬Order.IsPredPrelimit (sInf s) → sInf s ∈ s
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.mkBelowMatcher.addVars : Array Lean.Expr →
  Array (ℕ × Lean.Name) → ℕ → Array Lean.Expr → (Array Lean.Expr → Lean.MetaM Lean.Expr) → Lean.MetaM Lean.Expr
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableAtFilter.sup_iff : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε']
  [inst_1 : ESeminormedAddMonoid ε'] [TopologicalSpace.PseudoMetrizableSpace ε'] {f : α → ε'} {l l' : Filter α},
  MeasureTheory.IntegrableAtFilter f (l ⊔ l') μ ↔
    MeasureTheory.IntegrableAtFilter f l μ ∧ MeasureTheory.IntegrableAtFilter f l' μ
-- Mathlib.Order.Hom.Bounded
BotHom.instPreorder : {α : Type u_2} → {β : Type u_3} → [inst : Bot α] → [Preorder β] → [inst_2 : Bot β] → Preorder (BotHom α β)
-- Mathlib.Order.Antichain
IsStrongAntichain.subset : ∀ {α : Type u_1} {r : α → α → Prop} {s t : Set α}, IsStrongAntichain r s → t ⊆ s → IsStrongAntichain r t
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
/-- **Alias** of the forward direction of `mdifferentiable_iff_differentiable`.

---

For maps between vector spaces, `MDifferentiable` and `Differentiable` coincide  -/
MDifferentiable.differentiable : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {f : E → E'},
  MDiff f → Differentiable 𝕜 f
-- Mathlib.Order.Filter.Cofinite
Filter.mem_cofinite : ∀ {α : Type u_2} {s : Set α}, s ∈ Filter.cofinite ↔ sᶜ.Finite
-- Init.Data.Option.Attach
Option.attachWith_map_subtype_val : ∀ {α : Type u_1} {p : α → Prop} (o : Option α) (H : ∀ (a : α), o = some a → p a),
  Option.map Subtype.val (o.attachWith p H) = o
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.Bool.not_ite_beq : ∀ {a b c : Bool}, ((!bif c then a else b) == a) = (!c && a == !b)
-- Batteries.Tactic.PrintOpaques
/-- The command `#print opaques X` prints all opaque definitions that `X` depends on.

Opaque definitions include partial definitions and axioms. Only dependencies that occur in a
computationally relevant context are listed, occurrences within proof terms are omitted. This is
useful to determine whether and how a definition is possibly platform dependent, possibly partial,
or possibly noncomputable.

The command `#print opaques Std.HashMap.insert` shows that `Std.HashMap.insert` depends on the
opaque definitions: `System.Platform.getNumBits` and `UInt64.toUSize`. Thus `Std.HashMap.insert`
may have different behavior when compiled on a 32 bit or 64 bit platform.

The command `#print opaques Stream.forIn` shows that `Stream.forIn` is possibly partial since it
depends on the partial definition `Stream.forIn.visit`. Indeed, `Stream.forIn` may not terminate
when the input stream is unbounded.

The command `#print opaques Classical.choice` shows that `Classical.choice` is itself an opaque
definition: it is an axiom. However, `#print opaques Classical.axiomOfChoice` returns nothing
since it is a proposition, hence not computationally relevant. (The command `#print axioms` does
reveal that `Classical.axiomOfChoice` depends on the `Classical.choice` axiom.)
 -/
Batteries.Tactic.«command#printOpaques_» : Lean.ParserDescr
-- Mathlib.Probability.Kernel.RadonNikodym
/-- The set of points `a : α` such that `κ a ≪ η a` is measurable.  -/
ProbabilityTheory.Kernel.measurableSet_absolutelyContinuous : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ)
  [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η],
  MeasurableSet {a | (κ a).AbsolutelyContinuous (η a)}
-- Mathlib.Topology.NoetherianSpace
TopologicalSpace.NoetherianSpace.inter_of_right : ∀ {α : Type u_1} [inst : TopologicalSpace α] (W V : Set α) [TopologicalSpace.NoetherianSpace ↑V],
  TopologicalSpace.NoetherianSpace ↑(W ∩ V)
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.generateFrom_le_iff_subset_toPlots : ∀ {X : Type u_1} {g : Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X))} {d : DiffeologicalSpace X},
  DiffeologicalSpace.generateFrom g ≤ d ↔ g ⊆ d.toPlots
-- Lean.Declaration
Lean.mkConstructorValEx : Lean.Name → List Lean.Name → Lean.Expr → Lean.Name → ℕ → ℕ → ℕ → Bool → Lean.ConstructorVal
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_alter_le_size : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, (t.alter k f).size ≤ t.size + 1
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.id_τl : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} (α : a ⟶ b),
  (CategoryTheory.CategoryStruct.id α).τl = CategoryTheory.CategoryStruct.id α.l
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
IsAddKleinFour.add_self : ∀ {G : Type u_1} [inst : AddGroup G] [IsAddKleinFour G] (x : G), x + x = 0
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.comp_actionHomLeft_assoc : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {w x y : C} (f : w ⟶ x) (g : x ⟶ y) (z : D) {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj y z ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft (CategoryTheory.CategoryStruct.comp f g)
        z)
      h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f z)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft g z)
        h)
-- Lean.PrettyPrinter.Delaborator.Basic
/-- Creates an identifier that is annotated with the term `e`, using a fresh position using the `HoleIterator`.
 -/
Lean.PrettyPrinter.Delaborator.mkAnnotatedIdent : Lean.Name → Lean.Expr → Lean.PrettyPrinter.Delaborator.DelabM Lean.Ident
-- Mathlib.Topology.TietzeExtension
/-- **Tietze extension theorem** for real-valued bounded continuous maps, a version with a closed
embedding and unbundled composition. If `e : C(X, Y)` is a closed embedding of a topological space
into a normal topological space and `f : X →ᵇ ℝ` is a bounded continuous function, then there exists
a bounded continuous function `g : Y →ᵇ ℝ` of the same norm such that `g ∘ e = f`.  -/
BoundedContinuousFunction.exists_extension_norm_eq_of_isClosedEmbedding : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [NormalSpace Y]
  (f : BoundedContinuousFunction X ℝ) {e : X → Y}, Topology.IsClosedEmbedding e → ∃ g, ‖g‖ = ‖f‖ ∧ ⇑g ∘ e = ⇑f
-- Mathlib.LinearAlgebra.TensorProduct.Quotient
TensorProduct.tensorQuotientEquiv_symm_apply_tmul_mk : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (n : Submodule R N) (x : M) (y : N),
  (TensorProduct.tensorQuotientEquiv M n).symm (Submodule.Quotient.mk (x ⊗ₜ[R] y)) = x ⊗ₜ[R] Submodule.Quotient.mk y
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.LazyTraceChildren.mk.sizeOf_spec : ∀ (indent : ℕ) (children : Array (Lean.Server.WithRpcRef Lean.MessageData)),
  sizeOf { indent := indent, children := children } = 1 + sizeOf indent + sizeOf children
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.rTensor_sub : ∀ {R : Type u_1} [inst : CommSemiring R] {N : Type u_3} {P : Type u_4} {Q : Type u_5} [inst_1 : AddCommMonoid N]
  [inst_2 : AddCommGroup P] [inst_3 : AddCommMonoid Q] [inst_4 : Module R N] [inst_5 : Module R P] [inst_6 : Module R Q]
  (f g : N →ₗ[R] P), LinearMap.rTensor Q (f - g) = LinearMap.rTensor Q f - LinearMap.rTensor Q g
-- Mathlib.Topology.Algebra.Support
image_eq_one_of_notMem_mulTSupport : ∀ {X : Type u_1} {α : Type u_2} [inst : One α] [inst_1 : TopologicalSpace X] {f : X → α} {x : X},
  x ∉ mulTSupport f → f x = 1
-- Mathlib.CategoryTheory.Limits.Preorder
Preorder.instHasBinaryCoproducts : ∀ {C : Type u} [inst : SemilatticeSup C], CategoryTheory.Limits.HasBinaryCoproducts C
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.Embedding.r_eq_some : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') {i : ι} {i' : ι'},
  e.f i = i' → e.r i' = some i
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.ReflectsColimitsOfSize.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  autoParam
      (∀ {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J], CategoryTheory.Limits.ReflectsColimitsOfShape J F)
      CategoryTheory.Limits.ReflectsColimitsOfSize.reflectsColimitsOfShape._autoParam →
    CategoryTheory.Limits.ReflectsColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F
-- Lean.Language.Basic
/-- Returns the original snapshot value if it is of the given type.  -/
Lean.Language.DynamicSnapshot.toTyped? : (α : Type) → [TypeName α] → Lean.Language.DynamicSnapshot → Option α
-- Mathlib.NumberTheory.ADEInequality
/-- `D' r := {2,2,r}` is a `Multiset ℕ+`
that is a solution to the inequality
`(p⁻¹ + q⁻¹ + r⁻¹ : ℚ) > 1`.

These solutions are related to the Dynkin diagrams $D_{r+2}$.  -/
ADEInequality.D' : ℕ+ → Multiset ℕ+
-- Mathlib.Data.FunLike.Group
FunLike.cancelMonoid.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Mul F] [inst_2 : One F]
  [inst_3 : Pow F ℕ] [inst_4 : CancelMonoid β] [inst_5 : IsOneApply F α β] [inst_6 : IsMulApply F α β]
  [inst_7 : IsPowApply ℕ F α β], FunLike.cancelMonoid = Function.Injective.cancelMonoid (fun f => ⇑f) ⋯ ⋯ ⋯ ⋯
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.HasNoetherianRange.sub : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : Ring K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] {f g : V →ₗ[K] V₂},
  f.HasNoetherianRange → g.HasNoetherianRange → (f - g).HasNoetherianRange
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.map_one : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)], (PiTensorProduct.map fun i => 1) = 1
-- Mathlib.Topology.Order.OrderClosed
continuousWithinAt_Ioc_iff_Ioi : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α]
  [inst_3 : TopologicalSpace β] {a b : α} {f : α → β},
  b < a → (ContinuousWithinAt f (Set.Ioc b a) b ↔ ContinuousWithinAt f (Set.Ioi b) b)
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.instNormalAddSubgroup : ∀ {G : Type u_1} [inst : AddGroup G] (c : AddCon G), c.addSubgroup.Normal
-- Mathlib.GroupTheory.Index
AddSubgroup.finiteIndex_of_finite_quotient : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} [Finite (G ⧸ H)], H.FiniteIndex