mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.DeclModifiers
Lean.Elab.Modifiers.mk.inj : ∀ {stx : Lean.TSyntax `Lean.Parser.Command.declModifiers}
  {docString? : Option (Lean.TSyntax `Lean.Parser.Command.docComment)} {visibility : Lean.Elab.Visibility}
  {isProtected : Bool} {computeKind : Lean.Elab.ComputeKind} {recKind : Lean.Elab.RecKind} {isUnsafe : Bool}
  {attrs : Array Lean.Elab.Attribute} {stx_1 : Lean.TSyntax `Lean.Parser.Command.declModifiers}
  {docString?_1 : Option (Lean.TSyntax `Lean.Parser.Command.docComment)} {visibility_1 : Lean.Elab.Visibility}
  {isProtected_1 : Bool} {computeKind_1 : Lean.Elab.ComputeKind} {recKind_1 : Lean.Elab.RecKind} {isUnsafe_1 : Bool}
  {attrs_1 : Array Lean.Elab.Attribute},
  { stx := stx, docString? := docString?, visibility := visibility, isProtected := isProtected,
        computeKind := computeKind, recKind := recKind, isUnsafe := isUnsafe, attrs := attrs } =
      { stx := stx_1, docString? := docString?_1, visibility := visibility_1, isProtected := isProtected_1,
        computeKind := computeKind_1, recKind := recKind_1, isUnsafe := isUnsafe_1, attrs := attrs_1 } →
    stx = stx_1 ∧
      docString? = docString?_1 ∧
        visibility = visibility_1 ∧
          isProtected = isProtected_1 ∧
            computeKind = computeKind_1 ∧ recKind = recKind_1 ∧ isUnsafe = isUnsafe_1 ∧ attrs = attrs_1
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
lt_add_neg_iff_lt : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddRightStrictMono α] {a b : α}, 0 < a + -b ↔ b < a
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.counitIso_inv_app_tensor_comp_functor_map_δ_inverse_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [e.IsMonoidal] (X Y : C) {Z : D}
  (h :
    e.functor.obj
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (e.inverse.obj (e.functor.obj X))
          (e.inverse.obj (e.functor.obj Y))) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (e.counitIso.inv.app (CategoryTheory.MonoidalCategoryStruct.tensorObj (e.functor.obj X) (e.functor.obj Y)))
      (CategoryTheory.CategoryStruct.comp
        (e.functor.map (CategoryTheory.Functor.OplaxMonoidal.δ e.inverse (e.functor.obj X) (e.functor.obj Y))) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ e.functor X Y)
      (CategoryTheory.CategoryStruct.comp
        (e.functor.map (CategoryTheory.MonoidalCategoryStruct.tensorHom (e.unitIso.hom.app X) (e.unitIso.hom.app Y))) h)
-- Mathlib.Computability.RegularExpressions
RegularExpression.map_id : ∀ {α : Type u_1} (P : RegularExpression α), RegularExpression.map id P = P
-- Mathlib.Analysis.Seminorm
Seminorm.ball_smul : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E]
  (p : Seminorm 𝕜 E) {c : NNReal}, 0 < c → ∀ (r : ℝ) (x : E), (c • p).ball x r = p.ball x (r / ↑c)
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.isCommMonObj_asOver_pullback : ∀ {M S T : AlgebraicGeometry.Scheme} [inst : M.Over S] {f : T ⟶ S} [inst_1 : CategoryTheory.MonObj (M.asOver S)]
  [CategoryTheory.IsCommMonObj (M.asOver S)],
  CategoryTheory.IsCommMonObj ((CategoryTheory.Limits.pullback (M ↘ S) f).asOver T)
