mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Ray
SameRay.sameRay_comm : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {x y : M}, SameRay R x y ↔ SameRay R y x
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.VectorMeasure.ennrealVariation.eq_1 : ∀ {X : Type u_1} {mX : MeasurableSpace X} {V : Type u_2} [inst : TopologicalSpace V] [inst_1 : ENormedAddCommMonoid V]
  [inst_2 : T2Space V] (μ : MeasureTheory.VectorMeasure X V), μ.ennrealVariation = μ.variation.toENNRealVectorMeasure
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.coreS : Lean.Expr →
  Lean.Expr →
    Lean.Meta.Grind.Arith.CommRing.SemiringExpr →
      Lean.Meta.Grind.Arith.CommRing.SemiringExpr →
        Lean.Meta.Grind.Arith.CommRing.RingExpr →
          Lean.Meta.Grind.Arith.CommRing.RingExpr → Lean.Meta.Grind.Arith.CommRing.EqCnstrProof
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.appr.eq_2 : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]) (n : ℕ),
  x.appr n.succ =
    if hy : x - ↑(x.appr n) = 0 then x.appr n
    else
      have u := ↑(PadicInt.unitCoeff hy);
      x.appr n + p ^ n * (PadicInt.toZMod (u * ↑p ^ (↑(x - ↑(x.appr n)).valuation - ↑n).natAbs)).val
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.instInhabited : {R : Type u_1} →
  [inst : AddMonoid R] →
    {S : AddSubmonoid R} → [inst_1 : AddOreLocalization.AddOreSet S] → Inhabited (AddOreLocalization S R)
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
_private.Mathlib.CategoryTheory.Bicategory.InducedBicategory.0.CategoryTheory.Bicategory.InducedBicategory.Hom.mk.inj : ∀ {B : Type u_1} {C : Type u_2} {inst : CategoryTheory.Bicategory C} {F : B → C}
  {X Y : CategoryTheory.Bicategory.InducedBicategory C F} {hom hom_1 : F X ⟶ F Y},
  { hom := hom } = { hom := hom_1 } → hom = hom_1
-- Mathlib.Algebra.Order.Group.PosPart
posPart_nonneg : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : SubNegMonoid α] (a : α), 0 ≤ a⁺
-- Mathlib.Algebra.Algebra.Tower
AlgEquiv.toAlgHom_restrictScalars : ∀ (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B]
  (f : A ≃ₐ[S] B), ↑(AlgEquiv.restrictScalars R f) = AlgHom.restrictScalars R ↑f
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.unitIso_hom_app_hom_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C)
  (X_1 : CategoryTheory.Discrete PUnit.{w + 1}),
  ((CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.unitIso C).hom.app X).hom.app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj X_1)
-- Mathlib.Data.Nat.Init
Nat.two_le_iff : ∀ (n : ℕ), 2 ≤ n ↔ n ≠ 0 ∧ n ≠ 1
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.mapBifunctorLeftUnitor.congr_simp : ∀ {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : Zero I] [inst_3 : DecidableEq I]
  [inst_4 : CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C)
  (e e_1 : F.obj X ≅ CategoryTheory.Functor.id D),
  e = e_1 →
    ∀ [inst_5 : ∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)]
      (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) (Y : CategoryTheory.GradedObject J D)
      [inst_6 :
        (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj
              Y).HasMap
          p],
      CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y =
        CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e_1 p hp Y
-- Mathlib.ModelTheory.Order
/-- Any model of a theory of linear orders is a linear order.  -/
FirstOrder.Language.linearOrderOfModels : (L : FirstOrder.Language) →
  (M : Type w') →
    [inst : L.IsOrdered] →
      [inst_1 : L.Structure M] →
        [h : M ⊨ L.linearOrderTheory] →
          [DecidableRel fun a b => FirstOrder.Language.Structure.RelMap FirstOrder.Language.leSymb ![a, b]] →
            LinearOrder M
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Generators.toKaehler_cotangentSpaceBasis : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type w}
  {P : Algebra.Generators R S ι} (i : ι),
  P.toExtension.toKaehler (P.cotangentSpaceBasis i) = (KaehlerDifferential.D R S) (P.val i)
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- (Disjoint) union of seminorm families.  -/
SeminormFamily.sigma : {𝕜 : Type u_2} →
  {E : Type u_6} →
    {ι : Type u_9} →
      [inst : NormedField 𝕜] →
        [inst_1 : AddCommGroup E] →
          [inst_2 : Module 𝕜 E] →
            {κ : ι → Type u_11} → ((i : ι) → SeminormFamily 𝕜 E (κ i)) → SeminormFamily 𝕜 E ((i : ι) × κ i)
