mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.Extrema
/-- A local maximum of a concave function is a global maximum, restricted to a set `s`.  -/
IsMaxOn.of_isLocalMaxOn_of_concaveOn : ∀ {E : Type u_1} {β : Type u_2} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : Module ℝ E]
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [inst_5 : AddCommGroup β] [inst_6 : PartialOrder β]
  [IsOrderedAddMonoid β] [inst_8 : Module ℝ β] [IsOrderedModule ℝ β] [PosSMulReflectLE ℝ β] {s : Set E} {f : E → β}
  {a : E}, a ∈ s → IsLocalMaxOn f s a → ConcaveOn ℝ s f → IsMaxOn f s a
-- Mathlib.MeasureTheory.Measure.DiracProba
/-- The composition of `diracProbaEquiv.symm` and `diracProba` is the subtype inclusion.  -/
MeasureTheory.diracProba_comp_diracProbaEquiv_symm_eq_val : ∀ {X : Type u_1} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : OpensMeasurableSpace X]
  [inst_3 : T0Space X], MeasureTheory.diracProba ∘ ⇑MeasureTheory.diracProbaEquiv.symm = fun μ => ↑μ
-- Mathlib.Data.Set.Function
Set.InjOn.congr : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β}, Set.InjOn f₁ s → Set.EqOn f₁ f₂ s → Set.InjOn f₂ s
-- Mathlib.Algebra.Module.GradedModule
DirectSum.GdistribMulAction.mk : {ιA : Type u_1} →
  {ιB : Type u_2} →
    {A : ιA → Type u_3} →
      {M : ιB → Type u_4} →
        [inst : AddMonoid ιA] →
          [inst_1 : VAdd ιA ιB] →
            [inst_2 : GradedMonoid.GMonoid A] →
              [inst_3 : (i : ιB) → AddMonoid (M i)] →
                [toGMulAction : GradedMonoid.GMulAction A M] →
                  (∀ {i : ιA} {j : ιB} (a : A i) (b c : M j),
                      GradedMonoid.GSMul.smul a (b + c) = GradedMonoid.GSMul.smul a b + GradedMonoid.GSMul.smul a c) →
                    (∀ {i : ιA} {j : ιB} (a : A i), GradedMonoid.GSMul.smul a 0 = 0) → DirectSum.GdistribMulAction A M
-- Mathlib.Algebra.Polynomial.BigOperators
Polynomial.coeff_multiset_prod_of_natDegree_le : ∀ {R : Type u} [inst : CommSemiring R] (t : Multiset (Polynomial R)) (n : ℕ),
  (∀ p ∈ t, p.natDegree ≤ n) → t.prod.coeff (t.card * n) = (Multiset.map (fun p => p.coeff n) t).prod
-- Mathlib.Tactic.ClickSuggestions.Rewrite
Mathlib.Tactic.ClickSuggestions.instInhabitedRwKey.default : Mathlib.Tactic.ClickSuggestions.RwKey
-- Init.Data.BitVec.Lemmas
BitVec.ushiftRight_zero : ∀ {w : ℕ} (x : BitVec w), x >>> 0 = x
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorZero_inv_app_shift : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddCommMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] {X : C} (n : A),
  (CategoryTheory.shiftFunctorZero C A).inv.app ((CategoryTheory.shiftFunctor C n).obj X) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctorZero C A).inv.app X))
      ((CategoryTheory.shiftFunctorComm C n 0).inv.app X)
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- A category `C` which has products is said to have `AB4Star` (in literature AB4\*)
provided that products are exact.  -/
CategoryTheory.AB4Star : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Limits.HasProducts C] → Prop
-- Mathlib.Algebra.Order.Ring.Abs
abs_lt_iff_mul_self_lt : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α}, |a| < |b| ↔ a * a < b * b
-- Init.Data.List.MinMaxIdx
_private.Init.Data.List.MinMaxIdx.0.List.minIdxOn.go_lt_length_add : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {x : α} {i j : ℕ} {xs : List α},
  i < j → List.minIdxOn.go✝ f x i j xs < xs.length + j
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.pow_logSizeRadius_le_card_le_logSizeRadius : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {V : Finset T} {t : T},
  1 < a →
    t ∈ V →
      a ^ (PairReduction.logSizeRadius t V a c - 1) ≤
        ↑{x ∈ V | edist t x ≤ (↑(PairReduction.logSizeRadius t V a c) - 1) * c}.card
