mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Function.Bijective.mulActionHom_embedding_isBijective : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {H : Type u_3} {β : Type u_4}
  [inst_2 : Group H] [inst_3 : MulAction H β] {σ : G → H} {f : α →ₑ[σ] β} {ι : Type u_5} (hf : Function.Bijective ⇑f),
  Function.Bijective ⇑(Function.Injective.mulActionHom_embedding ι ⋯)
-- Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
/-- If a complete normed ring `R` acts continuously differentiably on a manifold `M`, its
submanifold of units does as well.  -/
Units.contMDiffSMul : ∀ {R : Type u_1} [inst : NormedRing R] [inst_1 : CompleteSpace R] {n : WithTop ℕ∞} {𝕜 : Type u_2}
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedAlgebra 𝕜 R] {H : Type u_3} [inst_4 : TopologicalSpace H]
  {E : Type u_4} [inst_5 : NormedAddCommGroup E] [inst_6 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_5}
  [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M] [inst_9 : MulAction R M]
  [ContMDiffSMul (modelWithCornersSelf 𝕜 R) I n R M], ContMDiffSMul (modelWithCornersSelf 𝕜 R) I n Rˣ M
-- Init.Control.MonadAttach
/-- This type class ensures that `MonadAttach.CanReturn` is the unique strongest possible
postcondition.
 -/
LawfulMonadAttach : (m : Type u → Type v) → [Monad m] → [MonadAttach m] → Prop
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.debug.tactic.simp.checkDefEqAttr : Lean.Option Bool
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
/-- Formula for geometric series.  -/
MvPowerSeries.WithPiTopology.one_sub_mul_tsum_pow_of_constantCoeff_eq_zero : ∀ {σ : Type u_1} {R : Type u_4} [inst : TopologicalSpace R] [inst_1 : Ring R] [IsTopologicalRing R] [T2Space R]
  {f : MvPowerSeries σ R}, MvPowerSeries.constantCoeff f = 0 → (1 - f) * ∑' (i : ℕ), f ^ i = 1
-- Mathlib.MeasureTheory.Integral.CircleTransform
Complex.norm_circleTransformBoundingFunction_le : ∀ {R r : ℝ},
  r < R →
    0 ≤ r →
      ∀ (z : ℂ),
        ∃ x,
          ∀ (y : ↑(Metric.closedBall z r ×ˢ Set.uIcc 0 (2 * Real.pi))),
            ‖Complex.circleTransformBoundingFunction R z ↑y‖ ≤ ‖Complex.circleTransformBoundingFunction R z ↑x‖
-- Mathlib.Order.UpperLower.Prod
/-- The product of two lower sets as a lower set.  -/
LowerSet.prod : {α : Type u_1} →
  {β : Type u_2} → [inst : Preorder α] → [inst_1 : Preorder β] → LowerSet α → LowerSet β → LowerSet (α × β)
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
HomotopicalAlgebra.Precylinder.LeftHomotopy.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {P : HomotopicalAlgebra.Precylinder X} {Y : C}
  {f g : X ⟶ Y} [inst_1 : SizeOf C] (h : P.I ⟶ Y)
  (h₀ :
    autoParam (CategoryTheory.CategoryStruct.comp P.i₀ h = f) HomotopicalAlgebra.Precylinder.LeftHomotopy.h₀._autoParam)
  (h₁ :
    autoParam (CategoryTheory.CategoryStruct.comp P.i₁ h = g)
      HomotopicalAlgebra.Precylinder.LeftHomotopy.h₁._autoParam),
  sizeOf { h := h, h₀ := h₀, h₁ := h₁ } = 1 + sizeOf h + sizeOf h₀ + sizeOf h₁
