mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- Use the fact that `(F ⊛ G).obj c` is a colimit to characterize morphisms out of it at a
point.  -/
CategoryTheory.MonoidalCategory.DayConvolution.convolution_hom_ext_at : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (F G : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolution F G] (c : C) {v : V}
  {f g : (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G).obj c ⟶ v},
  (∀ {x y : C} (u : CategoryTheory.MonoidalCategoryStruct.tensorObj x y ⟶ c),
      CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (x, y))
          (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.convolution F G).map u)
            f) =
        CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (x, y))
          (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.convolution F G).map u)
            g)) →
    f = g
-- Std.Data.DTreeMap.Internal.Operations
/-- Returns the tree `l ++ ⟨k, v⟩ ++ r`, with the largest element chopped off.  -/
Std.DTreeMap.Internal.Impl.maxView : {α : Type u} →
  {β : α → Type v} →
    (k : α) →
      β k →
        (l r : Std.DTreeMap.Internal.Impl α β) →
          l.Balanced →
            r.Balanced →
              Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size →
                Std.DTreeMap.Internal.Impl.View α β (l.size + r.size)
-- Mathlib.Algebra.Ring.Parity
range_two_mul : ∀ (α : Type u_4) [inst : NonAssocSemiring α], (Set.range fun x => 2 * x) = {a | Even a}
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.IsFinitePresentation.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R},
  (∃ σ, σ.IsFinitePresentation) → M.IsFinitePresentation
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
RootPairing.GeckConstruction.basis.congr_simp : ∀ {ι : Type u_1} {K : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : DecidableEq ι]
  [inst_2 : Field K] [inst_3 : CharZero K] [inst_4 : AddCommGroup M] [inst_5 : Module K M] [inst_6 : AddCommGroup N]
  [inst_7 : Module K N] {P : RootPairing ι K M N} [inst_8 : P.IsReduced] [inst_9 : P.IsCrystallographic]
  [inst_10 : P.IsIrreducible] [inst_11 : P.IsRootSystem] (b : P.Base),
  RootPairing.GeckConstruction.basis b = RootPairing.GeckConstruction.basis b
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- Constructor for `Equivalence.CommShift`.  -/
CategoryTheory.Equivalence.CommShift.mk' : ∀ {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] (E : C ≌ D) (A : Type u_3) [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : E.functor.CommShift A]
  [inst_6 : E.inverse.CommShift A], CategoryTheory.NatTrans.CommShift E.unitIso.hom A → E.CommShift A
