mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.ofIso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G X : C} [inst_2 : CategoryTheory.GrpObj G] (e : G ≅ X),
  CategoryTheory.GrpObj.inv =
    CategoryTheory.CategoryStruct.comp e.inv (CategoryTheory.CategoryStruct.comp CategoryTheory.GrpObj.inv e.hom)
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.fold_eq_foldTR.go : ∀ (α : Type u_1) (init : α) (m n : ℕ) (f : (i : ℕ) → i < m + n → α → α),
  (m + n).fold f init = Nat.foldTR.loop✝ (m + n) f m ⋯ (n.fold (fun i h => f i ⋯) init)
-- Mathlib.Order.WithBot
_private.Mathlib.Order.WithBot.0.WithBot.decidableLT.match_1.eq_1 : ∀ {α : Type u_1} (motive : WithBot α → WithBot α → Sort u_2) (x : WithBot α) (h_1 : (x : WithBot α) → motive x none)
  (h_2 : (a : α) → motive none (some a)) (h_3 : (a b : α) → motive (some a) (some b)),
  (match x, none with
    | x, none => h_1 x
    | none, some a => h_2 a
    | some a, some b => h_3 a b) =
    h_1 x
-- Mathlib.Algebra.Order.Group.MinMax
min_inv_inv_le : ∀ {G₀ : Type u_1} [inst : Inv G₀] [inst_1 : LinearOrder G₀] {x y : G₀}, min x⁻¹ y⁻¹ ≤ (max x y)⁻¹
-- Init.Prelude
/-- The proof that `val` satisfies the predicate `p`.
 -/
Subtype.property : ∀ {α : Sort u} {p : α → Prop} (self : Subtype p), p ↑self
-- Mathlib.Data.Finset.Union
Finset.biUnion_union : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t₁ t₂ : α → Finset β} [inst : DecidableEq β],
  (s.biUnion fun x => t₁ x ∪ t₂ x) = s.biUnion t₁ ∪ s.biUnion t₂
-- Mathlib.Order.SuccPred.Basic
Order.succ_eq_succ_iff_of_not_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α},
  ¬IsMax a → ¬IsMax b → (Order.succ a = Order.succ b ↔ a = b)
