mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.homologySequence_comp : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A)
  [inst_3 : CategoryTheory.Limits.HasZeroObject C] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  [inst_7 : CategoryTheory.Abelian A] [F.IsHomological] [inst_9 : F.ShiftSequence ℤ],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ (n₀ : ℤ), CategoryTheory.CategoryStruct.comp ((F.shift n₀).map T.mor₁) ((F.shift n₀).map T.mor₂) = 0
-- Mathlib.Data.Rat.Cast.Order
NNRat.preimage_cast_Ioc : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ≥0),
  NNRat.cast ⁻¹' Set.Ioc ↑p ↑q = Set.Ioc p q
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.add_le : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  (abv : AbsoluteValue R S) (x y : R), abv (x + y) ≤ abv x + abv y
-- Std.Time.Time.PlainTime
Std.Time.PlainTime.instHSubOffset : HSub Std.Time.PlainTime Std.Time.Nanosecond.Offset Std.Time.PlainTime
-- Init.Data.Array.Attach
/-- If we fold over `l.attach` with a function that ignores the membership predicate,
we get the same results as folding over `l` directly.

This is useful when we need to use `attach` to show termination.

Unfortunately this can't be applied by `simp` because of the higher order unification problem,
and even when rewriting we need to specify the function explicitly.
See however `foldl_subtype` below.
 -/
Array.foldl_attach : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : β → α → β} {b : β},
  Array.foldl (fun acc t => f acc ↑t) b xs.attach = Array.foldl f b xs
-- Mathlib.RingTheory.Multiplicity
pow_dvd_of_le_emultiplicity : ∀ {α : Type u_1} [inst : Monoid α] {a b : α} {k : ℕ}, ↑k ≤ emultiplicity a b → a ^ k ∣ b
-- Mathlib.Analysis.Normed.Operator.Extend
LinearEquiv.norm_extend_symm_le : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} {Fₗ : Type u_6}
  [inst : NormedDivisionRing 𝕜] [inst_1 : NormedDivisionRing 𝕜₂] [inst_2 : AddCommGroup E]
  [inst_3 : NormedAddCommGroup Eₗ] [inst_4 : AddCommGroup F] [inst_5 : NormedAddCommGroup Fₗ] [inst_6 : Module 𝕜 E]
  [inst_7 : Module 𝕜 Eₗ] [inst_8 : IsBoundedSMul 𝕜 Eₗ] [inst_9 : Module 𝕜₂ F] [inst_10 : Module 𝕜₂ Fₗ]
  [inst_11 : IsBoundedSMul 𝕜₂ Fₗ] [inst_12 : CompleteSpace Eₗ] [inst_13 : CompleteSpace Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂}
  {σ₂₁ : 𝕜₂ →+* 𝕜} [inst_14 : RingHomInvPair σ₁₂ σ₂₁] [inst_15 : RingHomInvPair σ₂₁ σ₁₂] (f : E ≃ₛₗ[σ₁₂] F)
  (e₁ : E →ₗ[𝕜] Eₗ) (e₂ : F →ₗ[𝕜₂] Fₗ) (C : ℝ) (h_dense₁ : DenseRange ⇑e₁)
  (h_norm₁ : ∃ C, ∀ (x : E), ‖e₂ (f x)‖ ≤ C * ‖e₁ x‖) (h_dense₂ : DenseRange ⇑e₂)
  (h_norm₂ : ∀ (x : F), ‖e₁ (f.symm x)‖ ≤ C * ‖e₂ x‖) (x : Fₗ),
  ‖(f.extend e₁ e₂ h_dense₁ h_norm₁ h_dense₂ ⋯).symm x‖ ≤ C * ‖x‖
-- Mathlib.Topology.Homotopy.Path
Path.Homotopic.refl : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ : X} (p : Path x₀ x₁), p.Homotopic p
-- Mathlib.Algebra.Order.Field.Basic
div_nat_lt_self_of_pos_of_two_le : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a : α} [IsStrictOrderedRing α],
  0 < a → ∀ {n : ℕ}, 2 ≤ n → a / ↑n < a
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain.addMonoidHom_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [inst : AddCommMonoid M] (f : β → γ) (g : α → β),
  Finsupp.mapDomain.addMonoidHom (f ∘ g) = (Finsupp.mapDomain.addMonoidHom f).comp (Finsupp.mapDomain.addMonoidHom g)