-- Mathlib.Geometry.Manifold.VectorBundle.Hom
/-- Consider a `C^n` map `v : M → E₁` to a vector bundle, over a base map `b : M → B`, and
linear maps `ϕ m : E₁ (b m) → E₂ (b m)` depending smoothly on `m`.
One can apply `ϕ m` to `v m`, and the resulting map is `C^n`.  -/
ContMDiff.clm_bundle_apply : ∀ {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {M : Type u_6} [inst : NontriviallyNormedField 𝕜]
  {n : WithTop ℕ∞} {E₁ : B → Type u_7} [inst_1 : (x : B) → AddCommGroup (E₁ x)] [inst_2 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁] [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
  [inst_6 : (x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_8} [inst_7 : (x : B) → AddCommGroup (E₂ x)]
  [inst_8 : (x : B) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂] [inst_10 : NormedSpace 𝕜 F₂]
  [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [inst_12 : (x : B) → TopologicalSpace (E₂ x)] {EB : Type u_10}
  [inst_13 : NormedAddCommGroup EB] [inst_14 : NormedSpace 𝕜 EB] {HB : Type u_11} [inst_15 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_16 : TopologicalSpace B] [inst_17 : ChartedSpace HB B] {EM : Type u_12}
  [inst_18 : NormedAddCommGroup EM] [inst_19 : NormedSpace 𝕜 EM] {HM : Type u_13} [inst_20 : TopologicalSpace HM]
  {IM : ModelWithCorners 𝕜 EM HM} [inst_21 : TopologicalSpace M] [inst_22 : ChartedSpace HM M]
  [inst_23 : FiberBundle F₁ E₁] [inst_24 : VectorBundle 𝕜 F₁ E₁] [inst_25 : FiberBundle F₂ E₂]
  [inst_26 : VectorBundle 𝕜 F₂ E₂] {b : M → B} {v : (x : M) → E₁ (b x)}
  [inst_27 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)] [inst_28 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
  {ϕ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x)},
  (ContMDiff IM (IB.prod (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂))) n fun m => ⟨b m, ϕ m⟩) →
    (ContMDiff IM (IB.prod (modelWithCornersSelf 𝕜 F₁)) n fun m => ⟨b m, v m⟩) →
      ContMDiff IM (IB.prod (modelWithCornersSelf 𝕜 F₂)) n fun m => ⟨b m, ⋯⟩
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.coe_liftAlgHom : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra S R] [inst_4 : Algebra S T] (p : Polynomial R) (i : R →ₐ[S] T) (x : T)
  (h : Polynomial.eval₂ (↑i) x p = 0), ⇑(AdjoinRoot.liftAlgHom p i x h) = ⇑(AdjoinRoot.lift i.toRingHom x h)
-- Mathlib.RingTheory.KrullDimension.Zero
instIsJacobsonRingOfKrullDimLEOfNatNat : ∀ {R : Type u_1} [inst : CommRing R] [Ring.KrullDimLE 0 R], IsJacobsonRing R
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.simpGoal : Lean.MVarId →
  Lean.Meta.Simp.Context →
    optParam Lean.Meta.Simp.SimprocsArray #[] →
      optParam (Option Lean.Meta.Simp.Discharge) none →
        optParam Bool true →
          optParam (Array Lean.FVarId) #[] →
            optParam Lean.Meta.Simp.Stats { } →
              Lean.MetaM (Option (Array Lean.FVarId × Lean.MVarId) × Lean.Meta.Simp.Stats)
-- Lean.EnvExtension
Lean.instInhabitedMapDeclarationExtension : {a : Type} → Inhabited (Lean.MapDeclarationExtension a)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.forInUncurried_eq_forIn_toList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {δ : Type w} {m' : Type w → Type w'} {β : Type v}
  {m : Std.DHashMap.Raw α fun x => β} [inst_2 : Monad m'] [LawfulMonad m'],
  m.WF →
    ∀ {f : α × β → δ → m' (ForInStep δ)} {init : δ},
      Std.DHashMap.Raw.Const.forInUncurried f init m = forIn (Std.DHashMap.Raw.Const.toList m) init f
-- Lean.Elab.Tactic.Grind.Basic
/-- Runs `tactic` with only the first unsolved goal as the goal, and expects it leave no goals.
Fails if there are no goal to be solved.
 -/
Lean.Elab.Tactic.Grind.focusAndDone : {α : Type} → Lean.Elab.Tactic.Grind.GrindTacticM α → Lean.Elab.Tactic.Grind.GrindTacticM α
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.IsDetecting.of_le : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.ObjectProperty C},
  P.IsDetecting → ∀ {Q : CategoryTheory.ObjectProperty C}, P ≤ Q → Q.IsDetecting
-- Mathlib.Analysis.InnerProductSpace.PiL2
Matrix.piLp_ofLp_toEuclideanLin : ∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {m : Type u_7} {n : Type u_8} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (A : Matrix m n 𝕜) (x : EuclideanSpace 𝕜 n), ((Matrix.toEuclideanLin A) x).ofLp = (Matrix.toLin' A) x.ofLp
-- Mathlib.Analysis.Fourier.Notation
FourierInvAdd.mk : ∀ {E : Type u_5} {F : outParam (Type u_6)} [inst : Add E] [inst_1 : Add F] [inst_2 : FourierTransformInv E F],
  (∀ (f g : E),
      FourierTransformInv.fourierInv (f + g) = FourierTransformInv.fourierInv f + FourierTransformInv.fourierInv g) →
    FourierInvAdd E F
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.any_eq_true_iff_exists_mem : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α] {p : α → Bool},
  m.WF → (m.any p = true ↔ ∃ a ∈ m, p a = true)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.refl_counitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.Equivalence.refl.counitIso =
    CategoryTheory.Iso.refl ((CategoryTheory.Functor.id C).comp (CategoryTheory.Functor.id C))
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.bijOn_sin : Set.BijOn Real.sin (Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) (Set.Icc (-1) 1)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
/-- The functor taking a morphism into `Y` to its kernel as an ideal sheaf on `Y`.  -/
AlgebraicGeometry.Scheme.kerFunctor : (Y : AlgebraicGeometry.Scheme) → CategoryTheory.Functor (CategoryTheory.Over Y)ᵒᵖ Y.IdealSheafData
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_mul_antidiag : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Mul M] (x y : MonoidAlgebra R M) (m : M)
  (s : Finset (M × M)), (∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m) → (x * y).coeff m = ∑ p ∈ s, x.coeff p.1 * y.coeff p.2
-- Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
WithIdeal.isTopologicallyNilpotent_of_mem : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : WithIdeal R] {a : R}, a ∈ WithIdeal.i → IsTopologicallyNilpotent a
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
_private.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.0.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.collectTrivialBottomUps : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeAppM Unit
-- Mathlib.Algebra.Group.Defs
add_left_cancel : ∀ {G : Type u_1} [inst : Add G] [IsLeftCancelAdd G] {a b c : G}, a + b = a + c → b = c
-- Mathlib.NumberTheory.NumberField.CMField
/-- The fundamental system of units of `K⁺` as a family of `(𝓞 K)ˣ`.
 -/
NumberField.IsCMField.realFundSystem : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : CharZero K] →
      [NumberField.IsCMField K] →
        [inst_3 : NumberField K] → Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
/-- The linear equivalence between sesquilinear maps and `n × m` matrices  -/
LinearMap.toMatrixₛₗ₂' : (R : Type u_1) →
  {R₁ : Type u_2} →
    {S₁ : Type u_3} →
      {R₂ : Type u_4} →
        {S₂ : Type u_5} →
          {N₂ : Type u_10} →
            {n : Type u_11} →
              {m : Type u_12} →
                [inst : CommSemiring R] →
                  [inst_1 : AddCommMonoid N₂] →
                    [inst_2 : Module R N₂] →
                      [inst_3 : Semiring R₁] →
                        [inst_4 : Semiring R₂] →
                          [inst_5 : Semiring S₁] →
                            [inst_6 : Semiring S₂] →
                              [inst_7 : Module S₁ N₂] →
                                [inst_8 : Module S₂ N₂] →
                                  [inst_9 : SMulCommClass S₁ R N₂] →
                                    [inst_10 : SMulCommClass S₂ R N₂] →
                                      [inst_11 : SMulCommClass S₂ S₁ N₂] →
                                        {σ₁ : R₁ →+* S₁} →
                                          {σ₂ : R₂ →+* S₂} →
                                            [Fintype n] →
                                              [Fintype m] →
                                                [DecidableEq n] →
                                                  [DecidableEq m] →
                                                    ((n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂) ≃ₗ[R] Matrix n m N₂
-- Init.ShareCommon
withShareCommon : {m : Type u_1 → Type u_2} → [self : MonadShareCommon m] → {α : Type u_1} → α → m α
-- Mathlib.SetTheory.Cardinal.Free
instCountableFreeAddMonoid : ∀ (α : Type u) [Countable α], Countable (FreeAddMonoid α)
-- Mathlib.CategoryTheory.Limits.Preorder
/-- A preorder with an initial object has a least element.  -/
Preorder.orderBotOfHasInitial : {C : Type u} → [inst : Preorder C] → [CategoryTheory.Limits.HasInitial C] → OrderBot C
-- Mathlib.NumberTheory.Chebyshev
/-- Extension for the `positivity` tactic: the first Chebyshev function is nonnegative.  -/
Mathlib.Meta.Positivity.evalTheta : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.MeasureTheory.Covering.Vitali
/-- Vitali covering theorem, open balls version: given a family `t` of balls, one can
extract a disjoint subfamily `u ⊆ t` so that all balls in `t` are covered by the τ-times
dilations of balls in `u`, for some `τ > 3`.  -/
Vitali.exists_disjoint_subfamily_covering_enlargement_ball : ∀ {α : Type u_1} {ι : Type u_2} [inst : PseudoMetricSpace α] (t : Set ι) (x : ι → α) (r : ι → ℝ) (R : ℝ),
  (∀ a ∈ t, r a ≤ R) →
    ∀ (τ : ℝ),
      3 < τ →
        ∃ u ⊆ t,
          (u.PairwiseDisjoint fun a => Metric.ball (x a) (r a)) ∧
            ∀ a ∈ t, ∃ b ∈ u, Metric.ball (x a) (r a) ⊆ Metric.ball (x b) (τ * r b)
-- Mathlib.Order.WithBot
WithBot.le_unbotD : ∀ {α : Type u_1} [inst : PartialOrder α] {y : WithBot α} {a b : α}, ↑b ≤ y → b ≤ WithBot.unbotD a y
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
fixingAddSubgroup_iUnion : ∀ (M : Type u_1) (α : Type u_2) [inst : AddGroup M] [inst_1 : AddAction M α] {ι : Sort u_3} {s : ι → Set α},
  fixingAddSubgroup M (⋃ i, s i) = ⨅ i, fixingAddSubgroup M (s i)
-- Mathlib.MeasureTheory.Measure.Support
MeasureTheory.Measure.isClosed_support : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X},
  IsClosed μ.support
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.IsHaarMeasure.smul : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : TopologicalSpace G]
  (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] {c : ENNReal}, c ≠ 0 → c ≠ ⊤ → (c • μ).IsHaarMeasure
