mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Coxeter.Basic
_private.Mathlib.GroupTheory.Coxeter.Basic.0.CoxeterSystem.toMonoidHom_apply_symm_apply : ∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W)
  (a : PresentedGroup M.relationsSet), cs.mulEquiv.toMonoidHom (cs.mulEquiv.symm a) = a
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.Equiv.filterMap : ∀ {α₁ α₂ β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : LawfulMonad m] [inst_2 : Std.Iterator α₁ m β]
  [inst_3 : Std.Iterator α₂ m β] {f : β → Option γ} {ita : Std.IterM m β} {itb : Std.IterM m β},
  ita.Equiv itb → (Std.IterM.filterMap f ita).Equiv (Std.IterM.filterMap f itb)
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.Node.measure.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β) → Sort u_3)
  (h_1 :
    Lean.PersistentHashMap.Entry.null = Lean.PersistentHashMap.Entry.null → motive Lean.PersistentHashMap.Entry.null)
  (h_2 :
    (key : α) →
      (val : β) →
        Lean.PersistentHashMap.Entry.null = Lean.PersistentHashMap.Entry.entry key val →
          motive (Lean.PersistentHashMap.Entry.entry key val))
  (h_3 :
    (node : Lean.PersistentHashMap.Node α β) →
      Lean.PersistentHashMap.Entry.null = Lean.PersistentHashMap.Entry.ref node →
        motive (Lean.PersistentHashMap.Entry.ref node)),
  (match h_eq : Lean.PersistentHashMap.Entry.null with
    | Lean.PersistentHashMap.Entry.null => h_1 h_eq
    | Lean.PersistentHashMap.Entry.entry key val => h_2 key val h_eq
    | Lean.PersistentHashMap.Entry.ref node => h_3 node h_eq) =
    h_1 ⋯
-- Mathlib.Data.Fintype.Sum
Fintype.card_sum : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β],
  Fintype.card (α ⊕ β) = Fintype.card α + Fintype.card β
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Biprod.inl_ofComponents : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ Y₁ Y₂ : C} (f₁₁ : X₁ ⟶ Y₁) (f₁₂ : X₁ ⟶ Y₂)
  (f₂₁ : X₂ ⟶ Y₁) (f₂₂ : X₂ ⟶ Y₂),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
      (CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂) =
    CategoryTheory.CategoryStruct.comp f₁₁ CategoryTheory.Limits.biprod.inl +
      CategoryTheory.CategoryStruct.comp f₁₂ CategoryTheory.Limits.biprod.inr
-- Mathlib.Analysis.Normed.Group.Basic
mem_closedBall_iff_norm' : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] {a b : E} {r : ℝ}, b ∈ Metric.closedBall a r ↔ ‖a - b‖ ≤ r
-- Std.Data.HashMap.Lemmas
Std.HashMap.toList_filter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {f : α → β → Bool},
  (Std.HashMap.filter f m).toList.Perm (List.filter (fun p => f p.1 p.2) m.toList)
-- Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
/-- The extension to `Set.Iic (Order.succ j) ⥤ C` of a functor `F : Set.Iic j ⥤ C`,
when we specify a morphism `F.obj ⟨j, _⟩ ⟶ X`.  -/
CategoryTheory.SmallObject.SuccStruct.extendToSucc : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {J : Type u} →
      [inst_1 : LinearOrder J] →
        [inst_2 : SuccOrder J] →
          {j : J} →
            ¬IsMax j →
              (F : CategoryTheory.Functor (↑(Set.Iic j)) C) →
                {X : C} → (F.obj ⟨j, ⋯⟩ ⟶ X) → CategoryTheory.Functor (↑(Set.Iic (Order.succ j))) C
-- Mathlib.Order.Filter.Bases.Finite
Filter.hasBasis_generate : ∀ {α : Type u_1} (s : Set (Set α)), (Filter.generate s).HasBasis (fun t => t.Finite ∧ t ⊆ s) fun t => ⋂₀ t
-- Mathlib.Combinatorics.Enumerative.Composition
/-- The boundaries of a composition, i.e., the leftmost point of all the blocks. We include
a virtual point at the right of the last block, to make for a nice equiv with
`CompositionAsSet n`.  -/
Composition.boundaries : {n : ℕ} → Composition n → Finset (Fin (n + 1))
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.nnnorm_coe_le_nnnorm : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
  (f : BoundedContinuousFunction α β) (x : α), ‖f x‖₊ ≤ ‖f‖₊
