mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
/-- If `e : G ≃* H` is a multiplicative equivalence between two monoids and
` ∀ (a : G) (x : A), a • x = (e a) • x`, then `SkewMonoidAlgebra.domCongr e` is an
algebra equivalence between their skew monoid algebras.  -/
SkewMonoidAlgebra.domCongrAlg : (k : Type u_1) →
  {G : Type u_2} →
    {H : Type u_3} →
      (A : Type u_4) →
        [inst : Monoid G] →
          [inst_1 : Monoid H] →
            [inst_2 : Semiring A] →
              [inst_3 : CommSemiring k] →
                [inst_4 : Algebra k A] →
                  [inst_5 : MulSemiringAction G A] →
                    [inst_6 : MulSemiringAction H A] →
                      [inst_7 : SMulCommClass G k A] →
                        [inst_8 : SMulCommClass H k A] →
                          {e : G ≃* H} →
                            (∀ (a : G) (x : A), a • x = e a • x) → SkewMonoidAlgebra A G ≃ₐ[k] SkewMonoidAlgebra A H
-- Mathlib.Logic.Equiv.Sum
/-- Type product is left distributive with respect to type sum up to an equivalence.  -/
Equiv.prodSumDistrib : (α : Type u_9) → (β : Type u_10) → (γ : Type u_11) → α × (β ⊕ γ) ≃ α × β ⊕ α × γ
-- Mathlib.Topology.Compactness.CountablyCompact
/-- If `f : X → Y` is an inducing map, the image `f '' s` of a set `s` is sequentially compact
if and only if `s` is sequentially compact.  -/
Topology.IsInducing.isSeqCompact_iff : ∀ {E : Type u_2} {F : Type u_3} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace F] {A : Set E} {f : E → F},
  Topology.IsInducing f → (IsSeqCompact A ↔ IsSeqCompact (f '' A))
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getEntryLT? : {α : Type u} → {β : α → Type v} → [Ord α] → α → Std.DTreeMap.Internal.Impl α β → Option ((a : α) × β a)
-- Mathlib.Order.Types.Defs
/-- An order type lifted to a lower or equal universe equals itself.  -/
OrderType.lift_id' : ∀ (o : OrderType.{max u v}), OrderType.lift.{u, max u v} o = o
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
/-- The central point of the walking cospan.  -/
CategoryTheory.Limits.WalkingCospan.one : CategoryTheory.Limits.WalkingCospan
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.piCongrLeft_symm_apply : ∀ {ι : Type u_7} {ι' : Type u_8} (S : ι' → Type u_9) (e : ι ≃ ι') [inst : (i : ι') → NonUnitalNonAssocSemiring (S i)]
  (a : (i : ι') → S i) (i : ι), (RingEquiv.piCongrLeft S e).symm a i = a (e i)
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.comapDomain'_single : ∀ {ι : Type u} {β : ι → Type v} {κ : Type u_1} [inst : DecidableEq ι] [inst_1 : DecidableEq κ]
  [inst_2 : (i : ι) → Zero (β i)] (h : κ → ι) {h' : ι → κ} (hh' : Function.LeftInverse h' h) (k : κ) (x : β (h k)),
  (DFinsupp.comapDomain' h hh' fun₀ | h k => x) = fun₀ | k => x
-- Mathlib.CategoryTheory.Action.Limits
/-- `F.mapAction : Action V G ⥤ Action W G` preserves the limit of some `K : J ⥤ Action V G` if
`K ⋙ forget V G` has a limit and `F` preserves the limit of `K ⋙ forget V G`.  -/
Action.Functor.mapActionPreservesLimit_of_preserves : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {W : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_2, u_3} W] (F : CategoryTheory.Functor V W) (G : Type u_4) [inst_2 : Monoid G]
  {J : Type u_5} [inst_3 : CategoryTheory.Category.{v_3, u_5} J] (K : CategoryTheory.Functor J (Action V G))
  [CategoryTheory.Limits.HasLimit (K.comp (Action.forget V G))]
  [CategoryTheory.Limits.PreservesLimit (K.comp (Action.forget V G)) F],
  CategoryTheory.Limits.PreservesLimit K (F.mapAction G)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.nat_mul_aleph0 : ∀ {n : ℕ}, n ≠ 0 → ↑n * Cardinal.aleph0 = Cardinal.aleph0
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- If F preserves one colimit cocone for the diagram K,
then it preserves any colimit cocone for K.  -/
CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C}
  {F : CategoryTheory.Functor C D} {t : CategoryTheory.Limits.Cocone K} (h : CategoryTheory.Limits.IsColimit t)
  (hF : CategoryTheory.Limits.IsColimit (F.mapCocone t)), CategoryTheory.Limits.PreservesColimit K F
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.fromNormalizedChainComplex_toNormalizedChainComplex : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C),
  CategoryTheory.CategoryStruct.comp (X.fromNormalizedChainComplex R) (X.toNormalizedChainComplex R) =
    CategoryTheory.CategoryStruct.id (X.normalizedChainComplex R)
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.unop_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Cᵒᵖ} (P : HomotopicalAlgebra.PrepathObject A),
  P.unop.π = P.ι.unop
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.add : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {l : Filter α} {f₁ f₂ : α → E'}, f₁ =O[l] g → f₂ =O[l] g → (fun x => f₁ x + f₂ x) =O[l] g
-- Std.Sat.AIG.CNF
/-- `State.Inv` holds for the CNF that we produce for a `Decl.atom`
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.Inv_atomToCNF : ∀ {upper : ℕ} {aig : Std.Sat.AIG ℕ} {a : ℕ} {h : upper < aig.decls.size},
  aig.decls[upper] = Std.Sat.AIG.Decl.atom a →
    Std.Sat.AIG.toCNF.State.Inv✝ aig (Std.Sat.AIG.Decl.atomToCNF✝ upper (a + aig.decls.size))
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- The measure of the intersection of a decreasing sequence of measurable
sets indexed by a linear order with first countable topology is the limit of the measures.  -/
MeasureTheory.tendsto_measure_biInter_gt : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_8} [inst : LinearOrder ι]
  [inst_1 : TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] {s : ι → Set α} {a : ι},
  (∀ r > a, MeasureTheory.NullMeasurableSet (s r) μ) →
    (∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j) →
      (∃ r > a, μ (s r) ≠ ⊤) → Filter.Tendsto (⇑μ ∘ s) (nhdsWithin a (Set.Ioi a)) (nhds (μ (⋂ r, ⋂ (_ : r > a), s r)))
