mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
/-- If `H : C ⥤ D` is an additive functor and `φ` is a morphism of cochain complexes
in `C`, this is the comparison isomorphism between the image by `H`
of `mappingCone φ` and the mapping cone of the image by `H` of `φ`.  -/
CochainComplex.mappingCone.mapHomologicalComplexIso : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v', u_2} D] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.Preadditive D] →
            {F G : CochainComplex C ℤ} →
              (φ : F ⟶ G) →
                [inst_4 : HomologicalComplex.HasHomotopyCofiber φ] →
                  (H : CategoryTheory.Functor C D) →
                    [inst_5 : H.Additive] →
                      [inst_6 :
                          HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)] →
                        (H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (CochainComplex.mappingCone φ) ≅
                          CochainComplex.mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
-- Mathlib.Algebra.Group.Defs
MulOneClass.ext_iff : ∀ {M : Type u} {m₁ m₂ : MulOneClass M}, m₁ = m₂ ↔ Mul.mul = Mul.mul
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.getInductiveVal? : Lean.Expr → Lean.MetaM (Option Lean.InductiveVal)
-- Lean.Util.FoldConsts
Lean.Expr.FoldConstsImpl.fold : {α : Type} → (Lean.Name → α → α) → Lean.Expr → α → Lean.Expr.FoldConstsImpl.FoldM α
-- Mathlib.Data.List.TakeWhile
List.takeWhile_idem : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.takeWhile p (List.takeWhile p l) = List.takeWhile p l
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivAtFilter_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (L : Filter (𝕜 × 𝕜)) (c : F), HasDerivAtFilter (fun x => c) 0 L
-- Mathlib.Order.KrullDimension
Order.coheight_le_iff : ∀ {α : Type u_1} [inst : Preorder α] {a : α} {n : ℕ∞},
  Order.coheight a ≤ n ↔ ∀ ⦃p : LTSeries α⦄, a ≤ RelSeries.head p → ↑p.length ≤ n
-- Mathlib.Analysis.InnerProductSpace.Projection.Submodule
/-- The orthogonal complement satisfies `Kᗮᗮᗮ = Kᗮ`.  -/
Submodule.triorthogonal_eq_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E}, Kᗮᗮᗮ = Kᗮ
-- Mathlib.CategoryTheory.Sites.CoverLifting
CategoryTheory.RanIsSheafOfIsCocontinuous.fac_assoc : ∀ {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] {G : CategoryTheory.Functor C D} {A : Type w}
  [inst_2 : CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C}
  {K : CategoryTheory.GrothendieckTopology D} [inst_3 : G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A}
  (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} {α : G.op.comp R ⟶ F}
  (hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension) {X : D} {S : K.Cover X}
  (s : CategoryTheory.Limits.Multifork (S.index R)) (i : S.Arrow) {Z : A} (h : R.obj (Opposite.op i.Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.lift hF hR s)
      (CategoryTheory.CategoryStruct.comp (R.map i.f.op) h) =
    CategoryTheory.CategoryStruct.comp (s.ι i) h
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.contSupp_cons₁ : ∀ (fs : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.contSupp (Turing.PartrecToTM2.Cont'.cons₁ fs k) =
    Turing.PartrecToTM2.trStmts₁
        (Turing.PartrecToTM2.move₂ (fun x => false) Turing.PartrecToTM2.K'.main Turing.PartrecToTM2.K'.aux
          (Turing.PartrecToTM2.move₂ (fun s => decide (s = Turing.PartrecToTM2.Γ'.consₗ)) Turing.PartrecToTM2.K'.stack
            Turing.PartrecToTM2.K'.main
            (Turing.PartrecToTM2.move₂ (fun x => false) Turing.PartrecToTM2.K'.aux Turing.PartrecToTM2.K'.stack
              (Turing.PartrecToTM2.trNormal fs k.cons₂)))) ∪
      Turing.PartrecToTM2.codeSupp fs k.cons₂
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.rightHomologyData_p : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [inst_2 : CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting),
  s.rightHomologyData.p = S.g
-- Mathlib.FieldTheory.Relrank
/-- `Subfield.relrank A B` is defined to be `[B : A ⊓ B]` as a `Cardinal`, in particular,
when `A ≤ B` it is `[B : A]`, the degree of the field extension `B / A`.
This is similar to `Subgroup.relIndex` but it is `Cardinal` valued.  -/
Subfield.relrank : {E : Type v} → [inst : Field E] → Subfield E → Subfield E → Cardinal.{v}
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
Order.cof_le : ∀ {α : Type u} [inst : Preorder α] {s : Set α}, IsCofinal s → Order.cof α ≤ Cardinal.mk ↑s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Real.sin_div_le_inv_abs : ∀ (x : ℝ), Real.sin x / x ≤ |x|⁻¹
-- Batteries.Lean.Meta.Basic
/-- Get the `MetavarDecl` of `mvarId`. If `mvarId` is not a declared metavariable
in the given `MetavarContext`, throw an error.
 -/
Lean.MetavarContext.getExprMVarDecl : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → Lean.MetavarContext → Lean.MVarId → m Lean.MetavarDecl
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_add : ∀ {x : NNReal}, x ≠ 0 → ∀ (y z : ℝ), x ^ (y + z) = x ^ y * x ^ z
-- Mathlib.Algebra.Ring.Defs
NonUnitalNonAssocRing.mk : {α : Type u} →
  [toAddCommGroup : AddCommGroup α] →
    [toMul : Mul α] →
      (∀ (a b c : α), a * (b + c) = a * b + a * c) →
        (∀ (a b c : α), (a + b) * c = a * c + b * c) →
          (∀ (a : α), 0 * a = 0) → (∀ (a : α), a * 0 = 0) → NonUnitalNonAssocRing α
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.exact : ∀ {V : Type u} {G : SimpleGraph V} {v w : V}, G.connectedComponentMk v = G.connectedComponentMk w → G.Reachable v w
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_inter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, (m₁ ∩ m₂).get? k = if k ∈ m₂ then m₁.get? k else none
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.mk.sizeOf_spec : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {c₁ c₂ c₃ : R}
  [inst_3 : SizeOf R] [inst_4 : SizeOf A] (i j k : A) (i_mul_i : i * i = c₁ • 1 + c₂ • i) (j_mul_j : j * j = c₃ • 1)
  (i_mul_j : i * j = k) (j_mul_i : j * i = c₂ • j - k),
  sizeOf { i := i, j := j, k := k, i_mul_i := i_mul_i, j_mul_j := j_mul_j, i_mul_j := i_mul_j, j_mul_i := j_mul_i } =
    1 + sizeOf i + sizeOf j + sizeOf k + sizeOf i_mul_i + sizeOf j_mul_j + sizeOf i_mul_j + sizeOf j_mul_i
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.Result.mk.inj : ∀ {proof proof_1 : Lean.Expr}, { proof := proof } = { proof := proof_1 } → proof = proof_1
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.toPoly'.go : ℤ → Int.Internal.Linear.Expr → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly
-- Init.Data.Array.Sort.Lemmas
_private.Init.Data.Array.Sort.Lemmas.0.List.mergeSort.eq_def : ∀ {α : Type u_1} (x : List α) (x_1 : α → α → Bool),
  x.mergeSort x_1 =
    match x, x_1 with
    | [], x => []
    | [a], x => [a]
    | a :: b :: xs, le =>
      have lr := List.MergeSort.Internal.splitInTwo ⟨a :: b :: xs, ⋯⟩;
      have this := ⋯;
      have this := ⋯;
      ((↑lr.1).mergeSort le).merge ((↑lr.2).mergeSort le) le
-- Lean.Meta.CongrTheorems
Lean.Meta.CongrTheorem.mk : Lean.Expr → Lean.Expr → Array Lean.Meta.CongrArgKind → Lean.Meta.CongrTheorem
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
EuclideanGeometry.oangle.congr_simp : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  (p₁ p₁_1 : P),
  p₁ = p₁_1 →
    ∀ (p₂ p₂_1 : P),
      p₂ = p₂_1 →
        ∀ (p₃ p₃_1 : P), p₃ = p₃_1 → EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₁_1 p₂_1 p₃_1
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.instBEqPolyCnstr.beq : Nat.Internal.Linear.PolyCnstr → Nat.Internal.Linear.PolyCnstr → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.ι_sndSigmaMap_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) [inst_1 : CategoryTheory.Limits.HasCoproduct I.left]
  [inst_2 : CategoryTheory.Limits.HasCoproduct I.right] (b : J.L) {Z : C} (h : ∐ I.right ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.left b)
      (CategoryTheory.CategoryStruct.comp I.sndSigmaMap h) =
    CategoryTheory.CategoryStruct.comp (I.snd b)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.right (J.snd b)) h)
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.IsTriangulated.instPreservesLimitsOfShapeDiscreteWalkingPair : ∀ {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] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  [inst_5 : CategoryTheory.Limits.HasZeroObject C] [inst_6 : CategoryTheory.Limits.HasZeroObject D]
  [inst_7 : CategoryTheory.Preadditive C] [inst_8 : CategoryTheory.Preadditive D]
  [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_10 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_11 : CategoryTheory.Pretriangulated C]
  [inst_12 : CategoryTheory.Pretriangulated D] [F.IsTriangulated],
  CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- When `IsEmpty ι`, this lemma does not hold without the additional assumption `p ≠ ∞` because
the left-hand side simplifies to `0`, while the right-hand side simplifies to `‖b‖₊`. See
`PiLp.norm_equiv_symm_const` for a version which exchanges the hypothesis `Nonempty ι`.
for `p ≠ ∞`.  -/
PiLp.norm_toLp_const' : ∀ {p : ENNReal} {ι : Type u_2} [hp : Fact (1 ≤ p)] [inst : Fintype ι] {β : Type u_5} [inst_1 : SeminormedAddCommGroup β]
  [Nonempty ι] (b : β), ‖WithLp.toLp p (Function.const ι b)‖ = ↑↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖
-- Mathlib.Analysis.Complex.Hadamard
/-- If z is on the closed strip `re ⁻¹' [l, u]`, then `(z - l) / (u - l)` is on the closed strip
`re ⁻¹' [0, 1]`.  -/
Complex.HadamardThreeLines.mem_verticalClosedStrip_of_scale_id_mem_verticalClosedStrip : ∀ {z : ℂ} {l u : ℝ},
  l < u →
    z ∈ Complex.HadamardThreeLines.verticalClosedStrip l u →
      z / (↑u - ↑l) - ↑l / (↑u - ↑l) ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 1
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.l_u_le_trans : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {u : α → β} {l : β → α},
  GaloisConnection l u → ∀ {x y z : α}, l (u y) ≤ x → l (u z) ≤ y → l (u z) ≤ x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
/-- If `φ` is mono, it is a normal additive group homomorphism if and only if for all
`X` the image of `H(X)` in `G(X)` is a normal additive subgroup.  -/
CategoryTheory.IsAddMonHom.normal_iff_normal_addMonoidHom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H : C} [inst_2 : CategoryTheory.AddGrpObj G] [inst_3 : CategoryTheory.AddGrpObj H] {φ : H ⟶ G}
  [inst_4 : CategoryTheory.IsAddMonHom φ] [CategoryTheory.Mono φ],
  CategoryTheory.IsAddMonHom.Normal φ ↔ ∀ (X : C), (CategoryTheory.IsAddMonHom.addMonoidHom φ X).range.Normal
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.shiftFunctor_obj_d : ∀ {S : Type u_1} [inst : AddCommGroupWithOne S] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] (n : S)
  (X : CategoryTheory.DifferentialObject S C),
  ((CategoryTheory.DifferentialObject.shiftFunctor C n).obj X).d =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map X.d)
      (CategoryTheory.shiftComm X.obj 1 n).hom