-- Mathlib.CategoryTheory.Sites.LeftExact
CategoryTheory.SheafOfTypes.adhesive : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [CategoryTheory.HasSheafify J (Type w)], CategoryTheory.Adhesive (CategoryTheory.Sheaf J (Type w))
-- Mathlib.LinearAlgebra.Matrix.Dual
dotProductEquiv_symm_apply : ∀ (R : Type u_1) (n : Type u_2) [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (f : Module.Dual R (n → R)) (i : n), (dotProductEquiv R n).symm f i = f ((LinearMap.single R (fun a => R) i) 1)
-- Mathlib.Algebra.Group.Commute.Units
Commute.units_inv_right : ∀ {M : Type u_1} [inst : Monoid M] {a : M} {u : Mˣ}, Commute a ↑u → Commute a ↑u⁻¹
-- Std.Data.Internal.List.Associative
Std.Internal.List.keys_eq_map : ∀ {α : Type u} {β : α → Type v} {l : List ((a : α) × β a)}, Std.Internal.List.keys l = List.map (fun x => x.fst) l
-- Mathlib.Data.Nat.Choose.Dvd
Nat.Prime.dvd_choose_self : ∀ {p k : ℕ}, Nat.Prime p → k ≠ 0 → k < p → p ∣ p.choose k
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {W : CategoryTheory.MorphismProperty C} {J : Type w}
  {inst_1 : LinearOrder J} {inst_2 : SuccOrder J} {inst_3 : OrderBot J} {inst_4 : WellFoundedLT J} {X Y : C} {f : X ⟶ Y}
  {toTransfiniteCompositionOfShape : CategoryTheory.TransfiniteCompositionOfShape J f}
  {map_mem : ∀ (j : J), ¬IsMax j → W (toTransfiniteCompositionOfShape.F.map (CategoryTheory.homOfLE ⋯))}
  {toTransfiniteCompositionOfShape_1 : CategoryTheory.TransfiniteCompositionOfShape J f}
  {map_mem_1 : ∀ (j : J), ¬IsMax j → W (toTransfiniteCompositionOfShape_1.F.map (CategoryTheory.homOfLE ⋯))},
  { toTransfiniteCompositionOfShape := toTransfiniteCompositionOfShape, map_mem := map_mem } =
      { toTransfiniteCompositionOfShape := toTransfiniteCompositionOfShape_1, map_mem := map_mem_1 } →
    toTransfiniteCompositionOfShape = toTransfiniteCompositionOfShape_1
-- Mathlib.Topology.Order.OrderClosed
Filter.Tendsto.eventually_le_const : ∀ {α : Type u} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {l : Filter γ}
  {f : γ → α} {u v : α}, v < u → Filter.Tendsto f l (nhds v) → ∀ᶠ (a : γ) in l, f a ≤ u
-- Mathlib.Topology.Algebra.Valued.WithVal
Valuation.IsEquiv.uniformEquiv.congr_simp : ∀ {R : Type u_4} {Γ₀ : Type u_5} {Γ₀' : Type u_6} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_2 : LinearOrderedCommGroupWithZero Γ₀'] {v : Valuation R Γ₀} {w : Valuation R Γ₀'} (h : v.IsEquiv w),
  h.uniformEquiv = h.uniformEquiv
-- Mathlib.Topology.ClusterPt
MapClusterPt.tendsto_comp : ∀ {X : Type u} [inst : TopologicalSpace X] {Y : Type v} {α : Type u_1} {F : Filter α} {u : α → X} {x : X}
  [inst_1 : TopologicalSpace Y] {f : X → Y} {y : Y},
  Filter.Tendsto f (nhds x) (nhds y) → MapClusterPt x F u → MapClusterPt y F (f ∘ u)
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.mulCayley_empty : ∀ {M : Type u_1} [inst : Mul M], SimpleGraph.mulCayley ∅ = ⊥
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.instNontrivialUnits : ∀ {α : Type u_1} [inst : Group α] [Nontrivial α], Nontrivial (WithZero α)ˣ
-- Init.Data.Range.Polymorphic.PRange
Std.Ric.HasRcoIntersection.mk : {α : Type w} → (Std.Ric α → Std.Rco α → Std.Rco α) → Std.Ric.HasRcoIntersection α
-- Lean.Meta.Tactic.Grind.Action
Lean.Meta.Grind.instToMessageDataActionResult : Lean.ToMessageData Lean.Meta.Grind.ActionResult
-- Mathlib.Control.Monad.Writer
MonadWriter.mk : {ω : outParam (Type u)} →
  {M : Type u → Type v} →
    (ω → M PUnit.{u + 1}) → ({α : Type u} → M α → M (α × ω)) → ({α : Type u} → M (α × (ω → ω)) → M α) → MonadWriter ω M
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.Equivalence.isDenseSubsite_functor_of_isCocontinuous : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D)
  [e.functor.IsCocontinuous J K] [e.inverse.IsCocontinuous K J], CategoryTheory.Functor.IsDenseSubsite J K e.functor
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.LaxTrans.Modification.id_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) (a : B),
  (CategoryTheory.Oplax.LaxTrans.Modification.id η).app a = CategoryTheory.CategoryStruct.id (η.app a)
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Sum.Swap.isEquivalence : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D],
  (CategoryTheory.Sum.swap C D).IsEquivalence
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.mem_support_iff : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R} {m : σ →₀ ℕ},
  m ∈ p.support ↔ MvPolynomial.coeff m p ≠ 0
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly.match_4.congr_eq_5 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Expr)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_3 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)) (a b : Lean.Grind.CommRing.Expr),
  x = a.add b →
    (match x with
      | Lean.Grind.CommRing.Expr.num k => h_1 k
      | Lean.Grind.CommRing.Expr.intCast k => h_2 k
      | Lean.Grind.CommRing.Expr.natCast k => h_3 k
      | Lean.Grind.CommRing.Expr.var x => h_4 x
      | a.add b => h_5 a b
      | a.mul b => h_6 a b
      | a.neg => h_7 a
      | a.sub b => h_8 a b
      | a.pow k => h_9 a k) ≍
      h_5 a b
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.instUniqueOfIsAlgebraicOfIsRelational : {L : FirstOrder.Language} → {L' : FirstOrder.Language} → [L.IsAlgebraic] → [L.IsRelational] → Unique (L →ᴸ L')
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_hom_inv_id_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C] {Z : ChainComplex C ℕ} (h : s.nondegComplex ⟶ Z),
  CategoryTheory.CategoryStruct.comp s.toKaroubiNondegComplexIsoN₁.hom.f
      (CategoryTheory.CategoryStruct.comp s.toKaroubiNondegComplexIsoN₁.inv.f h) =
    h
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.toNormalizedChainComplex_fromNormalizedChainComplex : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C),
  CategoryTheory.CategoryStruct.comp (X.toNormalizedChainComplex R) (X.fromNormalizedChainComplex R) =
    AlgebraicTopology.DoldKan.PInfty
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
IsSimpleGroup.prime_card : ∀ {α : Type u_1} [inst : CommGroup α] [IsSimpleGroup α], Nat.Prime (Nat.card α)
-- Mathlib.Topology.MetricSpace.Cauchy
/-- A Cauchy sequence on the natural numbers is bounded.  -/
cauchySeq_bdd : ∀ {α : Type u} [inst : PseudoMetricSpace α] {u : ℕ → α}, CauchySeq u → ∃ R > 0, ∀ (m n : ℕ), dist (u m) (u n) < R
-- Lean.Meta.Basic
/-- Set the array of postponed universe level constraints.  -/
Lean.Meta.setPostponed : Lean.PersistentArray Lean.Meta.PostponedEntry → Lean.MetaM Unit
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get_eq_getD : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {a : α} {fallback : β} {h : m.contains a = true},
      Std.DHashMap.Internal.Raw₀.Const.get m a h = Std.DHashMap.Internal.Raw₀.Const.getD m a fallback
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_sub_sub : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [inst : Sub β]
  [MeasurableSub₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k l : ι), i ≠ k → i ≠ l → j ≠ k → j ≠ l → ProbabilityTheory.Kernel.IndepFun (f i - f j) (f k - f l) κ μ
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Multipliable.vanishing : ∀ {α : Type u_1} {G : Type u_4} [inst : TopologicalSpace G] [inst_1 : CommGroup G] [IsTopologicalGroup G] {f : α → G},
  Multipliable f → ∀ ⦃e : Set G⦄, e ∈ nhds 1 → ∃ s, ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e
