mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- Composition by continuous linear equivs on the left respects higher differentiability at a
point.  -/
ContinuousLinearEquiv.comp_contDiffAt_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {x : E} {n : WithTop ℕ∞} (e : F ≃L[𝕜] G),
  ContDiffAt 𝕜 n (⇑e ∘ f) x ↔ ContDiffAt 𝕜 n f x
-- Mathlib.Algebra.Group.Submonoid.Membership
ofMul_image_powers_eq_multiples_ofMul : ∀ {M : Type u_1} [inst : Monoid M] {x : M},
  ⇑Additive.ofMul '' ↑(Submonoid.powers x) = ↑(AddSubmonoid.multiples (Additive.ofMul x))
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.continuous_inclusion : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} {𝓕 : Filter ι} [inst : (i : ι) → TopologicalSpace (R i)]
  {𝓖 : Filter ι} (h : 𝓕 ≤ 𝓖), Continuous (RestrictedProduct.inclusion R A h)
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.closure_mul_closure : ∀ {R : Type u_2} [inst : NonUnitalNonAssocSemiring R] (S T : Set R),
  AddSubmonoid.closure S * AddSubmonoid.closure T = AddSubmonoid.closure (S * T)
-- Mathlib.Algebra.Group.Submonoid.BigOperators
SubmonoidClass.coe_list_prod : ∀ {M : Type u_1} {B : Type u_3} [inst : Monoid M] [inst_1 : SetLike B M] [inst_2 : SubmonoidClass B M] {S : B}
  (l : List ↥S), ↑l.prod = (List.map Subtype.val l).prod
-- Init.Core
instSubsingletonProd : ∀ {α : Type u_1} {β : Type u_2} [Subsingleton α] [Subsingleton β], Subsingleton (α × β)
-- Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
/-- A small positive number such that any `1 - δ`-separated set in the ball of radius `2` has
cardinality at most `Besicovitch.multiplicity E`.  -/
Besicovitch.goodδ : (E : Type u_1) → [inst : NormedAddCommGroup E] → [inst_1 : NormedSpace ℝ E] → [FiniteDimensional ℝ E] → ℝ
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineMap.homothety_mem : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : CommRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : AffineSubspace k P} {c : P},
  c ∈ s → ∀ (r : k) {p : P}, p ∈ s → (AffineMap.homothety c r) p ∈ s
-- Mathlib.CategoryTheory.MarkovCategory.Basic
/-- Process then discard equals discard directly.  -/
CategoryTheory.MarkovCategory.discard_natural : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MarkovCategory C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp f CategoryTheory.ComonObj.counit = CategoryTheory.ComonObj.counit
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.ofNatCode.match_3.eq_2 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : Unit → motive 2)
  (h_4 : Unit → motive 3) (h_5 : (n : ℕ) → motive n.succ.succ.succ.succ),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | 2 => h_3 ()
    | 3 => h_4 ()
    | n.succ.succ.succ.succ => h_5 n) =
    h_2 ()