-- Mathlib.Analysis.Normed.Group.Quotient
/-- The norm of the image of `m : M` in the quotient by `S` is zero if and only if `m` belongs
to the closure of `S`.  -/
QuotientGroup.norm_mk_eq_zero_iff_mem_closure : ∀ {M : Type u_1} [inst : SeminormedCommGroup M] {S : Subgroup M} {m : M}, ‖↑m‖ = 0 ↔ m ∈ closure ↑S
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.SimpleFunc.setToSimpleFunc_zero_apply : ∀ {α : Type u_1} {F : Type u_3} {F' : Type u_4} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F]
  [inst_2 : NormedAddCommGroup F'] [inst_3 : NormedSpace ℝ F'] {m : MeasurableSpace α} (T : Set α → F →L[ℝ] F'),
  MeasureTheory.SimpleFunc.setToSimpleFunc T 0 = 0
-- Mathlib.Algebra.Ring.Subring.MulOpposite
/-- Pull an opposite subring back to a subring along `MulOpposite.op`  -/
Subring.unop : {R : Type u_2} → [inst : NonAssocRing R] → Subring Rᵐᵒᵖ → Subring R
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsLimitKernelFork_φH : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (c₁ : CategoryTheory.Limits.KernelFork S₁.g)
  (hc₁ : CategoryTheory.Limits.IsLimit c₁) (hf₂ : S₂.f = 0) (c₂ : CategoryTheory.Limits.KernelFork S₂.g)
  (hc₂ : CategoryTheory.Limits.IsLimit c₂) (f : c₁.pt ⟶ c₂.pt)
  (comm :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c₁) φ.τ₂ =
      CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Fork.ι c₂)),
  (CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsLimitKernelFork φ hf₁ c₁ hc₁ hf₂ c₂ hc₂ f comm).φH = f