-- Lean.Elab.Tactic.Induction
Lean.Elab.Tactic.ElimApp.Alt.mk.inj : ∀ {name : Lean.Name} {info : Lean.Meta.ElimAltInfo} {mvarId : Lean.MVarId} {name_1 : Lean.Name}
  {info_1 : Lean.Meta.ElimAltInfo} {mvarId_1 : Lean.MVarId},
  { name := name, info := info, mvarId := mvarId } = { name := name_1, info := info_1, mvarId := mvarId_1 } →
    name = name_1 ∧ info = info_1 ∧ mvarId = mvarId_1
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepSets_precomp_of_bijective : ∀ {Ω : Type u_1} {ι : Type u_2} {π : ι → Set (Set Ω)} {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  {ι' : Type u_6} {g : ι' → ι},
  Function.Bijective g → (ProbabilityTheory.iIndepSets (π ∘ g) μ ↔ ProbabilityTheory.iIndepSets π μ)
-- Mathlib.Algebra.Algebra.Spectrum.Basic
AlgHom.mem_resolventSet_apply : ∀ {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Ring A]
  [inst_2 : Algebra R A] [inst_3 : Ring B] [inst_4 : Algebra R B] [inst_5 : FunLike F A B] [AlgHomClass F R A B] (φ : F)
  {a : A} {r : R}, r ∈ resolventSet R a → r ∈ resolventSet R (φ a)
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.tensorCotangentEquiv_symm_apply : ∀ {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) (i : σ),
  (Algebra.Generators.PresentationOfFreeCotangent.Aux.tensorCotangentEquiv✝ D).symm (b i) =
    1 ⊗ₜ[Algebra.Generators.PresentationOfFreeCotangent.Aux.T✝ D]
      Algebra.Extension.Cotangent.mk (Algebra.Generators.PresentationOfFreeCotangent.Aux.kerGen✝ D i)
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.emptySC : ShareCommon.State Lean.ShareCommon.objectFactory
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
CovariantDerivative.ContMDiffCovariantDerivative.mk : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)]
  [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] [inst_14 : FiberBundle F V] [inst_15 : IsManifold I 1 M]
  [inst_16 : VectorBundle 𝕜 F V] {cov : CovariantDerivative I F V} {k : WithTop ℕ∞},
  ContMDiffCovariantDerivativeOn F k (↑cov) Set.univ → cov.ContMDiffCovariantDerivative k
-- Mathlib.AlgebraicGeometry.ColimitsOver
/-- (Implementation) Cocone for transition map for construction of
`AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor`.  -/
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  [inst : P.IsStableUnderBaseChange] →
    [inst_1 : P.IsMultiplicative] →
      {S : AlgebraicGeometry.Scheme} →
        {J : Type u_1} →
          [inst_2 : CategoryTheory.Category.{v_1, u_1} J] →
            {D : CategoryTheory.Functor J (P.Over ⊤ S)} →
              {𝒰 : S.OpenCover} →
                [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] →
                  [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] →
                    (d : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰) →
                      {i j : 𝒰.I₀} →
                        (hij : i ⟶ j) →
                          CategoryTheory.Limits.Cocone
                            (D.comp
                              ((CategoryTheory.MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).comp
                                (CategoryTheory.MorphismProperty.Over.map ⊤ ⋯)))
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
StarAlgebra.elemental.bijective_characterSpaceToSpectrum : ∀ {A : Type u_1} [inst : CStarAlgebra A] (a : A) [IsStarNormal a],
  Function.Bijective (StarAlgebra.elemental.characterSpaceToSpectrum a)
