mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- If `𝔖` and `𝔗` are families of sets in `α`, then the identity map
`(α →ᵤ[𝔗] β) → (α →ᵤ[𝔖] β)` is uniformly continuous if every `s ∈ 𝔖` is contained in a finite
union of elements of `𝔗`.

With more API around `Order.Ideal`, this could be phrased in that language instead.  -/
UniformOnFun.uniformContinuous_ofFun_toFun : ∀ {α : Type u_1} (β : Type u_2) [inst : UniformSpace β] (𝔖 𝔗 : Set (Set α)),
  (∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T) → UniformContinuous (⇑(UniformOnFun.ofFun 𝔗) ∘ ⇑(UniformOnFun.toFun 𝔖))
-- Mathlib.Algebra.Group.Submonoid.Defs
SubmonoidClass.subtype_apply : ∀ {M : Type u_1} {A : Type u_3} [inst : MulOneClass M] [inst_1 : SetLike A M] [hA : SubmonoidClass A M] {S' : A}
  (x : ↥S'), (SubmonoidClass.subtype S') x = ↑x
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithTerminal.liftFromOver_map_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {X_1 Y : CategoryTheory.Functor J (CategoryTheory.Over X)} (f : X_1 ⟶ Y) (x : CategoryTheory.WithTerminal J),
  (CategoryTheory.WithTerminal.liftFromOver.map f).app x =
    match x with
    | CategoryTheory.WithTerminal.of x => CategoryTheory.Over.Hom.left (f.app x)
    | CategoryTheory.WithTerminal.star => CategoryTheory.CategoryStruct.id X
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.toComplex_re_div : ∀ (x y : GaussianInt),
  (GaussianInt.toComplex (x / y)).re = ↑(round (GaussianInt.toComplex x / GaussianInt.toComplex y).re)
-- Mathlib.Topology.UnitInterval
/-- The unit interval `[0,1]` in ℝ.  -/
unitInterval.termI : Lean.ParserDescr
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.decEq : {w : ℕ} → DecidableEq (Std.Tactic.BVDecide.BVExpr w)
-- Lean.Meta.Eqns
/-- A mapping from equational theorem to the declaration it was derived from.   -/
Lean.Meta.eqnsExt : Lean.EnvExtension Lean.Meta.EqnsExtState
-- Mathlib.RingTheory.HopfAlgebra.Convolution
HopfAlgebra.toLinearMap_antipodeAlgHom : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : HopfAlgebra R A],
  (HopfAlgebra.antipodeAlgHom R A).toLinearMap = HopfAlgebraStruct.antipode R
-- Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
/-- `CochainComplex.singleFunctor` commutes with `F` and `F.mapHomologicalComplex`.  -/
CategoryTheory.Functor.mapCochainComplexSingleFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        {D : Type u'} →
          [inst_3 : CategoryTheory.Category.{v', u'} D] →
            [inst_4 : CategoryTheory.Abelian D] →
              (F : CategoryTheory.Functor C D) →
                [inst_5 : F.Additive] →
                  (n : ℤ) →
                    (CochainComplex.singleFunctor C n).comp (F.mapHomologicalComplex (ComplexShape.up ℤ)) ≅
                      F.comp (CochainComplex.singleFunctor D n)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.preEquivalence_counitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G),
  (CategoryTheory.StructuredArrow.preEquivalence F f).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun x =>
        CategoryTheory.StructuredArrow.isoMk
          (CategoryTheory.Iso.refl
            (((CategoryTheory.StructuredArrow.preEquivalenceInverse F f).comp
                    (CategoryTheory.StructuredArrow.preEquivalenceFunctor F f)).obj
                x).right)
          ⋯)
      ⋯
-- Mathlib.Data.FinEnum
FinEnum.equiv_down : ∀ {α : Type u} [inst : FinEnum α] (a' : ULift.{u_1, u} α), FinEnum.equiv a'.down = FinEnum.equiv a'
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.sub_mul_div_right : ∀ {R : Type u} [inst : EuclideanDomain R] (x y z : R), y ≠ 0 → y ∣ x → (x - z * y) / y = x / y - z
-- Mathlib.Analysis.Analytic.Constructions
/-- The Cartesian product of analytic functions within a set is analytic.  -/
AnalyticOn.prod : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {g : E → G} {s : Set E},
  AnalyticOn 𝕜 f s → AnalyticOn 𝕜 g s → AnalyticOn 𝕜 (fun x => (f x, g x)) s
-- Mathlib.Algebra.Order.Module.Field
Mathlib.Meta.Positivity.smul_nonneg_of_pos_of_pos : ∀ {α : Type u_3} {β : Type u_4} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulZeroClass α β] [inst_3 : Preorder α]
  [inst_4 : Preorder β] [PosSMulMono α β] {a : α} {b : β}, 0 < a → 0 < b → 0 ≤ a • b