-- Mathlib.Geometry.Manifold.IntegralCurve.Transform
IsMIntegralCurve.comp_add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {γ : ℝ → M}
  {v : (x : M) → TangentSpace I x}, IsMIntegralCurve γ v → ∀ (dt : ℝ), IsMIntegralCurve (γ ∘ fun x => x + dt) v
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- The `n`-dimensional generalized loops based at `x` in a space `X` are
continuous functions `I^n → X` that sends the boundary to `x`.
We allow an arbitrary indexing type `N` in place of `Fin n` here.  -/
Topology.Homotopy.«termΩ^» : Lean.ParserDescr
-- Mathlib.Algebra.CharP.Invertible
invertibleTwo : {K : Type u_2} → [inst : DivisionSemiring K] → [CharZero K] → Invertible 2
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- If two affine subspaces have a point in their inf, the direction of their inf equals the inf of
their directions.  -/
AffineSubspace.direction_inf_of_mem_inf : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {s₁ s₂ : AffineSubspace k P} {p : P},
  p ∈ s₁ ⊓ s₂ → (s₁ ⊓ s₂).direction = s₁.direction ⊓ s₂.direction
-- Mathlib.GroupTheory.SpecificGroups.Alternating
alternatingGroup.map_ofSubtype : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (s : Finset α),
  Subgroup.map Equiv.Perm.ofSubtype (alternatingGroup ↥s) = Equiv.Perm.ofSubtype.range ⊓ alternatingGroup α
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.extend_apply_of_one_le : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  (F : f₀.Homotopy f₁) {t : ℝ}, 1 ≤ t → ∀ (x : X), (F.extend t) x = f₁ x
-- Mathlib.Combinatorics.Graph.Basic
Graph.IsLoopAt.edge_mem : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β}, G.IsLoopAt e x → e ∈ G.edgeSet
-- Mathlib.RingTheory.PowerSeries.PiTopology
PowerSeries.WithPiTopology.summable_iff_summable_coeff : ∀ (R : Type u_1) [inst : TopologicalSpace R] [inst_1 : Semiring R] {ι : Type u_2} {f : ι → PowerSeries R},
  Summable f ↔ ∀ (d : ℕ), Summable fun i => (PowerSeries.coeff d) (f i)
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithInitial.coconeBack_map_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Under X)}
  {t₁ t₂ : CategoryTheory.Limits.Cocone (CategoryTheory.WithInitial.liftFromUnder.obj K)} {f : t₁ ⟶ t₂},
  (CategoryTheory.WithInitial.coconeBack✝.map f).hom = CategoryTheory.Under.homMk f.hom ⋯
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the largest key that is less than or equal to the
given key, returning `fallback` if no such key exists.
 -/
