mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
SSet.S.cast_dim : ∀ {X : SSet} (s : X.S) {d : ℕ} (hd : s.dim = d), (s.cast hd).dim = d
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
CurveIntegrable.trans : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b c : E} {ω : E → E →L[𝕜] F}
  {γab : Path a b} {γbc : Path b c}, CurveIntegrable ω γab → CurveIntegrable ω γbc → CurveIntegrable ω (γab.trans γbc)
-- Mathlib.CategoryTheory.Sites.Adjunction
/-- **Alias** of `CategoryTheory.Sheaf.adjunction_counit_app_hom`. -/
CategoryTheory.Sheaf.adjunction_counit_app_val : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E]
  {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} [inst_3 : CategoryTheory.HasWeakSheafify J D]
  [inst_4 : J.HasSheafCompose F] (adj : G ⊣ F) (Y : CategoryTheory.Sheaf J D),
  ((CategoryTheory.Sheaf.adjunction J adj).counit.app Y).hom =
    CategoryTheory.sheafifyLift J ((CategoryTheory.Adjunction.whiskerRight Cᵒᵖ adj).counit.app Y.obj) ⋯
-- Mathlib.Data.Finset.Prod
Finset.diag_inter : ∀ {α : Type u_1} (s t : Finset α) [inst : DecidableEq α], (s ∩ t).diag = s.diag ∩ t.diag
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
CategoryTheory.Functor.leftDerived_fac : ∀ {C : Type u_3} {D : Type u_1} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_1} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  (LF : CategoryTheory.Functor D H) {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α : L.comp LF ⟶ F) (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : LF.IsLeftDerivedFunctor α W] (G : CategoryTheory.Functor D H) (β : L.comp G ⟶ F),
  CategoryTheory.CategoryStruct.comp (L.whiskerLeft (LF.leftDerivedLift α W G β)) α = β
-- Mathlib.CategoryTheory.Groupoid
CategoryTheory.isGroupoid_iff_isomorphisms_eq_top : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C],
  CategoryTheory.IsGroupoid C ↔ CategoryTheory.MorphismProperty.isomorphisms C = ⊤
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get_alter_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : Option β → Option β} {hc : k ∈ Std.ExtDTreeMap.Const.alter t k f},
  Std.ExtDTreeMap.Const.get (Std.ExtDTreeMap.Const.alter t k f) k hc = (f (Std.ExtDTreeMap.Const.get? t k)).get ⋯
