mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
Algebra.Generators.compLocalizationAwayAlgHom_X_inl : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (g : S) [inst_7 : IsLocalization.Away g T] (P : Algebra.Generators R S ι),
  (Algebra.Generators.compLocalizationAwayAlgHom T g P) (MvPolynomial.X (Sum.inl ())) =
    IsLocalization.Away.invSelf ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g))
-- Mathlib.Algebra.BigOperators.GroupWithZero.Action
smul_finprod_perm : ∀ {N : Type u_2} [inst : CommMonoid N] {G : Type u_4} [inst_1 : Group G] [inst_2 : MulDistribMulAction G N] [Finite G]
  (b : N) (g : G), g • ∏ᶠ (h : G), h • b = ∏ᶠ (h : G), h • b
-- Aesop.Frontend.Basic
Aesop.Frontend.Parser.bool_litFalse : Lean.ParserDescr
-- Mathlib.Data.Seq.Basic
Stream'.Seq.all_cons : ∀ {α : Type u} {p : α → Prop} {hd : α} {tl : Stream'.Seq α}, p hd → (∀ x ∈ tl, p x) → ∀ x ∈ Stream'.Seq.cons hd tl, p x
-- Mathlib.AlgebraicTopology.DoldKan.Degeneracies
AlgebraicTopology.DoldKan.degeneraciesVanish_zero_iff_true : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} {T : C} (f : X.obj (Opposite.op { len := 0 }) ⟶ T),
  AlgebraicTopology.DoldKan.DegeneraciesVanish f ↔ True
-- Mathlib.Analysis.InnerProductSpace.GramMatrix
Matrix.gram_zero : ∀ {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E], Matrix.gram 𝕜 0 = 0
-- Aesop.RuleSet
Aesop.LocalRuleSet.applicableNormalizationRulesWith : Aesop.LocalRuleSet →
  Aesop.ForwardRuleMatches →
    Lean.MVarId → (Aesop.NormRule → Bool) → Aesop.BaseM (Array (Aesop.IndexMatchResult Aesop.NormRule))
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.rootSet_C : ∀ {S : Type v} {T : Type w} [inst : CommRing T] [inst_1 : CommRing S] [inst_2 : IsDomain S] [inst_3 : Algebra T S]
  (a : T), (Polynomial.C a).rootSet S = ∅
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.ofBijective.eq_1 : ∀ {M : Type u_9} {N : Type u_10} {F : Type u_11} [inst : Add M] [inst_1 : Add N] [inst_2 : FunLike F M N]
  [inst_3 : AddHomClass F M N] (f : F) (hf : Function.Bijective ⇑f),
  AddEquiv.ofBijective f hf = { toEquiv := Equiv.ofBijective (⇑f) hf, map_add' := ⋯ }
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Valuation.hasBasis_uniformity : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [_u : UniformSpace R] [IsUniformAddGroup R] [IsValuativeTopology R] (v : Valuation R Γ₀) [v.Compatible],
  (uniformity R).HasBasis (fun x => True) fun γ => {p | v.restrict (p.2 - p.1) < ↑γ}
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.hom_hom_comp : ∀ {X Y Z : NonemptyFinLinOrd} (f : X ⟶ Y) (g : Y ⟶ Z),
  LinOrd.Hom.hom (CategoryTheory.CategoryStruct.comp f g).hom = (LinOrd.Hom.hom g.hom).comp (LinOrd.Hom.hom f.hom)
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
CategoryTheory.Functor.shift_map_op_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.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ] {X Y : C} (f : X ⟶ Y)
  (n : ℤ) {Z : Dᵒᵖ} (h : (CategoryTheory.shiftFunctor Dᵒᵖ n).obj (Opposite.op (F.obj X)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor Dᵒᵖ n).map (F.map f).op) h =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F.op n).inv.app (Opposite.op Y))
      (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor Cᵒᵖ n).map f.op).unop).op
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F.op n).hom.app (Opposite.op X)) h))
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.checkColGe.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.Normed.Lp.LpEquiv
coe_ringEquiv_lpBCF_symm : ∀ {α : Type u_1} {R : Type u_3} [inst : TopologicalSpace α] [inst_1 : DiscreteTopology α]
  [inst_2 : NonUnitalNormedRing R] (f : BoundedContinuousFunction α R), ↑(RingEquiv.lpBCF.symm f) = ⇑f
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.toContinuousLinearEquiv_inv : ∀ {R : Type u_1} {E : Type u_5} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module R E]
  (e : E ≃ₗᵢ[R] E), ↑e⁻¹ = (↑e)⁻¹
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k a : α} {v : β}, (m.insert k v).getKey! a = if (k == a) = true then k else m.getKey! a
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.approx.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : SemilatticeSup β] [inst_2 : OrderBot β]
  [inst_3 : Zero β] (i : ℕ → β) (f : α → β) (n : ℕ),
  MeasureTheory.SimpleFunc.approx i f n =
    (Finset.range n).sup fun k => (MeasureTheory.SimpleFunc.const α (i k)).restrict {a | i k ≤ f a}