-- Mathlib.RingTheory.Multiplicity
multiplicity_of_isUnit_right : ∀ {α : Type u_1} [inst : CommMonoid α] {a b : α}, ¬IsUnit a → IsUnit b → multiplicity a b = 0
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g}
  {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf)
  (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt}
  (fac :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) =
      CategoryTheory.CategoryStruct.comp π ι)
  [inst_2 : CategoryTheory.Epi π] [inst_3 : CategoryTheory.Mono ι],
  (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData S hkf hcc fac).ι = ι
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mapNatIso_inverse_obj_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T T' : CategoryTheory.Functor C D} (i : T ≅ T')
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) T'),
  ((CategoryTheory.StructuredArrow.mapNatIso i).inverse.obj X).left = X.left
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_insert : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k a : α}
  {fallback : β a} {v : β k},
  (m.insert k v).getD a fallback = if h : (k == a) = true then cast ⋯ v else m.getD a fallback
-- Mathlib.Data.ENNReal.Inv
ENNReal.exists_nat_pos_mul_gt : ∀ {a b : ENNReal}, a ≠ 0 → b ≠ ⊤ → ∃ n > 0, b < ↑n * a
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Complex
RCLike.measurableSpace : {𝕜 : Type u_1} → [RCLike 𝕜] → MeasurableSpace 𝕜
-- Mathlib.Data.Fin.Basic
Fin.eq_one_of_ne_zero : ∀ (i : Fin 2), i ≠ 0 → i = 1
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.functorToRepresentables_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁)))
  (X : P.Elementsᵒᵖ),
  (CategoryTheory.Presheaf.functorToRepresentables P).obj X =
    CategoryTheory.uliftYoneda.{w, v₁, u₁}.obj (Opposite.unop (Opposite.unop X).fst)
-- Std.Do.WP.SimpLemmas
Std.Do.WP.read_ReaderT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ρ : Type u} {Q : Std.Do.PostCond ρ (Std.Do.PostShape.arg ρ ps)}
  [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps], (Std.Do.wp MonadReaderOf.read).apply Q = fun r => Q.1 r r
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_val_Ioo : ∀ {n : ℕ} (a b : Fin n), Finset.image Fin.val (Finset.Ioo a b) = Finset.Ioo ↑a ↑b
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.forM_eq_forM_toArray : ∀ {α : Type u} {m' : Type w → Type w'} {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [inst : Monad m']
  [LawfulMonad m'] {f : α → β → m' PUnit.{w + 1}},
  Std.DHashMap.Raw.forM f ↑m = Array.forM (fun a => f a.1 a.2) (Std.DHashMap.Raw.Const.toArray ↑m)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.eq_add_pi_of_two_zsmul_eq_of_sign_eq_neg : ∀ (a b : Real.Angle), 2 • a = 2 • b → a.sign = -b.sign → b.sign ≠ 0 → a = b + ↑Real.pi
-- Lean.Widget.InteractiveDiagnostic
/-- Nested text is ignored.  -/
_private.Lean.Widget.InteractiveDiagnostic.0.Lean.Widget.EmbedFmt.goal : Lean.Elab.ContextInfo → Lean.LocalContext → Lean.MVarId → Lean.Widget.EmbedFmt✝
-- Lean.Meta.CollectMVars
/-- Auxiliary definition for `getMVarDependencies`.  -/
_private.Lean.Meta.CollectMVars.0.addMVars : Lean.Expr → optParam Bool false → StateRefT' IO.RealWorld (Std.HashSet Lean.MVarId) Lean.MetaM Unit
-- Init.Data.List.MinMax
List.max?_eq_some_max : ∀ {α : Type u_1} [inst : Max α] {l : List α} (hl : l ≠ []), l.max? = some (l.max hl)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.isIso_subschemeι_iff_eq_bot : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData), CategoryTheory.IsIso I.subschemeι ↔ I = ⊥
-- Init.Data.Iterators.Combinators.Monadic.ULift
_private.Init.Data.Iterators.Combinators.Monadic.ULift.0.Std.Iterators.Types.ULiftIterator.instFinitenessRelation : {α : Type u} →
  {m : Type u → Type u'} →
    {n : Type (max u v) → Type v'} →
      {β : Type u} →
        {lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ} →
          [inst : Std.Iterator α m β] →
            [Std.Iterators.Finite α m] →
              [inst_2 : Monad n] → Std.Iterators.FinitenessRelation (Std.Iterators.Types.ULiftIterator α m n β lift) n
-- Init.Grind.Ring.Basic
Lean.Grind.Semiring.ofNat_add : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (a b : ℕ), OfNat.ofNat (a + b) = OfNat.ofNat a + OfNat.ofNat b
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.le_sup_lintegral : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f g : MeasureTheory.SimpleFunc α ENNReal),
  max (f.lintegral μ) (g.lintegral μ) ≤ (f ⊔ g).lintegral μ
-- Lean.LibrarySuggestions.SymbolFrequency
_private.Lean.LibrarySuggestions.SymbolFrequency.0.Lean.LibrarySuggestions.symbolFrequencyExt.unsafe_3 : Lean.Environment → Lean.OLeanEntries (Array (Lean.NameMap ℕ))
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.instMonoFDKernelSequence : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₂₃ : i₁ ⟶ i₃)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ n₃ : ℤ) (x : n₀ + 1 = n₁) (x_1 : n₁ + 1 = n₂)
  (x_2 : n₂ + 1 = n₃), CategoryTheory.Mono (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ x x_1 x_2).f
