mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesOnBall.hasSum : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal},
  HasFPowerSeriesOnBall f p x r → ∀ {y : E}, y ∈ Metric.eball 0 r → HasSum (fun n => (p n) fun x => y) (f (x + y))
-- Mathlib.Topology.CWComplex.Classical.Graph
Topology.CWComplex.OneSkeletonGraph_isLink : ∀ {X : Type u_1} [inst : TopologicalSpace X] (C : Set X) [inst_1 : Topology.CWComplex C]
  (e : Topology.RelCWComplex.cell C 1) (x y : Topology.RelCWComplex.cell C 0),
  (Topology.CWComplex.OneSkeletonGraph C).IsLink e x y =
    (Topology.RelCWComplex.cellFrontier 1 e =
      Topology.RelCWComplex.closedCell 0 x ∪ Topology.RelCWComplex.closedCell 0 y)
-- Init.Data.Order.PackageFactories
Std.Packages.PreorderOfLEArgs.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (le : autoParam (LE α) Std.Packages.PreorderOfLEArgs.le._autoParam)
  (decidableLE : autoParam (DecidableLE α) Std.Packages.PreorderOfLEArgs.decidableLE._autoParam)
  (lt :
    autoParam
      (let this := le;
      LT α)
      Std.Packages.PreorderOfLEArgs.lt._autoParam)
  (beq :
    autoParam
      (let this := le;
      let this := decidableLE;
      BEq α)
      Std.Packages.PreorderOfLEArgs.beq._autoParam)
  (lt_iff :
    autoParam
      (let this := le;
      let this_1 := lt;
      ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a)
      Std.Packages.PreorderOfLEArgs.lt_iff._autoParam)
  (decidableLT :
    autoParam
      (let this := le;
      let this := decidableLE;
      let this := lt;
      have this_1 := lt_iff;
      DecidableLT α)
      Std.Packages.PreorderOfLEArgs.decidableLT._autoParam)
  (beq_iff_le_and_ge :
    autoParam
      (let this := le;
      let this_1 := decidableLE;
      let this_2 := beq;
      ∀ (a b : α), (a == b) = true ↔ a ≤ b ∧ b ≤ a)
      Std.Packages.PreorderOfLEArgs.beq_iff_le_and_ge._autoParam)
  (le_refl :
    autoParam
      (let this := le;
      ∀ (a : α), a ≤ a)
      Std.Packages.PreorderOfLEArgs.le_refl._autoParam)
  (le_trans :
    autoParam
      (let this := le;
      ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c)
      Std.Packages.PreorderOfLEArgs.le_trans._autoParam),
  sizeOf
      { le := le, decidableLE := decidableLE, lt := lt, beq := beq, lt_iff := lt_iff, decidableLT := decidableLT,
        beq_iff_le_and_ge := beq_iff_le_and_ge, le_refl := le_refl, le_trans := le_trans } =
    1 + sizeOf le + sizeOf lt + sizeOf beq
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
/-- A limit of a.e.-measurable `ℝ≥0∞`-valued functions is a.e.-measurable.  -/
ENNReal.aemeasurable_of_tendsto : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : ℕ → α → ENNReal} {g : α → ENNReal} {μ : MeasureTheory.Measure α},
  (∀ (i : ℕ), AEMeasurable (f i) μ) →
    (∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun i => f i a) Filter.atTop (nhds (g a))) → AEMeasurable g μ
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.norm_orthogonalProjectionOnto_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection] {v : E}, v ∈ K → ‖K.orthogonalProjectionOnto v‖ = ‖v‖
-- Mathlib.FieldTheory.IsAlgClosed.Spectrum
_private.Mathlib.FieldTheory.IsAlgClosed.Spectrum.0.spectrum.termσ : Lean.ParserDescr
-- Mathlib.Algebra.Torsor.Defs
Equiv.coe_constVSub_symm : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [inst_1 : AddTorsor G P] (p : P),
  ⇑(Equiv.constVSub p).symm = fun v => -v +ᵥ p
