mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.Triangulated
/-- the octahedron axiom (TR 4)  -/
CategoryTheory.IsTriangulated.octahedron_axiom : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Preadditive C}
  {inst_2 : CategoryTheory.Limits.HasZeroObject C} {inst_3 : CategoryTheory.HasShift C ℤ}
  {inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst_5 : CategoryTheory.Pretriangulated C}
  [self : CategoryTheory.IsTriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  (comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : X₂ ⟶ Z₁₂}
  {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  (h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  (h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  (h₁₃ :
    CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
  Nonempty (CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.lift'.eq_1 : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_4}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {f : ℕ × M → A} (hf_zero : ∀ (m : M), f (0, m) = 1)
  (hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m))
  (hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m))
  (hf_add :
    ∀ (n : ℕ) (u v : M),
      f (n, u + v) =
        ∑ x ∈ Finset.HasAntidiagonal.antidiagonal n,
          match x with
          | (k, l) => f (k, u) * f (l, v)),
  DividedPowerAlgebra.lift' hf_zero hf_smul hf_mul hf_add =
    (DividedPowerAlgebra.ringCon R M).liftₐ (MvPolynomial.eval₂AlgHom R f) ⋯
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.mk.inj : ∀ {V : Type u} {Adj : V → V → Prop} {symm : autoParam (Std.Symm Adj) SimpleGraph.symm._autoParam}
  {loopless : autoParam (Std.Irrefl Adj) SimpleGraph.loopless._autoParam} {Adj_1 : V → V → Prop}
  {symm_1 : autoParam (Std.Symm Adj_1) SimpleGraph.symm._autoParam}
  {loopless_1 : autoParam (Std.Irrefl Adj_1) SimpleGraph.loopless._autoParam},
  { Adj := Adj, symm := symm, loopless := loopless } = { Adj := Adj_1, symm := symm_1, loopless := loopless_1 } →
    Adj = Adj_1
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.smul_div_one : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : MulAction R X] {p : R} {r : X} {s : ↥S}, (p /ₒ s) • (r /ₒ 1) = p • r /ₒ s
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey!_alter_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited α] {k : α} {f : Option β → Option β},
  (Std.DHashMap.Const.alter m k f).getKey! k = if (f (Std.DHashMap.Const.get? m k)).isSome = true then k else default
-- Std.Time.Format.Modifier
Std.Time.Year.twoDigit.sizeOf_spec : sizeOf Std.Time.Year.twoDigit = 1
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.mk.inj : ∀ {X : Type u_1} {inst : TopologicalSpace X} {U : Set X} {Y : Type u_2} {inst_1 : Zero Y} {toFun : X → Y}
  {supportWithinDomain' : Function.support toFun ⊆ U}
  {supportLocallyFiniteWithinDomain' : ∀ z ∈ U, ∃ t ∈ nhds z, (t ∩ Function.support toFun).Finite} {toFun_1 : X → Y}
  {supportWithinDomain'_1 : Function.support toFun_1 ⊆ U}
  {supportLocallyFiniteWithinDomain'_1 : ∀ z ∈ U, ∃ t ∈ nhds z, (t ∩ Function.support toFun_1).Finite},
  { toFun := toFun, supportWithinDomain' := supportWithinDomain',
        supportLocallyFiniteWithinDomain' := supportLocallyFiniteWithinDomain' } =
      { toFun := toFun_1, supportWithinDomain' := supportWithinDomain'_1,
        supportLocallyFiniteWithinDomain' := supportLocallyFiniteWithinDomain'_1 } →
    toFun = toFun_1
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.le_addConGen : ∀ {M : Type u_1} [inst : Add M] {r : M → M → Prop}, r ≤ ⇑(addConGen r)
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instOrdDiagnosticCode : Ord Lean.Lsp.DiagnosticCode
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.liftCycles.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) {A : C} (k k_1 : A ⟶ S.X₂) (e_k : k = k_1)
  (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) [inst_2 : S.HasLeftHomology],
  S.liftCycles k hk = S.liftCycles k_1 ⋯
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.foldr_eq_foldr_toList : ∀ {α : Type u} {δ : Type w} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} {f : α → β → δ → δ} {init : δ},
  Std.DTreeMap.Internal.Impl.foldr f init t =
    List.foldr (fun a b => f a.1 a.2 b) init (Std.DTreeMap.Internal.Impl.Const.toList t)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.map_sup : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (S T : Subalgebra R A),
  Subalgebra.map f (S ⊔ T) = Subalgebra.map f S ⊔ Subalgebra.map f T
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivWithinAt.of_finite : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E} [T1Space E],
  s.Finite → HasFDerivWithinAt f f' s x
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_ofList_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)} {k k' : α},
  (k == k') = true →
    ∀ {v fallback : β},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l → (k, v) ∈ l → (Std.ExtHashMap.ofList l).getD k' fallback = v
-- Init.GrindInstances.Ring.Fin
Lean.Grind.Fin.neg_mul : ∀ {n : ℕ} [NeZero n] (a b : Fin n), -a * b = -(a * b)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.linearMap_ext : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f]
  {N : Type u_6} {N' : Type u_7} [inst_6 : AddCommMonoid N] [inst_7 : Module R N] [inst_8 : AddCommMonoid N']
  [inst_9 : Module R N'] (f' : N →ₗ[R] N') [IsLocalizedModule S f'] ⦃g g' : M' →ₗ[R] N'⦄, g ∘ₗ f = g' ∘ₗ f → g = g'
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct : ∀ {C : Type uC} {inst : CategoryTheory.Category.{uC', uC} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  [self : CategoryTheory.Limits.HasBinaryBiproducts C] (P Q : C), CategoryTheory.Limits.HasBinaryBiproduct P Q
-- Mathlib.Tactic.Simproc.FinsetInterval
/-- Simproc to compute `Finset.Ioc a b` where `a` and `b` are numerals.

**Warnings**:
* With the standard depth recursion limit, this simproc can compute intervals of size 250 at most.
* Make sure to exclude `Finset.insert_eq_of_mem` from your simp call when using this simproc. This
  avoids a quadratic time performance hit.  -/
Finset.Ioc_ofNat_ofNat : Lean.Meta.Simp.Simproc
-- Mathlib.Topology.Category.TopPair
TopPair.Homotopy.symm_snd : ∀ {X Y : TopPair} {f₀ f₁ : X ⟶ Y} (F : TopPair.Homotopy f₀ f₁), F.symm.snd = F.snd.symm
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.map_eq_bot_iff_of_injective : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (H : AddSubgroup G) {f : G →+ N},
  Function.Injective ⇑f → (AddSubgroup.map f H = ⊥ ↔ H = ⊥)
-- Mathlib.Tactic.Linter.UnusedTactic
/-- `getNames mctx` extracts the names of all the local declarations implied by the
`MetavarContext` `mctx`.  -/
_private.Mathlib.Tactic.Linter.UnusedTactic.0.Mathlib.Linter.UnusedTactic.getNames : Lean.MetavarContext → List Lean.Name
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.linearMapAt_def_of_mem : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : AddCommMonoid F]
  [inst_5 : Module R F] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module R (E x)]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_8 : Bundle.Trivialization.IsLinear R e] {b : B}
  (hb : b ∈ e.baseSet), Bundle.Trivialization.linearMapAt R e b = ↑(Bundle.Trivialization.linearEquivAt R e b hb)
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.PrincipalSeg
/-- When `f : α <i β` and a functor `F : β ⥤ C`, this is the cocone
for `f.monotone.functor ⋙ F : α ⥤ C` whose point is `F.obj f.top`.  -/
PrincipalSeg.cocone : {α : Type u_1} →
  {β : Type u_2} →
    [inst : PartialOrder α] →
      [inst_1 : PartialOrder β] →
        (f : α <i β) →
          {C : Type u_3} →
            [inst_2 : CategoryTheory.Category.{v_1, u_3} C] →
              (F : CategoryTheory.Functor β C) → CategoryTheory.Limits.Cocone (⋯.functor.comp F)
-- Mathlib.RingTheory.Ideal.Span
Ideal.mem_span_insert : ∀ {α : Type u} [inst : Semiring α] {s : Set α} {x y : α},
  x ∈ Ideal.span (insert y s) ↔ ∃ a, ∃ z ∈ Ideal.span s, x = a * y + z
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
/-- Given a covariant derivative `cov` on a neighborhood `s` of a point `x`, if sections `σ` and
`σ'` agree on `s` and are differentiable at `x`, then `cov σ x = cov σ x'`.  -/
IsCovariantDerivativeOn.congr_of_eqOn : ∀ {𝕜 : 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]
  {cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x} {s : Set M},
  IsCovariantDerivativeOn F cov s →
    ∀ {σ σ' : (x : M) → V x} {x : M},
      MDiffAt (T% σ) x → MDiffAt (T% σ') x → s ∈ nhds x → (∀ x ∈ s, σ x = σ' x) → cov σ x = cov σ' x
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_alterKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {k k' : α} {fallback : β k'}
  {f : Option (β k) → Option (β k)} (l : List ((a : α) × β a)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValueCastD k' (Std.Internal.List.alterKey k f l) fallback =
      if heq : (k == k') = true then (Option.map (cast ⋯) (f (Std.Internal.List.getValueCast? k l))).getD fallback
      else Std.Internal.List.getValueCastD k' l fallback
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
AbstractSimplicialComplex.toPreAbstractSimplicialComplex : {ι : Type u_1} → AbstractSimplicialComplex ι → PreAbstractSimplicialComplex ι
-- Init.Data.Nat.Lemmas
_private.Init.Data.Nat.Lemmas.0.Nat.anyLTTR.loop.eq_2 : ∀ (n : ℕ) (f : (i : ℕ) → i < n → Bool) (i_1 : ℕ) (h : i_1 + 1 ≤ n),
  Nat.anyLTTR.loop✝ n f i_1.succ h = (f (n - (i_1 + 1)) ⋯ || Nat.anyLTTR.loop✝ n f i_1 ⋯)
-- Mathlib.Data.QPF.Multivariate.Basic
MvQPF.mk : {n : ℕ} →
  {F : TypeVec.{u} n → Type u_1} →
    [toMvFunctor : MvFunctor F] →
      (P : MvPFunctor.{u} n) →
        (abs : {α : TypeVec.{u} n} → ↑P α → F α) →
          (repr : {α : TypeVec.{u} n} → F α → ↑P α) →
            (∀ {α : TypeVec.{u} n} (x : F α), abs (repr x) = x) →
              (∀ {α β : TypeVec.{u} n} (f : α.Arrow β) (p : ↑P α), abs (MvFunctor.map f p) = MvFunctor.map f (abs p)) →
                MvQPF F
-- Lean.Elab.PreDefinition.Basic
_private.Lean.Elab.PreDefinition.Basic.0.Lean.Elab.addNonRecAux : Lean.LocalContext × Lean.LocalInstances →
  Lean.Elab.PreDefinition →
    Bool →
      List Lean.Name →
        optParam Bool true → optParam Bool true → optParam Bool false → optParam Bool false → Lean.Elab.TermElabM Unit
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_eq_top_iff : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a : M},
  MulArchimedeanClass.mk a = ⊤ ↔ a = 1
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.support_add : ∀ {R : Type u_1} [inst : Semiring R] {p q : SkewPolynomial R}, (p + q).support ⊆ p.support ∪ q.support
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
ChevalleyThm.MvPolynomialC.numBound_mono : ∀ {k₁ k₂ : ℕ} {D₁ D₂ : ℕ → ℕ},
  k₁ ≤ k₂ →
    ∀ (n : ℕ),
      (∀ i < n, D₁ i ≤ D₂ i) → ChevalleyThm.MvPolynomialC.numBound k₁ D₁ n ≤ ChevalleyThm.MvPolynomialC.numBound k₂ D₂ n
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.mk.congr_simp : ∀ (arr arr_1 : Array Batteries.UFNode) (e_arr : arr = arr_1)
  (parentD_lt : ∀ {i : ℕ}, i < arr.size → Batteries.UnionFind.parentD arr i < arr.size)
  (rankD_lt :
    ∀ {i : ℕ},
      Batteries.UnionFind.parentD arr i ≠ i →
        Batteries.UnionFind.rankD arr i < Batteries.UnionFind.rankD arr (Batteries.UnionFind.parentD arr i)),
  { arr := arr, parentD_lt := parentD_lt, rankD_lt := rankD_lt } = { arr := arr_1, parentD_lt := ⋯, rankD_lt := ⋯ }
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.instPartialOrder : {G : Type u_1} → [inst : Group G] → [inst_1 : TopologicalSpace G] → PartialOrder (OpenSubgroup G)
-- Mathlib.Algebra.Group.Basic
div_right_comm : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b c : α), a / b / c = a / c / b
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- Orbit-stabilizer theorem.  -/
MulAction.orbitProdStabilizerEquivGroup : (G : Type u) →
  {X : Type v} →
    [inst : Group G] → [inst_1 : MulAction G X] → (b : X) → ↑(MulAction.orbit G b) × ↥(MulAction.stabilizer G b) ≃ G
-- Mathlib.Analysis.Normed.Group.Ultra
/-- **Alias** of `IsUltrametricDist.exists_norm_finsetSum_le`.

---

Given a function `f : ι → M` and a finite set `t ⊆ ι`, we can always find `i : ι`,
belonging to `t` if `t` is nonempty, such that `‖∑ j ∈ t, f j‖ ≤ ‖f i‖`.  -/
IsUltrametricDist.exists_norm_finset_sum_le : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedAddCommGroup M] [IsUltrametricDist M] (t : Finset ι) [Nonempty ι]
  (f : ι → M), ∃ i, (t.Nonempty → i ∈ t) ∧ ‖∑ j ∈ t, f j‖ ≤ ‖f i‖
-- Mathlib.Data.Quot
Quotient.hrecOn'_mk'' : ∀ {α : Sort u_1} {s₁ : Setoid α} {φ : Quotient s₁ → Sort u_5} (f : (a : α) → φ (Quotient.mk'' a))
  (c : ∀ (a₁ a₂ : α), a₁ ≈ a₂ → f a₁ ≍ f a₂) (x : α), (Quotient.mk'' x).hrecOn' f c = f x
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
SimplexCategoryGenRel.toSimplexCategory_map_σ : ∀ {n : ℕ} (i : Fin (n + 1)),
  SimplexCategoryGenRel.toSimplexCategory.map (SimplexCategoryGenRel.σ i) = SimplexCategory.σ i
-- Std.Net.Addr
Std.Net.InterfaceAddress.mk.sizeOf_spec : ∀ (name : String) (physicalAddress : Std.Net.MACAddr) (isLoopback : Bool) (address netMask : Std.Net.IPAddr),
  sizeOf
      { name := name, physicalAddress := physicalAddress, isLoopback := isLoopback, address := address,
        netMask := netMask } =
    1 + sizeOf name + sizeOf physicalAddress + sizeOf isLoopback + sizeOf address + sizeOf netMask
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.IsSymmetric.clm_adjoint_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {A : E →L[𝕜] E}, (↑A).IsSymmetric → ContinuousLinearMap.adjoint A = A
-- Mathlib.MeasureTheory.Function.AEEqOfLIntegral
MeasureTheory.ae_le_const_iff_forall_gt_measure_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {β : Type u_2} [inst : LinearOrder β] [inst_1 : TopologicalSpace β]
  [OrderTopology β] [FirstCountableTopology β] {μ : MeasureTheory.Measure α} (f : α → β) (c : β),
  (∀ᵐ (x : α) ∂μ, f x ≤ c) ↔ ∀ (b : β), c < b → μ {x | b ≤ f x} = 0
-- Mathlib.Topology.Algebra.Module.LocallyConvex
LocallyConvexSpace.sInf : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {ts : Set (TopologicalSpace E)}, (∀ t ∈ ts, LocallyConvexSpace 𝕜 E) → LocallyConvexSpace 𝕜 E
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.instModule : {R : Type u_1} →
  [inst : CommRing R] →
    {K : Type u_2} →
      [inst_1 : LieRing K] →
        [inst_2 : LieAlgebra R K] →
          {L : Type u_3} →
            [inst_3 : LieRing L] → [inst_4 : LieAlgebra R L] → (ψ : L →ₗ⁅R⁆ LieDerivation R K K) → Module R (K ⋊⁅ψ⁆ L)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.filterENodes : (Lean.Meta.Grind.ENode → Lean.Meta.Grind.GoalM Bool) → Lean.Meta.Grind.GoalM (Array Lean.Meta.Grind.ENode)
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.πFunctorObj_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ] {X Y : C}
  (f : X ⟶ Y) (j : κ.ord.ToType),
  CategoryTheory.SmallObject.πFunctorObj I.homFamily
      (((CategoryTheory.SmallObject.iterationFunctor I κ).obj j).obj (CategoryTheory.Arrow.mk f)).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.relativeCellComplexιObjFObjSuccIso I κ f j).inv
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.SmallObject.relativeCellComplexιObj I κ f).incl.app (Order.succ j))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.πObj I κ f)
          (CategoryTheory.SmallObject.iterationFunctorObjObjRightIso I κ (CategoryTheory.Arrow.mk f) j).inv))