-- Mathlib.Analysis.Analytic.CPolynomialDef
/-- Given a function `f : E → F`, a formal multilinear series `p` and `n : ℕ`, we say that
`f` has `p` as a finite power series around `x` if `f (x + y) = ∑' pₙ yⁿ` for all `y` in a
neighborhood of `0` and `pₙ = 0` for `n ≤ m`.  -/
HasFiniteFPowerSeriesAt : {𝕜 : 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] → (E → F) → FormalMultilinearSeries 𝕜 E F → E → ℕ → Prop
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
/-- An abstract simplicial complex is a collection of nonempty finite sets of points ("faces")
which is downwards closed, i.e., any nonempty subset of a face is also a face.
 -/
PreAbstractSimplicialComplex : Type u_1 → Type u_1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pushout.congrHom_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f₁ f₂ : X ⟶ Y} {g₁ g₂ : X ⟶ Z} (h₁ : f₁ = f₂)
  (h₂ : g₁ = g₂) [inst_1 : CategoryTheory.Limits.HasPushout f₁ g₁] [inst_2 : CategoryTheory.Limits.HasPushout f₂ g₂],
  (CategoryTheory.Limits.pushout.congrHom h₁ h₂).inv =
    CategoryTheory.Limits.pushout.map f₂ g₂ f₁ g₁ (CategoryTheory.CategoryStruct.id Y)
      (CategoryTheory.CategoryStruct.id Z) (CategoryTheory.CategoryStruct.id X) ⋯ ⋯
-- Mathlib.Topology.Homotopy.LocallyContractible
/-- Each neighborhood filter has a basis of contractible subspace neighborhoods.  -/
StronglyLocallyContractibleSpace.contractible_basis : ∀ {X : Type u_4} {inst : TopologicalSpace X} [self : StronglyLocallyContractibleSpace X] (x : X),
  (nhds x).HasBasis (fun s => s ∈ nhds x ∧ ContractibleSpace ↑s) id
-- Mathlib.Analysis.InnerProductSpace.Orientation
/-- The output of the volume form of an oriented real inner product space `E` when evaluated on an
orthonormal basis is ±1.  -/
Orientation.abs_volumeForm_apply_of_orthonormal : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
  [_i : Fact (Module.finrank ℝ E = n)] (o : Orientation ℝ E (Fin n)) (v : OrthonormalBasis (Fin n) ℝ E),
  |o.volumeForm ⇑v| = 1
-- Mathlib.Data.Real.ENatENNReal
ENat.toENNReal_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], ↑(OfNat.ofNat n) = OfNat.ofNat n
-- Batteries.Recycling.RBTree.Basic
/-- `O(n)`. Constructs the array of keys of the map.  -/
RBTree.RBMap.keysArray : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → RBTree.RBMap α β cmp → Array α
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_eq_diagonal : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : AddMonoid α] [inst_2 : StarAddMonoid α]
  {M : Matrix n n α} {v : n → α}, M.conjTranspose = Matrix.diagonal v ↔ M = Matrix.diagonal (star v)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- Embedding of a subalgebra into the algebra.  -/
Subalgebra.val : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → (S : Subalgebra R A) → ↥S →ₐ[R] A
-- Std.Data.Internal.List.Associative
Std.Internal.List.DistinctKeys.perm : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)},
  l'.Perm l → Std.Internal.List.DistinctKeys l → Std.Internal.List.DistinctKeys l'
-- Mathlib.Order.OrdContinuous
RightOrdContinuous.comp : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
  {f : α → β}, RightOrdContinuous g → RightOrdContinuous f → RightOrdContinuous (g ∘ f)
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
/-- `cyclotomic n ℚ` is irreducible.  -/
Polynomial.cyclotomic.irreducible_rat : ∀ {n : ℕ}, 0 < n → Irreducible (Polynomial.cyclotomic n ℚ)
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Subcomplex.liftPath_vertex_coe : ∀ {X : SSet} (A : X.Subcomplex) {n : ℕ} (p : X.Path n)
  (hp₀ : ∀ (j : Fin (n + 1)), p.vertex j ∈ A.obj (Opposite.op { len := 0 }))
  (hp₁ : ∀ (j : Fin n), p.arrow j ∈ A.obj (Opposite.op { len := 1 })) (j : Fin (n + 1)),
  ↑((A.liftPath p hp₀ hp₁).vertex j) = p.vertex j