-- Mathlib.Analysis.Convex.Mul
ConvexOn.mul_concaveOn' : ∀ {𝕜 : Type u_1} {E : Type u_2} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : CommRing E] [inst_4 : LinearOrder E] [IsStrictOrderedRing E] [inst_6 : AddCommGroup G] [inst_7 : Module 𝕜 G]
  [inst_8 : Module 𝕜 E] {s : Set G} [IsOrderedModule 𝕜 E] [IsScalarTower 𝕜 E E] [SMulCommClass 𝕜 E E] {f g : G → E},
  ConvexOn 𝕜 s f →
    ConcaveOn 𝕜 s g →
      (∀ ⦃x : G⦄, x ∈ s → f x ≤ 0) → (∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x) → MonovaryOn f g s → ConvexOn 𝕜 s (f * g)
-- Mathlib.Data.Matrix.Mul
Matrix.vecMul_vecMulVec : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalSemiring α] [inst_1 : Fintype m] (u v : m → α)
  (w : n → α), Matrix.vecMul u (Matrix.vecMulVec v w) = (u ⬝ᵥ v) • w
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_filter_not_contains : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.getValueCast? k (List.filter (fun p => !l₂.contains p.fst) l₁) =
      if l₂.contains k = true then none else Std.Internal.List.getValueCast? k l₁
-- Mathlib.Analysis.RCLike.Lemmas
/-- An `RCLike` field is finite-dimensional over `ℝ`, since it is spanned by `{1, I}`.  -/
FiniteDimensional.rclike_to_real : ∀ {K : Type u_1} [inst : RCLike K], FiniteDimensional ℝ K
-- Mathlib.LinearAlgebra.Complex.Module
imaginaryPart_realPart : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A]
  {x : A}, imaginaryPart ↑(realPart x) = 0
-- Init.Data.Array.MinMax
Array.max.congr_simp : ∀ {α : Type u_1} [inst : Max α] (arr arr_1 : Array α) (e_arr : arr = arr_1) (h : arr ≠ #[]), arr.max h = arr_1.max ⋯
-- Mathlib.Data.ENNReal.Operations
ENNReal.sub_eq_top_iff : ∀ {a b : ENNReal}, a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.withUsed : {α : Type} →
  Array Lean.Expr →
    Array Lean.Elab.DefViewElabHeader →
      Array Lean.Expr →
        List Lean.Elab.Term.LetRecToLift → (Array Lean.Expr → Lean.Elab.TermElabM α) → Lean.Elab.TermElabM α
-- Mathlib.Algebra.Torsor.Basic
Equiv.constSMul_one : ∀ (G : Type u_1) (P : Type u_2) [inst : Group G] [inst_1 : Torsor G P], Equiv.constSMul P 1 = 1
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.min?.eq_3 : ∀ {α : Type u_1} (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α),
  (l = RBTree.RBNode.nil → False) → (RBTree.RBNode.node c l v r).min? = l.min?
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem_modify_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : β → β} {hc : k ∈ t.modify k f}, (t.modify k f)[k] = f t[k]
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.isOrtho_iff_inner_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U V : Submodule 𝕜 E}, U ⟂ V ↔ ∀ u ∈ U, ∀ v ∈ V, inner 𝕜 u v = 0
-- Std.Async.System
/-- The approximate clock speed of the CPU core in MHz.
 -/
Std.Async.System.CPUInfo.speed : Std.Async.System.CPUInfo → ℕ
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.linearMapEquivDerivation_apply_apply : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {M : Type u_1}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  (m : Ω[S⁄R] →ₗ[S] M) (x : S),
  ((KaehlerDifferential.linearMapEquivDerivation R S) m) x = m ((KaehlerDifferential.D R S) x)
