mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
/-- The Cartan matrix of a crystallographic root pairing, with respect to a base `b`.  -/
RootPairing.Base.cartanMatrix : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  {P : RootPairing ι R M N} → (b : P.Base) → [P.IsCrystallographic] → Matrix ↥b.support ↥b.support ℤ
-- Mathlib.Geometry.Diffeology.Basic
/-- A smooth function between spaces that are equipped with the D-topology is continuous.  -/
Diffeology.DSmooth.continuous' : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : DiffeologicalSpace X]
  [Diffeology.IsDTopologyCompatible X] [inst_3 : TopologicalSpace Y] [inst_4 : DiffeologicalSpace Y]
  [Diffeology.IsDTopologyCompatible Y] {f : X → Y}, Diffeology.DSmooth f → Continuous f
-- Mathlib.Algebra.Algebra.Equiv
RingEquiv.toNatAlgEquiv_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (f : R ≃+* S) (a : R), f.toNatAlgEquiv a = f a
-- Init.Data.Nat.Bitwise.Basic
_private.Init.Data.Nat.Bitwise.Basic.0.Nat.bitwise.eq_def : ∀ (f : Bool → Bool → Bool) (n m : ℕ),
  Nat.bitwise f n m =
    if n = 0 then if f false true = true then m else 0
    else
      if m = 0 then if f true false = true then n else 0
      else
        have n' := n / 2;
        have m' := m / 2;
        let b₁ := n % 2 = 1;
        let b₂ := m % 2 = 1;
        have r := Nat.bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r
-- Mathlib.LinearAlgebra.TensorPower.Symmetric
/-- The `ι`-indexed symmetric tensor power of a semimodule `M` over a commutative semiring `R`
is the quotient of the `ι`-indexed tensor power of `M` by the relation that two tensors are equal
if they are related by a permutation of `ι`.  -/
TensorProduct.«termSym[_]__» : Lean.ParserDescr
-- Mathlib.Algebra.Group.Subgroup.Basic
Group.conjugatesOfSet_mono : ∀ {G : Type u_1} [inst : Group G] {s t : Set G}, s ⊆ t → Group.conjugatesOfSet s ⊆ Group.conjugatesOfSet t
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.ImageMap.map_uniq_aux : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  [inst_1 : CategoryTheory.Limits.HasImage f.hom] [inst_2 : CategoryTheory.Limits.HasImage g.hom] {sq : f ⟶ g}
  (map : CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom),
  autoParam
      (CategoryTheory.CategoryStruct.comp map (CategoryTheory.Limits.image.ι g.hom) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom) (CategoryTheory.Arrow.Hom.right sq))
      CategoryTheory.Limits.ImageMap.map_uniq_aux._auto_1 →
    ∀ (map' : CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom),
      CategoryTheory.CategoryStruct.comp map' (CategoryTheory.Limits.image.ι g.hom) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom) (CategoryTheory.Arrow.Hom.right sq) →
        map = map'
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.Functor.flip_map_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) {d d' : D} (f : d ⟶ d') (c : C),
  (F.flip.map f).app c = (F.obj c).map f
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.spine.eq_1 : ∀ (X : SSet) (n : ℕ), X.spine n = ((SSet.truncation (n + 1)).obj X).spine n ⋯
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.OneHypercover.mk'_toPreOneHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {S : C}
  (E : CategoryTheory.PreOneHypercover S) [inst_1 : E.HasPullbacks] (mem₀ : E.sieve₀ ∈ J S)
  (mem₁' : ∀ (i₁ i₂ : E.I₀), E.sieve₁' i₁ i₂ ∈ J (CategoryTheory.Limits.pullback (E.f i₁) (E.f i₂))),
  (CategoryTheory.GrothendieckTopology.OneHypercover.mk' E mem₀ mem₁').toPreOneHypercover = E
-- Aesop.Rule.Forward
Aesop.ForwardRule.instToString : ToString Aesop.ForwardRule
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
lt_abs : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] {a b : α}, a < |b| ↔ a < b ∨ a < -b
-- Mathlib.Combinatorics.Colex
Finset.Colex.isInitSeg_empty : ∀ {α : Type u_1} [inst : LinearOrder α] {r : ℕ}, Finset.Colex.IsInitSeg ∅ r
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.restrictIndex_I₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {T : C} (E : CategoryTheory.PreZeroHypercover T) {ι : Type w'}
  (f : ι → E.I₀), (E.restrictIndex f).I₀ = ι
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.Is.mk : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X : C},
  P X → P.Is X