-- Lean.Data.JsonRpc
/-- A request message to describe a request between the client and the server. Every processed request must send a response back to the sender of the request.  -/
Lean.JsonRpc.Message.request : Lean.JsonRpc.RequestID → String → Option Lean.Json.Structured → Lean.JsonRpc.Message
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.nil_isSubwalk_iff_exists : ∀ {V : Type u_1} {G : SimpleGraph V} {u' u v : V} (q : G.Walk u v),
  SimpleGraph.Walk.nil.IsSubwalk q ↔ ∃ ru rv, q = ru.append rv
-- Mathlib.Data.Finsupp.Basic
Finsupp.sum_filter_index : ∀ {α : Type u_1} {M : Type u_5} {N : Type u_6} [inst : Zero M] (p : α → Prop) [inst_1 : DecidablePred p] (f : α →₀ M)
  [inst_2 : AddCommMonoid N] (g : α → M → N), (Finsupp.filter p f).sum g = ∑ x ∈ (Finsupp.filter p f).support, g x (f x)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.mk'_surjective : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) (z : N), ∃ x y, f.mk' x y = z
-- Mathlib.CategoryTheory.Sites.Preserves
/-- The two parallel maps in the equalizer diagram for the sheaf condition corresponding to the
inclusion maps in a disjoint coproduct are equal.
 -/
CategoryTheory.Presieve.firstMap_eq_secondMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : C} (F : CategoryTheory.Functor Cᵒᵖ (Type w)),
  CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a) →
    ∀ (hI : CategoryTheory.Limits.IsInitial I) {α : Type u_1} [inst_1 : Small.{w, u_1} α] {X : α → C}
      (c : CategoryTheory.Limits.Cofan X) [inst_2 : (CategoryTheory.Presieve.ofArrows X c.inj).HasPairwisePullbacks]
      [inst_3 : CategoryTheory.Limits.HasInitial C] [∀ (i : α), CategoryTheory.Mono (c.inj i)],
      (Pairwise fun i j =>
          CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to (X i)) (CategoryTheory.Limits.initial.to (X j))
            (c.inj i) (c.inj j)) →
        CategoryTheory.Equalizer.Presieve.Arrows.firstMap F X c.inj =
          CategoryTheory.Equalizer.Presieve.Arrows.secondMap F X c.inj
-- Mathlib.Topology.Hom.Open
ContinuousOpenMap.id_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α →CO β),
  (ContinuousOpenMap.id β).comp f = f
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Trie.brecOn_1.eq : ∀ {α : Type} {motive_1 : Lean.Meta.DiscrTree.Trie α → Sort u}
  {motive_2 : Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) → Sort u}
  {motive_3 : List (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) → Sort u}
  {motive_4 : Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α → Sort u}
  (t : Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α))
  (F_1 : (t : Lean.Meta.DiscrTree.Trie α) → t.below → motive_1 t)
  (F_2 :
    (t : Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)) →
      Lean.Meta.DiscrTree.Trie.below_1 t → motive_2 t)
  (F_3 :
    (t : List (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)) → Lean.Meta.DiscrTree.Trie.below_2 t → motive_3 t)
  (F_4 : (t : Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) → Lean.Meta.DiscrTree.Trie.below_3 t → motive_4 t),
  Lean.Meta.DiscrTree.Trie.brecOn_1 t F_1 F_2 F_3 F_4 = F_2 t (Lean.Meta.DiscrTree.Trie.brecOn_1.go t F_1 F_2 F_3 F_4).2
