mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.MatrixPolynomialAlgebra
/-- The algebra isomorphism stating "matrices of polynomials are the same as polynomials of matrices".

(You probably shouldn't attempt to use this underlying definition ---
it's an algebra equivalence, and characterised extensionally by the lemma
`matPolyEquiv_coeff_apply` below.)
 -/
matPolyEquiv : {R : Type u_1} →
  [inst : CommSemiring R] →
    {n : Type w} →
      [inst_1 : DecidableEq n] → [inst_2 : Fintype n] → Matrix n n (Polynomial R) ≃ₐ[R] Polynomial (Matrix n n R)
-- Mathlib.Data.Nat.Factorization.Basic
Nat.ordCompl_pos : ∀ {n : ℕ} (p : ℕ), n ≠ 0 → 0 < n / p ^ n.factorization p
-- Init.Data.Ord.Basic
_private.Init.Data.Ord.Basic.0.Ordering.swap.match_1.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) → (Unit → motive Ordering.lt) → (Unit → motive Ordering.eq) → (Unit → motive Ordering.gt) → motive x
-- Mathlib.GroupTheory.Congruence.Defs
/-- The binary function on the quotient by a congruence relation `c` induced by a binary function
that is constant on `c`'s equivalence classes.  -/
Con.liftOn₂ : {M : Type u_1} →
  [inst : Mul M] →
    {β : Sort u_4} →
      {c : Con M} →
        c.Quotient → c.Quotient → (f : M → M → β) → (∀ (a₁ a₂ b₁ b₂ : M), c a₁ b₁ → c a₂ b₂ → f a₁ a₂ = f b₁ b₂) → β
-- Mathlib.Logic.Function.Basic
Function.instIrreflSwapProp : ∀ {α : Sort u_1} (r : α → α → Prop) [Std.Irrefl r], Std.Irrefl (Function.swap r)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.self_le_maxKeyD_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β} {fallback : α}, (cmp k ((t.insertIfNew k v).maxKeyD fallback)).isLE = true
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.RightHomotopy.symm_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v : CategoryTheory.Arrow V} {f g : u ⟶ v} (h : CategoryTheory.Arrow.RightHomotopy f g), h.symm.hom = -h.hom
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.intermediateFieldEquivSubgroup.eq_1 : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] [hGKL : IsGaloisGroup G K L] [inst_5 : Finite G],
  IsGaloisGroup.intermediateFieldEquivSubgroup G K L =
    IsGalois.intermediateFieldEquivSubgroup.trans (IsGaloisGroup.mulEquivAlgEquiv G K L).comapSubgroup.dual
-- Lean.Data.JsonRpc
Lean.JsonRpc.instToJsonErrorCode : Lean.ToJson Lean.JsonRpc.ErrorCode
-- Mathlib.Logic.Equiv.Prod
/-- A family of equivalences `∀ (a : α₁), β₁ ≃ β₂` generates an equivalence
between `β₁ × α₁` and `β₂ × α₁`.  -/
Equiv.prodCongrLeft : {α₁ : Type u_9} → {β₁ : Type u_11} → {β₂ : Type u_12} → (α₁ → β₁ ≃ β₂) → β₁ × α₁ ≃ β₂ × α₁
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
RightPreLieAlgebra.mk : {R : Type u_1} →
  [inst : CommRing R] →
    {L : Type u_2} →
      [inst_1 : RightPreLieRing L] →
        [toModule : Module R L] →
          [toIsScalarTower : IsScalarTower R L L] → [toSMulCommClass : SMulCommClass R L L] → RightPreLieAlgebra R L
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
AlgebraicGeometry.ProjectiveSpectrum.comapFun.congr_simp : ∀ {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : CommRing B] [inst_4 : SetLike τ B] [inst_5 : AddSubgroupClass τ B]
  {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [inst_6 : GradedRing 𝒜] [inst_7 : GradedRing ℬ] (f f_1 : 𝒜 →+*ᵍ ℬ) (e_f : f = f_1)
  (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜))
  (p p_1 : ProjectiveSpectrum ℬ),
  p = p_1 →
    AlgebraicGeometry.ProjectiveSpectrum.comapFun f hf p = AlgebraicGeometry.ProjectiveSpectrum.comapFun f_1 ⋯ p_1
