mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Recycling.RBTree.Basic
/-- Fills the `Path` with a subtree.  -/
RBTree.RBNode.Path.fill : {α : Type u_1} → RBTree.RBNode.Path α → RBTree.RBNode α → RBTree.RBNode α
-- Mathlib.Tactic.Algebraize
/-- Tactic that, given `RingHom`s, adds the corresponding `Algebra` and (if possible)
`IsScalarTower` instances, as well as `Algebra` corresponding to `RingHom` properties available
as hypotheses.

Example: given `f : A →+* B` and `g : B →+* C`, and `hf : f.FiniteType`, `algebraize [f, g]` will
add the instances `Algebra A B`, `Algebra B C`, and `Algebra.FiniteType A B`.

See the `algebraize` tag for instructions on what properties can be added.

The tactic also comes with a configuration option `properties`. If set to `true` (default), the
tactic searches through the local context for `RingHom` properties that can be converted to
`Algebra` properties. The macro `algebraize_only` calls
`algebraize -properties`,
so in other words it only adds `Algebra` and `IsScalarTower` instances.  -/
Mathlib.Tactic.tacticAlgebraize__ : Lean.ParserDescr
-- Batteries.Data.Fin.Lemmas
Fin.isSome_findRev?_of_eq_true : ∀ {n : ℕ} {i : Fin n} {p : Fin n → Bool}, p i = true → (Fin.findRev? p).isSome = true
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
/-- Construct the smallest measure space containing a collection of basic sets  -/
MeasurableSpace.generateFrom : {α : Type u_1} → Set (Set α) → MeasurableSpace α
-- Mathlib.Algebra.DirectSum.Module
/-- Scalar multiplication commutes with direct sums.  -/
DirectSum.mk_smul : ∀ (R : Type u) [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] (s : Finset ι) (c : R) (x : (i : ↑↑s) → M ↑i),
  (DirectSum.mk M s) (c • x) = c • (DirectSum.mk M s) x
-- Lean.Elab.MatchAltView
Lean.Elab.Term.MatchAltView : Lean.SyntaxNodeKinds → Type
-- Lean.Parser.Extension
/-- The parsing tables for builtin parsers are "stored" in the extracted source code.
 -/
Lean.Parser.registerBuiltinParserAttribute : Lean.Name →
  Lean.Name →
    optParam Lean.Parser.LeadingIdentBehavior Lean.Parser.LeadingIdentBehavior.default →
      autoParam Lean.Name Lean.Parser.registerBuiltinParserAttribute._auto_1 → IO Unit
-- Mathlib.Order.Hom.Lex
OrderIso.sumLexIioIci_symm_apply_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] {x : α} (a : ↑(Set.Ici x)),
  (OrderIso.sumLexIioIci x).symm ↑a = toLex (Sum.inr a)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.contains_eq_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [PartialEquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α}, m.contains a = Std.Internal.List.containsKey a (Std.DHashMap.Internal.toListModel (↑m).buckets)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_eq_some_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α}, t.contains k = true → t.getKey? k = some k
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- For any model with corners, the model space is a `C^n` manifold  -/
instIsManifoldModelSpace : ∀ {𝕜 : 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} {n : WithTop ℕ∞},
  IsManifold I n H
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.lift_π_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {β : Type w} {f : β → C}
  [inst_1 : CategoryTheory.Limits.HasProduct f] {P : C} (p : (b : β) → P ⟶ f b) (b : β) {F : C → C → Type uF}
  {carrier : C → Type w_1} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)}
  [inst_2 : CategoryTheory.ConcreteCategory C F] (x : carrier P),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π f b))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.lift p)) x) =
    (CategoryTheory.ConcreteCategory.hom (p b)) x
