mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.shiftFunctorCompIsoId_op_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ)
  (n m : ℤ) (hnm : autoParam (n + m = 0) CategoryTheory.Pretriangulated.shiftFunctorCompIsoId_op_hom_app._auto_1),
  (CategoryTheory.shiftFunctorCompIsoId Cᵒᵖ n m hnm).hom.app X =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor Cᵒᵖ m).map ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).hom.app X))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n ⋯).hom.app
          (Opposite.op ((CategoryTheory.shiftFunctor C m).obj (Opposite.unop X))))
        ((CategoryTheory.shiftFunctorCompIsoId C m n ⋯).inv.app (Opposite.unop X)).op)
-- Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_δ_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_3 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare)
  (F : CategoryTheory.Sheaf J AddCommGrpCat) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) {Z : AddCommGrpCat} (h_1 : F.H' n₁ S.X₄ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (S.fromBiprod F n₀) (CategoryTheory.CategoryStruct.comp (S.δ F n₀ n₁ h) h_1) =
    CategoryTheory.CategoryStruct.comp 0 h_1
-- Mathlib.GroupTheory.Nilpotent
Subgroup.lowerCentralSeries_pi_of_finite : ∀ {η : Type u_2} {Gs : η → Type u_3} [inst : (i : η) → Group (Gs i)] [Finite η] (Ss : (i : η) → Subgroup (Gs i))
  (n : ℕ), (Subgroup.pi Set.univ Ss).lowerCentralSeries n = Subgroup.pi Set.univ fun i => (Ss i).lowerCentralSeries n
-- Mathlib.Analysis.LocallyConvex.AbsConvex
absConvex_absConvexHull : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜] {s : Set E}, AbsConvex 𝕜 ((absConvexHull 𝕜) s)
-- Mathlib.Data.ZMod.Basic
ZMod.ringEquivCongr_ringEquivCongr_apply : ∀ {a b c : ℕ} (hab : a = b) (hbc : b = c) (x : ZMod a),
  (ZMod.ringEquivCongr hbc) ((ZMod.ringEquivCongr hab) x) = (ZMod.ringEquivCongr ⋯) x
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.proj_bot_eq : ∀ {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : LocallyConnectedSpace X] {x y : X},
  ⊥.proj x = ⊥.proj y ↔ connectedComponent x = connectedComponent y
-- Mathlib.Topology.ContinuousMap.Interval
ContinuousMap.IccInclusionRight.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] {a b c : α} [inst_2 : Fact (a ≤ b)],
  ContinuousMap.IccInclusionRight = ContinuousMap.inclusion ⋯
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.solveCombine.injEq : ∀ (c₁ c₂ c₁_1 c₂_1 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.solveCombine c₁ c₂ =
      Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.solveCombine c₁_1 c₂_1) =
    (c₁ = c₁_1 ∧ c₂ = c₂_1)
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sin_bound : ∀ {x : ℂ}, ‖x‖ ≤ 1 → ‖Complex.sin x - (x - x ^ 3 / 6)‖ ≤ ‖x‖ ^ 5 / 100
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.addContent_iUnion : ∀ {α : Type u_1} {C : Set (Set α)} {G : Type u_2} [inst : AddCommMonoid G] {m : MeasureTheory.AddContent G C}
  {ι : Type u_3} [inst_1 : Fintype ι] {f : ι → Set α},
  (∀ (i : ι), f i ∈ C) → Pairwise (Function.onFun Disjoint f) → ⋃ i, f i ∈ C → m (⋃ i, f i) = ∑ i, m (f i)
-- Mathlib.GroupTheory.Perm.Support
/-- Two permutations `f` and `g` are `Disjoint` if their supports are disjoint, i.e.,
every element is fixed either by `f`, or by `g`.  -/
Equiv.Perm.Disjoint : {α : Type u_1} → Equiv.Perm α → Equiv.Perm α → Prop
-- Std.Data.DTreeMap.Lemmas
/-- Simpler variant of `getD_filter` when `LawfulEqCmp` is available.  -/
Std.DTreeMap.Const.getD_filter' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {f : α → β → Bool} {k : α} {fallback : β},
  Std.DTreeMap.Const.getD (Std.DTreeMap.filter f t) k fallback =
    (Option.filter (f k) (Std.DTreeMap.Const.get? t k)).getD fallback
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.mul_add_left_right_iff : ∀ {R : Type u_1} [inst : CommRing R] {x y z : R}, IsRelPrime x (x * z + y) ↔ IsRelPrime x y
-- Lean.Elab.App
/-- Returns the argument syntax if the next positional argument is of the form `_`.
 -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.nextArgHole? : Lean.Elab.Term.ElabAppArgs.M (Option Lean.Syntax)
