mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.List.InsertIdx
/-- Erasing `n`th element of a list, then inserting `a` at the same place
is the same as setting `n`th element to `a`.

We assume that `n ≠ length l`, because otherwise LHS equals `l ++ [a]` while RHS equals `l`.  -/
List.insertIdx_eraseIdx_self : ∀ {α : Type u} {l : List α} {n : ℕ}, n ≠ l.length → ∀ (a : α), (l.eraseIdx n).insertIdx n a = l.set n a
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.G : Std.Time.GenericFormat.DateBuilder✝ → Option Std.Time.Year.Era
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.mopMopEquivalenceFunctorMonoidal_μ : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X Y : Cᴹᵒᵖᴹᵒᵖ),
  CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.MonoidalOpposite.mopMopEquivalence C).functor X Y =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.unmop.unmop Y.unmop.unmop)
-- Mathlib.CategoryTheory.Functor.TwoSquare
CategoryTheory.TwoSquare.hComp_app : ∀ {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₄} {C₅ : Type u₅} {C₆ : Type u₆}
  [inst_4 : CategoryTheory.Category.{v₅, u₅} C₅] [inst_5 : CategoryTheory.Category.{v₆, u₆} C₆]
  {T' : CategoryTheory.Functor C₂ C₅} {R' : CategoryTheory.Functor C₅ C₆} {B' : CategoryTheory.Functor C₄ C₆}
  (w : CategoryTheory.TwoSquare T L R B) (w' : CategoryTheory.TwoSquare T' R R' B') (X : C₁),
  (w.hComp w').app X = CategoryTheory.CategoryStruct.comp (w'.natTrans.app (T.obj X)) (B'.map (w.natTrans.app X))
-- Lean.Compiler.IR.Basic
Lean.IR.DeclInfo.mk.sizeOf_spec : ∀ (sorryDep? : Option Lean.Name), sizeOf { sorryDep? := sorryDep? } = 1 + sizeOf sorryDep?
-- Mathlib.Algebra.GroupWithZero.Defs
MonoidWithZero.toSemigroupWithZero : {M₀ : Type u} → [self : MonoidWithZero M₀] → SemigroupWithZero M₀
-- Mathlib.Tactic.Module
Mathlib.Tactic.Module.NF.instSMulOfMul : {R : Type u_2} → {M : Type u_3} → [Mul R] → SMul R (Mathlib.Tactic.Module.NF R M)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.toContinuousLinearMap_one : ∀ {R₁ : Type u_1} [inst : Semiring R₁] (M₁ : Type u_4) [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁], ↑1 = 1
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.postSEval : Lean.Meta.Simp.SimprocsArray → Lean.Meta.Simp.Simproc
-- Mathlib.GroupTheory.GroupAction.Hom
instFunLikeAddActionHom.eq_1 : ∀ {M : Type u_2} {N : Type u_3} (φ : M → N) (X : Type u_5) [inst : VAdd M X] (Y : Type u_6) [inst_1 : VAdd N Y],
  instFunLikeAddActionHom φ X Y = { coe := AddActionHom.toFun, coe_injective := ⋯ }
-- Init.Data.SInt.Lemmas
ISize.le_refl : ∀ (a : ISize), a ≤ a
-- Mathlib.Algebra.Module.FinitePresentation
Module.FinitePresentation.of_equiv : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (e : M ≃ₗ[R] N) [Module.FinitePresentation R M],
  Module.FinitePresentation R N
-- Mathlib.NumberTheory.ModularForms.Derivative
Derivative.normalizedDerivOfComplex_pow : ∀ (F : UpperHalfPlane → ℂ) (n : ℕ),
  MDiff F → Derivative.normalizedDerivOfComplex (F ^ n) = ↑n * F ^ (n - 1) * Derivative.normalizedDerivOfComplex F
-- Mathlib.Topology.Order.LocalExtr
IsLocalMaxOn.comp_mono : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {f : α → β} {s : Set α} {a : α}, IsLocalMaxOn f s a → ∀ {g : β → γ}, Monotone g → IsLocalMaxOn (g ∘ f) s a
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
CochainComplex.shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex (CochainComplex C ℤ))
  (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting)
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {Z : CochainComplex C ℤ}
  (h : CochainComplex.mappingCone (CochainComplex.homOfDegreewiseSplit S σ) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map S.f)
      (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeHomOfDegreewiseSplitIso S σ).inv h) =
    CategoryTheory.CategoryStruct.comp (-CochainComplex.mappingCone.inr (CochainComplex.homOfDegreewiseSplit S σ)) h