-- Mathlib.Algebra.EuclideanDomain.Defs
/-- `gcd a b` is a (non-unique) element such that `gcd a b ∣ a` `gcd a b ∣ b`, and for
any element `c` such that `c ∣ a` and `c ∣ b`, then `c ∣ gcd a b`  -/
EuclideanDomain.gcd : {R : Type u} → [EuclideanDomain R] → [DecidableEq R] → R → R → R
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_eq_some_iff_exists_beq_and_mem_toArray : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {k : α} {v : β},
      Std.DHashMap.Internal.Raw₀.Const.get? m k = some v ↔
        ∃ k', (k == k') = true ∧ (k', v) ∈ Std.DHashMap.Raw.Const.toArray ↑m
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionAtOfComplement.codChart.congr_simp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I I_1 : ModelWithCorners 𝕜 E H}
  (e_I : I = I_1) {J J_1 : ModelWithCorners 𝕜 E'' G} (e_J : J = J_1) {M : Type u_11} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace H M] {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N]
  {n n_1 : WithTop ℕ∞} (e_n : n = n_1) {f f_1 : M → N} (e_f : f = f_1) {x x_1 : M} (e_x : x = x_1)
  (h : Manifold.IsImmersionAtOfComplement F I J n f x), h.codChart = ⋯.codChart
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
QuadraticModuleCat.Hom.toIsometry_injective : ∀ {R : Type u} [inst : CommRing R] (V W : QuadraticModuleCat R), Function.Injective QuadraticModuleCat.Hom.toIsometry
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.disjointSigma_isBase_iff : ∀ {α : Type u_1} {ι : Type u_2} {M : ι → Matroid α} {h : Pairwise (Function.onFun Disjoint fun i => (M i).E)}
  {B : Set α}, (Matroid.disjointSigma M h).IsBase B ↔ (∀ (i : ι), (M i).IsBase (B ∩ (M i).E)) ∧ B ⊆ ⋃ i, (M i).E
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.toRealLinearMap_apply : ∀ {α : Type u_2} [inst : TopologicalSpace α] (f : CompactlySupportedContinuousMap α NNReal),
  CompactlySupportedContinuousMap.toRealLinearMap f = f.toReal
-- Init.Grind.AC
Lean.Grind.AC.eq_simp_lhs_middle : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op}
  (lhs₁ rhs₁ head tail lhs₂ rhs₂ lhs₂' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.simp_middle_cert lhs₁ rhs₁ head tail lhs₂ lhs₂' = true →
    Lean.Grind.AC.Seq.denote ctx lhs₁ = Lean.Grind.AC.Seq.denote ctx rhs₁ →
      Lean.Grind.AC.Seq.denote ctx lhs₂ = Lean.Grind.AC.Seq.denote ctx rhs₂ →
        Lean.Grind.AC.Seq.denote ctx lhs₂' = Lean.Grind.AC.Seq.denote ctx rhs₂
-- Mathlib.Data.Int.ModEq
Int.ModEq.sub_left : ∀ {n a b : ℤ} (c : ℤ), a ≡ b [ZMOD n] → c - a ≡ c - b [ZMOD n]
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsSingular.natCast_lt : ∀ {c : Cardinal.{u_1}}, c.IsSingular → ∀ (n : ℕ), ↑n < c
-- Init.Data.Nat.Lcm
Nat.lcm_mul_left_left_eq_mul_of_lcm_eq_mul : ∀ {n m k : ℕ}, n.lcm m = n * m → (k * n).lcm m = n * k.lcm m
-- Mathlib.Algebra.Order.Group.Lattice
/-- Every lattice ordered commutative additive group is a distributive lattice  -/
AddCommGroup.toDistribLattice : (α : Type u_2) → [inst : Lattice α] → [inst_1 : AddCommGroup α] → [AddLeftMono α] → DistribLattice α
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
Lean.Meta.Grind.Arith.CommRing.getNonCommSemiringId? : Lean.Expr → Lean.Meta.Grind.GoalM (Option ℕ)
-- Init.Data.String.Basic
String.utf8SetAux : Char → List Char → String.Pos.Raw → String.Pos.Raw → List Char
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
HomotopyCategory.Pretriangulated.invRotate_distinguished_triangle' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C],
  ∀ T ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C,
    T.invRotate ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.coe_copy_eq : ∀ {M : Type u_4} {N : Type u_5} {x : Zero M} {x_1 : Zero N} (f : ZeroHom M N) (f' : M → N) (h : f' = ⇑f),
  f.copy f' h = f
-- Init.Data.List.Basic
/-- Returns the first element in the list if there is one, or `fallback` if the list is empty.

Use `List.head?` to return an `Option`, and `List.head!` to panic on empty lists.

Examples:
* `[].headD "empty" = "empty"`
* `[].headD 2 = 2`
* `["head", "shoulders", "knees"].headD "toes" = "head"`
 -/
List.headD : {α : Type u} → List α → α → α
-- Init.Data.Bool
Bool.toNat_lt : ∀ (b : Bool), b.toNat < 2
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
CochainComplex.mappingCone.triangleRotateShortComplex_X₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L),
  (CochainComplex.mappingCone.triangleRotateShortComplex φ).X₃ = (CochainComplex.mappingCone.triangle φ).rotate.obj₃