-- Mathlib.ModelTheory.Fraisse
/-- Any class in the age of a structure has a representative which is a finitely generated
substructure.  -/
FirstOrder.Language.age.has_representative_as_substructure : ∀ {L : FirstOrder.Language} (M : Type w) [inst : L.Structure M],
  ∀ C ∈ Quotient.mk' '' L.age M, ∃ V, ⟦{ α := ↥↑V, str := inferInstance }⟧ = C
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrableOn.mono_measure : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ ν : MeasureTheory.Measure X} {s : Set X},
  MeasureTheory.LocallyIntegrableOn f s μ → ν ≤ μ → MeasureTheory.LocallyIntegrableOn f s ν
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.PolynomialC.InductionObj.coeffSubmodule_mapRingHom_comp : ∀ {R₀ : Type u_1} {R : Type u_2} {S : Type u_3} [inst : CommRing R₀] [inst_1 : CommRing R] [inst_2 : Algebra R₀ R]
  [inst_3 : CommRing S] [inst_4 : Algebra R₀ S] {n : ℕ} (e : ChevalleyThm.PolynomialC.InductionObj✝ R n)
  (f : R →ₐ[R₀] S),
  ChevalleyThm.PolynomialC.InductionObj.coeffSubmodule✝ R₀
      { val := ⇑(Polynomial.mapRingHom ↑f) ∘ ChevalleyThm.PolynomialC.InductionObj.val✝ e } =
    Submodule.map f.toLinearMap (ChevalleyThm.PolynomialC.InductionObj.coeffSubmodule✝ R₀ e)
-- Mathlib.Data.PFunctor.Multivariate.M
/-- Constructor for M-types  -/
MvPFunctor.M.mk : {n : ℕ} → (P : MvPFunctor.{u} (n + 1)) → {α : TypeVec.{u} n} → ↑P (α ::: P.M α) → P.M α
-- Mathlib.Algebra.Free
FreeAddSemigroup.mk.inj : ∀ {α : Type u} {head : α} {tail : List α} {head_1 : α} {tail_1 : List α},
  { head := head, tail := tail } = { head := head_1, tail := tail_1 } → head = head_1 ∧ tail = tail_1
-- Mathlib.LinearAlgebra.Dimension.Finite
/-- **Alias** of `Module.exists_set_linearIndependent_of_lt_rank`. -/
exists_set_linearIndependent_of_lt_rank : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {c : Cardinal.{v}},
  c < Module.rank R M → ∃ s, Cardinal.mk ↑s = c ∧ LinearIndepOn R id s
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.eapproxDiff.eq_1 : ∀ {α : Type u_1} [inst : MeasurableSpace α] (f : α → ENNReal),
  MeasureTheory.SimpleFunc.eapproxDiff f 0 =
    MeasureTheory.SimpleFunc.map ENNReal.toNNReal (MeasureTheory.SimpleFunc.eapprox f 0)
-- Mathlib.RingTheory.PrincipalIdealDomainOfPrime
/-- If all prime ideals in a commutative ring are principal, so are all other ideals.  -/
IsPrincipalIdealRing.of_prime : ∀ {R : Type u_1} [inst : CommSemiring R],
  (∀ (P : Ideal R), P.IsPrime → Submodule.IsPrincipal P) → IsPrincipalIdealRing R
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfcHomSuperset_continuous : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Ring A] [inst_6 : StarRing A]
  [inst_7 : TopologicalSpace A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A} (ha : p a)
  {s : Set R} (hs : spectrum R a ⊆ s), Continuous ⇑(cfcHomSuperset ha hs)
-- Batteries.Data.Vector.Basic
/-- Fold an effectful function `f` over the array from the left, returning the list of partial results.
 -/
