mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.BigOperators.Group.Finset.Gaps
Finset.prod_eq_prod_range_intervalGapsWithin : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : CommGroup β] (F : Finset (α × α)) {k : ℕ}
  (h : F.card = k) {a b : α} (f : α → α → β),
  ∏ z ∈ F, f z.1 z.2 = ∏ i ∈ Finset.range k, f (F.intervalGapsWithin h a b ↑i).2 (F.intervalGapsWithin h a b ↑i.succ).1
-- Mathlib.Logic.Function.Basic
Function.FactorsThrough.rfl : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, Function.FactorsThrough f f
-- Mathlib.Data.Multiset.Filter
Multiset.monotone_filter_left : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p], Monotone (Multiset.filter p)
-- Mathlib.Data.Nat.Cast.Basic
Pi.ofNat_apply : ∀ {α : Type u_1} {π : α → Type u_3} (n : ℕ) [inst : (i : α) → OfNat (π i) n] (a : α), (OfNat.ofNat n) a = OfNat.ofNat n
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_prod : ∀ (α : Type u) (β : Type v),
  Cardinal.mk (α × β) = Cardinal.lift.{v, u} (Cardinal.mk α) * Cardinal.lift.{u, v} (Cardinal.mk β)
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.mk : {R : Type u_1} →
  [inst : CommRing R] →
    (toPowerSeries : MvPowerSeries (Fin 2) R) →
      MvPowerSeries.constantCoeff toPowerSeries = 0 →
        (MvPowerSeries.coeff fun₀ | 0 => 1) toPowerSeries = 1 →
          (MvPowerSeries.coeff fun₀ | 1 => 1) toPowerSeries = 1 →
            MvPowerSeries.subst
                  ![MvPowerSeries.subst ![MvPowerSeries.X 0, MvPowerSeries.X 1] toPowerSeries, MvPowerSeries.X 2]
                  toPowerSeries =
                MvPowerSeries.subst
                  ![MvPowerSeries.X 0, MvPowerSeries.subst ![MvPowerSeries.X 1, MvPowerSeries.X 2] toPowerSeries]
                  toPowerSeries →
              FormalGroup R
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.fold_eq_foldl_keysArray : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {δ : Type w} {f : δ → α → δ} {init : δ},
  Std.DHashMap.Raw.fold (fun d a x => f d a) init ↑m = Array.foldl f init (↑m).keysArray
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey!_modify : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  (↑m).WF →
    ∀ [inst_4 : Inhabited α] {k k' : α} {f : β → β},
      (Std.DHashMap.Internal.Raw₀.Const.modify m k f).getKey! k' =
        if (k == k') = true then if m.contains k = true then k else default else m.getKey! k'
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
EisensteinSeries.e2Summand_summable : ∀ (m : ℤ) (z : UpperHalfPlane), Summable fun n => EisensteinSeries.eisSummand 2 ![m, n] z
-- Lean.Meta.Tactic.Grind.AC.Seq
Lean.Grind.AC.SubseqResult.suffix.inj : ∀ {s s_1 : Lean.Grind.AC.Seq}, Lean.Grind.AC.SubseqResult.suffix s = Lean.Grind.AC.SubseqResult.suffix s_1 → s = s_1
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.liftNatTrans_id : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : L.IsLocalization W] (F : CategoryTheory.Functor C E) (F' : CategoryTheory.Functor D E)
  [h : CategoryTheory.Localization.Lifting L W F F'],
  CategoryTheory.Localization.liftNatTrans L W F F F' F' (CategoryTheory.CategoryStruct.id F) =
    CategoryTheory.CategoryStruct.id F'
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- `sheafCompose` commutes with `pushforward`  -/
AlgebraicGeometry.Scheme.Modules.sheafComposePushforwardComp : {R S : CommRingCat} →
  (φ : R ⟶ S) →
    (CategoryTheory.sheafCompose (Opens.grothendieckTopology ↥(AlgebraicGeometry.Spec S))
            (ModuleCat.restrictScalars
              (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.Spec.map φ))))).comp
        ((TopCat.Sheaf.pushforward (ModuleCat ↑((AlgebraicGeometry.Spec R).presheaf.obj (Opposite.op ⊤)))
              (AlgebraicGeometry.Spec.map φ).base).comp
          (CategoryTheory.sheafCompose (Opens.grothendieckTopology ↥(AlgebraicGeometry.Spec R))
            (ModuleCat.restrictScalars (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso R).inv)))) ≅
      (CategoryTheory.sheafCompose (Opens.grothendieckTopology ↥(AlgebraicGeometry.Spec S))
            (ModuleCat.restrictScalars (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso S).inv))).comp
        ((TopCat.Sheaf.pushforward (ModuleCat ↑S) (AlgebraicGeometry.Spec.map φ).base).comp
          (CategoryTheory.sheafCompose (Opens.grothendieckTopology ↥(AlgebraicGeometry.Spec R))
            (ModuleCat.restrictScalars (CommRingCat.Hom.hom φ))))