-- Mathlib.RingTheory.HahnSeries.Multiplication
/-- The group of invertible Hahn series close to 1, i.e., those series such that subtracting 1
yields a series with strictly positive `orderTop`.  -/
HahnSeries.orderTopSubOnePos : (Γ : Type u_6) →
  (R : Type u_7) →
    [inst : LinearOrder Γ] →
      [inst_1 : AddCommMonoid Γ] →
        [inst_2 : IsOrderedCancelAddMonoid Γ] → [inst_3 : CommRing R] → Subgroup (HahnSeries Γ R)ˣ
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.EMatchDiagNode.origin : Lean.Meta.Grind.EMatchDiagNode → Lean.Meta.Grind.Origin
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.functoriality_obj_π_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C)
  (G : CategoryTheory.Functor C D) (A : CategoryTheory.Limits.Cone F) (j : J),
  ((CategoryTheory.Limits.Cone.functoriality F G).obj A).π.app j = G.map (A.π.app j)
-- Mathlib.Data.Set.Sigma
Set.sigma_sdiff_sigma : ∀ {ι : Type u_1} {α : ι → Type u_3} {s₁ s₂ : Set ι} {t₁ t₂ : (i : ι) → Set (α i)},
  s₁.sigma t₁ \ s₂.sigma t₂ = s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- If each `Z i` is locally path-connected and all but finitely many are path-connected, then
`∀ i, Z i` is locally path-connected.  -/
Pi.locallyPathConnectedSpace_of_finite_not_pathConnectedSpace : ∀ {ι : Type u_3} {Z : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (Z i)]
  [∀ (i : ι), LocallyPathConnectedSpace (Z i)],
  {i | ¬PathConnectedSpace (Z i)}.Finite → LocallyPathConnectedSpace ((i : ι) → Z i)
-- Mathlib.Topology.AlexandrovDiscrete
isOpen_iInter₂ : ∀ {ι : Sort u_1} {κ : ι → Sort u_2} {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α]
  {f : (i : ι) → κ i → Set α}, (∀ (i : ι) (j : κ i), IsOpen (f i j)) → IsOpen (⋂ i, ⋂ j, f i j)
-- Mathlib.Algebra.Group.EvenFunction
Function.Even.add : ∀ {α : Type u_1} {β : Type u_2} [inst : Neg α] [inst_1 : Add β] {f g : α → β},
  Function.Even f → Function.Even g → Function.Even (f + g)
-- Mathlib.CategoryTheory.Adjunction.Comma
/-- If each structured arrow category on `G` has an initial object, we have a constructed left adjoint
to `G`.
 -/
CategoryTheory.adjunctionOfStructuredArrowInitials : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor D C) →
          [inst_2 : ∀ (A : C), CategoryTheory.Limits.HasInitial (CategoryTheory.StructuredArrow A G)] →
            CategoryTheory.leftAdjointOfStructuredArrowInitials G ⊣ G
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.mk : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Reader.State dir →
    ByteArray.Iterator → Std.Http.Protocol.H1.Message.Head dir → ℕ → ℕ → ℕ → Bool → Std.Http.Protocol.H1.Reader dir
-- Mathlib.Data.Int.Bitwise
Int.bitwise.eq_2 : ∀ (f : Bool → Bool → Bool) (m n : ℕ),
  Int.bitwise f (Int.ofNat m) (Int.negSucc n) = Int.natBitwise (fun x y => f x !y) m n
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.findSome?_eq_match_step : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β]
  [inst_2 : Std.IteratorLoop α m m] [LawfulMonad m] [Std.Iterators.Finite α m] [Std.LawfulIteratorLoop α m m]
  {it : Std.IterM m β} {f : β → Option γ},
  it.findSome? f = do
    let __do_lift ← it.step
    match ↑__do_lift.inflate with
      | Std.IterStep.yield it' out =>
        match f out with
        | none => it'.findSome? f
        | some fx => pure (some fx)
      | Std.IterStep.skip it' => it'.findSome? f
      | Std.IterStep.done => pure none
-- Mathlib.Algebra.SkewMonoidAlgebra.Single
SkewMonoidAlgebra.update_eq_erase_add_single : ∀ {M : Type u_4} {α : Type u_5} [inst : AddCommMonoid M] (f : SkewMonoidAlgebra M α) (a : α) (b : M),
  f.update a b = (SkewMonoidAlgebra.erase a) f + SkewMonoidAlgebra.single a b
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionUnitIso : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction Cᵒᵖ Dᵒᵖ] (x : D),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso x =
    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso (Opposite.op x)).symm.unop