-- Init.Data.List.MinMaxOn
_private.Init.Data.List.MinMaxOn.0.List.minOn?.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (x : α) (xs : List α) (h_1 : Unit → motive [])
  (h_2 : (x : α) → (xs : List α) → motive (x :: xs)),
  (match x :: xs with
    | [] => h_1 ()
    | x :: xs => h_2 x xs) =
    h_2 x xs
-- Mathlib.AlgebraicGeometry.Gluing
/-- (Implementation). The glued scheme of a glue data.
This should not be used outside this file. Use `AlgebraicGeometry.Scheme.GlueData.glued` instead.  -/
AlgebraicGeometry.Scheme.GlueData.gluedScheme : AlgebraicGeometry.Scheme.GlueData → AlgebraicGeometry.Scheme
-- Mathlib.RingTheory.Norm.Basic
/-- This is `Algebra.norm_eq_zero_iff` composed with `Algebra.norm_apply`.  -/
Algebra.norm_eq_zero_iff' : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] [IsDomain R] [IsDomain S]
  [Module.Free R S] [Module.Finite R S] {x : S}, LinearMap.det ((LinearMap.mul R S) x) = 0 ↔ x = 0
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.root?.eq_1 : ∀ {α : Type u_1}, RBTree.RBNode.nil.root? = none
-- Mathlib.Algebra.Notation.Support
Function.mulSupport_extend_one_subset : ∀ {ι : Type u_1} {κ : Type u_2} {N : Type u_4} [inst : One N] {f : ι → κ} {g : ι → N},
  Function.mulSupport (Function.extend f g 1) ⊆ f '' Function.mulSupport g
-- Mathlib.RingTheory.Coalgebra.Basic
/-- The `R`-module whose elements are dependent functions `(i : ι) → A i` which are zero on all but
finitely many elements of `ι` has a coalgebra structure.

The coproduct `Δ` is given by `Δ(fᵢ a) = fᵢ a₁ ⊗ fᵢ a₂` where `Δ(a) = a₁ ⊗ a₂` and the counit `ε`
by `ε(fᵢ a) = ε(a)`, where `fᵢ a` is the function sending `i` to `a` and all other elements of `ι`
to zero.  -/
DFinsupp.instCoalgebra : (R : Type u) →
  (ι : Type v) →
    (A : ι → Type w) →
      [DecidableEq ι] →
        [inst : CommSemiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (A i)] →
            [inst_2 : (i : ι) → Module R (A i)] → [(i : ι) → Coalgebra R (A i)] → Coalgebra R (Π₀ (i : ι), A i)
