mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.mem_vars_iff_mem_support : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R} (i : σ),
  i ∈ p.vars ↔ ∃ d ∈ p.support, i ∈ d.support
-- Lean.Meta.Tactic.Grind.Anchor
_private.Lean.Meta.Tactic.Grind.Anchor.0.Lean.Meta.Grind.mix : UInt64 → UInt64 → UInt64
-- Mathlib.RingTheory.FractionalIdeal.Extended
FractionalIdeal.extended_ne_zero : ∀ {A : Type u_1} [inst : CommRing A] {B : Type u_2} [inst_1 : CommRing B] {f : A →+* B} {K : Type u_3} {M : Submonoid A}
  [inst_2 : CommRing K] [inst_3 : Algebra A K] [inst_4 : IsLocalization M K] (L : Type u_4) {N : Submonoid B}
  [inst_5 : CommRing L] [inst_6 : Algebra B L] [inst_7 : IsLocalization N L] (hf : M ≤ Submonoid.comap f N)
  {I : FractionalIdeal M K} [IsDomain B], Function.Injective ⇑f → I ≠ 0 → 0 ∉ N → FractionalIdeal.extended L hf I ≠ 0
-- Mathlib.RingTheory.TensorProduct.Maps
/-- If `A`, `B`, `C` are `R`-algebras, `A` and `C` are also `S`-algebras (forming a tower as
`·/S/R`), then the product map of `f : A →ₐ[S] C` and `g : B →ₐ[R] C` is an `S`-algebra
homomorphism.

This is just a special case of `Algebra.TensorProduct.lift` for when `C` is commutative.  -/
Algebra.TensorProduct.productLeftAlgHom : {R : Type uR} →
  {S : Type uS} →
    {A : Type uA} →
      {B : Type uB} →
        {C : Type uC} →
          [inst : CommSemiring R] →
            [inst_1 : CommSemiring S] →
              [inst_2 : Algebra R S] →
                [inst_3 : Semiring A] →
                  [inst_4 : Algebra R A] →
                    [inst_5 : Algebra S A] →
                      [inst_6 : IsScalarTower R S A] →
                        [inst_7 : Semiring B] →
                          [inst_8 : Algebra R B] →
                            [inst_9 : CommSemiring C] →
                              [inst_10 : Algebra R C] →
                                [inst_11 : Algebra S C] →
                                  [IsScalarTower R S C] → (A →ₐ[S] C) → (B →ₐ[R] C) → TensorProduct R A B →ₐ[S] C
-- Mathlib.Data.Nat.ModEq
Nat.add_div_eq_of_le_mod_add_mod : ∀ {a b c : ℕ}, c ≤ a % c + b % c → 0 < c → (a + b) / c = a / c + b / c + 1
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.map_adj : ∀ {V : Type u_1} {W : Type u_2} (f : V ↪ W) (G : SimpleGraph V) (u v : W),
  (SimpleGraph.map (⇑f) G).Adj u v ↔ ∃ u' v', G.Adj u' v' ∧ f u' = u ∧ f v' = v
-- Mathlib.Topology.Homeomorph.Lemmas
/-- `Equiv.piCongrRight` as a homeomorphism: this is the natural homeomorphism
`Π i, Y₁ i ≃ₜ Π j, Y₂ i` obtained from homeomorphisms `Y₁ i ≃ₜ Y₂ i` for each `i`.  -/
Homeomorph.piCongrRight : {ι : Type u_7} →
  {Y₁ : ι → Type u_8} →
    {Y₂ : ι → Type u_9} →
      [inst : (i : ι) → TopologicalSpace (Y₁ i)] →
        [inst_1 : (i : ι) → TopologicalSpace (Y₂ i)] → ((i : ι) → Y₁ i ≃ₜ Y₂ i) → ((i : ι) → Y₁ i) ≃ₜ ((i : ι) → Y₂ i)
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_sum_range_succ : ∀ {α : Type u_1} {Ω : Type u_2} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω}
  {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [inst : AddCommMonoid β] [MeasurableAdd₂ β]
  {f : ℕ → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ℕ), Measurable (f i)) → ∀ (n : ℕ), ProbabilityTheory.Kernel.IndepFun (∑ j ∈ Finset.range n, f j) (f n) κ μ
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.mem_stabilizer_finset' : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] {a : G} [inst_2 : DecidableEq α]
  {s : Finset α}, a ∈ AddAction.stabilizer G s ↔ ∀ ⦃b : α⦄, b ∈ s → a +ᵥ b ∈ s
