mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- Extract the cocone from a binary bicone.  -/
CategoryTheory.Limits.BinaryBicone.toCocone : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} → CategoryTheory.Limits.BinaryBicone P Q → CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair P Q)
-- Mathlib.RingTheory.Polynomial.Basic
MvPolynomial.isEmptyAlgEquiv.congr_simp : ∀ (R : Type u) (σ : Type u_1) [inst : CommSemiring R] [inst_1 : IsEmpty σ],
  MvPolynomial.isEmptyAlgEquiv R σ = MvPolynomial.isEmptyAlgEquiv R σ
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.PInfty_toNondegComplex : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C],
  CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty s.toNondegComplex = s.toNondegComplex
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.Const.insertManyIfNewUnit_eq : ∀ {α : Type u} {ρ : Type w} [inst : ForIn Id ρ α] [inst_1 : BEq α] [inst_2 : Hashable α]
  {m : Std.DHashMap.Raw α fun x => Unit} {l : ρ} (h : m.WF),
  Std.DHashMap.Raw.Const.insertManyIfNewUnit m l = ↑↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit ⟨m, ⋯⟩ l)
-- Init.Data.Float.Model.Float
/-- Converts an `Int8` to a `Float.Model`, returning positive zero on zero.  -/
Float.Model.ofInt8 : Int8 → Float.Model
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_mul_Iic : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (fun x => a * x) ⁻¹' Set.Iic b = Set.Iic (b / a)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.rightHomologyι_naturality'_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) {Z : C}
  (h : h₂.Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂)
      (CategoryTheory.CategoryStruct.comp h₂.ι h) =
    CategoryTheory.CategoryStruct.comp h₁.ι
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂) h)
-- Mathlib.LinearAlgebra.RootSystem.RootPairingCat
RootPairingCat.coweightIsAddCommGroup : {R : Type u} → [inst : CommRing R] → (self : RootPairingCat R) → AddCommGroup self.coweight
-- Mathlib.Combinatorics.SetFamily.LYM
Finset.falling.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] (k : ℕ) (𝒜 : Finset (Finset α)),
  Finset.falling k 𝒜 = 𝒜.sup (Finset.powersetCard k)
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.hasGaussianLaw_iff_charFunDual_map_eq : ∀ {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : MeasurableSpace E] [BorelSpace E] {X : Ω → E} [inst_3 : NormedSpace ℝ E] [MeasureTheory.IsFiniteMeasure P],
  AEMeasurable X P →
    (ProbabilityTheory.HasGaussianLaw X P ↔
      ∀ (L : StrongDual ℝ E),
        MeasureTheory.charFunDual (MeasureTheory.Measure.map X P) L =
          Complex.exp (↑(∫ (x : Ω), (⇑L ∘ X) x ∂P) * Complex.I - ↑(ProbabilityTheory.variance (⇑L ∘ X) P) / 2))
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.eventually_filterAt_iff : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  (v : VitaliFamily μ) {x : X} {P : Set X → Prop},
  (∀ᶠ (t : Set X) in v.filterAt x, P t) ↔ ∃ ε > 0, ∀ t ∈ v.setsAt x, t ⊆ Metric.closedBall x ε → P t
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.foldRevM_eq_foldrM_keys : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {δ : Type w} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : δ → α → m' δ} {init : δ},
  Std.DHashMap.Raw.Internal.foldRevM (fun d a x => f d a) init ↑m = List.foldrM (fun a b => f b a) init (↑m).keys
