mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.div.injEq : ∀ (k : ℤ) (y? : Option Int.Internal.Linear.Var) (c : Lean.Meta.Grind.Arith.Cutsat.EqCnstr) (k_1 : ℤ)
  (y?_1 : Option Int.Internal.Linear.Var) (c_1 : Lean.Meta.Grind.Arith.Cutsat.EqCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.div k y? c = Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.div k_1 y?_1 c_1) =
    (k = k_1 ∧ y? = y?_1 ∧ c = c_1)
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.flip_comp_evaluation : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A (CategoryTheory.Functor B C)) (a : A),
  F.flip.comp ((CategoryTheory.evaluation A C).obj a) = F.obj a
-- Lean.Util.HasConstCache
Lean.HasConstCache.cache : {declNames : Array Lean.Name} → Lean.HasConstCache declNames → Std.HashMap.Raw Lean.Expr Bool
-- Std.Data.DHashMap.Internal.Model
/-- This is the general theorem used to show that access operations involving a proof (like `get`)
are correct.  -/
Std.DHashMap.Internal.apply_bucket_with_proof : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : PartialEquivBEq α]
  [LawfulHashable α] {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ (a : α)
      (f :
        (a : α) → (l : Std.DHashMap.Internal.AssocList α β) → Std.DHashMap.Internal.AssocList.contains a l = true → γ a)
      (g : (a : α) → (l : List ((a : α) × β a)) → Std.Internal.List.containsKey a l = true → γ a),
      (∀ {a : α} {l : Std.DHashMap.Internal.AssocList α β} {h : Std.DHashMap.Internal.AssocList.contains a l = true},
          f a l h = g a l.toList ⋯) →
        (∀ {l l' : List ((a : α) × β a)} {a : α} {h : Std.Internal.List.containsKey a l = true},
            Std.Internal.List.DistinctKeys l → ∀ (hl' : l.Perm l'), g a l h = g a l' ⋯) →
          ∀ {h : Std.DHashMap.Internal.AssocList.contains a (Std.DHashMap.Internal.bucket (↑m).buckets ⋯ a) = true}
            {h' : Std.Internal.List.containsKey a (Std.DHashMap.Internal.toListModel (↑m).buckets) = true},
            (∀ {l l' : List ((a : α) × β a)} {a : α} {h : Std.Internal.List.containsKey a (l ++ l') = true}
                (hl' : Std.Internal.List.containsKey a l' = false), g a (l ++ l') h = g a l ⋯) →
              f a (Std.DHashMap.Internal.bucket (↑m).buckets ⋯ a) h =
                g a (Std.DHashMap.Internal.toListModel (↑m).buckets) h'
-- Mathlib.Algebra.Order.Hom.TypeTags
/-- Reinterpret `G ≃+o H` as `Multiplicative G ≃*o Multiplicative H`.  -/
OrderAddMonoidIso.toMultiplicative : {G : Type u_1} →
  {H : Type u_2} →
    [inst : AddCommMonoid G] →
      [inst_1 : PartialOrder G] →
        [inst_2 : AddCommMonoid H] → [inst_3 : PartialOrder H] → (G ≃+o H) ≃ (Multiplicative G ≃*o Multiplicative H)
-- Mathlib.Order.Compare
Ordering.Compares.le_antisymm : ∀ {α : Type u_1} [inst : Preorder α] {a b : α} {o : Ordering}, o.Compares a b → a ≤ b → b ≤ a → a = b
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation
/-- Corollary of `integrableOn_cartanKernel`: If `f : ℂ → ℂ` is meromorphic, then the function
`β ↦ ∫ α in 0..2 * π, Cartan.cartanKernel f R α β` is integrable.
 -/
ValueDistribution.Cartan.integrableOn_intervalIntegral_cartanKernel_left : ∀ {f : ℂ → ℂ} {R : ℝ},
  Meromorphic f →
    MeasureTheory.IntegrableOn (fun x => ∫ (α : ℝ) in 0..2 * Real.pi, ValueDistribution.Cartan.cartanKernel f R α x)
      (Set.Ioc 0 (2 * Real.pi)) MeasureTheory.volume
-- Mathlib.AlgebraicTopology.DoldKan.Degeneracies
AlgebraicTopology.DoldKan.DegeneraciesVanish.σ_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} {n : ℕ} {T : C} {f : X.obj (Opposite.op { len := n + 1 }) ⟶ T},
  AlgebraicTopology.DoldKan.DegeneraciesVanish f → ∀ (i : Fin (n + 1)), CategoryTheory.CategoryStruct.comp (X.σ i) f = 0
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- Whiskering a 1-morphism is a functor.  -/
CategoryTheory.Bicategory.LeftExtension.whiskering : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : a ⟶ b} →
        {g : a ⟶ c} →
          {x : B} →
            (h : c ⟶ x) →
              CategoryTheory.Functor (CategoryTheory.Bicategory.LeftExtension f g)
                (CategoryTheory.Bicategory.LeftExtension f (CategoryTheory.CategoryStruct.comp g h))
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.IsTotallyReal.complexEmbedding_isReal : ∀ {K : Type u_2} [inst : Field K] [NumberField.IsTotallyReal K] (φ : K →+* ℂ), NumberField.ComplexEmbedding.IsReal φ
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.tilted_of_not_aemeasurable : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ}, ¬AEMeasurable f μ → μ.tilted f = 0
-- Mathlib.Order.Lattice
inf_eq_inf_iff_right : ∀ {α : Type u} [inst : SemilatticeInf α] {a b c : α}, a ⊓ c = b ⊓ c ↔ b ⊓ c ≤ a ∧ a ⊓ c ≤ b
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.le_induce_union : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {s s' : Set V}, G'.induce s ⊔ G'.induce s' ≤ G'.induce (s ∪ s')
-- Mathlib.Logic.Relation
Relation.TransGen.swap : ∀ {α : Type u_1} {r : α → α → Prop}, Function.swap (Relation.TransGen r) ≤ Relation.TransGen (Function.swap r)
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.biprod_inl_snd_f : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (K L : HomologicalComplex C c)
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] (i : ι),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inl.f i) (CategoryTheory.Limits.biprod.snd.f i) = 0
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.instOne : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : SMulCommClass 𝕜 A A] → [inst_4 : IsScalarTower 𝕜 A A] → One (DoubleCentralizer 𝕜 A)
-- Std.Do.WP.Sound
/-- Soundness lemma for `Id.run`. Derived from `WPSound.of_wp_canReturn`: `Id.run prog = x`
is the `MonadAttach.CanReturn prog x` witness.
 -/