Vector.scanlM : {m : Type u_1 → Type u_2} →
  {β : Type u_1} → {α : Type u_3} → {n : ℕ} → [Monad m] → (β → α → m β) → β → Vector α n → m (Vector β (n + 1))
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.curry.injEq : ∀ (ak : Mathlib.Tactic.ITauto.AndKind) (p : Mathlib.Tactic.ITauto.Proof) (ak_1 : Mathlib.Tactic.ITauto.AndKind)
  (p_1 : Mathlib.Tactic.ITauto.Proof),
  (Mathlib.Tactic.ITauto.Proof.curry ak p = Mathlib.Tactic.ITauto.Proof.curry ak_1 p_1) = (ak = ak_1 ∧ p = p_1)
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
EReal.log_exp : ∀ (x : EReal), x.exp.log = x
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_obj : ∀ {X Y : SSet.Truncated 2}
  (x : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 }))
  (y : Y.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })),
  (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).obj
      (SSet.Truncated.HomotopyCategory.mk x, SSet.Truncated.HomotopyCategory.mk y) =
    SSet.Truncated.HomotopyCategory.mk (x, y)
-- Mathlib.LinearAlgebra.Projectivization.Action
/-- The action of the special linear group on `ℙ F (ι → F)` factors through the
projective special linear group `PSL = SL ⧸ Z(SL)`.  -/
Projectivization.PSLAction.toPermHom : {K : Type u_1} →
  [inst : Field K] →
    {ι : Type u_3} →
      [inst_1 : Fintype ι] →
        [inst_2 : DecidableEq ι] → Matrix.ProjectiveSpecialLinearGroup ι K →* Equiv.Perm (Projectivization K (ι → K))
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Construct an isomorphism in `P.CostructuredArrow Q F X` by giving the isomorphism
on the underlying objects of `C`.  -/
CategoryTheory.MorphismProperty.CostructuredArrow.isoMk : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{u_3, u_1} C] →
      [inst_1 : CategoryTheory.Category.{u_4, u_2} D] →
        {P : CategoryTheory.MorphismProperty D} →
          {Q : CategoryTheory.MorphismProperty C} →
            [inst_2 : Q.IsMultiplicative] →
              {F : CategoryTheory.Functor C D} →
                {X : D} →
                  {A B : P.CostructuredArrow Q F X} →
                    (f : A.left ≅ B.left) →
                      Q f.hom →
                        Q f.inv →
                          autoParam (CategoryTheory.CategoryStruct.comp (F.map f.hom) B.hom = A.hom)
                              CategoryTheory.MorphismProperty.CostructuredArrow.isoMk._auto_1 →
                            (A ≅ B)
-- Lean.Server.AsyncList
/-- An async IO list is like a lazy list but instead of being *unevaluated* `Thunk`s,
`delayed` suffixes are `Task`s *being evaluated asynchronously*. A delayed suffix can signal the end
of computation (successful or due to a failure) with a terminating value of type `ε`.  -/
Lean.AsyncList : Type u → Type v → Type (max u v)
-- Mathlib.Logic.Equiv.Defs
/-- A `Sigma` with `PLift` fibers is equivalent to the subtype.  -/
Equiv.sigmaPLiftEquivSubtype : {α : Type v} → (P : α → Prop) → (i : α) × PLift (P i) ≃ Subtype P
-- Mathlib.Analysis.Complex.Norm
Complex.normSq_eq_norm_sq : ∀ (z : ℂ), Complex.normSq z = ‖z‖ ^ 2
-- Batteries.Data.BinomialHeap.Basic
/-- `O(log n)`. Get the smallest element in the heap, if it has an element.  -/
Batteries.BinomialHeap.Imp.Heap.head? : {α : Type u_1} → (α → α → Bool) → Batteries.BinomialHeap.Imp.Heap α → Option α
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
AEMeasurable.ennreal_tsum : ∀ {α : Type u_1} {mα : MeasurableSpace α} {ι : Type u_5} [Countable ι] {f : ι → α → ENNReal}
  {μ : MeasureTheory.Measure α}, (∀ (i : ι), AEMeasurable (f i) μ) → AEMeasurable (fun x => ∑' (i : ι), f i x) μ
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- A subalgebra over a ring is also a `Subring`.  -/
Subalgebra.toSubring : {R : Type u} →
  {A : Type v} → [inst : CommRing R] → [inst_1 : Ring A] → [inst_2 : Algebra R A] → Subalgebra R A → Subring A
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.mkOfHomEquiv_unit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : CategoryTheory.Adjunction.CoreHomEquiv F G)
  (X : C),
  (CategoryTheory.Adjunction.mkOfHomEquiv adj).unit.app X =
    (adj.homEquiv X (F.obj X)) (CategoryTheory.CategoryStruct.id (F.obj X))