-- Mathlib.CategoryTheory.Adjunction.Comma
/-- If each structured arrow category on `G` has an initial object, `G` is a right adjoint.  -/
CategoryTheory.isRightAdjointOfStructuredArrowInitials : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor D C) [∀ (A : C), CategoryTheory.Limits.HasInitial (CategoryTheory.StructuredArrow A G)],
  G.IsRightAdjoint
-- Mathlib.Algebra.Lie.Abelian
LieModule.isTrivial_iff_max_triv_eq_top : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M],
  LieModule.IsTrivial L M ↔ LieModule.maxTrivSubmodule R L M = ⊤
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.instIsZeroApplyUpperHalfPlaneComplex : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ}, IsZeroApply (CuspForm Γ k) UpperHalfPlane ℂ
-- Mathlib.Order.RelClasses
wellFounded_gt : ∀ {α : Type u} [inst : LT α] [WellFoundedGT α], WellFounded fun x1 x2 => x2 < x1
-- Std.Do.SPred.Laws
Std.Do.SPred.entails.eq_def : ∀ {σs : List (Type u)} (P Q : Std.Do.SPred σs),
  (P ⊢ₛ Q) =
    match σs, P, Q with
    | [], P, Q => P.down → Q.down
    | σ :: tail, P, Q => ∀ (s : σ), P s ⊢ₛ Q s
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} {k k' : α}
  [hi : Inhabited β] {f : β → β},
  Std.DTreeMap.Const.get! (Std.DTreeMap.Const.modify t k f) k' =
    if cmp k k' = Ordering.eq then (Option.map f (Std.DTreeMap.Const.get? t k)).get! else Std.DTreeMap.Const.get! t k'
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.toLinearEquiv_lidIsometry : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  (TensorProduct.lidIsometry 𝕜 E).toLinearEquiv = TensorProduct.lid 𝕜 E
-- Lean.Elab.MutualDef
Lean.Elab.DefViewElabHeader.mk.inj : ∀ {toDefView : Lean.Elab.DefView} {toDefViewElabHeaderData : Lean.Elab.DefViewElabHeaderData}
  {tacSnap? : Option (Lean.Language.SnapshotBundle Lean.Elab.Tactic.TacticParsedSnapshot)}
  {bodySnap? : Option (Lean.Language.SnapshotBundle (Option Lean.Elab.BodyProcessedSnapshot))}
  {toDefView_1 : Lean.Elab.DefView} {toDefViewElabHeaderData_1 : Lean.Elab.DefViewElabHeaderData}
  {tacSnap?_1 : Option (Lean.Language.SnapshotBundle Lean.Elab.Tactic.TacticParsedSnapshot)}
  {bodySnap?_1 : Option (Lean.Language.SnapshotBundle (Option Lean.Elab.BodyProcessedSnapshot))},
  { toDefView := toDefView, toDefViewElabHeaderData := toDefViewElabHeaderData, tacSnap? := tacSnap?,
        bodySnap? := bodySnap? } =
      { toDefView := toDefView_1, toDefViewElabHeaderData := toDefViewElabHeaderData_1, tacSnap? := tacSnap?_1,
        bodySnap? := bodySnap?_1 } →
    toDefView = toDefView_1 ∧
      toDefViewElabHeaderData = toDefViewElabHeaderData_1 ∧ tacSnap? = tacSnap?_1 ∧ bodySnap? = bodySnap?_1
-- Batteries.Data.MLList.Basic
/-- Repeatedly apply a function `f : α → m (α × List β)` to an initial `a : α`,
accumulating the elements of the resulting `List β` as a single monadic lazy list.  -/
MLList.fixl : {m : Type u → Type u} → [Monad m] → {α β : Type u} → (α → m (α × List β)) → α → MLList m β
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxEntryD_eq_getD_maxEntry? : ∀ {α : Type u} {β : α → Type v} {l : Std.DTreeMap.Internal.Impl α β} {fallback : (a : α) × β a},
  l.maxEntryD fallback = l.maxEntry?.getD fallback
-- Mathlib.Data.Nat.BitIndices
/-- The function which maps each natural number `∑ i ∈ s, 2 ^ i` to the list of
elements of `s` in increasing order.  -/
Nat.bitIndices : ℕ → List ℕ
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.mk_symm : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} {e : V ≃L[R] W}
  (he : ∀ (g : G), ↑e ∘SL ρ g = σ g ∘SL ↑e),
  (ContRepresentation.Equiv.mk e he).symm = ContRepresentation.Equiv.mk e.symm ⋯
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_filterMap_iff : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → β → Option γ},
  t.WF → ((Std.TreeMap.Raw.filterMap f t).isEmpty = true ↔ ∀ (k : α) (h : k ∈ t), f (t.getKey k h) t[k] = none)