-- Aesop.RuleSet.Member
Aesop.BaseRuleSetMember.unfoldRule.sizeOf_spec : ∀ (r : Aesop.UnfoldRule), sizeOf (Aesop.BaseRuleSetMember.unfoldRule r) = 1 + sizeOf r
-- Mathlib.LinearAlgebra.Matrix.Symmetric
Matrix.IsSymm.add : ∀ {α : Type u_1} {n : Type u_3} {A B : Matrix n n α} [inst : Add α], A.IsSymm → B.IsSymm → (A + B).IsSymm
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
/-- Part of an `sl₂` triple used in Geck's construction of a Lie algebra from a root system.  -/
RootPairing.GeckConstruction.f : {ι : 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} →
                    [P.IsCrystallographic] →
                      {b : P.Base} →
                        [Finite ι] →
                          [IsDomain R] → [CharZero R] → ↥b.support → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.getElem_toArray_eq : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxi.IsAlwaysFinite α] {r : Std.Roi α} {i : ℕ} {h : i < r.toArray.size},
  r.toArray[i] = (Std.PRange.succMany? (i + 1) r.lower).get ⋯
-- Mathlib.CategoryTheory.Sites.Subcanonical
/-- Variant of `uliftYonedaEquiv_naturality` with general `g`. This is technically strictly more
general than `uliftYonedaEquiv_naturality`, but `uliftYonedaEquiv_naturality` is sometimes
preferable because it can avoid the "motive is not type correct" error.  -/
CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_naturality' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] {X Y : Cᵒᵖ} {F : CategoryTheory.Sheaf J (Type (max v v'))}
  (f : (CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).obj (Opposite.unop X) ⟶ F) (g : X ⟶ Y),
  (CategoryTheory.ConcreteCategory.hom (F.obj.map g)) (J.uliftYonedaEquiv f) =
    J.uliftYonedaEquiv
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).map g.unop) f)
-- Mathlib.Logic.Nontrivial.Defs
not_nontrivial : ∀ (α : Type u_3) [Subsingleton α], ¬Nontrivial α
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.TZifV2.mk.inj : ∀ {toTZifV1 : Std.Time.TimeZone.TZif.TZifV1} {footer : Option String} {toTZifV1_1 : Std.Time.TimeZone.TZif.TZifV1}
  {footer_1 : Option String},
  { toTZifV1 := toTZifV1, footer := footer } = { toTZifV1 := toTZifV1_1, footer := footer_1 } →
    toTZifV1 = toTZifV1_1 ∧ footer = footer_1
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntry_eq_getEntry? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (l : Std.DTreeMap.Internal.Impl α β) {h : k ∈ l},
  some (l.getEntry k h) = l.getEntry? k
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_le_ofReal : ∀ {p q : ℝ}, p ≤ q → ENNReal.ofReal p ≤ ENNReal.ofReal q
-- Lean.Server.Requests
Lean.Server.ServerRequestResponse.failure.injEq : ∀ {α : Type} (code : Lean.JsonRpc.ErrorCode) (message : String) (code_1 : Lean.JsonRpc.ErrorCode) (message_1 : String),
  (Lean.Server.ServerRequestResponse.failure code message =
      Lean.Server.ServerRequestResponse.failure code_1 message_1) =
    (code = code_1 ∧ message = message_1)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.unitOfList_nil : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α], Std.HashMap.Raw.unitOfList [] = ∅
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- To construct a morphism of costructured arrows,
we need a morphism of the objects underlying the source,
and to check that the triangle commutes.
 -/
