mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.contains_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k k' : α}
  {f : Option β → Option β},
  (Std.DTreeMap.Const.alter t k f).contains k' =
    if cmp k k' = Ordering.eq then (f (Std.DTreeMap.Const.get? t k)).isSome else t.contains k'
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
HomotopyCategory.shift_quotient_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex C (ComplexShape.up ℤ)) (n : ℤ),
  (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).obj
      ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K) =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
      ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj K)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.δ_comp_whiskerLeft_δ_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]
  (F : CategoryTheory.Functor C D) [inst_4 : F.OplaxMonoidal] (X Y Z : C) {Z_1 : D}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X)
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj Y) (F.obj Z)) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxMonoidal.δ F X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.OplaxMonoidal.δ F Y Z))
        h) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OplaxMonoidal.δ F (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.OplaxMonoidal.δ F X Y) (F.obj Z))
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom h)))
-- Mathlib.CategoryTheory.Generator.Preadditive
CategoryTheory.isCoseparator_iff_faithful_preadditiveYoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (G : C),
  CategoryTheory.IsCoseparator G ↔ (CategoryTheory.preadditiveYoneda.obj G).Faithful
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.self_mem_cylinder : ∀ {E : ℕ → Type u_1} (x : (n : ℕ) → E n) (n : ℕ), x ∈ PiNat.cylinder x n
-- Mathlib.Data.Rel.Cover
SetRel.IsCover.anti : ∀ {X : Type u_1} {U : SetRel X X} {s t N : Set X}, s ⊆ t → U.IsCover t N → U.IsCover s N
-- Mathlib.Order.Filter.Basic
Filter.Eventually.mp : ∀ {α : Type u} {p q : α → Prop} {f : Filter α},
  (∀ᶠ (x : α) in f, p x) → (∀ᶠ (x : α) in f, p x → q x) → ∀ᶠ (x : α) in f, q x
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.coe_lt_coe : ∀ {E : Type u_3} [inst : AddGroup E] {p q : NonarchAddGroupSeminorm E}, ⇑p < ⇑q ↔ p < q
-- Std.Http.Protocol.H1.Error
/-- Unsupported HTTP version.
 -/
Std.Http.Protocol.H1.Error.unsupportedVersion : Std.Http.Protocol.H1.Error
-- Mathlib.Algebra.Module.Submodule.Map
/-- The pushforward of a submodule `p ⊆ M` by `f : M → M₂`  -/
Submodule.map : {R : Type u_1} →
  {R₂ : Type u_3} →
    {M : Type u_5} →
      {M₂ : Type u_7} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R₂ M₂] →
                    {σ₁₂ : R →+* R₂} → [RingHomSurjective σ₁₂] → (M →ₛₗ[σ₁₂] M₂) → Submodule R M → Submodule R₂ M₂
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- The inner product of two vectors, divided by the product of their
norms, has value -1 if and only if they are nonzero and one is
a negative multiple of the other.  -/
real_inner_div_norm_mul_norm_eq_neg_one_iff : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F),
  inner ℝ x y / (‖x‖ * ‖y‖) = -1 ↔ x ≠ 0 ∧ ∃ r < 0, y = r • x
-- Mathlib.Analysis.Convex.Piecewise
/-- The piecewise function `(Set.Iic e).piecewise f g` of a function `f` increasing and concave on
`Set.Iic e` and a function `g` decreasing and concave on `Set.Ici e`, such that `f e = g e`, is
concave on the universal set.  -/
concaveOn_univ_piecewise_Iic_of_monotoneOn_Iic_antitoneOn_Ici : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : Module 𝕜 E] [PosSMulMono 𝕜 E] [inst_7 : AddCommGroup β]
  [inst_8 : PartialOrder β] [IsOrderedAddMonoid β] [inst_10 : Module 𝕜 β] [PosSMulMono 𝕜 β] {e : E} {f g : E → β},
  ConcaveOn 𝕜 (Set.Iic e) f →
    ConcaveOn 𝕜 (Set.Ici e) g →
      MonotoneOn f (Set.Iic e) → AntitoneOn g (Set.Ici e) → f e = g e → ConcaveOn 𝕜 Set.univ ((Set.Iic e).piecewise f g)
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.dest_mk : ∀ {F : PFunctor.{uA, uB}} (x : ↑F F.M), (PFunctor.M.mk x).dest = x
-- Lean.SubExpr
Lean.SubExpr.Pos.pushNthBindingDomain : ℕ → Lean.SubExpr.Pos → Lean.SubExpr.Pos
-- Lean.Meta.Tactic.Grind.Split
/-- Given a `mvarId` associated with a subgoal created by `splitCore`, inspects the
proof term assigned to `mvarId` and tries to extract the proof of `False` that does not
depend on hypotheses introduced in the subgoal.
For example: suppose the subgoal is of the form `p → q → False` where `p` and `q` are new
hypotheses introduced during case analysis. If the proof is of the form `fun _ _ => h`, returns
`some h`.
 -/