-- Mathlib.RingTheory.Ideal.Pointwise
/-- Assume that `M` and `N` are isomorphic and act in a compatible way on `R`, then for any
ideal `I` of `R`, the stabilizer of `I` in `M` is isomorphic to the stabilizer of `I` in `N`.
 -/
Ideal.stabilizerEquiv : {M : Type u_1} →
  {R : Type u_3} →
    [inst : Group M] →
      [inst_1 : Semiring R] →
        [inst_2 : MulSemiringAction M R] →
          {N : Type u_4} →
            [inst_3 : Group N] →
              [inst_4 : MulSemiringAction N R] →
                (I : Ideal R) →
                  (e : M ≃* N) →
                    (∀ (m : M) (x : R), e m • x = m • x) → ↥(MulAction.stabilizer M I) ≃* ↥(MulAction.stabilizer N I)
-- Mathlib.CategoryTheory.Limits.Creates
/-- When `F` is fully faithful, and `HasLimit (K ⋙ F)`, to show that `F` creates the limit for `K`
it suffices to show that the chosen limit point is in the essential image of `F`.
 -/
CategoryTheory.createsLimitOfFullyFaithfulOfIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                [F.Full] →
                  [F.Faithful] →
                    [inst_5 : CategoryTheory.Limits.HasLimit (K.comp F)] →
                      (X : C) → (F.obj X ≅ CategoryTheory.Limits.limit (K.comp F)) → CategoryTheory.CreatesLimit K F
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.IterM.fold_map : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {Pred EPred : Type w} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m]
  [inst_2 : Monad m] [inst_3 : Std.Internal.Do.Assertion Pred] [inst_4 : Std.Internal.Do.Assertion EPred]
  [inst_5 : Std.Internal.Do.WPMonad m Pred EPred] [inst_6 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m]
  {f : β → γ} {g : δ → γ → δ} {init : δ} {it : Std.IterM m β} {P : Pred} {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄ Std.IterM.fold (fun d b => g d (f b)) init it ⦃ Q; eQ ⦄ →
    ⦃ P ⦄ Std.IterM.fold g init (Std.IterM.map f it) ⦃ Q; eQ ⦄
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reflect_C_mul : ∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R) (r : R) (N : ℕ),
  Polynomial.reflect N (Polynomial.C r * f) = Polynomial.C r * Polynomial.reflect N f
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_snd : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g),
  CategoryTheory.CategoryStruct.comp T.SpecTensorTo (CategoryTheory.Limits.pullback.snd f g) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map T.tensorInr) (Y.fromSpecResidueField T.y)
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.symm_symm : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂),
  e.symm.symm = e
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_inter_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Inhabited β] {k : α},
  k ∈ t₂ → Std.ExtDTreeMap.Const.get! (t₁ ∩ t₂) k = Std.ExtDTreeMap.Const.get! t₁ k
-- Mathlib.Algebra.Order.CompleteField
/-- **Alias** of `ConditionallyCompleteLinearOrderedField.inducedMap_self`. -/
LinearOrderedField.inducedMap_self : ∀ {β : Type u_3} [inst : Field β] [inst_1 : ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] (b : β),
  ConditionallyCompleteLinearOrderedField.inducedMap β β b = b
-- Mathlib.Data.Sum.Basic
/-- The map from the first summand into a ternary sum.  -/
Sum3.in₀ : {α : Type u} → {β : Type v} → {γ : Type u_1} → α → α ⊕ β ⊕ γ
-- Mathlib.Algebra.Category.Grp.ForgetCorepresentable
GrpCat.forget_isCorepresentable : (CategoryTheory.forget GrpCat).IsCorepresentable
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- A finite-product-preserving functor takes additive group objects to additive group objects.  -/
CategoryTheory.Functor.mapAddGrp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            (F : CategoryTheory.Functor C D) →
              [F.Monoidal] → CategoryTheory.Functor (CategoryTheory.AddGrp C) (CategoryTheory.AddGrp D)
-- Mathlib.RingTheory.Adjoin.Polynomial.Bivariate
Polynomial.Bivariate.Transcendental.algEquivAdjoin_apply : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {x : A}
  (hx : Transcendental R x) (p : Polynomial (Polynomial R)),
  (Polynomial.Bivariate.Transcendental.algEquivAdjoin hx) p = (Polynomial.mapAlgHom (Polynomial.aeval ⟨x, ⋯⟩)) p