-- Mathlib.Algebra.Homology.ExactSequenceFour
CategoryTheory.ComposableArrows.IsComplex.cokerToKer_fac_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.IsComplex) (k : ℕ)
  (hk : autoParam (k ≤ n) CategoryTheory.ComposableArrows.IsComplex.cokerToKer_fac._auto_1)
  [inst_2 : CategoryTheory.Limits.HasCokernel (S.map' k (k + 1) ⋯ ⋯)]
  [inst_3 : CategoryTheory.Limits.HasKernel (S.map' (k + 2) (k + 3) ⋯ ⋯)] {Z : C} (h : S.obj ⟨k + 2, ⋯⟩ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (S.map' k (k + 1) ⋯ ⋯))
      (CategoryTheory.CategoryStruct.comp (hS.cokerToKer k hk)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (S.map' (k + 2) (k + 3) ⋯ ⋯)) h)) =
    CategoryTheory.CategoryStruct.comp (S.map' (k + 1) (k + 2) ⋯ ⋯) h
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.zmodRepr_eq_zero_of_dvd : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] {x : ℤ_[p]}, ↑p ∣ x → x.zmodRepr = 0
-- Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
CategoryTheory.Presieve.EffectiveEpimorphic.isSheafFor_of_isRepresentable : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {R : CategoryTheory.Presieve X},
  R.EffectiveEpimorphic →
    ∀ (F : CategoryTheory.Functor Cᵒᵖ (Type w)) [F.IsRepresentable], CategoryTheory.Presieve.IsSheafFor F R
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.coord_apply_eq : ∀ {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) (i : ι), (b.coord i) (b i) = 1
-- Lean.Widget.TaggedText
Lean.Widget.instInhabitedTaggedText : {a : Type u_1} → Inhabited (Lean.Widget.TaggedText a)
-- Mathlib.LinearAlgebra.Matrix.Unique
Matrix.uniqueAlgEquiv_apply : ∀ {m : Type u_1} {A : Type u_3} {R : Type u_4} [inst : Unique m] [inst_1 : Semiring A] [inst_2 : CommSemiring R]
  [inst_3 : Algebra R A] (M : Matrix m m A), Matrix.uniqueAlgEquiv M = M default default
-- Mathlib.Lean.Meta.Simp
/-- Tests whether `decl` has `simp`-attribute `simpAttr`. Returns `false` is `simpAttr` is not a
valid simp-attribute.  -/
Lean.Meta.isInSimpSet : Lean.Name → Lean.Name → Lean.CoreM Bool
-- Mathlib.RingTheory.Length
Module.length_le_of_surjective : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {P : Type u_4}
  [inst_3 : AddCommGroup P] [inst_4 : Module R P] (g : M →ₗ[R] P),
  Function.Surjective ⇑g → Module.length R P ≤ Module.length R M
-- Mathlib.Topology.MetricSpace.Cover
/-- **Alias** of the reverse direction of `Metric.isCover_iff_subset_cthickening`. -/
Metric.IsCover.of_subset_cthickening : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {ε : NNReal} {s N : Set X} [ProperSpace X],
  IsClosed N → s ⊆ Metric.cthickening (↑ε) N → Metric.IsCover ε s N
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_Ioi_of_Ioi : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [OrderClosedTopology α] [OpensMeasurableSpace α] {a : ι → α}
  {A : α}, Filter.Tendsto a l (nhds A) → MeasureTheory.AECover (μ.restrict (Set.Ioi A)) l fun i => Set.Ioi (a i)
-- Aesop.Options.Public
Aesop.instBEqOptions : BEq Aesop.Options
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.lid_eq_rid : ∀ (R : Type u_1) [inst : CommSemiring R], TensorProduct.lid R R = TensorProduct.rid R R
-- Mathlib.Data.Bool.Basic
Bool.coe_xor_iff : ∀ (a b : Bool), (a ^^ b) = true ↔ Xor (a = true) (b = true)
-- Mathlib.Analysis.RCLike.Extend
StrongDual.extendRCLike.congr_simp : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {F : Type u_2} [inst_1 : TopologicalSpace F] [inst_2 : AddCommGroup F]
  [inst_3 : Module 𝕜 F] [inst_4 : ContinuousConstSMul 𝕜 F] [inst_5 : Module ℝ F] [inst_6 : IsScalarTower ℝ 𝕜 F]
  (fr fr_1 : StrongDual ℝ F), fr = fr_1 → fr.extendRCLike = fr_1.extendRCLike
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.union_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ m₃ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m₁.Equiv m₂ → (m₁ ∪ m₃).Equiv (m₂ ∪ m₃)
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
HomotopicalAlgebra.CofibrantBrownFactorization.s_p : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  {f : X ⟶ Y} (self : HomotopicalAlgebra.CofibrantBrownFactorization f),
  CategoryTheory.CategoryStruct.comp self.s self.p = CategoryTheory.CategoryStruct.id Y
-- Mathlib.Analysis.Normed.Group.Constructions
OrderDual.seminormedGroup.eq_1 : ∀ {E : Type u_2} [inst : SeminormedGroup E],
  OrderDual.seminormedGroup =
    { toNorm := OrderDual.toNorm, toGroup := OrderDual.instGroup, toPseudoMetricSpace := instPseudoMetricSpaceOrderDual,
      dist_eq := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- Associativity of the enriched structure  -/
CategoryTheory.MonoidalClosed.assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (w x y z : C)
  [inst_2 : CategoryTheory.Closed w] [inst_3 : CategoryTheory.Closed x] [inst_4 : CategoryTheory.Closed y],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (w ⟹ x) (x ⟹ y) (y ⟹ z)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalClosed.comp w x y) (y ⟹ z))
        (CategoryTheory.MonoidalClosed.comp w y z)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (w ⟹ x) (CategoryTheory.MonoidalClosed.comp x y z))
      (CategoryTheory.MonoidalClosed.comp w x z)
-- Mathlib.Geometry.Convex.Cone.Pointed
/-- Constructs an ordered module given an ordered group, a cone, and a proof that
the order relation is the one defined by the cone.  -/
PointedCone.to_isOrderedModule : ∀ {R : Type u_1} {E : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup E] [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module R E]
  (C : PointedCone R E), (∀ (x y : E), x ≤ y ↔ y - x ∈ C) → IsOrderedModule R E
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- Measurable equivalence between `Π j : Fin (n + 1), α j` and
`α i × Π j : Fin n, α (Fin.succAbove i j)`.

Measurable version of `Fin.insertNthEquiv`.  -/
MeasurableEquiv.piFinSuccAbove : {n : ℕ} →
  (α : Fin (n + 1) → Type u_8) →
    [inst : (i : Fin (n + 1)) → MeasurableSpace (α i)] →
      (i : Fin (n + 1)) → ((j : Fin (n + 1)) → α j) ≃ᵐ α i × ((j : Fin n) → α (i.succAbove j))
-- Mathlib.Order.Interval.Finset.Defs
Finset.subtype_Ioo_eq : ∀ {α : Type u_1} [inst : Preorder α] (p : α → Prop) [inst_1 : DecidablePred p] [inst_2 : LocallyFiniteOrder α]
  (a b : Subtype p), Finset.Ioo a b = Finset.subtype p (Finset.Ioo ↑a ↑b)
-- Mathlib.CategoryTheory.Sites.CompatiblePlus
CategoryTheory.GrothendieckTopology.plusCompIso_whiskerRight_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  (F : CategoryTheory.Functor D E)
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 :
    ∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_7 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E]
  [inst_8 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F]
  {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) {Z : CategoryTheory.Functor Cᵒᵖ E} (h : J.plusObj (Q.comp F) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (J.plusMap η) F)
      (CategoryTheory.CategoryStruct.comp (J.plusCompIso F Q).hom h) =
    CategoryTheory.CategoryStruct.comp (J.plusCompIso F P).hom
      (CategoryTheory.CategoryStruct.comp (J.plusMap (CategoryTheory.Functor.whiskerRight η F)) h)
-- Mathlib.Order.OmegaCompletePartialOrder
/-- The `ωSup` operator for continuous functions, which takes the pointwise countable supremum
of the functions in the `ω`-chain.  -/
OmegaCompletePartialOrder.ContinuousHom.ωSup : {α : Type u_2} →
  {β : Type u_3} →
    [inst : OmegaCompletePartialOrder α] →
      [inst_1 : OmegaCompletePartialOrder β] → OmegaCompletePartialOrder.Chain (α →𝒄 β) → α →𝒄 β
-- Mathlib.Data.Stream.Init
Stream'.tail_const : ∀ {α : Type u} (a : α), (Stream'.const a).tail = Stream'.const a
-- Init.Data.Int.ToString
Int.toString_eq_repr : ∀ {a : ℤ}, toString a = a.repr
-- Mathlib.Analysis.Distribution.TemperateGrowth
Function.RCLike.hasTemperateGrowth_ofReal : ∀ (𝕜 : Type u_2) [inst : RCLike 𝕜], Function.HasTemperateGrowth RCLike.ofReal
-- Mathlib.Data.PFun
PFun.restrict.congr_simp : ∀ {α : Type u_1} {β : Type u_2} (f f_1 : α →. β) (e_f : f = f_1) {p p_1 : Set α} (e_p : p = p_1) (H : p ⊆ f.Dom)
  (a a_1 : α), a = a_1 → f.restrict H a = f_1.restrict ⋯ a_1
