mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.InvariantForm
LieAlgebra.InvariantForm.restrict_orthogonal_nondegenerate : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L] [Module.Finite K L]
  (Φ : LinearMap.BilinForm K L),
  Φ.Nondegenerate →
    ∀ (hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ),
      Φ.IsRefl →
        (∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I) →
          ∀ (I : LieIdeal K L),
            IsAtom I →
              (Φ.restrict
                  (LieIdeal.toLieSubalgebra K L
                      (LieAlgebra.InvariantForm.orthogonal Φ hΦ_inv I)).toSubmodule).Nondegenerate
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
IsValuativeTopology.isTopologicalRing : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] [_t : TopologicalSpace R] [IsValuativeTopology R],
  IsTopologicalRing R
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.find?_toList_eq_none_iff_not_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α}, List.find? (fun x => cmp x.1 k == Ordering.eq) (Std.ExtDTreeMap.Const.toList t) = none ↔ k ∉ t
-- Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
MeasureTheory.projectiveFamilyContent_sdiff_of_subset : ∀ {ι : Type u_1} {α : ι → Type u_2} {mα : (i : ι) → MeasurableSpace (α i)}
  {P : (J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)} {s t : Set ((i : ι) → α i)}
  [∀ (J : Finset ι), MeasureTheory.IsFiniteMeasure (P J)] (hP : MeasureTheory.IsProjectiveMeasureFamily P),
  s ∈ MeasureTheory.measurableCylinders α →
    t ∈ MeasureTheory.measurableCylinders α →
      t ⊆ s →
        (MeasureTheory.projectiveFamilyContent hP) (s \ t) =
          (MeasureTheory.projectiveFamilyContent hP) s - (MeasureTheory.projectiveFamilyContent hP) t
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.eq_zero_or_opow_omega0_le_of_mul_eq_right : ∀ {a b : Ordinal.{u_1}}, a * b = b → b = 0 ∨ a ^ Ordinal.omega0 ≤ b
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.decidableMemCenter : {R : Type u_1} → [inst : Ring R] → [DecidableEq R] → [Fintype R] → DecidablePred fun x => x ∈ Subring.center R
-- Mathlib.CategoryTheory.Preadditive.Schur
/-- **Schur's lemma** for endomorphisms in `𝕜`-linear categories.
 -/
CategoryTheory.finrank_endomorphism_simple_eq_one : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (𝕜 : Type u_2)
  [inst_2 : Field 𝕜] [IsAlgClosed 𝕜] [inst_4 : CategoryTheory.Linear 𝕜 C] [CategoryTheory.Limits.HasKernels C] (X : C)
  [CategoryTheory.Simple X] [FiniteDimensional 𝕜 (X ⟶ X)], Module.finrank 𝕜 (X ⟶ X) = 1
-- Mathlib.Order.Interval.Set.Fin
Fin.image_natAdd_Ico : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Fin.natAdd m '' Set.Ico i j = Set.Ico (Fin.natAdd m i) (Fin.natAdd m j)
-- Init.Core
Function.comp_const : ∀ {β : Sort u_1} {γ : Sort u_2} {α : Sort u_3} {f : β → γ} {b : β}, f ∘ Function.const α b = Function.const α (f b)
-- Mathlib.Control.EquivFunctor.Instances
Fintype.ofBijective.congr_simp : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] (f f_1 : α → β) (e_f : f = f_1) (H : Function.Bijective f),
  Fintype.ofBijective f H = Fintype.ofBijective f_1 ⋯
-- Mathlib.Data.Seq.Computation
Computation.get_eq_of_mem : ∀ {α : Type u} (s : Computation α) [h : s.Terminates] {a : α}, a ∈ s → s.get = a
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- An additive monoid homomorphism `M →+ N` can equivalently be viewed as an additive monoid
homomorphism `Mᵃᵒᵖ →+ Nᵃᵒᵖ`. This is the action of the (fully faithful)
`ᵃᵒᵖ`-functor on morphisms.  -/
AddMonoidHom.op : {M : Type u_3} → {N : Type u_4} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → (M →+ N) ≃ (Mᵃᵒᵖ →+ Nᵃᵒᵖ)
-- Init.Data.Int.Order
Int.lt_asymm : ∀ {a b : ℤ}, a < b → ¬b < a
-- Mathlib.Algebra.Ring.Hom.Defs
/-- Bundled semiring homomorphisms; use this for bundled ring homomorphisms too.

