mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- `ContinuousMultilinearMap.pi` as a `LinearEquiv`.  -/
ContinuousMultilinearMap.piLinearEquiv : {ι : Type v} →
  {M₁ : ι → Type w₁} →
    {R' : Type u_1} →
      {A : Type u_2} →
        [inst : Semiring R'] →
          [inst_1 : Semiring A] →
            [inst_2 : (i : ι) → AddCommMonoid (M₁ i)] →
              [inst_3 : (i : ι) → TopologicalSpace (M₁ i)] →
                [inst_4 : (i : ι) → Module A (M₁ i)] →
                  {ι' : Type u_3} →
                    {M' : ι' → Type u_4} →
                      [inst_5 : (i : ι') → AddCommMonoid (M' i)] →
                        [inst_6 : (i : ι') → TopologicalSpace (M' i)] →
                          [inst_7 : ∀ (i : ι'), ContinuousAdd (M' i)] →
                            [inst_8 : (i : ι') → Module R' (M' i)] →
                              [inst_9 : (i : ι') → Module A (M' i)] →
                                [inst_10 : ∀ (i : ι'), SMulCommClass A R' (M' i)] →
                                  [inst_11 : ∀ (i : ι'), ContinuousConstSMul R' (M' i)] →
                                    ((i : ι') → ContinuousMultilinearMap A M₁ (M' i)) ≃ₗ[R']
                                      ContinuousMultilinearMap A M₁ ((i : ι') → M' i)
-- Mathlib.Probability.Independence.Basic
/-- **Alias** of the forward direction of `ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map`. -/
ProbabilityTheory.IndepFun.map_prod_eq_prod_map_map : ∀ {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ω → β}
  {g : Ω → β'} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} [MeasureTheory.IsFiniteMeasure μ],
  AEMeasurable f μ →
    AEMeasurable g μ →
      ProbabilityTheory.IndepFun f g μ →
        MeasureTheory.Measure.map (fun ω => (f ω, g ω)) μ =
          (MeasureTheory.Measure.map f μ).prod (MeasureTheory.Measure.map g μ)
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.subgroup_eq_top_of_swap_mem : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {H : Subgroup (Equiv.Perm α)}
  [d : DecidablePred fun x => x ∈ H] {τ : Equiv.Perm α},
  Nat.Prime (Fintype.card α) → Fintype.card α ∣ Fintype.card ↥H → τ ∈ H → τ.IsSwap → H = ⊤
-- Init.Internal.Order.While
_private.Init.Internal.Order.While.0.repeatM.body.match_1.splitter : {α β : Type u_1} →
  (motive : α ⊕ β → Sort u_2) →
    (__do_lift : α ⊕ β) → ((a : α) → motive (Sum.inl a)) → ((b : β) → motive (Sum.inr b)) → motive __do_lift
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Example.var.inj : ∀ {a a_1 : Lean.FVarId}, Lean.Meta.Match.Example.var a = Lean.Meta.Match.Example.var a_1 → a = a_1
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
MulOpposite.toContinuousLinearEquiv_opLinearIsometryEquiv : ∀ {R : Type u_11} {H : Type u_12} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup H] [inst_2 : Module R H],
  ↑(MulOpposite.opLinearIsometryEquiv R H) = MulOpposite.opContinuousLinearEquiv R
-- Mathlib.Order.Lattice
Prod.instSemilatticeSup.eq_1 : ∀ (α : Type u) (β : Type v) [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β],
  Prod.instSemilatticeSup α β =
    { toPartialOrder := Prod.instPartialOrder α β, sup := fun a b => (a.1 ⊔ b.1, a.2 ⊔ b.2), le_sup_left := ⋯,
      le_sup_right := ⋯, sup_le := ⋯ }
-- Mathlib.Data.EReal.Basic
EReal.image_coe_Ico : ∀ (x y : ℝ), Real.toEReal '' Set.Ico x y = Set.Ico ↑x ↑y
-- Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished
Polynomial.IsDistinguishedAt.toIsWeaklyEisensteinAt : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} {I : Ideal R}, f.IsDistinguishedAt I → f.IsWeaklyEisensteinAt I
-- Std.Time.Date.Unit.Month
/-- Creates an `Ordinal` from a `Fin`, ensuring the value is within bounds, if its 0 then its converted
to 1.
 -/
Std.Time.Month.Ordinal.ofFin : Fin 13 → Std.Time.Month.Ordinal
-- Mathlib.GroupTheory.OreLocalization.OreSet
/-- The Ore condition bundled in a sigma type. This is useful in situations where we want to obtain
both witnesses and the condition for a given difference.  -/
AddOreLocalization.addOreCondition : {R : Type u_1} →
  [inst : AddMonoid R] →
    {S : AddSubmonoid R} →
      [AddOreLocalization.AddOreSet S] → (r : R) → (s : ↥S) → (r' : R) ×' (s' : ↥S) ×' ↑s' + r = r' + ↑s
-- Mathlib.Algebra.Order.Group.DenselyOrdered
_private.Mathlib.Algebra.Order.Group.DenselyOrdered.0.exists_mul_right_lt : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : LT α] [DenselyOrdered α] [MulLeftStrictMono α] {a b c : α},
  a * b < c → ∃ b' > b, a * b' < c
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.hasPullbacksAgainst_top_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C),
  P.HasPullbacksAgainst ⊤ ↔ P.HasPullbacks
-- Mathlib.Algebra.Star.MonoidHom
/-- See Note [custom simps projection]  -/
StarMulEquiv.Simps.symm_apply : {A : Type u_2} →
  {B : Type u_3} → [inst : Mul A] → [inst_1 : Mul B] → [inst_2 : Star A] → [inst_3 : Star B] → (A ≃⋆* B) → B → A
-- Lean.Elab.Match
Lean.Elab.Term.Discr.mk.sizeOf_spec : ∀ (expr : Lean.Expr) (h? : Option Lean.Syntax), sizeOf { expr := expr, h? := h? } = 1 + sizeOf expr + sizeOf h?
-- Mathlib.GroupTheory.Coset.Basic
Subgroup.inclusion.congr_simp : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} (h : H ≤ K), Subgroup.inclusion h = Subgroup.inclusion h
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.instIsFilteredCostructuredArrowCompOfRepresentablyCoflat : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (X : E) [CategoryTheory.RepresentablyCoflat F]
  [h : CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow G X)],
  CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow (F.comp G) X)
-- Mathlib.Order.Heyting.Hom
/-- The proposition that a Heyting homomorphism preserves the Heyting implication.  -/
HeytingHomClass.map_himp : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} {inst : HeytingAlgebra α} {inst_1 : HeytingAlgebra β}
  {inst_2 : FunLike F α β} [self : HeytingHomClass F α β] (f : F) (a b : α), f (a ⇨ b) = f a ⇨ f b
-- Mathlib.Condensed.Limits
instHasLimitsOfSizeCondensedSet : CategoryTheory.Limits.HasLimitsOfSize.{u, u + 1, u + 1, u + 2} CondensedSet
-- Mathlib.Topology.Instances.EReal.Lemmas
_private.Mathlib.Topology.Instances.EReal.Lemmas.0.EReal.continuousAt_mul_symm2 : ∀ {a b : EReal}, ContinuousAt (fun p => p.1 * p.2) (a, b) → ContinuousAt (fun p => p.1 * p.2) (a, -b)
-- Mathlib.Order.Category.FinBddDistLat
/-- The underlying `BoundedLatticeHom`.  -/
FinBddDistLat.Hom.hom' : {X Y : FinBddDistLat} → X.Hom Y → BoundedLatticeHom ↑X.toDistLat ↑Y.toDistLat
-- Mathlib.Algebra.Order.Floor.Extended
ENat.floor_top : ⌊⊤⌋ₑ = ⊤
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] (h : t.WF) {k a : α} {v : β k}
  {h₁ : a ∈ (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl},
  (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.get a h₁ =
    if h₂ : compare k a = Ordering.eq ∧ k ∉ t then cast ⋯ v else t.get a ⋯
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.mem_edgeFinset : ∀ {V : Type u_1} {G : SimpleGraph V} {e : Sym2 V} [inst : Fintype ↑G.edgeSet], e ∈ G.edgeFinset ↔ e ∈ G.edgeSet
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_assoc : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) {Z : ModuleCat k}
  (h : (groupCohomology.shortComplexH0 B).X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupCohomology.cocyclesMap f φ 0)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.cocyclesIso₀ B).hom
        (CategoryTheory.CategoryStruct.comp (groupCohomology.shortComplexH0 B).f h)) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.cocyclesIso₀ A).hom
      (CategoryTheory.CategoryStruct.comp (groupCohomology.shortComplexH0 A).f
        (CategoryTheory.CategoryStruct.comp (Rep.Hom.toModuleCatHom φ) h))
-- Mathlib.Order.Antichain
IsMaxAntichain.image : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) {c : Set α},
  IsMaxAntichain r c → IsMaxAntichain s (⇑e '' c)
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.refl_trans : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (e : AddConstEquiv G H a b),
  (AddConstEquiv.refl a).trans e = e
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.instAdd : {R : Type u} →
  [inst : CommSemiring R] →
    {M : Type u_1} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → {N : Type u_2} → [inst_3 : AddCommMonoid N] → [inst_4 : Module R N] → Add (M →ₚₗ[R] N)
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- `LinearMap.compMultilinearMap` as an `S`-linear map.  -/
LinearMap.compMultilinearMapₗ : {R : Type uR} →
  (S : Type uS) →
    {ι : Type uι} →
      {M₁ : ι → Type v₁} →
        {M₂ : Type v₂} →
          {M₃ : Type v₃} →
            [inst : Semiring R] →
              [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
                [inst_2 : (i : ι) → Module R (M₁ i)] →
                  [inst_3 : AddCommMonoid M₂] →
                    [inst_4 : Module R M₂] →
                      [inst_5 : Semiring S] →
                        [inst_6 : Module S M₂] →
                          [inst_7 : SMulCommClass R S M₂] →
                            [inst_8 : AddCommMonoid M₃] →
                              [inst_9 : Module S M₃] →
                                [inst_10 : Module R M₃] →
                                  [inst_11 : SMulCommClass R S M₃] →
                                    [LinearMap.CompatibleSMul M₂ M₃ S R] →
                                      (M₂ →ₗ[R] M₃) → MultilinearMap R M₁ M₂ →ₗ[S] MultilinearMap R M₁ M₃
-- Mathlib.Order.GameAdd
/-- Induction on the well-founded `Sym2.GameAdd` relation.  -/
Sym2.GameAdd.induction : ∀ {α : Type u_1} {rα C : α → α → Prop},
  WellFounded rα →
    (∀ (a₁ b₁ : α), (∀ (a₂ b₂ : α), Sym2.GameAdd rα s(a₂, b₂) s(a₁, b₁) → C a₂ b₂) → C a₁ b₁) → ∀ (a b : α), C a b
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get_getElem? : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h : m.WF) {a : α} {h' : m[a]?.isSome = true}, m[a]?.get h' = m[a]
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.instTransIsBigOTVSIsLittleOTVS : {α : Type u_1} →
  {𝕜 : Type u_3} →
    {E : Type u_4} →
      {F : Type u_5} →
        {G : Type u_6} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : AddCommGroup E] →
              [inst_2 : TopologicalSpace E] →
                [inst_3 : Module 𝕜 E] →
                  [inst_4 : AddCommGroup F] →
                    [inst_5 : TopologicalSpace F] →
                      [inst_6 : Module 𝕜 F] →
                        [inst_7 : AddCommGroup G] →
                          [inst_8 : TopologicalSpace G] →
                            [inst_9 : Module 𝕜 G] →
                              {l : Filter α} →
                                Trans (Asymptotics.IsBigOTVS 𝕜 l) (Asymptotics.IsLittleOTVS 𝕜 l)
                                  (Asymptotics.IsLittleOTVS 𝕜 l)
-- Mathlib.SetTheory.ZFC.PSet
PSet.mem_insert_iff : ∀ {x y z : PSet.{u}}, x ∈ insert y z ↔ x.Equiv y ∨ x ∈ z
-- Init.Data.SInt.Lemmas
Int16.toBitVec_maxValue : Int16.maxValue.toBitVec = BitVec.intMax 16
-- Mathlib.GroupTheory.CoprodI
MulOneClass.toMulOne.hcongr_2 : ∀ (M M' : Type u),
  M = M' → ∀ (self : MulOneClass M) (self' : MulOneClass M'), self ≍ self' → self.toMulOne ≍ self'.toMulOne
-- Mathlib.Analysis.Fourier.AddCircleMulti
_private.Mathlib.Analysis.Fourier.AddCircleMulti.0.UnitAddTorus.«termL²(_)» : Lean.ParserDescr
-- Lean.Elab.Binders
Lean.Elab.Term.LetIdDeclView.mk.injEq : ∀ (id : Lean.Syntax) (binders : Array Lean.Syntax) (type value id_1 : Lean.Syntax) (binders_1 : Array Lean.Syntax)
  (type_1 value_1 : Lean.Syntax),
  ({ id := id, binders := binders, type := type, value := value } =
      { id := id_1, binders := binders_1, type := type_1, value := value_1 }) =
    (id = id_1 ∧ binders = binders_1 ∧ type = type_1 ∧ value = value_1)
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.lookahead.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_id_right_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b : B} (f : a ⟶ b),
  (F.mapComp f (CategoryTheory.CategoryStruct.id b)).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapId b).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).hom
        (F.map₂ (CategoryTheory.Bicategory.rightUnitor f).inv))
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- Special case of the **Plünnecke-Ruzsa inequality**. Subtraction version.  -/
Finset.pluennecke_ruzsa_inequality_nsmul_sub : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddCommGroup G] {A : Finset G},
  A.Nonempty → ∀ (B : Finset G) (n : ℕ), ↑(n • B).card ≤ (↑(A - B).card / ↑A.card) ^ n * ↑A.card
-- Mathlib.Algebra.Module.ULift
ULift.module : {R : Type u} →
  {M : Type v} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Module (ULift.{u_1, u} R) M
-- Mathlib.Algebra.Group.Defs
/-- Addition is commutative in a commutative additive magma.  -/
AddCommMagma.add_comm : ∀ {G : Type u} [self : AddCommMagma G] (a b : G), a + b = b + a
-- Lean.Elab.PreDefinition.Structural.Main
/-- Temporarily adds the recursive functions as axioms to the environment and runs the given action.
The environment is restored afterwards, so no persistent changes (e.g. auxiliary definitions) can
be made inside the action.

This is needed around any `MetaM` code that may try to infer the type of, or unfold, expressions
that still mention the recursive function constants (e.g. `isDefEq`, `inferType`, `whnf` on
arguments of recursive calls). Without these axioms, the kernel would reject the unknown constants.
 -/
_private.Lean.Elab.PreDefinition.Structural.Main.0.Lean.Elab.Structural.withRecFunsAsAxioms : {n : Type → Type} →
  {α : Type} →
    [Monad n] →
      [MonadLiftT Lean.MetaM n] → [Lean.MonadEnv n] → [MonadFinally n] → Array Lean.Elab.PreDefinition → n α → n α
-- Init.Data.List.Lemmas
List.getLast.eq_1 : ∀ {α : Type u} (h : [] ≠ []), [].getLast h = absurd ⋯ h
-- Mathlib.Data.Complex.Basic
Complex.range_im : Set.range Complex.im = Set.univ
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.IsBasis.of_delete : ∀ {α : Type u_1} {M : Matroid α} {I D X : Set α}, (M.delete D).IsBasis I X → M.IsBasis I X
-- Mathlib.Tactic.Explode.Datatypes
Mathlib.Explode.Entries.mk.injEq : ∀ (s : Lean.ExprMap Mathlib.Explode.Entry) (l : List Mathlib.Explode.Entry) (s_1 : Lean.ExprMap Mathlib.Explode.Entry)
  (l_1 : List Mathlib.Explode.Entry), ({ s := s, l := l } = { s := s_1, l := l_1 }) = (s = s_1 ∧ l = l_1)
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.valuation.eq_1 : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]), x.valuation = (↑x).valuation.toNat
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.Pattern.mk.inj : ∀ {A : Type u_1} {G : Type u_2} {inst : Inhabited A} {config : G → A} {support : Finset G}
  {condition : ∀ g ∉ support, config g = default} {config_1 : G → A} {support_1 : Finset G}
  {condition_1 : ∀ g ∉ support_1, config_1 g = default},
  { config := config, support := support, condition := condition } =
      { config := config_1, support := support_1, condition := condition_1 } →
    config = config_1 ∧ support = support_1
-- Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Ideal.mem_minimalPrimes_sup : ∀ {R : Type u_2} [inst : CommRing R] {p I J : Ideal R} [p.IsPrime],
  I ≤ p →
    Ideal.map (Ideal.Quotient.mk I) p ∈ (Ideal.map (Ideal.Quotient.mk I) J).minimalPrimes → p ∈ (I ⊔ J).minimalPrimes
-- Mathlib.NumberTheory.LSeries.Basic
/-- This states that the L-series of the sequence `f` converges absolutely at `s` and that
the value there is `a`.  -/
LSeriesHasSum : (ℕ → ℂ) → ℂ → ℂ → Prop
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.filter_equiv_self_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Bool},
  (Std.DHashMap.filter f m).Equiv m ↔ ∀ (k : α) (h : k ∈ m), f (m.getKey k h) (Std.DHashMap.Const.get m k h) = true
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.biprodXIso_hom_snd : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (K L : HomologicalComplex C c)
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] (i : ι),
  CategoryTheory.CategoryStruct.comp (K.biprodXIso L i).hom CategoryTheory.Limits.biprod.snd =
    CategoryTheory.Limits.biprod.snd.f i
-- Mathlib.RingTheory.Valuation.ValuationRing
PreValuationRing.cond : ∀ {A : Type u} [inst : Mul A] [PreValuationRing A] (a b : A), ∃ c, a * c = b ∨ b * c = a
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- Continuous linear equivalence between continuous linear functions `𝕜ⁿ → E` and `Eⁿ`.
The spaces `𝕜ⁿ` and `Eⁿ` are represented as `ι → 𝕜` and `ι → E`, respectively,
where `ι` is a finite type.  -/
ContinuousLinearEquiv.piRing : {𝕜 : Type u} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type v} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          [CompleteSpace 𝕜] → (ι : Type u_1) → [Fintype ι] → [DecidableEq ι] → ((ι → 𝕜) →L[𝕜] E) ≃L[𝕜] ι → E
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.comp_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Semiring C] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R C]
  [inst_7 : CoalgebraStruct R A] [inst_8 : CoalgebraStruct R B] [inst_9 : CoalgebraStruct R C] (φ₁ : B →ₐc[R] C)
  (φ₂ : A →ₐc[R] B) (x : A), (φ₁.comp φ₂) x = φ₁ (φ₂ x)