-- Lean.Parser.Command
Lean.Parser.Command.inductive.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.symm.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (f : α ≃+o β), f.symm = { toAddEquiv := f.symm, map_le_map_iff' := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Real.differentiableAt_tan_of_mem_Ioo : ∀ {x : ℝ}, x ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2) → DifferentiableAt ℝ Real.tan x
-- Mathlib.NumberTheory.ClassNumber.Finite
ClassGroup.prod_finsetApprox_ne_zero : ∀ {R : Type u_1} {S : Type u_2} [inst : EuclideanDomain R] [inst_1 : CommRing S] [inst_2 : IsDomain S]
  [inst_3 : Algebra R S] {abv : AbsoluteValue R ℤ} {ι : Type u_5} [inst_4 : DecidableEq ι] [inst_5 : Fintype ι]
  (bS : Module.Basis ι R S) (adm : abv.IsAdmissible) [inst_6 : Infinite R] [inst_7 : DecidableEq R],
  (algebraMap R S) (∏ m ∈ ClassGroup.finsetApprox bS adm, m) ≠ 0
-- Std.Sync.Semaphore
_private.Std.Sync.Semaphore.0.Std.Semaphore.mk.sizeOf_spec : ∀ (lock : Std.Mutex Std.SemaphoreState✝), sizeOf { lock := lock } = 1 + sizeOf lock
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.add_coeffs : ∀ {l₁ l₂ : Lean.Omega.LinearCombo}, (l₁ + l₂).coeffs = l₁.coeffs + l₂.coeffs
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.div_tendsto_atBot_zero_of_degree_lt : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜)
  [OrderTopology 𝕜],
  P.degree < Q.degree → Filter.Tendsto (fun x => Polynomial.eval x P / Polynomial.eval x Q) Filter.atBot (nhds 0)
