mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.not_isOfFinAddOrder_iff_forall_rat_ne_div : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] {p : 𝕜} [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {a : 𝕜},
  ¬IsOfFinAddOrder ↑a ↔ ∀ (q : ℚ), ↑q ≠ a / p
-- Mathlib.Data.Finset.Disjoint
Finset.disjoint_insert_right : ∀ {α : Type u_2} [inst : DecidableEq α] {s t : Finset α} {a : α}, Disjoint s (insert a t) ↔ a ∉ s ∧ Disjoint s t
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.UnfoldLift.modifyGet : ∀ {m : Type u → Type v} {n : Type u → Type u_1} {σ α : Type u} [inst : MonadLift m n] [inst_1 : MonadStateOf σ m]
  (f : σ → α × σ), MonadStateOf.modifyGet f = monadLift (MonadStateOf.modifyGet f)
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.RelabelNat.State.Inv1.empty : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α], Std.Sat.AIG.RelabelNat.State.Inv1 0 ∅
-- Lean.Elab.SyntheticMVars
Lean.Elab.Term.instBEqPostponeBehavior : BEq Lean.Elab.Term.PostponeBehavior
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.op_le_iff : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  {S₁ : Subalgebra R A} {S₂ : Subalgebra R Aᵐᵒᵖ}, S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop
-- Mathlib.Analysis.Complex.Trigonometric
Real.cosh_add_sinh : ∀ (x : ℝ), Real.cosh x + Real.sinh x = Real.exp x
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
/-- The forgetful functor `SheafOfModules.{v} R ⥤ PresheafOfModules R.val`.  -/
SheafOfModules.forget : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (R : CategoryTheory.Sheaf J RingCat) → CategoryTheory.Functor (SheafOfModules R) (PresheafOfModules R.obj)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- Flipping arguments gives a linear equivalence between `G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'`
and `ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')`  -/
ContinuousLinearMap.flipMultilinearEquivₗ : (𝕜 : Type u) →
  {ι : Type v} →
    (E : ι → Type wE) →
      (G : Type wG) →
        (G' : Type wG') →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
              [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] →
                [inst_3 : SeminormedAddCommGroup G] →
                  [inst_4 : NormedSpace 𝕜 G] →
                    [inst_5 : SeminormedAddCommGroup G'] →
                      [inst_6 : NormedSpace 𝕜 G'] →
                        [Fintype ι] →
                          (G →L[𝕜] ContinuousMultilinearMap 𝕜 E G') ≃ₗ[𝕜] ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')
-- Mathlib.Analysis.VonNeumannAlgebra.Basic
VonNeumannAlgebra.mem_carrier : ∀ {H : Type u} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H] [inst_2 : CompleteSpace H]
  {S : VonNeumannAlgebra H} {x : H →L[ℂ] H}, x ∈ S.toStarSubalgebra ↔ x ∈ ↑S
-- Mathlib.Order.Circular
/-- The following lemmas are about the non-instances `LE.toBtw`, `LT.toSBtw` and
`LinearOrder.toCircularOrder`.  -/
btw_iff : ∀ {α : Type u_1} {a b c : α} [inst : LE α], btw a b c ↔ a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.instFintypeElemForallNatBasisSet : {ι : Type u_3} →
  {s : Set (ι → ℕ)} → (hs : IsProperLinearSet s) → [inst : Finite ι] → Fintype ↑(IsProperLinearSet.basisSet✝ hs)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
/-- A simplified version of `TrivSqZeroExt.liftEquiv` for the commutative case.  -/
TrivSqZeroExt.liftEquivOfComm : {R' : Type u} →
  {M : Type v} →
    [inst : CommSemiring R'] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R' M] →
          [inst_3 : Module R'ᵐᵒᵖ M] →
            [inst_4 : IsCentralScalar R' M] →
              {A : Type u_2} →
                [inst_5 : Semiring A] →
                  [inst_6 : Algebra R' A] → { f // ∀ (x y : M), f x * f y = 0 } ≃ (TrivSqZeroExt R' M →ₐ[R'] A)
-- Mathlib.LinearAlgebra.Complex.Module
/-- Linear map version of the imaginary part function, from `ℂ` to `ℝ`.  -/
Complex.imLm : ℂ →ₗ[ℝ] ℝ
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.instInhabited : {L : FirstOrder.Language} → {M : Type w} → [inst : L.Structure M] → Inhabited (L.Embedding M M)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.coe_sub : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Sub α] (s t : Finset α), ↑(s - t) = ↑s - ↑t
-- Mathlib.Algebra.Group.Pointwise.Set.Small
small_add : ∀ {α : Type u_1} (s t : Set α) [inst : Add α] [Small.{u, u_1} ↑s] [Small.{u, u_1} ↑t], Small.{u, u_1} ↑(s + t)
-- Init.Data.List.Nat.Basic
_private.Init.Data.List.Nat.Basic.0.List.dropLast.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (head : α) (h_1 : Unit → motive []) (h_2 : (head : α) → motive [head])
  (h_3 : (a : α) → (as : List α) → motive (a :: as)),
  (match [head] with
    | [] => h_1 ()
    | [head] => h_2 head
    | a :: as => h_3 a as) =
    h_2 head
-- Mathlib.Probability.Distributions.Gamma
/-- The pdf of the gamma distribution integrates to 1  -/
ProbabilityTheory.lintegral_gammaPDF_eq_one : ∀ {a r : ℝ}, 0 < a → 0 < r → ∫⁻ (x : ℝ), ProbabilityTheory.gammaPDF a r x = 1
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Expr.toPoly.match_1.splitter : (motive : Lean.Grind.CommRing.Expr → Sort u_1) →
  (a : Lean.Grind.CommRing.Expr) →
    ((n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n)) →
      ((n : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast n)) →
        ((n : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast n)) →
          ((x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x)) →
            ((x : Lean.Grind.CommRing.Expr) →
                (∀ (n : ℤ), x = Lean.Grind.CommRing.Expr.num n → False) →
                  (∀ (n : ℤ), x = Lean.Grind.CommRing.Expr.intCast n → False) →
                    (∀ (n : ℕ), x = Lean.Grind.CommRing.Expr.natCast n → False) →
                      (∀ (x_4 : Lean.Grind.CommRing.Var), x = Lean.Grind.CommRing.Expr.var x_4 → False) → motive x) →
              motive a
-- Mathlib.GroupTheory.Perm.DomMulAct
DomMulAct.comp_stabilizerEquiv_invFun : ∀ {α : Type u_1} {ι : Type u_2} {f : α → ι} (g : (i : ι) → Equiv.Perm { a // f a = i }) (a : α),
  f (DomMulAct.stabilizerEquiv_invFun g a) = f a
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalExpr.evalNatExpr : Lean.Expr → Lean.MetaM ℕ
-- Init.Data.String.Lemmas.Splits
String.copy_sliceFrom_eq_iff_splits : ∀ {s : String} {p : s.Pos} {t₂ : String}, (s.sliceFrom p).copy = t₂ ↔ p.Splits (s.sliceTo p).copy t₂
-- Mathlib.SetTheory.ZFC.PSet
/-- Universe lift operation  -/
PSet.Lift : PSet.{u} → PSet.{max u v}
-- Mathlib.Combinatorics.SetFamily.Compression.UV
/-- UV-compression is injective on the elements it moves. See `UV.compress`.  -/
sup_sdiff_injOn : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] (u v : α),
  Set.InjOn (fun x => (x ⊔ u) \ v) {x | Disjoint u x ∧ v ≤ x}
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiff_iff_contDiffAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : WithTop ℕ∞}, ContDiff 𝕜 n f ↔ ∀ (x : E), ContDiffAt 𝕜 n f x
-- Mathlib.Logic.Equiv.Prod
Equiv.prodProdProdComm_symm : ∀ (α : Type u_9) (β : Type u_10) (γ : Type u_11) (δ : Type u_12),
  (Equiv.prodProdProdComm α β γ δ).symm = Equiv.prodProdProdComm α γ β δ
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.closure_toSubmonoid : ∀ {G : Type u_2} [inst : Group G] (S : Set G), (Subgroup.closure S).toSubmonoid = Submonoid.closure (S ∪ S⁻¹)
-- Batteries.Data.Char.AsciiCasing
Char.toUpper.eq_1 : ∀ (c : Char),
  c.toUpper = if h : 'a'.val ≤ c.val ∧ c.val ≤ 'z'.val then { val := c.val + ('A'.val - 'a'.val), valid := ⋯ } else c
-- Mathlib.CategoryTheory.Sites.Pretopology
CategoryTheory.Pretopology.instPartialOrder : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] → PartialOrder (CategoryTheory.Pretopology C)
-- Mathlib.RingTheory.Valuation.Extension
Valuation.HasExtension.val_map_eq_one_iff : ∀ {R : Type u_1} {A : Type u_2} {ΓR : Type u_3} {ΓA : Type u_4} [inst : CommRing R] [inst_1 : Ring A]
  [inst_2 : LinearOrderedCommMonoidWithZero ΓR] [inst_3 : LinearOrderedCommMonoidWithZero ΓA] [inst_4 : Algebra R A]
  (vR : Valuation R ΓR) (vA : Valuation A ΓA) [vR.HasExtension vA] (x : R), vA ((algebraMap R A) x) = 1 ↔ vR x = 1
-- Mathlib.Order.SuccPred.Basic
Order.gc_pred_succ : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [inst_2 : PredOrder α],
  GaloisConnection Order.pred Order.succ
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringRight_obj_obj : ∀ (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] (H : CategoryTheory.Functor D E)
  (F : CategoryTheory.Functor C D), ((CategoryTheory.Functor.whiskeringRight C D E).obj H).obj F = F.comp H
-- Mathlib.Algebra.Order.Ring.Cone
/-- Construct a cone from the set of non-negative elements of a partially ordered ring.  -/
RingCone.nonneg : (T : Type u_1) → [inst : Ring T] → [inst_1 : PartialOrder T] → [IsOrderedRing T] → RingCone T
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Measurable.ennreal_tsum : ∀ {α : Type u_1} {mα : MeasurableSpace α} {ι : Type u_5} [Countable ι] {f : ι → α → ENNReal},
  (∀ (i : ι), Measurable (f i)) → Measurable fun x => ∑' (i : ι), f i x
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnriched.hComp_id_heq : ∀ {C : Type u_1} [inst : CategoryTheory.EnrichedCategory CategoryTheory.Cat C] {a b : CategoryTheory.CatEnriched C}
  {f f' : a ⟶ b} (η : f ⟶ f'),
  CategoryTheory.CatEnriched.hComp η (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id b)) ≍ η
-- Init.Data.Repr
instReprUInt32 : Repr UInt32
-- Mathlib.LinearAlgebra.Semisimple
/-- A characterisation of `Module.End.IsFinitelySemisimple` using only the lattice of submodules of
`M` (thus avoiding submodules of submodules).  -/
Module.End.isFinitelySemisimple_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {f : Module.End R M},
  f.IsFinitelySemisimple ↔
    ∀ p ∈ f.invtSubmodule,
      Module.Finite R ↥p → ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ Disjoint q r ∧ q ⊔ r = p
-- Mathlib.RingTheory.AdjoinRoot
PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (pb : PowerBasis R S)
  (I : Ideal R) (a : Polynomial (R ⧸ I) ⧸ Ideal.span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}),
  (pb.quotientEquivQuotientMinpolyMap I).symm a =
    (Ideal.quotientMap (Ideal.map (algebraMap R S) I)
        ↑{ toEquiv := ↑(AdjoinRoot.equiv' (minpoly R pb.gen) pb ⋯ ⋯), map_mul' := ⋯, map_add' := ⋯ } ⋯)
      ((AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot I (minpoly R pb.gen)).symm a)
-- Mathlib.Topology.Sheaves.Stalks
/-- For presheaves valued in a concrete category whose forgetful functor preserves filtered colimits,
every element of the stalk is the germ of a section.
 -/
TopCat.Presheaf.exists_germ_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {FC : C → C → Type u_1} {CC : C → Type v} [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
  [instCC : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] (F : TopCat.Presheaf C X) {x : ↑X}
  (t : CategoryTheory.ToType (F.stalk x)),
  ∃ U, ∃ (m : x ∈ U), ∃ s, (CategoryTheory.ConcreteCategory.hom (F.germ U x m)) s = t
-- Mathlib.LinearAlgebra.Span.Basic
LinearEquiv.toSpanNonzeroSingleton_one : ∀ (R : Type u_1) (M : Type u_4) [inst : Ring R] [inst_1 : IsDomain R] [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [inst_4 : Module.IsTorsionFree R M] (x : M) (h : x ≠ 0), (LinearEquiv.toSpanNonzeroSingleton R M x h) 1 = ⟨x, ⋯⟩
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.InvariantCardinalRank.mk : ∀ {α : Type u} {M : Matroid α},
  (∀ ⦃I J X : Set α⦄, M.IsBasis I X → M.IsBasis J X → Cardinal.mk ↑(I \ J) = Cardinal.mk ↑(J \ I)) →
    M.InvariantCardinalRank
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.unopId_hom_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C),
  (CategoryTheory.Functor.unopId C).hom.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.LinearAlgebra.Matrix.Invertible
/-- A copy oy of `mul_invOf_eq_iff_eq_mul_right` for rectangular matrices.  -/
Matrix.mul_invOf_eq_iff_eq_mul_right : ∀ {m : Type u_1} {n : Type u_2} {α : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring α]
  {A B : Matrix m n α} {C : Matrix n n α} [inst_3 : Invertible C], A * ⅟C = B ↔ A = B * C
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.ofVal_inv : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : DivisionRing R]
  (v : Valuation R Γ₀) (x : WithVal v), x⁻¹.ofVal = x.ofVal⁻¹
-- Mathlib.Data.PFunctor.Multivariate.M
MvPFunctor.M.dest_map : ∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α β : TypeVec.{u} n} (g : α.Arrow β) (x : P.M α),
  MvPFunctor.M.dest P (MvFunctor.map g x) = MvFunctor.map (g ::: fun x => MvFunctor.map g x) (MvPFunctor.M.dest P x)
-- Mathlib.Algebra.Module.GradedModule
SetLike.gmulAction : {ιA : Type u_1} →
  {ιM : Type u_2} →
    {A : Type u_4} →
      {M : Type u_5} →
        {σ : Type u_6} →
          {σ' : Type u_7} →
            [inst : AddMonoid ιA] →
              [inst_1 : AddAction ιA ιM] →
                [inst_2 : Semiring A] →
                  (𝓐 : ιA → σ') →
                    [inst_3 : SetLike σ' A] →
                      (𝓜 : ιM → σ) →
                        [inst_4 : AddMonoid M] →
                          [inst_5 : DistribMulAction A M] →
                            [inst_6 : SetLike σ M] →
                              [inst_7 : SetLike.GradedMonoid 𝓐] →
                                [SetLike.GradedSMul 𝓐 𝓜] → GradedMonoid.GMulAction (fun i => ↥(𝓐 i)) fun i => ↥(𝓜 i)
-- Lean.Widget.UserWidget
Lean.Widget.evalPanelWidgets : Lean.MetaM (Array Lean.Widget.WidgetInstance)
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- If `f,g` is reflexive, then `g,f` is reflexive.  -/
CategoryTheory.IsReflexivePair.swap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} {f g : A ⟶ B} [CategoryTheory.IsReflexivePair f g],
  CategoryTheory.IsReflexivePair g f
-- Init.Data.Nat.Div.Lemmas
Nat.mod_mod_eq_mod_of_lt_right : ∀ {a b c : ℕ}, a < c → a % b % c = a % b
-- Mathlib.SetTheory.Cardinal.Basic
/-- A set of cardinals is bounded above iff it's small, i.e. it corresponds to a usual ZFC set.  -/
Cardinal.bddAbove_iff_small : ∀ {s : Set Cardinal.{u}}, BddAbove s ↔ Small.{u, u + 1} ↑s
-- Init.Data.Nat.Basic
Nat.mul_lt_mul_of_pos_right : ∀ {n m k : ℕ}, n < m → k > 0 → n * k < m * k
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_zero_singleton : ∀ (R : Type u_1) {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M], R ∙ 0 = ⊥
-- Mathlib.Geometry.Euclidean.MongePoint
/-- The Monge point of an (n+2)-simplex, minus the centroid of an
n-dimensional face, is orthogonal to the difference of the two
vertices not in that face.  -/
Affine.Simplex.inner_mongePoint_vsub_face_centroid_vsub : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 2)) {i₁ i₂ : Fin (n + 3)},
  inner ℝ (s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points) (s.points i₁ -ᵥ s.points i₂) = 0
-- Mathlib.AlgebraicGeometry.Sites.MorphismProperty
AlgebraicGeometry.Scheme.instIsStableUnderCompositionPrecoverageOfIsStableUnderComposition : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [P.IsStableUnderComposition],
  (AlgebraicGeometry.Scheme.precoverage P).IsStableUnderComposition
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
/-- The functor `FibrantObject C ⥤ HoCat C`, considered as a localizer morphism.  -/
HomotopicalAlgebra.FibrantObject.toHoCatLocalizerMorphism : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      CategoryTheory.LocalizerMorphism (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.FibrantObject C))
        (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.FibrantObject.HoCat C))
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
IsIntegralClosure.of_isIntegrallyClosedIn : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {B : Type u_3}
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [IsScalarTower R A B] [IsIntegrallyClosedIn A B]
  [Algebra.IsIntegral R A], IsIntegralClosure A R B
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isRat_sub : ∀ {α : Type u_1} [inst : Ring α] {f : α → α → α} {a b : α} {na nb nc : ℤ} {da db dc k : ℕ},
  f = HSub.hSub →
    Mathlib.Meta.NormNum.IsRat a na da →
      Mathlib.Meta.NormNum.IsRat b nb db →
        (na.mul ↑db).sub (nb.mul ↑da) = (↑k).mul nc → da.mul db = k.mul dc → Mathlib.Meta.NormNum.IsRat (f a b) nc dc
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.opEquiv.match_3.eq_1 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (x y : (CategoryTheory.WithTerminal C)ᵒᵖ) → (Opposite.unop y ⟶ Opposite.unop x) → (x ⟶ y) → Sort u_3)
  (x y : C)
  (f :
    Opposite.unop (Opposite.op (CategoryTheory.WithTerminal.of y)) ⟶
      Opposite.unop (Opposite.op (CategoryTheory.WithTerminal.of x)))
  (x_1 : Opposite.op (CategoryTheory.WithTerminal.of x) ⟶ Opposite.op (CategoryTheory.WithTerminal.of y))
  (h_1 :
    (x y : C) →
      (f :
          Opposite.unop (Opposite.op (CategoryTheory.WithTerminal.of y)) ⟶
            Opposite.unop (Opposite.op (CategoryTheory.WithTerminal.of x))) →
        (x_2 : Opposite.op (CategoryTheory.WithTerminal.of x) ⟶ Opposite.op (CategoryTheory.WithTerminal.of y)) →
          motive (Opposite.op (CategoryTheory.WithTerminal.of x)) (Opposite.op (CategoryTheory.WithTerminal.of y)) f
            x_2)
  (h_2 :
    (a : C) →
      (x :
          Opposite.unop (Opposite.op (CategoryTheory.WithTerminal.of a)) ⟶
            Opposite.unop (Opposite.op CategoryTheory.WithTerminal.star)) →
        (x_2 : Opposite.op CategoryTheory.WithTerminal.star ⟶ Opposite.op (CategoryTheory.WithTerminal.of a)) →
          motive (Opposite.op CategoryTheory.WithTerminal.star) (Opposite.op (CategoryTheory.WithTerminal.of a)) x x_2)
  (h_3 :
    (x :
        Opposite.unop (Opposite.op CategoryTheory.WithTerminal.star) ⟶
          Opposite.unop (Opposite.op CategoryTheory.WithTerminal.star)) →
      (x_2 : Opposite.op CategoryTheory.WithTerminal.star ⟶ Opposite.op CategoryTheory.WithTerminal.star) →
        motive (Opposite.op CategoryTheory.WithTerminal.star) (Opposite.op CategoryTheory.WithTerminal.star) x x_2),
  (match Opposite.op (CategoryTheory.WithTerminal.of x), Opposite.op (CategoryTheory.WithTerminal.of y), f, x_1 with
    | Opposite.op (CategoryTheory.WithTerminal.of x), Opposite.op (CategoryTheory.WithTerminal.of y), f, x_2 =>
      h_1 x y f x_2
    | Opposite.op CategoryTheory.WithTerminal.star, Opposite.op (CategoryTheory.WithTerminal.of a), x, x_2 =>
      h_2 a x x_2
    | Opposite.op CategoryTheory.WithTerminal.star, Opposite.op CategoryTheory.WithTerminal.star, x, x_2 => h_3 x x_2) =
    h_1 x y f x_1
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
groupHomology.map_chainsFunctor_shortExact : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)},
  X.ShortExact → (X.map (groupHomology.chainsFunctor k G)).ShortExact