-- Std.Http.Test.Helpers
_private.Std.Http.Test.Helpers.0.Std.Http.Internal.Test.sendRaw : Std.Http.Internal.Mock.Client →
  Std.Http.Internal.Mock.Server → ByteArray → Std.Http.Internal.Test.TestHandler → Std.Http.Config → IO ByteArray
-- Mathlib.Order.Disjointed
/-- The function mapping `i` to `f i \ (⨆ j < i, f j)`. When `ι` is a partial order, this is the
unique function `g` having the same `partialSups` as `f` and such that `g i` and `g j` are
disjoint whenever `i < j`.  -/
disjointed : {α : Type u_1} →
  {ι : Type u_2} → [GeneralizedBooleanAlgebra α] → [inst : Preorder ι] → [LocallyFiniteOrderBot ι] → (ι → α) → ι → α
-- Mathlib.Algebra.Group.Irreducible.Defs
of_addIrreducible_add : ∀ {M : Type u_1} [inst : AddMonoid M] {a b : M}, AddIrreducible (a + b) → IsAddUnit a ∨ IsAddUnit b
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.realize_term_substructure : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] {α : Type u_5} {S : L.Substructure M} (v : α → ↥S)
  (t : L.Term α), FirstOrder.Language.Term.realize (Subtype.val ∘ v) t = ↑(FirstOrder.Language.Term.realize v t)
