mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
/-- The short complex of the `r`th page of the spectral sequence on position `pq'`
identifies to the short complex given by the differentials of the spectral object.
Then, the homology of this short complex can be computed using
`SpectralSequence.dHomologyIso`.
(This only applies in the favourable case when there are `pq` and `pq''` such
that `(c r).Rel pq pq'` and `(c r).Rel pq' pq''` hold.)  -/
CategoryTheory.Abelian.SpectralObject.SpectralSequence.shortComplexIso : {C : Type u_1} →
  {ι : Type u_2} →
    {κ : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Abelian C] →
          [inst_2 : Preorder ι] →
            (X : CategoryTheory.Abelian.SpectralObject C ι) →
              {c : ℤ → ComplexShape κ} →
                {r₀ : ℤ} →
                  (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) →
                    (r : ℤ) →
                      (hr : r₀ ≤ r) →
                        (pq pq' pq'' : κ) →
                          (hpq : (c r).Rel pq pq') →
                            (hpq' : (c r).Rel pq' pq'') →
                              (n₀ n₁ n₂ n₃ n₄ : ℤ) →
                                (hn₁ : n₀ + 1 = n₁) →
                                  (hn₂ : n₁ + 1 = n₂) →
                                    (hn₃ : n₂ + 1 = n₃) →
                                      (hn₄ : n₃ + 1 = n₄) →
                                        n₂ = data.deg pq' →
                                          ((CategoryTheory.Abelian.SpectralObject.SpectralSequence.page X data r hr).sc'
                                              pq pq' pq'' ≅
                                            X.dShortComplex (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯)
                                              (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯)
                                              (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯)
                                              (CategoryTheory.homOfLE ⋯) n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄)
-- Mathlib.RingTheory.FreeRing
FreeRing.of_ne_zero : ∀ {α : Type u} (x : α), FreeRing.of x ≠ 0
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.Const.alterₘ.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.leftUnitor.eq_1 : ∀ {R : Type u} [inst : CommSemiring R] (M : SemimoduleCat R),
  SemimoduleCat.MonoidalCategory.leftUnitor M = (TensorProduct.lid R ↑M).toModuleIsoₛ
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.ground_subset_closure_iff : ∀ {α : Type u_2} {M : Matroid α} {X : Set α}, M.E ⊆ M.closure X ↔ M.closure X = M.E
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.isSeparated_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.IsSeparated f ↔
    autoParam (AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.pullback.diagonal f))
      AlgebraicGeometry.IsSeparated.isClosedImmersion_diagonal._autoParam
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
/-- The preimage of a separable set by an inducing map is separable.  -/
Topology.IsInducing.isSeparable_preimage : ∀ {β : Type v} {α : Type u_2} [inst : TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α] {f : β → α}
  [inst_2 : TopologicalSpace β],
  Topology.IsInducing f → ∀ {s : Set α}, TopologicalSpace.IsSeparable s → TopologicalSpace.IsSeparable (f ⁻¹' s)
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.outerMeasure_pos_of_is_add_left_invariant : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] [inst_2 : AddGroup G]
  [inst_3 : IsTopologicalAddGroup G],
  (∀ (g : G) {K : TopologicalSpace.Compacts G}, μ (TopologicalSpace.Compacts.map (fun x => g + x) ⋯ K) = μ K) →
    ∀ (K : TopologicalSpace.Compacts G), μ K ≠ 0 → ∀ {U : Set G}, IsOpen U → U.Nonempty → 0 < μ.outerMeasure U
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- If `f` is meromorphic in normal form, then so is its inverse.
 -/
MeromorphicNFAt.inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {f : 𝕜 → 𝕜}, MeromorphicNFAt f x → MeromorphicNFAt f⁻¹ x
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- We can get the usual Sylvester matrix of `f` and `f.derivative` back from the modified one
by multiplying the last row by the leading coefficient of `f`.  -/
Polynomial.sylvesterDeriv_updateRow : ∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R) (hf : 0 < f.natDegree),
  f.sylvesterDeriv.updateRow ⟨2 * f.natDegree - 2, ⋯⟩ (f.leadingCoeff • f.sylvesterDeriv ⟨2 * f.natDegree - 2, ⋯⟩) =
    (Polynomial.derivative f).sylvester f (f.natDegree - 1) f.natDegree