-- Mathlib.Combinatorics.Quiver.ConnectedComponent
/-- The canonical map from a vertex to its strongly connected component.  -/
Quiver.StronglyConnectedComponent.mk : {V : Type u_2} → [inst : Quiver V] → V → Quiver.StronglyConnectedComponent V
-- Lean.Meta.Sym.Canon
/-- Reduce a projection function application (e.g., `@Sigma.fst _ _ ⟨a, b⟩` → `a`).
Class projections are not reduced — they are support elements handled by instance synthesis.
 -/
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.reduceProjFn? : Lean.ProjectionFunctionInfo → Lean.Expr → Lean.Meta.Sym.SymM (Option Lean.Expr)
-- Mathlib.Order.Bounds.Basic
IsGLB.insert : ∀ {γ : Type u_3} [inst : SemilatticeInf γ] (a : γ) {b : γ} {s : Set γ}, IsGLB s b → IsGLB (insert a s) (a ⊓ b)
-- Mathlib.Algebra.Group.TypeTags.Basic
Multiplicative.isLeftCancelMul : ∀ {α : Type u} [inst : Add α] [IsLeftCancelAdd α], IsLeftCancelMul (Multiplicative α)
-- Mathlib.Order.Interval.Finset.Basic
Finset.uIcc_of_not_ge : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α},
  ¬b ≤ a → Finset.uIcc a b = Finset.Icc a b
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
IsStarNormal.cfcₙ_map : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] (f : R → R) (a : A),
  IsStarNormal (cfcₙ f a)
-- Init.Data.List.Scan.Lemmas
List.scanr_iff_nil : ∀ {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : α → β → β} (c : β), List.scanr f b l = [c] ↔ c = b ∧ l = []
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
pi_polarCoord_symm_target_ae_eq_univ : ∀ {ι : Type u_1} [inst : Fintype ι],
  ((Pi.map fun x => ↑polarCoord.symm) '' Set.univ.pi fun x => polarCoord.target) =ᵐ[MeasureTheory.volume] Set.univ
-- Init.Data.List.Lemmas
List.forall_mem_flatten : ∀ {α : Type u_1} {p : α → Prop} {L : List (List α)}, (∀ x ∈ L.flatten, p x) ↔ ∀ l ∈ L, ∀ x ∈ l, p x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
/-- The slope of the line through two nonsingular affine points `(x₁, y₁)` and `(x₂, y₂)` on a
Weierstrass curve `W`.

If `x₁ ≠ x₂`, then this line is the secant of `W` through `(x₁, y₁)` and `(x₂, y₂)`, and has slope
`(y₁ - y₂) / (x₁ - x₂)`. Otherwise, if `y₁ ≠ -y₁ - a₁x₁ - a₃`, then this line is the tangent of `W`
at `(x₁, y₁) = (x₂, y₂)`, and has slope `(3x₁² + 2a₂x₁ + a₄ - a₁y₁) / (2y₁ + a₁x₁ + a₃)`. Otherwise,
this line is vertical, in which case this returns the value `0`.

This depends on `W`, and has argument order: `x₁`, `x₂`, `y₁`, `y₂`.  -/
WeierstrassCurve.Affine.slope : {F : Type u} → [Field F] → WeierstrassCurve.Affine F → [DecidableEq F] → F → F → F → F → F
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.ringEquivOfRingEquiv_eq_map : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {T : Submonoid P}
  {Q : Type u_4} [inst_5 : CommSemiring Q] [inst_6 : Algebra P Q] [inst_7 : IsLocalization T Q] {j : R ≃+* P}
  (H : Submonoid.map j.toMonoidHom M = T), ↑(IsLocalization.ringEquivOfRingEquiv S Q j H) = IsLocalization.map Q ↑j ⋯
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.coe_vadd : ∀ {α : Type u_1} [inst : TopologicalSpace α] {R : Type u_3} {M : Type u_5} [inst_1 : TopologicalSpace M]
  [inst_2 : VAdd R M] [inst_3 : ContinuousConstVAdd R M] (c : R) (f : C(α, M)), ⇑(c +ᵥ f) = c +ᵥ ⇑f