Std.ExtTreeMap.getKeyLED : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → α → α
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- Two `AddSubsemigroup`s are equal if they have the same elements.  -/
AddSubsemigroup.ext : ∀ {M : Type u_1} [inst : Add M] {S T : AddSubsemigroup M}, (∀ (x : M), x ∈ S ↔ x ∈ T) → S = T
-- Mathlib.RingTheory.Extension.Cotangent.Basis
/-- The cotangent space of the constructed presentation is isomorphic
to `(g X - 1)/(g X - 1)² × S ⊗[T] J/J²`.  -/
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.cotangentEquivProd : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {ι : Type u_4} →
            {P : Algebra.Generators R S ι} →
              {σ : Type u_5} →
                {b : Module.Basis σ S P.toExtension.Cotangent} →
                  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b) →
                    [Nontrivial S] →
                      (Algebra.Generators.PresentationOfFreeCotangent.Aux.pres✝ D).toExtension.Cotangent ≃ₗ[S]
                        (Algebra.Generators.PresentationOfFreeCotangent.Aux.presRight✝ D).toExtension.Cotangent ×
                          TensorProduct (Algebra.Generators.PresentationOfFreeCotangent.Aux.T✝ D) S
                            (Algebra.Generators.PresentationOfFreeCotangent.Aux.presLeft✝ D).toExtension.Cotangent
-- Mathlib.Data.Rat.Cast.CharZero
Rat.cast_inv : ∀ {α : Type u_3} [inst : DivisionRing α] [CharZero α] (p : ℚ), ↑p⁻¹ = (↑p)⁻¹
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arctan`.  -/
EuclideanGeometry.oangle_left_eq_arctan_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P},
  EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) →
    EuclideanGeometry.oangle p₃ p₁ p₂ = ↑(Real.arctan (dist p₃ p₂ / dist p₁ p₂))
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.val_sub_ne_zero : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  {x : M}, x ∉ (↑f).domain → ∀ (y : ↥(↑f).domain), ↑y - x ≠ 0
-- Lean.Elab.ConfigEval.MetaInstances
Lean.Elab.ConfigEval.instEvalTermTransparencyMode : Lean.Elab.ConfigEval.EvalTerm Lean.Meta.TransparencyMode
-- Init.Data.Nat.MinMax
Nat.max_zero : ∀ (a : ℕ), max a 0 = a
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineSubspace.isometryEquivMap.apply_symm_apply : ∀ {𝕜 : Type u_1} {V₁' : Type u_4} {V₂ : Type u_5} {P₁' : Type u_9} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V₁'] [inst_2 : NormedSpace 𝕜 V₁'] [inst_3 : MetricSpace P₁']
  [inst_4 : NormedAddTorsor V₁' P₁'] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] {E : AffineSubspace 𝕜 P₁'} [inst_9 : Nonempty ↥E]
  {φ : P₁' →ᵃⁱ[𝕜] P₂} (x : ↥(AffineSubspace.map φ.toAffineMap E)),
  φ ↑((AffineSubspace.isometryEquivMap φ E).symm x) = ↑x
-- Mathlib.Computability.Primrec.Basic
Primrec.pair : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable γ]
  {f : α → β} {g : α → γ}, Primrec f → Primrec g → Primrec fun a => (f a, g a)
-- Aesop.Script.GoalWithMVars
Aesop.instInhabitedGoalWithMVars : Inhabited Aesop.GoalWithMVars
-- Mathlib.RingTheory.Ideal.Nonunits
Submonoid.isUnit_iff : ∀ {α : Type u_2} {C : Type u_4} [inst : SetLike C α] [inst_1 : Group α] [inst_2 : SubmonoidClass C α] {S : C} {a : ↥S},
  IsUnit a ↔ (↑a)⁻¹ ∈ S
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.PlacedTile.coeSet.eq_1 : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [inst : Group G] [inst_1 : MulAction G X]
  {ps : DiscreteTiling.Protoset G X ιₚ} (pt : DiscreteTiling.PlacedTile ps),
  ↑pt = Quotient.liftOn' pt.groupElts (fun g => g • ↑(↑ps pt.index)) ⋯
-- Mathlib.NumberTheory.NumberField.FractionalIdeal
NumberField.fractionalIdeal_rank : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ),
  Module.finrank ℤ ↥↑↑I = Module.finrank ℤ (NumberField.RingOfIntegers K)
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
of the real line. If `f` is differentiable on the interior of `D` and `f'` is negative, then
`f` is a strictly antitone function on `D`.  -/
strictAntiOn_of_deriv_neg : ∀ {D : Set ℝ}, Convex ℝ D → ∀ {f : ℝ → ℝ}, ContinuousOn f D → (∀ x ∈ interior D, deriv f x < 0) → StrictAntiOn f D
-- Mathlib.Analysis.Convex.Between
affineSegment_vsub_const_image : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (x y p : P),
  (fun x => x -ᵥ p) '' affineSegment R x y = affineSegment R (x -ᵥ p) (y -ᵥ p)