-- Mathlib.Order.Ideal
/-- The supremum of two ideals of a co-directed order is the union of the down sets of the pointwise
supremum of `I` and `J`.  -/
Order.Ideal.instMax : {P : Type u_1} → [inst : SemilatticeSup P] → [IsCodirectedOrder P] → Max (Order.Ideal P)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.tan_pi_div_two_sub : ∀ (x : ℂ), Complex.tan (↑Real.pi / 2 - x) = (Complex.tan x)⁻¹
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
pinGroup.instInhabitedSubtypeCliffordAlgebraMemSubmonoid : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {Q : QuadraticForm R M} → Inhabited ↥(pinGroup Q)
-- Batteries.Data.Array.Basic
_private.Batteries.Data.Array.Basic.0.Array.scanrMUnsafe : {m : Type u_1 → Type u_2} →
  {α : Type u_3} →
    {β : Type u_1} → [Monad m] → (α → β → m β) → β → (as : Array α) → optParam ℕ as.size → optParam ℕ 0 → m (Array β)
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.containsThenInsertIfNew_snd_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} (h : m.WF) {a : α}
  {b : β a}, (m.containsThenInsertIfNew a b).2 = ↑(Std.DHashMap.Internal.Raw₀.containsThenInsertIfNew ⟨m, ⋯⟩ a b).2
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_eq_false_iff_exists_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → (t.isEmpty = false ↔ ∃ a, a ∈ t)
-- Mathlib.Data.Matrix.Basis
Matrix.diag_single_of_ne : ∀ {n : Type u_3} {α : Type u_7} [inst : DecidableEq n] [inst_1 : Zero α] (i j : n) (c : α),
  i ≠ j → (Matrix.single i j c).diag = 0
-- Mathlib.CategoryTheory.ComposableArrows.Four
CategoryTheory.ComposableArrows.fourδ₂Toδ₁_app_two : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂)
  (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃),
  (CategoryTheory.ComposableArrows.fourδ₂Toδ₁ f₁ f₂ f₃ f₄ f₁₂ f₂₃ h₁₂ h₂₃).app 2 =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₃ f₁ f₂₃ f₄).obj 2)
-- Mathlib.Analysis.Calculus.FDeriv.Const
hasFDerivWithinAt_intCast : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : IntCast F] (z : ℤ) (x : E) (s : Set E), HasFDerivWithinAt (↑z) 0 s x
-- Mathlib.Algebra.GroupWithZero.Basic
exists_isNilpotent_of_not_isReduced : ∀ {R : Type u_5} [inst : Zero R] [inst_1 : Pow R ℕ], ¬IsReduced R → ∃ x, x ≠ 0 ∧ IsNilpotent x
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.aeval_root_eq_map : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f), Polynomial.aeval h.root = h.map
-- Mathlib.RingTheory.Ideal.Basic
Ideal.add_pow_add_pred_mem_of_pow_mem_of_commute : ∀ {α : Type u_6} [inst : Semiring α] (I : Ideal α) {a b : α} {m n : ℕ},
  a ^ m ∈ I → b ^ n ∈ I → Commute a b → (a + b) ^ (m + n - 1) ∈ I
-- Init.Grind.Ring.Basic
/-- Numerals are consistently defined with respect to the canonical map from natural numbers.  -/
Lean.Grind.Semiring.ofNat_eq_natCast : ∀ {α : Type u} [self : Lean.Grind.Semiring α] (n : ℕ), OfNat.ofNat n = ↑n
-- Lean.Elab.ConfigEval.MetaInstances
Lean.Elab.ConfigEval.instEvalExprEtaStructMode.evalExpr : Lean.Expr → Lean.MetaM Lean.Meta.EtaStructMode
-- Mathlib.Algebra.Notation.Prod
Prod.fst_neg : ∀ {G : Type u_8} {H : Type u_9} [inst : Neg G] [inst_1 : Neg H] (p : G × H), (-p).1 = -p.1
-- Mathlib.Order.WellFoundedSet
Set.IsWF.min_eq_of_lt : ∀ {α : Type u_2} [inst : Preorder α] {s : Set α} {a : α} (hs : s.IsWF) (ha : a ∈ s),
  (∀ b ∈ s, b ≠ a → a < b) → hs.min ⋯ = a
