mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.CommHopfAlgCat
/-- Forgetting to the underlying type and then building the bundled object returns the original Hopf
algebra.  -/
CommHopfAlgCat.ofIsoSelf : {R : Type u} →
  [inst : CommRing R] →
    (A : CommHopfAlgCat R) →
      { X := ↑A, commRing := CommHopfAlgCat.instCommRingObjForgetBialgHomX,
          hopfAlgebra := CommHopfAlgCat.instHopfAlgebraObjForgetBialgHomX } ≅
        A
-- Lean.Meta.DiscrTree.Util
/-- Fold the values stored in a `Trie`.
 -/
Lean.Meta.DiscrTree.Trie.foldValues : {σ : Type u_1} → {α : Type} → (σ → α → σ) → σ → Lean.Meta.DiscrTree.Trie α → σ
-- Mathlib.RingTheory.WittVector.Defs
WittVector.ext : ∀ {p : ℕ} {R : Type u_1} {x y : WittVector p R}, (∀ (n : ℕ), x.coeff n = y.coeff n) → x = y
-- Mathlib.Order.Filter.Pointwise
Filter.covariant_swap_div : ∀ {α : Type u_2} [inst : Div α],
  CovariantClass (Filter α) (Filter α) (Function.swap fun x1 x2 => x1 / x2) fun x1 x2 => x1 ≤ x2
-- Mathlib.Analysis.Fourier.ZMod
ZMod.invDFT_apply' : ∀ {N : ℕ} [inst : NeZero N] {E : Type u_1} [inst_1 : AddCommGroup E] [inst_2 : Module ℂ E] (Ψ : ZMod N → E)
  (k : ZMod N), ZMod.dft.symm Ψ k = (↑N)⁻¹ • ZMod.dft Ψ (-k)
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
/-- **Alias** of `Ordinal.cof_toType`. -/
Ordinal.cof_eq_cof_toType : ∀ (o : Ordinal.{u_1}), Order.cof o.ToType = o.cof
-- Init.Prelude
/-- The implementation of `~~~a : α`. 

Conventions for notations in identifiers:

 * The recommended spelling of `~~~` in identifiers is `not`. -/
Complement.complement : {α : Type u} → [self : Complement α] → α → α
-- Std.Async.Signal
Std.Async.Signal.sigttou.sizeOf_spec : sizeOf Std.Async.Signal.sigttou = 1
-- Mathlib.Topology.Algebra.OpenSubgroup
AddSubgroup.instFiniteQuotientSubtypeMemOpenAddSubgroupOfIsTopologicalAddGroupOfCompactSpace : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] [CompactSpace G]
  (U : OpenAddSubgroup G) (K : OpenAddSubgroup ↥U), Finite (↥U ⧸ ↑K)
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
seminormFromBounded'.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (f : R → ℝ) (x : R), seminormFromBounded' f x = ⨆ y, f (x * y) / f y
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
/-- The `ℕ∞`-valued additive valuation on a DVR.  -/
IsDiscreteValuationRing.addVal : (R : Type u) → [inst : CommRing R] → [inst_1 : IsDomain R] → [IsDiscreteValuationRing R] → AddValuation R ℕ∞
-- Init.Prelude
/-- Applies a function to the current state that has the explicitly-provided type `σ`. The function both
computes a new state and a value. The new state replaces the current state, and the value is
returned.

It is equivalent to `do let (a, s) := f (← getThe σ); set s; pure a`. However, using `modifyGetThe`
may lead to higher performance because it doesn't add a new reference to the state value. Additional
references can inhibit in-place updates of data.
 -/
modifyGetThe : {α : Type u} → (σ : Type u) → {m : Type u → Type v} → [MonadStateOf σ m] → (σ → α × σ) → m α
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.NonUnitalAlgebra.hom_ext_iff : ∀ {R : Type u_1} {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : CommSemiring R]
  [inst_5 : (i : ι) → NonUnitalNonAssocSemiring (G i)] [inst_6 : (i : ι) → DistribMulAction R (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)] [inst_8 : Nonempty ι] {P : Type u_7}
  [inst_9 : NonUnitalNonAssocSemiring P] [inst_10 : DistribMulAction R P] {g₁ g₂ : DirectLimit G f →ₙₐ[R] P},
  g₁ = g₂ ↔ ∀ (i : ι), g₁.comp (DirectLimit.NonUnitalAlgebra.of G f i) = g₂.comp (DirectLimit.NonUnitalAlgebra.of G f i)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.functorialityCompPostcompose_inv_app_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C}
  {H H' : CategoryTheory.Functor C D} (α : H ≅ H') (X : CategoryTheory.Limits.Cone F),
  ((CategoryTheory.Functor.functorialityCompPostcompose α).inv.app X).hom = α.inv.app X.pt