-- Mathlib.Data.List.Chain
List.isChain_cons_eq_iff_eq_replicate : ∀ {α : Type u_1} {a : α} {l : List α}, List.IsChain (fun x1 x2 => x1 = x2) (a :: l) ↔ l = List.replicate l.length a
-- Mathlib.Order.SupIndep
iSupIndep_iff_pairwiseDisjoint : ∀ {α : Type u_1} {ι : Type u_3} [inst : Order.Frame α] {f : ι → α}, iSupIndep f ↔ Pairwise (Function.onFun Disjoint f)
-- Mathlib.MeasureTheory.Covering.Vitali
/-- Vitali covering theorem, closed balls version: given a family `t` of closed balls, one can
extract a disjoint subfamily `u ⊆ t` so that all balls in `t` are covered by the τ-times
dilations of balls in `u`, for some `τ > 3`.  -/
Vitali.exists_disjoint_subfamily_covering_enlargement_closedBall : ∀ {α : Type u_1} {ι : Type u_2} [inst : PseudoMetricSpace α] (t : Set ι) (x : ι → α) (r : ι → ℝ) (R : ℝ),
  (∀ a ∈ t, r a ≤ R) →
    ∀ (τ : ℝ),
      3 < τ →
        ∃ u ⊆ t,
          (u.PairwiseDisjoint fun a => Metric.closedBall (x a) (r a)) ∧
            ∀ a ∈ t, ∃ b ∈ u, Metric.closedBall (x a) (r a) ⊆ Metric.closedBall (x b) (τ * r b)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.foldr_eq_foldr_keysArray : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {δ : Type w} {f : α → δ → δ} {init : δ},
  Std.DTreeMap.Internal.Impl.foldr (fun a x d => f a d) init t = Array.foldr f init t.keysArray
-- Mathlib.MeasureTheory.Measure.Comap
MeasureTheory.Measure.measure_image_eq_zero_of_comap_eq_zero : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α → β)
  (μ : MeasureTheory.Measure β),
  Function.Injective f →
    (∀ (s : Set α), MeasurableSet s → MeasureTheory.NullMeasurableSet (f '' s) μ) →
      ∀ {s : Set α}, (MeasureTheory.Measure.comap f μ) s = 0 → μ (f '' s) = 0
-- Mathlib.RingTheory.IsTensorProduct
/-- If `B = S ⊗[R] A`, this is the canonical `S`-isomorphism: `B ⊗[A] M ≃ₗ[S] S ⊗[R] M`.
This is the cancelling on the left version of
`TensorProduct.AlgebraTensorModule.cancelBaseChange`.  -/
Algebra.IsPushout.cancelBaseChange : (R : Type u_1) →
  (S : Type v₃) →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          (A : Type u_8) →
            (B : Type u_9) →
              [inst_3 : CommRing A] →
                [inst_4 : CommRing B] →
                  [inst_5 : Algebra R A] →
                    [inst_6 : Algebra R B] →
                      [inst_7 : Algebra A B] →
                        [inst_8 : Algebra S B] →
                          [inst_9 : IsScalarTower R A B] →
                            [inst_10 : IsScalarTower R S B] →
                              [Algebra.IsPushout R S A B] →
                                (M : Type u_10) →
                                  [inst_12 : AddCommGroup M] →
                                    [inst_13 : Module R M] →
                                      [inst_14 : Module A M] →
                                        [IsScalarTower R A M] → TensorProduct A B M ≃ₗ[S] TensorProduct R S M
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- **Alias** of `CategoryTheory.Mod.mod`. -/
CategoryTheory.Mod_.mod : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            {A : C} →
              [inst_4 : CategoryTheory.MonObj A] → (self : CategoryTheory.Mod D A) → CategoryTheory.ModObj A self.X
-- Mathlib.Data.Prod.Basic
Prod.lex_iff : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {x y : α × β},
  Prod.Lex r s x y ↔ r x.1 y.1 ∨ x.1 = y.1 ∧ s x.2 y.2
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.Hom.mk : {M N : SemiNormedGrp} → NormedAddGroupHom M.carrier N.carrier → M.Hom N
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- Sections of the structure sheaf of Spec R on a basic open as localization of R  -/
AlgebraicGeometry.StructureSheaf.IsLocalization.to_basicOpen : ∀ (R : Type u) [inst : CommRing R] (r : R),
  IsLocalization.Away r ↑((AlgebraicGeometry.Spec.structureSheaf R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen r)))