-- Init.Data.Array.Basic
Array.anyM.loop.eq_def : ∀ {α : Type u} {m : Type → Type w} [inst : Monad m] (p : α → m Bool) (as : Array α) (stop : ℕ) (h : stop ≤ as.size)
  (j : ℕ),
  Array.anyM.loop p as stop h j =
    if hlt : j < stop then
      have this := ⋯;
      do
      let __do_lift ← p as[j]
      if __do_lift = true then pure true else Array.anyM.loop p as stop h (j + 1)
    else pure false
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.verify₄.eq_1 : ∀ (w x y z : UInt8),
  ByteArray.utf8DecodeChar?.verify₄ w x y z =
    if
        (ByteArray.utf8DecodeChar?.isInvalidContinuationByte x ||
              ByteArray.utf8DecodeChar?.isInvalidContinuationByte y ||
            ByteArray.utf8DecodeChar?.isInvalidContinuationByte z) =
          true then
      false
    else
      have r := ByteArray.utf8DecodeChar?.assemble₄Unchecked w x y z;
      decide (65536 ≤ r ∧ r ≤ 1114111)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
/-- If `K / E / F` is a field extension tower, `L` is an intermediate field of `K / F`, such that
either `E / F` or `L / F` is algebraic, then `[E(L) : E] ≤ [L : F]`. A corollary of
`Subalgebra.adjoin_rank_le` since in this case `E(L) = E[L]`.  -/
IntermediateField.adjoin_rank_le_of_isAlgebraic : ∀ {F : Type u_1} [inst : Field F] (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u_3}
  [inst_3 : Field K] [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] (L : IntermediateField F K),
  Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L → Module.rank E ↥(IntermediateField.adjoin E ↑L) ≤ Module.rank F ↥L
-- Mathlib.Analysis.InnerProductSpace.Affine
inner_vsub_vsub_left_eq_dist_sq_right_iff : ∀ {V : Type u_2} {P : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {a b c : P}, inner ℝ (a -ᵥ b) (a -ᵥ c) = dist a c ^ 2 ↔ inner ℝ (c -ᵥ b) (a -ᵥ c) = 0
-- Mathlib.Data.Rel
SetRel.cod_mono : ∀ {α : Type u_1} {β : Type u_2} {R₁ R₂ : SetRel α β}, R₁ ⊆ R₂ → R₁.cod ⊆ R₂.cod
-- Mathlib.Algebra.Algebra.Hom
AlgHomClass.toLinearMap_toAlgHom : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {F : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : FunLike F A B]
  [inst_6 : AlgHomClass F R A B] (f : F), ↑↑f = ↑f
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.ofBddAugment.eq_1 : ∀ {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅)
  (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I)
  (indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I))
  (indep_bdd : ∃ n, ∀ (I : Set α), Indep I → I.encard ≤ ↑n) (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E),
  IndepMatroid.ofBddAugment E Indep indep_empty indep_subset indep_aug indep_bdd subset_ground =
    IndepMatroid.ofBdd E Indep indep_empty indep_subset ⋯ subset_ground indep_bdd
-- Mathlib.Topology.Order.Monotone
/-- An antitone function `f` sending `bot` to `top` and continuous at the supremum of a set sends
this supremum to the infimum of the image of this set.  -/
Antitone.map_sSup_of_continuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : CompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α},
  ContinuousAt f (sSup s) → Antitone f → f ⊥ = ⊤ → f (sSup s) = sInf (f '' s)