-- Mathlib.Data.Part
Part.inter_mem_inter : ∀ {α : Type u_1} [inst : Inter α] (a b : Part α) (ma mb : α), ma ∈ a → mb ∈ b → ma ∩ mb ∈ a ∩ b
-- Init.Data.Char.Basic
/-- Converts a character into a `UInt8` that contains its code point.

If the code point is larger than 255, it is truncated (reduced modulo 256).
 -/
Char.toUInt8 : Char → UInt8
-- Mathlib.AlgebraicGeometry.QuasiAffine
/-- A scheme `X` is quasi-affine if it is quasi-compact and `X ⟶ Spec Γ(X, ⊤)` is an immersion.
This actually implies that `X ⟶ Spec Γ(X, ⊤)` is an open immersion.  -/
AlgebraicGeometry.Scheme.IsQuasiAffine : AlgebraicGeometry.Scheme → Prop
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.coeff_subst_single : ∀ {R : Type u_2} [inst : CommRing R] {σ : Type u_7} [inst_1 : DecidableEq σ] (s : σ) (f : PowerSeries R) (e : σ →₀ ℕ),
  (MvPowerSeries.coeff e) (PowerSeries.subst (MvPowerSeries.X s) f) =
    if e = fun₀ | s => e s then (PowerSeries.coeff (e s)) f else 0
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.recOn.eq_1 : ∀ {α : Type u_1} {motive : FreeAddMonoid α → Sort u_6} (xs : FreeAddMonoid α) (one : motive 0)
  (of_mul : (x : α) → (xs : FreeAddMonoid α) → motive xs → motive (FreeAddMonoid.of x + xs)),
  FreeAddMonoid.recOn xs one of_mul = List.rec one of_mul xs
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
/-- Semilinear sets are closed under intersection.  -/
IsSemilinearSet.inter : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s₁ s₂ : Set M},
  IsSemilinearSet s₁ → IsSemilinearSet s₂ → IsSemilinearSet (s₁ ∩ s₂)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Sentence.realize_not : ∀ {L : FirstOrder.Language} (M : Type w) [inst : L.Structure M] {φ : L.Sentence},
  M ⊨ FirstOrder.Language.Formula.not φ ↔ ¬M ⊨ φ