-- Mathlib.Topology.UniformSpace.Separation
UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity : ∀ {α : Type u} [inst : UniformSpace α] [(uniformity α).IsCountablyGenerated], CompletelyNormalSpace α
-- Mathlib.Algebra.Module.Presentation.DirectSum
Module.Presentation.directSum_relation : ∀ {A : Type u} [inst : Ring A] {ι : Type w} [inst_1 : DecidableEq ι] {M : ι → Type v}
  [inst_2 : (i : ι) → AddCommGroup (M i)] [inst_3 : (i : ι) → Module A (M i)]
  (pres : (i : ι) → Module.Presentation A (M i)) (x : (i : ι) × ((fun i => (pres i).toRelations) i).R),
  (Module.Presentation.directSum pres).relation x =
    Finsupp.embDomain (Function.Embedding.sigmaMk x.fst) ((pres x.fst).relation x.snd)
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
/-- For any `i : U ⟶ V`, `M.map i` maps the submonoid `obj U` into the submonoid `obj V`.  -/
CategoryTheory.SubmonoidFunctor.map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : CategoryTheory.Functor C MonCat}
  (self : CategoryTheory.SubmonoidFunctor M) {U V : C} (i : U ⟶ V),
  self.obj U ≤ Submonoid.comap (MonCat.Hom.hom (M.map i)) (self.obj V)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.triangle_assoc_comp_left_inv_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c) {Z : a ⟶ c}
  (h :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b)) g ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor g).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.id b) g).inv h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor f).inv g) h
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instNonUnitalNonAssocRing : {n : Type u_2} → {A : Type u_5} → [Fintype n] → [NonUnitalNonAssocRing A] → NonUnitalNonAssocRing (CStarMatrix n n A)
-- Mathlib.LinearAlgebra.TensorProduct.Quotient
/-- Let `R` be a commutative ring, `S` be an `R`-algebra, `I` is be ideal of `R`, then `S ⧸ IS` is
isomorphic to `S ⊗[R] (R ⧸ I)` as `S` modules.  -/
Ideal.qoutMapEquivTensorQout : {R : Type u_1} →
  [inst : CommRing R] →
    (S : Type u_4) →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] → {I : Ideal R} → (S ⧸ Ideal.map (algebraMap R S) I) ≃ₗ[S] TensorProduct R S (R ⧸ I)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for `>` on `BitVec`s.  -/
BitVec.reduceGT : Lean.Meta.Simp.Simproc
-- Init.Grind.AC
Lean.Grind.AC.Seq.unionFuel_k : ℕ → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq
-- Mathlib.RingTheory.LocalProperties.Basic
RingHom.PropertyIsLocal.respectsIso : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  RingHom.PropertyIsLocal P → RingHom.RespectsIso P
-- Mathlib.Logic.Basic
heq_of_eq_cast : ∀ {α β : Sort u} {a : α} {b : β} (e : β = α), a = cast e b → a ≍ b
-- Mathlib.LinearAlgebra.Determinant
/-- The determinant of `f.symm` is the inverse of that of `f` when `f` is a linear equiv.  -/
LinearEquiv.det_coe_symm : ∀ {M : Type u_2} [inst : AddCommGroup M] {𝕜 : Type u_5} [inst_1 : Field 𝕜] [inst_2 : Module 𝕜 M] (f : M ≃ₗ[𝕜] M),
  LinearMap.det ↑f.symm = (LinearMap.det ↑f)⁻¹
-- Init.Data.Vector.Lemmas
Vector.mem_push : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {x y : α}, x ∈ xs.push y ↔ x ∈ xs ∨ x = y
-- Mathlib.Analysis.Calculus.FDeriv.Congr
Filter.EventuallyEq.hasFDerivAtFilter_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f₀ f₁ : E → F} {f₀' f₁' : E →L[𝕜] F} {L : Filter (E × E)},
  Prod.map f₀ f₀ =ᶠ[L] Prod.map f₁ f₁ →
    (∀ (x : E), f₀' x = f₁' x) → (HasFDerivAtFilter f₀ f₀' L ↔ HasFDerivAtFilter f₁ f₁' L)