_private.Lean.Meta.Tactic.Grind.Split.0.Lean.Meta.Grind.Action.getFalseProof? : Lean.MVarId → Lean.MetaM (Option Lean.Expr)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey_eq_iff_mem_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {he : t ≠ ∅} {km : α}, t.maxKey he = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
AlgebraNorm.algebraNormClass : ∀ {R : Type u_1} [inst : SeminormedCommRing R] {S : Type u_2} [inst_1 : Ring S] [inst_2 : Algebra R S],
  AlgebraNormClass (AlgebraNorm R S) R S
-- Mathlib.Topology.Basic
/-- **Alias** of the reverse direction of `TopologicalSpace.ext_iff_isClosed`. -/
TopologicalSpace.ext_isClosed : ∀ {X : Type u_2} {t₁ t₂ : TopologicalSpace X}, (∀ (s : Set X), IsClosed s ↔ IsClosed s) → t₁ = t₂
-- Mathlib.Algebra.Lie.Semisimple.Defs
LieAlgebra.hasTrivialRadical_iff : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  LieAlgebra.HasTrivialRadical R L ↔ LieAlgebra.radical R L = ⊥
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
IsSelfAdjoint.cfc_arg : ∀ {A : Type u_1} [inst : CStarAlgebra A] (u : A), IsSelfAdjoint (cfc (Complex.ofReal ∘ Complex.arg) u)
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
nonneg_of_mul_nonneg_right : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a b : R} [PosMulStrictMono R], 0 ≤ a * b → 0 < a → 0 ≤ b
-- Init.Data.SInt.Lemmas
instAssociativeInt8HAdd : Std.Associative fun x1 x2 => x1 + x2
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- Given a predicate `P : Set J.obj → Prop` on the underlying type
of `J : CardinalDirectedPoset κ` such that all the subsets satisfying `P`
are `κ`-filtered, this is the functor `Subtype P ⥤ CardinalDirectedPoset κ`
which sends a subset `S` of `J` satisfying `P` to the induced
partially ordered type `J`, as an object in `CardinalDirectedPoset κ`.  -/
CategoryTheory.CardinalDirectedPoset.functorOfPredicateSet : {κ : Cardinal.{u}} →
  [inst : Fact κ.IsRegular] →
    {J : CategoryTheory.CardinalDirectedPoset κ} →
      (P : Set ↑J.obj → Prop) →
        [∀ (S : Subtype P), CategoryTheory.IsCardinalFiltered (↑↑S) κ] →
          CategoryTheory.Functor (Subtype P) (CategoryTheory.CardinalDirectedPoset κ)