-- Mathlib.Geometry.Manifold.Immersion
/-- `f : M → N` is a `C^n` immersion if around each point `x ∈ M`,
there are charts `φ` and `ψ` of `M` and `N` around `x` and `f x`, respectively
such that in these charts, `f` looks like `u ↦ (u, 0)`.

Implicit in this definition is an abstract choice `F` of a complement of `E` in `E'`:
being an immersion includes a choice of linear isomorphism between `E × F` and `E'`, which is where
the choice of `F` enters. If you need stronger control over the complement `F`,
use `IsImmersionOfComplement` instead.

Note that our global choice of complement is a bit stronger than asking `f` to be an immersion at
each `x ∈ M` w.r.t. potentially varying complements: see `isImmersionAt` for details.
 -/
Manifold.IsImmersion : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      {E'' : Type u} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup E''] →
              [inst_4 : NormedSpace 𝕜 E''] →
                {H : Type u_7} →
                  [inst_5 : TopologicalSpace H] →
                    {G : Type u_9} →
                      [inst_6 : TopologicalSpace G] →
                        ModelWithCorners 𝕜 E H →
                          ModelWithCorners 𝕜 E'' G →
                            {M : Type u_11} →
                              [inst : TopologicalSpace M] →
                                [ChartedSpace H M] →
                                  {N : Type u_13} →
                                    [inst : TopologicalSpace N] → [ChartedSpace G N] → WithTop ℕ∞ → (M → N) → Prop
-- Mathlib.CategoryTheory.ShrinkYoneda
/-- `shrinkYoneda.obj X` is represented by `X`.  -/
CategoryTheory.shrinkYonedaRepresentableBy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
      (X : C) → (CategoryTheory.shrinkYoneda.{w, v, u}.obj X).RepresentableBy X
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.swap.inj : ∀ {c c_1 : Lean.Meta.Grind.AC.EqCnstr},
  Lean.Meta.Grind.AC.EqCnstrProof.swap c = Lean.Meta.Grind.AC.EqCnstrProof.swap c_1 → c = c_1
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.functorEquiv_unitIso_inv_app_app_inr : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {A' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] {B : Type u} [inst_2 : CategoryTheory.Category.{v, u} B]
  (X : CategoryTheory.Functor (A ⊕ A') B) (a' : A'),
  ((CategoryTheory.Sum.functorEquiv A A' B).unitIso.inv.app X).app (Sum.inr a') =
    CategoryTheory.CategoryStruct.id (X.obj (Sum.inr a'))
-- Mathlib.Data.Set.Image
Set.disjoint_preimage_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β},
  Function.Surjective f → ∀ {s t : Set β}, Disjoint (f ⁻¹' s) (f ⁻¹' t) ↔ Disjoint s t
-- Mathlib.Data.Set.Lattice
Set.iInter₂_mono : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} {s t : (i : ι) → κ i → Set α},
  (∀ (i : ι) (j : κ i), s i j ⊆ t i j) → ⋂ i, ⋂ j, s i j ⊆ ⋂ i, ⋂ j, t i j
-- Init.System.ST
/-- Reads the value of a mutable reference.
 -/
ST.Ref.get : {σ : Type} → {m : Type → Type} → [MonadLiftT (ST σ) m] → {α : Type} → ST.Ref σ α → m α
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
continuousOn_cfc_setProd_nhdsSet : ∀ {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NormedRing A] [inst_2 : StarRing A]
  [inst_3 : NormedAlgebra 𝕜 A] [inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p] [ContinuousStar A]
  [CompleteSpace A] {s : Set 𝕜},
  ContinuousOn (fun fa => cfc ((UniformOnFun.toFun {s}) fa.1) fa.2)
    ({f | ContinuousOn ((UniformOnFun.toFun {t | IsCompact t ∧ t ⊆ s}) f) s} ×ˢ {a | p a ∧ s ∈ nhdsSet (spectrum 𝕜 a)})
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
/-- The embedding `v.Completion →+* ℂ` has closed image inside `ℂ`.  -/
NumberField.InfinitePlace.Completion.isClosed_image_extensionEmbedding : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K),
  IsClosed (Set.range ⇑(NumberField.InfinitePlace.Completion.extensionEmbedding v))
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.coe_one : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R], ↑1 = 1
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.biUnion_congr_of_le : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I}
  {πi₁ πi₂ : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J},
  π₁ = π₂ → (∀ J ≤ I, πi₁ J = πi₂ J) → π₁.biUnion πi₁ = π₂.biUnion πi₂
-- Mathlib.Algebra.Group.Commute.Defs
Commute.inv : ∀ {G : Type u_1} [inst : DivisionMonoid G] {a b : G}, Commute a b → (a * b)⁻¹ = a⁻¹ * b⁻¹
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.lift₃_p₂_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Full] {A₁ A₂ A₃ : C} {X : D} {f₁ : F.obj A₁ ⟶ X}
  (hf₁ : F.relativelyRepresentable f₁) (f₂ : F.obj A₂ ⟶ X) (f₃ : F.obj A₃ ⟶ X)
  [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)] [inst_4 : F.Faithful] {Z : C} (x₁ : Z ⟶ A₁)
  (x₂ : Z ⟶ A₂) (x₃ : Z ⟶ A₃)
  (h₁₂ : CategoryTheory.CategoryStruct.comp (F.map x₁) f₁ = CategoryTheory.CategoryStruct.comp (F.map x₂) f₂)
  (h₁₃ : CategoryTheory.CategoryStruct.comp (F.map x₁) f₁ = CategoryTheory.CategoryStruct.comp (F.map x₃) f₃) {Z_1 : C}
  (h : A₂ ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (hf₁.lift₃ f₂ f₃ x₁ x₂ x₃ h₁₂ h₁₃)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₂ hf₁ f₂ f₃) h) =
    CategoryTheory.CategoryStruct.comp x₂ h