-- Init.Data.Int.DivMod.Lemmas
Int.eq_mul_of_tdiv_eq_right : ∀ {a b c : ℤ}, b ∣ a → a.tdiv b = c → a = b * c
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
/-- If `h : Homotopy φ₁ φ₂` and `n : ℤ`, this is the induced homotopy
between `φ₁⟦n⟧'` and `φ₂⟦n⟧'`.  -/
Homotopy.shift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        {φ₁ φ₂ : K ⟶ L} →
          Homotopy φ₁ φ₂ →
            (n : ℤ) →
              Homotopy ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map φ₁)
                ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map φ₂)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.AbsolutelyContinuous.refl : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  (v : MeasureTheory.VectorMeasure α M), v.AbsolutelyContinuous v
-- Mathlib.LinearAlgebra.Basis.Cardinality
/-- Over any nontrivial ring, the existence of a finite spanning set implies that any basis is finite.
 -/
basis_finite_of_finite_spans : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R]
  {s : Set M}, s.Finite → Submodule.span R s = ⊤ → ∀ {ι : Type w} (b : Module.Basis ι R M), Finite ι
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.image_closure : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : Set M₁), ⇑e '' closure s = closure (⇑e '' s)
-- Mathlib.Condensed.Basic
Condensed.hom_ext_iff : ∀ {C : Type w} [inst : CategoryTheory.Category.{v, w} C] {X Y : Condensed C} {f g : X ⟶ Y},
  f = g ↔ ∀ (S : CompHausᵒᵖ), f.hom.app S = g.hom.app S
-- Mathlib.CategoryTheory.Limits.Types.Filtered
CategoryTheory.Limits.Types.FilteredColimit.rel_equiv : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u))
  [CategoryTheory.IsFilteredOrEmpty J], Equivalence (CategoryTheory.Limits.Types.FilteredColimit.Rel F)
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
HasFibers.instIsEquivalenceFibFiberInducedFunctor : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) [inst_2 : HasFibers p] (S : 𝒮), (HasFibers.inducedFunctor p S).IsEquivalence
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.mem_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  {f : α → β → Bool} {k : α},
  t.WF →
    (k ∈ Std.DTreeMap.Raw.filter f t ↔ ∃ (h' : k ∈ t), f (t.getKey k h') (Std.DTreeMap.Raw.Const.get t k h') = true)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstr.strict : Lean.Meta.Grind.Arith.Linear.IneqCnstr → Bool
-- Mathlib.Topology.VectorBundle.Hom
/-- Given trivializations `e₁`, `e₂` in the atlas for vector bundles `E₁`, `E₂` over a base `B`,
the induced trivialization for the continuous `σ`-semilinear maps from `E₁` to `E₂`,
whose base set is `e₁.baseSet ∩ e₂.baseSet`.  -/
Bundle.Trivialization.continuousLinearMap : {𝕜₁ : Type u_1} →
  [inst : NontriviallyNormedField 𝕜₁] →
    {𝕜₂ : Type u_2} →
      [inst_1 : NontriviallyNormedField 𝕜₂] →
        (σ : 𝕜₁ →+* 𝕜₂) →
          {B : Type u_3} →
            {F₁ : Type u_4} →
              [inst_2 : NormedAddCommGroup F₁] →
                [inst_3 : NormedSpace 𝕜₁ F₁] →
                  {E₁ : B → Type u_5} →
                    [inst_4 : (x : B) → AddCommGroup (E₁ x)] →
                      [inst_5 : (x : B) → Module 𝕜₁ (E₁ x)] →
                        [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] →
                          {F₂ : Type u_6} →
                            [inst_7 : NormedAddCommGroup F₂] →
                              [inst_8 : NormedSpace 𝕜₂ F₂] →
                                {E₂ : B → Type u_7} →
                                  [inst_9 : (x : B) → AddCommGroup (E₂ x)] →
                                    [inst_10 : (x : B) → Module 𝕜₂ (E₂ x)] →
                                      [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] →
                                        [inst_12 : TopologicalSpace B] →
                                          (e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj) →
                                            (e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj) →
                                              [inst_13 : (x : B) → TopologicalSpace (E₁ x)] →
                                                [inst_14 : FiberBundle F₁ E₁] →
                                                  [inst_15 : VectorBundle 𝕜₁ F₁ E₁] →
                                                    [inst_16 : (x : B) → TopologicalSpace (E₂ x)] →
                                                      [inst_17 : FiberBundle F₂ E₂] →
                                                        [inst_18 : VectorBundle 𝕜₂ F₂ E₂] →
                                                          [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)] →
                                                            [inst_20 : ∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] →
                                                              [inst_21 : RingHomIsometric σ] →
                                                                [he₁ : MemTrivializationAtlas e₁] →
                                                                  [he₂ : MemTrivializationAtlas e₂] →
                                                                    Bundle.Trivialization (F₁ →SL[σ] F₂)
                                                                      Bundle.TotalSpace.proj
-- Mathlib.Order.Filter.Extr
IsExtrOn.elim : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α} {p : Prop},
  IsExtrOn f s a → (IsMinOn f s a → p) → (IsMaxOn f s a → p) → p
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.equivOfEq_trans : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S T U : Subalgebra R A) (hST : S = T) (hTU : T = U), (S.equivOfEq T hST).trans (T.equivOfEq U hTU) = S.equivOfEq U ⋯
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.fundSystem_mk : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (i : Fin (NumberField.Units.rank K)),
  Additive.ofMul ↑(NumberField.Units.fundSystem K i) = (NumberField.Units.basisModTorsion K) i
