mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Extension.Presentation.Submersive
/-- A `PreSubmersivePresentation` of an `R`-algebra `S` is a `Presentation`
with relations equipped with an injective `map : relations → vars`.

This map determines how the differential of `P` is constructed. See
`PreSubmersivePresentation.differential` for details.
 -/
Algebra.PreSubmersivePresentation : (R : Type u) →
  (S : Type v) →
    Type w → Type t → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → Type (max (max (max t u) v) w)
-- Lean.Parser.Term
Lean.Parser.Term.letDecl.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.FlatMap.0.Std.Iter.step_flatMapAfter.match_1.splitter : {α₂ γ : Type u_1} →
  (motive : Option (Std.Iter γ) → Sort u_2) →
    (it₂ : Option (Std.Iter γ)) → (Unit → motive none) → ((it₂ : Std.Iter γ) → motive (some it₂)) → motive it₂
-- Std.Internal.Parsec.Basic
/-- Attempt to parse with `p`, but don't consume input on failure.
 -/
Std.Internal.Parsec.attempt : {α ι : Type} → Std.Internal.Parsec ι α → Std.Internal.Parsec ι α
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_mul_Iio_of_neg : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (a : α) {c : α},
  c < 0 → (fun x => c * x) ⁻¹' Set.Iio a = Set.Ioi (a / c)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_div_const_Iio : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (fun x => x / a) '' Set.Iio b = Set.Iio (b / a)
-- Mathlib.Probability.BrownianMotion.Basic
ProbabilityTheory.IsPreBrownianReal.isGaussianProcess : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.IsPreBrownianReal B P → ProbabilityTheory.IsGaussianProcess B P
-- Mathlib.Probability.Martingale.Convergence
/-- The limiting process of an Lᵖ-bounded submartingale is Lᵖ.  -/
MeasureTheory.Submartingale.memLp_limitProcess : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
  {f : ℕ → Ω → ℝ} {R : NNReal} {p : ENNReal},
  MeasureTheory.Submartingale f ℱ μ →
    (∀ (n : ℕ), MeasureTheory.eLpNorm (f n) p μ ≤ ↑R) →
      MeasureTheory.MemLp (MeasureTheory.Filtration.limitProcess f ℱ μ) p μ
-- Mathlib.CategoryTheory.Monad.Equalizer
CategoryTheory.Comonad.CofreeEqualizer.bottomMap_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra),
  (CategoryTheory.Comonad.CofreeEqualizer.bottomMap X).f = T.δ.app X.A
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.filter_eq_filterₘ : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) (f : (a : α) → β a → Bool),
  Std.DHashMap.Internal.Raw₀.filter f m = m.filterₘ f
-- ProofWidgets.Data.Html
ProofWidgets.Jsx.«proofWidgetsJsxElement<__>_</_>» : Lean.ParserDescr
-- Mathlib.Order.Category.Preord
Preord.dual_map : ∀ {X Y : Preord} (f : X ⟶ Y), Preord.dual.map f = Preord.ofHom (OrderHom.dual (Preord.Hom.hom f))
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.rightUnitor.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.Center C),
  X.rightUnitor =
    CategoryTheory.Center.isoMk { f := (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.fst).hom, comm := ⋯ }
-- Init.Data.UInt.Lemmas
instCommutativeUInt64HMul : Std.Commutative fun x1 x2 => x1 * x2
-- Init.Data.List.MinMaxOn
List.maxOn_cons_cons_nil : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {a b : α} {f : α → β},
  List.maxOn f [a, b] ⋯ = maxOn f a b
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.sum_map_zsmul : ∀ {ι : Type u_2} {G : Type u_4} [inst : SubtractionCommMonoid G] {m : Multiset ι} {f : ι → G} {n : ℤ},
  (Multiset.map (fun i => n • f i) m).sum = n • (Multiset.map f m).sum
-- Mathlib.Topology.Algebra.Monoid.Defs
/-- Eta-expanded form of `ContinuousWithinAt.mul` -/
ContinuousWithinAt.fun_mul : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M] [ContinuousMul M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f g : X → M} {s : Set X} {x : X},
  ContinuousWithinAt f s x → ContinuousWithinAt g s x → ContinuousWithinAt (fun i => f i * g i) s x