-- Mathlib.Topology.MetricSpace.PiNat
Metric.PiNatEmbed.continuous_distDenseSeq_inv : ∀ {X : Type u_3} [inst : MetricSpace X] [inst_1 : TopologicalSpace.SeparableSpace X],
  Continuous Metric.PiNatEmbed.ofPiNat
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
/-- `ContDiffBump` is `𝒞ⁿ` in all its arguments.  -/
ContDiffAt.contDiffBump : ∀ {E : Type u_1} {X : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup X]
  [inst_3 : NormedSpace ℝ X] [inst_4 : HasContDiffBump E] {n : ℕ∞} {c g : X → E} {f : (x : X) → ContDiffBump (c x)}
  {x : X},
  ContDiffAt ℝ (↑n) c x →
    ContDiffAt ℝ (↑n) (fun x => (f x).rIn) x →
      ContDiffAt ℝ (↑n) (fun x => (f x).rOut) x → ContDiffAt ℝ (↑n) g x → ContDiffAt ℝ (↑n) (fun x => ↑(f x) (g x)) x
-- Mathlib.Topology.Sequences
/-- The sequential closure of a set is contained in the closure of that set.
The converse is not true.  -/
seqClosure_subset_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, seqClosure s ⊆ closure s
-- Std.Http.Server.Connection
/-- Dispatches a pending request head to the handler if one is waiting.
Spawns the handler as an async task and routes its result back through `state.response`.
Returns the updated state with `pendingHead` cleared and `handlerDispatched` set.
 -/
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.dispatchPendingRequest : {σ : Type} →
  [inst : Std.Http.Server.Handler σ] →
    σ →
      Std.Http.Extensions →
        Std.CancellationContext →
          Std.Http.Server.Connection.ConnectionState✝ (Std.Http.Server.Handler.ResponseBody σ) →
            Std.Async.Async (Std.Http.Server.Connection.ConnectionState✝ (Std.Http.Server.Handler.ResponseBody σ))
-- Mathlib.GroupTheory.Congruence.Hom
/-- The diagram describing the universal property for quotients of monoids commutes.  -/
Con.lift_comp_mk' : ∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] {c : Con M} {f : M →* P}
  (H : c ≤ Con.ker f), (c.lift f H).comp c.mk' = f
-- Mathlib.Algebra.GroupWithZero.Range
/-- For a morphism of monoids with zero `f`, this is a smallest subgroup with zero of the
codomain containing the range of `f`.  -/
MonoidWithZeroHom.ValueGroup₀ : {A : Type u_1} → {B : Type u_2} → [inst : MonoidWithZero A] → [inst_1 : MonoidWithZero B] → (A →*₀ B) → Type u_2
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- **Alias** of the forward direction of `hasDerivWithinAt_iff_hasFDerivWithinAt`.

---

Expressing `HasDerivWithinAt f f' s x` in terms of `HasFDerivWithinAt`  -/
HasDerivWithinAt.hasFDerivWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} [inst_4 : ContinuousSMul 𝕜 F] {f' : F},
  HasDerivWithinAt f f' s x → HasFDerivWithinAt f (ContinuousLinearMap.toSpanSingleton 𝕜 f') s x
-- Std.Data.DHashMap.Raw
/-- Retrieves the key from the mapping that matches `a`. Ensures that such a mapping exists by
requiring a proof of `a ∈ m`. The result is guaranteed to be pointer equal to the key in the map.
 -/