This extends from both `MonoidHom` and `MonoidWithZeroHom` in order to put the fields in a
sensible order, even though `MonoidWithZeroHom` already extends `MonoidHom`.  -/
RingHom : (α : Type u_5) → (β : Type u_6) → [NonAssocSemiring α] → [NonAssocSemiring β] → Type (max u_5 u_6)
-- Mathlib.Analysis.Complex.CoveringMap
isCoveringMapOn_zpow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [ProperSpace 𝕜] (n : ℤ),
  ↑n ≠ 0 → IsCoveringMapOn (fun x => x ^ n) {0}ᶜ
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_sum_left' : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ}
  {s : Finset ι} [MeasureTheory.IsFiniteMeasure μ],
  (∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) →
    MeasureTheory.MemLp Y 2 μ →
      ProbabilityTheory.covariance (∑ i ∈ s, X i) Y μ = ∑ i ∈ s, ProbabilityTheory.covariance (X i) Y μ
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- Get the next key.  -/
Lean.Meta.RefinedDiscrTree.keysAsPattern.next : Array Lean.Meta.RefinedDiscrTree.Key →
  StateRefT' IO.RealWorld (List Lean.Meta.RefinedDiscrTree.Key) Lean.CoreM Lean.Meta.RefinedDiscrTree.Key