-- Init.Data.Ord.Basic
Ordering.isLE_eq_isLT_or_isEq : ∀ {o : Ordering}, o.isLE = (o.isLT || o.isEq)
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.ofEquivalence_truth : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (𝒞₁ : CategoryTheory.Subobject.Classifier C) (e : C ≌ D), (𝒞₁.ofEquivalence e).truth = e.functor.map 𝒞₁.truth
-- Lean.Parser.Term.Basic
Lean.Parser.Term.structInstFieldBinder : Lean.Parser.Parser
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- Restrict the codomain of a non-unital star algebra homomorphism.  -/
NonUnitalStarAlgHom.codRestrict : {F : Type v'} →
  {R : Type u} →
    {A : Type v} →
      {B : Type w} →
        [inst : CommSemiring R] →
          [inst_1 : NonUnitalNonAssocSemiring A] →
            [inst_2 : Module R A] →
              [inst_3 : Star A] →
                [inst_4 : NonUnitalNonAssocSemiring B] →
                  [inst_5 : Module R B] →
                    [inst_6 : Star B] →
                      [inst_7 : FunLike F A B] →
                        [NonUnitalAlgHomClass F R A B] →
                          [StarHomClass F A B] →
                            (f : F) → (S : NonUnitalStarSubalgebra R B) → (∀ (x : A), f x ∈ S) → A →⋆ₙₐ[R] ↥S
-- Mathlib.Data.Fin.SuccPred
Fin.castSucc_pred_add_one_eq : ∀ {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ 0), (a.pred ha).castSucc + 1 = a
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.truncGEMap.eq_1 : ∀ {ι : 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]
  {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [inst_2 : e.IsTruncGE]
  [inst_3 : ∀ (i' : ι'), K.HasHomology i'] [inst_4 : ∀ (i' : ι'), L.HasHomology i']
  [inst_5 : CategoryTheory.Limits.HasZeroObject C],
  HomologicalComplex.truncGEMap φ e = (e.extendFunctor C).map (HomologicalComplex.truncGE'Map φ e)
-- Mathlib.Data.Set.Image
Set.isCompl_range_some_none : ∀ (α : Type u_5), IsCompl (Set.range some) {none}
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.toEquiv_injective : ∀ {α : Type u_9} {β : Type u_10} [inst : Mul α] [inst_1 : Mul β], Function.Injective MulEquiv.toEquiv
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepSets.biUnion : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ι → Set (Set Ω)}
  {s' : Set (Set Ω)} {u : Set ι},
  (∀ n ∈ u, ProbabilityTheory.IndepSets (s n) s' μ) → ProbabilityTheory.IndepSets (⋃ n ∈ u, s n) s' μ
-- Mathlib.Topology.Algebra.Valued.WithVal
Rat.ringOfIntegersWithValEquiv_apply : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℚ Γ₀)
  (a : NumberField.RingOfIntegers (WithVal v)),
  (Rat.ringOfIntegersWithValEquiv v) a =
    (IsIntegralClosure.equiv ℤ ℤ (WithVal v) (NumberField.RingOfIntegers (WithVal v))).symm a
-- Init.Data.List.ToArray
List.insertIdxIfInBounds_toArray : ∀ {α : Type u_1} (l : List α) (i : ℕ) (a : α), l.toArray.insertIdxIfInBounds i a = (l.insertIdx i a).toArray
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, k ∈ t₂ → (t₁ ∩ t₂).getKey! k = t₁.getKey! k
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.ι_preimage_self : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens), (TopologicalSpace.Opens.map U.ι.base).obj U = ⊤
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- The second arrow.  -/
CategoryTheory.GrothendieckTopology.Cover.Relation.snd : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} → {J : CategoryTheory.GrothendieckTopology C} → {S : J.Cover X} → S.Relation → S.Arrow
-- Mathlib.CategoryTheory.Monoidal.Hopf_
/-- Morphisms of Hopf monoids intertwine the antipodes.  -/
CategoryTheory.HopfObj.hom_antipode : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {A B : C} [inst_3 : CategoryTheory.HopfObj A]
  [inst_4 : CategoryTheory.HopfObj B] (f : A ⟶ B) [CategoryTheory.IsBimonHom f],
  CategoryTheory.CategoryStruct.comp f CategoryTheory.HopfObj.antipode =
    CategoryTheory.CategoryStruct.comp CategoryTheory.HopfObj.antipode f
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- Continuity from below:
the measure of the union of a monotone family of sets is equal to the supremum of their measures.
The theorem assumes that the `atTop` filter on the index set is countably generated,
so it works for a family indexed by a countable type, as well as `ℝ`.  -/
Monotone.measure_iUnion : ∀ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Preorder ι]
  [IsDirectedOrder ι] [Filter.atTop.IsCountablyGenerated] {s : ι → Set α}, Monotone s → μ (⋃ i, s i) = ⨆ i, μ (s i)