-- Init.Prelude
_private.Init.Prelude.0.Lean.eraseMacroScopesAux : Lean.Name → Lean.Name
-- Mathlib.LinearAlgebra.Complex.Module
imaginaryPart_I_smul : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A]
  (a : A), imaginaryPart (Complex.I • a) = realPart a
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.below.one_mul : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  {motive : (a a_1 : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Relation F a a_1 → Prop}
  (x : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation.below ⋯
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
/-- The collection of all single functors `C ⥤ HomotopyCategory.Plus C` for `n : ℤ`
along with their compatibilities with shifts.  -/
HomotopyCategory.Plus.singleFunctors : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasZeroObject C] → CategoryTheory.SingleFunctors C (HomotopyCategory.Plus C) ℤ
-- Mathlib.Order.Monotone.Defs
Antitone.comp_monotone : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
  {f : α → β}, Antitone g → Monotone f → Antitone (g ∘ f)
-- Std.Data.HashMap.Lemmas
Std.HashMap.length_toList : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m.toList.length = m.size
-- Mathlib.Logic.Basic
and_symm_right : ∀ {α : Sort u_1} (a b : α) (p : Prop), p ∧ a = b ↔ p ∧ b = a
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- **Alias** of `MonoidAlgebra.coeff_mapRingHom`. -/
MonoidAlgebra.mapRingHom_apply : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Monoid M]
  (f : R →+* S) (x : MonoidAlgebra R M) (m : M), ((MonoidAlgebra.mapRingHom M f) x).coeff m = f (x.coeff m)
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.instPartialOrder : {X : SSet} → PartialOrder X.N
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.hasSum_sumInvPow : ∀ (L : PeriodPair) (x : ℂ) {r : ℕ}, 2 < r → HasSum (fun l => ((↑l - x) ^ r)⁻¹) (L.sumInvPow x r)
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instAddCommMonoidWithOne : {n : Type u_2} → {A : Type u_5} → [DecidableEq n] → [AddCommMonoidWithOne A] → AddCommMonoidWithOne (CStarMatrix n n A)
-- Mathlib.Algebra.Module.ZMod
/-- The quotient of an abelian group by a subgroup containing all multiples of `n` is a
`n`-torsion group.  -/
QuotientAddGroup.zmodModule : {n : ℕ} →
  {G : Type u_3} → [inst : AddCommGroup G] → {H : AddSubgroup G} → (∀ (x : G), n • x ∈ H) → Module (ZMod n) (G ⧸ H)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β k}, (m.insert k v).size = if k ∈ m then m.size else m.size + 1
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.le_nfpFamily : ∀ {ι : Type u_1} [Small.{u, u_1} ι] (f : ι → Ordinal.{u} → Ordinal.{u}) (a : Ordinal.{u}), a ≤ Ordinal.nfpFamily f a
-- Mathlib.Algebra.Group.Submonoid.Units
/-- Given some `x : M` which is a member of the additive submonoid of additive unit
elements corresponding to a subgroup of units, produce a unit of `M` whose coercion is equal to
`x`.  -/
AddSubgroup.addUnit_of_mem_ofAddUnits : {M : Type u_1} → [inst : AddMonoid M] → (S : AddSubgroup (AddUnits M)) → {x : M} → x ∈ S.ofAddUnits → AddUnits M
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- Linear isometry between `E` and `EuclideanSpace 𝕜 ι` representing the orthonormal basis.  -/
OrthonormalBasis.repr : {ι : Type u_1} →
  {𝕜 : Type u_3} →
    [inst : RCLike 𝕜] →
      {E : Type u_4} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] → [inst_3 : Fintype ι] → OrthonormalBasis ι 𝕜 E → E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccPrelimit.isSuccLimit_of_not_isMin : ∀ {α : Type u_1} {a : α} [inst : Preorder α], Order.IsSuccPrelimit a → ¬IsMin a → Order.IsSuccLimit a
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.IsDetecting.isSeparating : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.ObjectProperty C}
  [CategoryTheory.Limits.HasEqualizers C], P.IsDetecting → P.IsSeparating