-- Mathlib.NumberTheory.Pell
/-- An alternative form of the equation, suitable for rewriting `d * y^2`.  -/
Pell.Solution₁.prop_y : ∀ {d : ℤ} (a : Pell.Solution₁ d), d * a.y ^ 2 = a.x ^ 2 - 1
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.lt_lsub_iff : ∀ {ι : Type u_3} {f : ι → Ordinal.{max u_4 u_3}} {a : Ordinal.{max u_3 u_4}}, a < Ordinal.lsub f ↔ ∃ i, a ≤ f i
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.isLongestMatchAtChain_iff_toList : ∀ {c : Char} {s : String.Slice} {pos pos' : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatchAtChain c pos pos' ↔
    ∃ (h : pos ≤ pos'), (s.slice pos pos' h).copy.toList = List.replicate (s.slice pos pos' h).copy.toList.length c
-- Init.Data.Iterators.Lemmas.Consumers.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Collect.0.Std.Iter.atIdxSlow?.match_3.eq_1 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] (it : Std.Iter β) (motive : it.Step → Sort u_2) (it' : Std.Iter β)
  (out : β) (property : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) →
        (property : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, property⟩)
  (h_2 :
    (it' : Std.Iter β) →
      (property : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', property⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.yield it' out, property⟩ with
    | ⟨Std.IterStep.yield it' out, property⟩ => h_1 it' out property
    | ⟨Std.IterStep.skip it', property⟩ => h_2 it' property
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_1 it' out property
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict.eq_1 : ∀ {α : Type u_2} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : Set α),
  μ.restrict s = (MeasureTheory.Measure.restrictₗ s) μ
-- Init.Data.Nat.Sqrt.Basic
/-- Integer square root function. Implemented via Newton's method.
 -/
Nat.sqrt : ℕ → ℕ
-- Mathlib.LinearAlgebra.Dual.Defs
Submodule.map_dualCoannihilator_le : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (Φ : Submodule R (Module.Dual R M)), Submodule.map (Module.Dual.eval R M) Φ.dualCoannihilator ≤ Φ.dualAnnihilator
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.map_addY : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Affine R} (f : R →+* S)
  (x₁ y₁ x₂ ℓ : R), (W'.map f).addY (f x₁) (f x₂) (f y₁) (f ℓ) = f (W'.addY x₁ x₂ y₁ ℓ)
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.gcd_ne_zero_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
  {f : β → α}, s.gcd f ≠ 0 ↔ ∃ x ∈ s, f x ≠ 0
-- Mathlib.Order.Bounded
Set.unbounded_inter_ge : ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α] (a : α),
  Set.Unbounded (fun x1 x2 => x1 > x2) (s ∩ {b | b ≤ a}) ↔ Set.Unbounded (fun x1 x2 => x1 > x2) s
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.comm : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp}, t₁.Equiv t₂ ↔ t₂.Equiv t₁
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.toMatrixOrthonormal_apply_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {n : Type u_6} [inst_3 : Fintype n] [inst_4 : DecidableEq n] [inst_5 : FiniteDimensional 𝕜 E]
  (v₁ : OrthonormalBasis n 𝕜 E) (f : E →ₗ[𝕜] E) (i j : n),
  (LinearMap.toMatrixOrthonormal v₁) f i j = inner 𝕜 (v₁ i) (f (v₁ j))
-- Mathlib.Data.ENat.Lattice
/-- **Alias** of `ENat.iSup_natCast_eq_top`. -/
ENat.iSup_coe_eq_top : ∀ {ι : Sort u_1} {f : ι → ℕ}, ⨆ i, ↑(f i) = ⊤ ↔ ¬BddAbove (Set.range f)
-- Mathlib.Data.Fin.Tuple.Reflection
FinVec.seq.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (n : ℕ) (f : Fin (n + 1) → α → β) (v : Fin (n + 1) → α),
  FinVec.seq f v = Matrix.vecCons (f 0 (v 0)) (FinVec.seq (Matrix.vecTail f) (Matrix.vecTail v))
-- Lean.Data.PersistentArray
Lean.PersistentArray.findSome? : {α : Type u} → {β : Type u_1} → Lean.PersistentArray α → (α → Option β) → Option β
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- **Alias** of `smul_apply`. -/
QuadraticMap.smul_apply : ∀ {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst : FunLike F α β}
  {inst_1 : SMul M β} {inst_2 : SMul M F} [self : IsSMulApply M F α β] (f : F) (r : M) (x : α), (r • f) x = r • f x
-- Mathlib.Order.ConditionallyCompletePartialOrder.Defs
DirectedOn.csSup_le : ∀ {α : Type u_2} [inst : ConditionallyCompletePartialOrderSup α] {s : Set α} {a : α},
  DirectedOn (fun x1 x2 => x1 ≤ x2) s → s.Nonempty → (∀ b ∈ s, b ≤ a) → sSup s ≤ a
-- Mathlib.Algebra.Lie.AdjointAction.Basic
Algebra.lsmul.eq_1 : ∀ (R : Type u) {A : Type w} (B : Type u₁) (M : Type v₁) [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : AddCommMonoid M] [inst_6 : Module R M]
  [inst_7 : Module A M] [inst_8 : Module B M] [inst_9 : IsScalarTower R A M] [inst_10 : IsScalarTower R B M]
  [inst_11 : SMulCommClass A B M],
  Algebra.lsmul R B M =
    { toFun := DistribSMul.toLinearMap B M, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯,
      commutes' := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.yonedaGrpFullyFaithful.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.yonedaGrpFullyFaithful =
    {
      preimage := fun {G H} α =>
        CategoryTheory.Grp.homMk'
          (CategoryTheory.yonedaMonFullyFaithful.preimage
            (CategoryTheory.Functor.whiskerRight α (CategoryTheory.forget₂ GrpCat MonCat))),
      map_preimage := ⋯, preimage_map := ⋯ }
-- Mathlib.FieldTheory.NormalizedTrace
_private.Mathlib.FieldTheory.NormalizedTrace.0.Algebra.normalizedTraceAux : (F : Type u_1) → (K : Type u_2) → [inst : Field F] → [inst_1 : Field K] → [Algebra F K] → K → F
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
/-- `C^{n + 1}` is equivalent to `C^n` and the `n`-th derivative being `C^1`.  -/
contDiff_nat_succ_iff_contDiff_one_iteratedDeriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {n : ℕ},
  ContDiff 𝕜 (↑(n + 1)) f ↔ ContDiff 𝕜 (↑n) f ∧ ContDiff 𝕜 1 (iteratedDeriv n f)
-- Mathlib.Order.Hom.Bounded
TopHomClass.toTopHom.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Top α] [inst_2 : Top β]
  [inst_3 : TopHomClass F α β] (f : F), ↑f = { toFun := ⇑f, map_top' := ⋯ }
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- The composition of equivalences between measurable spaces.  -/
MeasurableEquiv.trans : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      [inst : MeasurableSpace α] →
        [inst_1 : MeasurableSpace β] → [inst_2 : MeasurableSpace γ] → α ≃ᵐ β → β ≃ᵐ γ → α ≃ᵐ γ
-- Std.Data.DHashMap.Internal.AssocList.Basic
Std.DHashMap.Internal.instInhabitedAssocList : {a : Type u_1} → {a_1 : a → Type u_2} → Inhabited (Std.DHashMap.Internal.AssocList a a_1)
-- Lean.Meta.IntInstTesters
Lean.Meta.Structural.isInstDivInt : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.instUniqueOfSubsingleton.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Subsingleton G],
  AddSubgroup.instUniqueOfSubsingleton = { default := ⊥, uniq := ⋯ }
-- Std.Data.ExtTreeSet.Basic
/-- Returns the number of mappings present in the map.  -/
Std.ExtTreeSet.size : {α : Type u} → {cmp : α → α → Ordering} → Std.ExtTreeSet α cmp → ℕ
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.SemiCartesianMonoidalCategory.comp_toUnit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory C]
  {X Y : C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.SemiCartesianMonoidalCategory.toUnit Y) =
    CategoryTheory.SemiCartesianMonoidalCategory.toUnit X
