mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.InfiniteSum.Group
summable_iff_vanishing : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddCommGroup α] [IsUniformAddGroup α] {f : β → α}
  [CompleteSpace α], Summable f ↔ ∀ e ∈ nhds 0, ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b ∈ t, f b ∈ e
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lift_le : ∀ {a b : Cardinal.{v}}, Cardinal.lift.{u, v} a ≤ Cardinal.lift.{u, v} b ↔ a ≤ b
-- Mathlib.Algebra.Squarefree.Basic
Associated.squarefree_iff : ∀ {R : Type u_1} [inst : Monoid R] {x y : R}, Associated x y → (Squarefree x ↔ Squarefree y)
-- Mathlib.Geometry.Euclidean.NinePointCircle
Affine.Simplex.eulerPoint_restrict : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) (S : AffineSubspace ℝ P)
  (hS : affineSpan ℝ (Set.range s.points) ≤ S) (i : Fin (n + 1)), ↑((s.restrict S hS).eulerPoint i) = s.eulerPoint i
-- Mathlib.LinearAlgebra.FreeModule.PID
/-- A submodule inside the span of a linear independent family is a free `R`-module of finite rank,
if `R` is a principal ideal domain.  -/
Submodule.basisOfPidOfLESpan : {R : Type u_2} →
  [inst : CommRing R] →
    {M : Type u_3} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          [IsPrincipalIdealRing R] →
            [IsDomain R] →
              {ι : Type u_4} →
                [Finite ι] →
                  {b : ι → M} →
                    LinearIndependent R b →
                      {N : Submodule R M} → N ≤ Submodule.span R (Set.range b) → (n : ℕ) × Module.Basis (Fin n) R ↥N
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
cfcₙAux_injective : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A] [inst_2 : StarRing A]
  [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A] [inst_6 : StarModule 𝕜 A]
  {p : A → Prop} {p₁ : Unitization 𝕜 A → Prop} (hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x) (a : A) (ha : p a)
  [inst_7 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁], Function.Injective ⇑(cfcₙAux ⋯ a ha)
-- Std.Http.Internal.String
/-- Parses an HTTP `quoted-string`, returning the unescaped content when valid.
 -/
Std.Http.Internal.unquoteHttpString? : String → Option String
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iInter₂_smul_subset : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : SMul α β] (s : (i : ι) → κ i → Set α)
  (t : Set β), (⋂ i, ⋂ j, s i j) • t ⊆ ⋂ i, ⋂ j, s i j • t
-- Mathlib.Data.Multiset.Powerset
Multiset.map_single_le_powerset : ∀ {α : Type u_1} (s : Multiset α), Multiset.map singleton s ≤ s.powerset
-- Mathlib.Algebra.Lie.Basis.Base
/-- The distinguished root system base associated to a basis.  -/
LieAlgebra.Basis.base : {ι : Type u_1} →
  {K : Type u_2} →
    {L : Type u_3} →
      [inst : Fintype ι] →
        [inst_1 : Field K] →
          [inst_2 : CharZero K] →
            [inst_3 : LieRing L] →
              [inst_4 : LieAlgebra K L] →
                [inst_5 : FiniteDimensional K L] →
                  {H : LieSubalgebra K L} →
                    (b : LieAlgebra.Basis ι H) →
                      [inst_6 : LieModule.IsTriangularizable K (↥H) L] →
                        [inst_7 : LieAlgebra.IsKilling K L] → (LieAlgebra.IsKilling.rootSystem H).Base
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get?_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₂ → (t₁ \ t₂).get? k = none
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : LawfulBEq α]
  {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.containsKey k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) =
      Option.any (fun x => (f k x).isSome) (Std.Internal.List.getValueCast? k l)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
