mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Analytic.Basic
AnalyticWithinAt.eq_1 : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F) (s : Set E) (x : E),
  AnalyticWithinAt 𝕜 f s x = ∃ p, HasFPowerSeriesWithinAt f p s x
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.instSMul : {α : Type u_1} →
  {R : Type u_6} →
    [inst : SMul R ENNReal] →
      [IsScalarTower R ENNReal ENNReal] → {x : MeasurableSpace α} → SMul R (MeasureTheory.Measure α)
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.tail : Turing.ToPartrec.Code
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
/-- If `G` is a Galois group for `C/A`, the normal subgroup `N ≤ G` is a Galois group for `C/B`,
and `G'` is a Galois group for `B/A`, then `G ⧸ N ≃* G'`.  -/
IsGaloisGroup.quotientMulEquiv : (G : Type u_1) →
  (G' : Type u_2) →
    [inst : Group G] →
      [inst_1 : Group G'] →
        (A : Type u_5) →
          (B : Type u_6) →
            (C : Type u_7) →
              [inst_2 : CommRing A] →
                [inst_3 : CommRing B] →
                  [inst_4 : CommRing C] →
                    [IsDomain C] →
                      [inst_6 : Algebra A B] →
                        [inst_7 : Algebra A C] →
                          [inst_8 : Algebra B C] →
                            [FaithfulSMul A B] →
                              [FaithfulSMul B C] →
                                [IsScalarTower A B C] →
                                  [Finite G] →
                                    [Finite G'] →
                                      (N : Subgroup G) →
                                        [inst_14 : N.Normal] →
                                          [inst_15 : MulSemiringAction G C] →
                                            [IsGaloisGroup G A C] →
                                              [IsGaloisGroup (↥N) B C] →
                                                [inst_18 : MulSemiringAction G' B] →
                                                  [IsGaloisGroup G' A B] → G ⧸ N ≃* G'
-- Init.Data.Fin.Fold
_private.Init.Data.Fin.Fold.0.Fin.foldrM.loop.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] (n : ℕ) (f : Fin n → α → m α) (a : α) (property : 0 ≤ n),
  Fin.foldrM.loop✝ n f ⟨0, property⟩ a = pure a
-- Mathlib.AlgebraicGeometry.ZariskisMainTheorem
AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_eq_top : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyQuasiFinite f]
  [inst : AlgebraicGeometry.LocallyOfFiniteType f], AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus f = ⊤
-- Lean.Meta.GeneralizeVars
/-- Add to `forbidden` all a set of `FVarId`s containing `targets` and all variables they depend on.
 -/
Lean.Meta.mkGeneralizationForbiddenSet : Array Lean.Expr → optParam Lean.FVarIdSet ∅ → Lean.MetaM Lean.FVarIdSet
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.isOpen_image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) {s : Set X},
  IsOpen (⇑h '' s) ↔ IsOpen s
-- Mathlib.RingTheory.AdjoinRoot
Polynomial.Monic.finite_adjoinRoot : ∀ {R : Type u_1} [inst : CommRing R] {g : Polynomial R}, g.Monic → Module.Finite R (AdjoinRoot g)
-- Lean.Widget.Diff
_private.Lean.Widget.Diff.0.Lean.Widget.ExprDiffTag.insert.sizeOf_spec : sizeOf Lean.Widget.ExprDiffTag.insert✝ = 1
-- Mathlib.LinearAlgebra.Projectivization.Subspace
/-- Infimums of arbitrary collections of subspaces exist.  -/
Projectivization.Subspace.instInfSet : {K : Type u_1} →
  {V : Type u_2} →
    [inst : DivisionRing K] → [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → InfSet (Projectivization.Subspace K V)
-- Std.Data.Internal.List.Associative
Std.Internal.List.DistinctKeys.insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {k : α} {v : β k} {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l → Std.Internal.List.DistinctKeys (Std.Internal.List.insertEntryIfNew k v l)
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atBot_of_const_mul : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelMonoid M] {l : Filter α}
  {f : α → M} (C : M), Filter.Tendsto (fun x => C * f x) l Filter.atBot → Filter.Tendsto f l Filter.atBot
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
/-- The tail of an `m`-admissible list is (m+1)-admissible.  -/
SimplexCategoryGenRel.IsAdmissible.of_cons : ∀ {m a : ℕ} {L : List ℕ}, SimplexCategoryGenRel.IsAdmissible m (a :: L) → SimplexCategoryGenRel.IsAdmissible (m + 1) L
-- Lean.Parser.Syntax
/-- `infix:prec "op" => f` is equivalent to `notation:prec x:prec1 "op" y:prec1 => f x y`, where `prec1 := prec + 1`.
 -/
Lean.Parser.Command.infix : Lean.Parser.Parser
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_le_toNNReal_iff_of_pos : ∀ {r p : ℝ}, 0 < r → (r.toNNReal ≤ p.toNNReal ↔ r ≤ p)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_nil : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit),
  ↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m []) = m
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.instBoundedOrder : BoundedOrder BoxIntegral.IntegrationParams
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.braiding_inv_apply : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] [inst_2 : (i : I) → CategoryTheory.BraidedCategory (C i)]
  {X Y : (i : I) → C i} {i : I}, (β_ X Y).inv i = (β_ (X i) (Y i)).inv