-- Mathlib.CategoryTheory.Action.Monoidal
Action.whiskerLeft_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.MonoidalCategory V] (X : Action V G) {Y₁ Y₂ : Action V G} (f : Y₁ ⟶ Y₂),
  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).hom =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.V f.hom
-- Lean.Meta.Tactic.Assert
Lean.Meta.Hypothesis.type : Lean.Meta.Hypothesis → Lean.Expr
-- Init.Data.List.Nat.TakeDrop
List.take_one : ∀ {α : Type u_1} {l : List α}, List.take 1 l = l.head?.toList
-- Mathlib.RingTheory.Henselian
HenselianLocalRing.is_henselian : ∀ {R : Type u_1} {inst : CommRing R} [self : HenselianLocalRing R] (f : Polynomial R),
  f.Monic →
    ∀ (a₀ : R),
      Polynomial.eval a₀ f ∈ IsLocalRing.maximalIdeal R →
        IsUnit (Polynomial.eval a₀ (Polynomial.derivative f)) → ∃ a, f.IsRoot a ∧ a - a₀ ∈ IsLocalRing.maximalIdeal R
-- Mathlib.CategoryTheory.Presentable.SharplyLT.Basic
_private.Mathlib.CategoryTheory.Presentable.SharplyLT.Basic.0.Cardinal.SharplyLT.existsIsCardinalFilteredSetOfExistsCofinal.subset_iUnion : ∀ {κ₁ κ₂ : Cardinal.{w}} [Fact κ₁.IsRegular] {X : Type w}
  (Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (CategoryTheory.CardinalDirectedPoset.SetCardinalLT κ₁ ↑B))
  (m :
    (B : Set X) →
      (hB : HasCardinalLT (↑B) κ₂) → (C : CategoryTheory.CardinalDirectedPoset.SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X)
  (A : Set X), A ⊆ ⋃ j, transfiniteIterate (Cardinal.SharplyLT.existsIsCardinalFilteredSetOfExistsCofinal.φ✝ Y m) j A
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
/-- If `A` is local and `B` is a local and flat `A`-algebra, then `B` is faithfully flat.  -/
Module.FaithfullyFlat.of_flat_of_isLocalHom : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [IsLocalRing A]
  [IsLocalRing B] [Module.Flat A B] [IsLocalHom (algebraMap A B)], Module.FaithfullyFlat A B
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- `StructuredArrow.post` is a special case of `StructuredArrow.map₂` up to natural isomorphism.  -/
CategoryTheory.StructuredArrow.postIsoMap₂ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {B : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} B] →
            (S : C) →
              (F : CategoryTheory.Functor B C) →
                (G : CategoryTheory.Functor C D) →
                  CategoryTheory.StructuredArrow.post S F G ≅
                    CategoryTheory.StructuredArrow.map₂ (CategoryTheory.CategoryStruct.id (G.obj S))
                      (CategoryTheory.CategoryStruct.id (F.comp G))
-- Mathlib.Tactic.Widget.StringDiagram
/-- The underlying expression of the strand.  -/
Mathlib.Tactic.Widget.StringDiagram.Strand.atom₁ : Mathlib.Tactic.Widget.StringDiagram.Strand → Mathlib.Tactic.BicategoryLike.Atom₁
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_le_size_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, t.size ≤ (t.insertIfNew k v).size
-- Mathlib.Probability.Moments.MGFAnalytic
ProbabilityTheory.analyticOnNhd_mgf : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  AnalyticOnNhd ℝ (ProbabilityTheory.mgf X μ) (interior (ProbabilityTheory.integrableExpSet X μ))
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.MonadHom.app_η : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C}
  (self : CategoryTheory.MonadHom T₁ T₂) (X : C),
  CategoryTheory.CategoryStruct.comp (T₁.η.app X) (self.app X) = T₂.η.app X