-- Mathlib.Algebra.Order.Star.Basic
star_le_star_iff : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {x y : R}, star x ≤ star y ↔ x ≤ y
-- Lean.PrettyPrinter.Delaborator.SubExpr
Lean.PrettyPrinter.Delaborator.SubExpr.withProj : {α : Type} →
  [Inhabited α] →
    {m : Type → Type} → [Monad m] → [MonadReaderOf Lean.SubExpr m] → [MonadWithReaderOf Lean.SubExpr m] → m α → m α
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleIcc_def_gt' : ∀ {n : ℕ} {i j : Fin n}, ¬j ≤ i → j.cycleIcc i = 1
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.quotQuotEquivComm_comp_quotQuotMkₐ : ∀ (R : Type u) {A : Type u_1} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (I J : Ideal A),
  (↑(DoubleQuot.quotQuotEquivCommₐ R I J)).comp (DoubleQuot.quotQuotMkₐ R I J) = DoubleQuot.quotQuotMkₐ R J I
-- Mathlib.Algebra.GradedMonoid
List.dProdIndex_cons : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddMonoid ι] (a : α) (l : List α) (fι : α → ι),
  (a :: l).dProdIndex fι = fι a + l.dProdIndex fι
-- Mathlib.Analysis.Calculus.Deriv.AffineMap
AffineMap.differentiable : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (f : 𝕜 →ᵃ[𝕜] E), Differentiable 𝕜 ⇑f
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.exists_coeff_ne_zero_iff_ne_zero : ∀ {R : Type u_1} [inst : Semiring R] {φ : PowerSeries R}, (∃ n, (PowerSeries.coeff n) φ ≠ 0) ↔ φ ≠ 0
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
HasFTaylorSeriesUpToOn.fderivWithin : ∀ {𝕜 : 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] {n : WithTop ℕ∞}
  {f : E → F} {p : E → FormalMultilinearSeries 𝕜 E F} {s : Set E},
  HasFTaylorSeriesUpToOn n f p s →
    ∀ (m : ℕ), ↑m < n → ∀ x ∈ s, HasFDerivWithinAt (fun x => p x m) (p x m.succ).curryLeft s x
-- Mathlib.Geometry.Convex.Cone.DualFinite
/-- The dual of a finitely generated cone is dually finitely generated.  -/
PointedCone.DualFG.dual_of_fg : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  (p : M →ₗ[R] N →ₗ[R] R) {C : PointedCone R M}, Submodule.FG C → PointedCone.DualFG p (PointedCone.dual p ↑C)
-- Mathlib.Logic.Encodable.Basic
/-- Constructive choice function for a decidable predicate over an encodable type.  -/
Encodable.choose : {α : Type u_1} → {p : α → Prop} → [Encodable α] → [DecidablePred p] → (∃ x, p x) → α
-- Mathlib.Topology.MetricSpace.MetricSeparated
Metric.AreSeparated.finset_iUnion_right_iff : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {ι : Type u_3} {I : Finset ι} {s : Set X} {t : ι → Set X},
  Metric.AreSeparated s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, Metric.AreSeparated s (t i)
-- Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
/-- Reinterpret a linear map `𝕜 →ₗ[𝕜] E` as a continuous linear map. This construction
is generalized to the case of any finite-dimensional domain
in `LinearMap.toContinuousLinearMap`.  -/
LinearMap.toContinuousLinearMap₁ : {𝕜 : Type u_1} →
  {E : Type u_3} →
    [inst : SeminormedRing 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] → [inst_2 : Module 𝕜 E] → [IsBoundedSMul 𝕜 E] → (𝕜 →ₗ[𝕜] E) → 𝕜 →L[𝕜] E
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.piEquivalenceFunctorDiscreteCompEvaluationIso_hom_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u_2} (j : J) (X : J → C),
  (CategoryTheory.piEquivalenceFunctorDiscreteCompEvaluationIso C j).hom.app X = CategoryTheory.CategoryStruct.id (X j)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift
AffineSubspace.shift_bot : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : AddTorsor V P]
  [inst_3 : Module k V] (c : P) (r : k), ⊥.shift c r = ⊥
-- Mathlib.Topology.Sets.OpenCover
TopologicalSpace.IsOpenCover.exists_mem : ∀ {ι : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] {u : ι → TopologicalSpace.Opens X},
  TopologicalSpace.IsOpenCover u → ∀ (a : X), ∃ i, a ∈ u i
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.GetElem?.match_1.eq_2 : ∀ (elem : outParam (Type u_1)) (motive : Option elem → Sort u_2) (h_1 : (e : elem) → motive (some e))
  (h_2 : Unit → motive none),
  (match none with
    | some e => h_1 e
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.add_lt_add_of_lt_of_le : ∀ {α : Type u} [inst : Add α] {w x y z : WithTop α} [inst_1 : Preorder α] [AddLeftMono α] [AddRightStrictMono α],
  x ≠ ⊤ → w < y → x ≤ z → w + x < y + z
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.instMonoOfLE : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B : C} (X Y : CategoryTheory.Subobject B) (h : X ≤ Y),
  CategoryTheory.Mono (X.ofLE Y h)
-- Init.Data.Int.LemmasAux
Int.min_max_distrib_left : ∀ (a b c : ℤ), min a (max b c) = max (min a b) (min a c)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
Std.Iterators.Types.ULiftIterator.Monadic.modifyStep.eq_3 : ∀ {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u}
  {lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ},
  Std.Iterators.Types.ULiftIterator.Monadic.modifyStep Std.IterStep.done = Std.IterStep.done
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
/-- Auxiliary definition for `Embedding.homRestrict`.  -/
ComplexShape.Embedding.homRestrict.f : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {e : c.Embedding c'} →
          {C : Type u_3} →
            [inst : CategoryTheory.Category.{v_1, u_3} C] →
              [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
                [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
                  {K : HomologicalComplex C c'} →
                    {L : HomologicalComplex C c} →
                      [inst_3 : e.IsRelIff] → (K ⟶ L.extend e) → (i : ι) → (K.restriction e).X i ⟶ L.X i
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.comap_apply : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] (w : NumberField.InfinitePlace K) (f : k →+* K)
  (x : k), (w.comap f) x = w (f x)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
HomogeneousSubmodule.mem_toSubmodule_iff : ∀ {ιA : Type u_1} {ιM : Type u_2} {σA : Type u_3} {σM : Type u_4} {A : Type u_5} {M : Type u_6} [inst : Semiring A]
  [inst_1 : AddCommMonoid M] [inst_2 : Module A M] (𝒜 : ιA → σA) (ℳ : ιM → σM) [inst_3 : DecidableEq ιA]
  [inst_4 : AddMonoid ιA] [inst_5 : SetLike σA A] [inst_6 : AddSubmonoidClass σA A] [inst_7 : GradedRing 𝒜]
  [inst_8 : DecidableEq ιM] [inst_9 : SetLike σM M] [inst_10 : AddSubmonoidClass σM M]
  [inst_11 : DirectSum.Decomposition ℳ] [inst_12 : VAdd ιA ιM] [inst_13 : SetLike.GradedSMul 𝒜 ℳ]
  {I : HomogeneousSubmodule 𝒜 ℳ} {x : M}, x ∈ I.toSubmodule ↔ x ∈ I
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
AddGroup.addLeftReflectLT_of_addLeftStrictMono : ∀ {N : Type u_2} [inst : AddGroup N] [inst_1 : LT N] [AddLeftStrictMono N], AddLeftReflectLT N
-- Mathlib.LinearAlgebra.Reflection
Module.infinite_range_reflection_reflection_iterate_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x : M}
  {f : Module.Dual R M} {y : M} {g : Module.Dual R M} [IsAddTorsionFree M] (hfx : f x = 2) (hgy : g y = 2),
  f y * g x = 4 →
    ((Set.range fun n => (⇑(Module.reflection hgy ≪≫ₗ Module.reflection hfx))^[n] y).Infinite ↔ f y • x ≠ 2 • y)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- Given a morphism `φ : S₁ ⟶ S₂` of short complexes and homology data `h₁` and `h₂`
for `S₁` and `S₂` respectively, this is the induced homology map `h₁.left.H ⟶ h₁.left.H`.  -/
CategoryTheory.ShortComplex.homologyMap' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (S₁ ⟶ S₂) → (h₁ : S₁.HomologyData) → (h₂ : S₂.HomologyData) → h₁.left.H ⟶ h₂.left.H
-- Mathlib.LinearAlgebra.TensorProduct.Basis
TensorProduct.equivFinsuppOfBasisLeft_apply_tmul_apply : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : DecidableEq ι]
  (ℬ : Module.Basis ι R M) (m : M) (n : N) (i : ι),
  ((TensorProduct.equivFinsuppOfBasisLeft ℬ) (m ⊗ₜ[R] n)) i = (ℬ.repr m) i • n
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.sum_hom₂_nonempty : ∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : AddMonoid M] [inst_1 : AddMonoid N]
  [inst_2 : AddMonoid P] {l : List ι} (f : M → N → P),
  (∀ (a b : M) (c d : N), f (a + b) (c + d) = f a c + f b d) →
    ∀ (f₁ : ι → M) (f₂ : ι → N),
      l ≠ [] → (List.map (fun i => f (f₁ i) (f₂ i)) l).sum = f (List.map f₁ l).sum (List.map f₂ l).sum