/-- The reduction of the graph `G` along partition `P` has edges between `ε`-uniform pairs of parts
that have edge density at least `δ`.  -/
SimpleGraph.regularityReduced : {α : Type u_1} →
  {𝕜 : Type u_2} →
    [Field 𝕜] →
      [LinearOrder 𝕜] →
        [inst : DecidableEq α] →
          {A : Finset α} → Finpartition A → (G : SimpleGraph α) → [DecidableRel G.Adj] → 𝕜 → 𝕜 → SimpleGraph α
-- Mathlib.Topology.Algebra.LinearTopology
IsLinearTopology.tendsto_mul_zero_of_right : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : TopologicalSpace R] [IsLinearTopology R R] {ι : Type u_2} {f : Filter ι}
  (a b : ι → R), Filter.Tendsto b f (nhds 0) → Filter.Tendsto (a * b) f (nhds 0)
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
/-- The `trajContent κ x₀` of a cylinder indexed by first coordinates is given by `partialTraj`.  -/
ProbabilityTheory.Kernel.trajContent_cylinder : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {a b : ℕ} {S : Set ((i : ↥(Finset.Iic b)) → X ↑i)},
  MeasurableSet S →
    ∀ (x₀ : (i : ↥(Finset.Iic a)) → X ↑i),
      (ProbabilityTheory.Kernel.trajContent κ x₀) (MeasureTheory.cylinder (Finset.Iic b) S) =
        ((ProbabilityTheory.Kernel.partialTraj κ a b) x₀) S
-- Mathlib.Algebra.Star.Subalgebra
/-- The `carrier` is closed under the `star` operation.  -/
StarSubalgebra.star_mem' : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A] [inst_3 : StarRing A]
  [inst_4 : Algebra R A] [inst_5 : StarModule R A] (self : StarSubalgebra R A) {a : A},
  a ∈ self.carrier → star a ∈ self.carrier
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.MVarErrorInfo.mk.injEq : ∀ (mvarId : Lean.MVarId) (ref : Lean.Syntax) (kind : Lean.Elab.Term.MVarErrorKind) (mvarId_1 : Lean.MVarId)
  (ref_1 : Lean.Syntax) (kind_1 : Lean.Elab.Term.MVarErrorKind),
  ({ mvarId := mvarId, ref := ref, kind := kind } = { mvarId := mvarId_1, ref := ref_1, kind := kind_1 }) =
    (mvarId = mvarId_1 ∧ ref = ref_1 ∧ kind = kind_1)
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_inter_le_size_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  (m₁ ∩ m₂).size ≤ m₁.size
-- Mathlib.Topology.Continuous
ContinuousAt.comp' : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y} {g : Y → Z} {x : X},
  ContinuousAt g (f x) → ContinuousAt f x → ContinuousAt (fun x => g (f x)) x
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- The sheaf sections functor on `X` is given by evaluation of presheaves on `X`.  -/
CategoryTheory.sheafSectionsNatIsoEvaluation : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (A : Type u₂) →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
          {X : C} →
            (CategoryTheory.sheafSections J A).obj (Opposite.op X) ≅
              (CategoryTheory.sheafToPresheaf J A).comp ((CategoryTheory.evaluation Cᵒᵖ A).obj (Opposite.op X))
-- Lean.Meta.Tactic.Grind.MatchCond
_private.Lean.Meta.Tactic.Grind.MatchCond.0.Lean.Meta.Grind.collectMatchCondLhssAndAbstract.go.match_1.eq_1 : ∀ (motive : Option Lean.Expr → Sort u_1) (α : Lean.Expr) (h_1 : (α : Lean.Expr) → motive (some α))
  (h_2 : (x : Option Lean.Expr) → motive x),
  (match some α with
    | some α => h_1 α
    | x => h_2 x) =
    h_1 α
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inr_f_descCochain_v_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain F K m) (β : CochainComplex.HomComplex.Cochain G K n) (h : m + 1 = n)
  (p₁ p₂ : ℤ) (h₁₂ : p₁ + n = p₂) {Z : C} (h_1 : K.X p₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f p₁)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.descCochain φ α β h).v p₁ p₂ h₁₂) h_1) =
    CategoryTheory.CategoryStruct.comp (β.v p₁ p₂ h₁₂) h_1
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
Submodule.range_subtypeL : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (p : Submodule R M), (↑p.subtypeL).range = p
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.toBasicOpenₗ_injective : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : R),
  Function.Injective ⇑(AlgebraicGeometry.StructureSheaf.toBasicOpenₗ✝ R M f)