CategoryTheory.CostructuredArrow.homMk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {T : D} →
          {S : CategoryTheory.Functor C D} →
            {f f' : CategoryTheory.CostructuredArrow S T} →
              (g : f.left ⟶ f'.left) →
                autoParam (CategoryTheory.CategoryStruct.comp (S.map g) f'.hom = f.hom)
                    CategoryTheory.CostructuredArrow.homMk._auto_1 →
                  (f ⟶ f')
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_inv_hom_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] (x : C) {y z : D} (f : y ≅ z) {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj x z ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight x f.inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight x f.hom) h) =
    h
-- Init.Data.Int.Linear
Int.Internal.Linear.le_norm_poly : ∀ (ctx : Int.Internal.Linear.Context) (p p' : Int.Internal.Linear.Poly),
  Int.Internal.Linear.Poly.denote' ctx p = Int.Internal.Linear.Poly.denote' ctx p' →
    Int.Internal.Linear.Poly.denote' ctx p ≤ 0 → Int.Internal.Linear.Poly.denote' ctx p' ≤ 0
-- Mathlib.Data.List.Sublists
List.revzip_sublists : ∀ {α : Type u} (l l₁ l₂ : List α), (l₁, l₂) ∈ l.sublists.revzip → (l₁ ++ l₂).Perm l
-- Mathlib.Analysis.Convex.Star
starConvex_univ : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] (x : E), StarConvex 𝕜 x Set.univ
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_sub_natCast : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R) (n : ℕ),
  Int.fract (a - ↑n) = Int.fract a
-- Mathlib.Algebra.GroupWithZero.Semiconj
SemiconjBy.zpow_right₀ : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {a x y : G₀}, SemiconjBy a x y → ∀ (m : ℤ), SemiconjBy a (x ^ m) (y ^ m)
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
CategoryTheory.uliftFunctor.eq_1 : CategoryTheory.uliftFunctor.{v, u} =
  { obj := fun X => ULift.{v, u} X,
    map := fun {X x} f => TypeCat.ofHom fun x_1 => { down := (CategoryTheory.ConcreteCategory.hom f) x_1.down },
    map_id := CategoryTheory.uliftFunctor._proof_1, map_comp := @CategoryTheory.uliftFunctor._proof_2 }
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.rootSystem.congr_simp : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] (H : LieSubalgebra K L)
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L],
  LieAlgebra.IsKilling.rootSystem H = LieAlgebra.IsKilling.rootSystem H
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestMatchAtChain.cons : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  (startPos middlePos endPos : s.Pos),
  String.Slice.Pattern.Model.IsLongestMatchAt pat startPos middlePos →
    String.Slice.Pattern.Model.IsLongestMatchAtChain pat middlePos endPos →
      String.Slice.Pattern.Model.IsLongestMatchAtChain pat startPos endPos
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.invFun_eq_symm : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] {f : M ≃ₜ* N}, f.invFun = ⇑f.symm
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.instAlgebraCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecPresheafOpOpens : {R : CommRingCat} →
  {U : (AlgebraicGeometry.Spec R).Opens} → Algebra ↑R ↑((AlgebraicGeometry.Spec R).presheaf.obj (Opposite.op U))
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.orderTop_zero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R], HahnSeries.orderTop 0 = ⊤
-- Mathlib.Order.Partition.Basic
Partition.mem_iff_unique : ∀ {α : Type u_1} {x : α} {u : Set α} {P : Partition u}, x ∈ u ↔ ∃! t, t ∈ P ∧ x ∈ t
-- Init.Tactics
/-- `with_annotate_state stx t` annotates the lexical range of `stx : Syntax` with
the initial and final state of running tactic `t`.
 -/