-- Mathlib.RingTheory.PowerSeries.PiTopology
PowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_isNilpotent : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : CommSemiring R] {f : PowerSeries R},
  IsNilpotent (PowerSeries.constantCoeff f) → Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
-- Mathlib.RingTheory.PicardGroup
/-- The Picard group of a local semiring is trivial.  -/
CommRing.Pic.instSubsingletonOfIsLocalRing : ∀ {R : Type u} [inst : CommSemiring R] [IsLocalRing R], Subsingleton (CommRing.Pic R)
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (Hₚ : ι → CategoryTheory.Functor TopPair C)
  (H : ι → CategoryTheory.Functor TopCat C) (iso : (i : ι) → H i ≅ TopPair.incl.comp (Hₚ i))
  (δ : (i j : ι) → Hₚ i ⟶ TopPair.proj₂.comp (H j))
  (shape_δ : autoParam (∀ (i j : ι), ¬c.Rel i j → δ i j = 0) TopPair.HomologyPretheory.shape_δ._autoParam)
  (Hₚ_1 : ι → CategoryTheory.Functor TopPair C) (H_1 : ι → CategoryTheory.Functor TopCat C)
  (iso_1 : (i : ι) → H_1 i ≅ TopPair.incl.comp (Hₚ_1 i)) (δ_1 : (i j : ι) → Hₚ_1 i ⟶ TopPair.proj₂.comp (H_1 j))
  (shape_δ_1 : autoParam (∀ (i j : ι), ¬c.Rel i j → δ_1 i j = 0) TopPair.HomologyPretheory.shape_δ._autoParam),
  ({ Hₚ := Hₚ, H := H, iso := iso, δ := δ, shape_δ := shape_δ } =
      { Hₚ := Hₚ_1, H := H_1, iso := iso_1, δ := δ_1, shape_δ := shape_δ_1 }) =
    (Hₚ = Hₚ_1 ∧ H = H_1 ∧ iso ≍ iso_1 ∧ δ ≍ δ_1)
-- Mathlib.Order.Basic
Subtype.decidableLT : {α : Type u_2} → [inst : Preorder α] → [h : DecidableLT α] → {p : α → Prop} → DecidableLT (Subtype p)
-- Mathlib.Logic.Encodable.Basic
_private.Mathlib.Logic.Encodable.Basic.0.Encodable.encodeSum.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : α ⊕ β → Sort u_3) (a : α) (h_1 : (a : α) → motive (Sum.inl a))
  (h_2 : (b : β) → motive (Sum.inr b)),
  (match Sum.inl a with
    | Sum.inl a => h_1 a
    | Sum.inr b => h_2 b) =
    h_1 a
-- Mathlib.Condensed.TopCatAdjunction
_private.Mathlib.Condensed.TopCatAdjunction.0.CondensedSet.coinducingCoprod.eq_1 : ∀ (X : CondensedSet) (fst : CompHaus) (i : X.obj.obj (Opposite.op fst)) (s : ↑⟨fst, i⟩.fst.toTop),
  CondensedSet.coinducingCoprod✝ X ⟨⟨fst, i⟩, s⟩ =
    (CategoryTheory.ConcreteCategory.hom (X.obj.map (CompHausLike.const (CompHaus.of PUnit.{u + 1}) s).op)) i
-- Mathlib.Analysis.Normed.Group.Pointwise
sub_ball_zero : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (s : Set E), s - Metric.ball 0 δ = Metric.thickening δ s
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
DifferentiableWithinAt.continuousAlternatingMapCompContinuousLinearMap : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {H : Type u_6}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : NormedSpace 𝕜 H] {f : E → G [⋀^ι]→L[𝕜] H} {g : E → F →L[𝕜] G} {s : Set E}
  {x : E} [Finite ι],
  DifferentiableWithinAt 𝕜 f s x →
    DifferentiableWithinAt 𝕜 g s x → DifferentiableWithinAt 𝕜 (fun x => (f x).compContinuousLinearMap (g x)) s x