-- Mathlib.RepresentationTheory.Coinvariants
Representation.coinvariantsFinsuppLEquiv_apply : ∀ {k : Type u_6} {G : Type u_7} {V : Type u_8} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] {ρ : Representation k G V} {α : Type u_9} (x : (ρ.finsupp α).Coinvariants),
  (ρ.coinvariantsFinsuppLEquiv α) x = (ρ.coinvariantsToFinsupp α) x
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.CokernelCofork.mapIsoOfIsColimit_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} {X' Y' : C} {f' : X' ⟶ Y'} {cc : CategoryTheory.Limits.CokernelCofork f}
  {cc' : CategoryTheory.Limits.CokernelCofork f'} (hf : CategoryTheory.Limits.IsColimit cc)
  (hf' : CategoryTheory.Limits.IsColimit cc') (φ : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f'),
  (CategoryTheory.Limits.CokernelCofork.mapIsoOfIsColimit hf hf' φ).hom =
    CategoryTheory.Limits.CokernelCofork.mapOfIsColimit hf cc' φ.hom
-- Mathlib.Tactic.IntervalCases
/-- Given a type `ty` (the type of a hypothesis in the context or a provided expression),
attempt to parse it as an inequality, and return `(a, b, strict, positive)`, where
`positive` means it is a negated inequality and `strict` means it is a strict inequality
(`a < b` or `a ≱ b`). `a` is always the lesser argument and `b` the greater one.
 -/
Mathlib.Tactic.IntervalCases.parseBound : Lean.Expr → Lean.MetaM (Lean.Expr × Lean.Expr × Bool × Bool)
-- Mathlib.RingTheory.Valuation.Extension
Valuation.HasExtension.instAlgebra_valuationSubring : {K : outParam (Type u_5)} →
  {L : outParam (Type u_6)} →
    {Γ₀ : outParam (Type u_7)} →
      {Γ₁ : outParam (Type u_8)} →
        [inst : Field K] →
          [inst_1 : Field L] →
            [inst_2 : Algebra K L] →
              [inst_3 : LinearOrderedCommGroupWithZero Γ₀] →
                [inst_4 : LinearOrderedCommGroupWithZero Γ₁] →
                  (vK : Valuation K Γ₀) →
                    (vL : Valuation L Γ₁) → [vK.HasExtension vL] → Algebra ↥vK.valuationSubring ↥vL.valuationSubring
-- Mathlib.Probability.StrongLaw
ProbabilityTheory.truncation_nonneg : ∀ {α : Type u_1} {f : α → ℝ} (A : ℝ) {x : α}, 0 ≤ f x → 0 ≤ ProbabilityTheory.truncation f A x
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
/-- The property of being `C^n`, initially defined in terms of the Fréchet derivative, can be
reformulated in terms of the one-dimensional derivative on sets with unique derivatives.  -/
contDiffOn_iff_continuousOn_differentiableOn_deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} {n : ℕ∞},
  UniqueDiffOn 𝕜 s →
    (ContDiffOn 𝕜 (↑n) f s ↔
      (∀ (m : ℕ), ↑m ≤ n → ContinuousOn (iteratedDerivWithin m f s) s) ∧
        ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s)
-- Lean.Elab.MatchAltView
Lean.Elab.Term.MatchAltView.mk : {k : Lean.SyntaxNodeKinds} →
  Lean.Syntax → Array Lean.Syntax → Lean.Syntax → Lean.TSyntax k → Lean.Elab.Term.MatchAltView k
-- Std.Data.Internal.List.Associative
Std.Internal.List.foldrM_eq_foldrM_keys : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m' : Type w → Type w'} [inst : Monad m'] [LawfulMonad m']
  {l : List ((a : α) × β a)} {f : α → δ → m' δ} {init : δ},
  List.foldrM (fun a b => f a.fst b) init l = List.foldrM f init (Std.Internal.List.keys l)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_sqrt_three : Real.arctan √3 = Real.pi / 3
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.MapsTo.inv : ∀ {α : Type u_2} {β : Type u_3} [inst : InvolutiveInv β] {A : Set α} {B : Set β} {f : α → β},
  Set.MapsTo f A B → Set.MapsTo f⁻¹ A B⁻¹
-- Mathlib.MeasureTheory.Covering.VitaliFamily
Filter.HasBasis.vitaliFamily : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  (v : VitaliFamily μ) {ι : Sort u_2} {p : ι → Prop} {s : ι → Set X} {x : X},
  (nhds x).HasBasis p s → (v.filterAt x).HasBasis p fun i => {t | t ∈ v.setsAt x ∧ t ⊆ s i}
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.SymmetricRelation.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {R X : C} {p₁ p₂ : R ⟶ X}
  {toJointlyMono₂ : CategoryTheory.JointlyMono₂ p₁ p₂} {s : R ⟶ R}
  {symmetry₁ :
    autoParam (CategoryTheory.CategoryStruct.comp s p₁ = p₂) CategoryTheory.SymmetricRelation.symmetry₁._autoParam}
  {symmetry₂ :
    autoParam (CategoryTheory.CategoryStruct.comp s p₂ = p₁) CategoryTheory.SymmetricRelation.symmetry₂._autoParam}
  {toJointlyMono₂_1 : CategoryTheory.JointlyMono₂ p₁ p₂} {s_1 : R ⟶ R}
  {symmetry₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp s_1 p₁ = p₂) CategoryTheory.SymmetricRelation.symmetry₁._autoParam}
  {symmetry₂_1 :
    autoParam (CategoryTheory.CategoryStruct.comp s_1 p₂ = p₁) CategoryTheory.SymmetricRelation.symmetry₂._autoParam},
  { toJointlyMono₂ := toJointlyMono₂, s := s, symmetry₁ := symmetry₁, symmetry₂ := symmetry₂ } =
      { toJointlyMono₂ := toJointlyMono₂_1, s := s_1, symmetry₁ := symmetry₁_1, symmetry₂ := symmetry₂_1 } →
    s = s_1
-- Mathlib.Data.List.Sigma
List.dlookup_kunion_eq_some : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} {l₁ l₂ : List (Sigma β)},
  List.dlookup a (l₁.kunion l₂) = some b ↔ List.dlookup a l₁ = some b ∨ a ∉ l₁.keys ∧ List.dlookup a l₂ = some b