-- Mathlib.CategoryTheory.Comma.Final
CategoryTheory.Comma.isFiltered_of_isFiltered_structuredArrow : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) [CategoryTheory.IsFiltered A] [CategoryTheory.IsFiltered B]
  [∀ (a : A), CategoryTheory.IsFiltered (CategoryTheory.StructuredArrow (L.obj a) R)],
  CategoryTheory.IsFiltered (CategoryTheory.Comma L R)
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.leftInvSeq_nil : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W), cs.leftInvSeq [] = []
-- Lean.Parser.Extension
Lean.Parser.addToken : Lean.Parser.Token → Lean.AttributeKind → Lean.AttrM Unit
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.φ₂.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C),
  S.φ₂ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst S.L₁.g S.v₀₁.τ₃) S.v₁₂.τ₂
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- `Set α` is a `CommMonoid` under pointwise operations if `α` is.  -/
Set.commMonoid : {α : Type u_2} → [CommMonoid α] → CommMonoid (Set α)
-- Mathlib.Order.KrullDimension
Order.coheight_int : ∀ (n : ℤ), Order.coheight n = ⊤
-- Mathlib.NumberTheory.HeckeRing.Defs
/-- The identity double coset `H1H = H` of the diagonal (Hecke pair) case.  -/
HeckeCoset.instOne : {G : Type u_1} → [inst : Group G] → (Δ : Submonoid G) → (H : Subgroup G) → One (HeckeCoset Δ H H)
-- Init.Data.Array.Monadic
Array.foldrM_wfParam : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Array α}
  {f : α → β → m β} {init : β}, Array.foldrM f init (wfParam xs) = Array.foldrM f init xs.attach.unattach
-- Init.Data.List.Basic
List.unzip_eq_unzipTR : @List.unzip = @List.unzipTR
-- Mathlib.CategoryTheory.Limits.Preserves.Grothendieck
CategoryTheory.Limits.fiberwiseColimitLimitIso.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {H : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} H]
  {J : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} J] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  (K : CategoryTheory.Functor J (CategoryTheory.Functor (CategoryTheory.Grothendieck F) H))
  [inst_3 : ∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H]
  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J H]
  [inst_5 : ∀ (c : C), CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim],
  CategoryTheory.Limits.fiberwiseColimitLimitIso K = CategoryTheory.Limits.fiberwiseColimitLimitIso K
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- Linear equivalence between `SkewMonoidAlgebra k G` and `G →₀ k`.  -/
SkewMonoidAlgebra.coeffLinearEquiv : {k : Type u_1} →
  {G : Type u_2} →
    {S : Type u_3} →
      [inst : Semiring S] → [inst_1 : AddCommMonoid k] → [inst_2 : Module S k] → SkewMonoidAlgebra k G ≃ₗ[S] G →₀ k
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.tensorObj.eq_1 : ∀ {R : Type u} [inst : CommSemiring R] (M : SemimoduleCat R) (N : SemimoduleCat R),
  SemimoduleCat.MonoidalCategory.tensorObj M N = SemimoduleCat.of R (TensorProduct R ↑M ↑N)