-- Mathlib.Combinatorics.Quiver.SingleObj
Quiver.SingleObj.toPrefunctor_symm_id : ∀ {α : Type u_1}, Quiver.SingleObj.toPrefunctor.symm (𝟭q (Quiver.SingleObj α)) = id
-- Mathlib.Order.CompleteLattice.Basic
iSup_sigma' : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {κ : β → Type u_8} (f : (i : β) → κ i → α),
  ⨆ i, ⨆ j, f i j = ⨆ x, f x.fst x.snd
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.affine_isIntegral_iff : ∀ (R : CommRingCat), AlgebraicGeometry.IsIntegral (AlgebraicGeometry.Spec R) ↔ IsDomain ↑R
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.nonUnitalAlgHom_ext'_iff : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : Semiring R] [inst_1 : Add M]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] {φ₁ φ₂ : AddMonoidAlgebra R M →ₙₐ[R] A},
  φ₁ = φ₂ ↔ φ₁.toMulHom.comp (AddMonoidAlgebra.ofMagma R M) = φ₂.toMulHom.comp (AddMonoidAlgebra.ofMagma R M)
-- Mathlib.Data.Sign.Defs
SignType.instMul : Mul SignType
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.instIsAnisotropicOfIsCrystallographic : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : CommRing R] [inst_4 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  [CharZero R] [P.IsCrystallographic], P.IsAnisotropic
-- Mathlib.CategoryTheory.Localization.Bousfield
CategoryTheory.ObjectProperty.isLocal_eq_inverseImage_isomorphisms : ∀ {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] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : G ⊣ F) [F.Full] [F.Faithful],
  (CategoryTheory.ObjectProperty.isLocal fun x => x ∈ Set.range F.obj) =
    (CategoryTheory.MorphismProperty.isomorphisms C).inverseImage G
-- Mathlib.Tactic.ClickSuggestions.Rewrite
Mathlib.Tactic.ClickSuggestions.RwKey.mk.inj : ∀ {numGoals : ℕ} {symm : Bool} {nameLength replacementSize : ℕ} {name : String}
  {replacement : Lean.Meta.AbstractMVarsResult} {numGoals_1 : ℕ} {symm_1 : Bool} {nameLength_1 replacementSize_1 : ℕ}
  {name_1 : String} {replacement_1 : Lean.Meta.AbstractMVarsResult},
  { numGoals := numGoals, symm := symm, nameLength := nameLength, replacementSize := replacementSize, name := name,
        replacement := replacement } =
      { numGoals := numGoals_1, symm := symm_1, nameLength := nameLength_1, replacementSize := replacementSize_1,
        name := name_1, replacement := replacement_1 } →
    numGoals = numGoals_1 ∧
      symm = symm_1 ∧
        nameLength = nameLength_1 ∧ replacementSize = replacementSize_1 ∧ name = name_1 ∧ replacement = replacement_1