-- Mathlib.Analysis.Complex.Hadamard
/-- Rewrite for `InterpStrip` when `0 < sSupNormIm f 0` and `0 < sSupNormIm f 1`.  -/
Complex.HadamardThreeLines.interpStrip_eq_of_pos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℂ → E) (z : ℂ),
  0 < Complex.HadamardThreeLines.sSupNormIm f 0 →
    0 < Complex.HadamardThreeLines.sSupNormIm f 1 →
      Complex.HadamardThreeLines.interpStrip f z =
        ↑(Complex.HadamardThreeLines.sSupNormIm f 0) ^ (1 - z) * ↑(Complex.HadamardThreeLines.sSupNormIm f 1) ^ z
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
/-- Any ball `Metric.ball x r`, `0 < r` is the image of the unit ball under `fun y ↦ x + r • y`.  -/
affinity_unitBall : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {r : ℝ},
  0 < r → ∀ (x : E), x +ᵥ r • Metric.ball 0 1 = Metric.ball x r
-- Mathlib.RingTheory.Extension.Cotangent.Basis
/-- The forward direction of the isomorphism `S ⊗[T] J/J² ≃ₗ[S] I/I²`.  -/
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.tensorCotangentHom : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {ι : Type u_4} →
            {P : Algebra.Generators R S ι} →
              {σ : Type u_5} →
                {b : Module.Basis σ S P.toExtension.Cotangent} →
                  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b) →
                    TensorProduct (Algebra.Generators.PresentationOfFreeCotangent.Aux.T✝ D) S
                        (Algebra.Generators.PresentationOfFreeCotangent.Aux.presLeft✝ D).toExtension.Cotangent →ₗ[S]
                      P.toExtension.Cotangent
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalExpr.instDataValue : Lean.Elab.ConfigEval.EvalExpr Lean.DataValue
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.aleph_le_beth : ∀ (o : Ordinal.{u_1}), Cardinal.aleph o ≤ Cardinal.beth o
-- Mathlib.RepresentationTheory.Continuous.TopRep
/-- The functor taking a topological `G`-representation to a topological `H`-representation
along a monoid homomorphism `φ : H →* G`.  -/
TopRep.resFunctor : {k : Type u} →
  [inst : TopologicalSpace k] →
    [inst_1 : Ring k] →
      {G : Type v} →
        [inst_2 : Group G] →
          {H : Type u_1} → [inst_3 : Monoid H] → (H →* G) → CategoryTheory.Functor (TopRep k G) (TopRep k H)
-- Lean.Message
Lean.instFromJsonSerialMessage.fromJson : Lean.Json → Except String Lean.SerialMessage
-- Init.Data.Nat.Gcd
Nat.gcd_mul_right_add_right : ∀ (m n k : ℕ), m.gcd (k * m + n) = m.gcd n
-- Mathlib.Algebra.CharP.Algebra
ExpChar.of_injective_algebraMap' : ∀ (R : Type u_1) {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] [FaithfulSMul R A]
  (q : ℕ) [ExpChar R q], ExpChar A q
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.gaussianPDFReal_def : ∀ (μ : ℝ) (v : NNReal),
  ProbabilityTheory.gaussianPDFReal μ v = fun x => (√(2 * Real.pi * ↑v))⁻¹ * Real.exp (-(x - μ) ^ 2 / (2 * ↑v))