-- Mathlib.Order.Hom.Basic
OrderIso.coe_toRelIsoLT : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β), ⇑e.toRelIsoLT = ⇑e
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.mem_support_iff : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v), w ∈ p.support ↔ w = u ∨ w ∈ p.support.tail
-- Mathlib.CategoryTheory.EssentialImage
CategoryTheory.Functor.toEssImageCompι_hom_app : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (X : C), F.toEssImageCompι.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.Analysis.Normed.Ring.InfiniteSum
tsum_mul_tsum_of_summable_norm' : ∀ {R : Type u_1} {ι : Type u_2} {ι' : Type u_3} [inst : NormedRing R] {f : ι → R} {g : ι' → R},
  (Summable fun x => ‖f x‖) →
    Summable f →
      (Summable fun x => ‖g x‖) → Summable g → (∑' (x : ι), f x) * ∑' (y : ι'), g y = ∑' (z : ι × ι'), f z.1 * g z.2
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_mono_ae_restrict : ∀ {f g : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
  a ≤ b →
    IntervalIntegrable f μ a b →
      IntervalIntegrable g μ a b →
        f ≤ᵐ[μ.restrict (Set.Icc a b)] g → ∫ (u : ℝ) in a..b, f u ∂μ ≤ ∫ (u : ℝ) in a..b, g u ∂μ
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
Std.Iterators.Types.FilterMap.mk : {α β γ : Type w} →
  {m : Type w → Type w'} →
    {n : Type w → Type w''} →
      {lift : ⦃α : Type w⦄ → m α → n α} →
        {f : β → Std.Iterators.PostconditionT n (Option γ)} → Std.IterM m β → Std.Iterators.Types.FilterMap α m n lift f
-- Lean.Data.Lsp.Window
Lean.Lsp.instFromJsonShowMessageRequestParams : Lean.FromJson Lean.Lsp.ShowMessageRequestParams
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- The 2-cocycles of the complex of inhomogeneous cochains of `A` are isomorphic to
`cocycles₂ A`, which is a simpler type.  -/
groupCohomology.isoCocycles₂ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) → groupCohomology.cocycles A 2 ≅ ModuleCat.of k ↥(groupCohomology.cocycles₂ A)
-- Mathlib.Topology.Algebra.Group.SubmonoidClosure
mapClusterPt_atTop_pow_iff_mem_topologicalClosure_zpowers : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [CompactSpace G] [inst_3 : IsTopologicalGroup G]
  {x y : G}, (MapClusterPt x Filter.atTop fun x => y ^ x) ↔ x ∈ (Subgroup.zpowers y).topologicalClosure
-- Mathlib.Analysis.SpecialFunctions.Log.Summable
Real.hasProd_of_hasSum_log : ∀ {ι : Type u_1} {f : ι → ℝ} {a : ℝ}, (∀ (i : ι), 0 < f i) → HasSum (fun i => Real.log (f i)) a → HasProd f (Real.exp a)
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteAddGrp.instCoeSortType.eq_1 : FiniteAddGrp.instCoeSortType = { coe := fun G => ↑G.toAddGrp }
-- Mathlib.Topology.Sets.VietorisTopology
Continuous.compacts_map' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f : α → TopologicalSpace.Compacts β} {g : α → β → γ},
  Continuous f →
    ∀ (hg : Continuous (Function.uncurry g)), Continuous fun x => TopologicalSpace.Compacts.map (g x) ⋯ (f x)
-- Mathlib.RingTheory.Coalgebra.MulOpposite
MulOpposite.instCoalgebraStruct : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid A] → [inst_2 : Module R A] → [CoalgebraStruct R A] → CoalgebraStruct R Aᵐᵒᵖ
-- Mathlib.Dynamics.TopologicalEntropy.Semiconj
Dynamics.coverEntropy_image_le_of_uniformContinuousOn_invariant : ∀ {X : Type u_1} {Y : Type u_2} [inst : UniformSpace X] [inst_1 : UniformSpace Y] {S : X → X} {T : Y → Y} {φ : X → Y},
  Function.Semiconj φ S T →
    ∀ {F G : Set X},
      UniformContinuousOn φ G → F ⊆ G → Set.MapsTo S G G → Dynamics.coverEntropy T (φ '' F) ≤ Dynamics.coverEntropy S F
-- Init.Data.List.Lemmas
List.self_eq_append_left : ∀ {α : Type u_1} {xs ys : List α}, ys = xs ++ ys ↔ xs = []
-- Mathlib.Algebra.Algebra.Hom
Algebra.toRingHom_ofId : ∀ {R : Type u} (A : Type v) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  ↑(Algebra.ofId R A) = algebraMap R A
-- Init.Data.List.Lemmas
List.length_map : ∀ {α : Type u_1} {β : Type u_2} {as : List α} (f : α → β), (List.map f as).length = as.length
-- Init.Data.Nat.Gcd
Nat.pow_dvd_pow_iff : ∀ {a b n : ℕ}, n ≠ 0 → (a ^ n ∣ b ^ n ↔ a ∣ b)
-- Mathlib.Topology.Neighborhoods
/-- If a predicate is true in a neighborhood of `x`, then it is true for `x`.  -/
Filter.Eventually.self_of_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {p : X → Prop}, (∀ᶠ (y : X) in nhds x, p y) → p x
-- Mathlib.Algebra.Lie.EngelSubalgebra
LieSubalgebra.self_mem_engel : ∀ (R : Type u_1) {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (x : L),
  x ∈ LieSubalgebra.engel R x
-- Mathlib.GroupTheory.Commutator.Basic
commutatorSet.eq_1 : ∀ (G : Type u_1) [inst : Group G], commutatorSet G = {g | ∃ g₁ g₂, ⁅g₁, g₂⁆ = g}
-- Init.Data.Sum.Lemmas
Sum.elim_inl_inr : ∀ {α : Type u_1} {β : Type u_2}, Sum.elim Sum.inl Sum.inr = id
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.subst_add : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {a : MvPowerSeries τ S},
  PowerSeries.HasSubst a →
    ∀ (f g : PowerSeries R), PowerSeries.subst a (f + g) = PowerSeries.subst a f + PowerSeries.subst a g
-- Mathlib.Topology.MetricSpace.Holder
/-- If a function is `(C₁, r)`-Hölder and `(C₂, s)`-Hölder, then it is
`(C₁ ^ t₁ * C₂ ^ t₂, r * t₁ + s * t₂)`-Hölder for all `t₁ t₂ : ℝ≥0` such that
`t₁ + t₂ = 1`.  -/
HolderWith.interpolate : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {r : NNReal} {f : X → Y}
  {C₁ C₂ s t₁ t₂ : NNReal},
  HolderWith C₁ r f → HolderWith C₂ s f → t₁ + t₂ = 1 → HolderWith (C₁ ^ ↑t₁ * C₂ ^ ↑t₂) (r * t₁ + s * t₂) f
-- Init.Omega.Int
Lean.Omega.Int.emod_ofNat_nonneg : ∀ {x : ℕ} {y : ℤ}, 0 ≤ ↑x % y
-- Mathlib.Topology.NoetherianSpace
TopologicalSpace.noetherianSpace_set_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s : Set α), TopologicalSpace.NoetherianSpace ↑s ↔ ∀ t ⊆ s, IsCompact t
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.FunctorObjIndex.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {I : Type w} {A B : I → C} {f : (i : I) → A i ⟶ B i} {S X : C}
  {πX : X ⟶ S} {i : I} {t : A i ⟶ X} {b : B i ⟶ S}
  {w : CategoryTheory.CategoryStruct.comp t πX = CategoryTheory.CategoryStruct.comp (f i) b} {i_1 : I} {t_1 : A i_1 ⟶ X}
  {b_1 : B i_1 ⟶ S} {w_1 : CategoryTheory.CategoryStruct.comp t_1 πX = CategoryTheory.CategoryStruct.comp (f i_1) b_1},
  { i := i, t := t, b := b, w := w } = { i := i_1, t := t_1, b := b_1, w := w_1 } → i = i_1 ∧ t ≍ t_1 ∧ b ≍ b_1
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.addEquivOfLocalizations_left_neg : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) (k : N ≃+ P),
  f.addEquivOfLocalizations (f.ofAddEquivOfLocalizations k) = k
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.instUniqueRMulticospanShapeSigmaOfIsColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      (E : CategoryTheory.PreOneHypercover S) →
        {c : CategoryTheory.Limits.Cofan E.X} →
          (hc : CategoryTheory.Limits.IsColimit c) →
            {d : CategoryTheory.Limits.Cofan E.Y'} →
              (hd : CategoryTheory.Limits.IsColimit d) → Unique (E.sigmaOfIsColimit hc hd).multicospanShape.R
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `DifferentiableAt.sub` -/
DifferentiableAt.fun_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {x : E}, DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 g x → DifferentiableAt 𝕜 (fun i => f i - g i) x
-- Lean.Meta.PProdN
/-- Given values `xᵢ` of type `tᵢ`, produces value of type `t₁ ×' t₂ ×' t₃`  -/
Lean.Meta.PProdN.mk : Lean.Level → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.Vector.Basic
Vector.firstM : {β : Type v} → {n : ℕ} → {α : Type u} → {m : Type v → Type w} → [Alternative m] → (α → m β) → Vector α n → m β
-- Mathlib.Computability.Partrec
Computable₂.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} [inst : Primcodable α] [inst_1 : Primcodable β]
  [inst_2 : Primcodable γ] [inst_3 : Primcodable σ] {f : β → γ → σ} {g : α → β} {h : α → γ},
  Computable₂ f → Computable g → Computable h → Computable fun a => f (g a) (h a)
-- Mathlib.Data.Fin.Parity
Fin.odd_add_one_iff_even : ∀ {n : ℕ} {k : Fin n} [inst : NeZero n], Odd (k + 1) ↔ Even k
-- Aesop.Util.Basic
Aesop.tacticsToMessageData : Array Lean.Syntax.Tactic → Lean.MessageData
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_le_one : ∀ {x : NNReal} {z : ℝ}, x ≤ 1 → 0 ≤ z → x ^ z ≤ 1
-- Mathlib.Analysis.Normed.Group.Constructions
MulOpposite.norm_op : ∀ {E : Type u_2} [inst : SeminormedAddGroup E] (a : E), ‖MulOpposite.op a‖ = ‖a‖
-- Mathlib.RingTheory.Polynomial.Dickson
Polynomial.dickson_two_one_eq_chebyshev_U : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : Invertible 2] (n : ℕ),
  Polynomial.dickson 2 1 n = (Polynomial.Chebyshev.U R ↑n).comp (Polynomial.C ⅟2 * Polynomial.X)
-- Mathlib.Probability.ProductMeasure
/-- `partialTraj κ a b` is a kernel which up to an equivalence is equal to
`Kernel.id ×ₖ (κ a ⊗ₖ ... ⊗ₖ κ (b - 1))`. This lemma therefore states that if the kernel `κ i`
is constant equal to `μ i` for all `i`, then up to an equivalence
`partialTraj κ a b = Kernel.id ×ₖ Kernel.const (⨂ μ i)`.  -/
MeasureTheory.partialTraj_const : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} (μ : (n : ℕ) → MeasureTheory.Measure (X n))
  [hμ : ∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μ n)] {a b : ℕ},
  ProbabilityTheory.Kernel.partialTraj
      (fun n => ProbabilityTheory.Kernel.const ((i : ↥(Finset.Iic n)) → X ↑i) (μ (n + 1))) a b =
    (ProbabilityTheory.Kernel.id.prod
          (ProbabilityTheory.Kernel.const ((i : ↥(Finset.Iic a)) → X ↑i) (MeasureTheory.Measure.pi fun i => μ ↑i))).map
      (IicProdIoc a b)