-- Mathlib.Data.Fin.VecNotation
Fin.tail_vecCons : ∀ {α : Type u} {n : ℕ} (x : α) (t : Fin n → α), Fin.tail (Matrix.vecCons x t) = t
-- Mathlib.RingTheory.WittVector.Isocrystal
WittVector.IsocrystalHom.mk.inj : ∀ {p : ℕ} {inst : Fact (Nat.Prime p)} {k : Type u_1} {inst_1 : CommRing k} {inst_2 : CharP k p}
  {inst_3 : PerfectRing k p} {V : Type u_2} {inst_4 : AddCommGroup V} {inst_5 : WittVector.Isocrystal p k V}
  {V₂ : Type u_3} {inst_6 : AddCommGroup V₂} {inst_7 : WittVector.Isocrystal p k V₂}
  {toLinearMap : V →ₗ[FractionRing (WittVector p k)] V₂}
  {frob_equivariant :
    ∀ (x : V),
      (WittVector.Isocrystal.frobenius p k) (toLinearMap x) = toLinearMap ((WittVector.Isocrystal.frobenius p k) x)}
  {toLinearMap_1 : V →ₗ[FractionRing (WittVector p k)] V₂}
  {frob_equivariant_1 :
    ∀ (x : V),
      (WittVector.Isocrystal.frobenius p k) (toLinearMap_1 x) =
        toLinearMap_1 ((WittVector.Isocrystal.frobenius p k) x)},
  { toLinearMap := toLinearMap, frob_equivariant := frob_equivariant } =
      { toLinearMap := toLinearMap_1, frob_equivariant := frob_equivariant_1 } →
    toLinearMap = toLinearMap_1
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.MatchResult.push : {α : Type} → Lean.Meta.LazyDiscrTree.MatchResult α → ℕ → Array α → Lean.Meta.LazyDiscrTree.MatchResult α
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
/-- the set of type (II) simplices  -/
SSet.Subcomplex.Pairing.II : {X : SSet} → {A : X.Subcomplex} → A.Pairing → Set A.N
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey_filter : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : (a : α) → β a → Bool} {k : α} (h : (↑m).WF)
  {h' : (Std.DHashMap.Internal.Raw₀.filter f m).contains k = true},
  (Std.DHashMap.Internal.Raw₀.filter f m).getKey k h' = m.getKey k ⋯
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.toEndRingHom_apply : ∀ (α : Type u_5) [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α), (CentroidHom.toEndRingHom α) f = f.toEnd
-- Mathlib.FieldTheory.IntermediateField.Algebraic
/-- If `F ≤ E` are two intermediate fields of `L / K` such that `[F : K] = [E : K]` are finite,
then `F = E`.  -/
IntermediateField.eq_of_le_of_finrank_eq : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {F E : IntermediateField K L}
  [FiniteDimensional K ↥E], F ≤ E → Module.finrank K ↥F = Module.finrank K ↥E → F = E
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.isTop.sizeOf_spec : ∀ (idx : ℕ), sizeOf (Mathlib.Tactic.Order.AtomicFact.isTop idx) = 1 + sizeOf idx
-- Std.Data.TreeMap.Raw.Basic
Std.TreeMap.Raw.instForMProdOfMonad : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} → {m : Type w → Type w₂} → [Monad m] → ForM m (Std.TreeMap.Raw α β cmp) (α × β)
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.instHasTwoOutOfThreePropertyFullSubcategoryWeakEquivalences : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  {P : CategoryTheory.ObjectProperty C} [(HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty],
  (HomotopicalAlgebra.weakEquivalences P.FullSubcategory).HasTwoOutOfThreeProperty
-- Init.GrindInstances.Ring.SInt
Lean.Grind.ISize.natCast : NatCast ISize
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.shiftIso_zero_hom_app : ∀ {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] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] (F : CategoryTheory.SingleFunctors C D A) (a : A) (X : C),
  (F.shiftIso 0 a a ⋯).hom.app X = (CategoryTheory.shiftFunctorZero D A).hom.app ((F.functor a).obj X)
-- Mathlib.Data.Finsupp.Basic
Finsupp.comapDomain_inl_sumElim : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Zero γ] (f : α →₀ γ) (g : β →₀ γ),
  Finsupp.comapDomain Sum.inl (f.sumElim g) ⋯ = f
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.le_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → ∀ {k : α}, (cmp k t.minKey!).isLE = true ↔ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.Order.Preorder.Chain
IsChain.succ : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, IsChain r s → IsChain r (SuccChain r s)
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
IsLocalDiffeomorphAt.localInverse_contMDiffOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (hf : IsLocalDiffeomorphAt I J n f x), ContMDiffOn J I n (↑hf.localInverse.toPartialEquiv) hf.localInverse.source
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
fderivWithin_continuousAlternatingMapCompContinuousLinearMap : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {H : Type u_6}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : NormedSpace 𝕜 H] {f : E → G [⋀^ι]→L[𝕜] H} {g : E → F →L[𝕜] G} {s : Set E}
  {x : E} [inst_9 : Fintype ι] [inst_10 : DecidableEq ι],
  DifferentiableWithinAt 𝕜 f s x →
    DifferentiableWithinAt 𝕜 g s x →
      UniqueDiffWithinAt 𝕜 s x →
        fderivWithin 𝕜 (fun x => (f x).compContinuousLinearMap (g x)) s x =
          ContinuousAlternatingMap.compContinuousLinearMapCLM (g x) ∘SL fderivWithin 𝕜 f s x +
            (f x).fderivCompContinuousLinearMap (g x) ∘SL fderivWithin 𝕜 g s x
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_principal_principal : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {t : Set β},
  Filter.Tendsto f (Filter.principal s) (Filter.principal t) ↔ ∀ a ∈ s, f a ∈ t