-- Mathlib.Topology.Algebra.Monoid
/-- Let `M` be a topological space with a continuous multiplication operation and a `0`.
Let `l` be a filter on `M` which is disjoint from the cocompact filter. Then, the multiplication map
`M × M → M` tends to zero on the filter product `𝓝 0 ×ˢ l`.  -/
tendsto_mul_nhds_zero_prod_of_disjoint_cocompact : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : MulZeroClass M] [ContinuousMul M] {l : Filter M},
  Disjoint l (Filter.cocompact M) → Filter.Tendsto (fun x => x.1 * x.2) (nhds 0 ×ˢ l) (nhds 0)
-- Init.GrindInstances.ToInt
Fin.instOfNat.eq_1 : ∀ {n : ℕ} [inst : NeZero n] {i : ℕ}, Fin.instOfNat = { ofNat := Fin.ofNat n i }
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.IsOrdinal.not_subset_iff_mem : ∀ {x y : ZFSet.{u}}, x.IsOrdinal → y.IsOrdinal → (¬x ⊆ y ↔ y ∈ x)
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.MVarValue.expr.injEq : ∀ (e e_1 : Lean.Expr), (Aesop.EqualUpToIds.MVarValue.expr e = Aesop.EqualUpToIds.MVarValue.expr e_1) = (e = e_1)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.PreOneHypercover.multifork.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} A]
  {S : C} (E : CategoryTheory.PreOneHypercover S) (F : CategoryTheory.Functor Cᵒᵖ A),
  E.multifork F =
    CategoryTheory.Limits.Multifork.ofι (E.multicospanIndex F) (F.obj (Opposite.op S)) (fun i₀ => F.map (E.f i₀).op) ⋯
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstr.mk.injEq : ∀ (p : Lean.Grind.Linarith.Poly) (strict : Bool) (h : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof)
  (p_1 : Lean.Grind.Linarith.Poly) (strict_1 : Bool) (h_1 : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof),
  ({ p := p, strict := strict, h := h } = { p := p_1, strict := strict_1, h := h_1 }) =
    (p = p_1 ∧ strict = strict_1 ∧ h = h_1)
-- Mathlib.Data.Set.Countable
Set.countable_univ : ∀ {α : Type u} [Countable α], Set.univ.Countable
-- Mathlib.Algebra.Colimit.Ring
Field.DirectLimit.exists_inv : ∀ {ι : Type u_1} [inst : Preorder ι] (G : ι → Type u_2) [Nonempty ι] [IsDirectedOrder ι]
  [inst_3 : (i : ι) → Field (G i)] (f : (i j : ι) → i ≤ j → G i → G j) {p : Ring.DirectLimit G f},
  p ≠ 0 → ∃ y, p * y = 1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_of_isEmpty : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, m.isEmpty = true → Std.DHashMap.Raw.Const.get? m a = none