-- Std.Data.HashMap.IteratorLemmas
Std.HashMap.Raw.toList_valuesIter_eq_toList_map_snd : ∀ {α β : Type u} {m : Std.HashMap.Raw α β}, m.valuesIter.toList = List.map Prod.snd m.toList
-- Init.Data.List.Sort.Lemmas
_private.Init.Data.List.Sort.Lemmas.0.List.merge.eq_3 : ∀ {α : Type u_1} (le : α → α → Bool) (x : α) (xs_2 : List α) (y : α) (ys_2 : List α),
  (x :: xs_2).merge (y :: ys_2) le =
    if le x y = true then x :: xs_2.merge (y :: ys_2) le else y :: (x :: xs_2).merge ys_2 le
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.symm_symm : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (f : α ≃+o β), f.symm.symm = f
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.card_le_preBeth : ∀ (o : Ordinal.{u_1}), o.card ≤ Cardinal.preBeth o
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.coe_injective : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M],
  Function.Injective DFunLike.coe
-- Lean.Data.LOption
Lean.LOption.undef : {α : Type u} → Lean.LOption α
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
_private.Lean.Meta.Tactic.Grind.Arith.CommRing.RingId.0.Lean.Meta.Grind.Arith.CommRing.getNonCommSemiringId?.go? : Lean.Expr → Lean.Meta.Grind.GoalM (Option ℕ)
-- Mathlib.RepresentationTheory.Intertwining
/-- If `g` is a central element of a monoid `G`, then this is the action of `g`, considered as an
intertwining map from any representation of `G` to itself.  -/
Representation.IntertwiningMap.centralMul : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommSemiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid V] →
            [inst_3 : Module A V] → (ρ : Representation A G V) → (g : G) → g ∈ Submonoid.center G → ρ.IntertwiningMap ρ
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
CategoryTheory.bicategoricalComp.eq_1 : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g h i : a ⟶ b}
  [inst_1 : CategoryTheory.BicategoricalCoherence g h] (η : f ⟶ g) (θ : h ⟶ i),
  CategoryTheory.bicategoricalComp η θ =
    CategoryTheory.CategoryStruct.comp η
      (CategoryTheory.CategoryStruct.comp CategoryTheory.BicategoricalCoherence.iso.hom θ)
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_right_le_size_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m₂.size ≤ (m₁ ∪ m₂).size
-- Mathlib.Data.ENat.Basic
instSubENat : Sub ℕ∞
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_eq_some_getD_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {a fallback : α},
  t.contains a = true → t.get? a = some (t.getD a fallback)
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
/-- The inverse map in `rTensor.equiv_of_rightInverse` (computably, given a right inverse)  -/
rTensor.inverse_of_rightInverse : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      {P : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : AddCommGroup N] →
              [inst_3 : AddCommGroup P] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Module R P] →
                      {f : M →ₗ[R] N} →
                        {g : N →ₗ[R] P} →
                          (Q : Type u_5) →
                            [inst_7 : AddCommGroup Q] →
                              [inst_8 : Module R Q] →
                                {h : P → N} →
                                  Function.Exact ⇑f ⇑g →
                                    Function.RightInverse h ⇑g →
                                      TensorProduct R P Q →ₗ[R] TensorProduct R N Q ⧸ (LinearMap.rTensor Q f).range
-- Mathlib.NumberTheory.RamificationInertia.Ramification
Ideal.IsDedekindDomain.ramificationIdx'_ne_zero : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R} {P : Ideal S}
  [IsDedekindDomain S],
  Ideal.map (algebraMap R S) p ≠ ⊥ → P.IsPrime → Ideal.map (algebraMap R S) p ≤ P → p.ramificationIdx' P ≠ 0