-- Mathlib.Analysis.Convex.Cone.Closure
PointedCone.coe_closure : ∀ {𝕜 : Type u_1} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : IsOrderedRing 𝕜] {E : Type u_2}
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : ContinuousAdd E] [inst_6 : Module 𝕜 E]
  [inst_7 : ContinuousConstSMul 𝕜 E] (K : PointedCone 𝕜 E), ↑K.closure = closure ↑K
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.vsub_iUnion : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [inst : VSub α β] (s : Set β) (t : ι → Set β),
  s -ᵥ ⋃ i, t i = ⋃ i, s -ᵥ t i
-- Mathlib.Order.WithBot
WithTop.forall_ne_top : ∀ {α : Type u_1} {p : WithTop α → Prop}, (∀ (x : WithTop α), x ≠ ⊤ → p x) ↔ ∀ (x : α), p ↑x
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.coneOfConeCurry_pt : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (G : CategoryTheory.Functor (J × K) C) {D : CategoryTheory.Limits.DiagramOfCones (CategoryTheory.Functor.curry.obj G)}
  (Q : (j : J) → CategoryTheory.Limits.IsLimit (D.obj j)) (c : CategoryTheory.Limits.Cone G),
  (CategoryTheory.Limits.coneOfConeCurry G Q c).pt = c.pt
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.MonoidalPreadditive.instAdditiveFunctorFlipCurriedTensor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C],
  (CategoryTheory.MonoidalCategory.curriedTensor C).flip.Additive
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
ExistsContDiffBumpBase.y_eq_one_of_mem_closedBall : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {D : ℝ} {x : E},
  0 < D → x ∈ Metric.closedBall 0 (1 - D) → ExistsContDiffBumpBase.y D x = 1
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.adjoin_toNonUnitalSubalgebra : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] (s : Set A),
  (NonUnitalStarAlgebra.adjoin R s).toNonUnitalSubalgebra = NonUnitalAlgebra.adjoin R (s ∪ star s)
-- Init.Data.Order.Lemmas
Std.instAssociativeMaxOfIsLinearOrderOfLawfulOrderMax : ∀ {α : Type u} [inst : LE α] [inst_1 : Max α] [Std.IsLinearOrder α] [Std.LawfulOrderMax α], Std.Associative max
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.endofunctorMonoidalCategory_whiskerLeft_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {F H K : CategoryTheory.Functor C C} {β : H ⟶ K} (X : C),
  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft F β).app X = β.app (F.obj X)
-- Mathlib.Order.Interval.Set.LinearOrder
/-- **Alias** of `Set.Ico_sdiff_Iio`. -/
Set.Ico_diff_Iio : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Ico a b \ Set.Iio c = Set.Ico (max a c) b
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
CategoryTheory.IsAddMonHom.Normal.exists_comp_eq_addConj : ∀ {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}
  [self : CategoryTheory.IsAddMonHom.Normal φ],
  ∃ ψ,
    CategoryTheory.CategoryStruct.comp ψ φ =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G φ)
        (CategoryTheory.AddGrpObj.addConj G)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
Left.self_le_neg : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : Preorder α] [AddLeftMono α] {a : α}, a ≤ 0 → a ≤ -a
-- Mathlib.Analysis.Meromorphic.Order
meromorphicAt_of_meromorphicOrderAt_ne_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜}, meromorphicOrderAt f x ≠ 0 → MeromorphicAt f x
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.mem_singleton : ∀ {α : Type u_1} [inst : TopologicalSpace α] (x y : α), x ∈ {y} ↔ x = y
-- Mathlib.RingTheory.FractionalIdeal.Basic
/-- Map an ideal `I` to a fractional ideal by forgetting `I` is integral.

This is the function that implements the coercion `Ideal R → FractionalIdeal S P`.  -/
FractionalIdeal.coeIdeal : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} → {P : Type u_2} → [inst_1 : CommRing P] → [inst_2 : Algebra R P] → Ideal R → FractionalIdeal S P
-- Init.Prelude
Nat.le_of_ble_eq_true : ∀ {n m : ℕ}, n.ble m = true → n ≤ m
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
hasProd_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α]
  {L : SummationFilter β} [ContinuousMul α] {f : γ → β → α} {a : γ → α} {s : Finset γ},
  (∀ i ∈ s, HasProd (f i) (a i) L) → HasProd (fun b => ∏ i ∈ s, f i b) (∏ i ∈ s, a i) L