-- Mathlib.Order.Atoms
/-- Every simple lattice over a partial order is order-isomorphic to `Bool`.  -/
IsSimpleOrder.orderIsoBool : {α : Type u_2} → [DecidableEq α] → [inst : PartialOrder α] → [inst_1 : BoundedOrder α] → [IsSimpleOrder α] → α ≃o Bool
-- Mathlib.Data.Finset.Prod
Finset.subset_product_image_snd : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} [inst : DecidableEq β], Finset.image Prod.snd (s ×ˢ t) ⊆ t
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.hvadd.eq_1 : ∀ {R : Type u_1} {M : Type u_3} {X : Type u_4} [inst : AddMonoid M] {S : AddSubmonoid M}
  [inst_1 : AddOreLocalization.AddOreSet S] [inst_2 : AddAction M X] [inst_3 : VAdd R M] (c : R),
  AddOreLocalization.hvadd c =
    AddOreLocalization.liftExpand
      (fun m s => (AddOreLocalization.oreMin (c +ᵥ 0) s +ᵥ m) -ₒ AddOreLocalization.oreSubtra (c +ᵥ 0) s) ⋯
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
TendstoUniformlyOn.tendsto_intervalIntegral_of_continuousOn : ∀ {ι : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [l.IsCountablyGenerated] {F : ι → ℝ → E}
  [MeasureTheory.IsLocallyFiniteMeasure μ],
  (∀ᶠ (i : ι) in l, ContinuousOn (F i) (Set.uIcc a b)) →
    TendstoUniformlyOn F f l (Set.uIcc a b) →
      Filter.Tendsto (fun n => ∫ (x : ℝ) in a..b, F n x ∂μ) l (nhds (∫ (x : ℝ) in a..b, f x ∂μ))
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.mk_add_mk : ∀ {R : Type u_1} {a b : R} [inst : Add R] (z w : QuadraticAlgebra R a b),
  { re := z.re, im := z.im } + { re := w.re, im := w.im } = { re := z.re + w.re, im := z.im + w.im }
-- Mathlib.Analysis.Complex.HalfPlane
/-- An open upper half-plane is an open set in the complex plane.  -/
Complex.isOpen_im_gt : ∀ (x : ℝ), IsOpen {z | x < z.im}
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.containsThenInsert_fst : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k}, (Std.DTreeMap.Internal.Impl.containsThenInsert k v t ⋯).1 = Std.DTreeMap.Internal.Impl.contains k t
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.ofMatrix_eq_ofMatrixL : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_3} [inst : NonUnitalCStarAlgebra A],
  ⇑CStarMatrix.ofMatrix = ⇑CStarMatrix.ofMatrixL
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.hom_injective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.AddMon C}, Function.Injective CategoryTheory.AddMon.Hom.hom
-- Init.Prelude
instDecidableAnd : {p q : Prop} → [dp : Decidable p] → [dq : Decidable q] → Decidable (p ∧ q)
-- Mathlib.Order.Hom.Lattice
LatticeHom.dual_id : ∀ {α : Type u_2} [inst : Lattice α], LatticeHom.dual (LatticeHom.id α) = LatticeHom.id αᵒᵈ
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.Struct.nsmulFn? : Lean.Meta.Grind.Arith.Linear.Struct → Option Lean.Expr
-- Init.Data.UInt.Lemmas
UInt32.ofFin_add : ∀ (a b : Fin UInt32.size), UInt32.ofFin (a + b) = UInt32.ofFin a + UInt32.ofFin b
-- Mathlib.Order.Atoms
isAtom_compl : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {a : α}, IsAtom aᶜ ↔ IsCoatom a
-- Init.Data.Int.DivMod.Lemmas
Int.ext_ediv_emod_iff : ∀ (n a b : ℤ), a = b ↔ a / n = b / n ∧ a % n = b % n
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_indicator₂ : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {β : Type u_8}
  (f : β → X → E) (s : Set β) (b : β),
  ∫ᵛ (y : X), s.indicator (fun x => f x y) b ∂[B; μ] = s.indicator (fun x => ∫ᵛ (y : X), f x y ∂[B; μ]) b