-- Mathlib.Computability.TuringMachine.Tape
_private.Mathlib.Computability.TuringMachine.Tape.0.Turing.Tape.nth.match_1.eq_1 : ∀ (motive : ℤ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive (Int.ofNat n.succ))
  (h_3 : (n : ℕ) → motive (Int.negSucc n)),
  (match 0 with
    | 0 => h_1 ()
    | Int.ofNat n.succ => h_2 n
    | Int.negSucc n => h_3 n) =
    h_1 ()
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticFinishedSnapshot.mk.inj : ∀ {toSnapshot : Lean.Language.Snapshot} {state? : Option Lean.Elab.Tactic.SavedState}
  {moreSnaps : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)} {toSnapshot_1 : Lean.Language.Snapshot}
  {state?_1 : Option Lean.Elab.Tactic.SavedState}
  {moreSnaps_1 : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)},
  { toSnapshot := toSnapshot, state? := state?, moreSnaps := moreSnaps } =
      { toSnapshot := toSnapshot_1, state? := state?_1, moreSnaps := moreSnaps_1 } →
    toSnapshot = toSnapshot_1 ∧ state? = state?_1 ∧ moreSnaps = moreSnaps_1
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : SupSet α] [inst_1 : SupSet β] {f g : sSupHom α β}, f = g ↔ ∀ (a : α), f a = g a
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.mem_sup_left : ∀ {M : Type u_1} [inst : AddZeroClass M] {S T : AddSubmonoid M} {x : M}, x ∈ S → x ∈ S ⊔ T
-- Mathlib.Analysis.Calculus.Deriv.Polynomial
Polynomial.deriv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} (p : Polynomial 𝕜),
  deriv (fun x => Polynomial.eval x p) x = Polynomial.eval x (Polynomial.derivative p)
-- Mathlib.Data.Set.Image
Set.exists_mem_image : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {p : β → Prop}, (∃ y ∈ f '' s, p y) ↔ ∃ x ∈ s, p (f x)
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxc.Iterator.next : {α : Type u} → Std.Rxc.Iterator α → Option α
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_ord_cof : ∀ (o : Ordinal.{u_1}), o.cof.ord.cof = o.cof
-- Mathlib.Data.ENNReal.Operations
ENNReal.pow_ne_zero : ∀ {a : ENNReal}, a ≠ 0 → ∀ (n : ℕ), a ^ n ≠ 0
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_eq_card_multiples : ∀ {G : Type u_1} [inst : AddLeftCancelMonoid G] [inst_1 : Fintype G] {x : G},
  addOrderOf x = Fintype.card ↥(AddSubmonoid.multiples x)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.eq_d₁₂_comp_inv_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : G → ↑A),
  (CategoryTheory.ConcreteCategory.hom
        (CochainComplex.of.d (fun n => ModuleCat.of k ((Fin n → G) → ↑A)) (fun n => inhomogeneousCochains.d A n) 1 2))
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsIso₁ A).inv) x) =
    (CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsIso₂ A).inv)
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.d₁₂ A)) x)
-- Mathlib.Order.Heyting.Hom
CoheytingHom.coe_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : CoheytingAlgebra α] [inst_1 : CoheytingAlgebra β]
  [inst_2 : CoheytingAlgebra γ] (f : CoheytingHom β γ) (g : CoheytingHom α β), ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.singleton_repr : ∀ (ι : Type u_7) (R : Type u_8) [inst : Unique ι] [inst_1 : Semiring R] (x : R) (i : ι),
  ((Module.Basis.singleton ι R).repr x) i = x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.size_ofList : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {l : List (α × β)},
  List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l → (Std.DTreeMap.Const.ofList l cmp).size = l.length
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate `f ◁ α`  -/
Mathlib.Tactic.BicategoryLike.MkEvalWhiskerLeft.mkEvalWhiskerLeftNil : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MkEvalWhiskerLeft m] →
    Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Structural → m Lean.Expr
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.exp_nsmul : ∀ {M : Type u_4} [inst : AddMonoid M] (n : ℕ) (a : M), WithZero.exp (n • a) = WithZero.exp a ^ n
-- Lean.Compiler.LCNF.Types
/-- Whether the type is a scalar as opposed to a pointer (or a value disguised as a pointer).
 -/