-- Mathlib.Analysis.Convex.Function
ConcaveOn.comp_convexOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid α] [inst_4 : PartialOrder α] [inst_5 : AddCommMonoid β]
  [inst_6 : PartialOrder β] [inst_7 : SMul 𝕜 E] [inst_8 : SMul 𝕜 α] [inst_9 : SMul 𝕜 β] {s : Set E} {f : E → β}
  {g : β → α}, ConcaveOn 𝕜 (f '' s) g → ConvexOn 𝕜 s f → AntitoneOn g (f '' s) → ConcaveOn 𝕜 s (g ∘ f)
-- Mathlib.Algebra.Module.SpanRank
Submodule.spanRank.eq_1 : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M),
  p.spanRank = ⨅ s, Cardinal.mk ↑↑s
-- ProofWidgets.Component.PenroseDiagram
ProofWidgets.Penrose.DiagramProps.sub : ProofWidgets.Penrose.DiagramProps → String
-- Mathlib.AlgebraicGeometry.Cover.Over
AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_I₀ : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme)
  [inst : P.IsStableUnderBaseChange] [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P]
  {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  (f : W ⟶ X) [inst_2 : W.Over S] [inst_3 : X.Over S] [inst_4 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰]
  [inst_5 : AlgebraicGeometry.Scheme.Hom.IsOver f S] {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  [inst_6 : Q.HasOfPostcompProperty Q] [inst_7 : Q.IsStableUnderBaseChange] [inst_8 : Q.IsStableUnderComposition]
  (hX : Q (X ↘ S)) (hW : Q (W ↘ S)) (hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)),
  (AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp' S 𝒰 f hX hW hQ).I₀ = 𝒰.I₀
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.norm.injEq : ∀ (c₁ : Lean.Meta.Grind.Arith.Linear.IneqCnstr) (k : ℕ) (c₁_1 : Lean.Meta.Grind.Arith.Linear.IneqCnstr) (k_1 : ℕ),
  (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.norm c₁ k = Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.norm c₁_1 k_1) =
    (c₁ = c₁_1 ∧ k = k_1)
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- The Law of Quadratic Reciprocity for the Jacobi symbol  -/
jacobiSym.quadratic_reciprocity : ∀ {a b : ℕ}, Odd a → Odd b → jacobiSym (↑a) b = (-1) ^ (a / 2 * (b / 2)) * jacobiSym (↑b) a
-- Mathlib.ModelTheory.Order
/-- The order structure on an ordered language is decidable.  -/
FirstOrder.Language.decidableLEOfStructure : (L : FirstOrder.Language) →
  (M : Type w') →
    [inst : L.IsOrdered] →
      [inst_1 : L.Structure M] →
        [h : DecidableRel fun a b => FirstOrder.Language.Structure.RelMap FirstOrder.Language.leSymb ![a, b]] →
          DecidableLE M
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.maxEntry.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.isEmpty = false → Sort u_3)
  (size : ℕ) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β)
  (x : (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).isEmpty = false)
  (h_1 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (x : (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).isEmpty = false) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l l_1 : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_2 r : Std.DTreeMap.Internal.Impl α β) →
                    l_1 = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r →
                      (h :
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                                (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r)).isEmpty =
                            false) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r))
                          h),
  (match Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x with
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_1 size k v l x
    | Std.DTreeMap.Internal.Impl.inner size k v l l_1@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r), h_3 =>
      h_2 size k v l l_1 size_1 k_1 v_1 l_2 r h h_3) =
    h_1 size k v l x
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
_private.Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf.0.CategoryTheory.Precoverage.SmallConstruction.Witness.eval.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {F : CategoryTheory.Functor Cᵒᵖ (Type w)}
  (hF : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor F R) (ι : C → Type (max u v))
  (t t_1 : (X : C) → ι X → F.obj (Opposite.op X)),
  t = t_1 →
    ∀ {X : C} (a a_1 : CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι X),
      a = a_1 →
        CategoryTheory.Precoverage.SmallConstruction.Witness.eval✝ hF ι t a =
          CategoryTheory.Precoverage.SmallConstruction.Witness.eval✝ hF ι t_1 a_1
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.evalOp_obj_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (A : Type u₁) [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  [inst_2 : CategoryTheory.Limits.HasProducts A] (F : CategoryTheory.Functor Cᵒᵖ A)
  {X Y : (CategoryTheory.Limits.FormalCoproduct C)ᵒᵖ} (f : X ⟶ Y),
  ((CategoryTheory.Limits.FormalCoproduct.evalOp C A).obj F).map f =
    CategoryTheory.Limits.Pi.lift fun i =>
      CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.Pi.π (fun i => F.obj (Opposite.op ((Opposite.unop X).obj i))) (f.unop.f i))
        (F.map (f.unop.φ i).op)