-- Mathlib.CategoryTheory.Shift.InducedShiftSequence
CategoryTheory.Functor.ShiftSequence.induced.shiftIso_hom_app_obj : ∀ {C : Type u_1} {D : Type u_2} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} A]
  (L : CategoryTheory.Functor C D) (G : CategoryTheory.Functor C A) (M : Type u_4) [inst_3 : AddMonoid M]
  [inst_4 : CategoryTheory.HasShift C M] [inst_5 : G.ShiftSequence M] (F' : M → CategoryTheory.Functor D A)
  (e' : (m : M) → L.comp (F' m) ≅ G.shift m) [inst_6 : ((CategoryTheory.Functor.whiskeringLeft C D A).obj L).Full]
  [inst_7 : ((CategoryTheory.Functor.whiskeringLeft C D A).obj L).Faithful] [inst_8 : CategoryTheory.HasShift D M]
  [inst_9 : L.CommShift M] (n a a' : M) (ha' : n + a = a') (X : C),
  (CategoryTheory.Functor.ShiftSequence.induced.shiftIso L G M F' e' n a a' ha').hom.app (L.obj X) =
    CategoryTheory.CategoryStruct.comp ((F' a).map ((CategoryTheory.Functor.commShiftIso L n).inv.app X))
      (CategoryTheory.CategoryStruct.comp ((e' a).hom.app ((CategoryTheory.shiftFunctor C n).obj X))
        (CategoryTheory.CategoryStruct.comp ((G.shiftIso n a a' ha').hom.app X) ((e' a').inv.app X)))
-- Mathlib.Analysis.InnerProductSpace.Spectrum
/-- A choice of orthonormal basis of eigenvectors for self-adjoint operator `T` on a
finite-dimensional inner product space `E`.  Eigenvectors are sorted in decreasing
order of their eigenvalues.  -/
LinearMap.IsSymmetric.eigenvectorBasis : {𝕜 : Type u_3} →
  [inst : RCLike 𝕜] →
    {E : Type u_4} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] →
          {T : E →ₗ[𝕜] E} →
            [FiniteDimensional 𝕜 E] → {n : ℕ} → T.IsSymmetric → Module.finrank 𝕜 E = n → OrthonormalBasis (Fin n) 𝕜 E
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.comp_id : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β] (f : α →*o β), f.comp (OrderMonoidHom.id α) = f
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Basic
/-- The continuous cohomology of a continuous representation defined by taking homology
of the homogeneous cochains.  -/
continuousCohomology : {k : Type u_1} →
  {G : Type u_2} →
    [inst : Ring k] →
      [inst_1 : Group G] →
        [inst_2 : TopologicalSpace k] →
          [inst_3 : TopologicalSpace G] → [IsTopologicalGroup G] → ℕ → TopRep k G → TopModuleCat k
-- Mathlib.Condensed.Discrete.LocallyConstant
/-- The functor from sets to condensed sets given by locally constant maps into the set.  -/
CondensedSet.LocallyConstant.functor : CategoryTheory.Functor (Type (u + 1)) CondensedSet
-- Mathlib.LinearAlgebra.Dimension.RankNullity
Submodule.rank_add_le_rank_add_rank : ∀ {R : Type u_1} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [HasRankNullity.{u, u_1} R] (s t : Submodule R M), Module.rank R ↥(s ⊔ t) ≤ Module.rank R ↥s + Module.rank R ↥t
-- Lean.Meta.Sym.LitValues
Lean.Meta.Sym.FinValue.mk.injEq : ∀ (n : ℕ) (val : Fin n) (n_1 : ℕ) (val_1 : Fin n_1),
  ({ n := n, val := val } = { n := n_1, val := val_1 }) = (n = n_1 ∧ val ≍ val_1)
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.coe_zero : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β], ⇑0 = 0
-- Mathlib.Analysis.Convolution
MeasureTheory.ConvolutionExistsAt.eq_1 : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] [inst_3 : NontriviallyNormedField 𝕜]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F] [inst_7 : MeasurableSpace G]
  [inst_8 : Sub G] (f : G → E) (g : G → E') (x : G) (L : E →L[𝕜] E' →L[𝕜] F) (μ : MeasureTheory.Measure G),
  MeasureTheory.ConvolutionExistsAt f g x L μ = MeasureTheory.Integrable (fun t => (L (f t)) (g (x - t))) μ
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.instMonoidalCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → CategoryTheory.MonoidalCategory (CategoryTheory.AddGrp C)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.isoMk₃_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 3}
  (app₀ : f.obj' 0 _proof_297✝ ≅ g.obj' 0 _proof_297✝) (app₁ : f.obj' 1 _proof_298✝ ≅ g.obj' 1 _proof_298✝)
  (app₂ : f.obj' 2 _proof_299✝ ≅ g.obj' 2 _proof_299✝) (app₃ : f.obj' 3 _proof_300✝ ≅ g.obj' 3 _proof_300✝)
  (w₀ :
    CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_298✝)
        app₁.hom =
      CategoryTheory.CategoryStruct.comp app₀.hom
        (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_298✝))
  (w₁ :
    CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_299✝) app₂.hom =
      CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 _proof_246✝ _proof_299✝))
  (w₂ :
    CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_299✝ _proof_300✝) app₃.hom =
      CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 _proof_299✝ _proof_300✝)),
  (CategoryTheory.ComposableArrows.isoMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).inv =
    CategoryTheory.ComposableArrows.homMk₃ app₀.inv app₁.inv app₂.inv app₃.inv ⋯ ⋯ ⋯
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.instUniqueOfIsEmpty : {α : Type u_2} → [inst : BooleanAlgebra α] → [IsEmpty α] → Unique (BooleanSubalgebra α)
-- Mathlib.Algebra.Polynomial.Module.AEval
Module.AEval'.X_pow_smul_of : ∀ {R : Type u_2} {M : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (φ : M →ₗ[R] M)
  (m : M) (n : ℕ), Polynomial.X ^ n • (Module.AEval'.of φ) m = (Module.AEval'.of φ) (φ ^ n • m)