-- Mathlib.Algebra.Order.Floor.Extended
/-- **Alias** of the reverse direction of `ENat.ceil_pos`. -/
Mathlib.Meta.Positivity.natCeil_pos : ∀ {r : ENNReal}, 0 < r → 0 < ⌈r⌉ₑ
-- Mathlib.CategoryTheory.Localization.Bifunctor
CategoryTheory.Localization.Lifting₂.mk : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D₁ : Type u_3} →
      {D₂ : Type u_4} →
        {E : Type u_5} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} E] →
                    {L₁ : CategoryTheory.Functor C₁ D₁} →
                      {L₂ : CategoryTheory.Functor C₂ D₂} →
                        {W₁ : CategoryTheory.MorphismProperty C₁} →
                          {W₂ : CategoryTheory.MorphismProperty C₂} →
                            {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E)} →
                              {F' : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)} →
                                ((((CategoryTheory.Functor.whiskeringLeft₂ E).obj L₁).obj L₂).obj F' ≅ F) →
                                  CategoryTheory.Localization.Lifting₂ L₁ L₂ W₁ W₂ F F'
-- Init.Data.Array.Erase
Array.erase_of_not_mem : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {xs : Array α}, a ∉ xs → xs.erase a = xs
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs_by_cases : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] {a : α} (P : α → Prop), P a → P (-a) → P |a|
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extend_op_d_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') (i' j' : ι')
  {Z : Cᵒᵖ} (h : (K.op.extend e.op).X j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((K.op.extend e.op).d i' j') h =
    CategoryTheory.CategoryStruct.comp ((K.extendOpIso e).hom.f i')
      (CategoryTheory.CategoryStruct.comp ((K.extend e).d j' i').op
        (CategoryTheory.CategoryStruct.comp ((K.extendOpIso e).inv.f j') h))
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.op : Cᵒᵖ ⥤ Dᵒᵖ` preserves finite limits, then `F : C ⥤ D` preserves finite colimits.  -/
CategoryTheory.Limits.preservesFiniteColimits_of_op : ∀ {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.Limits.PreservesFiniteLimits F.op],
  CategoryTheory.Limits.PreservesFiniteColimits F
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.inv_mem_iff : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) {c d : C} (f : c ⟶ d),
  CategoryTheory.Groupoid.inv f ∈ S.arrows d c ↔ f ∈ S.arrows c d
-- Mathlib.Algebra.Order.Floor.Semifield
Mathlib.Meta.NormNum.IsRat.natFloor : ∀ {R : Type u_3} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R] (r : R)
  (n d : ℕ), Mathlib.Meta.NormNum.IsRat r (Int.negOfNat n) d → Mathlib.Meta.NormNum.IsNat ⌊r⌋₊ 0
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {X₁ X₂ : HomotopicalAlgebra.CofibrantObject C} (f : X₁ ⟶ X₂),
  CategoryTheory.CategoryStruct.comp X₁.iBifibrantResolutionObj
      (HomotopicalAlgebra.CofibrantObject.homMk (HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap f).hom) =
    CategoryTheory.CategoryStruct.comp f X₂.iBifibrantResolutionObj
-- ProofWidgets.Util
instToJsonUnit_proofWidgets : Lean.ToJson Unit
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_eq_none_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {a : α}, m.contains a = false → m.getKey? a = none
-- Mathlib.Algebra.Group.Ideal
/-- The semigroup ideal generated by `s` is `s ∪ Set.univ * s`.  -/
SemigroupIdeal.coe_closure : ∀ {M : Type u_1} [inst : Semigroup M] {s : Set M}, ↑(SemigroupIdeal.closure s) = s ∪ Set.univ * s
-- Mathlib.Algebra.Azumaya.Defs
/-- The canonical map from `A ⊗[R] Aᵐᵒᵖ` to `Module.End R A` where
`a ⊗ b` maps to `f : x ↦ a * x * b`.  -/
AlgHom.mulLeftRight : (R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] → [inst_2 : Algebra R A] → TensorProduct R A Aᵐᵒᵖ →ₐ[R] Module.End R A
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformFun.instCompleteSpace : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] [CompleteSpace β], CompleteSpace (UniformFun α β)
-- Mathlib.MeasureTheory.Measure.Count
MeasureTheory.Measure.le_count_apply : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α}, ∑' (x : ↑s), 1 ≤ MeasureTheory.Measure.count s
-- Init.Data.Ord.Basic
Ordering.isLE_then_iff_and : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isLE = true ↔ o₁.isLE = true ∧ (o₁ = Ordering.lt ∨ o₂.isLE = true)
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.State.mk.inj : ∀ {stxTrav : Lean.Syntax.Traverser} {leadWord : String} {leadWordIdent isUngrouped mustBeGrouped : Bool}
  {stack : Array Std.Format} {stxTrav_1 : Lean.Syntax.Traverser} {leadWord_1 : String}
  {leadWordIdent_1 isUngrouped_1 mustBeGrouped_1 : Bool} {stack_1 : Array Std.Format},
  { stxTrav := stxTrav, leadWord := leadWord, leadWordIdent := leadWordIdent, isUngrouped := isUngrouped,
        mustBeGrouped := mustBeGrouped, stack := stack } =
      { stxTrav := stxTrav_1, leadWord := leadWord_1, leadWordIdent := leadWordIdent_1, isUngrouped := isUngrouped_1,
        mustBeGrouped := mustBeGrouped_1, stack := stack_1 } →
    stxTrav = stxTrav_1 ∧
      leadWord = leadWord_1 ∧
        leadWordIdent = leadWordIdent_1 ∧
          isUngrouped = isUngrouped_1 ∧ mustBeGrouped = mustBeGrouped_1 ∧ stack = stack_1
-- Init.Prelude
/-- `And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`. -/
And : Prop → Prop → Prop
-- Mathlib.Data.Finset.SDiff
Finset.sdiff_nonempty : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, (s \ t).Nonempty ↔ ¬s ⊆ t
-- Mathlib.CategoryTheory.Action.Limits
Action.res_linear : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.Preadditive V] {R : Type u_3} [inst_3 : Semiring R] [inst_4 : CategoryTheory.Linear R V]
  {H : Type u_4} [inst_5 : Monoid H] (f : G →* H), CategoryTheory.Functor.Linear R (Action.res V f)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
le_mul_inv_iff_mul_le : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulRightMono α] {a b c : α}, c ≤ a * b⁻¹ ↔ c * b ≤ a
-- Mathlib.CategoryTheory.Quotient
/-- An equivalence between the type synonym for a quotient category and the type alias
for the original category.  -/
CategoryTheory.Quotient.equiv : {C : Type u_2} → [inst : CategoryTheory.Category.{v_2, u_2} C] → (r : HomRel C) → CategoryTheory.Quotient r ≃ C
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_intCast : ∀ {K : Type u_1} [inst : RCLike K] (n : ℤ), ↑↑n = ↑n
-- Mathlib.Topology.EMetricSpace.Basic
/-- A very useful criterion to show that a space is complete is to show that all sequences
which satisfy a bound of the form `edist (u n) (u m) < B N` for all `n m ≥ N` are
converging. This is often applied for `B N = 2^{-N}`, i.e., with a very fast convergence to
`0`, which makes it possible to use arguments of converging series, while this is impossible
to do in general for arbitrary Cauchy sequences.  -/
EMetric.complete_of_convergent_controlled_sequences : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (B : ℕ → ENNReal),
  (∀ (n : ℕ), 0 < B n) →
    (∀ (u : ℕ → α),
        (∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (u n) (u m) < B N) → ∃ x, Filter.Tendsto u Filter.atTop (nhds x)) →
      CompleteSpace α
-- Lean.Elab.InfoTree.Types
Lean.Elab.InfoState.mk : Bool →
  Lean.PersistentHashMap Lean.MVarId Lean.Elab.InfoTree →
    Lean.PersistentHashMap Lean.MVarId (Task Lean.Elab.InfoTree) →
      Lean.PersistentArray Lean.Elab.InfoTree → Lean.Elab.InfoState
-- Mathlib.Algebra.Group.Equiv.TypeTags
monoidEndToAdditive_symm_apply_apply : ∀ (M : Type u_4) [inst : MulOneClass M] (f : Additive M →+ Additive M) (a : M),
  ((monoidEndToAdditive M).symm f) a = Additive.toMul (f (Additive.ofMul a))
-- Mathlib.Order.PiLex
/-- If we swap two strictly decreasing values in a function, then the result is lexicographically
smaller than the original function.  -/
Pi.lex_desc : ∀ {ι : Type u_1} {α : Type u_3} [inst : Preorder ι] [inst_1 : DecidableEq ι] [inst_2 : LT α] {f : ι → α} {i j : ι},
  i ≤ j → f j < f i → toLex (f ∘ ⇑(Equiv.swap i j)) < toLex f
-- Mathlib.Analysis.Convex.EGauge
/-- If `c • x ∈ s`, then `egauge 𝕜 s x` is at most `‖c‖ₑ⁻¹`.

See also `egauge_le_of_smul_mem_of_ne`.  -/
egauge_le_of_smul_mem : ∀ {𝕜 : Type u_1} [inst : NormedDivisionRing 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {c : 𝕜}
  {s : Set E} {x : E}, c • x ∈ s → egauge 𝕜 s x ≤ ‖c‖ₑ⁻¹
-- Mathlib.Data.Real.Basic
Real.instZeroLEOneClass : ZeroLEOneClass ℝ
-- Mathlib.Algebra.Algebra.Pi
/-- **Alias** of `AlgHom.pi_evalAlgHom`. -/
Pi.algHom_evalAlgHom : ∀ {ι : Type u_1} (R : Type u_2) (A : ι → Type u_3) [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (A i)]
  [inst_2 : (i : ι) → Algebra R (A i)], AlgHom.pi (Pi.evalAlgHom R A) = AlgHom.id R ((i : ι) → A i)
-- Mathlib.Tactic.CongrExclamation
/-- According to the configuration, how many of the arguments in `numArgs` should be considered.  -/
Congr!.Config.maxArgsFor : Congr!.Config → ℕ → ℕ
-- Init.Data.Rat.Lemmas
Rat.inv_def : ∀ (a : ℚ), a⁻¹ = Rat.divInt (↑a.den) a.num
-- Aesop.Forward.State
/-- The substitution that results from matching the hypothesis against a
premise or that was derived from the pattern.  -/
Aesop.Hyp.subst : Aesop.Hyp → Aesop.Substitution
-- Mathlib.Data.NNReal.Defs
Real.le_toNNReal_iff_coe_le' : ∀ {r : NNReal} {p : ℝ}, 0 < r → (r ≤ p.toNNReal ↔ ↑r ≤ p)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_eq_some_getD : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} {fallback : β}, a ∈ m → m[a]? = some (m.getD a fallback)
-- Mathlib.NumberTheory.JacobiSum.Basic
/-- The Jacobi sum is compatible with ring homomorphisms.  -/
jacobiSum_ringHomComp : ∀ {R : Type u_1} {R' : Type u_2} [inst : CommRing R] [inst_1 : Fintype R] [inst_2 : CommRing R'] {R'' : Type u_3}
  [inst_3 : CommRing R''] (χ ψ : MulChar R R') (f : R' →+* R''),
  jacobiSum (χ.ringHomComp f) (ψ.ringHomComp f) = f (jacobiSum χ ψ)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCircuit.of_map : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u : V} {p : G.Walk u u},
  (SimpleGraph.Walk.map f p).IsCircuit → p.IsCircuit
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.algEquivCMulXAddC_apply : ∀ {R : Type u_3} [inst : CommRing R] (a b : R) [inst_1 : Invertible a] (a_1 : Polynomial R),
  (Polynomial.algEquivCMulXAddC a b) a_1 = (Polynomial.aeval (Polynomial.C a * Polynomial.X + Polynomial.C b)) a_1
-- Mathlib.GroupTheory.QuotientGroup.Basic
Subgroup.Characteristic.comap_quotient_mk : ∀ {G : Type u} [inst : Group G] {H : Subgroup G} [hH : H.Characteristic] {K : Subgroup (G ⧸ H)},
  K.Characteristic → (Subgroup.comap (QuotientGroup.mk' H) K).Characteristic
-- Mathlib.Analysis.Calculus.Deriv.Mul
ContinuousLinearMap.hasDerivAt_of_bilinear : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type w} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {G : Type u_1}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : 𝕜} {B : E →L[𝕜] F →L[𝕜] G} {u : 𝕜 → E} {v : 𝕜 → F}
  {u' : E} {v' : F},
  (x ∈ tsupport v → HasDerivAt u u' x) →
    (x ∈ tsupport u → HasDerivAt v v' x) → HasDerivAt (fun x => (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) x
-- Init.Control.Option
/-- Sequences two potentially-failing actions. The second action is run only if the first succeeds.
 -/
OptionT.bind : {m : Type u → Type v} → [Monad m] → {α β : Type u} → OptionT m α → (α → OptionT m β) → OptionT m β
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.append_concat : ∀ {V : Type u} {G : SimpleGraph V} {u v w x : V} (p : G.Walk u v) (q : G.Walk v w) (h : G.Adj w x),
  p.append (q.concat h) = (p.append q).concat h
-- Mathlib.RepresentationTheory.Rep.Basic
/-- Given a `G`-action on `H`, this is `k[H]` bundled with the natural representation
`G →* End(k[H])` as a term of type `Rep k G`.  -/
Rep.ofMulAction : (k : Type u) →
  (G : Type v) → [inst : Ring k] → [inst_1 : Monoid G] → (H : Type w') → [MulAction G H] → Rep.{max u w', u, v} k G
-- Mathlib.LinearAlgebra.TensorAlgebra.Basis
/-- A basis on `M` can be lifted to a basis on `TensorAlgebra R M`  -/
Module.Basis.tensorAlgebra : {κ : Type uκ} →
  {R : Type uR} →
    {M : Type uM} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] → Module.Basis κ R M → Module.Basis (FreeMonoid κ) R (TensorAlgebra R M)
-- Mathlib.Computability.Ackermann
ack_succ_succ : ∀ (m n : ℕ), ack (m + 1) (n + 1) = ack m (ack (m + 1) n)
-- Std.Http.Internal.Char
/-- Checks if a byte is a valid character in a URI query component according to RFC 3986.
`query = *( pchar / "/" / "?" )`
 -/
Std.Http.Internal.Char.isQueryChar : UInt8 → Bool
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
/-- The maps `mapTrifunctorMapObj F p X₁ X₂ X₃ ⟶ mapTrifunctorMapObj F p Y₁ Y₂ Y₃` which
express the functoriality of `mapTrifunctorMapObj`, see `mapTrifunctorMap`  -/
CategoryTheory.GradedObject.mapTrifunctorMapMap : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) →
                  {I₁ : Type u_7} →
                    {I₂ : Type u_8} →
                      {I₃ : Type u_9} →
                        {J : Type u_10} →
                          (p : I₁ × I₂ × I₃ → J) →
                            {X₁ Y₁ : CategoryTheory.GradedObject I₁ C₁} →
                              (X₁ ⟶ Y₁) →
                                {X₂ Y₂ : CategoryTheory.GradedObject I₂ C₂} →
                                  (X₂ ⟶ Y₂) →
                                    {X₃ Y₃ : CategoryTheory.GradedObject I₃ C₃} →
                                      (X₃ ⟶ Y₃) →
                                        [inst_4 :
                                            ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj
                                                      X₂).obj
                                                  X₃).HasMap
                                              p] →
                                          [inst_5 :
                                              ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj
                                                        Y₂).obj
                                                    Y₃).HasMap
                                                p] →
                                            CategoryTheory.GradedObject.mapTrifunctorMapObj F p X₁ X₂ X₃ ⟶
                                              CategoryTheory.GradedObject.mapTrifunctorMapObj F p Y₁ Y₂ Y₃
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- **Sequential characterization of lower hemicontinuity**:
A set-valued function `f : α → Set β` is lower hemicontinuous at `x₀ : α` if for every sequence
`x : ℕ → α` tending to `x₀` and every `y₀ ∈ f x₀`, there exists a sequence `y : ℕ → β` with
`y n ∈ f (x n)` for all `n` that tends to `y₀`.  -/
LowerHemicontinuousAt.of_sequences : ∀ {α : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {x₀ : α}
  [(nhds x₀).IsCountablyGenerated],
  (∀ (x : ℕ → α),
      Filter.Tendsto x Filter.atTop (nhds x₀) →
        ∀ y₀ ∈ f x₀, ∃ y, (∀ (n : ℕ), y n ∈ f (x n)) ∧ Filter.Tendsto y Filter.atTop (nhds y₀)) →
    LowerHemicontinuousAt f x₀
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h : m.WF) {l : List (α × β)} {k : α}
  (contains_eq_false : (List.map Prod.fst l).contains k = false) {h' : k ∈ m.insertMany l},
  (m.insertMany l).getKey k h' = m.getKey k ⋯
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.mem_toList : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α],
  m.WF → ∀ {k : α}, k ∈ m.toList ↔ k ∈ m
-- Init.Grind.Lemmas
Lean.Grind.Semiring.zero_mul_congr : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] {a b : α}, a = 0 → a * b = 0
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.homMk_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : CategoryTheory.Grp C} (f : A.X ⟶ B.X) [inst_2 : CategoryTheory.IsMonHom f],
  (CategoryTheory.Grp.homMk f).hom.hom = f
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.Functor.IsAccessible.exists_cardinal : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} [self : CategoryTheory.Functor.IsAccessible.{w, v₁, v₂, u₁, u₂} F],
  ∃ κ, ∃ (x : Fact κ.IsRegular), F.IsCardinalAccessible κ
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
_private.Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer.0.CategoryTheory.Limits.MultispanIndex.multispan.match_1.splitter : {J : CategoryTheory.Limits.MultispanShape} →
  (motive : (x y : CategoryTheory.Limits.WalkingMultispan J) → (x ⟶ y) → Sort u_3) →
    (x y : CategoryTheory.Limits.WalkingMultispan J) →
      (f : x ⟶ y) →
        ((x : CategoryTheory.Limits.WalkingMultispan J) →
            motive x x (CategoryTheory.Limits.WalkingMultispan.Hom.id x)) →
          ((b : J.L) →
              motive (CategoryTheory.Limits.WalkingMultispan.left b)
                (CategoryTheory.Limits.WalkingMultispan.right (J.fst b))
                (CategoryTheory.Limits.WalkingMultispan.Hom.fst b)) →
            ((b : J.L) →
                motive (CategoryTheory.Limits.WalkingMultispan.left b)
                  (CategoryTheory.Limits.WalkingMultispan.right (J.snd b))
                  (CategoryTheory.Limits.WalkingMultispan.Hom.snd b)) →
              motive x y f
-- Lean.Elab.Command
Lean.Elab.Command.Linter.run : Lean.Linter → Lean.Syntax → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_monomial_mul : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (m n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (a : R),
  (MvPowerSeries.coeff m) ((MvPowerSeries.monomial n) a * φ) = if n ≤ m then a * (MvPowerSeries.coeff (m - n)) φ else 0
-- Std.Sync.Channel
/-- Consumers that are blocked on a producer providing them a value, as there was no value
enqueued when they tried to dequeue. They will be resolved to `false` if the channel closes.
 -/
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.State.consumers : {α : Type} → Std.CloseableChannel.Bounded.State✝ α → Std.Queue (Std.CloseableChannel.Bounded.Consumer✝ α)
-- Init.Grind.Config
Lean.Grind.NoopConfig.mk.injEq : ∀ (toConfig toConfig_1 : Lean.Grind.Config),
  ({ toConfig := toConfig } = { toConfig := toConfig_1 }) = (toConfig = toConfig_1)
-- Aesop.Util.Unfold
Aesop.unfoldManyCore : Lean.Meta.Simp.Context →
  (Lean.Name → Option (Option Lean.Name)) →
    Lean.Expr → StateRefT' IO.RealWorld (Array Lean.Name) Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.Order.Lattice
SemilatticeInf.toMin.eq_1 : ∀ {α : Type u} [inst : SemilatticeInf α], SemilatticeInf.toMin = { min := fun a b => SemilatticeInf.inf a b }
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.inv_indexEquiv : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι₂ : Type u_8} {M₂ : Type u_9} {N₂ : Type u_10}
  [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂] [inst_7 : AddCommGroup N₂] [inst_8 : Module R N₂]
  (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (f : P.Equiv Q),
  (↑(RootPairing.Equiv.symm P Q f)).indexEquiv = (↑f).indexEquiv.symm
-- Init.Grind.Config
/-- When `true` (default: `true`), enables the procedure for handling orders that implement
at least `Std.IsPreorder`
 -/
Lean.Grind.Config.order : Lean.Grind.Config → Bool