-- Lean.Meta.AppBuilder
/-- Given `h₁ : f = g` and `h₂ : a = b`, returns a proof of `f a = g b`.  -/
Lean.Meta.mkCongr : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.const_mul_right : ∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] {S : Type u_17} [inst_1 : NormedRing S] [NormMulClass S] {f : α → E}
  {l : Filter α} {g : α → S} {c : S}, c ≠ 0 → f =O[l] g → f =O[l] fun x => c * g x
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.symm_trans_apply : ∀ {R : Type u_4} {S : Type u_5} {S' : Type u_6} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S]
  [inst_4 : Mul S'] [inst_5 : Add S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') (a : S'),
  (e₁.trans e₂).symm a = e₁.symm (e₂.symm a)
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_castAddEmb_Ioi : ∀ {n : ℕ} (m : ℕ) [inst : NeZero m] (i : Fin n),
  Finset.map (Fin.castAddEmb m) (Finset.Ioi i) = Finset.Ioo (Fin.castAdd m i) (Fin.natAdd n 0)
-- Lean.Structure
_private.Lean.Structure.0.Lean.getPathToBaseStructure?.go : Lean.Environment → Lean.Name → Lean.Name → List Lean.Name → OptionT (StateM Lean.NameSet) (List Lean.Name)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {a : α} {c : ℕ},
  (Std.DHashMap.Internal.Raw₀.emptyWithCapacity c).contains a = false
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instLattice : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} →
        [inst_1 : TopologicalSpace β] → [inst_2 : Lattice β] → [TopologicalLattice β] → Lattice (α →ₘ[μ] β)
-- Mathlib.Topology.Algebra.AsymptoticCone
Filter.Tendsto.atTop_smul_nhds_tendsto_asymptoticNhds : ∀ {k : Type u_1} {V : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : TopologicalSpace V] {α : Type u_4} {l : Filter α} [inst_5 : TopologicalSpace k]
  [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] {f : α → k} {g : α → V}
  {v : V},
  Filter.Tendsto f l Filter.atTop →
    Filter.Tendsto g l (nhds v) → Filter.Tendsto (fun x => f x • g x) l (AffineSpace.asymptoticNhds k V v)
-- Mathlib.Analysis.Convex.Join
convexHull_union : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {s t : Set E},
  s.Nonempty → t.Nonempty → (convexHull 𝕜) (s ∪ t) = convexJoin 𝕜 ((convexHull 𝕜) s) ((convexHull 𝕜) t)
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.op_toSubmonoid : ∀ {R : Type u_2} [inst : NonAssocSemiring R] (S : Subsemiring R), S.op.toSubmonoid = S.op
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
/-- Evaluating the pointwise product `k ↦ ∏ᶜ fun (s : α) => (F s).obj (k s)` at `d` is the same as
taking the pointwise product `k ↦ ∏ᶜ fun (s : α) => ((F s).obj (k s)).obj d`.  -/
CategoryTheory.Limits.pointwiseProductCompEvaluation : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {α : Type u_3} →
          {I : α → Type u_4} →
            [inst_2 : (i : α) → CategoryTheory.Category.{u_5, u_4} (I i)] →
              [inst_3 : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete α) C] →
                (F : (i : α) → CategoryTheory.Functor (I i) (CategoryTheory.Functor D C)) →
                  (d : D) →
                    (CategoryTheory.Limits.pointwiseProduct F).comp ((CategoryTheory.evaluation D C).obj d) ≅
                      CategoryTheory.Limits.pointwiseProduct fun s => (F s).comp ((CategoryTheory.evaluation D C).obj d)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.ExprCnstr.toPoly.eq_1 : ∀ (c : Nat.Internal.Linear.ExprCnstr), c.toPoly = { eq := c.eq, lhs := c.lhs.toPoly, rhs := c.rhs.toPoly }
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.nnnorm : ∀ {α : Type u_1} {x : MeasurableSpace α} {β : Type u_5} [inst : SeminormedAddCommGroup β] {f : α → β},
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun x => ‖f x‖₊
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_empty : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [inst_2 : Inhabited β] {a : α},
  Std.DHashMap.Raw.Const.get! ∅ a = default
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.inter_smul_subset : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s₁ s₂ : Finset α} {t : Finset β}
  [inst_2 : DecidableEq α], (s₁ ∩ s₂) • t ⊆ s₁ • t ∩ s₂ • t
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.ValueGroup₀.restrict₀_surjective : ∀ {A : Type u_1} {B : Type u_2} [inst : GroupWithZero A] [inst_1 : GroupWithZero B] (f : A →*₀ B),
  Function.Surjective ⇑(MonoidWithZeroHom.ValueGroup₀.restrict₀ f)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKeyD_alter_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [Inhabited α] {k fallback : α} {f : Option β → Option β},
  (Std.ExtDTreeMap.Const.alter t k f).getKeyD k fallback =
    if (f (Std.ExtDTreeMap.Const.get? t k)).isSome = true then k else fallback
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.units_smul : ∀ {S : Type u_1} {R : Type u_2} {M : Type u_3} [inst : SetLike S M] [inst_1 : Monoid R] [inst_2 : MulAction R M]
  [SMulMemClass S R M] (s : S) (r : Rˣ), r • ↑s = ↑s