-- Mathlib.Data.List.Sigma
List.sizeOf_cons_le_sizeOf_cons : ∀ {α : Type u_1} [inst : SizeOf α] {l r : List α} (a : α), sizeOf l ≤ sizeOf r → sizeOf (a :: l) ≤ sizeOf (a :: r)
-- Mathlib.Algebra.Group.Invertible.Defs
/-- `invOf a` is a left inverse of `a`  -/
Invertible.invOf_mul_self : ∀ {α : Type u} {inst : Mul α} {inst_1 : One α} {a : α} [self : Invertible a], ⅟a * a = 1
-- Mathlib.GroupTheory.Perm.MaximalSubgroups
Equiv.Perm.isCoatom_stabilizer_of_ncard_lt_ncard_compl : ∀ {α : Type u_2} [Finite α] {s : Set α},
  s.Nonempty → s.ncard < sᶜ.ncard → IsCoatom (MulAction.stabilizer (Equiv.Perm α) s)
-- Mathlib.Analysis.Matrix.LDL
LDL.lowerInv.eq_1 : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : LinearOrder n] [inst_2 : WellFoundedLT n]
  [inst_3 : LocallyFiniteOrderBot n] {S : Matrix n n 𝕜} [inst_4 : Fintype n] (hS : S.PosDef),
  LDL.lowerInv hS = InnerProductSpace.gramSchmidt 𝕜 ⇑(Pi.basisFun 𝕜 n)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.cosh_half_dist : ∀ (z w : UpperHalfPlane), Real.cosh (dist z w / 2) = dist (↑z) ((starRingEnd ℂ) ↑w) / (2 * √(z.im * w.im))
-- Mathlib.CategoryTheory.Sites.Point.Map
CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D)
  (K : CategoryTheory.GrothendieckTopology D) [inst_2 : F.IsCocontinuous J K]
  [inst_3 : CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [inst_4 : CategoryTheory.Category.{v'', u''} A]
  [inst_5 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] {P Q : CategoryTheory.Functor Dᵒᵖ A} (g : P ⟶ Q)
  (X : C) (x : Φ.fiber.obj X) {Z : A} (h : (Φ.map F K).presheafFiber.obj Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x)
      (CategoryTheory.CategoryStruct.comp ((Φ.map F K).presheafFiber.map g) h) =
    CategoryTheory.CategoryStruct.comp (g.app (Opposite.op (F.obj X)))
      (CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K Q X x) h)
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.coe_sup : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : NormedAddCommGroup β] [inst_2 : Lattice β]
  [inst_3 : HasSolidNorm β] [inst_4 : IsOrderedAddMonoid β] (f g : BoundedContinuousFunction α β), ⇑(f ⊔ g) = ⇑f ⊔ ⇑g