-- Mathlib.Probability.Independence.Process.Basic
/-- Stochastic processes $((X^s_t)_{t \in T_s})_{s \in S}$ are mutually independent if
for all $s_1, ..., s_n$ and all $t^{s_i}_1, ..., t^{s_i}_{p_i}$ the families
$(X^{s_1}_{t^{s_1}_1}, ..., X^{s_1}_{t^{s_1}_{p_1}}), ...,
(X^{s_n}_{t^{s_n}_1}, ..., X^{s_n}_{t^{s_n}_{p_n}})$ are mutually independent.  -/
ProbabilityTheory.iIndepFun.iIndepFun_process : ∀ {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {T : S → Type u_4}
  {𝓧 : (i : S) → T i → Type u_5} [inst : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)]
  {X : (i : S) → (j : T i) → Ω → 𝓧 i j},
  (∀ (i : S) (j : T i), Measurable (X i j)) →
    (∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), ProbabilityTheory.iIndepFun (fun i ω j => X (↑i) (↑j) ω) P) →
      ProbabilityTheory.iIndepFun (fun i ω j => X i j ω) P
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.ofHom_comp : ∀ {X Y Z : Type u} [inst : Group X] [inst_1 : Group Y] [inst_2 : Group Z] (f : X →* Y) (g : Y →* Z),
  GrpCat.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (GrpCat.ofHom f) (GrpCat.ofHom g)
-- Lean.Parser.Basic
Lean.Parser.optionalNoAntiquot : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.LHom.onBoundedFormula.eq_4 : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} (g : L →ᴸ L') (x : ℕ)
  (f₁ f₂ : L.BoundedFormula α x), g.onBoundedFormula (f₁.imp f₂) = (g.onBoundedFormula f₁).imp (g.onBoundedFormula f₂)
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_zero : ∀ {R : Type u} [inst : Semiring R], Polynomial.derivative 0 = 0
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_filter_not_contains_of_contains_eq_false_right : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l₁ : List ((_ : α) × β)} {l₂ : List α} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    l₂.contains k = false →
      Std.Internal.List.getValue? k (List.filter (fun p => !l₂.contains p.fst) l₁) = Std.Internal.List.getValue? k l₁
-- Init.Data.List.Sublist
List.append_subset : ∀ {α : Type u_1} {l₁ l₂ l : List α}, l₁ ++ l₂ ⊆ l ↔ l₁ ⊆ l ∧ l₂ ⊆ l
-- Mathlib.Data.Matrix.Block
Matrix.fromBlocks_submatrix_sum_swap_left : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {p : Type u_5} {α : Type u_12} (A : Matrix n l α)
  (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (f : p → l ⊕ m),
  (Matrix.fromBlocks A B C D).submatrix Sum.swap f = (Matrix.fromBlocks C D A B).submatrix id f
-- Mathlib.Order.Interval.Finset.Basic
Finset.Iic_filter_lt_of_lt_right : ∀ {α : Type u_3} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] {a c : α}
  [inst_2 : DecidablePred fun x => x < c], a < c → {x ∈ Finset.Iic a | x < c} = Finset.Iic a
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
/-- The `essSup` of a function `g` on the additive quotient space `G ⧸ Γ` with respect
to the pushforward of the restriction, `μ_𝓕`, of a right-invariant measure `μ` to a fundamental
domain `𝓕`, is the same as the `essSup` of `g`'s lift to the universal cover `G` with respect
to `μ`.  -/
essSup_comp_quotientAddGroup_mk : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G]
  [IsTopologicalAddGroup G] [BorelSpace G] {μ : MeasureTheory.Measure G} {Γ : AddSubgroup G} {𝓕 : Set G},
  MeasureTheory.IsAddFundamentalDomain (↥Γ.op) 𝓕 μ →
    ∀ [Countable ↥Γ] [inst_6 : MeasurableSpace (G ⧸ Γ)] [BorelSpace (G ⧸ Γ)] [μ.IsAddRightInvariant]
      {g : G ⧸ Γ → ENNReal},
      AEMeasurable g (MeasureTheory.Measure.map QuotientAddGroup.mk (μ.restrict 𝓕)) →
        essSup g (MeasureTheory.Measure.map QuotientAddGroup.mk (μ.restrict 𝓕)) = essSup (fun x => g ↑x) μ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}
  [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α},
  t.WF → (k ∈ Std.DTreeMap.Raw.filterMap f t ↔ ∃ (h : k ∈ t), (f k (t.get k h)).isSome = true)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The affine span of a set is nonempty if and only if that set is.  -/