-- Mathlib.Analysis.LocallyConvex.Separation
RCLike.iInter_halfSpaces_eq' : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E] {s : Set E}
  [inst_3 : RCLike 𝕜] [inst_4 : Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  [LocallyConvexSpace ℝ E],
  Convex ℝ s → IsClosed s → ⋂ l, ⋂ c, ⋂ (_ : ∀ y ∈ s, RCLike.re (l y) ≤ c), {x | RCLike.re (l x) ≤ c} = s
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₂₁_apply_mem_cycles₁ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (x : G × G →₀ ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.d₂₁ A)) x ∈ groupHomology.cycles₁ A
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.map : ∀ {M : Type u_2} {N : Type u_3} [inst : Monoid M] [inst_1 : Monoid N] {F : Type u_4} [inst_2 : FunLike F M N]
  [MonoidHomClass F M N] (f : F) {x y : M}, Associated x y → Associated (f x) (f y)
-- Mathlib.Data.PNat.Prime
PNat.gcd_dvd_right : ∀ (n m : ℕ+), n.gcd m ∣ m
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.instIsPreorderQ : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] [inst_1 : LE α] [inst_2 : Std.IsPreorder α]
  [inst_3 : Lean.Grind.OrderedAdd α], Std.IsPreorder (Lean.Grind.Ring.OfSemiring.Q α)
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.ReflexiveCofork.condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C}
  (G : CategoryTheory.Limits.ReflexiveCofork F),
  CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left) G.π =
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right) G.π
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inter_div_union_subset_union : ∀ {α : Type u_2} [inst : Div α] {s₁ s₂ t₁ t₂ : Set α}, s₁ ∩ s₂ / (t₁ ∪ t₂) ⊆ s₁ / t₁ ∪ s₂ / t₂
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
AlgebraicGeometry.Scheme.instEtaleOverLeftDiscretePUnitInferInstanceOverClass : ∀ (X : AlgebraicGeometry.Scheme) (Y : X.Etale), AlgebraicGeometry.Etale (Y.left ↘ X)
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.ne_and_ne_of_swap_mul_apply_ne_self : ∀ {α : Type u_1} [inst : DecidableEq α] {f : Equiv.Perm α} {x y : α}, (Equiv.swap x (f x) * f) y ≠ y → f y ≠ y ∧ y ≠ x
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- A functor between preadditive categories that preserves (zero morphisms and) finite biproducts
preserves finite coproducts.  -/
CategoryTheory.Limits.preservesCoproduct_of_preservesBiproduct : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] {J : Type u_1} [Finite J] {f : J → C}
  [CategoryTheory.Limits.PreservesBiproduct f F],
  CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) F
-- Mathlib.Topology.EMetricSpace.Defs
Metric.eball_disjoint : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {ε₁ ε₂ : ENNReal},
  ε₁ + ε₂ ≤ edist x y → Disjoint (Metric.eball x ε₁) (Metric.eball y ε₂)
-- Init.Data.List.Attach
List.flatMap_unattach : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} {xs : List (Subtype P)} {f : α → List β},
  List.flatMap f xs.unattach =
    List.flatMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (f (wfParam x))))
      xs
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extend.mapX_some : ∀ {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : HomologicalComplex C c} (φ : K ⟶ L) {i : Option ι} {a : ι} (hi : i = some a),
  HomologicalComplex.extend.mapX φ i =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.extend.XIso K hi).hom
      (CategoryTheory.CategoryStruct.comp (φ.f a) (HomologicalComplex.extend.XIso L hi).inv)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapMonCompIso_inv_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [inst_6 : F.LaxMonoidal] [inst_7 : G.LaxMonoidal]
  (X : CategoryTheory.Mon C),
  (CategoryTheory.Functor.mapMonCompIso.inv.app X).hom = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.X))