-- Mathlib.Data.QPF.Multivariate.Constructions.Comp
/-- Constructor for functor composition  -/
MvQPF.Comp.mk : {n m : ℕ} →
  {F : TypeVec.{u} n → Type u_1} →
    {G : Fin2 n → TypeVec.{u} m → Type u} → {α : TypeVec.{u} m} → (F fun i => G i α) → MvQPF.Comp F G α
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_sum : ∀ {K : Type u_1} [inst : RCLike K] {α : Type u_3} (s : Finset α) (f : α → ℝ), ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.degree_scaleRoots : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) {s : R}, (p.scaleRoots s).degree = p.degree
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
Module.End.injective_of_surjective : ∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  [Module.Finite R M] [IsStablyFiniteRing R] {f : Module.End R M}, Function.Surjective ⇑f → Function.Injective ⇑f
-- Mathlib.Algebra.Star.Basic
Int.instTrivialStar : TrivialStar ℤ
-- Init.Data.Float.Float32
/-- Strict inequality of floating-point numbers. Typically used via the `<` operator.
 -/
Float32.lt : Float32 → Float32 → Bool
-- Mathlib.CategoryTheory.Groupoid.VertexGroup
CategoryTheory.Groupoid.vertexGroup_inv : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (c : C) (a : c ⟶ c), a⁻¹ = CategoryTheory.Groupoid.inv a