Std.DHashMap.Raw.getKey : {α : Type u} →
  {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → (m : Std.DHashMap.Raw α β) → (a : α) → a ∈ m → α
-- Init.Data.Iterators.Consumers.Monadic.Collect
Std.IterM.toListRev.go : {α : Type w} →
  {m : Type w → Type w'} → [Monad m] → {β : Type w} → [Std.Iterator α m β] → Std.IterM m β → List β → m (List β)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_mem_of_nonempty : ∀ {α : Type u_2} {ι : Type u_5} [inst : LinearOrder α] [inst_1 : OrderTop α] {s : Finset ι} {f : ι → α},
  s.Nonempty → s.inf f ∈ f '' ↑s
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.ordered_containsThenInsertIfNew! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {k : α} {v : β k} {l : Std.DTreeMap.Internal.Impl α β},
  l.Balanced → l.Ordered → (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew! k v l).2.Ordered
-- Batteries.Data.List.Lemmas
List.cons_diff_of_not_mem : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l₂ : List α},
  a ∉ l₂ → ∀ (l₁ : List α), (a :: l₁).diff l₂ = a :: l₁.diff l₂
-- Mathlib.CategoryTheory.Monad.Coequalizer
/-- The top map in the coequalizer diagram we will construct.  -/
CategoryTheory.Monad.FreeCoequalizer.topMap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} → (X : T.Algebra) → T.free.obj (T.obj X.A) ⟶ T.free.obj X.A
-- Mathlib.Algebra.Algebra.Rat
RingEquivClass.toLinearEquivClassRat : ∀ {F : Type u_1} {R : Type u_2} {S : Type u_3} [inst : DivisionRing R] [inst_1 : CharZero R] [inst_2 : DivisionRing S]
  [inst_3 : CharZero S] [inst_4 : EquivLike F R S] [RingEquivClass F R S], LinearEquivClass F ℚ R S
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.under_eq_inverseImage : ∀ {T : Type u_3} [inst : CategoryTheory.Category.{v_3, u_3} T] (W : CategoryTheory.MorphismProperty T) (X : T),
  W.under = W.inverseImage (CategoryTheory.Under.forget X)
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_congr' : ∀ {M : Type u_2} [inst : CommMonoid M] {a b : ℕ} (f : Fin b → M) (h : a = b), ∏ i, f (Fin.cast h i) = ∏ i, f i
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
/-- If a function is differentiable inside a convex set with nonempty interior, and has a second
derivative at a point of this convex set, then this second derivative is symmetric.  -/
Convex.second_derivative_within_at_symmetric : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {s : Set E},
  Convex ℝ s →
    (interior s).Nonempty →
      ∀ {f : E → F} {f' : E → E →L[ℝ] F} {f'' : E →L[ℝ] E →L[ℝ] F},
        (∀ x ∈ interior s, HasFDerivAt f (f' x) x) →
          ∀ {x : E}, x ∈ s → HasFDerivWithinAt f' f'' (interior s) x → ∀ (v w : E), (f'' v) w = (f'' w) v
-- Std.Http.Protocol.H1.Parser
/-- Parses a request line and returns a fully-typed `Request.Head`.
`request-line = method SP request-target SP HTTP-version`
 -/
Std.Http.Protocol.H1.parseRequestLine : Std.Http.Protocol.H1.Config → Std.Internal.Parsec.ByteArray.Parser Std.Http.Request.Head
-- Mathlib.Data.Subtype
Subtype.coind_coe : ∀ {α : Sort u_4} {β : Sort u_5} (f : α → β) {p : β → Prop} (h : ∀ (a : α), p (f a)) (a : α),
  ↑(Subtype.coind f h a) = f a
-- Std.Time.Date.Unit.Day
/-- Convert `Day.Offset` into `Minute.Offset`.
 -/
Std.Time.Day.Offset.toMinutes : Std.Time.Day.Offset → Std.Time.Minute.Offset
-- Mathlib.Computability.TuringMachine.Tape
/-- The `i`-th projection as a pointed map.  -/
Turing.proj : {ι : Type u_1} →
  {Γ : ι → Type u_2} → [inst : (i : ι) → Inhabited (Γ i)] → (i : ι) → Turing.PointedMap ((i : ι) → Γ i) (Γ i)
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeAddGroupBasis.instFunLike.eq_1 : ∀ {ι : Type u_1} {G : Type u_3} [inst : AddGroup G],
  FreeAddGroupBasis.instFunLike = { coe := fun b i => b.repr.symm (FreeAddGroup.of i), coe_injective := ⋯ }
-- Mathlib.Control.Bitraversable.Instances
Prod.bitraverse.eq_1 : ∀ {F : Type u → Type u} [inst : Applicative F] {α : Type u_1} {α' : Type u} {β : Type u_2} {β' : Type u} (f : α → F α')
  (f' : β → F β') (x_1 : α) (y : β), Prod.bitraverse f f' (x_1, y) = Prod.mk <$> f x_1 <*> f' y
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.kernelOpOp_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (f : X ⟶ Y),
  (CategoryTheory.kernelOpOp f).inv = CategoryTheory.Limits.kernel.lift f.op (CategoryTheory.Limits.cokernel.π f).op ⋯
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toArray_rcc_eq_some : ∀ {m n i : ℕ}, i < n + 1 - m → (m...=n).toArray[i]? = some (m + i)
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.Arrow.augmentedCechConerve_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C)
  [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom],
  f.augmentedCechConerve.right = f.cechConerve
-- Std.Http.Internal.Char
/-- Checks if a byte is a sub-delimiter character according to RFC 3986.
Sub-delimiters are: `!`, `$`, `&`, `'`, `(`, `)`, `*`, `+`, `,`, `;`, `=`.
 -/
Std.Http.Internal.Char.isSubDelims : UInt8 → Bool
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.leftUnitor_inv_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f : X ⟶ Y) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) f) h)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.eq_d₂₃_comp_inv_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : ModuleCat.of k ((Fin 3 → G) → ↑A) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₂ A).inv
      (CategoryTheory.CategoryStruct.comp
        (CochainComplex.of.d (fun n => ModuleCat.of k ((Fin n → G) → ↑A)) (fun n => inhomogeneousCochains.d A n) 2 3)
        h) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.d₂₃ A)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₃ A).inv h)