-- Mathlib.Algebra.NeZero
one_ne_zero' : ∀ (α : Type u_2) [inst : Zero α] [inst_1 : One α] [NeZero 1], 1 ≠ 0
-- Aesop.Frontend.Extension.Init
/-- An environment extension containing an Aesop rule set. Each rule set has its
own extension.
 -/
Aesop.RuleSetExtension : Type
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.SurjectiveOfEpiAuxs.one_smul : ∀ {A B : GrpCat} (f : A ⟶ B) (x : GrpCat.SurjectiveOfEpiAuxs.XWithInfinity f), 1 • x = x
-- Mathlib.Geometry.Euclidean.MongePoint
/-- The position of the orthocenter in relation to the circumcenter
and centroid.  -/
Affine.Triangle.orthocenter_eq_smul_vsub_vadd_circumcenter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P),
  t.orthocenter =
    3 • (Finset.centroid ℝ Finset.univ t.points -ᵥ Affine.Simplex.circumcenter t) +ᵥ Affine.Simplex.circumcenter t
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Enriched.Functor.associator_hom_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (K L M N : CategoryTheory.Functor C D) {X : C}
  (x :
    (CategoryTheory.MonoidalCategoryStruct.tensorObj
          (CategoryTheory.MonoidalCategoryStruct.tensorObj (K.functorHom L) (L.functorHom M)) (M.functorHom N)).obj
      X),
  (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.MonoidalCategoryStruct.associator
            ((K.homObjFunctor L).obj (Opposite.op (CategoryTheory.coyoneda.obj (Opposite.op X))))
            ((L.homObjFunctor M).obj (Opposite.op (CategoryTheory.coyoneda.obj (Opposite.op X))))
            ((M.homObjFunctor N).obj (Opposite.op (CategoryTheory.coyoneda.obj (Opposite.op X))))).hom)
      x =
    (x.1.1, x.1.2, x.2)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- A matrix representation of a quadratic form `Q : QuadraticForm R (n → R)`.
See also `QuadraticForm.toMatrix` which gives the matrix in a given basis of a quadratic form on
an abstract vector space.  -/
QuadraticForm.toMatrix' : {R : Type u_3} →
  {n : Type w} →
    [Fintype n] → [DecidableEq n] → [inst : CommRing R] → [Invertible 2] → QuadraticForm R (n → R) → Matrix n n R