Std.Do.Id.of_wp_run_eq : ∀ {α : Type u} {x : α} {prog : Id α},
  prog.run = x → ∀ (P : α → Prop), (⊢ₛ (Std.Do.wp prog).apply (Std.Do.PostCond.noThrow fun a => { down := P a })) → P x
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.generates_reverse_comm : ∀ {T : Type u_1} {g : ContextFreeGrammar T} {u : List (Symbol T g.NT)}, g.reverse.Generates u ↔ g.Generates u.reverse
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
CategoryTheory.HasSplitCoequalizer.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y},
  (∃ Z h, Nonempty (CategoryTheory.IsSplitCoequalizer f g h)) → CategoryTheory.HasSplitCoequalizer f g
-- Mathlib.Dynamics.PeriodicPts.Lemmas
/-- This `sInf` can be regarded as a generalized version of LCM
for possibly infinite sets and types.  -/
Function.minimalPeriod_piMap : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → α i → α i} {x : (i : ι) → α i},
  Function.minimalPeriod (Pi.map f) x = sInf {n | n > 0 ∧ ∀ (i : ι), Function.minimalPeriod (f i) (x i) ∣ n}
-- Mathlib.RingTheory.WittVector.Basic
WittVector.instNontrivial : ∀ {p : ℕ} {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] [Nontrivial R], Nontrivial (WittVector p R)
-- Init.Data.UInt.Bitwise
instCommutativeUInt64HOr : Std.Commutative fun x1 x2 => x1 ||| x2
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.IsRkFinite.sdiff_singleton_iff : ∀ {α : Type u_1} {M : Matroid α} {X : Set α} {e : α}, M.IsRkFinite (X \ {e}) ↔ M.IsRkFinite X
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.getKeyGT!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getKeyGT! k = t₂.getKeyGT! k
-- Mathlib.Tactic.Widget.StringDiagram
/-- Display the string diagrams if the goal is an equality of morphisms in a monoidal category.  -/
Mathlib.Tactic.Widget.StringDiagram : ProofWidgets.Component ProofWidgets.PanelWidgetProps
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.shortComplexH1.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{max u u_1, u, u} k G),
  groupCohomology.shortComplexH1 A =
    { X₁ := ModuleCat.of k ↑A, X₂ := ModuleCat.of k (G → ↑A), X₃ := ModuleCat.of k (G × G → ↑A),
      f := groupCohomology.d₀₁ A, g := groupCohomology.d₁₂ A, zero := ⋯ }