-- Mathlib.LinearAlgebra.Basis.VectorSpace
Module.Basis.range_extendLe : ∀ {K : Type u_3} {V : Type u_4} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s t : Set V}
  (hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ Submodule.span K t),
  Set.range ⇑(Module.Basis.extendLe hs hst ht) = hs.extend hst
-- Lean.Elab.Tactic.Omega.Frontend
/-- Facts which have already been processed; we keep these to avoid duplicates.  -/
Lean.Elab.Tactic.Omega.MetaProblem.processedFacts : Lean.Elab.Tactic.Omega.MetaProblem → Std.HashSet Lean.Expr
-- Mathlib.NumberTheory.LSeries.RiemannZeta
/-- The Riemann zeta function agrees with the naive Dirichlet-series definition when the latter
converges. (Note that this is false without the assumption: when `re s ≤ 1` the sum is divergent,
and we use a different definition to obtain the analytic continuation to all `s`.)  -/
zeta_eq_tsum_one_div_nat_cpow : ∀ {s : ℂ}, 1 < s.re → riemannZeta s = ∑' (n : ℕ), 1 / ↑n ^ s
-- Mathlib.Algebra.Order.Module.Defs
PosSMulMono.mk : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero α],
  (∀ ⦃a : α⦄, 0 ≤ a → ∀ ⦃b₁ b₂ : β⦄, b₁ ≤ b₂ → a • b₁ ≤ a • b₂) → PosSMulMono α β