-- Mathlib.Order.IsNormal
Order.IsNormal.map_iSup : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : ConditionallyCompleteLinearOrder α]
  [inst_1 : ConditionallyCompleteLinearOrder β] {ι : Sort u_4} [Nonempty ι] {g : ι → α},
  Order.IsNormal f → BddAbove (Set.range g) → f (⨆ i, g i) = ⨆ i, f (g i)
-- Lean.Elab.Do.Basic
/-- Refine the result type of the `do` block and its `return` continuation for the scope of `k`,
as needed for a dependent `match` branch where a bare `return` targets the refined branch type.

Relies on the `return` continuation result type coinciding with the `do` block result type, which
holds for the tail-position dependent `match` this serves.
 -/
Lean.Elab.Do.withRefinedResultType : {α : Type} → Lean.Expr → Lean.Elab.Do.DoElabM α → Lean.Elab.Do.DoElabM α
-- Lean.Meta.LazyDiscrTree
/-- This is a hook to determine if we should add an expression as a wildcard pattern.

Clone of `Lean.Meta.DiscrTree.shouldAddAsStar`.  See it for more discussion.
 -/
Lean.Meta.LazyDiscrTree.MatchClone.shouldAddAsStar : Lean.Name → Lean.Expr → Lean.MetaM Bool
-- Init.Data.Format.Basic
Std.Format.defUnicode : Bool
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPolynomial.coe_def : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (φ : MvPolynomial σ R), ↑φ = fun n => MvPolynomial.coeff n φ
-- Mathlib.Computability.AkraBazzi.AkraBazzi
/-- The **Akra-Bazzi theorem**: `T ∈ O(n^p (1 + ∑_u^n g(u) / u^{p+1}))`  -/
AkraBazziRecurrence.isBigO_asympBound : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r), T =O[Filter.atTop] AkraBazziRecurrence.asympBound g a b
-- Mathlib.Algebra.Group.Basic
one_div_pow : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a : α) (n : ℕ), (1 / a) ^ n = 1 / a ^ n
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.polar_sub_right : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticMap R M N) (x y y' : M),
  QuadraticMap.polar (⇑Q) x (y - y') = QuadraticMap.polar (⇑Q) x y - QuadraticMap.polar (⇑Q) x y'
-- Mathlib.LinearAlgebra.Prod
LinearEquiv.uniqueProd_symm_apply : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] [inst_5 : Unique M₂] (a : M),
  LinearEquiv.uniqueProd.symm a = (default, a)
-- Mathlib.Algebra.Order.Module.Defs
isOrderedModule_iff_smul_one_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β] [inst_3 : Preorder α]
  [inst_4 : Preorder β] [inst_5 : MulOneClass β] [ZeroLEOneClass β] [PosMulMono β] [MulPosMono β] [IsScalarTower α β β],
  IsOrderedModule α β ↔ Monotone fun x => x • 1