-- Mathlib.Algebra.BrauerGroup.Defs
IsBrauerEquivalent.refl : ∀ {K : Type u} [inst : Field K] (A : CSA K), IsBrauerEquivalent A A
-- Mathlib.Algebra.Order.GroupWithZero.Basic
mul_neg_of_neg_of_pos : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b : α} [inst_1 : Preorder α] [MulPosStrictMono α], a < 0 → 0 < b → a * b < 0
-- Init.System.IO
/-- Configuration for the standard input, output, and error handles of a child process.
 -/
IO.Process.StdioConfig : Type
-- Std.Time.Format.Modifier
Std.Time.Modifier.m.sizeOf_spec : ∀ (presentation : Std.Time.Number), sizeOf (Std.Time.Modifier.m presentation) = 1 + sizeOf presentation
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.empty_mem_countableGeneratingSet : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace.CountablyGenerated α],
  ∅ ∈ MeasurableSpace.countableGeneratingSet α
-- Mathlib.Order.Hom.WithTopBot
WithTop.coe_toDualBotEquiv : ∀ {α : Type u_1} [inst : LE α], ⇑WithTop.toDualBotEquiv = ⇑OrderDual.toDual ∘ ⇑WithTop.ofDual
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Raw.toArray.eq_1 : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Raw α β),
  m.toArray = Std.DHashMap.Raw.fold (fun acc k v => acc.push ⟨k, v⟩) (Array.emptyWithCapacity m.size) m
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapId'_eq_mapId : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) (b : B), F.mapId' (CategoryTheory.CategoryStruct.id b) ⋯ = F.mapId b
-- Lean.Language.Lean.Types
Lean.Language.Lean.CommandResultSnapshot.mk.sizeOf_spec : ∀ (toSnapshot : Lean.Language.Snapshot) (cmdState : Lean.Elab.Command.State),
  sizeOf { toSnapshot := toSnapshot, cmdState := cmdState } = 1 + sizeOf toSnapshot + sizeOf cmdState
-- Init.Data.UInt.Lemmas
USize.lt_iff_le_and_ne : ∀ {a b : USize}, a < b ↔ a ≤ b ∧ a ≠ b