-- Lean.Data.Position
Lean.FileMap.toPosition : Lean.FileMap → String.Pos.Raw → Lean.Position
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBump.one_of_mem_closedBall : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E] {c : E}
  (f : ContDiffBump c) {x : E}, x ∈ Metric.closedBall c f.rIn → ↑f x = 1
-- Mathlib.Data.Set.Subsingleton
Set.not_nontrivial_empty : ∀ {α : Type u}, ¬∅.Nontrivial
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1SCLM_zero_left : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ 0 C) (f : ↥(α →₁ₛ[μ] E)),
  (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f = 0
-- Mathlib.Algebra.GroupWithZero.ProdHom
MonoidWithZeroHom.inr_apply_unit : ∀ {G₀ : Type u_1} {H₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : GroupWithZero H₀]
  [inst_2 : DecidablePred fun x => x = 0] (x : H₀ˣ), (MonoidWithZeroHom.inr G₀ H₀) ↑x = ↑(1, x)
-- Mathlib.RingTheory.KrullDimension.Module
Module.supportDim_eq_bot_iff_subsingleton : ∀ (R : Type u_1) [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.supportDim R M = ⊥ ↔ Subsingleton M
-- Mathlib.Order.Defs.PartialOrder
instIsPartialOrder_mathlib : ∀ {α : Type u_1} [inst : PartialOrder α], Std.IsPartialOrder α
-- Mathlib.Analysis.InnerProductSpace.PiL2
FiniteDimensional.orthonormalBasisSingleton_apply : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : Unique ι] (h : Module.finrank 𝕜 E = 1) {v : E}
  (hv : ‖v‖ = 1) (i : ι), (FiniteDimensional.orthonormalBasisSingleton ι 𝕜 h v hv) i = v
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Bialgebra.TensorProduct.counitAlgHom_def : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Bialgebra S A] [inst_5 : Bialgebra R B] [inst_6 : Algebra R A]
  [inst_7 : Algebra R S] [inst_8 : IsScalarTower R S A],
  Bialgebra.counitAlgHom S (TensorProduct R A B) =
    (↑(Algebra.TensorProduct.rid R S S)).comp
      (Algebra.TensorProduct.map (Bialgebra.counitAlgHom S A) (Bialgebra.counitAlgHom R B))
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.toSetoid_injective : ∀ {M : Type u_1} [inst : Add M], Function.Injective AddCon.toSetoid
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.mapCongr_inv_app : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f g : X ⟶ Y) (h : f = g)
  (X_1 : CategoryTheory.Under Y), (CategoryTheory.Under.mapCongr f g h).inv.app X_1 = CategoryTheory.eqToHom ⋯
-- Lean.Widget.Diff
_private.Lean.Widget.Diff.0.Lean.Widget.instEmptyCollectionExprDiff : EmptyCollection Lean.Widget.ExprDiff✝
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.opIso_hom_fst : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P Q : C) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct P Q],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.opIso P Q).hom CategoryTheory.Limits.biprod.fst =
    CategoryTheory.Limits.biprod.inl.op
-- Mathlib.Algebra.Order.Monovary
AntivaryOn.mul_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : PartialOrder β] {s : Set ι} {f₁ f₂ : ι → α} {g : ι → β},
  AntivaryOn f₁ g s → AntivaryOn f₂ g s → AntivaryOn (f₁ * f₂) g s
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
/-- Left homotopy is an equivalence relation on the edges of `A`.
Remark: We could have equivalently chosen right homotopy, as shown by `homotopicL_iff_homotopicR`.
 -/