-- Mathlib.CategoryTheory.Monoidal.CommMon_
/-- The forgetful functor from commutative monoid objects to the ambient category.  -/
CategoryTheory.CommMon.forget : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.Functor (CategoryTheory.CommMon C) C
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.ExtractAndExtendBitTarget.mk.inj : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {aig : Std.Sat.AIG α} {w start : ℕ} {x : aig.RefVec w}
  {start_1 : ℕ} {x_1 : aig.RefVec w},
  { start := start, x := x } = { start := start_1, x := x_1 } → start = start_1 ∧ x = x_1
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.isStrictlyGE_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ) (n : ℤ),
  K.IsStrictlyGE n ↔
    ∀ (i : ℤ), autoParam (i < n) CochainComplex.isStrictlyGE_iff._auto_1 → CategoryTheory.Limits.IsZero (K.X i)
-- Mathlib.Topology.Algebra.Group.TopologicalAbelianization
_private.Mathlib.Topology.Algebra.Group.TopologicalAbelianization.0.termG_ab : Lean.ParserDescr
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.eval_rename_prod_mk : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (g : σ × τ → R) (i : σ) (p : MvPolynomial τ R),
  (MvPolynomial.eval g) ((MvPolynomial.rename (Prod.mk i)) p) = (MvPolynomial.eval fun j => g (i, j)) p
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.mapLIncl.eq_1 : ∀ {ι : Type u_1} [inst : Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] (p : (i : ι) → Submodule 𝕜 (E i)),
  PiTensorProduct.mapLIncl p = PiTensorProduct.mapL fun i => (p i).subtypeL
-- Lean.Meta.Sym.Apply
Lean.Meta.Sym.BackwardRule.mk.sizeOf_spec : ∀ (expr : Lean.Expr) (pattern : Lean.Meta.Sym.Pattern) (resultPos : List ℕ),
  sizeOf { expr := expr, pattern := pattern, resultPos := resultPos } =
    1 + sizeOf expr + sizeOf pattern + sizeOf resultPos
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.diagonal_transvection_induction' : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] [Nontrivial ι]
  (P : Matrix.SpecialLinearGroup ι F → Prop) (M : Matrix.SpecialLinearGroup ι F),
  (∀ (i j : ι) (hij : i ≠ j) {c : F} (hc : c ≠ 0), P (Matrix.SpecialLinearGroup.diag2n hij c hc)) →
    (∀ (i j : ι) (hij : i ≠ j) (a : F), P (Matrix.SpecialLinearGroup.transvection hij a)) →
      (∀ (A B : Matrix.SpecialLinearGroup ι F), P A → P B → P (A * B)) → P M