-- Init.Data.UInt.Lemmas
UInt64.ofInt_add : ∀ (x y : ℤ), UInt64.ofInt (x + y) = UInt64.ofInt x + UInt64.ofInt y
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.hasZeroMorphismsPEmpty : CategoryTheory.Limits.HasZeroMorphisms (CategoryTheory.Discrete PEmpty.{u_1 + 1})
-- Lean.Util.CollectLevelParams
Lean.CollectLevelParams.State.mk.inj : ∀ {visitedLevel : Lean.LevelSet} {visitedExpr : Lean.ExprSet} {params : Array Lean.Name}
  {visitedLevel_1 : Lean.LevelSet} {visitedExpr_1 : Lean.ExprSet} {params_1 : Array Lean.Name},
  { visitedLevel := visitedLevel, visitedExpr := visitedExpr, params := params } =
      { visitedLevel := visitedLevel_1, visitedExpr := visitedExpr_1, params := params_1 } →
    visitedLevel = visitedLevel_1 ∧ visitedExpr = visitedExpr_1 ∧ params = params_1
-- Std.Http.Internal.Char
_private.Std.Http.Internal.Char.0.Std.Http.Internal.Char.qdtext.match_1.eq_4 : ∀ (motive : Char → Sort u_1) (x : Char) (h_1 : Unit → motive '\t') (h_2 : Unit → motive ' ') (h_3 : Unit → motive '!')
  (h_4 : (x : Char) → motive x),
  (x = '\t' → False) →
    (x = ' ' → False) →
      (x = '!' → False) →
        (match x with
          | '\t' => h_1 ()
          | ' ' => h_2 ()
          | '!' => h_3 ()
          | x => h_4 x) =
          h_4 x
-- Mathlib.Data.Fintype.Sets
Set.toFinset_congr : ∀ {α : Type u_1} {s t : Set α} [inst : Fintype ↑s] [inst_1 : Fintype ↑t], s = t → s.toFinset = t.toFinset
-- Mathlib.RingTheory.Grassmannian
Module.Grassmannian.finite_quotient : ∀ {R : Type u} [inst : CommRing R] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {k : ℕ}
  (self : Module.Grassmannian R M k), Module.Finite R (M ⧸ self.toSubmodule)
-- Mathlib.RingTheory.OrderOfVanishing.Basic
Ring.ord_le_ord_of_dvd : ∀ {R : Type u_1} [inst : CommRing R] {a x : R}, a ∣ x → Ring.ord R a ≤ Ring.ord R x
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.direction_iInf_of_mem : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Sort u_4} (s : ι → AffineSubspace k P) (p : P),
  (∀ (i : ι), p ∈ s i) → (iInf s).direction = ⨅ i, (s i).direction
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.getLast?.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.domDomCongr_eq_zero_iff : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ≃ ι') (f : M [⋀^ι]→ₗ[R] N),
  AlternatingMap.domDomCongr σ f = 0 ↔ f = 0
-- Mathlib.RingTheory.Coalgebra.Basic
/-- The counit of the coalgebra  -/
CoalgebraStruct.counit : {R : Type u} →
  {A : Type v} →
    {inst : CommSemiring R} →
      {inst_1 : AddCommMonoid A} → {inst_2 : Module R A} → [self : CoalgebraStruct R A] → A →ₗ[R] R
-- Mathlib.Analysis.Normed.Group.Pointwise
mul_ball : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (s : Set E) (x : E),
  s * Metric.ball x δ = x • Metric.thickening δ s
-- Mathlib.CategoryTheory.Monoidal.Category
/-- The associator as a natural isomorphism.  -/
CategoryTheory.MonoidalCategory.associatorNatIso : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.MonoidalCategory.leftAssocTensor C ≅ CategoryTheory.MonoidalCategory.rightAssocTensor C
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithUpperSet.isOpen_ofUpperSet_preimage : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, IsOpen (⇑Topology.WithUpperSet.ofUpperSet ⁻¹' s) ↔ IsUpperSet s
-- Lean.Parser.Command
Lean.Parser.Command.structInstBinder.formatter : Lean.PrettyPrinter.Formatter
-- Plausible.Gen
_private.Plausible.Gen.0.Plausible.Gen.pickDrop : {α : Type u_1} → List (ℕ × Plausible.Gen α) → ℕ → ℕ × Plausible.Gen α × List (ℕ × Plausible.Gen α)
-- Lean.DocString.Syntax
/-- A link. The link's target may either be a concrete URL (written in parentheses) or a named URL
(written in square brackets).
 -/
Lean.Doc.Syntax.link : Lean.ParserDescr
-- Mathlib.Algebra.Order.Ring.Cast
Int.cast_max : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a b : ℤ}, ↑(max a b) = max ↑a ↑b
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.LimitOfShape.toLimitPresentation : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {P : CategoryTheory.ObjectProperty C} →
      {J : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} J] →
          {X : C} → P.LimitOfShape J X → CategoryTheory.Limits.LimitPresentation J X