Lean.Parser.Tactic.withAnnotateState : Lean.ParserDescr
-- Mathlib.Algebra.Order.Monoid.Defs
/-- An ordered monoid is a monoid with a preorder such that multiplication is monotone.  -/
IsOrderedMonoid : (α : Type u_2) → [CommMonoid α] → [Preorder α] → Prop
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.ker_map : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] (N : Subgroup G) [nN : N.Normal] (M : Subgroup H)
  [inst_2 : M.Normal] (f : G →* H) (h : N ≤ Subgroup.comap f M),
  (QuotientGroup.map N M f h).ker = Subgroup.map (QuotientGroup.mk' N) (Subgroup.comap f M)
-- Aesop.Search.Expansion
Aesop.SafeRuleResult.postponed.sizeOf_spec : ∀ (result : Aesop.PostponedSafeRule), sizeOf (Aesop.SafeRuleResult.postponed result) = 1 + sizeOf result
-- Init.Data.Slice.Array.Lemmas
Array.toArray_mkSlice_rii : ∀ {α : Type u_1} {xs : Array α}, Std.Slice.toArray (Std.Rii.Sliceable.mkSlice xs *...*) = xs
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- The property that a morphism property `W` is stable under colimits
indexed by a category `J`.  -/
CategoryTheory.MorphismProperty.IsStableUnderColimitsOfShape : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.MorphismProperty C → (J : Type u_1) → [CategoryTheory.Category.{v_1, u_1} J] → Prop
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableAt.add : ∀ {𝕜 : 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'] {z : M} {f g : M → E'}, MDiffAt f z → MDiffAt g z → MDiffAt (f + g) z
-- Mathlib.Order.Directed
exists_le_le : ∀ {α : Type u_1} [inst : LE α] [IsCodirectedOrder α] (a b : α), ∃ c ≤ a, c ≤ b
-- Mathlib.Algebra.Order.GroupWithZero.Basic
le_mul_of_one_le_right : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Zero α] {a b : α} [inst_2 : Preorder α] [PosMulMono α],
  0 ≤ a → 1 ≤ b → a ≤ a * b
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
/-- The image of `IsFractionRing.liftAlgHom` is the intermediate field generated by `s`,
if the image of the algebra hom is the subalgebra generated by `s`.  -/
IsFractionRing.liftAlgHom_fieldRange_eq_of_range_eq : ∀ {F : Type u_1} {A : Type u_2} {K : Type u_3} {L : Type u_4} [inst : Field F] [inst_1 : CommRing A]
  [inst_2 : Algebra F A] [inst_3 : Field K] [inst_4 : Algebra F K] [inst_5 : Algebra A K] [inst_6 : IsFractionRing A K]
  [inst_7 : Field L] [inst_8 : Algebra F L] {g : A →ₐ[F] L} [inst_9 : IsScalarTower F A K] (hg : Function.Injective ⇑g)
  {s : Set L}, g.range = Algebra.adjoin F s → (IsFractionRing.liftAlgHom hg).fieldRange = IntermediateField.adjoin F s
-- Mathlib.Analysis.Normed.Group.Pointwise
neg_ball : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x : E), -Metric.ball x δ = Metric.ball (-x) δ
-- Init.Data.Array.MinMax
Array.le_max_of_mem : ∀ {α : Type u_1} [inst : Max α] [inst_1 : LE α] [Std.IsLinearOrder α] [Std.LawfulOrderMax α] {xs : Array α} {a : α}
  (ha : a ∈ xs), a ≤ xs.max ⋯
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
/-- Taking the involute of the product a list of $n$ vectors lifted via `ι` is equivalent to
premultiplying by ${-1}^n$.  -/
CliffordAlgebra.involute_prod_map_ι : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (l : List M),
  CliffordAlgebra.involute (List.map (⇑(CliffordAlgebra.ι Q)) l).prod =
    (-1) ^ l.length • (List.map (⇑(CliffordAlgebra.ι Q)) l).prod
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isLittleOTVS_insert : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {f : α → E} {g : α → F} [inst_7 : TopologicalSpace α] {x : α}
  {s : Set α}, f x = 0 → (f =o[𝕜; nhdsWithin x (insert x s)] g ↔ f =o[𝕜; nhdsWithin x s] g)
-- Mathlib.Combinatorics.Quiver.Push
/-- The prefunctor induced by pushing arrows via `σ`  -/
Quiver.Push.of : {V : Type u_1} → [inst : Quiver V] → {W : Type u_2} → (σ : V → W) → V ⥤q Quiver.Push σ
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instCommMonoid : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommMonoid R] →
      [inst_1 : NonUnitalCommSemiring A] →
        [inst_2 : DistribMulAction R A] → [IsScalarTower R A A] → [SMulCommClass R A A] → CommMonoid (Unitization R A)