-- Mathlib.Topology.Algebra.Monoid
AddSubsemigroup.topologicalClosure_minimal : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddSemigroup M] [inst_2 : SeparatelyContinuousAdd M]
  (s : AddSubsemigroup M) {t : AddSubsemigroup M}, s ≤ t → IsClosed ↑t → s.topologicalClosure ≤ t
-- Mathlib.Analysis.SpecialFunctions.Log.InvLog
Real.deriv_log_log : (deriv fun x => Real.log (Real.log x)) = fun x => x⁻¹ / Real.log x
-- Init.System.IO
/-- Converts an `Except ε` action into an `IO` action.

If the `Except ε` action throws an exception, then the exception type's `ToString` instance is used
to convert it into an `IO.Error`, which is thrown. Otherwise, the value is returned.
 -/
IO.ofExcept : {ε : Type u_1} → {α : Type} → [ToString ε] → Except ε α → IO α
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
RootPairing.exists_form_eq_form_and_form_ne_zero : ∀ {ι : 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] (P : RootPairing ι R M N) [NeZero 2]
  [P.IsIrreducible] (B : P.InvariantForm) (i j : ι),
  ∃ k, (B.form (P.root k)) (P.root k) = (B.form (P.root j)) (P.root j) ∧ (B.form (P.root i)) (P.root k) ≠ 0
-- Mathlib.LinearAlgebra.Coevaluation
/-- This lemma corresponds to one of the coherence laws for duals in rigid categories, see
`CategoryTheory.Monoidal.Rigid`.  -/
contractLeft_assoc_coevaluation' : ∀ (K : Type u) [inst : Field K] (V : Type v) [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : FiniteDimensional K V],
  LinearMap.lTensor V (contractLeft K V) ∘ₗ
      ↑(TensorProduct.assoc K V (Module.Dual K V) V) ∘ₗ LinearMap.rTensor V (coevaluation K V) =
    ↑(TensorProduct.rid K V).symm ∘ₗ ↑(TensorProduct.lid K V)
-- Mathlib.CategoryTheory.Quotient
/-- Inverse of a map in the quotient category of a groupoid.  -/
CategoryTheory.Quotient.inv : {G : Type u_2} →
  [inst : CategoryTheory.Groupoid G] → (r : HomRel G) → {X Y : CategoryTheory.Quotient r} → (X ⟶ Y) → (Y ⟶ X)
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteSupport.sub : ∀ {α : Type u_1} {M : Type u_3} [inst : SubtractionMonoid M] {f g : α → M},
  Function.HasFiniteSupport f → Function.HasFiniteSupport g → Function.HasFiniteSupport (f - g)
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
instCategoryDerivedCategory : (C : Type u_2) →
  [inst : CategoryTheory.Category.{u_3, u_2} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] → CategoryTheory.Category.{u_1, max u_2 u_3} (DerivedCategory C)
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubmonoid.val_neg_addUnitsEquivAddUnitsType_apply_coe : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) (x : ↥S.addUnits),
  ↑↑(-S.addUnitsEquivAddUnitsType x) = (AddUnits.coeHom M) (-↑x)
-- Init.Data.SInt.Float32
/-- Truncates a floating-point number to the nearest word-sized signed integer, rounding towards zero.