-- Mathlib.Combinatorics.SetFamily.Shatter
Finset.Shatters.subset_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {s t : Finset α},
  𝒜.Shatters s → (t ⊆ s ↔ ∃ u ∈ 𝒜, s ∩ u = t)
-- Mathlib.Topology.MetricSpace.Antilipschitz
/-- **Alias** of the reverse direction of `antilipschitzWith_iff_le_mul_dist`. -/
AntilipschitzWith.of_le_mul_dist : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β},
  (∀ (x y : α), dist x y ≤ ↑K * dist (f x) (f y)) → AntilipschitzWith K f
-- Init.SimpLemmas
not_iff_self : ∀ {a : Prop}, ¬(¬a ↔ a)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The 3rd object in the complex of inhomogeneous chains of `A : Rep k G` is isomorphic
to `G³ → A` as a `k`-module.  -/
groupHomology.chainsIso₃ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) → (groupHomology.inhomogeneousChains A).X 3 ≅ ModuleCat.of k (G × G × G →₀ ↑A)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- If this is a `OfSemiring.Q α` ring, this field contain the
`semiringId` for `α`.
 -/
Lean.Meta.Grind.Arith.CommRing.CommRing.semiringId? : Lean.Meta.Grind.Arith.CommRing.CommRing → Option ℕ
-- Init.Data.UInt.Basic
instHModUInt32Nat : HMod UInt32 ℕ UInt32
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charpoly_reindex : ∀ {R : Type u_1} [inst : CommRing R] {m : Type u_3} {n : Type u_4} [inst_1 : DecidableEq m] [inst_2 : DecidableEq n]
  [inst_3 : Fintype m] [inst_4 : Fintype n] (e : n ≃ m) (M : Matrix n n R),
  ((Matrix.reindex e e) M).charpoly = M.charpoly
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
/-- The coercion into the ring as a `AddMonoidHom`  -/
TwoSidedIdeal.coeAddMonoidHom : {R : Type u_1} → [inst : NonUnitalNonAssocRing R] → (I : TwoSidedIdeal R) → ↥I →+ R
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.SheafedSpace.GlueData.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (toGlueData : CategoryTheory.GlueData (AlgebraicGeometry.SheafedSpace C)) →
      (∀ (i j : toGlueData.J), AlgebraicGeometry.SheafedSpace.IsOpenImmersion (toGlueData.f i j)) →
        AlgebraicGeometry.SheafedSpace.GlueData C
-- Mathlib.Probability.Distributions.Uniform
MeasureTheory.pdf.IsUniform.hasPDF : ∀ {E : Type u_1} [inst : MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : Type u_2} {x : MeasurableSpace Ω}
  {ℙ : MeasureTheory.Measure Ω} {X : Ω → E} {s : Set E},
  μ s ≠ 0 → μ s ≠ ⊤ → MeasureTheory.pdf.IsUniform X s ℙ μ → MeasureTheory.HasPDF X ℙ μ
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.toAddSubmonoid_injective : ∀ {G : Type u_1} [inst : AddGroup G], Function.Injective AddSubgroup.toAddSubmonoid
-- Std.Time.Duration
Std.Time.Duration.instHMulInt : HMul ℤ Std.Time.Duration Std.Time.Duration
-- Mathlib.Tactic.Bound.Attribute
/-- Map a score to either `norm apply` or `safe apply <priority>`  -/
Mathlib.Tactic.Bound.scoreToConfig : Lean.Name → ℕ → Aesop.Frontend.RuleConfig
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.Legacy.foldl.match_1.eq_1 : ∀ (motive : Substring.Raw → Sort u_1) (s : String) (b e : String.Pos.Raw)
  (h_1 : (s : String) → (b e : String.Pos.Raw) → motive { str := s, startPos := b, stopPos := e }),
  (match { str := s, startPos := b, stopPos := e } with
    | { str := s, startPos := b, stopPos := e } => h_1 s b e) =
    h_1 s b e
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- Let `C(G, A)` denote the complex of inhomogeneous chains of `A : Rep k G`. This lemma
says `d₃₂` gives a simpler expression for the 2nd differential: that is, the following
square commutes:
```
   C₃(G, A) --d 3 2--> C₂(G, A)
    |                    |
    |                    |
    |                    |
    v                    v
  (G³ →₀ A) --d₃₂--> (G² →₀ A)
```
where the vertical arrows are `chainsIso₃` and `chainsIso₂` respectively.
 -/