-- Mathlib.Data.Fin.Tuple.Basic
Fin.cons_right_injective : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u} (x₀ : α 0), Function.Injective (Fin.cons x₀)
-- Mathlib.CategoryTheory.Bicategory.Monad.Basic
CategoryTheory.Bicategory.Comonad.comul_assoc_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a : B} (t : a ⟶ a) [inst_1 : CategoryTheory.Bicategory.Comonad t]
  {Z : a ⟶ a} (h : CategoryTheory.CategoryStruct.comp t (CategoryTheory.CategoryStruct.comp t t) ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.Comonad.comul
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft t CategoryTheory.Bicategory.Comonad.comul) h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.Comonad.comul
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight CategoryTheory.Bicategory.Comonad.comul t)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator t t t).hom h))
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.iterate_eq_iterate_iff_of_lt_minimalPeriod : ∀ {α : Type u_1} {f : α → α} {x : α} {m n : ℕ},
  m < Function.minimalPeriod f x → n < Function.minimalPeriod f x → (f^[m] x = f^[n] x ↔ m = n)
-- Mathlib.AlgebraicGeometry.Sites.AffineEtale
AlgebraicGeometry.Scheme.AffineEtale.instFaithfulEtaleSpec : ∀ {S : AlgebraicGeometry.Scheme}, (AlgebraicGeometry.Scheme.AffineEtale.Spec S).Faithful
-- Init.Data.List.Sublist
List.filterMap_subset : ∀ {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} (f : α → Option β), l₁ ⊆ l₂ → List.filterMap f l₁ ⊆ List.filterMap f l₂
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.le_maxKey?_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {k km : α} (hc : t.contains k = true), t.maxKey?.get ⋯ = km → (cmp k km).isLE = true
-- Aesop.Search.Expansion
Aesop.expandGoal : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.GoalRef → Aesop.SearchM Q Aesop.RuleResult
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.assignmentToMessageData : Array Lean.Expr → Array Lean.MessageData
-- Mathlib.Data.List.Chain
List.isChain_cons_iff : ∀ {α : Type u_1} (R : α → α → Prop) (a : α) (l : List α),
  List.IsChain R (a :: l) ↔ l = [] ∨ ∃ b l', R a b ∧ List.IsChain R (b :: l') ∧ l = b :: l'
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.mulShift_apply : ∀ {A : Type u_1} {G : Type u_2} [inst : Monoid G] (g : G) (x : G → A) (h : G),
  SymbolicDynamics.FullShift.mulShift g x h = x (g * h)
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Verify that TryThis suggestions from a tactic actually work.