-- Mathlib.LinearAlgebra.Matrix.Circulant
Matrix.circulant_add : ∀ {α : Type u_1} {n : Type u_3} [inst : Add α] [inst_1 : Sub n] (v w : n → α),
  Matrix.circulant (v + w) = Matrix.circulant v + Matrix.circulant w
-- Mathlib.CategoryTheory.GuitartExact.Basic
CategoryTheory.TwoSquare.EquivalenceJ.functor_map : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B) {X₂ : C₂}
  {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃) {f₁ f₂ : w.StructuredArrowRightwards g} (φ : f₁ ⟶ f₂),
  (CategoryTheory.TwoSquare.EquivalenceJ.functor w g).map φ =
    CategoryTheory.CostructuredArrow.homMk
      (CategoryTheory.StructuredArrow.homMk (CategoryTheory.StructuredArrow.Hom.right φ).left ⋯) ⋯
-- Mathlib.FieldTheory.LinearDisjoint
IntermediateField.LinearDisjoint.basisOfBasisLeft_repr_apply : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E}
  (H : A.LinearDisjoint ↥B) (H' : A.toSubalgebra ⊔ B.toSubalgebra = ⊤) {ι : Type u_1} (b : Module.Basis ι F ↥A) (x : ↥A)
  (i : ι), (algebraMap (↥B) E) (((H.basisOfBasisLeft H' b).repr ↑x) i) = (algebraMap F E) ((b.repr x) i)
-- Mathlib.Algebra.Torsor.Defs
/-- `p' ↦ p -ᵥ p'` as an equivalence.  -/
Equiv.constVSub : {G : Type u_1} → {P : Type u_2} → [inst : AddGroup G] → [AddTorsor G P] → P → P ≃ G
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
SSet.Subcomplex.N.mk_dim : ∀ {X : SSet} {A : X.Subcomplex} {n : ℕ} (x : X.obj (Opposite.op { len := n })) (hx : x ∈ X.nonDegenerate n)
  (hx' : x ∉ A.obj (Opposite.op { len := n })), (SSet.Subcomplex.N.mk x hx hx').dim = n
-- Mathlib.Algebra.Order.SuccPred
Order.pred_iterate : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommGroupWithOne α] [inst_2 : PredSubOrder α] (x : α) (n : ℕ),
  Order.pred^[n] x = x - ↑n
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
OrdinalApprox.gfpApprox_le : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} {a : Ordinal.{u}}, OrdinalApprox.gfpApprox f x a ≤ x
-- Mathlib.Geometry.Convex.ConvexSpace.Module
Convexity.StdSimplex.isAffineMap_weights : ∀ (R : Type u_2) (I : Type u_5) [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R],
  Convexity.IsAffineMap R Convexity.StdSimplex.weights
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.red_invRev_iff : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)},
  FreeGroup.Red (FreeGroup.invRev L₁) (FreeGroup.invRev L₂) ↔ FreeGroup.Red L₁ L₂
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
CochainComplex.Plus.instInjectiveXIntAsHomologicalComplexUpHomotopicObjHomotopyCategoryPlusObjPlusInjectiveObjectMapHomotopyCategoryPlusι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (X : HomotopyCategory.Plus (CategoryTheory.InjectiveObject C)) (n : ℤ),
  CategoryTheory.Injective (((CategoryTheory.InjectiveObject.ι C).mapHomotopyCategoryPlus.obj X).obj.as.X n)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.associator_inv_left_fst_fst_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  (R S T : CategoryTheory.Over X) {Z : C} (h : R.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.associator R S T).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst R.hom S.hom) R.hom) T.hom)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst R.hom S.hom) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst R.hom (CategoryTheory.MonoidalCategoryStruct.tensorObj S T).hom) h
-- Mathlib.Order.RelSeries
LTSeries.exists_relSeries_covBy_and_head_eq_bot_and_last_eq_bot : ∀ {α : Type u_3} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [WellFoundedLT α] [WellFoundedGT α] (s : LTSeries α),
  ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.id_comp : ∀ {M : Type u_4} {N : Type u_5} [inst : One M] [inst_1 : One N] (f : OneHom M N), (OneHom.id N).comp f = f