-- Lean.Parser.Basic
Lean.Parser.quotedCharFn : Lean.Parser.ParserFn
-- Mathlib.CategoryTheory.SmallRepresentatives
/-- Index set of a representative set of all categories `C` which satisfy
`HasCardinalLT C κ`, see `SmallCategoryCardinalLT.categoryFamily`.  -/
CategoryTheory.SmallCategoryCardinalLT : Cardinal.{w} → Type w
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.prod_top : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] [inst_4 : NonUnitalSemiring B] [inst_5 : StarRing B] [inst_6 : Module R B] [inst_7 : StarRing R]
  [inst_8 : IsScalarTower R A A] [inst_9 : SMulCommClass R A A] [inst_10 : StarModule R A]
  [inst_11 : IsScalarTower R B B] [inst_12 : SMulCommClass R B B] [inst_13 : StarModule R B], ⊤.prod ⊤ = ⊤
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isEmpty_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  (t₁ ∪ t₂).isEmpty = (t₁.isEmpty && t₂.isEmpty)
-- Mathlib.Probability.Distributions.Gaussian.Multivariate
ProbabilityTheory.measurePreserving_eval_multivariateGaussian : ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {μ : EuclideanSpace ℝ ι} {S : Matrix ι ι ℝ},
  S.PosSemidef →
    ∀ {i : ι},
      MeasureTheory.MeasurePreserving (fun x => x.ofLp i) (ProbabilityTheory.multivariateGaussian μ S)
        (ProbabilityTheory.gaussianReal (μ.ofLp i) (S i i).toNNReal)
-- Mathlib.Topology.PartitionOfUnity
PartitionOfUnity.exists_finset_nhds_support_subset : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} {f : PartitionOfUnity ι X s} {U : ι → Set X},
  f.IsSubordinate U →
    (∀ (i : ι), IsOpen (U i)) →
      ∀ (x : X), ∃ is, ∃ n ∈ nhds x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (Function.support fun x => (f x) z) ⊆ ↑is
-- Lean.Meta.Match.Basic
Lean.Meta.Match.MatcherResult.mk : Lean.Expr → Array Lean.Meta.Match.CounterExample → List ℕ → Lean.MetaM Unit → Lean.Meta.Match.MatcherResult
-- Mathlib.MeasureTheory.Group.LIntegral
/-- Translating a function by right-addition does not change its Lebesgue integral with
respect to a right-invariant measure.  -/
MeasureTheory.lintegral_add_right_eq_self : ∀ {G : Type u_1} [inst : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_1 : AddGroup G] [MeasurableAdd G]
  [μ.IsAddRightInvariant] (f : G → ENNReal) (g : G), ∫⁻ (x : G), f (x + g) ∂μ = ∫⁻ (x : G), f x ∂μ
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_top : ∀ {a : ENNReal}, a / ⊤ = 0
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.growsPolynomially_log : AkraBazziRecurrence.GrowsPolynomially Real.log
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Pretrivialization.linear : ∀ (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] (e : Bundle.Pretrivialization F Bundle.TotalSpace.proj) [inst_3 : AddCommMonoid F]
  [inst_4 : Module R F] [inst_5 : (x : B) → AddCommMonoid (E x)] [inst_6 : (x : B) → Module R (E x)]
  [Bundle.Pretrivialization.IsLinear R e] {b : B}, b ∈ e.baseSet → IsLinearMap R fun x => (↑e ⟨b, x⟩).2
-- Lean.Elab.Deriving.Basic
Lean.Elab.DerivingClassView : Type
-- Mathlib.Algebra.Free
FreeSemigroup.mk.injEq : ∀ {α : Type u} (head : α) (tail : List α) (head_1 : α) (tail_1 : List α),
  ({ head := head, tail := tail } = { head := head_1, tail := tail_1 }) = (head = head_1 ∧ tail = tail_1)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_inter_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₂.isEmpty = true → (t₁ ∩ t₂).isEmpty = true
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
SimpleGraph.EdgeDisjointTriangles.map : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} (f : α ↪ β),
  G.EdgeDisjointTriangles → (SimpleGraph.map (⇑f) G).EdgeDisjointTriangles
-- Mathlib.Algebra.Notation.Prod
Prod.swap_sub : ∀ {G : Type u_8} {H : Type u_9} [inst : Sub G] [inst_1 : Sub H] (a b : G × H), (a - b).swap = a.swap - b.swap
-- Mathlib.Data.Fintype.Pi
Fintype.piFinset_image : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {γ : α → Type u_3} {δ : α → Type u_4}
  [inst_2 : (a : α) → DecidableEq (δ a)] (f : (a : α) → γ a → δ a) (s : (a : α) → Finset (γ a)),
  (Fintype.piFinset fun a => Finset.image (f a) (s a)) = Finset.image (fun b a => f a (b a)) (Fintype.piFinset s)