-- Mathlib.Analysis.Complex.ExponentialBounds
Real.exp_neg_one_gt_d9 : 0.36787944116 < Real.exp (-1)
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.vanishingIdeal_singleton : ∀ {R : Type u} [inst : CommSemiring R] (x : PrimeSpectrum R), PrimeSpectrum.vanishingIdeal {x} = x.asIdeal
-- Mathlib.Data.Seq.Basic
_private.Mathlib.Data.Seq.Basic.0.Stream'.Seq.drop.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.ExistsHomHomCompEqCompAux.range_g_subset : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] {S X : AlgebraicGeometry.Scheme}
  {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} {t : D ⟶ (CategoryTheory.Functor.const I).obj S} {f : X ⟶ S}
  [inst_1 : ∀ (i : I), CompactSpace ↥(D.obj i)] [inst_2 : CategoryTheory.IsCofiltered I]
  [inst_3 : ∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)]
  (A : AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f),
  Set.range ⇑A.g ⊆ ↑(AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X)
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Syntax.decodeHexLitAux : String → String.Pos.Raw → ℕ → Option ℕ
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
PresheafOfModules.HasDifferentials.exists_universal_derivation : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {φ : S ⟶ F.op.comp R} [self : PresheafOfModules.HasDifferentials φ],
  ∃ M d, Nonempty d.Universal
-- Mathlib.Analysis.Calculus.ContDiff.WithLp
contDiffOn_piLp_apply : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → NormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_3 : Fintype ι]
  (p : ENNReal) [inst_4 : Fact (1 ≤ p)] {n : WithTop ℕ∞} {i : ι} {t : Set (PiLp p E)},
  ContDiffOn 𝕜 n (fun f => f.ofLp i) t
-- Lean.Util.MonadCache
Lean.MonadStateCacheT.instMonadRef : {α β : Type} →
  {m : Type → Type} →
    [inst : BEq α] → [inst_1 : Hashable α] → [Monad m] → [Lean.MonadRef m] → Lean.MonadRef (Lean.MonadStateCacheT α β m)
-- Mathlib.Order.Bounds.Lattice
gc_lowerBounds_upperBounds : ∀ {α : Type u_1} [inst : Preorder α],
  GaloisConnection (⇑OrderDual.toDual ∘ lowerBounds) (upperBounds ∘ ⇑OrderDual.ofDual)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.mop_id_unmop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : Cᴹᵒᵖ},
  (CategoryTheory.CategoryStruct.id X.unmop).mop = CategoryTheory.CategoryStruct.id X
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.toSubsemiring_injective : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  Function.Injective Subalgebra.toSubsemiring
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.TypeDefinitionParams.mk.injEq : ∀ (toTextDocumentPositionParams toTextDocumentPositionParams_1 : Lean.Lsp.TextDocumentPositionParams),
  ({ toTextDocumentPositionParams := toTextDocumentPositionParams } =
      { toTextDocumentPositionParams := toTextDocumentPositionParams_1 }) =
    (toTextDocumentPositionParams = toTextDocumentPositionParams_1)
-- Lean.Elab.Command
/-- Wraps the given action for use in `BaseIO.asTask` etc., discarding its final state except for
`logSnapshotTask` tasks, which are reported as part of the returned tree. The given cancellation
token, if any, should be stored in a `SnapshotTask` for the server to trigger it when the result is
no longer needed.
 -/
Lean.Elab.Command.wrapAsyncAsSnapshot : {α : Type} →
  (α → Lean.Elab.Command.CommandElabM Unit) →
    Option IO.CancelToken →
      autoParam String Lean.Elab.Command.wrapAsyncAsSnapshot._auto_1 →
        Lean.Elab.Command.CommandElabM (α → BaseIO Lean.Language.SnapshotTree)