-- Mathlib.Algebra.BigOperators.Group.Finset.Sigma
/-- An uncurried version of `Finset.prod_product_right`.  -/
Finset.prod_product_right' : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : CommMonoid β] (s : Finset γ) (t : Finset α) (f : γ → α → β),
  ∏ x ∈ s ×ˢ t, f x.1 x.2 = ∏ y ∈ t, ∏ x ∈ s, f x y
-- Mathlib.Logic.Function.Basic
Function.Injective.surjective_comp_right' : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β},
  Function.Injective f → ∀ (g₀ : β → γ), Function.Surjective fun g => g ∘ f
-- Mathlib.Order.ModularLattice
eq_of_le_of_inf_le_of_le_sup : ∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α] {x y z : α}, x ≤ y → y ⊓ z ≤ x → y ≤ x ⊔ z → x = y
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.entails_2 : ∀ {σ₁ σ₂ : Type u_1} {P Q : Std.Do.SPred [σ₁, σ₂]}, P ⊢ₛ Q ↔ ∀ (s₁ : σ₁) (s₂ : σ₂), (P s₁ s₂).down → (Q s₁ s₂).down
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_eq_some_iff_exists_beq_and_mem_toArray : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {v : β}, m[k]? = some v ↔ ∃ k', (k == k') = true ∧ (k', v) ∈ m.toArray
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.le_pullback_bind : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (S : CategoryTheory.Presieve X)
  (R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → CategoryTheory.Sieve Y) (f : Y ⟶ X) (h : S f),
  R h ≤ CategoryTheory.Sieve.pullback f (CategoryTheory.Sieve.bind S R)
-- Mathlib.Algebra.Group.Hom.Defs
/-- `M →ₙ* N` is the type of functions `M → N` that preserve multiplication. The `ₙ` in the notation
stands for "non-unital" because it is intended to match the notation for `NonUnitalAlgHom` and
`NonUnitalRingHom`, so a `MulHom` is a non-unital monoid hom.

When possible, instead of parametrizing results over `(f : M →ₙ* N)`,
you should parametrize over `(F : Type*) [MulHomClass F M N] (f : F)`.
When you extend this structure, make sure to extend `MulHomClass`.
 -/
MulHom : (M : Type u_10) → (N : Type u_11) → [Mul M] → [Mul N] → Type (max u_10 u_11)
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.term_ord_aux : ∀ {I : Type u} [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {i : I}
  (ho : Profinite.NobelingProof.ord I i < Ordinal.type fun x1 x2 => x1 < x2), Profinite.NobelingProof.term I ho = i
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.map_apply : ∀ {n : ℕ} (d : ℕ) (a : Fin n → ℕ), (Behrend.map d) a = ∑ i, a i * d ^ ↑i
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.ofHom_id : ∀ {R : Type u} [inst : CommRing R] {X : Type v} [inst_1 : CommRing X] [inst_2 : Algebra R X],
  CommAlgCat.ofHom (AlgHom.id R X) = CategoryTheory.CategoryStruct.id (CommAlgCat.of R X)
-- Mathlib.Algebra.GroupWithZero.Basic
eq_of_zero_eq_one : ∀ {M₀ : Type u_1} [inst : MulZeroOneClass M₀], 0 = 1 → ∀ (a b : M₀), a = b