-- Mathlib.ModelTheory.Definability
Set.termDefinable_empty_iff : ∀ {M : Type w} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {f : (α → M) → M},
  ∅.TermDefinable L f ↔ ∃ φ, f = fun v => FirstOrder.Language.Term.realize v φ
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrableOn_zero : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} {s : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε'] [inst_1 : ESeminormedAddMonoid ε'], MeasureTheory.IntegrableOn (fun x => 0) s μ
-- Init.Data.List.SplitOn.Lemmas
List.splitOnP_cons_eq_if_splitOnPPrepend : ∀ {α : Type u_1} {p : α → Bool} {x : α} {xs : List α},
  List.splitOnP p (x :: xs) = if p x = true then [] :: List.splitOnP p xs else List.splitOnPPrepend p xs [x]
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
/-- If `g : Y ⟶ Z` is iso, then `X ×[Z] Y ≅ X`. This is the explicit limit cone.  -/
CategoryTheory.Limits.pullbackConeOfRightIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → [CategoryTheory.IsIso g] → CategoryTheory.Limits.PullbackCone f g
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.toList_cons : ∀ {α : Type u_1} {k : α} {β : α → Type u_2} {v : β k} {tree : Std.DTreeMap.Internal.Impl α β}
  {next : Std.DTreeMap.Internal.Zipper α β},
  (Std.DTreeMap.Internal.Zipper.cons k v tree next).toList = ⟨k, v⟩ :: tree.toList ++ next.toList
-- Mathlib.NumberTheory.LegendreSymbol.ZModChar
ZMod.χ₈_apply : ∀ (a : ZMod 8),
  ZMod.χ₈ a =
    match a with
    | 0 => 0
    | 2 => 0
    | 4 => 0
    | 6 => 0
    | 1 => 1
    | 7 => 1
    | 3 => -1
    | 5 => -1
-- Mathlib.MeasureTheory.Group.Arithmetic
Subgroup.instMeasurableSMul : ∀ {G : Type u_2} {α : Type u_3} [inst : MeasurableSpace G] [inst_1 : MeasurableSpace α] [inst_2 : Group G]
  [inst_3 : MulAction G α] [MeasurableSMul G α] (s : Subgroup G), MeasurableSMul (↥s) α
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  {F : CategoryTheory.Functor C FintypeCat} {A B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F}
  (val : A.obj ⟶ B.obj)
  (comp :
    autoParam ((CategoryTheory.ConcreteCategory.hom (F.map val)) A.pt = B.pt)
      CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.comp._autoParam)
  (val_1 : A.obj ⟶ B.obj)
  (comp_1 :
    autoParam ((CategoryTheory.ConcreteCategory.hom (F.map val_1)) A.pt = B.pt)
      CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.comp._autoParam),
  ({ val := val, comp := comp } = { val := val_1, comp := comp_1 }) = (val = val_1)