-- Init.Data.BitVec.Bitblast
BitVec.DivModArgs.mk.inj : ∀ {w : ℕ} {n d n_1 d_1 : BitVec w}, { n := n, d := d } = { n := n_1, d := d_1 } → n = n_1 ∧ d = d_1
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.size_eq_match_roi : ∀ {α : Type u} {r : Std.Rii α} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.Rxi.HasSize α] [Std.PRange.LawfulUpwardEnumerable α] [Std.Rxi.IsAlwaysFinite α]
  [Std.Rxi.LawfulHasSize α],
  r.size =
    match Std.PRange.least? with
    | none => 0
    | some next => next<...*.size + 1
-- Lean.Data.Lsp.Client
Lean.Lsp.RegistrationParams.mk.sizeOf_spec : ∀ (registrations : Array Lean.Lsp.Registration), sizeOf { registrations := registrations } = 1 + sizeOf registrations
-- Batteries.Data.List.Lemmas
List.foldlIdx_nil : ∀ {α : Type u_1} {α_1 : Sort u_2} {f : ℕ → α_1 → α → α_1} {i : α_1} {s : ℕ}, List.foldlIdx f i [] s = i
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- The action by an intermediate field is the action by the underlying field.  -/
IntermediateField.instModuleSubtypeMem : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          {X : Type u_4} → [inst_3 : AddCommMonoid X] → [Module L X] → (F : IntermediateField K L) → Module (↥F) X
-- Init.Data.BitVec.Bitblast
BitVec.getMsbD_add : ∀ {w i : ℕ} {i_lt : i < w} {x y : BitVec w},
  (x + y).getMsbD i = (x.getMsbD i ^^ (y.getMsbD i ^^ BitVec.carry (w - 1 - i) x y false))
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
/-- An open ball centred at the origin in a valued ring is open.  -/
Valued.isOpen_ball : ∀ (R : Type u) [inst : Ring R] {Γ₀ : Type v} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀]
  (r : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀), IsOpen {x | Valued.v.restrict x < r}
-- Mathlib.RingTheory.WittVector.Truncated
WittVector.truncate_mk' : ∀ (p n : ℕ) {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (f : ℕ → R),
  (WittVector.truncate n) { coeff := f } = TruncatedWittVector.mk p fun k => f ↑k
-- Lean.Data.AssocList
Lean.AssocList.cons : {α : Type u} → {β : Type v} → α → β → Lean.AssocList α β → Lean.AssocList α β
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- If `f₁` and `f₂` have equal order at `x` and if their trailing coefficients do not cancel, then the
trailing coefficient of `f₁ - f₂` at `x` is the sum of the trailing coefficients.
 -/
MeromorphicAt.meromorphicTrailingCoeffAt_sub_eq_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f₁ f₂ : 𝕜 → E},
  MeromorphicAt f₁ x →
    MeromorphicAt f₂ x →
      meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x →
        meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x ≠ 0 →
          meromorphicTrailingCoeffAt (f₁ - f₂) x = meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x
-- Mathlib.MeasureTheory.Covering.OneDim
Real.tendsto_Icc_vitaliFamily_left : ∀ (x : ℝ),
  Filter.Tendsto (fun y => Set.Icc y x) (nhdsWithin x (Set.Iio x))
    ((IsUnifLocDoublingMeasure.vitaliFamily MeasureTheory.volume 1).filterAt x)
-- Mathlib.Topology.Algebra.Module.IsWeak
/-- `E` is a `IsTopologicalAddGroup` when `E` is equipped with a `LinearMap.IsWeak` topology.  -/
LinearMap.IsWeak.isTopologicalAddGroup : ∀ {𝕜 : Type u_7} {E : Type u_8} {F : Type u_9} [inst : CommRing 𝕜] [inst_1 : TopologicalSpace 𝕜]
  [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace E] [ContinuousAdd 𝕜] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [hB : B.IsWeak], IsTopologicalAddGroup E