Lean.Compiler.LCNF.ImpureType.Lean.Expr.isScalar : Lean.Expr → Bool
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l → k ∈ List.map Prod.fst l → (t.insertMany l).getKey! k' = k
-- Init.Data.String.Bootstrap
Substring.Raw.Internal.beq : Substring.Raw → Substring.Raw → Bool
-- Mathlib.RingTheory.Idempotents
OrthogonalIdempotents.mul_eq : ∀ {R : Type u_1} [inst : Semiring R] {I : Type u_3} {e : I → R} [inst_1 : DecidableEq I],
  OrthogonalIdempotents e → ∀ (i j : I), e i * e j = if i = j then e i else 0
-- Mathlib.Algebra.Category.MonCat.Colimits
/-- The function from the colimit monoid to the cone point of any other cocone.  -/
MonCat.Colimits.descFun : {J : Type v} →
  [inst : CategoryTheory.Category.{u, v} J] →
    (F : CategoryTheory.Functor J MonCat) → (s : CategoryTheory.Limits.Cocone F) → MonCat.Colimits.ColimitType F → ↑s.pt
-- Init.Data.Vector.Attach
Vector.getElem?_unattach : ∀ {α : Type u_1} {n : ℕ} {p : α → Prop} {xs : Vector { x // p x } n} (i : ℕ),
  xs.unattach[i]? = Option.map Subtype.val xs[i]?
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.connectedComponentMk_mem : ∀ {V : Type u} {G : SimpleGraph V} {v : V}, v ∈ G.connectedComponentMk v
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.expansion.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (K : ℝ) (S A : Finset G),
  Finset.expansion✝ K S A = ↑(A * S).card - K * ↑A.card
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.subsingleton_iff_eq_bot : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p : Submodule R M}, Subsingleton ↥p ↔ p = ⊥
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_f : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) [H : CompactSpace ↥X] (x : ↥⋯.choose),
  𝒰.finiteSubcover.f x = 𝒰.f (AlgebraicGeometry.Scheme.Cover.idx 𝒰 ↑x)
-- Init.Data.SInt.Lemmas
Int8.ofBitVec_ofInt : ∀ (n : ℤ), Int8.ofBitVec (BitVec.ofInt 8 n) = Int8.ofInt n
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
Right.self_lt_neg : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : Preorder α] [AddRightStrictMono α] {a : α}, a < 0 → a < -a
-- Lean.Compiler.IR.Basic
Lean.IR.LocalContext.contains : Lean.IR.LocalContext → Lean.IR.Index → Bool
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.smul_eq_map : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {K : Type u_5} [inst_1 : SMul K β] (k : K)
  (f : MeasureTheory.SimpleFunc α β), k • f = MeasureTheory.SimpleFunc.map (fun x => k • x) f
-- Std.Do.SPred.Laws
Std.Do.SVal.evalsTo_nil : ∀ {α : Type u_1} {f : Std.Do.SVal [] α} {a : α}, f.evalsTo a = ⌜a = f⌝
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.dTo_comp_dFrom : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) (j : ι),
  CategoryTheory.CategoryStruct.comp (C.dTo j) (C.dFrom j) = 0
-- Mathlib.CategoryTheory.SingleObj
/-- If `M` is finite and in universe zero, then `SingleObj M` is a `FinCategory`.  -/
CategoryTheory.SingleObj.finCategoryOfFintype : (M : Type) → [Fintype M] → [inst : Monoid M] → CategoryTheory.FinCategory (CategoryTheory.SingleObj M)
-- Mathlib.CategoryTheory.Limits.Preserves.Limits
CategoryTheory.preservesLimitIso_hom_π_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J]
  (F : CategoryTheory.Functor J C) [inst_3 : CategoryTheory.Limits.PreservesLimit F G]
  [inst_4 : CategoryTheory.Limits.HasLimit F] (j : J) {Z : D} (h : G.obj (F.obj j) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesLimitIso G F).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.comp G) j) h) =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.limit.π F j)) h
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Function.Bijective.addActionHom_embedding_isBijective : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {H : Type u_3} {β : Type u_4}
  [inst_2 : AddGroup H] [inst_3 : AddAction H β] {σ : G → H} {f : α →ₑ[σ] β} {ι : Type u_5}
  (hf : Function.Bijective ⇑f), Function.Bijective ⇑(Function.Injective.addActionHom_embedding ι ⋯)
-- Mathlib.Order.SupClosed
infClosed_infClosure : ∀ {α : Type u_3} [inst : SemilatticeInf α] {s : Set α}, InfClosed (infClosure s)