-- Mathlib.Logic.UnivLE
univLE_iff : UnivLE.{u, v} ↔ ∀ (α : Type u), Small.{v, u} α
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.size_ofList_le : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {l : List (α × β)},
  (Std.DTreeMap.Raw.Const.ofList l cmp).size ≤ l.length
-- Mathlib.RingTheory.NonUnitalSubring.Defs
/-- A non-unital subring is closed under subtraction  -/
NonUnitalSubring.sub_mem : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (s : NonUnitalSubring R) {x y : R}, x ∈ s → y ∈ s → x - y ∈ s
-- Lean.Meta.Coe
/-- Coerces `expr` to `expectedType` using `CoeT`.  -/
Lean.Meta.coerceSimple? : Lean.Expr → Lean.Expr → Lean.MetaM (Lean.LOption Lean.Expr)
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePresentation.hasMap : ∀ {R : Type u_4} {S : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (self : StandardEtalePresentation R S), self.HasMap self.x
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapPair_obj_left : ∀ {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] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] (Fₗ : CategoryTheory.Functor C E) (Fᵣ : CategoryTheory.Functor D E')
  (c : C), (CategoryTheory.Join.mapPair Fₗ Fᵣ).obj (CategoryTheory.Join.left c) = CategoryTheory.Join.left (Fₗ.obj c)
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
StandardSubspace.mk.inj : ∀ {H : Type u_1} {inst : NormedAddCommGroup H} {inst_1 : InnerProductSpace ℂ H}
  {toClosedSubmodule : ClosedSubmodule ℝ H} {IsSeparating : toClosedSubmodule ⊓ toClosedSubmodule.mulI = ⊥}
  {IsCyclic : toClosedSubmodule ⊔ toClosedSubmodule.mulI = ⊤} {toClosedSubmodule_1 : ClosedSubmodule ℝ H}
  {IsSeparating_1 : toClosedSubmodule_1 ⊓ toClosedSubmodule_1.mulI = ⊥}
  {IsCyclic_1 : toClosedSubmodule_1 ⊔ toClosedSubmodule_1.mulI = ⊤},
  { toClosedSubmodule := toClosedSubmodule, IsSeparating := IsSeparating, IsCyclic := IsCyclic } =
      { toClosedSubmodule := toClosedSubmodule_1, IsSeparating := IsSeparating_1, IsCyclic := IsCyclic_1 } →
    toClosedSubmodule = toClosedSubmodule_1
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
/-- A functor reflects finite effective epimorphic families if finite families that are
mapped to effective epimorphic families are themselves effective epimorphic families.
 -/
CategoryTheory.Functor.ReflectsFiniteEffectiveEpiFamilies.reflects : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {D : Type u_2}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {F : CategoryTheory.Functor C D}
  [self : F.ReflectsFiniteEffectiveEpiFamilies] {α : Type} [Finite α] {B : C} (X : α → C) (π : (a : α) → X a ⟶ B),
  (CategoryTheory.EffectiveEpiFamily (fun a => F.obj (X a)) fun a => F.map (π a)) →
    CategoryTheory.EffectiveEpiFamily X π
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.all.eq_1 : ∀ {α : Type u_1} (p : α → Bool), RBTree.RBNode.all p RBTree.RBNode.nil = true
-- Mathlib.Algebra.Group.Hom.Defs
AddHom.inverse_apply : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N) (g : N → M)
  (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) (a : N), (f.inverse g h₁ h₂) a = g a