-- Lean.Attributes
Lean.ParametricAttribute.getParam? : {α : Type} → [Inhabited α] → Lean.ParametricAttribute α → Lean.Environment → Lean.Name → Option α
-- Mathlib.Algebra.Group.Finsupp
Finsupp.instIsLeftCancelAdd : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] [IsLeftCancelAdd M], IsLeftCancelAdd (ι →₀ M)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- Functor composition induces a functor on truncated simplicial objects.  -/
CategoryTheory.SimplicialObject.Truncated.whiskering : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    {n : ℕ} →
      (D : Type u_1) →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
          CategoryTheory.Functor (CategoryTheory.Functor C D)
            (CategoryTheory.Functor (CategoryTheory.SimplicialObject.Truncated C n)
              (CategoryTheory.SimplicialObject.Truncated D n))
-- Lean.Meta.InferType
_private.Lean.Meta.InferType.0.Lean.Meta.inferAppType : Lean.Expr → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
_private.Mathlib.Algebra.Order.Monoid.Unbundled.WithTop.0.WithTop.addMonoid.match_1.eq_1 : ∀ {α : Type u_1} (motive : WithTop α → ℕ → Sort u_2) (a : α) (n : ℕ) (h_1 : (a : α) → (n : ℕ) → motive (some a) n)
  (h_2 : Unit → motive none 0) (h_3 : (_n : ℕ) → motive none _n.succ),
  (match some a, n with
    | some a, n => h_1 a n
    | none, 0 => h_2 ()
    | none, _n.succ => h_3 _n) =
    h_1 a n
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_of_contains_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → β → γ} {k : α}, t.WF → (Std.TreeMap.Raw.map f t).contains k = true → t.contains k = true
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.map_constants_inclusion_isExpansionOn : ∀ (L : FirstOrder.Language) {M : Type w} [inst : L.Structure M] {A B : Set M} (h : A ⊆ B),
  (L.lhomWithConstantsMap (Set.inclusion h)).IsExpansionOn M
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
ContinuousLinearMap.locallyIntegrableOn_comp : ∀ {X : Type u_1} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] {μ : MeasureTheory.Measure X} {s : Set X}
  {E : Type u_9} {H : Type u_10} {𝕜 : Type u_11} {𝕜' : Type u_12} [inst_2 : NontriviallyNormedField 𝕜]
  [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜' E]
  [inst_6 : NormedAddCommGroup H] [inst_7 : NormedSpace 𝕜 H] {σ : 𝕜 →+* 𝕜'} [RingHomIsometric σ] {f : X → H}
  (L : H →SL[σ] E), MeasureTheory.LocallyIntegrableOn f s μ → MeasureTheory.LocallyIntegrableOn (⇑L ∘ f) s μ
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
Submodule.closure_le : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M] [inst_4 : ContinuousAdd M] [inst_5 : ContinuousConstSMul R M] {s : Submodule R M}
  {t : ClosedSubmodule R M}, s.closure ≤ t ↔ s ≤ ↑t
-- Mathlib.Topology.Order
nhds_inf : ∀ {α : Type u} {t₁ t₂ : TopologicalSpace α} {a : α}, nhds a = nhds a ⊓ nhds a
-- Mathlib.Algebra.Order.GroupWithZero.Basic
eq_and_eq_of_pos_of_le_of_mul_le_mul : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b c d : α} [inst_1 : PartialOrder α] [PosMulReflectLE α] [MulPosReflectLE α]
  [PosMulMono α] [MulPosMono α], 0 < a → 0 < c → a ≤ b → c ≤ d → b * d ≤ a * c → a = b ∧ c = d
-- Mathlib.AlgebraicGeometry.Morphisms.Constructors
AlgebraicGeometry.stalkwise.eq_1 : ∀ (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop)
  (x x_1 : AlgebraicGeometry.Scheme) (f : x ⟶ x_1),
  AlgebraicGeometry.stalkwise P f = ∀ (x_2 : ↥x), P (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x_2))
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.map_cocompact : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  Filter.map (⇑h) (Filter.cocompact X) = Filter.cocompact Y
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_add_one' : ∀ {x y : ℝ}, 0 ≤ x → y + 1 ≠ 0 → x ^ (y + 1) = x ^ y * x
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
/-- Extension of a natural transformation `φ` between functors
`C ⥤ Karoubi D` to a natural transformation between the
extension of these functors to `Karoubi C ⥤ Karoubi D`  -/
CategoryTheory.Idempotents.FunctorExtension₁.map : {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 G : CategoryTheory.Functor C (CategoryTheory.Idempotents.Karoubi D)} →
          (F ⟶ G) →
            (CategoryTheory.Idempotents.FunctorExtension₁.obj F ⟶ CategoryTheory.Idempotents.FunctorExtension₁.obj G)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.covolume.eq_1 : ∀ (G : Type u_6) (α : Type u_7) [inst : One G] [inst_1 : SMul G α] [inst_2 : MeasurableSpace α]
  (ν : MeasureTheory.Measure α),
  MeasureTheory.covolume G α ν = if funDom : MeasureTheory.HasFundamentalDomain G α ν then ν ⋯.choose else 0