-- Mathlib.MeasureTheory.Integral.Marginal
MeasureTheory.lmarginal_update_of_notMem : ∀ {δ : Type u_1} {X : δ → Type u_3} [inst : (i : δ) → MeasurableSpace (X i)] {μ : (i : δ) → MeasureTheory.Measure (X i)}
  [inst_1 : DecidableEq δ] {s : Finset δ} [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] {i : δ}
  {f : ((i : δ) → X i) → ENNReal},
  Measurable f →
    i ∉ s →
      ∀ (x : (i : δ) → X i) (y : X i),
        (∫⋯∫⁻_s, f ∂μ) (Function.update x i y) = (∫⋯∫⁻_s, f ∘ fun x => Function.update x i y ∂μ) x
-- Mathlib.Algebra.CubicDiscriminant
Cubic.degree_of_c_ne_zero : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.a = 0 → P.b = 0 → P.c ≠ 0 → P.toPoly.degree = 1
-- Mathlib.Algebra.Module.ZLattice.Basic
ZLattice.rank : ∀ (K : Type u_1) [inst : NormedField K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [HasSolidNorm K] [FloorRing K]
  {E : Type u_2} [inst_5 : NormedAddCommGroup E] [inst_6 : NormedSpace K E] [FiniteDimensional K E] [ProperSpace E]
  (L : Submodule ℤ E) [inst_9 : DiscreteTopology ↥L] [hs : IsZLattice K L], Module.finrank ℤ ↥L = Module.finrank K E
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.SimpM : Type → Type
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.findIdx.go.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → ℕ → Sort u_2) (n : ℕ) (h_1 : (n : ℕ) → motive [] n)
  (h_2 : (a : α) → (l : List α) → (n : ℕ) → motive (a :: l) n),
  (match [], n with
    | [], n => h_1 n
    | a :: l, n => h_2 a l n) =
    h_1 n
-- Lean.Data.Options
Lean.withInPattern : {m : Type → Type} → {α : Type} → [Lean.MonadWithOptions m] → m α → m α
-- Init.Data.Array.Lemmas
Array.getElem?_append_left : ∀ {α : Type u_1} {xs ys : Array α} {i : ℕ}, i < xs.size → (xs ++ ys)[i]? = xs[i]?
-- Mathlib.Analysis.RCLike.Basic
RCLike.nnnorm_two : ∀ {K : Type u_1} [inst : RCLike K], ‖2‖₊ = 2
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.dist_of_mem_subset_sphere : ∀ {P : Type u_2} [inst : MetricSpace P] {p : P} {ps : Set P} {s : EuclideanGeometry.Sphere P},
  p ∈ ps → ps ⊆ Metric.sphere s.center s.radius → dist p s.center = s.radius
-- Mathlib.Data.List.Sort
/-- The list `List.ofFn f` is strictly sorted with respect to `(· ≤ ·)` if and only if `f` is
strictly monotone.  -/
List.sortedLT_ofFn_iff : ∀ {α : Type u_1} [inst : Preorder α] {n : ℕ} {f : Fin n → α}, (List.ofFn f).SortedLT ↔ StrictMono f
-- Mathlib.Data.Set.Lattice
Set.Sigma.univ : ∀ {α : Type u_1} (X : α → Type u_12), Set.univ = ⋃ a, Set.range (Sigma.mk a)
-- Mathlib.RingTheory.Derivation.MapCoeffs
Differential.implicitDeriv_C : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Differential A] (v : Polynomial A) (b : A),
  (Differential.implicitDeriv v) (Polynomial.C b) = Polynomial.C b′