-- Mathlib.Data.Finset.Sigma
Set.biUnion_finsetSigma : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} (s : Finset ι) (t : (i : ι) → Finset (α i)) (f : Sigma α → Set β),
  ⋃ ij ∈ s.sigma t, f ij = ⋃ i ∈ s, ⋃ j ∈ t i, f ⟨i, j⟩
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_eq_empty : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, ¬a ≤ b → Set.Icc a b = ∅
-- Mathlib.RingTheory.Frobenius
/-- Suppose `S` is an `R` algebra, `M` is a monoid acting on `S` whose action is trivial on `R`
`σ : M` is an (arithmetic) Frobenius at an ideal `Q` of `S` if `σ • x ≡ x ^ q (mod Q)` for all `x`.
 -/
IsArithFrobAt : (R : Type u_1) →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {M : Type u_3} →
            [inst_3 : Monoid M] → [inst_4 : MulSemiringAction M S] → [SMulCommClass M R S] → M → Ideal S → Prop
-- Mathlib.Data.Set.Finite.Lemmas
/-- Induction up to `univ`.  -/
Set.Finite.induction_to_univ : ∀ {α : Type u} [Finite α] {C : Set α → Prop} (S0 : Set α),
  C S0 → (∀ (S : Set α), S ≠ Set.univ → C S → ∃ a ∉ S, C (insert a S)) → C Set.univ
-- Mathlib.GroupTheory.Perm.Fin
Fin.sign_cycleIcc_of_ge : ∀ {n : ℕ} {i j : Fin n}, i ≤ j → Equiv.Perm.sign (j.cycleIcc i) = 1
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom.congr_simp : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₁_1 : CategoryTheory.Functor J C) (e_F₁ : F₁ = F₁_1)
  (F₂ F₂_1 : CategoryTheory.Functor J C) (e_F₂ : F₂ = F₂_1)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂],
  CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁ F₂ =
    CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁_1 F₂_1
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.quasiIsoAt_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] (n₀ n₁ : ℤ),
  n₀ + 1 = n₁ →
    (∀ i ≤ n₀, QuasiIsoAt f i) →
      ∀ i ≤ n₀, QuasiIsoAt (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.ι✝ f n₁) i
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.Scheme.Hom.flat_appTop : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y]
  [AlgebraicGeometry.Flat f], (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop f)).Flat
-- Init.Core
/-- If `TransGen r a b` and `r b c`, then `TransGen r a c`.
This is the inductive case of the transitive closure.  -/
Relation.TransGen.tail : ∀ {α : Sort u} {r : α → α → Prop} {a b c : α}, Relation.TransGen r a b → r b c → Relation.TransGen r a c
-- Batteries.Data.Array.Scan
Array.scanrM_extract : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {stop start : ℕ} {init : β} [inst : Monad m] [LawfulMonad m]
  {f : α → β → m β} {as : Array α}, Array.scanrM f init (as.extract stop start) = Array.scanrM f init as start stop