affineSpan_nonempty : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P}, (↑(affineSpan k s)).Nonempty ↔ s.Nonempty
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.LaxTrans.naturality_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (self : CategoryTheory.Oplax.LaxTrans F G) {a b : B} {f g : a ⟶ b}
  (η : f ⟶ g),
  CategoryTheory.CategoryStruct.comp (self.naturality f)
      (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (self.app b)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.map₂ η))
      (self.naturality g)
-- Mathlib.Control.Bitraversable.Basic
Bitraversable.mk : {t : Type u → Type u → Type u} →
  [toBifunctor : Bifunctor t] →
    ({m : Type u → Type u} → [Applicative m] → {α α' β β' : Type u} → (α → m α') → (β → m β') → t α β → m (t α' β')) →
      Bitraversable t
-- Lean.Meta.Basic
/-- `withDefault x` executes `x` using the default transparency setting.  -/
Lean.Meta.withDefault : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → n α → n α
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.ofCoeff_finsuppSum : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} {ι : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid N]
  (f : ι →₀ N) (g : ι → N → M →₀ R),
  AddMonoidAlgebra.ofCoeff (f.sum g) = f.sum fun i n => AddMonoidAlgebra.ofCoeff (g i n)
-- Init.Data.Option.Lemmas
Option.isNone_min : ∀ {α : Type u_1} [inst : Min α] {o o' : Option α}, (o ⊓ o').isNone = (o.isNone || o'.isNone)
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
CategoryTheory.Functor.weightedLimObjMap_comp_assoc : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  (W : CategoryTheory.Functor J (Type w)) {F₁ F₂ F₃ : CategoryTheory.Functor J C}
  [inst_2 : CategoryTheory.Limits.HasWeightedLimit W F₁] [inst_3 : CategoryTheory.Limits.HasWeightedLimit W F₂]
  [inst_4 : CategoryTheory.Limits.HasWeightedLimit W F₃] (f : F₁ ⟶ F₂) (g : F₂ ⟶ F₃) {Z : C}
  (h : W.weightedLimObjObj F₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (W.weightedLimObjMap (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp (W.weightedLimObjMap f)
      (CategoryTheory.CategoryStruct.comp (W.weightedLimObjMap g) h)
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.BoundedFormula.listEncode.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} (x : ℕ),
  FirstOrder.Language.BoundedFormula.falsum.listEncode = [Sum.inr (Sum.inr (x + 2))]
-- Mathlib.Analysis.VonNeumannAlgebra.Basic
/-- The double commutant (a.k.a. centralizer) of a `VonNeumannAlgebra` is itself.  -/
VonNeumannAlgebra.centralizer_centralizer' : ∀ {H : Type u} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H] [inst_2 : CompleteSpace H]
  (self : VonNeumannAlgebra H), self.carrier.centralizer.centralizer = self.carrier
-- Mathlib.Algebra.Group.Hom.Defs
map_comp_div' : ∀ {ι : Type u_1} {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : DivInvMonoid G]
  [inst_2 : DivInvMonoid H] [MulHomClass F G H] (f : F),
  (∀ (a : G), f a⁻¹ = (f a)⁻¹) → ∀ (g h : ι → G), ⇑f ∘ (g / h) = ⇑f ∘ g / ⇑f ∘ h
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instAddCommMonoid : {α : Type u_1} → [AddCommMonoid α] → AddCommMonoid αᵃᵒᵖ
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.sigmaFinite_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  MeasureTheory.SigmaFinite μ ↔ Nonempty (μ.FiniteSpanningSetsIn Set.univ)
-- Mathlib.Probability.Distributions.Gaussian.Multivariate
ProbabilityTheory.isGaussian_stdGaussian : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [BorelSpace E], ProbabilityTheory.IsGaussian (ProbabilityTheory.stdGaussian E)
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.subsemigroup_eq_subgroup : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M]
  {s : UpperSet (FiniteMulArchimedeanClass M)},
  ↑(MulArchimedeanClass.subsemigroup (FiniteMulArchimedeanClass.toUpperSetMulArchimedeanClass s)) =
    ↑(FiniteMulArchimedeanClass.subgroup s)
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
sq_nonneg : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftMono R] (a : R),
  0 ≤ a ^ 2
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithUpperSet.isUpperSet_toUpperSet_preimage : ∀ {α : Type u_1} [inst : Preorder α] {s : Set (Topology.WithUpperSet α)},
  IsUpperSet (⇑Topology.WithUpperSet.toUpperSet ⁻¹' s) ↔ IsOpen s
-- Mathlib.MeasureTheory.Group.Defs
MeasureTheory.smulInvariantMeasure_iff : ∀ (M : Type u_1) (α : Type u_2) [inst : SMul M α] {x : MeasurableSpace α} (μ : MeasureTheory.Measure α),
  MeasureTheory.SMulInvariantMeasure M α μ ↔ ∀ (c : M) ⦃s : Set α⦄, MeasurableSet s → μ ((fun x => c • x) ⁻¹' s) = μ s
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.colimitIsoColimitCurryCompColim_ι_hom_assoc : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (G : CategoryTheory.Functor (J × K) C) [inst_3 : CategoryTheory.Limits.HasColimitsOfShape K C]
  [inst_4 : CategoryTheory.Limits.HasColimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)]
  {j : J} {k : K} {Z : C}
  (h : CategoryTheory.Limits.colimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G (j, k))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitIsoColimitCurryCompColim G).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj G).obj j) k)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim) j) h)