-- Mathlib.Algebra.BigOperators.Finprod
/-- See also `finsum_mem_finset_product'`.  -/
finsum_mem_finset_product : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] (s : Finset (α × β)) (f : α × β → M),
  ∑ᶠ (ab : α × β) (_ : ab ∈ s), f ab = ∑ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b)
-- Mathlib.Analysis.RCLike.Basic
RCLike.norm_two : ∀ {K : Type u_1} [inst : RCLike K], ‖2‖ = 2
-- Init.Data.Array.Lemmas
Array.foldl_eq_foldl_extract : ∀ {α : Type u_1} {β : Type u_2} {start stop : ℕ} {xs : Array α} {f : β → α → β} {init : β},
  Array.foldl f init xs start stop = Array.foldl f init (xs.extract start stop)
-- Lean.Environment
Lean.OLeanLevel.server.sizeOf_spec : sizeOf Lean.OLeanLevel.server = 1
-- Aesop.Search.Expansion.Norm
Aesop.NormM.Context : Type
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Countable.instBorelSpace : ∀ {α : Type u_1} [Countable α] [inst : MeasurableSpace α] [MeasurableSingletonClass α] [inst_2 : TopologicalSpace α]
  [DiscreteTopology α], BorelSpace α
-- Mathlib.MeasureTheory.Function.Holder
ContinuousLinearMap.holder_smul_left : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {p q r : ENNReal} [hpqr : p.HolderTriple q r] [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedAddCommGroup G]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 F] [inst_6 : NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G) (c : 𝕜)
  (f : ↥(MeasureTheory.Lp E p μ)) (g : ↥(MeasureTheory.Lp F q μ)),
  ContinuousLinearMap.holder r B (c • f) g = c • ContinuousLinearMap.holder r B f g
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.lift_power : ∀ (a b : Cardinal.{u}), Cardinal.lift.{v, u} (a ^ b) = Cardinal.lift.{v, u} a ^ Cardinal.lift.{v, u} b
-- Mathlib.LinearAlgebra.Alternating.DomCoprod
AlternatingMap.domCoprod.summand_mk'' : ∀ {ιa : Type u_1} {ιb : Type u_2} [inst : Fintype ιa] [inst_1 : Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4}
  {N₁ : Type u_5} {N₂ : Type u_6} [inst_2 : CommSemiring R'] [inst_3 : AddCommGroup N₁] [inst_4 : Module R' N₁]
  [inst_5 : AddCommGroup N₂] [inst_6 : Module R' N₂] [inst_7 : AddCommMonoid Mᵢ] [inst_8 : Module R' Mᵢ]
  [inst_9 : DecidableEq ιa] [inst_10 : DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂)
  (σ : Equiv.Perm (ιa ⊕ ιb)),
  AlternatingMap.domCoprod.summand a b (Quotient.mk'' σ) =
    Equiv.Perm.sign σ • MultilinearMap.domDomCongr σ ((↑a).domCoprod ↑b)
-- Init.Data.List.Sublist
List.suffix_filter_iff : ∀ {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α}, l₂ <:+ List.filter p l₁ ↔ ∃ l, l <:+ l₁ ∧ l₂ = List.filter p l
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Coverage.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (toPrecoverage : CategoryTheory.Precoverage C) →
      (∀ ⦃X Y : C⦄ (f : Y ⟶ X),
          ∀ S ∈ toPrecoverage.coverings X, ∃ T ∈ toPrecoverage.coverings Y, T.FactorsThruAlong S f) →
        CategoryTheory.Coverage C