-- Init.Data.UInt.Lemmas
UInt64.toUInt8_sub : ∀ (a b : UInt64), (a - b).toUInt8 = a.toUInt8 - b.toUInt8
-- Mathlib.Algebra.Algebra.Subalgebra.Rank
Subalgebra.finrank_left_dvd_finrank_sup_of_free : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (A B : Subalgebra R S)
  [Module.Free R ↥A] [Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)], Module.finrank R ↥A ∣ Module.finrank R ↥(A ⊔ B)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey?_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k k' : α} {f : β → β},
  (Std.DHashMap.Const.modify m k f).getKey? k' =
    if (k == k') = true then if k ∈ m then some k else none else m.getKey? k'
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- A binary cofan in the opposite category gives a binary fan.  -/
CategoryTheory.Limits.BinaryCofan.unop : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → CategoryTheory.Limits.BinaryCofan (Opposite.op X) (Opposite.op Y) → CategoryTheory.Limits.BinaryFan X Y
-- Init.Data.Int.Lemmas
Int.sub_neg : ∀ (a b : ℤ), a - -b = a + b
-- Init.Data.Order.Ord
Std.LawfulBEqOrd.equivBEq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Ord α] [Std.LawfulBEqOrd α] [Std.TransOrd α], EquivBEq α
-- Mathlib.Order.Minimal
/-- If two sets are order isomorphic, their maximals are also order isomorphic.  -/
OrderIso.mapSetOfPredMaximal : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        {s : Set α} → {t : Set β} → ↑s ≃o ↑t → ↑{x | Maximal (fun x => x ∈ s) x} ≃o ↑{x | Maximal (fun x => x ∈ t) x}
-- Lean.Server.CodeActions.Provider
/-- A code action which calls all `@[hole_code_action]` code actions on each hole
(`?_`, `_`, or `sorry`).
 -/