Runs the given tactic at each proof step, captures any "Try this:" suggestions,
then re-runs the suggested tactic to verify it succeeds.
Only reports failures (where the suggestion doesn't close the goal).  -/
Mathlib.TacticAnalysis.verifyTryThisSuggestions : (Lean.Syntax → Lean.MVarId → Lean.Elab.Command.CommandElabM (Option (Lean.TSyntax `tactic))) →
  String → Mathlib.TacticAnalysis.Config
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.ofCoeff.inj : ∀ {R : Type u_8} {M : Type u_9} {inst : Semiring R} {coeff coeff_1 : M →₀ R},
  MonoidAlgebra.ofCoeff coeff = MonoidAlgebra.ofCoeff coeff_1 → coeff = coeff_1
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonWorkspaceSymbolParams : Lean.ToJson Lean.Lsp.WorkspaceSymbolParams
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Cofork.ofπ_ι_app : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {P : C} (π : Y ⟶ P)
  (w : CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π)
  (X_1 : CategoryTheory.Limits.WalkingParallelPair),
  (CategoryTheory.Limits.Cofork.ofπ π w).ι.app X_1 =
    CategoryTheory.Limits.WalkingParallelPair.casesOn X_1 (CategoryTheory.CategoryStruct.comp f π) π
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.coe_toOrderIso : ∀ (f : CircleDeg1Liftˣ), ⇑(CircleDeg1Lift.toOrderIso f) = ⇑↑f
-- Mathlib.LinearAlgebra.Matrix.Integer
Matrix.den_transpose : ∀ {m : Type u_1} {n : Type u_2} [inst : Fintype m] [inst_1 : Fintype n] (A : Matrix m n ℚ), A.transpose.den = A.den
-- Mathlib.Algebra.MonoidAlgebra.Grading
/-- The submodule corresponding to each grade.  -/
AddMonoidAlgebra.grade : {M : Type u_1} → (R : Type u_3) → [inst : CommSemiring R] → M → Submodule R (AddMonoidAlgebra R M)
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.comp_coe : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Semiring C]
  [inst_6 : TopologicalSpace C] [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : Algebra R C] (e₁ : A ≃A[R] B)
  (e₂ : B ≃A[R] C), (↑e₂.toAlgEquiv).comp ↑e₁.toAlgEquiv = ↑↑(e₁.trans e₂)
-- Mathlib.Algebra.Star.Pi
Pi.instTrivialStarForall : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Star (f i)] [∀ (i : I), TrivialStar (f i)],
  TrivialStar ((i : I) → f i)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_of_contains_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w} [Std.TransCmp cmp]
  {f : (a : α) → β a → γ a} {k : α}, (Std.DTreeMap.map f t).contains k = true → t.contains k = true
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.Uniformizer.mk.injEq : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] {v : Valuation A Γ}
  [hv : v.IsRankOneDiscrete] (val : ↥v.integer) (valuation_gt_one : v.IsUniformizer ↑val) (val_1 : ↥v.integer)
  (valuation_gt_one_1 : v.IsUniformizer ↑val_1),
  ({ val := val, valuation_gt_one := valuation_gt_one } = { val := val_1, valuation_gt_one := valuation_gt_one_1 }) =
    (val = val_1)
-- Mathlib.Tactic.Ring.Basic
/-- Converts `ExSum sα` to `ExSum sβ`, assuming `sα` and `sβ` are defeq.  -/
Mathlib.Tactic.Ring.ExSum.cast : {u : Lean.Level} →
  {α : Q(Type u)} →
    (sα : Q(CommSemiring «$α»)) →
      {v : Lean.Level} →
        {β : Q(Type v)} →
          {sβ : Q(CommSemiring «$β»)} →
            {a : Q(«$α»)} → Mathlib.Tactic.Ring.ExSum sα a → (a : Q(«$β»)) × Mathlib.Tactic.Ring.ExSum sβ a
-- Mathlib.Topology.Order.Hom.Esakia
ContinuousOrderHom.copy.congr_simp : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : TopologicalSpace β]
  [inst_3 : Preorder β] (f f_1 : α →Co β) (e_f : f = f_1) (f' f'_1 : α → β) (e_f' : f' = f'_1) (h : f' = ⇑f),
  f.copy f' h = f_1.copy f'_1 ⋯
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.toOrderIso.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (f : α ≃+o β), f.toOrderIso = { toEquiv := f.toEquiv, map_rel_iff' := ⋯ }
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.congr_simp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : CategoryTheory.Limits.HasInitial C],
  HomotopicalAlgebra.CofibrantObject C = HomotopicalAlgebra.CofibrantObject C
-- Mathlib.Analysis.SpecificLimits.Basic
ENNReal.tsum_geometric_two_encode_le_two : ∀ {ι : Type u_4} [inst : Encodable ι], ∑' (i : ι), 2⁻¹ ^ Encodable.encode i ≤ 2
-- Mathlib.Combinatorics.Graph.Basic
Graph.IsLink.edge_mem : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β}, G.IsLink e x y → e ∈ G.edgeSet
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.binaryBiproductData_bicone_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hT₀ : T.mor₃ = 0) (inr : T.obj₃ ⟶ T.obj₂)
  (inr_snd : CategoryTheory.CategoryStruct.comp inr T.mor₂ = CategoryTheory.CategoryStruct.id T.obj₃)
  (fst : T.obj₂ ⟶ T.obj₁)
  (total :
    CategoryTheory.CategoryStruct.comp fst T.mor₁ + CategoryTheory.CategoryStruct.comp T.mor₂ inr =
      CategoryTheory.CategoryStruct.id T.obj₂),
  (CategoryTheory.Pretriangulated.binaryBiproductData T hT hT₀ inr inr_snd fst total).bicone.fst = fst
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
/-- The complex consisting of all faces present in either of its arguments.  -/
PreAbstractSimplicialComplex.instMax : (ι : Type u_1) → Max (PreAbstractSimplicialComplex ι)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_diff_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k fallback : α}, k ∈ t₂ → (t₁ \ t₂).getD k fallback = fallback
-- Mathlib.Order.Atoms
/-- A lattice is atomistic iff every element is a `sSup` of a set of atoms.  -/
IsAtomistic : (α : Type u_2) → [inst : PartialOrder α] → [OrderBot α] → Prop
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.rightOpComp_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor Cᵒᵖ D)
  (G : CategoryTheory.Functor D E) (X : C),
  (F.rightOpComp G).hom.app X = CategoryTheory.CategoryStruct.id (Opposite.op (G.obj (F.obj (Opposite.op X))))
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_minKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → ∀ {fallback : α}, t.getKey! (t.minKeyD fallback) = t.minKeyD fallback
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteGrp.instCoeSortType : CoeSort FiniteGrp.{u} (Type u)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
_private.Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer.0.CategoryTheory.Limits.MulticospanIndex.multicospanMapIso.match_1.eq_1 : ∀ {J : CategoryTheory.Limits.MulticospanShape} (motive : CategoryTheory.Limits.WalkingMulticospan J → Sort u_3)
  (a : J.L) (h_1 : (a : J.L) → motive (CategoryTheory.Limits.WalkingMulticospan.left a))
  (h_2 : (a : J.R) → motive (CategoryTheory.Limits.WalkingMulticospan.right a)),
  (match CategoryTheory.Limits.WalkingMulticospan.left a with
    | CategoryTheory.Limits.WalkingMulticospan.left a => h_1 a
    | CategoryTheory.Limits.WalkingMulticospan.right a => h_2 a) =
    h_1 a
-- Mathlib.Combinatorics.Quiver.ConnectedComponent
Quiver.WeaklyConnectedComponent.instCoeTC : {V : Type u_1} → [inst : Quiver V] → CoeTC V (Quiver.WeaklyConnectedComponent V)
-- Lean.Meta.WHNF
_private.Lean.Meta.WHNF.0.Lean.Meta.mkNullaryCtor : Lean.Expr → ℕ → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Analysis.Seminorm
/-- The sum over a finite set of continuous seminorms is continuous.  -/
Seminorm.continuous_finsetSum : ∀ {𝕝 : Type u_6} {E : Type u_7} {ι : Type u_11} [inst : SeminormedRing 𝕝] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕝 E] [inst_3 : TopologicalSpace E] {p : ι → Seminorm 𝕝 E} {s : Finset ι},
  (∀ i ∈ s, Continuous ⇑(p i)) → Continuous ⇑(∑ i ∈ s, p i)
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanOrder.val_symm_eq : ∀ {M : Type u_1}, ArchimedeanOrder.val.symm = ArchimedeanOrder.of
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- A characterization lemma for the scalar multiplication on the Ore localization,
allowing for a choice of Ore numerator and Ore denominator.  -/
OreLocalization.oreDiv_smul_char : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : MulAction R X] (r₁ : R) (r₂ : X) (s₁ s₂ : ↥S) (r' : R) (s' : ↥S),
  ↑s' * r₁ = r' * ↑s₂ → (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = r' • r₂ /ₒ (s' * s₁)
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
/-- **Alias** of the forward direction of `Matrix.nonsingular_transpose_iff`. -/
Matrix.Nonsingular.of_transpose : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R]
  {A : Matrix n n R}, A.transpose.Nonsingular → A.Nonsingular
-- Lean.Meta.AbstractMVars
Lean.Meta.AbstractMVars.State.mk : Lean.NameGenerator →
  Lean.LocalContext →
    Lean.MetavarContext →
      ℕ →
        Array Lean.Name →
          Array Lean.Expr →
            Array Lean.Expr →
              Std.HashMap Lean.LMVarId Lean.Level →
                Std.HashMap Lean.MVarId Lean.Expr → Bool → Lean.Meta.AbstractMVars.State
-- Mathlib.Geometry.Convex.Hull
Convexity.convexHull_mono : ∀ {R : Type u_1} {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {s t : Set X}, s ⊆ t → (Convexity.convexHull R) s ⊆ (Convexity.convexHull R) t
-- Mathlib.Order.Hom.WithTopBot
/-- Adjoins a `⊥` to the domain of a `SupHom`.  -/
SupHom.withBot' : {α : Type u_1} →
  {β : Type u_2} →
    [inst : SemilatticeSup α] →
      [inst_1 : SemilatticeSup β] → [inst_2 : OrderBot β] → SupHom α β → SupBotHom (WithBot α) β
-- Mathlib.Algebra.Ring.Prod
RingEquiv.prodZeroRing_apply : ∀ (R : Type u_1) (S : Type u_3) [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] [inst_2 : Subsingleton S]
  (x : R), (RingEquiv.prodZeroRing R S) x = (x, 0)
-- Mathlib.FieldTheory.Galois.Profinite
/-- The `ContinuousMulEquiv` between `Gal(K/k)` and `lim Gal(L/k)` where `L` is a
`FiniteGaloisIntermediateField` ordered by inverse inclusion, obtained
from `InfiniteGalois.mulEquivToLimit`  -/
InfiniteGalois.continuousMulEquivToLimit : (k : Type u_3) →
  (K : Type u_4) →
    [inst : Field k] →
      [inst_1 : Field K] →
        [inst_2 : Algebra k K] →
          [IsGalois k K] →
            Gal(K/k) ≃ₜ* ↑(ProfiniteGrp.limit (InfiniteGalois.asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
-- Mathlib.MeasureTheory.Measure.Regular
/-- In a finite measure space, assume that any open set can be approximated from inside by closed
sets. Then the measure is weakly regular.  -/
MeasureTheory.Measure.InnerRegularWRT.weaklyRegular_of_finite : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [BorelSpace α] (μ : MeasureTheory.Measure α)
  [MeasureTheory.IsFiniteMeasure μ], μ.InnerRegularWRT IsClosed IsOpen → μ.WeaklyRegular
-- Mathlib.Topology.Order
instIndiscreteTopologyEmpty : IndiscreteTopology Empty
-- Lean.Parser.Term
Lean.Parser.Term.funStrictImplicitBinder.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ioc.coe_le_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] (x : ↑(Set.Ioc 0 1)), ↑x ≤ 1
-- Std.Do.PredTrans
Std.Do.PredTrans.apply_Pure_pure : ∀ {ps : Std.Do.PostShape} {α : Type u} (a : α) (Q : Std.Do.PostCond α ps), (pure a).apply Q = Q.1 a
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
/-- Structure for matrices over ℚ.

So far it is just a 2d-array carrying dimensions (that are supposed to match with the actual
dimensions of `data`), but the plan is to add some `Prop`-data and make the structure strict and
safe.

Note: we avoid using `Matrix` because it is far more efficient to store a matrix as its entries than
as function between `Fin`-s.
 -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.DenseMatrix : ℕ → ℕ → Type
-- Mathlib.CategoryTheory.Subfunctor.Finite
CategoryTheory.Subfunctor.IsFinite.exists_isGeneratedBy : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {F : CategoryTheory.Functor Cᵒᵖ (Type w)}
  {G : CategoryTheory.Subfunctor F} [self : G.IsFinite], ∃ ι, ∃ (_ : Finite ι), ∃ X x, Nonempty (G.IsGeneratedBy x)
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_comp_of_one : ∀ {α : Type u_1} {M : Type u_3} {N : Type u_4} [inst : One M] [inst_1 : One N] {s : Set α} {f : α → M} {g : M → N},
  g 1 = 1 → s.mulIndicator (g ∘ f) = g ∘ s.mulIndicator f
-- Mathlib.CategoryTheory.Sites.Point.Monoidal
CategoryTheory.GrothendieckTopology.Point.instPreservesColimitsOfShapeOppositeElementsFiberObjFunctorFlipCurriedTensor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.MonoidalCategory A]
  [CategoryTheory.LocallySmall.{w, v, u} C]
  [∀ (X : A),
      CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  (M : A),
  CategoryTheory.Limits.PreservesColimitsOfShape Φ.fiber.Elementsᵒᵖ
    ((CategoryTheory.MonoidalCategory.curriedTensor A).flip.obj M)
-- Mathlib.Analysis.Calculus.Gradient.Basic
/-- `f` has the gradient `f'` at the point `x` if
`f x' = f x + ⟨f', x' - x⟩ + o (x' - x)` where `x'` converges to `x`.  -/
HasGradientAt : {𝕜 : Type u_1} →
  {F : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup F] → [InnerProductSpace 𝕜 F] → [CompleteSpace F] → (F → 𝕜) → F → F → Prop
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
/-- **Alias** of the reverse direction of `NonnegSpectrumClass.iff_spectrum_nonneg`. -/
NonnegSpectrumClass.of_spectrum_nonneg : ∀ {𝕜 : Type u_3} {A : Type u_4} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : Ring A]
  [inst_3 : PartialOrder A] [inst_4 : Algebra 𝕜 A],
  (∀ (a : A), 0 ≤ a → ∀ x ∈ spectrum 𝕜 a, 0 ≤ x) → NonnegSpectrumClass 𝕜 A
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.Walk.isHamiltonianCycle_isCycle_and_isHamiltonian_tail : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a : α} {p : G.Walk a a},
  p.IsHamiltonianCycle ↔ p.IsCycle ∧ p.tail.IsHamiltonian
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_subtype_mulSupport : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (f : β → α),
  ∏' (x : ↑(Function.mulSupport f)), f ↑x = ∏' (x : β), f x
-- Mathlib.Data.Finset.Grade
Finset.isCoatom_compl_singleton : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (a : α), IsCoatom {a}ᶜ
-- Std.Http.Data.URI.Basic
Std.Http.URI.instInhabitedPath.default : Std.Http.URI.Path
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.cosPartialEquiv_symm_apply : ∀ (x : ℝ), ↑Real.cosPartialEquiv.symm x = Real.arccos x
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- The nonsingular inverse is the same as the general `Ring.inverse`.  -/
Matrix.nonsing_inv_eq_ringInverse : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α),
  A⁻¹ = Ring.inverse A
-- Mathlib.Analysis.InnerProductSpace.ProdL2
/-- If a subspace `K` of an inner product space `E` admits an orthogonal projection, then the
quotient `E ⧸ K` is isometrically isomorphic to the orthogonal complement `Kᗮ` of `K`.  -/
Submodule.quotientEquivOrthogonal : {𝕜 : Type u_1} →
  {E : Type u_4} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] → (K : Submodule 𝕜 E) → [K.HasOrthogonalProjection] → E ⧸ K ≃ₗᵢ[𝕜] ↥Kᗮ
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExSumNat.zero.sizeOf_spec : sizeOf Mathlib.Tactic.Ring.Common.ExSumNat.zero = 1
-- Mathlib.CategoryTheory.Monoidal.Closed.Functor
/-- If the Frobenius morphism at `A` is an isomorphism, then the exponential comparison transformation
(at `A`) is an isomorphism.
 -/
CategoryTheory.expComparison_iso_of_frobeniusMorphism_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v, u'} D]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) {L : CategoryTheory.Functor D C} [inst_4 : CategoryTheory.MonoidalClosed C]
  [inst_5 : CategoryTheory.MonoidalClosed D]
  [inst_6 : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F]
  (h : L ⊣ F) (A : C) [i : CategoryTheory.IsIso (CategoryTheory.frobeniusMorphism F h A)],
  CategoryTheory.IsIso (CategoryTheory.expComparison F A).natTrans
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.Range.end : Lean.Lsp.Range → Lean.Lsp.Position
-- Mathlib.Topology.Sheaves.LocalPredicate
TopCat.LocalPredicate.mk : {X : TopCat} →
  {T : ↑X → Type u_1} →
    (toPrelocalPredicate : TopCat.PrelocalPredicate T) →
      (∀ {U : TopologicalSpace.Opens ↑X} (f : (x : ↥U) → T ↑x),
          (∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, toPrelocalPredicate.pred fun x => f (i x)) →
            toPrelocalPredicate.pred f) →
        TopCat.LocalPredicate T