-- Mathlib.Topology.Sequences
/-- If the domain of a function is a sequential space, then continuity of this function is
equivalent to its sequential continuity.  -/
continuous_iff_seqContinuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [SequentialSpace X]
  {f : X → Y}, Continuous f ↔ SeqContinuous f
-- Init.Data.List.MinMax
List.min_le_of_mem : ∀ {α : Type u_1} [inst : Min α] [inst_1 : LE α] [Std.IsLinearOrder α] [Std.LawfulOrderMin α] {l : List α} {a : α}
  (ha : a ∈ l), l.min ⋯ ≤ a
-- Mathlib.Data.TypeVec
TypeVec.comp_id : ∀ {n : ℕ} {α : TypeVec.{u} n} {β : TypeVec.{v} n} (f : α.Arrow β), TypeVec.comp f TypeVec.id = f
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- Given left homology map data for morphisms `φ` and `φ'`, this is
the induced left homology map data for `φ + φ'`.  -/
CategoryTheory.ShortComplex.LeftHomologyMapData.add : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ φ' : S₁ ⟶ S₂} →
          {h₁ : S₁.LeftHomologyData} →
            {h₂ : S₂.LeftHomologyData} →
              CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂ →
                CategoryTheory.ShortComplex.LeftHomologyMapData φ' h₁ h₂ →
                  CategoryTheory.ShortComplex.LeftHomologyMapData (φ + φ') h₁ h₂
-- Mathlib.Topology.ContinuousOn
continuousWithinAt_congr_of_mem : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {s : Set α}
  {x : α}, (∀ y ∈ s, g y = f y) → x ∈ s → (ContinuousWithinAt g s x ↔ ContinuousWithinAt f s x)
-- Mathlib.GroupTheory.Commutator.Basic
/-- Additive subgroup generated by representatives `g₁ g₂ : G` of additive
commutators `⁅g₁, g₂⁆ ∈ G`.  -/
closureAddCommutatorRepresentatives : (G : Type u_1) → [inst : AddGroup G] → AddSubgroup G
-- Mathlib.RingTheory.Frobenius
AlgHom.IsArithFrobAt.restrict_injective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {φ : S →ₐ[R] S}
  {Q : Ideal S} (H : φ.IsArithFrobAt Q) [Q.IsPrime], Function.Injective ⇑H.restrict
-- Mathlib.RingTheory.Coalgebra.TensorProduct
_private.Mathlib.RingTheory.Coalgebra.TensorProduct.0.Coalgebra.«term_⊗ₘ_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Constructions.SumProd
isOpen_setOfPred_disjoint_nhds_nhds : ∀ {X : Type u} [inst : TopologicalSpace X], IsOpen {p | Disjoint (nhds p.1) (nhds p.2)}
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toList_filterMapM_eq_toList_filterMapWithPostcondition : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n]
  [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_6 : MonadLiftT m n] [LawfulMonadLiftT m n]
  [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] {f : β → n (Option γ)} {it : Std.IterM m β},
  (Std.IterM.filterMapM f it).toList =
    (Std.IterM.filterMapWithPostcondition (fun b => Std.Iterators.PostconditionT.attachLift (f b)) it).toList