-- Init.Data.Vector.Lemmas
Vector.none_eq_getElem?_iff : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ}, none = xs[i]? ↔ n ≤ i
-- Lean.Hygiene
Lean.NameSanitizerState.options : Lean.NameSanitizerState → Lean.Options
-- Mathlib.Algebra.FreeMonoid.Count
FreeMonoid.countP'.eq_1 : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (l : FreeMonoid α),
  FreeMonoid.countP' p l = List.countP (fun b => decide (p b)) (FreeMonoid.toList l)
-- Mathlib.Data.Complex.Basic
Complex.ofReal_nnqsmul : ∀ (q : ℚ≥0) (r : ℝ), ↑(q • r) = q • ↑r
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquivClass.coe_symm_apply_apply : ∀ {α : Type u_9} {β : Type u_10} [inst : Add α] [inst_1 : Add β] {F : Type u_11} [inst_2 : EquivLike F α β]
  [inst_3 : AddEquivClass F α β] (e : F) (x : α), (↑e).symm (e x) = x
-- Mathlib.CategoryTheory.Retract
CategoryTheory.RetractArrow.op_r : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W}
  (h : CategoryTheory.RetractArrow f g),
  h.op.r = CategoryTheory.Arrow.homMk (CategoryTheory.Arrow.Hom.right h.i).op (CategoryTheory.Arrow.Hom.left h.i).op ⋯
-- Mathlib.Data.Finsupp.Interval
Finsupp.rangeSingleton_apply : ∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] (f : ι →₀ α) (i : ι), f.rangeSingleton i = {f i}
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalSubgroup.mk.sizeOf_spec : ∀ {G : Type u} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : SizeOf G] (toOpenSubgroup : OpenSubgroup G)
  (isNormal' : autoParam (↑toOpenSubgroup).Normal OpenNormalSubgroup.isNormal'._autoParam),
  sizeOf { toOpenSubgroup := toOpenSubgroup, isNormal' := isNormal' } = 1 + sizeOf toOpenSubgroup + sizeOf isNormal'
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.preimage_image_mk_eq_iUnion_image : ∀ {α : Type u_1} [inst : Group α] (N : Subgroup α) (s : Set α),
  QuotientGroup.mk ⁻¹' QuotientGroup.mk '' s = ⋃ x, (fun x_1 => x_1 * ↑x) '' s
-- Init.Data.Nat.Gcd
Nat.gcd_rec : ∀ (m n : ℕ), m.gcd n = (n % m).gcd m
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
/-- Taking the reverse of the product a list of $n$ vectors lifted via `ι` is equivalent to
taking the product of the reverse of that list.  -/
CliffordAlgebra.reverse_prod_map_ι : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (l : List M),
  CliffordAlgebra.reverse (List.map (⇑(CliffordAlgebra.ι Q)) l).prod =
    (List.map (⇑(CliffordAlgebra.ι Q)) l).reverse.prod
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.map_update_add : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) (v : ι → M)
  [inst_5 : DecidableEq ι] (i : ι) (x y : M),
  f (Function.update v i (x + y)) = f (Function.update v i x) + f (Function.update v i y)