-- Init.Data.BitVec.Lemmas
/-- Non-overflowing signed division bounds when numerator is nonpos, denominator is less than -1.  -/
BitVec.toInt_ediv_toInt_lt_of_nonpos_of_lt_neg_one : ∀ {w : ℕ} {x y : BitVec w}, x.toInt ≤ 0 → y.toInt < -1 → x.toInt / y.toInt < 2 ^ (w - 1)
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
/-- The symplectic complement of a standard subspace, bundled as a `StandardSubspace`.  -/
StandardSubspace.symplComp : {H : Type u_1} →
  [inst : NormedAddCommGroup H] →
    [inst_1 : InnerProductSpace ℂ H] → [CompleteSpace H] → StandardSubspace H → StandardSubspace H
-- Init.Prelude
/-- Constructs a `Max` instance from a decidable `≤` operation.
 -/
maxOfLe : {α : Type u_1} → [inst : LE α] → [DecidableRel LE.le] → Max α
-- Lean.EnvExtension
Lean.TagDeclarationExtension.instInhabited : Inhabited Lean.TagDeclarationExtension
-- Mathlib.Data.Finsupp.Defs
Finsupp.mk : {α : Type u_9} →
  {M : Type u_10} →
    [inst : Zero M] → (support : Finset α) → (toFun : α → M) → (∀ (a : α), a ∈ support ↔ toFun a ≠ 0) → α →₀ M
-- Mathlib.GroupTheory.FreeAbelianGroup
instUniqueFreeAbelianGroupOfIsEmpty : (α : Type u) → [IsEmpty α] → Unique (FreeAbelianGroup α)
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Comma.hasColimitsOfShape : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {A : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  {B : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃}
  [inst_3 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
  [CategoryTheory.Limits.HasColimitsOfShape J A] [CategoryTheory.Limits.HasColimitsOfShape J B]
  [CategoryTheory.Limits.PreservesColimitsOfShape J L],
  CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.Comma L R)
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- Intermediate stage of assembling the unit.  -/
CategoryTheory.OverPresheafAux.unitAuxAux : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      (η : F ⟶ A) →
        CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf A
            (CategoryTheory.OverPresheafAux.restrictedYonedaObj η) ≅
          F
-- Aesop.Tree.Data
Aesop.instBEqNodeState.beq : Aesop.NodeState → Aesop.NodeState → Bool
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.ofAlgebraAut.eq_1 : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  Rep.ofAlgebraAut R S = Rep.ofDistribMulAction ℤ (S ≃ₐ[R] S) S
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
CategoryTheory.Functor.IsStronglyCocartesian.fac : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsStronglyCocartesian f φ]
  {S' : 𝒮} {b' : 𝒳} {g : S ⟶ S'} {f' : R ⟶ S'} (hf' : f' = CategoryTheory.CategoryStruct.comp f g) (φ' : a ⟶ b')
  [inst_3 : p.IsHomLift f' φ'],
  CategoryTheory.CategoryStruct.comp φ (CategoryTheory.Functor.IsStronglyCocartesian.map p f φ hf' φ') = φ'
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- The left action on objects. This is denoted `c ⊙ₗ d`.  -/
CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj : {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} →
        {inst_2 : CategoryTheory.MonoidalCategoryStruct C} →
          [self : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct C D] → C → D → D
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
OrderIso.map_csInf : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] [inst_1 : ConditionallyCompleteLattice β]
  (e : α ≃o β) {s : Set α}, s.Nonempty → BddBelow s → e (sInf s) = ⨅ x, e ↑x
-- Init.Data.Array.MapIdx
Array.exists_of_mem_mapFinIdx : ∀ {β : Type u_1} {α : Type u_2} {b : β} {xs : Array α} {f : (i : ℕ) → α → i < xs.size → β},
  b ∈ xs.mapFinIdx f → ∃ i, ∃ (h : i < xs.size), f i xs[i] h = b
-- Std.Data.HashMap.Basic
/-- Returns `true` if there is a mapping for the given key. There is also a `Prop`-valued version
of this: `a ∈ m` is equivalent to `m.contains a = true`.