-- Mathlib.RepresentationTheory.Submodule
Representation.invtSubmodule.coe_top : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring k] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ : Representation k G V), ↑⊤ = ⊤
-- Mathlib.Data.List.AList
/-- The underlying `List` of an `AList`  -/
AList.entries : {α : Type u} → {β : α → Type v} → AList β → List (Sigma β)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.reduce_fold_fn.match_1.eq_1 : ∀ (motive : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Sort u_1)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg)
  (h_3 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.both)
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned),
  (match Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos with
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg => h_2 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.both => h_3 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned => h_4 ()) =
    h_1 ()
-- Mathlib.CategoryTheory.Preadditive.Mat
/-- `Mat_.lift F` is the unique additive functor `L : Mat_ C ⥤ D` such that `F ≅ embedding C ⋙ L`.
 -/
CategoryTheory.Mat_.liftUnique : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {D : Type u₁} →
        [inst_2 : CategoryTheory.Category.{v₁, u₁} D] →
          [inst_3 : CategoryTheory.Preadditive D] →
            [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts D] →
              (F : CategoryTheory.Functor C D) →
                [inst_5 : F.Additive] →
                  (L : CategoryTheory.Functor (CategoryTheory.Mat_ C) D) →
                    [L.Additive] → ((CategoryTheory.Mat_.embedding C).comp L ≅ F) → (L ≅ CategoryTheory.Mat_.lift F)
-- Init.Prelude
/-- `a % b` computes the remainder upon dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For `Nat` and `Int` it satisfies `a % b + b * (a / b) = a`,
  and `a % 0` is defined to be `a`. 

Conventions for notations in identifiers:

 * The recommended spelling of `%` in identifiers is `mod`. -/
HMod.hMod : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HMod α β γ] → α → β → γ
-- Mathlib.Data.Real.Basic
Real.lattice : Lattice ℝ
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.apply_mem_span_image_iff_mem_span : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂]
  [RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂} {x : M} {s : Set M},
  Function.Injective ⇑f → (f x ∈ Submodule.span R₂ (⇑f '' s) ↔ x ∈ Submodule.span R s)
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.map_obj_injective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f],
  Function.Injective (CategoryTheory.Subobject.map f).obj
-- Mathlib.Topology.Algebra.Monoid
/-- Let `M` be a topological space with a continuous multiplication operation and a `0`.
Let `f : α → M` and `g : α → M` be functions. If `g` tends to zero on a filter `l`
and the image of `l` under `f` is disjoint from the cocompact filter on `M`, then
`fun x : α ↦ f x * g x` also tends to zero on `l`.  -/
Tendsto.tendsto_mul_zero_of_disjoint_cocompact_left : ∀ {M : Type u_3} {α : Type u_6} [inst : TopologicalSpace M] [inst_1 : MulZeroClass M] [ContinuousMul M] {f g : α → M}
  {l : Filter α},
  Disjoint (Filter.map f l) (Filter.cocompact M) →
    Filter.Tendsto g l (nhds 0) → Filter.Tendsto (fun x => f x * g x) l (nhds 0)
-- Mathlib.Topology.UnitInterval
unitInterval.symm_symm : ∀ (x : ↑unitInterval), unitInterval.symm (unitInterval.symm x) = x
-- Mathlib.Tactic.LinearCombinationPrime
Mathlib.Tactic.LinearCombinationPrime.c_sub_pf : ∀ {α : Type u_1} {b c : α} [inst : Sub α], b = c → ∀ (a : α), a - b = a - c
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.LeftAdjointCommShift.iso.eq_1 : ∀ {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] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) {A : Type u_3} [inst_2 : AddGroup A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] (a : A) [inst_5 : G.CommShift A],
  CategoryTheory.Adjunction.LeftAdjointCommShift.iso adj a =
    CategoryTheory.Adjunction.LeftAdjointCommShift.iso' adj a (-a) ⋯
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.sdiv.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : SDiv α β], Set.sdiv = { sdiv := Set.image2 fun x1 x2 => x1 /ₛ x2 }