-- Init.System.CancelToken
/-- Registers a callback to run when the cancellation token is set or dropped. The callback runs as a
synchronous task dependency, so it executes inline on the thread that calls `set` (or on the
finalizer thread if the token is dropped). If the token is already set when `onSet` is called,
the callback runs immediately.
 -/
IO.CancelToken.onSet : IO.CancelToken → BaseIO Unit → BaseIO Unit
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.eval.eq_5 : ∀ (f g : Turing.ToPartrec.Code), (f.comp g).eval = fun v => g.eval v >>= f.eval
-- Std.Http.Protocol.H1.Parser
/-- Parses a quoted-string value, unescaping quoted-pairs.

`quoted-string = DQUOTE *( qdtext / quoted-pair ) DQUOTE`
 -/
_private.Std.Http.Protocol.H1.Parser.0.Std.Http.Protocol.H1.parseQuotedString : ℕ → Std.Internal.Parsec.ByteArray.Parser String
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.shiftMap_comp_assoc : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : F.ShiftSequence M] {X Y Z : C} {n : M}
  (f : X ⟶ (CategoryTheory.shiftFunctor C n).obj Y) (g : Y ⟶ Z) (a a' : M) (ha' : n + a = a') {Z_1 : A}
  (h : (F.shift a').obj Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (F.shiftMap (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.shiftFunctor C n).map g)) a a' ha') h =
    CategoryTheory.CategoryStruct.comp (F.shiftMap f a a' ha')
      (CategoryTheory.CategoryStruct.comp ((F.shift a').map g) h)
-- Mathlib.Analysis.Normed.Module.MStructure
/-- A projection on a normed space `X` is said to be an M-projection if, for all `x` in `X`,
$\|x\| = max(\|P x\|,\|(1 - P) x\|)$.

Note that we write `P • x` instead of `P x` for reasons described in the module docstring.
 -/
IsMprojection : (X : Type u_1) → [inst : NormedAddCommGroup X] → {M : Type u_2} → [inst_1 : Ring M] → [Module M X] → M → Prop
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of the forward direction of `SimpleGraph.Walk.isCircuit_mapLe`. -/
SimpleGraph.Walk.IsCircuit.of_mapLe : ∀ {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u : V} {p : G.Walk u u},
  (SimpleGraph.Walk.mapLe h p).IsCircuit → p.IsCircuit
-- Mathlib.Data.List.Rotate
List.rotate_mod : ∀ {α : Type u} (l : List α) (n : ℕ), l.rotate (n % l.length) = l.rotate n
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
lineDeriv_zero_of_not_lineDifferentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {x v : E},
  ¬LineDifferentiableAt 𝕜 f x v → lineDeriv 𝕜 f x v = 0
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Fintype.piFinset_vadd : ∀ {ι : Type u_5} {α : ι → Type u_6} {β : ι → Type u_7} [inst : Fintype ι] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → DecidableEq (β i)] [inst_3 : (i : ι) → VAdd (α i) (β i)] (s : (i : ι) → Finset (α i))
  (t : (i : ι) → Finset (β i)), (Fintype.piFinset fun i => s i +ᵥ t i) = Fintype.piFinset s +ᵥ Fintype.piFinset t
-- Mathlib.RingTheory.PrincipalIdealDomain
mod_mem_iff : ∀ {R : Type u} [inst : EuclideanDomain R] {S : Ideal R} {x y : R}, y ∈ S → (x % y ∈ S ↔ x ∈ S)
-- Init.Data.List.Monadic
/-- This lemma identifies monadic folds over lists of subtypes, where the function only depends on the value, not the proposition,
and simplifies these to the function directly taking the value.
 -/
List.foldrM_subtype : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {p : α → Prop}
  {l : List { x // p x }} {f : { x // p x } → β → m β} {g : α → β → m β} {x : β},
  (∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b) → List.foldrM f x l = List.foldrM g x l.unattach
-- Init.SizeOf
Decidable.isTrue.sizeOf_spec : ∀ {p : Prop} [inst : SizeOf p] (h : p), sizeOf (isTrue h) = 1 + sizeOf h
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.characteristic_inf : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} [H.Characteristic] [K.Characteristic], (H ⊓ K).Characteristic
-- Mathlib.LinearAlgebra.Trace
/-- Auxiliary lemma for `trace_eq_matrix_trace`.  -/
LinearMap.trace_eq_matrix_trace_of_finset : ∀ (R : Type u) [inst : CommSemiring R] {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Finset M}
  (b : Module.Basis (↥s) R M) (f : M →ₗ[R] M), (LinearMap.trace R M) f = ((LinearMap.toMatrix b b) f).trace
-- Mathlib.Order.Preorder.Chain
IsChain.lt_of_le : ∀ {α : Type u_1} [inst : PartialOrder α] {s : Set α},
  IsChain (fun x1 x2 => x1 ≤ x2) s → IsChain (fun x1 x2 => x1 < x2) s
-- Lean.Parser.Extra
Lean.Parser.evalInsideQuot.formatter : Lean.Name → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.Data.Setoid.Basic
/-- A bijection between the product of two quotients and the quotient by the product of the
equivalence relations.  -/
Setoid.prodQuotientEquiv : {α : Type u_1} → {β : Type u_2} → (r : Setoid α) → (s : Setoid β) → Quotient r × Quotient s ≃ Quotient (r.prod s)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂.of.sizeOf_spec : ∀ (η : Mathlib.Tactic.BicategoryLike.Atom), sizeOf (Mathlib.Tactic.BicategoryLike.Mor₂.of η) = 1 + sizeOf η
-- Mathlib.Order.Filter.AtTopBot.Prod
Filter.prod_map_atBot_eq : ∀ {α₁ : Type u_6} {α₂ : Type u_7} {β₁ : Type u_8} {β₂ : Type u_9} [inst : Preorder β₁] [inst_1 : Preorder β₂]
  (u₁ : β₁ → α₁) (u₂ : β₂ → α₂),
  Filter.map u₁ Filter.atBot ×ˢ Filter.map u₂ Filter.atBot = Filter.map (Prod.map u₁ u₂) Filter.atBot
-- Mathlib.RingTheory.Invariant.Defs
Algebra.IsInvariant.mk : ∀ {A : Type u_1} {B : Type u_2} {G : Type u_3} [inst : CommSemiring A] [inst_1 : Semiring B] [inst_2 : Algebra A B]
  [inst_3 : Group G] [inst_4 : MulSemiringAction G B],
  (∀ (b : B), (∀ (g : G), g • b = b) → ∃ a, (algebraMap A B) a = b) → Algebra.IsInvariant A B G
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
/-- Assuming `levyProkhorovEDist μ ν < ε`, we can bound `∫ f ∂μ` in terms of
`∫ t in (0, ‖f‖], ν (thickening ε {x | f(x) ≥ t}) dt` and `‖f‖`.  -/
MeasureTheory.BoundedContinuousFunction.integral_le_of_levyProkhorovEDist_lt : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoMetricSpace Ω] [OpensMeasurableSpace Ω]
  (μ ν : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {ε : ℝ},
  0 < ε →
    MeasureTheory.levyProkhorovEDist μ ν < ENNReal.ofReal ε →
      ∀ (f : BoundedContinuousFunction Ω ℝ),
        0 ≤ᵐ[μ] ⇑f →
          ∫ (ω : Ω), f ω ∂μ ≤ (∫ (t : ℝ) in Set.Ioc 0 ‖f‖, ν.real (Metric.thickening ε {a | t ≤ f a})) + ε * ‖f‖
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.mul_subset_iff_left : ∀ {α : Type u_2} [inst : Mul α] {s t u : Set α}, s * t ⊆ u ↔ ∀ a ∈ s, a • t ⊆ u
-- Mathlib.Algebra.WithConv
WithConv.toConv_sub : ∀ {A : Type u_2} [inst : AddGroup A] (x y : A), WithConv.toConv (x - y) = WithConv.toConv x - WithConv.toConv y
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.HasLaw.identDistrib : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ}
  {κ : MeasureTheory.Measure γ},
  ProbabilityTheory.HasLaw f κ μ → ProbabilityTheory.HasLaw g κ ν → ProbabilityTheory.IdentDistrib f g μ ν
-- Init.Grind.AC
Lean.Grind.AC.instBEqSeq.beq_spec_1 : ∀ (a b : Lean.Grind.AC.Var), (Lean.Grind.AC.Seq.var a == Lean.Grind.AC.Seq.var b) = (a == b)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.toZeroAtInfty.congr_simp : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : ProperSpace E] (f f_1 : SchwartzMap E F),
  f = f_1 → f.toZeroAtInfty = f_1.toZeroAtInfty
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.isEmbedding_isZariskiLocalAtTarget : AlgebraicGeometry.IsZariskiLocalAtTarget
  (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsEmbedding)
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Algebra.SubmersivePresentation.cotangentComplexAux_surjective : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ),
  Function.Surjective ⇑P.cotangentComplexAux
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aevalTower_comp_toAlgHom : ∀ {R : Type u} {S : Type v} {A' : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring A'] [inst_2 : CommSemiring S]
  [inst_3 : Algebra S R] [inst_4 : Algebra S A'] (g : R →ₐ[S] A') (y : A'),
  (Polynomial.aevalTower g y).comp (IsScalarTower.toAlgHom S R (Polynomial R)) = g
-- Init.Data.Dyadic.Basic
/-- The dyadic number `n * 2^(-k)` for some odd `n` and integer `k`.  -/
Dyadic.ofOdd : (n : ℤ) → ℤ → n % 2 = 1 → Dyadic
-- Mathlib.Data.Ordmap.Ordnode
/-- Auxiliary definition for `findGe`.  -/
Ordnode.findGeAux : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → α → Ordnode α → α → α
-- Mathlib.Algebra.Homology.AlternatingConst
/-- The `j`th homology of the alternating constant complex on `φ, ψ : A ⟶ A` is the homology of
`A --φ--> A --ψ--> A` when `prev(j) ~ j, j ~ next(j)` and `j` is odd.  -/
HomologicalComplex.alternatingConstHomologyIsoOdd : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (A : C) →
        {φ ψ : A ⟶ A} →
          (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) →
            (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) →
              {c : ComplexShape ℕ} →
                [inst_2 : DecidableRel c.Rel] →
                  (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) →
                    [inst_3 : CategoryTheory.CategoryWithHomology C] →
                      {j : ℕ} →
                        c.Rel (c.prev j) j →
                          c.Rel j (c.next j) →
                            Odd j →
                              ((HomologicalComplex.alternatingConst A hOdd hEven hc).homology j ≅
                                { X₁ := A, X₂ := A, X₃ := A, f := φ, g := ψ, zero := hOdd }.homology)
-- Mathlib.Order.Monotone.Basic
StrictAntiOn.cmp_map_eq : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β} {s : Set α} {x y : α},
  StrictAntiOn f s → x ∈ s → y ∈ s → cmp (f x) (f y) = cmp y x
-- Mathlib.GroupTheory.Exponent
/-- **Alias** of the reverse direction of `AddMonoid.exponent_pos`. -/
AddMonoid.ExponentExists.exponent_pos : ∀ {G : Type u} [inst : AddMonoid G], AddMonoid.ExponentExists G → 0 < AddMonoid.exponent G
-- Lean.Elab.ConfigEval.Commands
/-- `declare_config_elab f struct binders* [where ...]` defines a configuration elaborator
```lean
f binders* (cfg : Syntax) (init : struct := {}) (logExceptions : Bool := true) : TacticM struct
```
that evaluates the `cfg` configuration items to update `init`.
Acceptable configuration syntax is documented in `Lean.Elab.ConfigEval.foldConfigM`,
which includes anything that looks like `Lean.Parser.Term.optConfig`, possibly wrapped
in null nodes.

When `logExceptions` is true, it uses the current `recover` state to decide whether or not to
recover by logging errors and skipping invalid options.

The command will transitively derive any necessary `ConfigEval.EvalTerm`/`ConfigEval.EvalExpr`
instances to support evaluation of configuration options for structure fields.
These instances will be `private local`.

See `ConfigEval.defEvalConfigItemCmd` for further documentation.

See also `declare_core_config_elab`, `declare_term_config_elab`, and `declare_command_config_elab`.
 -/
Lean.Elab.ConfigEval.declareTacticConfig : Lean.ParserDescr
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.jmp.sizeOf_spec : ∀ (ref : Lean.Syntax) (jpName : Lean.Name) (args : Array Lean.Syntax),
  sizeOf (Lean.Elab.Term.Do.Code.jmp ref jpName args) = 1 + sizeOf ref + sizeOf jpName + sizeOf args
-- Lean.Compiler.Options
Lean.Compiler.compiler.checkMeta : Lean.Option Bool
-- Mathlib.MeasureTheory.Measure.NullMeasurable
/-- A null measurable set `t` is Carathéodory measurable: for any `s`, we have
`μ (s ∩ t) + μ (s \ t) = μ s`.  -/
MeasureTheory.measure_inter_add_sdiff₀ : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α),
  MeasureTheory.NullMeasurableSet t μ → μ (s ∩ t) + μ (s \ t) = μ s
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
_private.Mathlib.MeasureTheory.Integral.Lebesgue.Countable.0.MeasureTheory.«term_→ₛ_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
PresheafOfModules.tensorObj_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat}
  (M₁ M₂ : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))) (X : Cᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ M₂).obj X =
    CategoryTheory.MonoidalCategoryStruct.tensorObj (M₁.obj X) (M₂.obj X)