Observe that this is different behavior than for lists: for lists, `∈` uses `=` and `contains` uses
`==` for comparisons, while for hash maps, both use `==`.
 -/
Std.HashMap.contains : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → α → Bool
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_updateCol_smul_left : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (M : Matrix n n R)
  (j : n) (s : R) (u : n → R), ((s • M).updateCol j u).det = s ^ (Fintype.card n - 1) * (M.updateCol j u).det
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- **Alias** of the reverse direction of `SimpleGraph.isContained_congr_right`. -/
SimpleGraph.IsContained.congr_right : ∀ {α : Type u_4} {β : Type u_5} {γ : Type u_6} {A : SimpleGraph α} {B : SimpleGraph β} {C : SimpleGraph γ}
  (e₂ : B ≃g C), A.IsContained C → A.IsContained B
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.toFiberBundleCore_indexAt : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι),
  Z.toFiberBundleCore.indexAt = Z.indexAt
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
addLeftReflectLT_of_addLeftMono : ∀ (N : Type u_2) [inst : Add N] [inst_1 : LinearOrder N] [AddLeftMono N], AddLeftReflectLT N
-- Mathlib.Tactic.Algebraize
Mathlib.Tactic.Algebraize.instInhabitedConfig : Inhabited Mathlib.Tactic.Algebraize.Config
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonProgressParams : {α : Type} → [Lean.ToJson α] → Lean.ToJson (Lean.Lsp.ProgressParams α)
-- Mathlib.Topology.Separation.SeparatedNhds
SeparatedNhds.disjoint : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, SeparatedNhds s t → Disjoint s t
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.finite.congr_simp : ∀ (sign sign_1 : Float.Model.UnpackedFloat.Sign),
  sign = sign_1 →
    ∀ (mantissa mantissa_1 : ℕ) (e_mantissa : mantissa = mantissa_1) (exponent exponent_1 : ℤ),
      exponent = exponent_1 →
        ∀ (mantissa_pos : 0 < mantissa),
          Float.Model.UnpackedFloat.finite sign mantissa exponent mantissa_pos =
            Float.Model.UnpackedFloat.finite sign_1 mantissa_1 exponent_1 ⋯
-- Mathlib.CategoryTheory.Bicategory.Opposites
/-- A 2-isomorphism in `Bᵒᵖ` gives a 2-isomorphism in `B`  -/
CategoryTheory.Iso.unop2_op : {B : Type u} → [inst : CategoryTheory.Bicategory B] → {a b : B} → {f g : a ⟶ b} → (f.op ≅ g.op) → (f ≅ g)
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
lt_or_lt_of_mul_lt_mul : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Mul α] [MulLeftMono α] [MulRightMono α] {a₁ a₂ b₁ b₂ : α},
  a₁ * b₁ < a₂ * b₂ → a₁ < a₂ ∨ b₁ < b₂
-- Init.Data.Range.Polymorphic.UInt
UInt64.instLawfulUpwardEnumerableLeast? : Std.PRange.LawfulUpwardEnumerableLeast? UInt64
-- Mathlib.Order.Hom.Lattice
InfHom.mk.injEq : ∀ {α : Type u_6} {β : Type u_7} [inst : Min α] [inst_1 : Min β] (toFun : α → β)
  (map_inf' : ∀ (a b : α), toFun (a ⊓ b) = toFun a ⊓ toFun b) (toFun_1 : α → β)
  (map_inf'_1 : ∀ (a b : α), toFun_1 (a ⊓ b) = toFun_1 a ⊓ toFun_1 b),
  ({ toFun := toFun, map_inf' := map_inf' } = { toFun := toFun_1, map_inf' := map_inf'_1 }) = (toFun = toFun_1)
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.instTop.eq_1 : ∀ {α : Type u} [inst : Group α],
  GroupTopology.instTop = { top := { toTopologicalSpace := ⊤, toIsTopologicalGroup := ⋯ } }