groupHomology.comp_d₃₂_eq : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₃ A).hom (groupHomology.d₃₂ A) =
    CategoryTheory.CategoryStruct.comp ((groupHomology.inhomogeneousChains A).d 3 2) (groupHomology.chainsIso₂ A).hom
-- Mathlib.CategoryTheory.Quotient
/-- In order to define a natural isomorphism `F ≅ G` with `F G : Quotient r ⥤ D`, it suffices
to do so after precomposing with `Quotient.functor r`.  -/
CategoryTheory.Quotient.natIsoLift : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (r : HomRel C) →
      {D : Type u_2} →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          {F G : CategoryTheory.Functor (CategoryTheory.Quotient r) D} →
            ((CategoryTheory.Quotient.functor r).comp F ≅ (CategoryTheory.Quotient.functor r).comp G) → (F ≅ G)
-- Mathlib.Data.Vector.Basic
List.Vector.exists_eq_cons : ∀ {α : Type u_1} {n : ℕ} (v : List.Vector α n.succ), ∃ a as, v = a ::ᵥ as
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.instIsScalarTower : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)], IsScalarTower R R (PiTensorProduct R fun i => s i)
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.instFullFunctorOppositeTypeShrinkYoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C],
  CategoryTheory.shrinkYoneda.{w, v, u}.Full
-- Mathlib.Topology.Algebra.ConstMulAction
Homeomorph.smul_apply : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [inst_3 : ContinuousConstSMul G α] (γ : G) (x : α), (Homeomorph.smul γ) x = γ • x
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
isTheta_deriv_rpow_const_atTop : ∀ {p : ℝ}, p ≠ 0 → (deriv fun x => x ^ p) =Θ[Filter.atTop] fun x => x ^ (p - 1)
-- Mathlib.Data.Set.Basic
Set.Subset.antisymm_iff : ∀ {α : Type u} {a b : Set α}, a = b ↔ a ⊆ b ∧ b ⊆ a
-- Mathlib.Data.Int.Bitwise
Int.lor_bit : ∀ (a : Bool) (m : ℤ) (b : Bool) (n : ℤ), (Int.bit a m).lor (Int.bit b n) = Int.bit (a || b) (m.lor n)
-- Mathlib.Algebra.Group.Even
/-- **Alias** of the forward direction of `isSquare_iff_exists_mul_self`. -/
IsSquare.exists_mul_self : ∀ {α : Type u_2} [inst : Mul α] (a : α), IsSquare a → ∃ r, a = r * r
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.pairing_II : ∀ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore), h.pairing.II = h.II
-- Mathlib.Algebra.CharP.Defs
CharP.false_of_nontrivial_of_char_one : ∀ {R : Type u_1} [inst : NonAssocSemiring R] [Nontrivial R] [CharP R 1], False
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {l : List ((a : α) × β a)} {k k' : α},
  compare k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬compare a.fst b.fst = Ordering.eq) l →
      k ∈ List.map Sigma.fst l →
        ∀ {h' : Std.DTreeMap.Internal.Impl.contains k' ↑(t.insertMany l ⋯) = true},
          (↑(t.insertMany l ⋯)).getKey k' h' = k
-- Mathlib.Analysis.Calculus.VectorField
Filter.EventuallyEq.lieBracketWithin_vectorField : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W V₁ W₁ : E → E} {s : Set E} {x : E},
  V₁ =ᶠ[nhdsWithin x s] V →
    W₁ =ᶠ[nhdsWithin x s] W →
      VectorField.lieBracketWithin 𝕜 V₁ W₁ s =ᶠ[nhdsWithin x s] VectorField.lieBracketWithin 𝕜 V W s
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.preimage_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X : C} [inst_2 : F.Full] [F.Faithful],
  F.preimage (CategoryTheory.CategoryStruct.id (F.obj X)) = CategoryTheory.CategoryStruct.id X
-- Mathlib.SetTheory.Ordinal.Notation
ONote.ofNat.eq_1 : ↑0 = 0