-- Mathlib.Geometry.Manifold.Instances.Real
instInhabitedEuclideanQuadrant : {n : ℕ} → Inhabited (EuclideanQuadrant n)
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
/-- The `j`th face of codimension `1` of the `i`-th horn.  -/
SSet.horn.face : {n : ℕ} → (i j : Fin (n + 2)) → j ≠ i → (SSet.horn (n + 1) i).toSSet.obj (Opposite.op { len := n })
-- Init.Data.Order.PackageFactories
Std.Packages.LinearOrderOfLEArgs.mk.inj : ∀ {α : Type u} {toLinearPreorderOfLEArgs : Std.Packages.LinearPreorderOfLEArgs α}
  {le_antisymm :
    autoParam
      (let this := toLinearPreorderOfLEArgs.le;
      ∀ (a b : α), a ≤ b → b ≤ a → a = b)
      Std.Packages.PartialOrderOfLEArgs.le_antisymm._autoParam}
  {min :
    autoParam
      (let this := toLinearPreorderOfLEArgs.le;
      let this := toLinearPreorderOfLEArgs.decidableLE;
      Min α)
      Std.Packages.LinearOrderOfLEArgs.min._autoParam}
  {max :
    autoParam
      (let this := toLinearPreorderOfLEArgs.le;
      let this := toLinearPreorderOfLEArgs.decidableLE;
      Max α)
      Std.Packages.LinearOrderOfLEArgs.max._autoParam}
  {min_eq :
    autoParam
      (let this := toLinearPreorderOfLEArgs.le;
      let this_1 := toLinearPreorderOfLEArgs.decidableLE;
      let this_2 := min;
      ∀ (a b : α), a ⊓ b = if a ≤ b then a else b)
      Std.Packages.LinearOrderOfLEArgs.min_eq._autoParam}
  {max_eq :
    autoParam
      (let this := toLinearPreorderOfLEArgs.le;
      let this_1 := toLinearPreorderOfLEArgs.decidableLE;
      let this_2 := max;
      ∀ (a b : α), a ⊔ b = if b ≤ a then a else b)
      Std.Packages.LinearOrderOfLEArgs.max_eq._autoParam}
  {toLinearPreorderOfLEArgs_1 : Std.Packages.LinearPreorderOfLEArgs α}
  {le_antisymm_1 :
    autoParam
      (let this := toLinearPreorderOfLEArgs_1.le;
      ∀ (a b : α), a ≤ b → b ≤ a → a = b)
      Std.Packages.PartialOrderOfLEArgs.le_antisymm._autoParam}
  {min_1 :
    autoParam
      (let this := toLinearPreorderOfLEArgs_1.le;
      let this := toLinearPreorderOfLEArgs_1.decidableLE;
      Min α)
      Std.Packages.LinearOrderOfLEArgs.min._autoParam}
  {max_1 :
    autoParam
      (let this := toLinearPreorderOfLEArgs_1.le;
      let this := toLinearPreorderOfLEArgs_1.decidableLE;
      Max α)
      Std.Packages.LinearOrderOfLEArgs.max._autoParam}
  {min_eq_1 :
    autoParam
      (let this := toLinearPreorderOfLEArgs_1.le;
      let this_1 := toLinearPreorderOfLEArgs_1.decidableLE;
      let this_2 := min_1;
      ∀ (a b : α), a ⊓ b = if a ≤ b then a else b)
      Std.Packages.LinearOrderOfLEArgs.min_eq._autoParam}
  {max_eq_1 :
    autoParam
      (let this := toLinearPreorderOfLEArgs_1.le;
      let this_1 := toLinearPreorderOfLEArgs_1.decidableLE;
      let this_2 := max_1;
      ∀ (a b : α), a ⊔ b = if b ≤ a then a else b)
      Std.Packages.LinearOrderOfLEArgs.max_eq._autoParam},
  { toLinearPreorderOfLEArgs := toLinearPreorderOfLEArgs, le_antisymm := le_antisymm, min := min, max := max,
        min_eq := min_eq, max_eq := max_eq } =
      { toLinearPreorderOfLEArgs := toLinearPreorderOfLEArgs_1, le_antisymm := le_antisymm_1, min := min_1,
        max := max_1, min_eq := min_eq_1, max_eq := max_eq_1 } →
    toLinearPreorderOfLEArgs = toLinearPreorderOfLEArgs_1 ∧ min = min_1 ∧ max = max_1
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isCoseparator_coseparator : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.HasCoseparator C],
  CategoryTheory.IsCoseparator (CategoryTheory.coseparator C)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.List.filterMapM_cons.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Lean.Data.Lsp.Basic