-- Init.Prelude
/-- The modulo operator, which computes the remainder when dividing one natural number by another.
Usually accessed via the `%` operator. When the divisor is `0`, the result is the dividend rather
than an error.

This is the core implementation of `Nat.mod`. It computes the correct result for any two closed
natural numbers, but it does not have some convenient [definitional
reductions](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=type-system) when the `Nat`s contain free variables. The wrapper
`Nat.mod` handles those cases specially and then calls `Nat.modCore`.

This function is overridden at runtime with an efficient implementation. This definition is the
logical model.
 -/
Nat.modCore : ℕ → ℕ → ℕ
-- Init.Data.Int.DivMod.Lemmas
Int.eq_mul_of_fdiv_eq_left : ∀ {a b c : ℤ}, b ∣ a → a.fdiv b = c → a = c * b
-- Mathlib.Topology.Category.LightProfinite.Basic
LightProfinite.instHasPropAndTotallyDisconnectedSpaceCarrierSecondCountableTopology : ∀ (X : Type u_1) [inst : TopologicalSpace X] [TotallyDisconnectedSpace X] [SecondCountableTopology X],
  CompHausLike.HasProp (fun Y => TotallyDisconnectedSpace ↑Y ∧ SecondCountableTopology ↑Y) X
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedAddSubgroup.toAddSubgroup : {G : Type u} → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → ClosedAddSubgroup G → AddSubgroup G
-- Mathlib.Data.PFun
PFun.image_mono : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β) {s t : Set α}, s ⊆ t → f.image s ⊆ f.image t
-- Mathlib.Algebra.NoZeroSMulDivisors.Defs
noZeroSMulDivisors_iff : ∀ (R : Type u_4) (M : Type u_5) [inst : Zero R] [inst_1 : Zero M] [inst_2 : SMul R M],
  NoZeroSMulDivisors R M ↔ ∀ {c : R} {x : M}, c • x = 0 → c = 0 ∨ x = 0
-- Mathlib.Tactic.DefEqAbuse
_private.Mathlib.Tactic.DefEqAbuse.0.Lean.MessageData.VisitStep.descend.sizeOf_spec : ∀ {α : Type u_1} [inst : SizeOf α] (butFirst : optParam (Option α) none),
  sizeOf (Lean.MessageData.VisitStep.descend✝ butFirst) = 1 + sizeOf butFirst
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueD_filter_not_contains_map_fst_of_containsKey_eq_false_right : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α} {fallback : β},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₂ = false →
      Std.Internal.List.getValueD k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) fallback =
        Std.Internal.List.getValueD k l₁ fallback
-- Mathlib.Topology.Separation.Basic
eventually_nhdsNE_eventually_nhds_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {a : X} {p : X → Prop},
  (∀ᶠ (y : X) in nhdsWithin a {a}ᶜ, ∀ᶠ (x : X) in nhds y, p x) ↔ ∀ᶠ (x : X) in nhdsWithin a {a}ᶜ, p x