-- Mathlib.SetTheory.Ordinal.Veblen
_private.Mathlib.SetTheory.Ordinal.Veblen.0.Ordinal.veblenWith.match_1.eq_1 : ∀ (o : Ordinal.{u_1}) (motive : { x // x ∈ Set.Iio o } → Sort u_2) (x : Ordinal.{u_1}) (property : x ∈ Set.Iio o)
  (h_1 : (x : Ordinal.{u_1}) → (property : x ∈ Set.Iio o) → motive ⟨x, property⟩),
  (match ⟨x, property⟩ with
    | ⟨x, property⟩ => h_1 x property) =
    h_1 x property
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.equivComma_functor_map_left_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {X Y : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D} (η : X ⟶ Y) (X_1 : C),
  (CategoryTheory.WithTerminal.equivComma.functor.map η).left.app X_1 = η.app (CategoryTheory.WithTerminal.incl.obj X_1)
-- Init.Data.Nat.Coprime
Nat.Coprime.mul_gcd : ∀ {m n : ℕ}, m.Coprime n → ∀ (k : ℕ), (m * n).gcd k = m.gcd k * n.gcd k
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.EdgeLabeling.compRight_get : ∀ {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {K' : Type u_4} {C : G.EdgeLabeling K} (f : K → K') (x y : V)
  (h : G.Adj x y), (C.compRight f).get x y h = f (C.get x y h)
-- Mathlib.Data.FunLike.IsApply
IsDivApply.mk : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} [inst : FunLike F α β] [inst_1 : Div β]
  [inst_2 : Div F], (∀ (f g : F) (x : α), (f / g) x = f x / g x) → IsDivApply F α β
-- Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
CochainComplex.singleFunctors.eq_1 : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C],
  CochainComplex.singleFunctors C =
    { functor := fun n => HomologicalComplex.single C (ComplexShape.up ℤ) n,
      shiftIso := fun n a a' ha' =>
        CategoryTheory.NatIso.ofComponents
          (fun X => HomologicalComplex.Hom.isoOfComponents (fun i => CategoryTheory.eqToIso ⋯) ⋯) ⋯,
      shiftIso_zero := ⋯, shiftIso_add := ⋯ }
-- Mathlib.Topology.ClopenBox
/-- Every clopen set in a product of two compact spaces
is a union of finitely many clopen boxes.  -/
TopologicalSpace.Clopens.exists_finset_eq_sup_prod : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [CompactSpace Y]
  [CompactSpace X] (W : TopologicalSpace.Clopens (X × Y)), ∃ I, W = I.sup fun i => i.1 ×ˢ i.2
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Subalgebra.mulMap_comm : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (A B : Subalgebra R S), B.mulMap A = (A.mulMap B).comp ↑(Algebra.TensorProduct.comm R ↥B ↥A)
-- Std.Data.ByteSlice
instSliceableByteArrayNatByteSlice_3 : Std.Roc.Sliceable ByteArray ℕ ByteSlice
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_inter_of_mem_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → (m₁ ∩ m₂).get? k = m₁.get? k
-- Mathlib.Algebra.Group.Defs
/-- If all additions cancel on the left then every element is add-left-regular.  -/
IsAddLeftRegular.all : ∀ {R : Type u_2} [inst : Add R] [IsLeftCancelAdd R] (g : R), IsAddLeftRegular g
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.CanonArgKey.mk.injEq : ∀ (f : Lean.Expr) (i : ℕ) (arg f_1 : Lean.Expr) (i_1 : ℕ) (arg_1 : Lean.Expr),
  ({ f := f, i := i, arg := arg } = { f := f_1, i := i_1, arg := arg_1 }) = (f = f_1 ∧ i = i_1 ∧ arg = arg_1)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.Ring.of_apply : ∀ {ι : Type u_2} [inst : Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  [inst_4 : (i : ι) → NonAssocSemiring (G i)] [inst_5 : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)]
  [inst_6 : Nonempty ι] (i : ι) (x : G i), (DirectLimit.Ring.of G f i) x = ⟦⟨i, x⟩⟧
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.Equation.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R) (P : Fin 3 → R),
  W'.Equation P = ((MvPolynomial.eval P) W'.polynomial = 0)
-- Init.Data.Int.DivMod.Lemmas
Int.fdiv_eq_ediv_of_nonneg : ∀ (a : ℤ) {b : ℤ}, 0 ≤ b → a.fdiv b = a / b