-- Mathlib.LinearAlgebra.QuadraticForm.Dual
LinearMap.isSymm_dualProd : ∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  LinearMap.IsSymm (LinearMap.dualProd R M)
-- Mathlib.Topology.EMetricSpace.Weak
/-- Given some (extended) distance function on `α`, it can be extended to a distance function on
`Option α` by defining `edist none a = 0` if `a = none` and `∞` otherwise.  -/
Option.toEDist : {α : Type u} → [EDist α] → EDist (Option α)
-- Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
CategoryTheory.Limits.isIndObject_colimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : Type v) [inst_1 : CategoryTheory.SmallCategory I]
  [CategoryTheory.IsFiltered I] (F : CategoryTheory.Functor I (CategoryTheory.Functor Cᵒᵖ (Type v))),
  (∀ (i : I), CategoryTheory.Limits.IsIndObject (F.obj i)) →
    CategoryTheory.Limits.IsIndObject (CategoryTheory.Limits.colimit F)
-- Mathlib.Order.Hom.WithTopBot
/-- Adjoins a `⊥` to the domain and codomain of a `LatticeHom`.  -/
LatticeHom.withBot : {α : Type u_1} →
  {β : Type u_2} → [inst : Lattice α] → [inst_1 : Lattice β] → LatticeHom α β → LatticeHom (WithBot α) (WithBot β)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.map₂Congr_hom_app_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B}
  {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : F.comp U ⟶ S.comp G) (β : G.obj T ⟶ V)
  {F' : CategoryTheory.Functor C A} {G' : CategoryTheory.Functor D B} (e₁ : F ≅ F') (e₂ : G ≅ G')
  (α' : F'.comp U ⟶ S.comp G') (β' : G'.obj T ⟶ V)
  (hα :
    CategoryTheory.CategoryStruct.comp α (S.whiskerLeft e₂.hom) =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight e₁.hom U) α')
  (hβ : β = CategoryTheory.CategoryStruct.comp (e₂.hom.app T) β') (X : CategoryTheory.CostructuredArrow S T),
  ((CategoryTheory.CostructuredArrow.map₂Congr α β e₁ e₂ α' β' hα hβ).hom.app X).left = e₁.hom.app X.left
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- `fderiv 𝕜 f` is smooth.  -/
ContDiff.fderiv_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {m n : WithTop ℕ∞},
  ContDiff 𝕜 n f → m + 1 ≤ n → ContDiff 𝕜 m (fderiv 𝕜 f)
-- Mathlib.Analysis.Normed.Affine.AddTorsor
/-- The midpoint of the segment AB is the same distance from A as it is from B.  -/
dist_left_midpoint_eq_dist_right_midpoint : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 V]
  [inst_5 : Invertible 2] (p₁ p₂ : P), dist p₁ (midpoint 𝕜 p₁ p₂) = dist p₂ (midpoint 𝕜 p₁ p₂)
-- Mathlib.NumberTheory.JacobiSum.Basic
/-- If `χ` is a multiplicative character of order `n ≥ 2` on a finite field `F`,
then `g(χ)^n = χ(-1) * #F * J(χ,χ) * J(χ,χ²) * ... * J(χ,χⁿ⁻²)`.  -/
gaussSum_pow_eq_prod_jacobiSum : ∀ {F : Type u_1} {R : Type u_2} [inst : Fintype F] [inst_1 : Field F] [inst_2 : CommRing R] [IsDomain R]
  {χ : MulChar F R} {ψ : AddChar F R},
  2 ≤ orderOf χ →
    ψ.IsPrimitive →
      gaussSum χ ψ ^ orderOf χ = χ (-1) * ↑(Fintype.card F) * ∏ i ∈ Finset.Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ i)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.boundariesToCycles₁_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (x : ↥(groupHomology.boundaries₁ A)),
  ↑((groupHomology.boundariesToCycles₁ A) x) = ↑x
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalarsEquivalenceOfRingEquiv_functor : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (e : R ≃+* S),
  (ModuleCat.restrictScalarsEquivalenceOfRingEquiv e).functor = ModuleCat.restrictScalars e.toRingHom