-- Mathlib.Algebra.DirectSum.Algebra
GradedMonoid.smulCommClass_right : ∀ {ι : Type uι} (R : Type uR) (A : ι → Type uA) [inst : CommSemiring R] [inst_1 : (i : ι) → AddCommMonoid (A i)]
  [inst_2 : (i : ι) → Module R (A i)] [inst_3 : AddMonoid ι] [inst_4 : DirectSum.GSemiring A] [DirectSum.GAlgebra R A],
  SMulCommClass R (GradedMonoid A) (GradedMonoid A)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.linear_ofLinearEquiv : ∀ {k : Type u_10} {V : Type u_11} {P : Type u_12} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (A : V ≃ₗ[k] V) (p₀ p₁ : P), (AffineEquiv.ofLinearEquiv A p₀ p₁).linear = A
-- Mathlib.Order.Category.Semilat
SemilatSupCat.coe_forget_to_partOrd : ∀ (X : SemilatSupCat), ↑((CategoryTheory.forget₂ SemilatSupCat PartOrd).obj X) = X.X
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.dsimp : Lean.Meta.Sym.DSimp.DSimproc
-- Mathlib.Analysis.Analytic.Constructions
/-- Eta-expanded form of `AnalyticWithinAt.zpow_nonneg`

---

ZPowers of analytic functions (into a normed division algebra over `𝕜`) are analytic if the
exponent is nonnegative.  -/
AnalyticWithinAt.fun_zpow_nonneg : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f : E → 𝕝}
  {z : E} {s : Set E} {n : ℤ}, AnalyticWithinAt 𝕜 f s z → 0 ≤ n → AnalyticWithinAt 𝕜 (fun i => f i ^ n) s z
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_cons_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k},
  Std.Internal.List.containsKey a (⟨k, v⟩ :: l) = false ↔ (k == a) = false ∧ Std.Internal.List.containsKey a l = false
-- Mathlib.Data.WSeq.Basic
/-- Weak sequences.

While the `Seq` structure allows for lists which may not be finite,
a weak sequence also allows the computation of each element to
involve an indeterminate amount of computation, including possibly
an infinite loop. This is represented as a regular `Seq` interspersed
with `none` elements to indicate that computation is ongoing.