SSet.Truncated.instSetoidEdge : {A : SSet.Truncated 2} →
  [A.Quasicategory₂] →
    (x y : A.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })) →
      Setoid (SSet.Truncated.Edge x y)
-- Mathlib.Algebra.CharP.Defs
CharP.congr : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {q : ℕ}, p = q → CharP R q
-- Lean.Meta.Sym.SymM
/-- Reports an issue if `verbose` mode is enabled. Does nothing if `verbose` is `false`.  -/
Lean.Meta.Sym.reportIssueIfVerbose : Lean.MessageData → Lean.Meta.Sym.SymM Unit
-- Mathlib.Data.Set.Disjoint
Set.disjoint_univ : ∀ {α : Type u} {s : Set α}, Disjoint s Set.univ ↔ s = ∅
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.symm_self_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y), α.symm ≪≫ α = CategoryTheory.Iso.refl Y
-- Mathlib.Algebra.GroupWithZero.Indicator
Function.support_pow' : ∀ {ι : Type u_1} {M₀ : Type u_4} [inst : MonoidWithZero M₀] [IsReduced M₀] {n : ℕ} (f : ι → M₀),
  n ≠ 0 → Function.support (f ^ n) = Function.support f
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.isRegularMono_unop_iff_isRegularEpi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ⟶ Y),
  CategoryTheory.IsRegularMono f.unop ↔ CategoryTheory.IsRegularEpi f
-- Mathlib.Combinatorics.Additive.ETransform
/-- An **e-transform**. Turns `(s, t)` into `(s ∪ s • e, t ∩ e⁻¹ • t)`. This reduces the
product of the two sets.  -/
Finset.mulETransformRight : {α : Type u_1} → [DecidableEq α] → [Group α] → α → Finset α × Finset α → Finset α × Finset α
-- Mathlib.NumberTheory.LSeries.ZMod
/-- The L-function of `Φ` has a residue at `s = 1` equal to the average value of `Φ`.  -/
ZMod.LFunction_residue_one : ∀ {N : ℕ} [inst : NeZero N] (Φ : ZMod N → ℂ),
  Filter.Tendsto (fun s => (s - 1) * ZMod.LFunction Φ s) (nhdsWithin 1 {1}ᶜ) (nhds (∑ j, Φ j / ↑N))
-- Mathlib.Data.Nat.Choose.Multinomial
Finsupp.multinomial_update : ∀ {α : Type u_1} (a : α) (f : α →₀ ℕ), f.multinomial = (f.sum fun x => id).choose (f a) * (f.update a 0).multinomial
-- Init.Data.UInt.Lemmas
USize.ofNat_add : ∀ (a b : ℕ), USize.ofNat (a + b) = USize.ofNat a + USize.ofNat b
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.mem_top : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] {x : A}, x ∈ ⊤
-- Mathlib.Order.SuccPred.Limit
Order.isSuccPrelimitRecOn.eq_1 : ∀ {α : Type u_1} (b : α) {motive : α → Sort u_2} [inst : PartialOrder α] [inst_1 : SuccOrder α]
  (succ : (a : α) → ¬IsMax a → motive (Order.succ a)) (isSuccPrelimit : (a : α) → Order.IsSuccPrelimit a → motive a),
  Order.isSuccPrelimitRecOn b succ isSuccPrelimit =
    if hb : Order.IsSuccPrelimit b then isSuccPrelimit b hb else cast ⋯ (succ (Classical.choose ⋯) ⋯)
-- Init.Data.Array.Bootstrap
_private.Init.Data.Array.Bootstrap.0.Array.toListImpl.eq_1 : ∀ {α : Type u} (as : Array α), as.toListImpl = Array.foldr List.cons [] as
-- Mathlib.ModelTheory.Basic
/-- The homomorphism sends related elements to related elements  -/
FirstOrder.Language.HomClass.map_rel : ∀ {L : outParam FirstOrder.Language} {F : Type u_3} {M : outParam (Type u_4)} {N : outParam (Type u_5)}
  {inst : FunLike F M N} {inst_1 : L.Structure M} {inst_2 : L.Structure N} [self : L.HomClass F M N] (φ : F) {n : ℕ}
  (r : L.Relations n) (x : Fin n → M),
  FirstOrder.Language.Structure.RelMap r x → FirstOrder.Language.Structure.RelMap r (⇑φ ∘ x)