-- Lean.Widget.InteractiveGoal
Lean.Widget.InteractiveGoalCore.hyps : Lean.Widget.InteractiveGoalCore → Array Lean.Widget.InteractiveHypothesisBundle
-- Mathlib.Order.Lattice
Monotone.map_sup : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : SemilatticeSup β] {f : α → β},
  Monotone f → ∀ (x y : α), f (max x y) = f x ⊔ f y
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extendCyclesIso_hom_naturality : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {K L : HomologicalComplex C c} (φ : K ⟶ L) (e : c.Embedding c')
  {j : ι} {j' : ι'} (hj' : e.f j = j') [inst_3 : K.HasHomology j] [inst_4 : L.HasHomology j]
  [inst_5 : (K.extend e).HasHomology j'] [inst_6 : (L.extend e).HasHomology j'],
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap (HomologicalComplex.extendMap φ e) j')
      (L.extendCyclesIso e hj').hom =
    CategoryTheory.CategoryStruct.comp (K.extendCyclesIso e hj').hom (HomologicalComplex.cyclesMap φ j)
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
Finset.invMulSubgroup.congr_simp : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (A A_1 : Finset G) (e_A : A = A_1)
  (h : ↑(A * A).card < 3 / 2 * ↑A.card), A.invMulSubgroup h = A_1.invMulSubgroup ⋯
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.exp_eq_one : ∀ {r : ℝ}, Circle.exp r = 1 ↔ ∃ n, r = ↑n * (2 * Real.pi)
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.lsub_le_of_range_subset : ∀ {ι : Type u} {ι' : Type v} {f : ι → Ordinal.{max (max u v) w}} {g : ι' → Ordinal.{max (max u v) w}},
  Set.range f ⊆ Set.range g → Ordinal.lsub f ≤ Ordinal.lsub g
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.ExtraTheorem.const.sizeOf_spec : ∀ (declName : Lean.Name), sizeOf (Lean.Elab.Tactic.Grind.ExtraTheorem.const declName) = 1 + sizeOf declName
-- Mathlib.MeasureTheory.Measure.AddContent
/-- If an additive content is σ-additive on a set ring, then the content of a monotone sequence of
sets tends to the content of the union.  -/
MeasureTheory.tendsto_atTop_addContent_iUnion_of_addContent_iUnion_eq_tsum : ∀ {α : Type u_1} {C : Set (Set α)} {m : MeasureTheory.AddContent ENNReal C},
  MeasureTheory.IsSetRing C →
    (∀ (f : ℕ → Set α),
        (∀ (i : ℕ), f i ∈ C) →
          ⋃ i, f i ∈ C → Pairwise (Function.onFun Disjoint f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)) →
      ∀ ⦃f : ℕ → Set α⦄,
        Monotone f →
          (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Filter.Tendsto (fun n => m (f n)) Filter.atTop (nhds (m (⋃ i, f i)))
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- The push-forward of a finite measure by a function between measurable spaces as a linear map.  -/
MeasureTheory.FiniteMeasure.mapHom : {Ω : Type u_1} →
  {Ω' : Type u_2} →
    [inst : MeasurableSpace Ω] →
      [inst_1 : MeasurableSpace Ω'] →
        {f : Ω → Ω'} → Measurable f → MeasureTheory.FiniteMeasure Ω →ₗ[NNReal] MeasureTheory.FiniteMeasure Ω'
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Subsemigroup.nonUnitalSubsemiringClosure_coe : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (M : Subsemigroup R),
  ↑M.nonUnitalSubsemiringClosure = ↑(AddSubmonoid.closure ↑M)
-- Mathlib.Analysis.InnerProductSpace.ExteriorPower
exteriorPower.inner_ιMulti_self : ∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  (x : Fin n → E), inner ℝ ((exteriorPower.ιMulti ℝ n) x) ((exteriorPower.ιMulti ℝ n) x) = (Matrix.gram ℝ x).det
-- Mathlib.Analysis.Normed.Group.NullSubmodule
/-- The null subgroup with respect to the norm.  -/
nullSubgroup : (M : Type u_1) → [inst : SeminormedCommGroup M] → Subgroup M
-- Lean.Data.Lsp.Workspace
Lean.Lsp.FileEvent.mk.sizeOf_spec : ∀ (uri : Lean.Lsp.DocumentUri) (type : Lean.Lsp.FileChangeType),
  sizeOf { uri := uri, type := type } = 1 + sizeOf uri + sizeOf type
-- Mathlib.Data.Sum.Interval
Sum.Ico_inr_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] (b₁ b₂ : β),
  Finset.Ico (Sum.inr b₁) (Sum.inr b₂) = Finset.map Function.Embedding.inr (Finset.Ico b₁ b₂)
-- Init.Prelude
Lean.Name.brecOn.eq : ∀ {motive : Lean.Name → Sort u} (t : Lean.Name) (F_1 : (t : Lean.Name) → Lean.Name.below t → motive t),
  Lean.Name.brecOn t F_1 = F_1 t (Lean.Name.brecOn.go t F_1).2
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHomClass.toContinuousMapClass : ∀ {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} {inst : Preorder α} {inst_1 : Preorder β}
  {inst_2 : TopologicalSpace α} {inst_3 : TopologicalSpace β} {inst_4 : FunLike F α β}
  [self : ContinuousOrderHomClass F α β], ContinuousMapClass F α β
-- Init.GetElem
/-- The syntax `arr[i]` gets the `i`'th element of the collection `arr`. If there
are proof side conditions to the application, they will be automatically
inferred by the `get_elem_tactic` tactic.


Conventions for notations in identifiers:

 * The recommended spelling of `xs[i]'h` in identifiers is `getElem`. -/
«term__[_]'_» : Lean.TrailingParserDescr
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
/-- The underlying simplicial set of a subcomplex.  -/
SSet.Subcomplex.toSSet : {X : SSet} → X.Subcomplex → SSet
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.add_lt_add_of_lt_of_le : ∀ {α : Type u} [inst : Add α] {w x y z : WithBot α} [inst_1 : Preorder α] [AddLeftMono α] [AddRightStrictMono α],
  x ≠ ⊥ → w < y → x ≤ z → w + x < y + z
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.setLIntegral_compProd : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ]
  {f : α × β → ENNReal},
  Measurable f →
    ∀ {s : Set α},
      MeasurableSet s →
        ∀ {t : Set β},
          MeasurableSet t →
            ∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ.compProd κ = ∫⁻ (a : α) in s, ∫⁻ (b : β) in t, f (a, b) ∂κ a ∂μ
-- Mathlib.AlgebraicGeometry.Cover.Directed
/-- A directed `P`-cover of a scheme `X` is a cover `𝒰` with an ordering
on the indices and compatible transition maps `𝒰ᵢ ⟶ 𝒰ⱼ` for `i ≤ j` such that
every `x : 𝒰ᵢ ×[X] 𝒰ⱼ` comes from some `𝒰ₖ` for a `k ≤ i` and `k ≤ j`.  -/
AlgebraicGeometry.Scheme.Cover.LocallyDirected : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {X : AlgebraicGeometry.Scheme} →
    (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) →
      [CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] → Type (max (max u u_1) v_1)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
/-- `zeroLocus` and `vanishingIdeal` form a Galois connection.  -/
ProjectiveSpectrum.gc_set : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜],
  GaloisConnection (fun s => ProjectiveSpectrum.zeroLocus 𝒜 s) fun t => ↑(ProjectiveSpectrum.vanishingIdeal t)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.max!_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → t.isEmpty = false → t.max! ∈ t
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.instModuleCotangent : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {P : Algebra.Extension R S} →
            {R₀ : Type u_1} → [inst_3 : CommRing R₀] → [Algebra R₀ S] → Module R₀ P.Cotangent
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.const_apply : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {m' : MeasurableSpace Ω} {hm' : m' ≤ m}
  (i : ι), ↑(MeasureTheory.Filtration.const ι m' hm') i = m'
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getEntry.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) (x : Std.DHashMap.Internal.AssocList α β)
  (x_1 : Std.DHashMap.Internal.AssocList.contains a x = true),
  Std.DHashMap.Internal.AssocList.getEntry a x x_1 =
    match x, x_1 with
    | Std.DHashMap.Internal.AssocList.cons k v es, h =>
      if hka : (k == a) = true then ⟨k, v⟩ else Std.DHashMap.Internal.AssocList.getEntry a es ⋯
-- Init.Data.List.Range
List.range_add : ∀ {n m : ℕ}, List.range (n + m) = List.range n ++ List.map (fun x => n + x) (List.range m)
-- Mathlib.Analysis.BoxIntegral.Integrability
/-- For a simple function, its McShane (or Henstock, or `⊥`) box integral is equal to its
integral in the sense of `MeasureTheory.SimpleFunc.integral`.  -/
MeasureTheory.SimpleFunc.box_integral_eq_integral : ∀ {ι : Type u} {E : Type v} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  (f : MeasureTheory.SimpleFunc (ι → ℝ) E) (μ : MeasureTheory.Measure (ι → ℝ))
  [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ] (I : BoxIntegral.Box ι) (l : BoxIntegral.IntegrationParams),
  l.bRiemann = false →
    BoxIntegral.integral I l (⇑f) μ.toBoxAdditive.toSMul = MeasureTheory.SimpleFunc.integral (μ.restrict ↑I) f
-- Init.System.IO
_private.Init.System.IO.0.IO.eprintlnAux : String → IO Unit
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
/-- Returns `true` if `x` has been eliminated using an equality constraint.  -/
Lean.Meta.Grind.Arith.Linear.eliminated : Lean.Grind.Linarith.Var → Lean.Meta.Grind.Arith.Linear.LinearM Bool
-- Mathlib.LinearAlgebra.SModEq.Basic
Submodule.vadd_set_subset_vadd_set_iff : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {U : Submodule R M}
  {x y : M}, x +ᵥ ↑U ⊆ y +ᵥ ↑U ↔ x ≡ y [SMOD U]
-- Mathlib.Order.Extension.Linear
/-- The embedding of `α` into `LinearExtension α` as an order homomorphism.  -/
toLinearExtension : {α : Type u} → [inst : PartialOrder α] → α →o LinearExtension α
-- Mathlib.Topology.Algebra.Valued.WithVal
/-- **Alias** of `WithVal.apply_ofVal`. -/
WithVal.apply_equiv : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  (r : WithVal v), v r.ofVal = Valued.v r
-- Mathlib.Order.Atoms
CompleteLattice.isCoatomistic_iff : ∀ {α : Type u_4} [inst : CompleteLattice α], IsCoatomistic α ↔ ∀ (b : α), ∃ s, b = sInf s ∧ ∀ a ∈ s, IsCoatom a
-- Mathlib.CategoryTheory.Sites.Precoverage
/-- Pullbacks are preserved by a functor `F : C ⥤ D` for the precoverage `J` on `C` if
`F` preserves all pairwise pullbacks of presieves in `J`.  -/
CategoryTheory.Precoverage.PullbacksPreservedBy : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] → CategoryTheory.Precoverage C → CategoryTheory.Functor C D → Prop
-- Lean.Syntax
_private.Lean.Syntax.0.Lean.Syntax.identComponents.nameComps : Lean.Name → Option ℕ → List Lean.Name
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.Eval.Result.mk : Mathlib.Tactic.BicategoryLike.NormalExpr → Lean.Expr → Mathlib.Tactic.BicategoryLike.Eval.Result
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.Weight.mk.inj : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} {inst : CommRing R} {inst_1 : LieRing L} {inst_2 : LieAlgebra R L}
  {inst_3 : AddCommGroup M} {inst_4 : Module R M} {inst_5 : LieRingModule L M} {inst_6 : LieModule R L M}
  {inst_7 : LieRing.IsNilpotent L} {toFun : L → R} {genWeightSpace_ne_bot' : LieModule.genWeightSpace M toFun ≠ ⊥}
  {toFun_1 : L → R} {genWeightSpace_ne_bot'_1 : LieModule.genWeightSpace M toFun_1 ≠ ⊥},
  { toFun := toFun, genWeightSpace_ne_bot' := genWeightSpace_ne_bot' } =
      { toFun := toFun_1, genWeightSpace_ne_bot' := genWeightSpace_ne_bot'_1 } →
    toFun = toFun_1