-- Mathlib.LinearAlgebra.FreeProduct.Basic
/-- Multiplication in the free product of the injections of any two `aᵢ aᵢ': A i` for
the same `i` is just the injection of multiplication `aᵢ * aᵢ'` in `A i`.  -/
LinearAlgebra.FreeProduct.mul_injections : ∀ {I : Type u} [inst : DecidableEq I] {i : I} (R : Type v) [inst_1 : CommSemiring R] (A : I → Type w)
  [inst_2 : (i : I) → Semiring (A i)] [inst_3 : (i : I) → Algebra R (A i)] (a₁ a₂ : A i),
  (LinearAlgebra.FreeProduct.ι' R A) ((DirectSum.lof R I A i) a₁) *
      (LinearAlgebra.FreeProduct.ι' R A) ((DirectSum.lof R I A i) a₂) =
    (LinearAlgebra.FreeProduct.ι' R A) ((DirectSum.lof R I A i) (a₁ * a₂))
-- Mathlib.Data.Set.Sigma
Sigma.map.eq_1 : ∀ {α₁ : Type u_2} {α₂ : Type u_3} {β₁ : α₁ → Type u_5} {β₂ : α₂ → Type u_6} (f₁ : α₁ → α₂)
  (f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)) (x : Sigma β₁), Sigma.map f₁ f₂ x = ⟨f₁ x.fst, f₂ x.fst x.snd⟩
-- Init.Data.UInt.Lemmas
UInt64.toNat_ofNat_of_lt : ∀ {n : ℕ}, n < UInt64.size → UInt64.toNat (OfNat.ofNat n) = n
-- Mathlib.Data.List.Destutter
/-- `destutter ≠` has length monotone under `List.cons`.  -/
List.length_destutter_ne_le_length_destutter_cons : ∀ {α : Type u_1} {l : List α} {a : α} [inst : DecidableEq α],
  (List.destutter (fun x1 x2 => x1 ≠ x2) l).length ≤ (List.destutter (fun x1 x2 => x1 ≠ x2) (a :: l)).length
-- Mathlib.RingTheory.Ideal.Operations
Ideal.bot_pow : ∀ {R : Type u} [inst : Semiring R] {n : ℕ}, n ≠ 0 → ⊥ ^ n = ⊥
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
/-- If `F₁` and `F₂` are functors `J ⥤ C`, and `G : K ⥤ J`,
then this is the induced morphism
`enrichedHom V F₁ F₂ ⟶ enrichedHom V (G ⋙ F₁) (G ⋙ F₂)` in `V`
when `C` is a category enriched in `V`.  -/
CategoryTheory.Enriched.FunctorCategory.precompEnrichedHom : (V : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} C] →
          {J : Type u₃} →
            [inst_3 : CategoryTheory.Category.{v₃, u₃} J] →
              {K : Type u₄} →
                [inst_4 : CategoryTheory.Category.{v₄, u₄} K] →
                  [inst_5 : CategoryTheory.EnrichedOrdinaryCategory V C] →
                    (F₁ F₂ : CategoryTheory.Functor J C) →
                      (G : CategoryTheory.Functor K J) →
                        [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] →
                          [inst_7 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V (G.comp F₁) (G.comp F₂)] →
                            CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₂ ⟶
                              CategoryTheory.Enriched.FunctorCategory.enrichedHom V (G.comp F₁) (G.comp F₂)
-- Mathlib.LinearAlgebra.Finsupp.Supported
Finsupp.disjoint_supported_supported_iff : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Nontrivial M] {s t : Set α}, Disjoint (Finsupp.supported M R s) (Finsupp.supported M R t) ↔ Disjoint s t
-- Aesop.Tree.Data
Aesop.Rapp.forSubgoalsM : {m : Type → Type} → [Monad m] → [MonadLiftT (ST IO.RealWorld) m] → (Aesop.GoalRef → m Unit) → Aesop.Rapp → m Unit
-- Init.Data.Array.Lemmas
Array.back?_eq_getElem? : ∀ {α : Type u_1} {xs : Array α}, xs.back? = xs[xs.size - 1]?
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.toList_rii : ∀ {α : Type u} {β : Type v} (t : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.Slice.toList (Std.Rii.Sliceable.mkSlice t *...*) = Std.DTreeMap.Internal.Impl.Const.toList t
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.inv_hom_apply : ∀ {X Y : GrpCat} (e : X ≅ Y) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
-- Std.Async.Basic
Std.Async.MonadAwait.mk : {t m : Type → Type} → ({α : Type} → t α → m α) → Std.Async.MonadAwait t m
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.toProd_apply_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] (x : N),
  Monoid.Coprod.toProd (Monoid.Coprod.inr x) = (1, x)
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- The integral `PowerBasis` of `𝓞 K` given by a primitive root of unity, where `K` is a `p ^ k`
cyclotomic extension of `ℚ`.  -/
IsPrimitiveRoot.integralPowerBasisOfPrimePow : {p k : ℕ} →
  {K : Type u} →
    [inst : Field K] →
      {ζ : K} →
        [hp : Fact (Nat.Prime p)] →
          [inst_1 : CharZero K] →
            [IsCyclotomicExtension {p ^ k} ℚ K] →
              IsPrimitiveRoot ζ (p ^ k) → PowerBasis ℤ (NumberField.RingOfIntegers K)
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.Monic.ne_zero_of_C : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R] {c : R}, (Polynomial.C c).Monic → c ≠ 0
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.toBitVec_eq_of_parseFirstByte_eq_threeMore : ∀ {b : UInt8},
  ByteArray.utf8DecodeChar?.parseFirstByte b = ByteArray.utf8DecodeChar?.FirstByte.threeMore →
    b.toBitVec = 30#5 ++ BitVec.setWidth 3 b.toBitVec
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.kerProj_of : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {A : Type u_4} [inst_2 : CommRing A]
  [inst_3 : Algebra R A] [inst_4 : Algebra R S] {f : S →ₐ[R] A} (hf : Function.Surjective ⇑f) (x : S),
  (AdicCompletion.kerProj hf) ((AdicCompletion.of (RingHom.ker f) S) x) = f x
-- Init.Data.List.Erase
_private.Init.Data.List.Erase.0.List.eraseIdx.match_1.splitter : {α : Type u_1} →
  (motive : List α → ℕ → Sort u_2) →
    (x : List α) →
      (x_1 : ℕ) →
        ((x : ℕ) → motive [] x) →
          ((head : α) → (as : List α) → motive (head :: as) 0) →
            ((a : α) → (as : List α) → (n : ℕ) → motive (a :: as) n.succ) → motive x x_1