-- Mathlib.Analysis.Convex.AmpleSet
/-- A whole vector space is ample.  -/
ampleSet_univ : ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F], AmpleSet Set.univ
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- If `𝔖` covers `α`, then the topology of `𝔖`-convergence is T₂.  -/
UniformOnFun.t2Space_of_covering : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] {𝔖 : Set (Set α)} [T2Space β],
  ⋃₀ 𝔖 = Set.univ → T2Space (UniformOnFun α β 𝔖)
-- Mathlib.Analysis.Rat.NatSqrt.Real
Nat.ratSqrt_mem_Ioc : ∀ (x : ℕ) {prec : ℕ}, 0 < prec → ↑(x.ratSqrt prec) ∈ Set.Ioc (√↑x - 1 / ↑prec) √↑x
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.keyAtIdx!.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Inhabited α] (x : Std.DTreeMap.Internal.Impl α β) (x_1 : ℕ),
  x.keyAtIdx! x_1 =
    match x, x_1 with
    | Std.DTreeMap.Internal.Impl.leaf, x =>
      panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.keyAtIdx!" 503 16
        "Out-of-bounds access"
    | Std.DTreeMap.Internal.Impl.inner size k v l r, n =>
      match compare n l.size with
      | Ordering.lt => l.keyAtIdx! n
      | Ordering.eq => k
      | Ordering.gt => r.keyAtIdx! (n - l.size - 1)
-- Mathlib.Order.CompleteLattice.Basic
iInf_le_of_le : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {f : ι → α} {a : α} (i : ι), f i ≤ a → iInf f ≤ a
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheorem.proof : Lean.Meta.SimpTheorem → Lean.Expr
-- Mathlib.Analysis.Normed.Operator.Banach
/-- Upgrade a `LinearMap` to a `ContinuousLinearMap` using the **closed graph theorem**.  -/
ContinuousLinearMap.ofIsClosedGraph : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_3} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          [CompleteSpace E] →
            {F : Type u_5} →
              [inst_4 : NormedAddCommGroup F] →
                [inst_5 : NormedSpace 𝕜 F] → [CompleteSpace F] → {g : E →ₗ[𝕜] F} → IsClosed ↑g.graph → E →L[𝕜] F
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.ofHoms_v : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (ψ : (p : ℤ) → F.X p ⟶ G.X p) (p : ℤ),
  (CochainComplex.HomComplex.Cochain.ofHoms ψ).v p p ⋯ = ψ p
-- Lean.Meta.Eqns
Lean.Meta.instInhabitedEqnsExtState : Inhabited Lean.Meta.EqnsExtState