-- Mathlib.Data.List.MinMax
/-- `maximum l` returns a `WithBot α`, the largest element of `l` for nonempty lists, and `⊥` for
`[]`  -/
List.maximum : {α : Type u_1} → [inst : Preorder α] → [DecidableLT α] → List α → WithBot α
-- Init.Core
eq_self_iff_true : ∀ {α : Sort u_1} (a : α), a = a ↔ True
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_inter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, (m₁ ∩ m₂)[k]? = if k ∈ m₂ then m₁[k]? else none
-- Mathlib.Algebra.Module.ZLattice.Covolume
ZLattice.covolume_eq_measure_fundamentalDomain : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [inst_5 : DiscreteTopology ↥L] [IsZLattice ℝ L]
  (μ : autoParam (MeasureTheory.Measure E) _auto_19✝) [μ.IsAddHaarMeasure] {F : Set E},
  MeasureTheory.IsAddFundamentalDomain (↥L) F μ → ZLattice.covolume L μ = μ.real F
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbol.brecOn_1.go : {motive_1 : Lean.Lsp.DocumentSymbol → Sort u} →
  {motive_2 : Lean.Lsp.DocumentSymbolAux Lean.Lsp.DocumentSymbol → Sort u} →
    {motive_3 : Option (Array Lean.Lsp.DocumentSymbol) → Sort u} →
      {motive_4 : Array Lean.Lsp.DocumentSymbol → Sort u} →
        {motive_5 : List Lean.Lsp.DocumentSymbol → Sort u} →
          (t : Lean.Lsp.DocumentSymbolAux Lean.Lsp.DocumentSymbol) →
            ((t : Lean.Lsp.DocumentSymbol) → t.below → motive_1 t) →
              ((t : Lean.Lsp.DocumentSymbolAux Lean.Lsp.DocumentSymbol) →
                  Lean.Lsp.DocumentSymbol.below_1 t → motive_2 t) →
                ((t : Option (Array Lean.Lsp.DocumentSymbol)) → Lean.Lsp.DocumentSymbol.below_2 t → motive_3 t) →
                  ((t : Array Lean.Lsp.DocumentSymbol) → Lean.Lsp.DocumentSymbol.below_3 t → motive_4 t) →
                    ((t : List Lean.Lsp.DocumentSymbol) → Lean.Lsp.DocumentSymbol.below_4 t → motive_5 t) →
                      motive_2 t ×' Lean.Lsp.DocumentSymbol.below_1 t
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
modularCyclotomicCharacter'.unique' : ∀ (L : Type u) [inst : CommRing L] [inst_1 : IsDomain L] (n : ℕ) [inst_2 : NeZero n] (g : L ≃+* L)
  {c : ZMod (Nat.card ↥(rootsOfUnity n L))},
  (∀ t ∈ rootsOfUnity n L, g ↑t = ↑t ^ c.val) → c = ↑((modularCyclotomicCharacter' L n) g)
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upperCrossingTime_stabilize' : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n m : ℕ} {ω : Ω},
  n ≤ m → N ≤ MeasureTheory.upperCrossingTime a b f N n ω → MeasureTheory.upperCrossingTime a b f N m ω = N
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.prodComparisonIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) (A B : C)
  [inst_4 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F],
  (CategoryTheory.CartesianMonoidalCategory.prodComparisonIso F A B).hom =
    CategoryTheory.CartesianMonoidalCategory.prodComparison F A B
-- Lean.PrettyPrinter.Delaborator.Builtins
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.shouldGroupWithNext.getPPBinderTypes : Lean.Expr → Lean.Options → Bool
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion_inv : ∀ {α : Type u_2} {ι : Sort u_5} [inst : Inv α] (s : ι → Set α), (⋃ i, s i)⁻¹ = ⋃ i, (s i)⁻¹
-- Mathlib.RingTheory.LocalRing.Etale
/-- When `β` generates `S` over `R`, the residue `β₀ = β mod m_S`
generates `S/m_S` over `R/m_R`.  -/
IsLocalRing.adjoin_residue_eq_top_iff_adjoin_eq_top : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalRing S] [inst_4 : IsLocalRing R] [inst_5 : Module.Finite R S] [inst_6 : FaithfulSMul R S]
  [Algebra.FormallyUnramified R S] (β : S), (IsLocalRing.ResidueField R)[(IsLocalRing.residue S) β] = ⊤ ↔ R[β] = ⊤
-- Mathlib.Data.Nat.Factorial.Basic
Nat.add_factorial_succ_lt_factorial_add_succ : ∀ {i : ℕ} (n : ℕ), 2 ≤ i → i + (n + 1).factorial < (i + n + 1).factorial
-- Init.WF
PSigma.revLex : ∀ {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop},
  WellFounded r → WellFounded s → WellFounded (PSigma.RevLex r s)
-- Init.Notation
/-- `a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator). -/
«term_-_» : Lean.TrailingParserDescr