-- Mathlib.Tactic.NormNum.NatLog
Mathlib.Meta.NormNum.nat_log_one : ∀ (n : ℕ), Nat.log 1 n = 0
-- Mathlib.Logic.Equiv.Defs
Equiv.subsingleton_congr : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), Subsingleton α ↔ Subsingleton β
-- Mathlib.Analysis.Convex.Gauge
setOfPred_gauge_lt_eq' : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E},
  Absorbent ℝ s → ∀ (a : ℝ), {x | gauge s x < a} = ⋃ r, ⋃ (_ : 0 < r), ⋃ (_ : r < a), r • s
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.module' : {R' : Type u'} →
  {R : Type u} →
    {A : Type v} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            (S : Subalgebra R A) →
              [inst_3 : Semiring R'] →
                [inst_4 : SMul R' R] → [inst_5 : Module R' A] → [IsScalarTower R' R A] → Module R' ↥S
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.instZero : {R : Type u_3} →
  {M : Type u_4} →
    {N : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] → [inst_3 : AddCommMonoid N] → [inst_4 : Module R N] → Zero (QuadraticMap R M N)
-- Mathlib.Algebra.MvPolynomial.Comap
MvPolynomial.comap_comp_apply : ∀ {σ : Type u_1} {τ : Type u_2} {υ : Type u_3} {R : Type u_4} [inst : CommSemiring R]
  (f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R) (g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R) (x : υ → R),
  MvPolynomial.comap (g.comp f) x = MvPolynomial.comap f (MvPolynomial.comap g x)
-- Aesop.Script.StructureDynamic
Aesop.Script.DynStructureM.Context.mk.injEq : ∀ (steps steps_1 : Lean.PHashMap Lean.MVarId (ℕ × Aesop.Script.Step)),
  ({ steps := steps } = { steps := steps_1 }) = (steps = steps_1)
-- Init.Data.Array.Lemmas
Array.foldl_push_eq_append : ∀ {α : Type u_1} {β : Type u_2} {stop : ℕ} {as : Array α} {bs : Array β} {f : α → β},
  stop = as.size → Array.foldl (fun acc a => acc.push (f a)) bs as 0 stop = bs ++ Array.map f as
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.le_normalizer_iff_addCommutator_le_right : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, H ≤ AddSubgroup.normalizer ↑K ↔ ⁅H, K⁆ ≤ K
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.FactorSet.coe_add : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] {a b : Multiset { a // Irreducible a }}, ↑(a + b) = ↑a + ↑b
-- Batteries.Tactic.PrintDependents
/-- Collects the result of a `CollectDependents` query.  -/
Batteries.Tactic.CollectDependents.State : Type
-- Init.Data.List.Lemmas
List.map_eq_cons_iff' : ∀ {α : Type u_1} {β : Type u_2} {b : β} {l₂ : List β} {f : α → β} {l : List α},
  List.map f l = b :: l₂ ↔ Option.map f l.head? = some b ∧ Option.map (List.map f) l.tail? = some l₂
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.instFullSkeletonFromSkeleton : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C], (CategoryTheory.fromSkeleton C).Full
-- Mathlib.Order.CompleteLattice.Basic
biInf_le_eq_inf : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Type u_8} [inst_1 : PartialOrder ι] (f : ι → α) (i : ι),
  ⨅ j, ⨅ (_ : j ≤ i), f j = (⨅ j, ⨅ (_ : j < i), f j) ⊓ f i
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castSucc_Ioc_castSucc : ∀ {n : ℕ} (i j : Fin n), Fin.castSucc ⁻¹' Set.Ioc i.castSucc j.castSucc = Set.Ioc i j
-- Batteries.Classes.Order
/-- Class for types where the ordering function is compatible with the `LE`, `LT` and `Eq`.  -/
Std.LawfulOrd : (α : Type u_1) → [LE α] → [LT α] → [Ord α] → Prop
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.opensRange_homOfLE : ∀ {X : AlgebraicGeometry.Scheme} {U V : X.Opens} (e : U ≤ V),
  AlgebraicGeometry.Scheme.Hom.opensRange (X.homOfLE e) = (TopologicalSpace.Opens.map V.ι.base).obj U
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.le_normalClosure : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H ≤ Subgroup.normalClosure ↑H
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.adjoin_eq : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] (s : NonUnitalStarSubalgebra R A), NonUnitalStarAlgebra.adjoin R ↑s = s
-- Mathlib.Algebra.Homology.ImageToKernel
imageToKernel_comp_left : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V}
  (f : A ⟶ B) (g : B ⟶ C) [inst_2 : CategoryTheory.Limits.HasKernels V] [inst_3 : CategoryTheory.Limits.HasImages V]
  {Z : V} (h : Z ⟶ A) (w : CategoryTheory.CategoryStruct.comp f g = 0),
  imageToKernel (CategoryTheory.CategoryStruct.comp h f) g ⋯ =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp h f)).ofLE
        (CategoryTheory.Limits.imageSubobject f) ⋯)
      (imageToKernel f g w)
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.stabilizer_union_eq_right : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] {s t : Set α},
  Disjoint s t →
    AddAction.stabilizer G t ≤ AddAction.stabilizer G s →
      AddAction.stabilizer G (s ∪ t) ≤ AddAction.stabilizer G s →
        AddAction.stabilizer G (s ∪ t) = AddAction.stabilizer G t