-- Mathlib.Algebra.Order.Rearrangement
/-- **Strict inequality case of the Rearrangement Inequality**: Pointwise scalar multiplication of
`f` and `g`, which monovary together on `s`, is strictly decreased by a permutation if and only if
`f` and `g ∘ σ` do not monovary together on `s`. Stated by permuting the entries of `g`.  -/
MonovaryOn.sum_smul_comp_perm_lt_sum_smul_iff : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [ExistsAddOfLE α] [inst_4 : AddCommMonoid β] [inst_5 : LinearOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module α β] [PosSMulStrictMono α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β},
  MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → (∑ i ∈ s, f i • g (σ i) < ∑ i ∈ s, f i • g i ↔ ¬MonovaryOn f (g ∘ ⇑σ) ↑s)
-- Init.Data.Int.Linear
Int.Internal.Linear.dvd_solve_combine : ∀ (ctx : Int.Internal.Linear.Context) (d₁ : ℤ) (p₁ : Int.Internal.Linear.Poly) (d₂ : ℤ) (p₂ : Int.Internal.Linear.Poly)
  (d : ℤ) (p : Int.Internal.Linear.Poly) (g α β : ℤ),
  Int.Internal.Linear.dvd_solve_combine_cert d₁ p₁ d₂ p₂ d p g α β = true →
    d₁ ∣ Int.Internal.Linear.Poly.denote' ctx p₁ →
      d₂ ∣ Int.Internal.Linear.Poly.denote' ctx p₂ → d ∣ Int.Internal.Linear.Poly.denote' ctx p
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionHom_unop : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction Cᵒᵖ Dᵒᵖ] {c c' : Cᵒᵖ} {d d' : Dᵒᵖ} (f : c ⟶ c')
  (g : d ⟶ d'),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f.unop g.unop =
    Opposite.unop (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f g)
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
EuclideanGeometry.Sphere.center_mem_orthRadius_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p : P}, s.center ∈ s.orthRadius p ↔ p = s.center
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.instIsRightAdjointOfMonadicRightAdjoint : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (R : CategoryTheory.Functor D C) [CategoryTheory.MonadicRightAdjoint R], R.IsRightAdjoint
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.set.sizeOf_spec : ∀ (x : Lean.IR.VarId) (i : ℕ) (y : Lean.IR.Arg) (b : Lean.IR.FnBody),
  sizeOf (Lean.IR.FnBody.set x i y b) = 1 + sizeOf x + sizeOf i + sizeOf y + sizeOf b
-- Mathlib.Condensed.Discrete.Colimit
/-- A finite set is the coproduct of its points in `Profinite`.  -/
Condensed.fintypeCatAsCofanIsColimit : (X : Profinite) → [Finite ↑X.toTop] → CategoryTheory.Limits.IsColimit (Condensed.fintypeCatAsCofan X)
-- Aesop.Script.TacticState
Aesop.Script.TacticState.mkInitial : Lean.MVarId → Lean.MetaM Aesop.Script.TacticState
-- Lean.Server.References
Lean.Server.instFromJsonIlean : Lean.FromJson Lean.Server.Ilean
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientMap_surjective : ∀ {R : Type u} [inst : Ring R] {S : Type v} [inst_1 : Ring S] {J : Ideal R} {I : Ideal S} [inst_2 : I.IsTwoSided]
  [inst_3 : J.IsTwoSided] {f : R →+* S} {H : J ≤ Ideal.comap f I},
  Function.Surjective ⇑f → Function.Surjective ⇑(Ideal.quotientMap I f H)
-- Init.Data.Int.Order
Int.sign_neg_one : (-1).sign = -1
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.format : Lean.PrettyPrinter.Formatter → Lean.Syntax → Lean.CoreM Std.Format
-- Mathlib.Data.Fin.Tuple.Reflection
FinVec.sum.eq_def : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Zero α] (x : ℕ) (x_1 : Fin x → α),
  FinVec.sum x_1 =
    match x, x_1 with
    | 0, x => 0
    | 1, v => v 0
    | n.succ.succ, v => (FinVec.sum fun i => v i.castSucc) + v (Fin.last (n + 1))