-- Mathlib.Algebra.Order.Field.Basic
/-- For the single implications with fewer assumptions, see `one_div_lt_one_div_of_lt` and
`lt_of_one_div_lt_one_div`  -/
one_div_lt_one_div : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b : α} [IsStrictOrderedRing α],
  0 < a → 0 < b → (1 / a < 1 / b ↔ b < a)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
CFC.log.congr_simp : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a a_1 : A), a = a_1 → CFC.log a = CFC.log a_1
-- Mathlib.Probability.Kernel.Integral
ProbabilityTheory.Kernel.setIntegral_deterministic' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {E : Type u_3}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : β → E} {a : α} [CompleteSpace E] {g : α → β}
  (hg : Measurable g),
  MeasureTheory.StronglyMeasurable f →
    ∀ {s : Set β},
      MeasurableSet s →
        ∀ [inst_3 : Decidable (g a ∈ s)],
          ∫ (x : β) in s, f x ∂(ProbabilityTheory.Kernel.deterministic g hg) a = if g a ∈ s then f (g a) else 0
-- Mathlib.ModelTheory.Syntax
/-- Applies a binary relation to two terms as a formula.  -/
FirstOrder.Language.Relations.formula₂ : {L : FirstOrder.Language} → {α : Type u'} → L.Relations 2 → L.Term α → L.Term α → L.Formula α
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.prod_bot : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_8}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'], ⊥.prod ⊥ = ⊥
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.approx_mk : ∀ {F : PFunctor.{uA, uB}} (a : F.A) (f : F.B a → F.M) (i : ℕ),
  (PFunctor.M.mk ⟨a, f⟩).approx i.succ = PFunctor.Approx.CofixA.intro a fun j => (f j).approx i
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.prevn_add_one : ∀ {n : ℕ} {s : String.Slice} {p : s.Pos}, p.prevn (n + 1) = if h : p = s.startPos then p else (p.prev h).prevn n
-- Mathlib.Topology.Algebra.Algebra
/-- The coercion from an elemental algebra to the full algebra is a `IsClosedEmbedding`.  -/
Algebra.elemental.isClosedEmbedding_coe : ∀ (R : Type u_1) [inst : CommSemiring R] {A : Type u} [inst_1 : TopologicalSpace A] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : IsSemitopologicalSemiring A] (x : A), Topology.IsClosedEmbedding Subtype.val
-- Init.Data.Array.Lemmas
List.map_toArray : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α}, Array.map f l.toArray = (List.map f l).toArray
-- Init.Data.List.Find
List.isNone_finIdxOf? : ∀ {α : Type u_1} [inst : BEq α] [PartialEquivBEq α] {l : List α} {a : α}, (List.finIdxOf? a l).isNone = !l.contains a
-- Mathlib.Order.Atoms
IsCompl.isAtom_iff_isCoatom : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : BoundedOrder α] [IsModularLattice α] {a b : α},
  IsCompl a b → (IsAtom a ↔ IsCoatom b)
-- Mathlib.NumberTheory.ModularForms.QExpansion
ModularForm.qExpansion_of_pow : ∀ {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} [inst : Γ.HasDetPlusMinusOne],
  0 < h →
    h ∈ Γ.strictPeriods →
      ∀ (f : ModularForm Γ k) (n : ℕ),
        UpperHalfPlane.qExpansion h ⇑(((DirectSum.of (ModularForm Γ) k) f ^ n) (↑n * k)) =
          UpperHalfPlane.qExpansion h ⇑f ^ n