-- Mathlib.Algebra.Star.Basic
Pi.star_single : ∀ {ι : Type u_1} {R : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddMonoid (R i)]
  [inst_2 : (i : ι) → StarAddMonoid (R i)] (i : ι) (r : R i), star (Pi.single i r) = Pi.single i (star r)
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.customEliminatorExt : Lean.SimpleScopedEnvExtension Lean.Meta.CustomEliminator Lean.Meta.CustomEliminators
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Reachable.mono : ∀ {V : Type u} {u v : V} {G G' : SimpleGraph V}, G ≤ G' → G.Reachable u v → G'.Reachable u v
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
/-- Given `F : C ⥤ D`, this is the partial adjoint functor `F.PartialRightAdjointSource ⥤ C`.  -/
CategoryTheory.Functor.partialRightAdjoint : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) → CategoryTheory.Functor F.PartialRightAdjointSource C
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
CliffordAlgebra.even.lift.aux_mul : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {A : Type u_3} [inst_3 : Ring A] [inst_4 : Algebra R A] (f : CliffordAlgebra.EvenHom Q A)
  (x y : ↥(CliffordAlgebra.even Q)),
  (CliffordAlgebra.even.lift.aux f) (x * y) = (CliffordAlgebra.even.lift.aux f) x * (CliffordAlgebra.even.lift.aux f) y
-- Mathlib.LinearAlgebra.Dimension.OrzechProperty
linearIndependent_iff_card_le_finrank_span : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [OrzechProperty R] [inst_2 : AddCommMonoid M] [inst_3 : Module R M]
  [Nontrivial R] {ι : Type u_3} [inst_5 : Fintype ι] {b : ι → M},
  LinearIndependent R b ↔ Fintype.card ι ≤ Set.finrank R (Set.range b)
-- Mathlib.Analysis.Normed.Module.Convex
convexOn_univ_dist : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (z : E),
  ConvexOn ℝ Set.univ fun z' => dist z' z
-- Std.Http.Protocol.H1.Config
/-- Maximum allowed chunk payload size in bytes (default: 8 MiB).
 -/
Std.Http.Protocol.H1.Config.maxChunkSize : Std.Http.Protocol.H1.Config → ℕ
-- Mathlib.GroupTheory.Abelianization.Defs
Abelianization.coe_lift_symm : ∀ {G : Type u} [inst : Group G] {A : Type v} [inst_1 : CommGroup A],
  ⇑Abelianization.lift.symm = fun x => x.comp Abelianization.of