-- Mathlib.RingTheory.RingHom.Smooth
RingHom.FormallySmooth.isStableUnderBaseChange : RingHom.IsStableUnderBaseChange @RingHom.FormallySmooth
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
/-- Loop through all constants that appear in the module `mdata`,
and add the entries generated by `act` to the `PreDiscrTree`.
 -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.loadImportedModule : {α : Type} →
  Lean.Core.Context →
    Lean.Environment →
      Lean.Meta.RefinedDiscrTree.ImportErrorData✝ →
        IO.Ref Lean.Meta.State →
          IO.Ref Lean.Core.State →
            (Lean.Name →
                Lean.ConstantInfo →
                  Lean.MetaM
                    (List (α × List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry)))) →
              Lean.Name →
                Lean.ModuleData →
                  Lean.Meta.RefinedDiscrTree.PreDiscrTree α →
                    optParam ℕ 0 → BaseIO (Lean.Meta.RefinedDiscrTree.PreDiscrTree α)
-- Lean.Elab.Do.InferControlInfo
Lean.Elab.Do.mkControlInfoElemAttribute : Lean.Name → IO (Lean.KeyedDeclsAttribute Lean.Elab.Do.ControlInfoHandler)
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Functor.map.instIsComon_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]
  (F : CategoryTheory.Functor C D) [inst_4 : F.OplaxMonoidal] {X Y : C} [inst_5 : CategoryTheory.ComonObj X]
  [inst_6 : CategoryTheory.ComonObj Y] (f : X ⟶ Y) [CategoryTheory.IsComonHom f], CategoryTheory.IsComonHom (F.map f)