-- Mathlib.Algebra.Algebra.Tower
AlgHom.coe_restrictScalars : ∀ (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B]
  (f : A →ₐ[S] B), ↑(AlgHom.restrictScalars R f) = ↑f
-- LeanSearchClient.Syntax
LeanSearchClient.SearchServer.url : LeanSearchClient.SearchServer → String
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.IsZeroOrProbabilityMeasure.mk : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  μ Set.univ = 0 ∨ μ Set.univ = 1 → MeasureTheory.IsZeroOrProbabilityMeasure μ
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.Hom.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} (app : (X : Cᵒᵖ) → M₁.obj X ⟶ M₂.obj X)
  (naturality :
    autoParam
      (∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
        CategoryTheory.CategoryStruct.comp (M₁.map f)
            ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (app Y)) =
          CategoryTheory.CategoryStruct.comp (app X) (M₂.map f))
      PresheafOfModules.Hom.naturality._autoParam)
  (app_1 : (X : Cᵒᵖ) → M₁.obj X ⟶ M₂.obj X)
  (naturality_1 :
    autoParam
      (∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
        CategoryTheory.CategoryStruct.comp (M₁.map f)
            ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (app_1 Y)) =
          CategoryTheory.CategoryStruct.comp (app_1 X) (M₂.map f))
      PresheafOfModules.Hom.naturality._autoParam),
  ({ app := app, naturality := naturality } = { app := app_1, naturality := naturality_1 }) = (app = app_1)
-- Mathlib.LinearAlgebra.Matrix.Hermitian
/-- Assumes `IsSelfAdjoint ⅟k` instead of `IsSelfAdjoint k`.
These are equivalent given `StarMul R`  -/
Matrix.IsHermitian.of_smul' : ∀ {α : Type u_1} {n : Type u_4} {R : Type u_5} [inst : Monoid R] [inst_1 : Star R] [inst_2 : Star α]
  [inst_3 : MulAction R α] [StarModule R α] {A : Matrix n n α} {k : R} [inst_5 : Invertible k],
  (k • A).IsHermitian → IsSelfAdjoint ⅟k → A.IsHermitian