-- Mathlib.LinearAlgebra.Projectivization.Basic
/-- Choose a representative of `v : Projectivization K V` in `V`.  -/
Projectivization.rep : {K : Type u_1} →
  {V : Type u_2} →
    [inst : DivisionRing K] → [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → Projectivization K V → V
-- Mathlib.LinearAlgebra.QuadraticForm.Isometry
QuadraticMap.Isometry.mk.sizeOf_spec : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {N : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} [inst_7 : SizeOf R] [inst_8 : SizeOf M₁]
  [inst_9 : SizeOf M₂] [inst_10 : SizeOf N] (toLinearMap : M₁ →ₗ[R] M₂)
  (map_app' : ∀ (m : M₁), Q₂ (toLinearMap.toFun m) = Q₁ m),
  sizeOf { toLinearMap := toLinearMap, map_app' := map_app' } = 1 + sizeOf toLinearMap
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.one_add_of_omega0_le : ∀ {o : Ordinal.{u_4}}, Ordinal.omega0 ≤ o → 1 + o = o
-- Mathlib.MeasureTheory.Integral.IntegrableOn
/-- If `μ` is a measure finite at filter `l` and `f` is a function such that its norm is bounded
above at `l`, then `f` is integrable at `l`.  -/
MeasureTheory.Measure.FiniteAtFilter.integrableAtFilter : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  {f : α → E} {l : Filter α} [l.IsMeasurablyGenerated],
  StronglyMeasurableAtFilter f l μ →
    μ.FiniteAtFilter l →
      Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ f) → MeasureTheory.IntegrableAtFilter f l μ
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.addMonoidal_tensorObj_as : ∀ (M : Type u) [inst : AddMonoid M] (X Y : CategoryTheory.Discrete M),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).as = X.as + Y.as
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- The oriented angle between two nonzero vectors is plus or minus the unoriented angle.  -/
Orientation.oangle_eq_angle_or_eq_neg_angle : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V},
  x ≠ 0 → y ≠ 0 → o.oangle x y = ↑(InnerProductGeometry.angle x y) ∨ o.oangle x y = -↑(InnerProductGeometry.angle x y)
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.surjOn_log' : Set.SurjOn Real.log (Set.Iio 0) Set.univ
-- Mathlib.Algebra.Module.Submodule.Equiv
/-- A linear map `f : M →ₗ[R] M₂` with a left-inverse `g : M₂ →ₗ[R] M` defines a linear
equivalence between `M` and `f.range`.

This is a computable alternative to `LinearEquiv.ofInjective`, and a bidirectional version of
`LinearMap.rangeRestrict`.  -/
LinearEquiv.ofLeftInverse : {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₂] →
                {module_M : Module R M} →
                  {module_M₂ : Module R₂ M₂} →
                    {σ₁₂ : R →+* R₂} →
                      {σ₂₁ : R₂ →+* R} →
                        {f : M →ₛₗ[σ₁₂] M₂} →
                          [inst_4 : RingHomInvPair σ₁₂ σ₂₁] →
                            [inst_5 : RingHomInvPair σ₂₁ σ₁₂] →
                              {g : M₂ → M} → Function.LeftInverse g ⇑f → M ≃ₛₗ[σ₁₂] ↥f.range
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roc_eq_singleton_iff : ∀ {k m n : ℤ}, (m<...=n).toList = [k] ↔ n = m + 1 ∧ m + 1 = k
-- Init.Data.Array.Lemmas
Array.append_eq_toArray_iff : ∀ {α : Type u_1} {xs ys : Array α} {as : List α}, xs ++ ys = as.toArray ↔ xs.toList ++ ys.toList = as
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {l : List ((a : α) × β a)} {k : α}, (List.map Sigma.fst l).contains k = false → (m.insertMany l).get? k = m.get? k
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instMulAction : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      {R : Type u_5} → [inst_1 : Monoid R] → [MulAction R Y] → MulAction R (LocallyConstant X Y)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ : ∀ {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ X.toTopCat}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U)
  (hx : x ∈ V),
  CategoryTheory.CategoryStruct.comp (X.presheaf.germ (h.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯)
      (X.restrictStalkIso h x).inv =
    (X.restrict h).presheaf.germ V x hx
-- Lean.Meta.CongrTheorems
_private.Lean.Meta.CongrTheorems.0.Lean.Meta.mkCongrSimpCore?.mkProof : Lean.Expr → Array Lean.Meta.CongrArgKind → Lean.MetaM Lean.Expr
-- Lean.Util.CollectAxioms
_private.Lean.Util.CollectAxioms.0.Lean.instInhabitedExportedAxiomsState : Inhabited Lean.ExportedAxiomsState✝
-- Mathlib.Data.PFunctor.Univariate.M
/-- corecursor for `M F` with swapped arguments  -/
PFunctor.M.corecOn : {F : PFunctor.{uA, uB}} → {X : Type u_2} → X → (X → ↑F X) → F.M
-- Lean.Exception
Lean.MonadError.toMonadExceptOf : {m : Type → Type} → [self : Lean.MonadError m] → MonadExceptOf Lean.Exception m