-- Mathlib.Algebra.Ring.Units
Units.divp_sub_divp_same : ∀ {α : Type u} [inst : Ring α] (a b : α) (u : αˣ), a /ₚ u - b /ₚ u = (a - b) /ₚ u
-- Lean.Data.Lsp.CodeActions
/-- Whether we can [register capabilities dynamically](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#client_registerCapability).  -/
Lean.Lsp.CodeActionClientCapabilities.dynamicRegistration? : Lean.Lsp.CodeActionClientCapabilities → Option Bool
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.op_iSup : ∀ {ι : Sort u_1} {M : Type u_2} [inst : MulOneClass M] (S : ι → Submonoid M), (iSup S).op = ⨆ i, (S i).op
-- Mathlib.Analysis.Calculus.MeanValue
IsOpen.exists_eq_add_of_fderiv_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
  [inst_2 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f g : E → G} {s : Set E},
  IsOpen s →
    IsPreconnected s →
      DifferentiableOn 𝕜 f s →
        DifferentiableOn 𝕜 g s → Set.EqOn (fderiv 𝕜 f) (fderiv 𝕜 g) s → ∃ a, Set.EqOn f (fun x => g x + a) s
-- Mathlib.Order.Hom.Bounded
BotHom.instMin.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst_1 : SemilatticeInf β] [inst_2 : OrderBot β],
  BotHom.instMin = { min := fun f g => { toFun := ⇑f ⊓ ⇑g, map_bot' := ⋯ } }
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIoo_self : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α}, Set.uIoo a a = ∅
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
/-- The image of a spectral by a triangulated functor.  -/
CategoryTheory.Triangulated.SpectralObject.mapTriangulatedFunctor : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
          [inst_3 : CategoryTheory.HasShift C ℤ] →
            [inst_4 : CategoryTheory.Preadditive C] →
              [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
                [inst_6 : CategoryTheory.Pretriangulated C] →
                  {D : Type u_3} →
                    [inst_7 : CategoryTheory.Category.{v_3, u_3} D] →
                      [inst_8 : CategoryTheory.Limits.HasZeroObject D] →
                        [inst_9 : CategoryTheory.HasShift D ℤ] →
                          [inst_10 : CategoryTheory.Preadditive D] →
                            [inst_11 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] →
                              [inst_12 : CategoryTheory.Pretriangulated D] →
                                CategoryTheory.Triangulated.SpectralObject C ι →
                                  (F : CategoryTheory.Functor C D) →
                                    [inst_13 : F.CommShift ℤ] →
                                      [F.IsTriangulated] → CategoryTheory.Triangulated.SpectralObject D ι
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The bifunctor `F - ⊗ F -`.  -/
CategoryTheory.MonoidalCategory.curriedTensorPre : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [CategoryTheory.MonoidalCategory D] →
          CategoryTheory.Functor C D → CategoryTheory.Functor C (CategoryTheory.Functor C D)
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.inverse'.eq_1 : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : SMul M X] {Y : Type u_6} [inst_1 : SMul N Y]
  {φ' : N → M} (f : X →ₑ[φ] Y) (g : Y → X) (k : Function.RightInverse φ' φ) (h₁ : Function.LeftInverse g ⇑f)
  (h₂ : Function.RightInverse g ⇑f), f.inverse' g k h₁ h₂ = { toFun := g, map_smul' := ⋯ }
-- Mathlib.Geometry.Manifold.StructureGroupoid
/-- To construct a groupoid, one may consider classes of open partial homeomorphisms such that
both the function and its inverse have some property. If this property is stable under composition,
one gets a groupoid. `Pregroupoid` bundles the properties needed for this construction, with the
groupoid of smooth functions with smooth inverses as an application.  -/
Pregroupoid : (H : Type u_2) → [TopologicalSpace H] → Type u_2
-- Init.PropLemmas
ite_then_decide_not_self : ∀ (p : Prop) [h : Decidable p] {w : Decidable p} (q : Bool), (if p then !decide p else q) = (!decide p && q)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.comap_iInf : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {ι : Sort u_1} (f : R →+* S)
  (s : ι → Subsemiring S), Subsemiring.comap f (iInf s) = ⨅ i, Subsemiring.comap f (s i)
-- Init.Data.Option.Lemmas
Option.min_guard_some : ∀ {α : Type u_1} [inst : Min α] [Std.IdempotentOp min] {x : α} {p : α → Bool},
  Option.guard p x ⊓ some x = Option.guard p x
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.EvalTacticFailure.mk.sizeOf_spec : ∀ (exception : Lean.Exception) (state : Lean.Elab.Tactic.Grind.SavedState),
  sizeOf { exception := exception, state := state } = 1 + sizeOf exception + sizeOf state
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Real.enorm_rpow_of_nonneg : ∀ {x y : ℝ}, 0 ≤ x → 0 ≤ y → ‖x ^ y‖ₑ = ‖x‖ₑ ^ y
-- Std.Data.DHashMap.Raw
/-- Returns `true` if the hash map contains no mappings.

Note that if your `BEq` instance is not reflexive or your `Hashable` instance is not
lawful, then it is possible that this function returns `false` even though is not possible
to get anything out of the hash map.
 -/
Std.DHashMap.Raw.isEmpty : {α : Type u} → {β : α → Type v} → Std.DHashMap.Raw α β → Bool
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isBigO_iff_exists_eq_mul : ∀ {α : Type u_1} {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {l : Filter α} {u v : α → 𝕜},
  u =O[l] v ↔ ∃ φ, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v
-- Mathlib.Algebra.Group.Action.Pi
Pi.isScalarTower : ∀ {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [inst : SMul M N] [inst_1 : (i : ι) → SMul N (α i)]
  [inst_2 : (i : ι) → SMul M (α i)] [∀ (i : ι), IsScalarTower M N (α i)], IsScalarTower M N ((i : ι) → α i)
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.sum_hom₂ : ∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : AddMonoid M] [inst_1 : AddMonoid N]
  [inst_2 : AddMonoid P] (l : List ι) (f : M → N → P),
  (∀ (a b : M) (c d : N), f (a + b) (c + d) = f a c + f b d) →
    f 0 0 = 0 →
      ∀ (f₁ : ι → M) (f₂ : ι → N),
        (List.map (fun i => f (f₁ i) (f₂ i)) l).sum = f (List.map f₁ l).sum (List.map f₂ l).sum
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.inclusion.congr_simp : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {E F : IntermediateField K L}
  (hEF : E ≤ F), IntermediateField.inclusion hEF = IntermediateField.inclusion hEF
-- Mathlib.Topology.Constructions.SumProd
Filter.EventuallyLE.prodMap_nhds : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {α : Type u_5} {β : Type u_6}
  [inst_2 : LE α] [inst_3 : LE β] {f₁ f₂ : X → α} {g₁ g₂ : Y → β} {x : X} {y : Y},
  f₁ ≤ᶠ[nhds x] f₂ → g₁ ≤ᶠ[nhds y] g₂ → Prod.map f₁ g₁ ≤ᶠ[nhds (x, y)] Prod.map f₂ g₂
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
le_mul_of_le_left : ∀ {α : Type u} [inst : Mul α] [inst_1 : Preorder α] [CanonicallyOrderedMul α] {a b c : α}, a ≤ b → a ≤ b * c
-- Mathlib.RingTheory.PowerSeries.Substitution
/-- Substitution by `p` commutes with scalar homothety.  -/
PowerSeries.subst_rescale_of_degree_eq_one : ∀ {R : Type u_2} [inst : CommRing R] (a : R) {σ : Type u_7} (p : MvPowerSeries σ R),
  (∀ d ∈ Function.support p, Finsupp.degree d = 1) →
    ∀ (f : PowerSeries R),
      PowerSeries.subst p ((PowerSeries.rescale a) f) =
        (MvPowerSeries.rescale (Function.const σ a)) (PowerSeries.subst p f)
-- Lean.Elab.Tactic.Config
_private.Lean.Elab.Tactic.Config.0.Lean.Elab.Tactic.checkCommandConfigElab : Lean.Linter.MissingDocs.SimpleHandler
-- Init.Grind.Config
/-- A `grind` configuration that only uses `ring`.
 -/
Lean.Grind.GrobnerConfig : Type
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonRpcConnected.fromJson : Lean.Json → Except String Lean.Lsp.RpcConnected
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.mk.eq_1 : ∀ {α : Type u} (L : List (α × Bool)), FreeAddGroup.mk L = Quot.mk FreeAddGroup.Red.Step L
-- Mathlib.CategoryTheory.Limits.Preserves.Limits
CategoryTheory.preservesLimitNatIso_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J]
  [inst_3 : CategoryTheory.Limits.PreservesLimitsOfShape J G] [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J D]
  [inst_5 : CategoryTheory.Limits.HasLimitsOfShape J C] (X : CategoryTheory.Functor J C),
  (CategoryTheory.preservesLimitNatIso G).inv.app X = (CategoryTheory.preservesLimitIso G X).inv
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get_union_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (mem : k ∈ m₂), (m₁ ∪ m₂).get k ⋯ = m₂.get k mem