If the `Float` is larger than the maximum value for `ISize` (including `Inf`), returns the maximum
value of `ISize` (i.e. `ISize.maxValue`). If it is smaller than the minimum value for `ISize`
(including `-Inf`), returns the minimum value of `ISize` (i.e. `ISize.minValue`). If it is `NaN`,
returns `0`.

This function does not reduce in the kernel.
 -/
Float32.toISize : Float32 → ISize
-- Init.Grind.Interactive
/-- `rw [h₁, ..., hₙ]` rewrites the goal target using the given equations or iffs, left to right.
Use `← h` to rewrite right to left. Only available in `sym =>` mode, and it only rewrites the
target: in `sym =>` mode hypotheses are never modified.

Premises of a conditional rewrite rule that cannot be resolved by unification or type class
resolution become new goals.

`rw` is **not** a high-performance tactic: it does not exploit the maximal sharing maintained
by `sym =>` mode, and should be used for surgical changes to the goal, not for bulk
simplification. Use `simp`/`dsimp` variants for that.
 -/
Lean.Parser.Tactic.Grind.symRw : Lean.ParserDescr
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.weierstrassMod_zero_right : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] (f : PowerSeries A)
  [inst_2 : IsPrecomplete (IsLocalRing.maximalIdeal A) A], f %ʷ 0 = 0
-- Mathlib.RingTheory.HopfAlgebra.Quotient
/-- An ideal whose underlying `R`-submodule is a coideal and which is stable under the
antipode (`S(I) ⊆ I`). Together with `I.IsTwoSided`, this makes `I` a *Hopf ideal*.  -/
Ideal.IsHopfIdeal : (R : Type u_1) → {A : Type u_2} → [inst : CommRing R] → [inst_1 : Ring A] → [HopfAlgebraStruct R A] → Ideal A → Prop
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidIso.unitsWithZero_apply : ∀ {α : Type u_6} [inst : Group α] [inst_1 : Preorder α] (a : (WithZero α)ˣ),
  OrderMonoidIso.unitsWithZero a = WithZero.unzero ⋯
-- Mathlib.Topology.Algebra.Group.Basic
Filter.tendsto_const_div_iff' : ∀ {G : Type w} {α : Type u} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] (b : G) {c : G}
  {f : α → G} {l : Filter α}, Filter.Tendsto (fun k => b / f k) l (nhds (b / c)) ↔ Filter.Tendsto f l (nhds c)
-- Batteries.Data.BinomialHeap.Basic
/-- `O(n)`. Fold a function over the tree structure to accumulate a value.  -/
Batteries.BinomialHeap.Imp.Heap.foldTree : {β : Type u_1} → {α : Type u_2} → β → (α → β → β → β) → Batteries.BinomialHeap.Imp.Heap α → β
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_insert_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, k ∈ m.insert k v
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.blsub_le : ∀ {o : Ordinal.{u_3}} {f : (b : Ordinal.{u_3}) → b < o → Ordinal.{max u_3 u_4}} {a : Ordinal.{max u_3 u_4}},
  (∀ (i : Ordinal.{u_3}) (h : i < o), f i h < a) → o.blsub f ≤ a
-- Mathlib.Analysis.Calculus.FDeriv.Add
differentiable_const_add_iff : ∀ {𝕜 : 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] {f : E → F}
  (c : F), (Differentiable 𝕜 fun y => c + f y) ↔ Differentiable 𝕜 f
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.InitResults.mk.injEq : ∀ {α : Type} (tree : Lean.Meta.RefinedDiscrTree.PreDiscrTree α)
  (errors : Array Lean.Meta.RefinedDiscrTree.ImportFailure✝) (tree_1 : Lean.Meta.RefinedDiscrTree.PreDiscrTree α)
  (errors_1 : Array Lean.Meta.RefinedDiscrTree.ImportFailure✝),
  ({ tree := tree, errors := errors } = { tree := tree_1, errors := errors_1 }) = (tree = tree_1 ∧ errors = errors_1)