-- Init.Core
/-- If the right type in a sum is inhabited then the sum is inhabited.

This is not an instance to avoid non-canonical instances when both the left and right types are
inhabited.
 -/
Sum.inhabitedRight : {α : Type u} → {β : Type v} → [Inhabited β] → Inhabited (α ⊕ β)
-- Mathlib.CategoryTheory.Sites.Plus
CategoryTheory.GrothendieckTopology.isoToPlus_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  (P : CategoryTheory.Functor Cᵒᵖ D) [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  (hP : CategoryTheory.Presheaf.IsSheaf J P), (J.isoToPlus P hP).hom = J.toPlus P
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.extFunctorObj_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (X : C) (n : ℕ) {X_1 Y : C} (f : X_1 ⟶ Y),
  (CategoryTheory.Abelian.extFunctorObj X n).map f =
    AddCommGrpCat.ofHom ((CategoryTheory.Abelian.Ext.mk₀ f).postcomp X ⋯)
-- Mathlib.LinearAlgebra.RootSystem.Hom
/-- A morphism of root pairings is a pair of mutually transposed maps of weight and coweight spaces
that preserves roots and coroots.  We make the map of indexing sets explicit.  -/
RootPairing.Hom : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  {ι₂ : Type u_5} →
                    {M₂ : Type u_6} →
                      {N₂ : Type u_7} →
                        [inst_5 : AddCommGroup M₂] →
                          [inst_6 : Module R M₂] →
                            [inst_7 : AddCommGroup N₂] →
                              [inst_8 : Module R N₂] →
                                RootPairing ι R M N →
                                  RootPairing ι₂ R M₂ N₂ → Type (max (max (max (max (max u_1 u_3) u_4) u_5) u_6) u_7)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
MeasureTheory.integral_norm_condExp_le : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] (f : α → E), ∫ (x : α), ‖μ[f | m] x‖ ∂μ ≤ ∫ (x : α), ‖f x‖ ∂μ
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.tacGen.sizeOf_spec : ∀ (decl : Lean.Name), sizeOf (Aesop.RuleTacDescr.tacGen decl) = 1 + sizeOf decl
-- Mathlib.LinearAlgebra.Matrix.StdBasis
Module.Basis.matrix.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} (m : Type u_4) (n : Type u_5) [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (b : Module.Basis ι R M),
  Module.Basis.matrix m n b =
    ((Pi.basis fun x => Pi.basis fun x => b).reindex
          ((Equiv.sigmaEquivProd m ((_ : n) × ι)).trans ((Equiv.refl m).prodCongr (Equiv.sigmaEquivProd n ι)))).map
      (Matrix.ofLinearEquiv R)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.pairwise_toList_upwardEnumerableLt : ∀ {α : Type u} {r : Std.Rci α} [LE α] [inst : Std.PRange.UpwardEnumerable α]
  [inst_1 : Std.PRange.LawfulUpwardEnumerable α] [inst_2 : Std.Rxi.IsAlwaysFinite α],
  List.Pairwise (fun a b => Std.PRange.UpwardEnumerable.LT a b) r.toList
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.SubobjectRepresentableBy.Ω₀`.

---

`h.Ω₀` is the subobject of `Ω` which corresponds to the identity `𝟙 Ω`,
given `h : SubobjectRepresentableBy Ω`.  -/
CategoryTheory.Classifier.SubobjectRepresentableBy.Ω₀ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      {Ω : C} → CategoryTheory.SubobjectRepresentableBy Ω → CategoryTheory.Subobject Ω
-- Mathlib.Order.Bounds.Image
MonotoneOn.mem_lowerBounds_image_self : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {t : Set α} {a : α},
  MonotoneOn f t → a ∈ lowerBounds t → a ∈ t → f a ∈ lowerBounds (f '' t)
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.mem_fromIdeal : ∀ {R : Type u_1} [inst : Ring R] {I : Ideal R} {x : R}, x ∈ TwoSidedIdeal.fromIdeal I ↔ x ∈ TwoSidedIdeal.span ↑I
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- Any structured arrow factors through a universal arrow.  -/
CategoryTheory.StructuredArrow.IsUniversal.fac_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {f : CategoryTheory.StructuredArrow S T} (h : f.IsUniversal)
  (g : CategoryTheory.StructuredArrow S T) {Z : D} (h_1 : T.obj g.right ⟶ Z),
  CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp (T.map (h.desc g)) h_1) =
    CategoryTheory.CategoryStruct.comp g.hom h_1