-- Mathlib.Data.List.ToFinsupp
/-- Indexing into a `l : List M`, as a finitely-supported function,
where the support are all the indices within the length of the list
that index to a non-zero value. Indices beyond the end of the list are sent to 0.

This is a computable version of the `Finsupp.onFinset` construction.
 -/
List.toFinsupp : {M : Type u_1} → [inst : Zero M] → (l : List M) → [DecidablePred fun x => l.getD x 0 ≠ 0] → ℕ →₀ M
-- Mathlib.Algebra.Category.Grp.Images
AddCommGrpCat.instMonoι : ∀ {G H : AddCommGrpCat} (f : G ⟶ H), CategoryTheory.Mono (AddCommGrpCat.image.ι f)
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.Equivalence.sheafCongr.functor_obj_obj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃)
  [inst_2 : CategoryTheory.Category.{v₃, u₃} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite K J e.inverse]
  (X : CategoryTheory.Sheaf J A) (X_1 : Dᵒᵖ),
  ((CategoryTheory.Equivalence.sheafCongr.functor J K e A).obj X).obj.obj X_1 =
    X.obj.obj (Opposite.op (e.inverse.obj (Opposite.unop X_1)))
-- Mathlib.Topology.Algebra.Group.Basic
Filter.tendsto_mul_const_iff : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] (b : G) {c : G}
  {f : α → G} {l : Filter α}, Filter.Tendsto (fun x => f x * b) l (nhds (c * b)) ↔ Filter.Tendsto f l (nhds c)
-- Mathlib.Algebra.Order.Module.Defs
smul_nonpos_iff_pos_imp_nonpos : ∀ {α : Type u_1} {β : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [PosSMulStrictMono α β] {a : α} {b : β}, a • b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_assoc : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁)
  (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃)
  (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
  (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) {Z : F.obj b₀ ⟶ F.obj b₃}
  (h : CategoryTheory.CategoryStruct.comp (F.map f₀₁) (F.map f₁₃) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).hom h =
    CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv) h)))
-- Lean.Data.Lsp.Extra
/-- `$/lean/plainTermGoal` client<-server reply.  -/
Lean.Lsp.PlainTermGoal : Type
-- Std.Time.Format
/-- Formats a `PlainDate` using a specific format and locale.
 -/
Std.Time.PlainDate.format : Std.Time.PlainDate → String → optParam Std.Time.DateFormat Std.Time.DateFormat.enUS → String
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.le_maxKey_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (hc : k ∈ t), (cmp k (t.maxKey ⋯)).isLE = true
-- Mathlib.Algebra.BigOperators.Ring.Finset
Int.cast_multiset_sum : ∀ {R : Type u_4} [inst : AddCommGroupWithOne R] (s : Multiset ℤ), ↑s.sum = (Multiset.map Int.cast s).sum
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.equal.sizeOf_spec : ∀ {L : FirstOrder.Language} {α : Type u'} [inst : SizeOf α] {n : ℕ} (t₁ t₂ : L.Term (α ⊕ Fin n)),
  sizeOf (FirstOrder.Language.BoundedFormula.equal t₁ t₂) = 1 + sizeOf n + sizeOf t₁ + sizeOf t₂
-- Batteries.Data.Array.Basic
_private.Batteries.Data.Array.Basic.0.Array.scanlMFast.loop : {m : Type u_1 → Type u_2} →
  {β : Type u_1} →
    {α : Type u_3} →
      [Monad m] →
        (β → α → m β) → β → (as : Array α) → USize → (stop : USize) → stop.toNat ≤ as.size → Array β → m (Array β)
-- Mathlib.CategoryTheory.Adjunction.CompositionIso
/-- A natural isomorphism `G₂₁ ⋙ G₁₀ ≅ G₂₀` involving right adjoint functors
induces a natural isomorphism `F₀₁ ⋙ F₁₂ ≅ F₀₂` between the corresponding
left adjoint functors.  -/
CategoryTheory.Adjunction.leftAdjointCompIso : {C₀ : Type u_1} →
  {C₁ : Type u_2} →
    {C₂ : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₀] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₁] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C₂] →
            {F₀₁ : CategoryTheory.Functor C₀ C₁} →
              {F₁₂ : CategoryTheory.Functor C₁ C₂} →
                {F₀₂ : CategoryTheory.Functor C₀ C₂} →
                  {G₁₀ : CategoryTheory.Functor C₁ C₀} →
                    {G₂₁ : CategoryTheory.Functor C₂ C₁} →
                      {G₂₀ : CategoryTheory.Functor C₂ C₀} →
                        (F₀₁ ⊣ G₁₀) → (F₁₂ ⊣ G₂₁) → (F₀₂ ⊣ G₂₀) → (G₂₁.comp G₁₀ ≅ G₂₀) → (F₀₁.comp F₁₂ ≅ F₀₂)
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverEntropyInfEntourage_antitone : ∀ {X : Type u_1} (T : X → X) (F : Set X), Antitone fun U => Dynamics.coverEntropyInfEntourage T F U
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.compMonoidHom'.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {γ : Type u_3}
  [inst_2 : TopologicalSpace γ] [inst_3 : MulOneClass γ] [inst_4 : ContinuousMul γ] (g : C(α, β)),
  g.compMonoidHom' = { toFun := fun f => f.comp g, map_one' := ⋯, map_mul' := ⋯ }