-- Mathlib.CategoryTheory.Limits.Over
CategoryTheory.Under.instHasLimitsOfShape : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {X : C} [CategoryTheory.Limits.HasLimitsOfShape J C],
  CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.Under X)
-- Mathlib.Algebra.Category.CommAlgCat.Monoidal
/-- The initial object of `CommAlgCat R` is `R` as an algebra over itself.  -/
CommAlgCat.isInitialSelf : {R : Type u} → [inst : CommRing R] → CategoryTheory.Limits.IsInitial (CommAlgCat.of R R)
-- Mathlib.Analysis.SpecialFunctions.Log.Summable
/-- **Alias** of `summable_finsetProd_of_summable_norm`. -/
summable_finset_prod_of_summable_norm : ∀ {ι : Type u_1} {R : Type u_2} [inst : NormedCommRing R] [NormOneClass R] {f : ι → R} [CompleteSpace R],
  (Summable fun i => ‖f i‖) → Summable fun s => ∏ i ∈ s, f i
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.rightUnitor_inv_left_fst_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  (Y : CategoryTheory.Over X) {Z : C} (h : Y.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst Y.hom (CategoryTheory.CategoryStruct.id X)) h) =
    h
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.presentation_R : ∀ (R : Type u) [inst : CommRing R] (n : ℕ) (M : Type u_1) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  (exteriorPower.presentation R n M).R = exteriorPower.presentation.Rels R (Fin n) M