This model is appropriate for Haskell style lazy lists, and is closed
under most interesting computation patterns on infinite lists,
but conversely it is difficult to extract elements from it.  -/
Stream'.WSeq : Type u_1 → Type u_1
-- Lean.Meta.Hint
Lean.Meta.Hint.DiffGranularity.auto.sizeOf_spec : sizeOf Lean.Meta.Hint.DiffGranularity.auto = 1
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
ProbabilityTheory.Kernel.partialTraj_le_def : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} {a b : ℕ}
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))} (hab : a ≤ b),
  ProbabilityTheory.Kernel.partialTraj κ a b =
    Nat.leRec ProbabilityTheory.Kernel.id
      (fun k x κ_k =>
        ((ProbabilityTheory.Kernel.id.prod ((κ k).map ⇑(MeasurableEquiv.piSingleton k))).comp κ_k).map
          (IicProdIoc k (k + 1)))
      hab
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.instCoeTC : {X : Type u_1} → CoeTC X (OnePoint X)
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.OplaxTrans.Hom.of.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} [inst_2 : SizeOf B] [inst_3 : SizeOf C]
  (as : CategoryTheory.Oplax.OplaxTrans.Modification η θ), sizeOf { as := as } = 1 + sizeOf as
-- Mathlib.Data.EReal.Inv
EReal.div_eq_inv_mul : ∀ (a b : EReal), a / b = b⁻¹ * a
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.HandlerTrie.insertStruct : Lean.Elab.ConfigEval.HandlerTrie✝ → Lean.Name → Lean.Name → Lean.Elab.ConfigEval.HandlerTrie✝
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
/-- A periodic function is interval integrable over every interval if it is interval integrable over one
period.
 -/
Function.Periodic.intervalIntegrable : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T t : ℝ},
  Function.Periodic f T →
    T ≠ 0 →
      IntervalIntegrable f MeasureTheory.volume t (t + T) →
        ∀ (a₁ a₂ : ℝ), IntervalIntegrable f MeasureTheory.volume a₁ a₂
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.splitMin'.match_3.eq_2 : ∀ {α : Type u_1} (motive : Ordnode α → α → Ordnode α → Sort u_2) (size : ℕ) (ll : Ordnode α) (lx : α) (lr : Ordnode α)
  (x : α) (r : Ordnode α) (h_1 : (x : α) → (r : Ordnode α) → motive Ordnode.nil x r)
  (h_2 :
    (size : ℕ) →
      (ll : Ordnode α) →
        (lx : α) → (lr : Ordnode α) → (x : α) → (r : Ordnode α) → motive (Ordnode.node size ll lx lr) x r),
  (match Ordnode.node size ll lx lr, x, r with
    | Ordnode.nil, x, r => h_1 x r
    | Ordnode.node size ll lx lr, x, r => h_2 size ll lx lr x r) =
    h_2 size ll lx lr x r
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjectiveSpectrum.Proj.isIso_toSpec : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A) {m : ℕ},
  f ∈ 𝒜 m → 0 < m → CategoryTheory.IsIso (AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f)
-- Mathlib.Analysis.Calculus.FDeriv.Mul
HasStrictFDerivAt.mul' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸] {a b : E → 𝔸}
  {a' b' : E →L[𝕜] 𝔸} {x : E},
  HasStrictFDerivAt a a' x →
    HasStrictFDerivAt b b' x → HasStrictFDerivAt (a * b) (a x • b' + MulOpposite.op (b x) • a') x
-- Mathlib.Combinatorics.SimpleGraph.Copy
_private.Mathlib.Combinatorics.SimpleGraph.Copy.0.SimpleGraph.aux : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W},
  H ≠ ⊥ → ∀ {G' : G.Subgraph}, Nonempty (H ≃g G'.coe) → G'.edgeSet.Nonempty
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.diff.congr_simp : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m₁ m₁_1 : Std.ExtHashSet α), m₁ = m₁_1 → ∀ (m₂ m₂_1 : Std.ExtHashSet α), m₂ = m₂_1 → m₁.diff m₂ = m₁_1.diff m₂_1