-- Batteries.Data.Fin.Lemmas
Fin.sum_eq_sum_map_finRange : ∀ {α : Type u_1} {n : ℕ} [inst : Zero α] [inst_1 : Add α] (x : Fin n → α),
  Fin.sum x = (List.map x (List.finRange n)).sum
-- Lean.Meta.Sym.Pattern
/-- Attempts to unify expression `e` against pattern `p`, allowing metavariables in `e`.

Returns `some result` if unification succeeds, where `result` contains:
- `us`: Level assignments for the pattern's universe variables
- `args`: Expression assignments for the pattern's bound variables

Unlike `match?`, this handles terms containing metavariables by deferring
constraints to Phase 2 unification. Use this when matching against goal
expressions that may contain unsolved metavariables.

Instance arguments are synthesized (or assigned by unification). Any that cannot be resolved are
reported in `MatchUnifyResult.unresolvedInsts` rather than silently left as loose metavariables in
`args`. Proof arguments are skipped via proof irrelevance.
 -/
Lean.Meta.Sym.Pattern.unify? : Lean.Meta.Sym.Pattern → Lean.Expr → optParam Bool true → Lean.Meta.Sym.SymM (Option Lean.Meta.Sym.MatchUnifyResult)
-- Mathlib.Order.Interval.Finset.Defs
Set.toFinset_Iic : ∀ {α : Type u_3} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] (a : α) [inst_2 : Fintype ↑(Set.Iic a)],
  (Set.Iic a).toFinset = Finset.Iic a
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.div_const : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ}
  [inst_3 : Div γ] [MeasurableDiv γ],
  ProbabilityTheory.IdentDistrib f g μ ν →
    ∀ (c : γ), ProbabilityTheory.IdentDistrib (fun x => f x / c) (fun x => g x / c) μ ν
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorXMapBifunctorMapObjπ : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_4} C₂₃] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₂₃] [inst_9 : CategoryTheory.Preadditive C₄]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)}
  {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [inst_10 : G₂₃.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_12 : F.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₂₃ : Type u_11}
  {ι₄ : Type u_12} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁)
  (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄)
  [inst_14 : TotalComplexShape c₂ c₃ c₂₃] [inst_15 : TotalComplexShape c₁ c₂₃ c₄]
  [inst_16 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [inst_17 : DecidableEq ι₂₃]
  [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄],
  (((CategoryTheory.GradedObject.mapBifunctor F ι₁ ι₂₃).obj K₁.X).obj
        (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ (c₂.π c₃ c₂₃) K₂.X K₃.X)).HasMap
    (c₁.π c₂₃ c₄)
-- Mathlib.MeasureTheory.PiSystem
isPiSystem_Ico : ∀ {α : Type u_1} {ι : Sort u_3} {ι' : Sort u_4} [inst : LinearOrder α] (f : ι → α) (g : ι' → α),
  IsPiSystem {S | ∃ i j, f i < g j ∧ Set.Ico (f i) (g j) = S}
-- Mathlib.Topology.EMetricSpace.Defs
Metric.isOpen_eball : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {ε : ENNReal}, IsOpen (Metric.eball x ε)
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- `t : Cone F` is a limit cone if and only if `t.op : Cocone F.op` is a colimit cocone.
 -/
CategoryTheory.Limits.isLimitEquivIsColimitOp : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cone F} → CategoryTheory.Limits.IsLimit t ≃ CategoryTheory.Limits.IsColimit t.op
-- Mathlib.Data.Nat.ModEq
Nat.modEq_zero_iff : ∀ {a b : ℕ}, a ≡ b [MOD 0] ↔ a = b