/-- An item to transfer a text document from the client to the server.

[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocumentItem)
 -/
Lean.Lsp.TextDocumentItem : Type
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.instEpiFactorThruImageSubobjectOfHasEqualizers : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasImage f] [CategoryTheory.Limits.HasEqualizers C],
  CategoryTheory.Epi (CategoryTheory.Limits.factorThruImageSubobject f)
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_apply : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens)
  (x : ↑(Y.presheaf.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom
        (AlgebraicGeometry.Scheme.Hom.appLE f (AlgebraicGeometry.Scheme.Hom.opensRange f ⊓ U)
          ((TopologicalSpace.Opens.map f.base).obj U) ⋯))
      ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op)) x) =
    (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app f U)) x
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.repr_reindex : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (b : Module.Basis ι R M) (x : M) (e : ι ≃ ι'),
  (b.reindex e).repr x = Finsupp.mapDomain (⇑e) (b.repr x)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstr.lhs : Lean.Meta.Grind.AC.EqCnstr → Lean.Grind.AC.Seq
-- Mathlib.Order.Basic
dense_or_discrete : ∀ {α : Type u_2} [inst : LinearOrder α] (a₁ a₂ : α),
  (∃ a, a₁ < a ∧ a < a₂) ∨ (∀ (a : α), a₁ < a → a₂ ≤ a) ∧ ∀ a < a₂, a ≤ a₁
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- The range of a surjective ring homomorphism is the whole of the codomain.  -/
NonUnitalRingHom.range_eq_top_of_surjective : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] (f : R →ₙ+* S),
  Function.Surjective ⇑f → f.range = ⊤
-- Std.Data.ExtDTreeMap.Basic
/-- Given a proof that such a mapping exists, retrieves the key-value pair with the largest key that is
less than the given key.
 -/
Std.ExtDTreeMap.getEntryLT : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [inst : Std.TransCmp cmp] →
        (t : Std.ExtDTreeMap α β cmp) → (k : α) → (∃ a ∈ t, cmp a k = Ordering.lt) → (a : α) × β a
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
right_sub_midpoint : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V] [inst_3 : Module R V]
  (v₁ v₂ : V), v₂ - midpoint R v₁ v₂ = ⅟2 • (v₂ - v₁)