-- Mathlib.Order.Closure
/-- Define a closure operator from a predicate that's preserved under infima.  -/
ClosureOperator.ofCompletePred : {α : Type u_1} →
  [inst : CompleteLattice α] → (p : α → Prop) → (∀ (s : Set α), (∀ a ∈ s, p a) → p (sInf s)) → ClosureOperator α
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
/-- A `n + 1`-simplex  -/
SSet.PtSimplex.RelStruct.map : {X : SSet} →
  {n : ℕ} →
    {x : X.obj (Opposite.op { len := 0 })} →
      {f g : X.PtSimplex n x} → {i : Fin (n + 1)} → f.RelStruct g i → (SSet.stdSimplex.obj { len := n + 1 } ⟶ X)
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.a₃_of_isCharThreeJNeZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF], W.a₃ = 0
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Module.FaithfullyFlat.iff_flat_and_lTensor_faithful : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.FaithfullyFlat R M ↔
    Module.Flat R M ∧
      ∀ (N : Type (max u v)) [inst_3 : AddCommGroup N] [inst_4 : Module R N],
        Nontrivial N → Nontrivial (TensorProduct R M N)
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instDecidableLeOffset : {x y : Std.Time.Nanosecond.Offset} → Decidable (x ≤ y)
-- Lean.Elab.Arg
Lean.Elab.Term.instToStringNamedArg : ToString Lean.Elab.Term.NamedArg
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapCycles₁_comp_i_apply : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (x : ↥(groupHomology.cycles₁ A)),
  (ModuleCat.Hom.hom (groupHomology.shortComplexH1 B).g).ker.subtype
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.mapCycles₁ f φ)) x) =
    (Finsupp.mapRange.linearMap (Rep.Hom.hom φ).toLinearMap)
      ((Finsupp.lmapDomain (↑A) k ⇑f) ((ModuleCat.Hom.hom (groupHomology.shortComplexH1 A).g).ker.subtype x))
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.neg_apply : ∀ {p : ENNReal} {ι : Type u_2} (β : ι → Type u_4) [inst : (i : ι) → SeminormedAddCommGroup (β i)] (x : PiLp p β)
  (i : ι), (-x).ofLp i = -x.ofLp i
-- Mathlib.CategoryTheory.Sites.ConstantSheaf
/-- A variant of `isConstant_iff_isIso_counit_app` for a general left adjoint to evaluation at a
terminal object.
 -/
CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  {D : Type u_2} [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {L : CategoryTheory.Functor D (CategoryTheory.Sheaf J D)} {T : C} (hT : CategoryTheory.Limits.IsTerminal T)
  (adj : L ⊣ (CategoryTheory.sheafSections J D).obj (Opposite.op T)) [L.Faithful] [L.Full]
  (F : CategoryTheory.Sheaf J D), CategoryTheory.Sheaf.IsConstant J F ↔ CategoryTheory.IsIso (adj.counit.app F)
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.IsSplitMono.id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) [hf : CategoryTheory.IsSplitMono f],
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.retraction f) = CategoryTheory.CategoryStruct.id Y
-- Mathlib.Analysis.Normed.Group.BallSphere
instContinuousNegElemSphereOfNat : ∀ {E : Type u_1} [i : SeminormedAddCommGroup E] {r : ℝ}, ContinuousNeg ↑(Metric.sphere 0 r)
-- Mathlib.Algebra.Free
/-- Recursor on `FreeAddMagma` using `pure` instead of `of`.  -/
FreeAddMagma.recOnPure : {α : Type u} →
  {C : FreeAddMagma α → Sort l} →
    (x : FreeAddMagma α) → ((x : α) → C (pure x)) → ((x y : FreeAddMagma α) → C x → C y → C (x + y)) → C x