-- Mathlib.Algebra.Order.Archimedean.IndicatorCard
Set.sum_indicator_eventually_eq_card : ∀ {α : Type u_1} [inst : AddCommMonoid α] (a : α) {s : Set ℕ},
  s.Finite → ∀ᶠ (n : ℕ) in Filter.atTop, ∑ k ∈ Finset.range n, s.indicator (fun x => a) k = Nat.card ↑s • a
-- Mathlib.Order.UpperLower.Principal
UpperSet.Ici_ne_top : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, UpperSet.Ici a ≠ ⊤
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.mk.injEq : ∀ {G : Type u} [inst : TopologicalSpace G] {H : Type v} [inst_1 : TopologicalSpace H] [inst_2 : Mul G] [inst_3 : Mul H]
  (toMulEquiv : G ≃* H)
  (continuous_toFun : autoParam (Continuous toMulEquiv.toFun) Homeomorph.continuous_toFun._autoParam)
  (continuous_invFun : autoParam (Continuous toMulEquiv.invFun) Homeomorph.continuous_invFun._autoParam)
  (toMulEquiv_1 : G ≃* H)
  (continuous_toFun_1 : autoParam (Continuous toMulEquiv_1.toFun) Homeomorph.continuous_toFun._autoParam)
  (continuous_invFun_1 : autoParam (Continuous toMulEquiv_1.invFun) Homeomorph.continuous_invFun._autoParam),
  ({ toMulEquiv := toMulEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun } =
      { toMulEquiv := toMulEquiv_1, continuous_toFun := continuous_toFun_1,
        continuous_invFun := continuous_invFun_1 }) =
    (toMulEquiv = toMulEquiv_1)
-- Init.Notation
/-- Sequences the effects of two terms, discarding the value of the second. This function is usually
invoked via the `<*` operator.

Given `x : f α` and `y : f β`, `x <* y` runs `x`, then runs `y`, and finally returns the result of
`x`.

The evaluation of the second argument is delayed by wrapping it in a function, enabling
“short-circuiting” behavior from `f`.


Conventions for notations in identifiers:

 * The recommended spelling of `<*` in identifiers is `seqLeft`. -/
«term_<*_» : Lean.TrailingParserDescr
-- Mathlib.Data.Fin.SuccPredOrder
Fin.orderSucc_castSucc : ∀ {n : ℕ} (i : Fin n), Order.succ i.castSucc = i.succ
-- Mathlib.CategoryTheory.Limits.Types.Pullbacks
CategoryTheory.Limits.PullbackCone.toPullbackObj_coe_snd : ∀ {X Y S : Type v} {f : X ⟶ S} {g : Y ⟶ S} (c : CategoryTheory.Limits.PullbackCone f g) (x : c.pt),
  (↑(c.toPullbackObj x)).2 = (CategoryTheory.ConcreteCategory.hom c.snd) x
-- Lean.Elab.Command
/-- Return identifier names in the given bracketed binder.  -/
Lean.Elab.Command.getBracketedBinderIds : Lean.Syntax → Lean.Elab.Command.CommandElabM (Array Lean.Name)
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.instSMulMemClassMulOpposite : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R], SMulMemClass (TwoSidedIdeal R) Rᵐᵒᵖ R
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.Slice.endsWith_char_eq_false_iff_forall_append : ∀ {c : Char} {s : String.Slice}, s.endsWith c = false ↔ ∀ (t : String), s.copy ≠ t ++ String.singleton c
-- Mathlib.Order.LiminfLimsup
Filter.limsup_le_limsup : ∀ {β : Type u_2} {α : Type u_6} [inst : ConditionallyCompleteLattice β] {f : Filter α} {u v : α → β},
  u ≤ᶠ[f] v →
    autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) Filter.limsup_le_limsup._auto_1 →
      autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) Filter.limsup_le_limsup._auto_3 →
        Filter.limsup u f ≤ Filter.limsup v f