-- Mathlib.Analysis.Normed.Group.Basic
exists_nnnorm_ne_zero : ∀ (E : Type u_5) [inst : SeminormedAddGroup E] [NontrivialTopology E], ∃ x, ‖x‖₊ ≠ 0
-- Mathlib.RingTheory.SimpleModule.WedderburnArtin
/-- The **Wedderburn–Artin Theorem**, algebra form, finite case: a finite Artinian simple algebra is
isomorphic to a matrix algebra over a finite division algebra.  -/
IsSimpleRing.exists_algEquiv_matrix_divisionRing_finite : ∀ (R₀ : Type u_1) (R : Type u) [inst : CommSemiring R₀] [inst_1 : Ring R] [inst_2 : Algebra R₀ R] [IsSimpleRing R]
  [IsArtinianRing R] [Module.Finite R₀ R],
  ∃ n, ∃ (_ : NeZero n), ∃ D x x_1, ∃ (_ : Module.Finite R₀ D), Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) D)
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableOn.fun_sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {ι : Type u_4} {u : Finset ι} {A : ι → E → F},
  (∀ i ∈ u, DifferentiableOn 𝕜 (A i) s) → DifferentiableOn 𝕜 (fun y => ∑ i ∈ u, A i y) s
-- Std.Time.Time.Unit.Hour
/-- Creates an `Offset` from a natural number.
 -/
Std.Time.Hour.Offset.ofNat : ℕ → Std.Time.Hour.Offset
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasDerivAt.rpow_const : ∀ {f : ℝ → ℝ} {f' x p : ℝ},
  HasDerivAt f f' x → f x ≠ 0 ∨ 1 ≤ p → HasDerivAt (fun y => f y ^ p) (f' * p * f x ^ (p - 1)) x
-- Mathlib.Algebra.Algebra.Basic
/-- If `R →+* S` is surjective, then `R`-linear maps are also `S`-linear.  -/
LinearMap.extendScalarsOfSurjective : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring S] →
        [inst_2 : Algebra R S] →
          {M : Type u_3} →
            {N : Type u_4} →
              [inst_3 : AddCommMonoid M] →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module S M] →
                      [IsScalarTower R S M] →
                        [inst_8 : Module R N] →
                          [inst_9 : Module S N] →
                            [IsScalarTower R S N] → Function.Surjective ⇑(algebraMap R S) → (M →ₗ[R] N) → M →ₗ[S] N
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier.eq_1 : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] {f : A} (x : ↑((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).toTopCat),
  AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier x =
    Ideal.comap (algebraMap (HomogeneousLocalization.Away 𝒜 f) (Localization.Away f))
      (Ideal.map (algebraMap A (Localization.Away f)) (↑x).asHomogeneousIdeal.toIdeal)
-- Mathlib.Data.ENNReal.Basic
ENNReal.ofNNReal_natCast_sub : ∀ (n : ℕ) (r : NNReal), ↑(↑n - r) = ↑n - ↑r
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.toEquiv_refl : ∀ (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁], (AffineEquiv.refl k P₁).toEquiv = Equiv.refl P₁
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.associatorImpl_hom_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y Z : CategoryTheory.Dial C),
  (X.associatorImpl Y Z).hom.f =
    CategoryTheory.Limits.prod.lift
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst)
      (CategoryTheory.Limits.prod.lift
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd)
        CategoryTheory.Limits.prod.snd)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Decl.mk : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Signature pu →
    Lean.Compiler.LCNF.DeclValue pu → Bool → Option Lean.Compiler.InlineAttributeKind → Lean.Compiler.LCNF.Decl pu
-- Mathlib.RingTheory.Polynomial.Basic
Ideal.leadingCoeffNth_mono : ∀ {R : Type u} [inst : CommSemiring R] (I : Ideal (Polynomial R)) {m n : ℕ},
  m ≤ n → I.leadingCoeffNth m ≤ I.leadingCoeffNth n
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
LinearIsometryEquiv.comp_fderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {x : G},
  fderiv 𝕜 (⇑iso ∘ f) x = ↑↑iso ∘SL fderiv 𝕜 f x
-- Mathlib.RingTheory.Algebraic.Basic
/-- If `Polynomial.aeval r f` is transcendental over `R`, then `f : R[X]` is also
transcendental over `R`. In fact, the `r` is also transcendental over `R` provided that `R`
is a field (see `transcendental_aeval_iff`).  -/
Transcendental.of_aeval : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {r : A} {f : Polynomial R},
  Transcendental R ((Polynomial.aeval r) f) → Transcendental R f