-- Mathlib.CategoryTheory.GradedObject.Associator
CategoryTheory.GradedObject.ι_mapBifunctorAssociator_inv_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Category.{v_6, u_4} C₂₃]
  {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)}
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)}
  {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)}
  (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G ≅ CategoryTheory.bifunctorComp₂₃ F G₂₃) {I₁ : Type u_7}
  {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J}
  (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r)
  (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁)
  (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃)
  [inst_6 : (((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
  [inst_7 :
    (((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
              (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
          X₃).HasMap
      ρ₁₂.q]
  [inst_8 : (((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
  [inst_9 :
    (((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
          (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap
      ρ₂₃.q]
  [H₁₂ : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
  [H₂₃ : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J)
  (h : r (i₁, i₂, i₃) = j) {Z : C₄}
  (h_1 :
    CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q
        (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.GradedObject.mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).inv j) h_1) =
    CategoryTheory.CategoryStruct.comp (((associator.inv.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) h_1)
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.mem_sup : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x : M}
  {p p' : Submodule R M}, x ∈ p ⊔ p' ↔ ∃ y ∈ p, ∃ z ∈ p', y + z = x
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.map_sub_eq_zero_iff : ∀ {R : Type u_5} {S : Type u_6} [inst : Ring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  (abv : AbsoluteValue R S) (a b : R), abv (a - b) = 0 ↔ a = b
-- Mathlib.Analysis.Real.OfDigits
/-- Converts a real number `x` from the interval `[0, 1)` into sequence of
its digits in base `b`.  -/
Real.digits : ℝ → (b : ℕ) → [NeZero b] → ℕ → Fin b
-- Lean.Declaration
Lean.AxiomVal.toConstantVal : Lean.AxiomVal → Lean.ConstantVal
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDeriv_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : ℕ} {x : 𝕜} {𝔸 : Type u_5} [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {f g : 𝕜 → 𝔸},
  ContDiffAt 𝕜 (↑n) f x →
    ContDiffAt 𝕜 (↑n) g x →
      iteratedDeriv n (f * g) x =
        ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * iteratedDeriv i f x * iteratedDeriv (n - i) g x
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.invFun_eq_symm : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] (e : A ≃ₗc[R] B), e.invFun = ⇑e.symm
-- Lean.Data.Lsp.Internal
/-- Parent declaration of the reference. Empty string if the reference is itself a declaration.
We do not use `Option` for memory consumption reasons.
 -/
Lean.Lsp.RefInfo.Location.parentDecl : Lean.Lsp.RefInfo.Location → String
-- Mathlib.Data.Multiset.Bind
Multiset.product_cons : ∀ {α : Type u_1} {β : Type v} (b : β) (s : Multiset α) (t : Multiset β),
  s ×ˢ (b ::ₘ t) = Multiset.map (fun a => (a, b)) s + s ×ˢ t
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normalClosure_mono : ∀ {G : Type u_1} [inst : Group G] {s t : Set G}, s ⊆ t → Subgroup.normalClosure s ≤ Subgroup.normalClosure t
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.zero_notMem_sub_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddGroup α] {s t : Finset α}, 0 ∉ s - t ↔ Disjoint s t
-- Mathlib.RingTheory.PrincipalIdealDomain
span_singleton_inf_span_singleton : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : GCDMonoid R] (n m : R),
  Ideal.span {n} ⊓ Ideal.span {m} = Ideal.span {lcm n m}
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
DerivedCategory.Plus.instIsLocalizationPlusQhTrWSubcategoryAcyclic : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C],
  DerivedCategory.Plus.Qh.IsLocalization (HomotopyCategory.Plus.subcategoryAcyclic C).trW
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.coe_mk : ∀ {X : Type u_1} {R : Type u_3} [inst : Zero X] [inst_1 : Zero R] [inst_2 : TopologicalSpace X]
  [inst_3 : TopologicalSpace R] {f : C(X, R)} {h0 : f 0 = 0}, ⇑{ toContinuousMap := f, map_zero' := h0 } = ⇑f
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.isCentralScalar : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] [inst_2 : SMul αᵐᵒᵖ β] [IsCentralScalar α β],
  IsCentralScalar α (Finset β)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.forget_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  (R : CategoryTheory.Sheaf J RingCat) {X Y : SheafOfModules R} (φ : X ⟶ Y), (SheafOfModules.forget R).map φ = φ.val
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree
SheafOfModules.pullbackObjFreeIso.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
  [inst_3 : (SheafOfModules.pushforward φ).IsRightAdjoint] [inst_4 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_5 : CategoryTheory.HasWeakSheafify K AddCommGrpCat] [inst_6 : J.WEqualsLocallyBijective AddCommGrpCat]
  [inst_7 : K.WEqualsLocallyBijective AddCommGrpCat] [inst_8 : F.Final] (I : Type u),
  SheafOfModules.pullbackObjFreeIso φ I = SheafOfModules.pullbackObjFreeIso φ I