-- Aesop.Tree.State
Aesop.MVarCluster.isUnprovableNoCache : Aesop.MVarCluster → BaseIO Bool
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_emptyWithCapacity : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {a : α} {fallback : β} {c : ℕ},
  Std.DHashMap.Internal.Raw₀.Const.getD (Std.DHashMap.Internal.Raw₀.emptyWithCapacity c) a fallback = fallback
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.Ico_add_one_right_eq_Icc_of_not_isMax : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Add α] [SuccAddOrder α] {b : α},
  ¬IsMax b → ∀ (a : α), Set.Ico a (b + 1) = Set.Icc a b
-- Mathlib.RingTheory.RootsOfUnity.Basic
/-- The group of group homomorphisms from a finite cyclic group `G` of order `n` into another
group `G'` is (noncanonically) isomorphic to the group of `n`th roots of unity in `G'`.  -/
IsCyclic.monoidHom_mulEquiv_rootsOfUnity : ∀ (G : Type u_7) [inst : CommGroup G] [IsCyclic G] (G' : Type u_8) [inst_2 : CommGroup G'],
  Nonempty ((G →* G') ≃* ↥(rootsOfUnity (Nat.card G) G'))
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.liftAlgHom_eq_algHom : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] (f : Polynomial R) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (ϕ : AdjoinRoot f →ₐ[R] S), AdjoinRoot.liftAlgHom f (Algebra.ofId R S) (ϕ (AdjoinRoot.root f)) ⋯ = ϕ