-- Mathlib.CategoryTheory.Bicategory.Monad.Basic
CategoryTheory.Bicategory.Comonad.comul_assoc_flip : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a : B} (t : a ⟶ a) [inst_1 : CategoryTheory.Bicategory.Comonad t],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.Comonad.comul
      (CategoryTheory.Bicategory.whiskerRight CategoryTheory.Bicategory.Comonad.comul t) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.Comonad.comul
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft t CategoryTheory.Bicategory.Comonad.comul)
        (CategoryTheory.Bicategory.associator t t t).inv)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.Hom.mk'.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.AddMon C} (f : M.X ⟶ N.X)
  (one_f : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero f = CategoryTheory.AddMonObj.zero)
  (mul_f :
    CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add f =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f)
        CategoryTheory.AddMonObj.add),
  CategoryTheory.AddMon.Hom.mk' f one_f mul_f = { hom := f, isAddMonHom_hom := ⋯ }
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
/-- The adjoint as a linear map from its domain to `E`.

This is an auxiliary definition needed to define the adjoint operator as a `LinearPMap` without
the assumption that `T.domain` is dense.  -/
LinearPMap.adjointAux : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : InnerProductSpace 𝕜 F] →
                {T : E →ₗ.[𝕜] F} → [CompleteSpace E] → Dense ↑T.domain → ↥T.adjointDomain →ₗ[𝕜] E
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.mgf_zero_measure : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ}, ProbabilityTheory.mgf X 0 = 0
-- Init.Data.Nat.Basic
Nat.lt_of_sub_ne_zero : ∀ {n m : ℕ}, n - m ≠ 0 → m < n
-- Mathlib.RingTheory.Polynomial.GaussLemma
/-- **Gauss's Lemma** for integrally closed domains states that a monic polynomial is irreducible
iff it is irreducible in the fraction field.  -/
Polynomial.Monic.irreducible_iff_irreducible_map_fraction_map : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] [IsFractionRing R K]
  [IsIntegrallyClosed R] {p : Polynomial R}, p.Monic → (Irreducible p ↔ Irreducible (Polynomial.map (algebraMap R K) p))
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedInClass.instBoundedContinuousMapClass : ∀ (B : Type u_5) (E : outParam (Type u_6)) (F : outParam (Type u_7)) [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ E] [inst_3 : NormedSpace ℝ F] (n : outParam ℕ∞)
  (K : outParam (TopologicalSpace.Compacts E)) [inst_4 : ContDiffMapSupportedInClass B E F n K],
  BoundedContinuousMapClass B E F
-- Mathlib.Order.SuccPred.Archimedean
monotone_of_le_succ : ∀ {α : Type u_3} {β : Type u_4} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : SuccOrder α]
  [IsSuccArchimedean α] {f : α → β}, (∀ (a : α), ¬IsMax a → f a ≤ f (Order.succ a)) → Monotone f
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.not_nonpos_iff_pos_of_sum_mem_range_root : ∀ {ι : 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] {P : RootPairing ι R M N} (b : P.Base)
  [CharZero R] (f : ι → ℤ),
  ∑ j ∈ b.support, f j • P.root j ∈ Set.range ⇑P.root → Function.support f ⊆ ↑b.support → (¬f ≤ 0 ↔ 0 < f)
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.mkHom.eq_1 : ∀ {n m : ℕ} (f : Fin (n + 1) →o Fin (m + 1)), SimplexCategory.mkHom f = SimplexCategory.Hom.mk f
-- Batteries.Data.PairingHeap
_private.Batteries.Data.PairingHeap.0.Batteries.PairingHeapImp.Heap.combine.match_1.eq_1 : ∀ {α : Type u_1} (motive : Batteries.PairingHeapImp.Heap α → Sort u_2) (a : α) (child : Batteries.PairingHeapImp.Heap α)
  (a_1 : α) (child_1 s : Batteries.PairingHeapImp.Heap α)
  (h_1 :
    (h₁ : Batteries.PairingHeapImp.Heap α) →
      (a : α) →
        (child h₂ : Batteries.PairingHeapImp.Heap α) →
          (a_2 : α) →
            (child_2 s : Batteries.PairingHeapImp.Heap α) →
              h₂ = Batteries.PairingHeapImp.Heap.node a_2 child_2 s →
                h₁ = Batteries.PairingHeapImp.Heap.node a child (Batteries.PairingHeapImp.Heap.node a_2 child_2 s) →
                  motive
                    (Batteries.PairingHeapImp.Heap.node a child (Batteries.PairingHeapImp.Heap.node a_2 child_2 s)))
  (h_2 : (h : Batteries.PairingHeapImp.Heap α) → motive h),
  (match Batteries.PairingHeapImp.Heap.node a child (Batteries.PairingHeapImp.Heap.node a_1 child_1 s) with
    | h₁@h_3:(Batteries.PairingHeapImp.Heap.node a child h₂@h:(Batteries.PairingHeapImp.Heap.node a_2 child_2 s)) =>
      h_1 h₁ a child h₂ a_2 child_2 s h h_3
    | h => h_2 h) =
    h_1 (Batteries.PairingHeapImp.Heap.node a child (Batteries.PairingHeapImp.Heap.node a_1 child_1 s)) a child
      (Batteries.PairingHeapImp.Heap.node a_1 child_1 s) a_1 child_1 s ⋯ ⋯
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
/-- The lift of a functor from `C` to a groupoid to a functor from
`FreeGroupoid C` to the groupoid  -/
CategoryTheory.FreeGroupoid.lift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {G : Type u₁} →
      [inst_1 : CategoryTheory.Groupoid G] →
        CategoryTheory.Functor C G → CategoryTheory.Functor (CategoryTheory.FreeGroupoid C) G