-- Mathlib.RingTheory.FiniteType
Subalgebra.fg_iff_finiteType : ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A),
  S.FG ↔ Algebra.FiniteType R ↥S
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolutionUnit.corepresentableByLeft_homEquiv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (U : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolutionUnit U]
  (F : CategoryTheory.Functor C V)
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution U F] {Y : CategoryTheory.Functor C V},
  (CategoryTheory.MonoidalCategory.DayConvolutionUnit.corepresentableByLeft U F).homEquiv =
    ((CategoryTheory.MonoidalCategory.DayConvolution.convolution U F).homEquivOfIsLeftKanExtension
          (CategoryTheory.MonoidalCategory.DayConvolution.unit U F) Y).trans
      ((CategoryTheory.MonoidalCategory.externalProduct U F).homEquivOfIsLeftKanExtension
        (CategoryTheory.MonoidalCategory.ExternalProduct.extensionUnitLeft U
          (CategoryTheory.MonoidalCategory.DayConvolutionUnit.φ U) F)
        ((CategoryTheory.MonoidalCategory.tensor C).comp Y))
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.getDiscrs : Lean.Syntax → Array Lean.Syntax
-- Mathlib.Algebra.Homology.ShortComplex.Limits
CategoryTheory.ShortComplex.instPreservesFiniteLimitsπ₂ : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{v_2, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteLimits C], CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.ShortComplex.π₂
-- Mathlib.Algebra.Order.Monoid.Canonical.Basic
lt_add_iff_lt_right_or_exists_lt : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α} [inst_1 : AddCommMagma α] [CanonicallyOrderedAdd α]
  [AddLeftReflectLT α] [IsLeftCancelAdd α], a < b + c ↔ a < c ∨ ∃ d < b, a = d + c
-- Mathlib.Topology.VectorBundle.Basic
VectorPrebundle.trivializationOfMemPretrivializationAtlas.eq_1 : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : (x : B) → TopologicalSpace (E x)]
  (a : VectorPrebundle R F E) {e : Bundle.Pretrivialization F Bundle.TotalSpace.proj}
  (he : e ∈ a.pretrivializationAtlas),
  a.trivializationOfMemPretrivializationAtlas he = a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he
-- Lean.Meta.Eqns
/-- Registers a new function for retrieving a "unfold" equation theorem.

We generate this kind of equation theorem on demand, and it is generated by more than one module.
For example, the structural and well-founded recursion modules generate it.
Most recent getters are tried first.

A getter returns an `Option Name`. The result is `none` if the getter failed.
Otherwise, it is a theorem name. Example: the definition

```
def f (xs : List Nat) : List Nat :=
  match xs with
  | [] => []
  | x::xs => (x+1)::f xs
```
should have the theorem
```
(xs : Nat) →
  f xs =
    match xs with
    | [] => []
    | x::xs => (x+1)::f xs
```
 -/
Lean.Meta.registerGetUnfoldEqnFn : Lean.Meta.GetUnfoldEqnFn → IO Unit
-- Mathlib.Algebra.Group.Center
Set.inv_mem_centralizer : ∀ {M : Type u_1} {S : Set M} [inst : Group M] {a : M}, a ∈ S.centralizer → a⁻¹ ∈ S.centralizer
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- Subtracting two points in the subspace produces a vector in the direction.  -/
AffineSubspace.vsub_mem_direction : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : AffineSubspace k P} {p₁ p₂ : P}, p₁ ∈ s → p₂ ∈ s → p₁ -ᵥ p₂ ∈ s.direction
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → (t₁ ∩ t₂).getKey? k = none
-- Mathlib.Data.Num.Lemmas
Num.dvd_to_nat : ∀ (m n : Num), ↑m ∣ ↑n ↔ m ∣ n
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.get?.match_1.eq_1 : ∀ {α : Type u_2} {β : Type u_1} (motive : (Std.DHashMap.Internal.AssocList α fun x => β) → Sort u_3)
  (h_1 : Unit → motive Std.DHashMap.Internal.AssocList.nil)
  (h_2 :
    (k : α) →
      (v : β) →
        (es : Std.DHashMap.Internal.AssocList α fun x => β) → motive (Std.DHashMap.Internal.AssocList.cons k v es)),
  (match Std.DHashMap.Internal.AssocList.nil with
    | Std.DHashMap.Internal.AssocList.nil => h_1 ()
    | Std.DHashMap.Internal.AssocList.cons k v es => h_2 k v es) =
    h_1 ()