-- Init.Data.Nat.MinMax
Nat.instCommutativeMin : Std.Commutative min
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.Simp.simpLambda : Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Result
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.erase_single_same : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] (i : ι) (x : β i),
  (DFinsupp.erase i fun₀ | i => x) = 0
-- Mathlib.Data.Nat.BinaryRec
Nat.bit_lt_two_pow_succ_iff : ∀ {b : Bool} {x n : ℕ}, Nat.bit b x < 2 ^ (n + 1) ↔ x < 2 ^ n
-- Mathlib.Algebra.BigOperators.Finprod
/-- If `f a = 0`, then the sum of `f i` over `i ∈ insert a s` equals the sum of `f i`
over `i ∈ s`.  -/
finsum_mem_insert_zero : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {a : α} {s : Set α},
  f a = 0 → ∑ᶠ (i : α) (_ : i ∈ insert a s), f i = ∑ᶠ (i : α) (_ : i ∈ s), f i
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
complEDS'_odd : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (k : ℤ) (m : ℕ),
  complEDS' b c d k (2 * (m + 1) + 1) =
    complEDS' b c d k (m + 1) ^ 2 * normEDS b c d ((↑m + 2) * k + 1) * normEDS b c d ((↑m + 2) * k - 1) -
      complEDS' b c d k (m + 2) ^ 2 * normEDS b c d ((↑m + 1) * k + 1) * normEDS b c d ((↑m + 1) * k - 1)
-- Mathlib.Analysis.Normed.Algebra.GelfandFormula
/-- In a complex Banach algebra, if every element of the spectrum has norm strictly less than
`r : ℝ≥0`, then the spectral radius is also strictly less than `r`.  -/
spectrum.spectralRadius_lt_of_forall_lt : ∀ {A : Type u_2} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [CompleteSpace A] [Nontrivial A] (a : A)
  {r : NNReal}, (∀ z ∈ spectrum ℂ a, ‖z‖₊ < r) → spectralRadius ℂ a < ↑r
-- Mathlib.Algebra.Ring.InjSurj
/-- A type endowed with `0`, `1` and `+` is an additive monoid with one,
if it admits a surjective map that preserves `0`, `1` and `*` from an additive monoid with one.
See note [reducible non-instances].  -/
Function.Surjective.addCommMonoidWithOne : {R : Type u_1} →
  {S : Type u_2} →
    (f : R → S) →
      Function.Surjective f →
        [inst : Add S] →
          [inst_1 : Zero S] →
            [inst_2 : One S] →
              [inst_3 : SMul ℕ S] →
                [inst_4 : NatCast S] →
                  [inst_5 : AddCommMonoidWithOne R] →
                    f 0 = 0 →
                      f 1 = 1 →
                        (∀ (x y : R), f (x + y) = f x + f y) →
                          (∀ (n : ℕ) (x : R), f (n • x) = n • f x) → (∀ (n : ℕ), f ↑n = ↑n) → AddCommMonoidWithOne S
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_rev_Ioi : ∀ {n : ℕ} (i : Fin n), Fin.rev ⁻¹' Set.Ioi i = Set.Iio i.rev
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.isIndContained_iff_exists_comap_eq : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W},
  H.IsIndContained G ↔ ∃ f, SimpleGraph.comap (⇑f) G = H
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.filterMapM.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) →
    (__do_lift : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive __do_lift
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- `f.prev j` is `f.f i` if there is some `r i j`, and `f.f j` otherwise.  -/
HomologicalComplex.Hom.prev : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        {c : ComplexShape ι} → {C₁ C₂ : HomologicalComplex V c} → C₁.Hom C₂ → (j : ι) → C₁.xPrev j ⟶ C₂.xPrev j
-- Init.Data.List.Sublist
List.dropLast_subset : ∀ {α : Type u_1} (l : List α), l.dropLast ⊆ l
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.unit_leftAdjointUniq_hom_app : ∀ {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 F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (x : C),
  CategoryTheory.CategoryStruct.comp (adj1.unit.app x) (G.map ((adj1.leftAdjointUniq adj2).hom.app x)) = adj2.unit.app x