-- Mathlib.Order.Filter.Basic
/-- **Alias** of the reverse direction of `Filter.principal_neBot_iff`. -/
Set.Nonempty.principal_neBot : ∀ {α : Type u} {s : Set α}, s.Nonempty → (Filter.principal s).NeBot
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.Matroidᵣ.lt_iff : ∀ {α : Type u_1} {M M' : Matroid.Matroidᵣ α}, M < M' ↔ M.toMatroid.IsStrictRestriction M'.toMatroid
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.isFinValueTransition : Lean.Meta.Match.Problem → Lean.MetaM Bool
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.symm_toAlgEquiv : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B), e.symm.toAlgEquiv = e.symm
-- Mathlib.Order.Basic
Prod.mk_lt_mk_of_lt_of_le : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {a₁ a₂ : α} {b₁ b₂ : β},
  a₁ < a₂ → b₁ ≤ b₂ → (a₁, b₁) < (a₂, b₂)
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.coe_mk : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂] (f : V₁ → V₂)
  (h₁ : ∀ (v₁ v₂ : V₁), f (v₁ + v₂) = f v₁ + f v₂) (h₂ : ℝ) (h₃ : ∀ (v : V₁), ‖f v‖ ≤ h₂ * ‖v‖),
  ⇑{ toFun := f, map_add' := h₁, bound' := ⋯ } = f
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubMulAction.ofStabilizer.conjMap_comp_apply : ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] {g h k : G} {a b c : α} {hg : b = g • a}
  {hh : c = h • b} {hk : c = k • a},
  k = h * g →
    ∀ (x : ↥(SubMulAction.ofStabilizer G a)),
      (SubMulAction.ofStabilizer.conjMap hh) ((SubMulAction.ofStabilizer.conjMap hg) x) =
        (SubMulAction.ofStabilizer.conjMap hk) x
-- Mathlib.LinearAlgebra.FreeModule.PID
Ideal.selfBasis.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R]
  {S : Type u_4} [inst_3 : CommRing S] [inst_4 : IsDomain S] [inst_5 : Algebra R S] [inst_6 : Finite ι]
  (b b_1 : Module.Basis ι R S),
  b = b_1 → ∀ (I : Ideal S) (hI : I ≠ ⊥), Ideal.selfBasis b I hI = Ideal.selfBasis b_1 I hI
-- Mathlib.Topology.Instances.Nat
Nat.instNoncompactSpace : NoncompactSpace ℕ
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.one.eq_1 : ∀ {M : Type u_4} [inst : MulOneClass M] (S : Submonoid M), S.one = { one := ⟨1, ⋯⟩ }
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.codeSupp_succ : ∀ (k : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.codeSupp Turing.ToPartrec.Code.succ k =
    Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal Turing.ToPartrec.Code.succ k) ∪
      Turing.PartrecToTM2.contSupp k
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_hom_app_app : ∀ {X Y : AlgebraicGeometry.Scheme} {U : X.Opens} {f g : X ⟶ Y} (hf : f = g) [inst : AlgebraicGeometry.IsOpenImmersion f]
  [inst_1 : AlgebraicGeometry.IsOpenImmersion g] (M : Y.Modules),
  AlgebraicGeometry.Scheme.Modules.Hom.app ((AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr hf).hom.app M) U =
    M.presheaf.map (CategoryTheory.eqToHom ⋯).op
-- Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
Polynomial.residueFieldMapCAlgEquiv_algebraMap : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) [inst_1 : I.IsPrime] (J : Ideal (Polynomial R)) [inst_2 : J.IsPrime]
  [inst_3 : J.LiesOver I] [inst_4 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)]
  [inst_5 : Localization.AtPrime.IsLiesOverAlgebra I J] (hJ : J = Ideal.map Polynomial.C I) (p : Polynomial R),
  (Polynomial.residueFieldMapCAlgEquiv I J hJ) ((algebraMap (Polynomial R) J.ResidueField) p) =
    (algebraMap (Polynomial I.ResidueField) (RatFunc I.ResidueField)) (Polynomial.map (algebraMap R I.ResidueField) p)
-- Mathlib.Algebra.Homology.Opposite
/-- Auxiliary definition for `unopEquivalence`.  -/
HomologicalComplex.unopInverse : {ι : Type u_1} →
  (V : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_2} V] →
      (c : ComplexShape ι) →
        [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
          CategoryTheory.Functor (HomologicalComplex V c.symm) (HomologicalComplex Vᵒᵖ c)ᵒᵖ
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- The canonical basis of the additive free group over `X`.  -/
FreeAddGroupBasis.ofFreeAddGroup : (X : Type u_5) → FreeAddGroupBasis X (FreeAddGroup X)