-- Init.Data.List.Basic
List.replicate_succ : ∀ {α : Type u} {a : α} {n : ℕ}, List.replicate (n + 1) a = a :: List.replicate n a
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi'.eq_1 : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [inst_2 : Encodable ι],
  MeasureTheory.Measure.pi' μ =
    MeasureTheory.Measure.map (List.TProd.elim' ⋯) (MeasureTheory.Measure.tprod (Encodable.sortedUniv ι) μ)
-- Mathlib.Order.RelSeries
/-- if `α` is infinite dimensional, then `α` is nonempty.  -/
LTSeries.nonempty_of_infiniteDimensionalOrder : ∀ (α : Type u_1) [inst : Preorder α] [InfiniteDimensionalOrder α], Nonempty α
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
CategoryTheory.Functor.WellOrderInductionData.Extension.map_succ : ∀ {J : Type u} [inst : LinearOrder J] [inst_1 : SuccOrder J] {F : CategoryTheory.Functor Jᵒᵖ (Type v)}
  {d : F.WellOrderInductionData} [inst_2 : OrderBot J] {val₀ : F.obj (Opposite.op ⊥)} {j : J}
  (self : d.Extension val₀ j) (i : J) (hi : i < j),
  (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) self.val =
    d.succ i ⋯ ((CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) self.val)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.le_def : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [inst : LE β],
  (fun x1 x2 => x1 ≤ x2) = Filter.Germ.LiftRel fun x1 x2 => x1 ≤ x2
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
preNormEDS'_four : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R), preNormEDS' b c d 4 = d
-- Mathlib.RingTheory.Localization.BaseChange
/-- If `A` is a localization of `R`, tensoring two `A`-modules over `A` is the same as
tensoring them over `R`.  -/
IsLocalization.moduleTensorEquiv : {R : Type u_1} →
  [inst : CommSemiring R] →
    (S : Submonoid R) →
      (A : Type u_2) →
        [inst_1 : CommSemiring A] →
          [inst_2 : Algebra R A] →
            [IsLocalization S A] →
              (M₁ : Type u_5) →
                (M₂ : Type u_6) →
                  [inst_4 : AddCommMonoid M₁] →
                    [inst_5 : AddCommMonoid M₂] →
                      [inst_6 : Module R M₁] →
                        [inst_7 : Module R M₂] →
                          [inst_8 : Module A M₁] →
                            [inst_9 : Module A M₂] →
                              [inst_10 : IsScalarTower R A M₁] →
                                [IsScalarTower R A M₂] → TensorProduct A M₁ M₂ ≃ₗ[A] TensorProduct R M₁ M₂