-- Mathlib.MeasureTheory.Measure.Prod
/-- The product of two sets is null measurable
if and only if both of them are null measurable or one of them has measure zero.  -/
MeasureTheory.Measure.nullMeasurableSet_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] {s : Set α} {t : Set β},
  MeasureTheory.NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔
    MeasureTheory.NullMeasurableSet s μ ∧ MeasureTheory.NullMeasurableSet t ν ∨ μ s = 0 ∨ ν t = 0
-- Mathlib.Analysis.InnerProductSpace.ProdL2
Submodule.toLinearEquiv_orthogonalDecomposition_symm : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection],
  K.orthogonalDecomposition.symm.toLinearEquiv = WithLp.linearEquiv 2 𝕜 (↥K × ↥Kᗮ) ≪≫ₗ K.prodEquivOfIsCompl Kᗮ ⋯
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_ssubset_Icc_left : ∀ {α : Type u_2} {a₁ a₂ b₁ b₂ : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α],
  a₂ ≤ b₂ → a₂ < a₁ → b₁ ≤ b₂ → Finset.Icc a₁ b₁ ⊂ Finset.Icc a₂ b₂
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.floor : {ι : Type u_3} →
  {s : Set (ι → ℕ)} → (hs : IsProperLinearSet s) → [inst : Finite ι] → (ι → ℕ) → ↑(IsProperLinearSet.basisSet✝ hs) → ℤ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get_insertMany_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List (α × β)} {k k' : α},
      (k == k') = true →
        ∀ {v : β},
          List.Pairwise (fun a b => (a.1 == b.1) = false) l →
            (k, v) ∈ l →
              ∀ {h' : k' ∈ Std.DHashMap.Raw.Const.insertMany m l},
                Std.DHashMap.Raw.Const.get (Std.DHashMap.Raw.Const.insertMany m l) k' h' = v
-- Mathlib.Analysis.Calculus.FDeriv.Basic
Asymptotics.IsBigO.hasFDerivWithinAt : ∀ {𝕜 : 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] {f : E → F}
  {x₀ : E} {s : Set E} {n : ℕ},
  (f =O[nhdsWithin x₀ s] fun x => ‖x - x₀‖ ^ n) → x₀ ∈ s → 1 < n → HasFDerivWithinAt f 0 s x₀
-- Mathlib.LinearAlgebra.FreeModule.Int
/-- Given a submodule `N` in Smith normal form of a free `R`-module, its index as an additive
subgroup is an appropriate power of the cardinality of `R` multiplied by the product of the
indexes of the ideals generated by each basis vector.  -/
Module.Basis.SmithNormalForm.toAddSubgroup_index_eq_pow_mul_prod : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {n : ℕ} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Fintype ι] [inst_3 : Module R M] {N : Submodule R M} (snf : Module.Basis.SmithNormalForm N ι n),
  N.toAddSubgroup.index =
    Nat.card R ^ (Fintype.card ι - n) * ∏ i, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index
-- Mathlib.Data.Nat.Cast.Basic
/-- **Alias** of `Nat.cast_dvd_cast`. -/
Dvd.dvd.natCast : ∀ {α : Type u_1} [inst : Semiring α] {m n : ℕ}, m ∣ n → ↑m ∣ ↑n
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
/-- The natural isomorphism between the homology of a spectral sequence on the
object `pq : κ` of the `r`th page and the corresponding object on the next page.  -/
CategoryTheory.SpectralSequence.pageHomologyNatIso : (C : Type u_1) →
  [inst : CategoryTheory.Category.{u_3, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {κ : Type u_2} →
        (c : ℤ → ComplexShape κ) →
          (r₀ r r' : ℤ) →
            (pq : κ) →
              (hrr' : autoParam (r + 1 = r') CategoryTheory.SpectralSequence.pageHomologyNatIso._auto_1) →
                (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence.pageHomologyNatIso._auto_3) →
                  (CategoryTheory.SpectralSequence.pageFunctor C c r₀ r ⋯).comp
                      (HomologicalComplex.homologyFunctor C (c r) pq) ≅
                    (CategoryTheory.SpectralSequence.pageFunctor C c r₀ r' ⋯).comp (HomologicalComplex.eval C (c r') pq)
-- Mathlib.Analysis.Normed.Affine.AddTorsorBases
Convex.interior_nonempty_iff_affineSpan_eq_top : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [FiniteDimensional ℝ V] {s : Set V},
  Convex ℝ s → ((interior s).Nonempty ↔ affineSpan ℝ s = ⊤)
-- Mathlib.Data.Int.Lemmas
Int.natAbs_le_iff_sq_le : ∀ {a b : ℤ}, a.natAbs ≤ b.natAbs ↔ a ^ 2 ≤ b ^ 2
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- Transfer an `AddActionObj` along isomorphisms.  -/
CategoryTheory.AddModObj.ofIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            {M : C} →
              [inst_4 : CategoryTheory.AddMonObj M] →
                {X : D} →
                  {N : C} →
                    [inst_5 : CategoryTheory.AddMonObj N] →
                      (e₁ : M ≅ N) →
                        [CategoryTheory.IsAddMonHom e₁.hom] →
                          {Y : D} → (X ≅ Y) → [CategoryTheory.AddModObj M X] → CategoryTheory.AddModObj N Y
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
IsIntegralClosure.mk'.congr_simp : ∀ {R : Type u_1} (A : Type u_2) {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R B] [inst_4 : Algebra A B] [inst_5 : IsIntegralClosure A R B] (x x_1 : B) (e_x : x = x_1)
  (hx : IsIntegral R x), IsIntegralClosure.mk' A x hx = IsIntegralClosure.mk' A x_1 ⋯
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.continuous_pow : ∀ (n : ℕ), Continuous fun a => a ^ n
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
/-- If `A` is determinant balanced with respect to `a` and `b`, any submatrix of
the same or bigger size (possibly with repeated rows or columns) is also.  -/
Matrix.IsDetpBalanced.submatrix_of_card_le : ∀ {n : Type u_1} {m : Type u_2} {R : Type u_3} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : CommSemiring R] {A : Matrix n n R} {a b : R},
  A.IsDetpBalanced a b → Fintype.card n ≤ Fintype.card m → ∀ (f g : m → n), (A.submatrix f g).IsDetpBalanced a b
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
CategoryTheory.Limits.weakPullback.condition_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasWeakPullback f g] {Z_1 : C} (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakPullback.fst f g)
      (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakPullback.snd f g)
      (CategoryTheory.CategoryStruct.comp g h)
-- Lean.Compiler.InlineAttrs
Lean.Compiler.InlineAttributeKind.inlineIfReduce : Lean.Compiler.InlineAttributeKind