Lean.CodeAction.holeCodeActionProvider : Lean.Server.CodeActionProvider
-- Mathlib.Topology.Algebra.Constructions
Units.isEmbedding_embedProduct : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Monoid M], Topology.IsEmbedding ⇑(Units.embedProduct M)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
/-- Conditional expectation of a function as a linear map from `α →₁[μ] F'` to itself.  -/
MeasureTheory.condExpL1CLM : {α : Type u_1} →
  (F' : Type u_3) →
    [inst : NormedAddCommGroup F'] →
      [inst_1 : NormedSpace ℝ F'] →
        {m m0 : MeasurableSpace α} →
          (hm : m ≤ m0) →
            (μ : MeasureTheory.Measure α) →
              [CompleteSpace ↥(MeasureTheory.Lp F' 1 μ)] →
                [MeasureTheory.SigmaFinite (μ.trim hm)] → ↥(MeasureTheory.Lp F' 1 μ) →L[ℝ] ↥(MeasureTheory.Lp F' 1 μ)
-- Init.Data.Array.Lemmas
Array.replicate.eq_1 : ∀ {α : Type u} (n : ℕ) (v : α), Array.replicate n v = { toList := List.replicate n v }
-- Mathlib.Algebra.Tropical.Basic
Tropical.mulLeftStrictMono : ∀ {R : Type u} [inst : LT R] [inst_1 : Add R] [AddLeftStrictMono R], MulLeftStrictMono (Tropical R)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem_toList_rco : ∀ {m n i : ℕ} (_h : i < (m...n).toList.length), (m...n).toList[i] = m + i
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
_private.Mathlib.CategoryTheory.Limits.Shapes.Countable.0.CategoryTheory.Limits.IsCofiltered.hasCountableLimits_of_hasFiniteLimits_and_hasSequentialLimits : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Limits.HasFiniteLimits C] →
      [CategoryTheory.Limits.HasLimitsOfShape ℕᵒᵖ C] → ProofWanted (CategoryTheory.Limits.HasCountableLimits C)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.instIsSubApply : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E}, IsSubApply (ContDiffMapSupportedIn E F n K) E F
-- Std.Data.ByteSlice
_private.Std.Data.ByteSlice.0.Std.Slice.Internal.ByteSliceData.mk.injEq : ∀ (byteArray : ByteArray) (start stop : ℕ) (start_le_stop : start ≤ stop)
  (stop_le_size_byteArray : stop ≤ byteArray.size) (byteArray_1 : ByteArray) (start_1 stop_1 : ℕ)
  (start_le_stop_1 : start_1 ≤ stop_1) (stop_le_size_byteArray_1 : stop_1 ≤ byteArray_1.size),
  ({ byteArray := byteArray, start := start, stop := stop, start_le_stop := start_le_stop,
        stop_le_size_byteArray := stop_le_size_byteArray } =
      { byteArray := byteArray_1, start := start_1, stop := stop_1, start_le_stop := start_le_stop_1,
        stop_le_size_byteArray := stop_le_size_byteArray_1 }) =
    (byteArray = byteArray_1 ∧ start = start_1 ∧ stop = stop_1)
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.Injective.mk : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {ϕ : L →ᴸ L'},
  (∀ {n : ℕ}, Function.Injective fun f => ϕ.onFunction f) →
    (∀ {n : ℕ}, Function.Injective fun R => ϕ.onRelation R) → ϕ.Injective
-- Init.Data.Array.Basic
Array.idxOfAux : {α : Type u} → [BEq α] → (xs : Array α) → α → ℕ → Option (Fin xs.size)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- The abbreviation for the limit of `ProfiniteAddGrp`s.  -/
ProfiniteAddGrp.limit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    CategoryTheory.Functor J ProfiniteAddGrp.{max v u} → ProfiniteAddGrp.{max v u}
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.Multiset.ProveZeroOrConsResult.zero.inj : ∀ {u : Lean.Level} {α : Q(Type u)} {s : Q(Multiset «$α»)} {pf pf_1 : Q(«$s» = 0)},
  Mathlib.Meta.Multiset.ProveZeroOrConsResult.zero pf = Mathlib.Meta.Multiset.ProveZeroOrConsResult.zero pf_1 →
    pf = pf_1
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.comp_mapAddGrp_add_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {E : Type u₃} [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.CartesianMonoidalCategory E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [inst_6 : F.Monoidal] [inst_7 : G.Monoidal]
  (A : CategoryTheory.AddGrp C) {Z : E} (h : ((F.comp G).mapAddGrp.obj A).X ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (F.comp G) A.X A.X)
        (G.map (F.map CategoryTheory.AddMonObj.add)))
      h
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Prod.swap_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X Y : C × D} (f : X ⟶ Y), (CategoryTheory.Prod.swap C D).map f = CategoryTheory.Prod.mkHom f.2 f.1
-- Mathlib.Topology.Algebra.Field
affineHomeomorph_image_Ico : ∀ {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [inst_4 : IsTopologicalRing 𝕜] (a b c d : 𝕜) (h : 0 < a),
  ⇑(affineHomeomorph a b ⋯) '' Set.Ico c d = Set.Ico (a * c + b) (a * d + b)
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.parenthesizerForKindUnsafe : Lean.SyntaxNodeKind → Lean.PrettyPrinter.Parenthesizer
-- Lean.Elab.PreDefinition.Structural.IndPred
_private.Lean.Elab.PreDefinition.Structural.IndPred.0.Lean.Elab.Structural.replaceIndPredRecApps.loop : Array Lean.Elab.Structural.RecArgInfo →
  Lean.Elab.Structural.Positions →
    Array Lean.Expr →
      (recFnNames : Array Lean.Name) →
        (Lean.Expr → StateRefT' IO.RealWorld (Lean.HasConstCache recFnNames) Lean.Elab.Structural.IndPredM✝ Bool) →
          Lean.Meta.IndPredBelow.RecursionContext →
            Lean.Expr → StateRefT' IO.RealWorld (Lean.HasConstCache recFnNames) Lean.Elab.Structural.IndPredM✝ Lean.Expr
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_filter_not_contains_map_fst : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.getKey? k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) =
      if Std.Internal.List.containsKey k l₂ = true then none else Std.Internal.List.getKey? k l₁
-- Mathlib.RingTheory.DedekindDomain.Factorization
Ideal.finprod_heightOneSpectrum_pow_multiplicity : ∀ {R : Type u_3} [inst : CommRing R] [IsDedekindDomain R] {I : Ideal R},
  I ≠ ⊥ → ∏ᶠ (p : IsDedekindDomain.HeightOneSpectrum R), p.asIdeal ^ multiplicity p.asIdeal I = I
-- Mathlib.Topology.Category.CompactlyGenerated
CompactlyGenerated.compactlyGeneratedToTop_map : ∀ {X Y : CategoryTheory.InducedCategory TopCat CompactlyGenerated.toTop} (f : X ⟶ Y),
  CompactlyGenerated.compactlyGeneratedToTop.map f = f.hom
-- Mathlib.Algebra.Category.MonCat.Colimits
/-- The function from the free monoid on the diagram to the cone point of any other cocone.  -/
MonCat.Colimits.descFunLift : {J : Type v} →
  [inst : CategoryTheory.Category.{u, v} J] →
    (F : CategoryTheory.Functor J MonCat) → (s : CategoryTheory.Limits.Cocone F) → MonCat.Colimits.Prequotient F → ↑s.pt
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.coe_copy : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} (f : 𝒜 →+*ᵍ ℬ) (f' : A → B) (h : f' = ⇑f),
  ⇑(f.copy f' h) = f'
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.add_mk_eq_max : ∀ {α β : Type u} [Infinite α], Cardinal.mk α + Cardinal.mk β = max (Cardinal.mk α) (Cardinal.mk β)
-- Init.Data.UInt.Lemmas
BitVec.ofFin_uInt64ToFin : ∀ (n : UInt64), { toFin := n.toFin } = n.toBitVec
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValRat.self_pow_inv : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (r : ℕ), padicValRat p (↑p ^ r)⁻¹ = -↑r
-- Mathlib.Data.Seq.Defs
Stream'.Seq.coinduction : ∀ {α : Type u} {s₁ s₂ : Stream'.Seq α},
  s₁.head = s₂.head → (∀ (β : Type u) (fr : Stream'.Seq α → β), fr s₁ = fr s₂ → fr s₁.tail = fr s₂.tail) → s₁ = s₂
-- Mathlib.Tactic.FunProp.FunctionData
Mathlib.Meta.FunProp.DecompositionResult.uncurried.sizeOf_spec : sizeOf Mathlib.Meta.FunProp.DecompositionResult.uncurried = 1
-- Mathlib.Data.FunLike.IsApply
/-- `IsDivApply F α β` states for all `f g : F` and `x : α`, `(f / g) x = f x / g x`.  -/
IsDivApply : (F : Type u_1) → (α : outParam (Type u_2)) → (β : outParam (Type u_3)) → [FunLike F α β] → [Div β] → [Div F] → Prop
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
/-- The equivalence of categories `(C ⥤ Karoubi D) ≌ (Karoubi C ⥤ Karoubi D)`.  -/
CategoryTheory.Idempotents.karoubiUniversal₁ : (C : Type u_1) →
  (D : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        CategoryTheory.Functor C (CategoryTheory.Idempotents.Karoubi D) ≌
          CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi C) (CategoryTheory.Idempotents.Karoubi D)
-- Init.Data.Order.Lemmas
Std.le_min_iff : ∀ {α : Type u} [inst : Min α] [inst_1 : LE α] [Std.LawfulOrderInf α] {a b c : α}, a ≤ b ⊓ c ↔ a ≤ b ∧ a ≤ c
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.addActionHom_singleton.eq_1 : ∀ (G : Type u_1) [inst : AddGroup G] (α : Type u_2) [inst_1 : AddAction G α] [inst_2 : DecidableEq α],
  Set.powersetCard.addActionHom_singleton G α = { toFun := ⇑Set.powersetCard.ofSingleton, map_vadd' := ⋯ }
-- Lean.Elab.PreDefinition.PartialFixpoint.Eqns
Lean.Elab.PartialFixpoint.EqnInfo.fixpointType : Lean.Elab.PartialFixpoint.EqnInfo → Array Lean.Elab.PartialFixpointType
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.add_const : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : AddGroup ι] [inst_1 : Preorder ι] [AddRightMono ι]
  [AddLeftMono ι] {f : MeasureTheory.Filtration ι m} {τ : Ω → WithTop ι},
  MeasureTheory.IsStoppingTime f τ → ∀ {i : ι}, 0 ≤ i → MeasureTheory.IsStoppingTime f fun ω => τ ω + ↑i
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.dirac_eq_zero_iff_not_mem : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α} {a : α},
  MeasurableSet s → ((MeasureTheory.Measure.dirac a) s = 0 ↔ a ∉ s)
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- Writing explicitly the `n+1`-th derivative as the composition of a currying linear equiv,
and the derivative of the `n`-th derivative.  -/
iteratedFDerivWithin_succ_eq_comp_left : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : ℕ},
  iteratedFDerivWithin 𝕜 (n + 1) f s =
    ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm ∘ fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s