-- Init.Data.Nat.Basic
Nat.succ_le_of_lt : ∀ {n m : ℕ}, n < m → n.succ ≤ m
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- If we're boundaryless, `extChartAt` has open target  -/
isOpen_extChartAt_target : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] [I.Boundaryless] (x : M), IsOpen (extChartAt I x).target
-- Init.Data.Array.Attach
Array.getElem?_attach : ∀ {α : Type u_1} {xs : Array α} {i : ℕ}, xs.attach[i]? = Option.pmap Subtype.mk xs[i]? ⋯
-- Mathlib.Topology.Instances.RatLemmas
Rat.interior_compact_eq_empty : ∀ {s : Set ℚ}, IsCompact s → interior s = ∅
-- Lean.Parser.Basic
Lean.Parser.OrElseOnAntiquotBehavior.merge.sizeOf_spec : sizeOf Lean.Parser.OrElseOnAntiquotBehavior.merge = 1
-- Init.MetaTypes
/-- A list of indices for which occurrences should be rewritten.  -/
Lean.Meta.Occurrences.pos : List ℕ → Lean.Meta.Occurrences
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Report places where `omega` can be replaced by `lia`.  -/
linter.tacticAnalysis.omegaToLia : Lean.Option Bool
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffOn.sub_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [inst_1 : TopologicalSpace H]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : SubNegMonoid G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G]
  {E' : Type u_5} [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_6}
  [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_11 : TopologicalSpace M]
  [inst_12 : ChartedSpace H' M] {f : M → G} {s : Set M} (c : G),
  ContMDiffOn I' I n f s → ContMDiffOn I' I n (fun x => f x - c) s
-- Mathlib.AlgebraicGeometry.Morphisms.Constructors
AlgebraicGeometry.HasAffineProperty.diagonal_of_openCover : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {Q : AlgebraicGeometry.AffineTargetMorphismProperty}
  [AlgebraicGeometry.HasAffineProperty P Q] {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover)
  [inst : ∀ (i : 𝒰.I₀), AlgebraicGeometry.IsAffine (𝒰.X i)]
  (𝒰' : (i : 𝒰.I₀) → (CategoryTheory.Limits.pullback f (𝒰.f i)).OpenCover)
  [inst_1 : ∀ (i : 𝒰.I₀) (j : (𝒰' i).I₀), AlgebraicGeometry.IsAffine ((𝒰' i).X j)],
  (∀ (i : 𝒰.I₀) (j k : (𝒰' i).I₀),
      Q
        (CategoryTheory.Limits.pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k)
          (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f i))) →
    P.diagonal f
-- Init.Data.Int.Linear
Int.Internal.Linear.le_combine : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ p₃ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.le_combine_cert p₁ p₂ p₃ = true →
    Int.Internal.Linear.Poly.denote' ctx p₁ ≤ 0 →
      Int.Internal.Linear.Poly.denote' ctx p₂ ≤ 0 → Int.Internal.Linear.Poly.denote' ctx p₃ ≤ 0
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanOrder.val.eq_1 : ∀ {M : Type u_1}, MulArchimedeanOrder.val = Equiv.refl (MulArchimedeanOrder M)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.mem_ofArrows_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} {X : C} (Y : I → C) (f : (i : I) → Y i ⟶ X)
  {W : C} (g : W ⟶ X),
  (CategoryTheory.Sieve.ofArrows Y f).arrows g ↔ ∃ i a, g = CategoryTheory.CategoryStruct.comp a (f i)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.instSupSet.eq_1 : ∀ {R : Type u} {M : Type v} [inst : VAdd R M],
  SubAddAction.instSupSet = { sSup := fun S => { carrier := ⋃ s ∈ S, ↑s, vadd_mem' := ⋯ } }
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.range_mapRangeAddMonoidHom : ∀ {ι : Type u_1} {β₁ : ι → Type u_8} {β₂ : ι → Type u_9} [inst : (i : ι) → AddCommGroup (β₁ i)]
  [inst_1 : (i : ι) → AddCommGroup (β₂ i)] (f : (i : ι) → β₂ i →+ β₁ i),
  (DFinsupp.mapRange.addMonoidHom f).range =
    AddSubgroup.comap DFinsupp.coeFnAddMonoidHom (AddSubgroup.pi Set.univ fun x => (f x).range)
-- Mathlib.Analysis.Convex.Between
sbtw_comm : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] {x y z : P}, Sbtw R x y z ↔ Sbtw R z y x
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.simp_middle : Bool →
  Lean.Grind.AC.Seq →
    Lean.Grind.AC.Seq → Lean.Meta.Grind.AC.EqCnstr → Lean.Meta.Grind.AC.DiseqCnstr → Lean.Meta.Grind.AC.DiseqCnstrProof
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanQueryModuleParams.mk.injEq : ∀ (sourceRequestID : Lean.JsonRpc.RequestID) (queries : Array Lean.Lsp.LeanModuleQuery)
  (sourceRequestID_1 : Lean.JsonRpc.RequestID) (queries_1 : Array Lean.Lsp.LeanModuleQuery),
  ({ sourceRequestID := sourceRequestID, queries := queries } =
      { sourceRequestID := sourceRequestID_1, queries := queries_1 }) =
    (sourceRequestID = sourceRequestID_1 ∧ queries = queries_1)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.contains_of_contains_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k : α},
  (Std.ExtHashMap.filterMap f m).contains k = true → m.contains k = true
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.mk_neg : ∀ (z : ℂ) (hz : ‖-z‖ < 1), Complex.UnitDisc.mk (-z) hz = -Complex.UnitDisc.mk z ⋯
-- Mathlib.Data.Finset.Defs
List.instDecidableMapsToCoeFinsetOfDecidablePredMemSet : {α : Type u_1} →
  {β : Type u_2} →
    {f : α → β} → {s : Finset α} → {t : Set β} → [DecidablePred fun x => x ∈ t] → Decidable (Set.MapsTo f (↑s) t)
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
/-- Action of `iterateFrobeniusₛₗ` on the base field.  -/
IsPurelyInseparable.iterateFrobeniusₛₗ_algebraMap_base : ∀ (F : Type u_1) (K : Type u_2) (L : Type u_3) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsPurelyInseparable.HasExponent K L] (p : ℕ) [inst_4 : ExpChar K p] [inst_5 : Field F]
  [inst_6 : Algebra F K] [inst_7 : Algebra F L] [inst_8 : IsScalarTower F K L] [inst_9 : ExpChar F p] {n : ℕ}
  (hn : IsPurelyInseparable.exponent K L ≤ n) (a : F),
  (IsPurelyInseparable.iterateFrobeniusₛₗ F K L p hn) ((algebraMap F L) a) = (algebraMap F K) a ^ p ^ n
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.widePushoutShapeUnop_obj : ∀ (J : Type w) (X : (CategoryTheory.Limits.WidePushoutShape J)ᵒᵖ),
  (CategoryTheory.Limits.widePushoutShapeUnop J).obj X = Opposite.unop X
-- Lean.Parser.Syntax
Lean.Parser.Syntax.cat.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Homology.ShortComplex.ShortExact
CategoryTheory.ShortComplex.ShortExact.mono_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C}, S.ShortExact → CategoryTheory.Mono S.f
-- Mathlib.Util.Superscript
/-- Shorthand for `superscript(term)`.

This is needed because the initializer below does not always run, and if it has not run then
downstream parsers using the combinators will crash.

See https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Non-builtin.20parser.20aliases/near/365125476
for some context.  -/
Mathlib.Tactic.superscriptTerm : Lean.Parser.Parser
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.Cover.map_prop : ∀ {X : AlgebraicGeometry.Scheme} {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) (i : 𝒰.I₀), P (𝒰.f i)
-- Mathlib.Topology.GDelta.Basic
exists_of_not_isMeagre_biUnion : ∀ {X : Type u_1} {ι : Type u_3} [inst : TopologicalSpace X] {I : Set ι},
  I.Countable → ∀ {A : ι → Set X}, ¬IsMeagre (⋃ i ∈ I, A i) → ∃ i ∈ I, ¬IsMeagre (A i)
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.add_mem : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (L' : LieSubalgebra R L)
  {x y : L}, x ∈ L' → y ∈ L' → x + y ∈ L'
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.Hom.eq_3 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (x : CategoryTheory.WithTerminal C),
  x.Hom CategoryTheory.WithTerminal.star = PUnit.{v + 1}
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
/-- the natural morphism `F.obj j ⟶ Y`  -/
CategoryTheory.TransfiniteCompositionOfShape.incl : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          {X Y : C} →
            {f : X ⟶ Y} →
              [inst_3 : SuccOrder J] →
                [inst_4 : WellFoundedLT J] →
                  (self : CategoryTheory.TransfiniteCompositionOfShape J f) →
                    self.F ⟶ (CategoryTheory.Functor.const J).obj Y
-- Init.Data.List.Impl
List.zipIdx.eq_1 : ∀ {α : Type u} (x : ℕ), [].zipIdx x = []
-- Mathlib.Algebra.Ring.Subsemiring.Defs
NonUnitalSubsemiring.toSubsemiring_toNonUnitalSubsemiring : ∀ {R : Type u} [inst : NonAssocSemiring R] (S : NonUnitalSubsemiring R) (h1 : 1 ∈ S),
  (S.toSubsemiring h1).toNonUnitalSubsemiring = S
-- Lean.Parser.Do
/-- `for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass.
`break` and `continue` are supported inside `for` loops.
`for x in e, x2 in e2, ... do s` iterates over the given collections in parallel,
until at least one of them is exhausted.
The types of `e2` etc. must implement the `Std.ToStream` typeclass.
 -/
Lean.Parser.Term.doFor : Lean.Parser.Parser
-- Mathlib.Tactic.Core
/-- Extract the arguments from a `dsimpArgs` syntax as an array of syntaxes  -/
Mathlib.Tactic.getDSimpArgs : Lean.Syntax → Lean.Elab.Tactic.TacticM (Array Lean.Syntax)
-- Mathlib.FieldTheory.SeparablyGenerated
exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow' : ∀ {k : Type u_1} {K : Type u_2} {ι : Type u_3} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] (p : ℕ),
  Nat.Prime p →
    (∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x => x ^ p) ↑s) →
      ∀ {a : ι → K} [ExpChar k p] (s : Set ι) (n : ι),
        (IsTranscendenceBasis k fun i => a ↑i) →
          n ∉ s →
            ∃ i,
              (IsTranscendenceBasis k fun j => a ↑j) ∧
                IsSeparable (↥(IntermediateField.adjoin k (a '' (insert n s \ {i})))) (a i)
-- Mathlib.CategoryTheory.Endomorphism
CategoryTheory.End.ext : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {X : C} {x y : CategoryTheory.End X},
  x.asHom = y.asHom → x = y
-- Init.Internal.Order.Basic
Lean.Order.coind_monotone_forall : ∀ {α : Sort u_1} [inst : Lean.Order.PartialOrder α] {β : Sort u_2} (f : α → β → Lean.Order.ReverseImplicationOrder),
  Lean.Order.monotone f → Lean.Order.monotone fun x => ∀ (y : β), f x y
-- Init.Data.Fin.Basic
/-- Negation on `Fin n`  -/
Fin.neg : (n : ℕ) → Neg (Fin n)
-- Mathlib.Order.WellFoundedSet
/-- Stronger version of `PSigma.lex_wf`. Instead of requiring `rπ on g` to be well-founded, we only
require it to be well-founded on fibers of `f`.  -/
WellFounded.sigma_lex_of_wellFoundedOn_fiber : ∀ {ι : Type u_1} {γ : Type u_4} {π : ι → Type u_5} {rι : ι → ι → Prop} {rπ : (i : ι) → π i → π i → Prop} {f : γ → ι}
  {g : (i : ι) → γ → π i},
  WellFounded (Function.onFun rι f) →
    (∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (Function.onFun (rπ i) (g i))) →
      WellFounded (Function.onFun (Sigma.Lex rι rπ) fun c => ⟨f c, g (f c) c⟩)
-- Mathlib.Topology.Connected.LocallyPathConnected
LocallyPathConnectedSpace.mk : ∀ {X : Type u_4} [inst : TopologicalSpace X],
  (∀ (x : X), (nhds x).HasBasis (fun s => s ∈ nhds x ∧ IsPathConnected s) id) → LocallyPathConnectedSpace X
-- Init.Grind.ToInt
_private.Init.Grind.ToInt.0.Lean.Grind.instBEqIntInterval.beq.eq_def : ∀ (x x_1 : Lean.Grind.IntInterval),
  Lean.Grind.instBEqIntInterval.beq x x_1 =
    match x, x_1 with
    | Lean.Grind.IntInterval.co a a_1, Lean.Grind.IntInterval.co b b_1 => a == b && a_1 == b_1
    | Lean.Grind.IntInterval.ci a, Lean.Grind.IntInterval.ci b => a == b
    | Lean.Grind.IntInterval.io a, Lean.Grind.IntInterval.io b => a == b
    | Lean.Grind.IntInterval.ii, Lean.Grind.IntInterval.ii => true
    | x, x_2 => false
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.homeoOfIso_symm_apply : ∀ {X Y : TopCat} (f : X ≅ Y) (a : ↑Y), (TopCat.homeoOfIso f).symm a = (CategoryTheory.ConcreteCategory.hom f.inv) a
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.finiteArchimedeanClassOrderIsoLex_apply_fst : ∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : LinearOrder R] [inst_2 : AddCommGroup R]
  [inst_3 : IsOrderedAddMonoid R] {x : Lex (HahnSeries Γ R)} (h : x ≠ 0),
  ↑(ofLex ((HahnSeries.finiteArchimedeanClassOrderIsoLex Γ R) (FiniteArchimedeanClass.mk x h))).1 = (ofLex x).orderTop
-- Init.Prelude
/-- - `unicode("→", "->")` parses a symbol matching either `→` or `->`. Each symbol is reserved.
  The second symbol is an ASCII version of the first.
  The  `pp.unicode` option controls which is used when pretty printing.
- `unicode("→", "->", preserveForPP)` is the same except for pretty printing behavior.
  When the `pp.unicode` option is enabled, then the pretty printer uses whichever symbol
  matches the underlying atom in the syntax.
  The intent is that `preserveForPP` means that the ASCII variant is preferred.
  For example, `fun` notation uses `preserveForPP` for its arrow; the delaborator chooses
  `↦` or `=>` depending on the value of `pp.unicode.fun`, letting users opt-in to formatting with `↦`.
  Note that `notation` creates a pretty printer preferring the ASCII version.
 -/
Lean.ParserDescr.unicodeSymbol : String → String → Bool → Lean.ParserDescr
-- Mathlib.Tactic.Bound
Mathlib.Tactic.Bound.lt_max_of_lt_left_or_lt_right : ∀ {α : Type} [inst : LinearOrder α] {a b c : α}, a < b ∨ a < c → a < max b c
-- Mathlib.NumberTheory.RatFunc.Ostrowski
/-- **Alias** of `RatFunc.setOfPred_polynomial_valuation_lt_one_and_ne_zero_nonempty`. -/
RatFunc.setOf_polynomial_valuation_lt_one_and_ne_zero_nonempty : ∀ {K : Type u_1} {Γ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ]
  {v : Valuation (RatFunc K) Γ} [v.IsNontrivial] [Valuation.IsTrivialOn K v],
  v RatFunc.X ≤ 1 → {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Construct the expression for `f ◁ η`.  -/
Mathlib.Tactic.BicategoryLike.WhiskerLeft.whisker : Mathlib.Tactic.BicategoryLike.Mor₂ →
  Mathlib.Tactic.BicategoryLike.Atom₁ →
    Mathlib.Tactic.BicategoryLike.WhiskerLeft → Mathlib.Tactic.BicategoryLike.WhiskerLeft