-- Mathlib.Algebra.Lie.Sl2
IsSl2Triple.HasPrimitiveVectorWith.congr_simp : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {h h_1 : L} (e_h : h = h_1) {e e_1 : L} (e_e : e = e_1) {f f_1 : L}
  (e_f : f = f_1) (t : IsSl2Triple h e f) (m m_1 : M),
  m = m_1 → ∀ (μ μ_1 : R), μ = μ_1 → t.HasPrimitiveVectorWith m μ = ⋯.HasPrimitiveVectorWith m_1 μ_1
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.mul_one : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] (χ : MulChar R R'), χ * 1 = χ
-- Mathlib.Data.Set.Prod
toPullbackDiag_coe : ∀ {X : Type u_1} {Y : Sort u_2} (f : X → Y) (x : X), ↑(toPullbackDiag f x) = (x, x)
-- Mathlib.Data.Matrix.Mul
Matrix.vecMul_neg : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocRing α] [inst_1 : Fintype m] (v : m → α)
  (A : Matrix m n α), Matrix.vecMul v (-A) = -Matrix.vecMul v A
-- Init.Data.Order.LemmasExtra
/-- This lemma derives a `LawfulOrderSup α` instance from a property involving an `Ord α` instance.
 -/
Std.LawfulOrderSup.of_ord : ∀ (α : Type u) [inst : Ord α] [inst_1 : Max α] [inst_2 : LE α] [Std.LawfulOrderOrd α],
  (∀ (a b c : α), (compare (a ⊔ b) c).isLE = true ↔ (compare a c).isLE = true ∧ (compare b c).isLE = true) →
    Std.LawfulOrderSup α
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.ιTruncLE_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : ∀ (i : ℤ), HomologicalComplex.HasHomology K i] [inst_4 : ∀ (i : ℤ), HomologicalComplex.HasHomology L i]
  (n : ℤ),
  CategoryTheory.CategoryStruct.comp (CochainComplex.truncLEMap φ n) (L.ιTruncLE n) =
    CategoryTheory.CategoryStruct.comp (K.ιTruncLE n) φ
-- Init.Data.List.MinMax
List.max_replicate : ∀ {α : Type u_1} [inst : Max α] [Std.MaxEqOr α] {n : ℕ} {a : α} (h : List.replicate n a ≠ []),
  (List.replicate n a).max h = a
-- Mathlib.Order.SuccPred.Limit
IsLUB.mem_of_not_isSuccLimit : ∀ {α : Type u_1} {a : α} [inst : LinearOrder α] {s : Set α}, IsLUB s a → s.Nonempty → ¬Order.IsSuccLimit a → a ∈ s
-- Mathlib.Geometry.Manifold.Instances.Real
/-- Definition of the model with corners `(EuclideanSpace ℝ (Fin n), EuclideanHalfSpace n)`, used as
a model for manifolds with boundary. In the scope `Manifold`, use the shortcut `𝓡∂ n`.
 -/
modelWithCornersEuclideanHalfSpace : (n : ℕ) → [inst : NeZero n] → ModelWithCorners ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanHalfSpace n)
-- Mathlib.Algebra.Star.Basic
star_zsmul : ∀ {R : Type u} [inst : AddGroup R] [inst_1 : StarAddMonoid R] (n : ℤ) (x : R), star (n • x) = n • star x
-- Mathlib.GroupTheory.OrderOfElement
/-- Inverses of elements of finite order have finite order.  -/
isOfFinOrder_inv_iff : ∀ {G : Type u_1} [inst : Group G] {x : G}, IsOfFinOrder x⁻¹ ↔ IsOfFinOrder x
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.instSetLike.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G],
  FiniteIndexNormalAddSubgroup.instSetLike = { coe := fun U => ↑U.toAddSubgroup, coe_injective := ⋯ }
-- Mathlib.Computability.NFA
NFA.Path.cons.inj : ∀ {α : Type u} {σ : Type v} {M : NFA α σ} {t s u : σ} {a : α} {x : List α} {a_1 : t ∈ M.step s a} {a_2 : M.Path t u x}
  {t_1 : σ} {a_3 : t_1 ∈ M.step s a} {a_4 : M.Path t_1 u x},
  NFA.Path.cons t s u a x a_1 a_2 = NFA.Path.cons t_1 s u a x a_3 a_4 → t = t_1 ∧ a_2 ≍ a_4