-- Mathlib.Topology.Algebra.Group.Basic
isClosedMap_neg : ∀ (G : Type w) [inst : TopologicalSpace G] [inst_1 : InvolutiveNeg G] [ContinuousNeg G], IsClosedMap Neg.neg
-- Mathlib.CategoryTheory.Category.Preorder
/-- Extract the underlying inequality from a morphism in a preorder category.  -/
Quiver.Hom.le : ∀ {X : Type u_1} [inst : Preorder X] {x y : X} (h : x ⟶ y), x ≤ y
-- Mathlib.Data.Nat.Sqrt
Nat.sqrt_le' : ∀ (n : ℕ), n.sqrt ^ 2 ≤ n
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- SubMulAction on the complement of an invariant subset  -/
SubMulAction.instCompl : {R : Type u} → {M : Type v} → [inst : Group R] → [inst_1 : MulAction R M] → Compl (SubMulAction R M)
-- Aesop.Rule.Basic
Aesop.Rule.tac : {α : Type} → Aesop.Rule α → Aesop.RuleTacDescr
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.pullbackIsoProdSubtype_hom_fst : ∀ {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (TopCat.pullbackIsoProdSubtype f g).hom (TopCat.pullbackFst f g) =
    CategoryTheory.Limits.pullback.fst f g
-- Lean.Elab.Binders
Lean.Elab.Term.LetConfig.mk.inj : ∀ {nondep usedOnly zeta postponeValue generalize : Bool} {eq? : Option Lean.Ident}
  {nondep_1 usedOnly_1 zeta_1 postponeValue_1 generalize_1 : Bool} {eq?_1 : Option Lean.Ident},
  { nondep := nondep, usedOnly := usedOnly, zeta := zeta, postponeValue := postponeValue, generalize := generalize,
        eq? := eq? } =
      { nondep := nondep_1, usedOnly := usedOnly_1, zeta := zeta_1, postponeValue := postponeValue_1,
        generalize := generalize_1, eq? := eq?_1 } →
    nondep = nondep_1 ∧
      usedOnly = usedOnly_1 ∧ zeta = zeta_1 ∧ postponeValue = postponeValue_1 ∧ generalize = generalize_1 ∧ eq? = eq?_1
-- Mathlib.Topology.Order.OrderClosed
CovBy.nhdsLE : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {a b : α},
  a ⋖ b → nhdsWithin b (Set.Iic b) = pure b
-- Mathlib.RingTheory.NonUnitalSubring.Defs
/-- Construct a `NonUnitalSubring R` from a set `s`, a subsemigroup `sm`, and an additive
subgroup `sa` such that `x ∈ s ↔ x ∈ sm ↔ x ∈ sa`.  -/
NonUnitalSubring.mk' : {R : Type u} →
  [inst : NonUnitalNonAssocRing R] →
    (s : Set R) → (sm : Subsemigroup R) → (sa : AddSubgroup R) → ↑sm = s → ↑sa = s → NonUnitalSubring R
-- Init.Data.SInt.IntToBitVec
Int16.toBitVec64_toISize : ∀ (n : Int16) (h : System.Platform.numBits = 64), n.toISize.toBitVec64 h = BitVec.signExtend 64 n.toBitVec
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.IsAffineHom.of_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
  [AlgebraicGeometry.IsAffineHom (CategoryTheory.CategoryStruct.comp f g)] [AlgebraicGeometry.IsSeparated g],
  AlgebraicGeometry.IsAffineHom f
-- Lean.Data.JsonRpc
Lean.JsonRpc.instInhabitedErrorCode : Inhabited Lean.JsonRpc.ErrorCode
-- Init.Data.Array.Erase
Array.size_eraseP_le : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α}, (xs.eraseP p).size ≤ xs.size
-- Mathlib.Algebra.Category.Ring.Limits
SemiRingCat.forget₂Mon_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ SemiRingCat MonCat)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
/-- Simpler version of `mkBinOpThms` for operators that have only one congruence theorem.  -/
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt.0.Lean.Meta.Grind.Arith.Cutsat.mkPowThm? : Lean.Meta.Grind.Arith.Cutsat.ToIntM (Option Lean.Expr)