mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.natDegree_polynomial : ∀ {R : Type r} [inst : CommRing R] {W : WeierstrassCurve.Affine R} [Nontrivial R], W.polynomial.natDegree = 2
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
CategoryTheory.PreGaloisCategory.toAutHomeo_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.GaloisCategory C] {G : Type u_1} [inst_2 : Group G]
  [inst_3 : (X : C) → MulAction G (F.obj X).obj] [inst_4 : CategoryTheory.PreGaloisCategory.FiberFunctor F]
  [inst_5 : TopologicalSpace G] [inst_6 : IsTopologicalGroup G] [inst_7 : CompactSpace G]
  [inst_8 : CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G] (g : G),
  (CategoryTheory.PreGaloisCategory.toAutHomeo F G) g = (CategoryTheory.PreGaloisCategory.toAut F G) g
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.normalize_apply : ∀ {α : Type u_1} {f : α → ENNReal} (hf0 : tsum f ≠ 0) (hf : tsum f ≠ ⊤) (a : α),
  (PMF.normalize f hf0 hf) a = f a * (∑' (x : α), f x)⁻¹
-- Mathlib.Topology.Algebra.Group.Torsor
Homeomorph.vaddConst_apply : ∀ {V : Type u_1} {P : Type u_2} [inst : AddGroup V] [inst_1 : TopologicalSpace V] [inst_2 : AddTorsor V P]
  [inst_3 : TopologicalSpace P] [inst_4 : IsTopologicalAddTorsor P] (p : P) (v : V), (Homeomorph.vaddConst p) v = v +ᵥ p
-- Mathlib.Algebra.Order.Ring.IsNonarchimedean
/-- **Alias** of `IsNonarchimedean.apply_intCast_le_one`.

---

If `f` is a nonarchimedean additive group seminorm on `α` with `f 1 = 1`, then for every `n : ℤ`
we have `f n ≤ 1`.  -/
IsNonarchimedean.apply_intCast_le_one_of_isNonarchimedean : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {F : Type u_2} {α : Type u_3}
  [inst_3 : AddGroupWithOne α] [inst_4 : FunLike F α R] [AddGroupSeminormClass F α R] [OneHomClass F α R] {f : F},
  IsNonarchimedean ⇑f → ∀ {n : ℤ}, f ↑n ≤ 1
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.IterM.forIn_filterWithPostcondition : ∀ {α : Type u₁} {n : Type u₁ → Type u_1} {o : Type u₁ → Type u_2} {γ : Type u₁} {m : Type u₁ → Type u_3} {β : Type u₁}
  {ps : Std.Do.PostShape} [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Monad o]
  [LawfulMonad o] [inst_6 : Std.Do.WPMonad o ps] [inst_7 : MonadLiftT m n] [LawfulMonadLiftT m n]
  [inst_9 : MonadLiftT n o] [LawfulMonadLiftT n o] [inst_11 : Std.Iterator α m β] [Std.Iterators.Finite α m]
  [inst_13 : Std.IteratorLoop α m o] [Std.LawfulIteratorLoop α m o] {it : Std.IterM m β}
  {f : β → Std.Iterators.PostconditionT n (ULift.{u₁, 0} Bool)} {init : γ} {g : β → γ → o (ForInStep γ)}
  {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond γ ps},
  ⦃P⦄
      forIn it init fun out acc => do
        let __do_lift ← liftM (f out).run
        if __do_lift.down = true then g out acc else pure (ForInStep.yield acc) ⦃Q⦄ →
    ⦃P⦄ forIn (Std.IterM.filterWithPostcondition f it) init g ⦃Q⦄
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- **The (little) ℓᵖ space**: The additive subgroup of a type synonym of `Π i, E i`, which consists
of those functions `f` such that `Memℓp f p` (i.e., `f` has finite `p`-norm).

The non-dependent version comes equipped with the notation `ℓ^p(ι, E)` in the `lp` namespace. When
`p` takes the values `0`, `1` or `2`, the notation `ℓ⁰(ι, E)`, `ℓ¹(ι, E)`, `ℓ²(ι, E)` is also
available.  -/
lp.«termℓ^_(_,_)» : Lean.ParserDescr
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- The `0` power series is the unique power series with infinite order.  -/
MvPowerSeries.order_eq_top_iff : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {f : MvPowerSeries σ R}, f.order = ⊤ ↔ f = 0
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.instSecondCountableOpens : ∀ {α : Type u_2} [inst : TopologicalSpace α] [SecondCountableTopology α] (U : TopologicalSpace.Opens α),
  SecondCountableTopology ↥U
-- Std.Sync.Channel
Std.CloseableChannel.instHashableError.hash : Std.CloseableChannel.Error → UInt64
-- Mathlib.Topology.Constructions
Topology.IsOpenEmbedding.restrict : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsOpenEmbedding f →
    ∀ {s : Set X} {t : Set Y} (H : Set.MapsTo f s t), IsOpen s → Topology.IsOpenEmbedding (Set.MapsTo.restrict f s t H)
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.IsVonNBounded.vadd : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E] [ContinuousAdd E] {s : Set E},
  Bornology.IsVonNBounded 𝕜 s → ∀ (x : E), Bornology.IsVonNBounded 𝕜 (x +ᵥ s)
-- Mathlib.Analysis.Meromorphic.LogDeriv
/-- The logarithmic derivative converts products into sums: away from a codiscrete subset of `𝕜`, the
logarithmic derivative of a finite product of meromorphic functions is the sum of the logarithmic
derivatives.
 -/
Meromorphic.logDeriv_finprod_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {ι : Type u_3} {F : ι → 𝕜 → 𝕜'},
  (Function.mulSupport F).Finite →
    (∀ (i : ι), Meromorphic (F i)) →
      (∀ (i : ι) (x : 𝕜), meromorphicOrderAt (F i) x ≠ ⊤) →
        logDeriv (∏ᶠ (i : ι), F i) =ᶠ[Filter.codiscrete 𝕜] ∑ᶠ (i : ι), logDeriv (F i)
-- Lean.Meta.Tactic.Util
/-- Collect nondependent hypotheses that are propositions.  -/
Lean.MVarId.getNondepPropHyps : Lean.MVarId → Lean.MetaM (Array Lean.FVarId)
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.smul_vec3 : ∀ {α : Type u} {R : Type u_1} [inst : SMul R α] (x : R) (a₀ a₁ a₂ : α), x • ![a₀, a₁, a₂] = ![x • a₀, x • a₁, x • a₂]
-- Init.Conv
/-- Puts term in normal form, this tactic is meant for debugging purposes only.  -/
Lean.Parser.Tactic.Conv.reduce : Lean.ParserDescr
-- Mathlib.Order.Atoms
/-- A simple `BoundedOrder` is also complete.  -/
IsSimpleOrder.completeLattice : {α : Type u_2} → [inst : Lattice α] → [inst_1 : BoundedOrder α] → [IsSimpleOrder α] → CompleteLattice α
-- Mathlib.Algebra.Category.Ring.Limits
RingCat.forget₂SemiRing_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ RingCat SemiRingCat)
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.SL2_inv_expl : ∀ {R : Type v} [inst : CommRing R] (A : Matrix.SpecialLinearGroup (Fin 2) R),
  A⁻¹ = ⟨![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]], ⋯⟩
-- Lean.Meta.Tactic.FunIndCollect
Lean.Meta.FunInd.Call : Type
-- Mathlib.GroupTheory.Sylow
IsPGroup.le_sylow_of_normal : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {N : Subgroup G} [N.Normal], IsPGroup p ↥N → ∀ (H : Sylow p G), N ≤ ↑H
-- Mathlib.Analysis.Complex.Trigonometric
/-- Extension for the `positivity` tactic: `Real.cosh` is always positive.  -/
Mathlib.Meta.Positivity.evalCosh : Mathlib.Meta.Positivity.PositivityExt
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getEntry!.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) [inst_1 : Inhabited ((a : α) × β a)] (a_1 : α) (b : β a_1)
  (es : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.getEntry! a (Std.DHashMap.Internal.AssocList.cons a_1 b es) =
    if (a_1 == a) = true then ⟨a_1, b⟩ else Std.DHashMap.Internal.AssocList.getEntry! a es
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
/-- Given a property of objects `P` for a pseudofunctor from `B` to `Cat`, this is
the induced pseudofunctor which sends `X : B` to the full subcategory of `F.obj X`
consisting of objects satisfying `P`.  -/
CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat} →
      (P : F.ObjectProperty) → [P.IsClosedUnderMapObj] → CategoryTheory.Pseudofunctor B CategoryTheory.Cat
-- Lean.Elab.MutualInductive
Lean.Elab.Command.inductive.autoPromoteIndices : Lean.Option Bool
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.postMap_app : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : T} {F G : CategoryTheory.Functor T D} (e : F ⟶ G) (Y : CategoryTheory.Under X),
  (CategoryTheory.Under.postMap e).app Y = CategoryTheory.Under.homMk (e.app Y.right) ⋯
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
CategoryTheory.CostructuredArrow.grothendieckProj_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (L : CategoryTheory.Functor C D) {X Y : CategoryTheory.Grothendieck (CategoryTheory.CostructuredArrow.functor L)}
  (f : X ⟶ Y), (CategoryTheory.CostructuredArrow.grothendieckProj L).map f = f.fiber.left
-- Mathlib.Algebra.Homology.ShortComplex.ShortExact
CategoryTheory.ShortComplex.ShortExact.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C},
  S.Exact → ∀ [mono_f : CategoryTheory.Mono S.f] [epi_g : CategoryTheory.Epi S.g], S.ShortExact
-- Mathlib.Algebra.Group.ULift
ULift.addSemigroup.eq_1 : ∀ {α : Type u} [inst : AddSemigroup α], ULift.addSemigroup = Function.Injective.addSemigroup ⇑AddEquiv.ulift ⋯ ⋯
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.whiskerLeft_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y : CategoryTheory.AddMon C} (f : X ⟶ Y) (Z : CategoryTheory.AddMon C),
  (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z).hom =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom Z.X
-- Mathlib.LinearAlgebra.BilinearForm.Hom
/-- Apply a linear map to the left argument of a bilinear form.  -/
LinearMap.BilinForm.compLeft : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → LinearMap.BilinForm R M → (M →ₗ[R] M) → LinearMap.BilinForm R M
-- Mathlib.Data.Nat.Factorization.Basic
/-- An upper bound on `n.factorization p`  -/
Nat.factorization_le_of_le_pow : ∀ {n p b : ℕ}, n ≤ p ^ b → n.factorization p ≤ b
-- Mathlib.MeasureTheory.Measure.OpenPos
IsClosed.measure_eq_univ_iff_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure]
  {F : Set X} [OpensMeasurableSpace X] [MeasureTheory.IsFiniteMeasure μ], IsClosed F → (μ F = μ Set.univ ↔ F = Set.univ)
-- Lean.Environment
_private.Lean.Environment.0.Lean.AsyncConsts.revList : Lean.AsyncConsts✝ → List Lean.AsyncConst✝
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.add_coe_eq_bot_iff : ∀ {α : Type u} [inst : Add α] {x : WithBot α} {b : α}, x + ↑b = ⊥ ↔ x = ⊥
-- Mathlib.Order.Closure
ClosureOperator.closure_sup_closure : ∀ {α : Type u_1} [inst : SemilatticeSup α] (c : ClosureOperator α) (x y : α), c (c x ⊔ c y) = c (x ⊔ y)
-- Mathlib.Probability.Moments.CovarianceBilinDual
ProbabilityTheory.uncenteredCovarianceBilinDual_of_not_memLp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E}
  [inst_1 : NormedSpace ℝ E] [inst_2 : OpensMeasurableSpace E],
  ¬MeasureTheory.MemLp id 2 μ →
    ∀ (L₁ L₂ : StrongDual ℝ E), ((ProbabilityTheory.uncenteredCovarianceBilinDual μ) L₁) L₂ = 0
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.add_apply : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddZeroClass (β i)] (g₁ g₂ : Π₀ (i : ι), β i) (i : ι),
  (g₁ + g₂) i = g₁ i + g₂ i
-- Init.Prelude
/-- Source information that relates syntax to the context that it came from.

The primary purpose of `SourceInfo` is to relate the output of the parser and the macro expander to
the original source file. When produced by the parser, `Syntax.node` does not carry source info; the
parser associates it only with atoms and identifiers. If a `Syntax.node` is introduced by a
quotation, then it has synthetic source info that both associates it with an original reference
position and indicates that the original atoms in it may not originate from the Lean file under
elaboration.

Source info is also used to relate Lean's output to the internal data that it represents; this is
the basis for many interactive features. When used this way, it can occur on `Syntax.node` as well.
 -/
Lean.SourceInfo : Type
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.instDecidableRelRelDown.eq_1 : ∀ (α : Type u_1) [inst : AddRightCancelSemigroup α] [inst_1 : DecidableEq α] [inst_2 : One α],
  ComplexShape.instDecidableRelRelDown α = id inferInstance
-- Mathlib.Algebra.Notation.Defs
/-- `a /ₛ b` computes the quotient of `a` and `b`. The meaning of this notation is
type-dependent, but it is intended to be used for multiplicative torsors. 

Conventions for notations in identifiers:

 * The recommended spelling of `/ₛ` in identifiers is `sdiv`. -/
«term_/ₛ_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
/-- The obvious map `Cofork f g → Fork f.op g.op`  -/
CategoryTheory.Limits.Cofork.op : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → {f g : X ⟶ Y} → CategoryTheory.Limits.Cofork f g → CategoryTheory.Limits.Fork f.op g.op
-- Mathlib.Algebra.Group.Action.Basic
invOf_smul_eq_iff : ∀ {α : Type u_5} {β : Type u_6} [inst : Monoid α] [inst_1 : MulAction α β] {c : α} {x y : β} [inst_2 : Invertible c],
  ⅟c • x = y ↔ x = c • y
-- Mathlib.Algebra.Order.Module.Defs
strictAnti_smul_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [PosSMulStrictMono α β], a < 0 → StrictAnti fun x => a • x
-- Lean.Meta.Tactic.Util
Lean.Meta.TacticResultCNM : Type
-- Mathlib.LinearAlgebra.Multilinear.DirectSum
MultilinearMap.fromDirectSumEquiv.congr_simp : ∀ {R : Type u_1} {ι : Type u_2} {M' : Type u_3} {κ : ι → Type u_4} {M : (i : ι) → κ i → Type u_5}
  [inst : CommSemiring R] [inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)]
  [inst_2 : (i : ι) → (j : κ i) → Module R (M i j)] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M']
  [inst_5 : DecidableEq ι] [inst_6 : Finite ι], MultilinearMap.fromDirectSumEquiv = MultilinearMap.fromDirectSumEquiv
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.mem_insertMany_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List (α × β)} {k : α},
      k ∈ Std.DHashMap.Raw.Const.insertMany m l ↔ k ∈ m ∨ (List.map Prod.fst l).contains k = true
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.exists_get?_of_mem : ∀ {α : Type u} {s : Stream'.WSeq α} {a : α}, a ∈ s → ∃ n, some a ∈ s.get? n
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Limits.IsZero.hasZeroObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C},
  CategoryTheory.Limits.IsZero X → CategoryTheory.Limits.HasZeroObject C
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.OneCocycle.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {G : CategoryTheory.Functor Cᵒᵖ GrpCat} {I : Type w'}
  {U : I → C} {toOneCochain : CategoryTheory.PresheafOfGroups.OneCochain G U}
  {ev_trans :
    autoParam
      (∀ (i j k : I) ⦃T : C⦄ (a : T ⟶ U i) (b : T ⟶ U j) (c : T ⟶ U k),
        toOneCochain.ev i j a b * toOneCochain.ev j k b c = toOneCochain.ev i k a c)
      CategoryTheory.PresheafOfGroups.OneCocycle.ev_trans._autoParam}
  {toOneCochain_1 : CategoryTheory.PresheafOfGroups.OneCochain G U}
  {ev_trans_1 :
    autoParam
      (∀ (i j k : I) ⦃T : C⦄ (a : T ⟶ U i) (b : T ⟶ U j) (c : T ⟶ U k),
        toOneCochain_1.ev i j a b * toOneCochain_1.ev j k b c = toOneCochain_1.ev i k a c)
      CategoryTheory.PresheafOfGroups.OneCocycle.ev_trans._autoParam},
  { toOneCochain := toOneCochain, ev_trans := ev_trans } = { toOneCochain := toOneCochain_1, ev_trans := ev_trans_1 } →
    toOneCochain = toOneCochain_1
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.measurableSet_support : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {m : MeasurableSpace α} [inst : Zero β] [inst_1 : TopologicalSpace β]
  [TopologicalSpace.MetrizableSpace β], MeasureTheory.StronglyMeasurable f → MeasurableSet (Function.support f)
-- Mathlib.Order.RelSeries
RelSeries.singleton_length : ∀ {α : Type u_1} (r : SetRel α α) (a : α), (RelSeries.singleton r a).length = 0
-- Mathlib.Logic.Encodable.Basic
Directed.rel_sequence : ∀ {α : Type u_1} {β : Type u_2} [inst : Encodable α] [inst_1 : Inhabited α] {r : β → β → Prop} {f : α → β}
  (hf : Directed r f) (a : α), r (f a) (f (Directed.sequence f hf (Encodable.encode a + 1)))
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.coequalizer.desc.congr_simp : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasCoequalizer f g] {W : C} (k k_1 : Y ⟶ W) (e_k : k = k_1)
  (h : CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k),
  CategoryTheory.Limits.coequalizer.desc k h = CategoryTheory.Limits.coequalizer.desc k_1 ⋯
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.prod_prod_apply_embedding : ∀ {n : ℕ} {A : Type u_1} [inst : CommMonoid A] (a : Fin n → A) (x : Composition n),
  ∏ i, ∏ j, a ((x.embedding i) j) = ∏ i, a i
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Copy.isContained : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (f : G.Copy H), G.IsContained H
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {f : (a : α) → β a → Bool} {k fallback : α} (h : m.WF),
  (Std.DHashMap.Raw.filter f m).getKeyD k fallback = ((m.getKey? k).pfilter fun x h' => f x (m.get x ⋯)).getD fallback
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α} {fallback : γ k},
  m.WF → (Std.DHashMap.Raw.filterMap f m).getD k fallback = ((m.get? k).bind (f k)).getD fallback
-- Batteries.Data.List.Perm
List.subperm_nil : ∀ {α : Type u_1} {l : List α}, l.Subperm [] ↔ l = []
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.instSemilatticeInfFiniteIndexNormalAddSubgroup.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G],
  FiniteIndexNormalAddSubgroup.instSemilatticeInfFiniteIndexNormalAddSubgroup =
    Function.Injective.semilatticeInf SetLike.coe ⋯ ⋯ ⋯ ⋯
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.BodyState.fixed.sizeOf_spec : ∀ (remaining : ℕ), sizeOf (Std.Http.Protocol.H1.Reader.BodyState.fixed remaining) = 1 + sizeOf remaining
-- Mathlib.Analysis.Asymptotics.ExpGrowth
Eventually.le_expGrowthInf : ∀ {u : ℕ → ENNReal} {a : EReal}, (∀ᶠ (n : ℕ) in Filter.atTop, (a * ↑n).exp ≤ u n) → a ≤ ExpGrowth.expGrowthInf u
-- Std.Time.Format.Modifier
Std.Time.Modifier.d.inj : ∀ {presentation presentation_1 : Std.Time.Number},
  Std.Time.Modifier.d presentation = Std.Time.Modifier.d presentation_1 → presentation = presentation_1
-- Mathlib.Order.Category.FinBoolAlg
FinBoolAlg.largeCategory : CategoryTheory.LargeCategory FinBoolAlg
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsSlice.sep_apply_eq : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Add (M i)] {s : Set ((i : ι) → M i)},
  IsSlice✝ s → ∀ (i : ι) (a : M i), IsSlice✝ {x | x ∈ s ∧ x i = a}
-- Mathlib.Data.Set.Lattice
Set.biUnion_le : ∀ {α : Type u_1} {ι : Type u_12} [inst : PartialOrder ι] (s : ι → Set α) (i : ι),
  ⋃ j, ⋃ (_ : j ≤ i), s j = (⋃ j, ⋃ (_ : j < i), s j) ∪ s i
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The identity 1-morphism `𝟙 a`.  -/
Mathlib.Tactic.BicategoryLike.NormalizedHom.nil : Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Obj → Mathlib.Tactic.BicategoryLike.NormalizedHom
-- Mathlib.CategoryTheory.Equivalence.Symmetry
CategoryTheory.Equivalence.symmEquiv_unitIso : ∀ (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],
  (CategoryTheory.Equivalence.symmEquiv C D).unitIso =
    CategoryTheory.NatIso.ofComponents (fun e => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (C ≌ D)).obj e)) ⋯
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureInformation.mk.inj : ∀ {label : String} {documentation? : Option Lean.Lsp.MarkupContent}
  {parameters? : Option (Array Lean.Lsp.ParameterInformation)} {activeParameter? : Option ℕ} {label_1 : String}
  {documentation?_1 : Option Lean.Lsp.MarkupContent} {parameters?_1 : Option (Array Lean.Lsp.ParameterInformation)}
  {activeParameter?_1 : Option ℕ},
  { label := label, documentation? := documentation?, parameters? := parameters?,
        activeParameter? := activeParameter? } =
      { label := label_1, documentation? := documentation?_1, parameters? := parameters?_1,
        activeParameter? := activeParameter?_1 } →
    label = label_1 ∧
      documentation? = documentation?_1 ∧ parameters? = parameters?_1 ∧ activeParameter? = activeParameter?_1
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.neg_le_neg : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddCommGroup M]
  [inst_2 : PartialOrder M] [IsOrderedAddMonoid M] [inst_4 : IsTopologicalAddGroup M]
  (v w : MeasureTheory.VectorMeasure α M) {i : Set α},
  MeasurableSet i → v.restrict i ≤ w.restrict i → (-w).restrict i ≤ (-v).restrict i
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
IsAddCyclic.image_range_addOrderOf : ∀ {α : Type u_1} {a : α} [inst : AddGroup α] [inst_1 : Fintype α] [inst_2 : DecidableEq α],
  (∀ (x : α), x ∈ AddSubgroup.zmultiples a) → Finset.image (fun i => i • a) (Finset.range (addOrderOf a)) = Finset.univ
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerRightIso_inv : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c),
  (CategoryTheory.Bicategory.whiskerRightIso η h).inv = CategoryTheory.Bicategory.whiskerRight η.inv h
-- Mathlib.Computability.RecursiveIn
Nat.RecursiveIn.of_eq_tot : ∀ {f : ℕ →. ℕ} {g : ℕ → ℕ} {O : Set (ℕ →. ℕ)}, Nat.RecursiveIn O f → (∀ (n : ℕ), g n ∈ f n) → Nat.RecursiveIn O ↑g
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.map_eq_span_zeta_sub_one_pow : ∀ (p k : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))),
  Ideal.map (algebraMap ℤ (NumberField.RingOfIntegers K)) (Ideal.span {↑p}) =
    Ideal.span {hζ.toInteger - 1} ^ Module.finrank ℚ K
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.p₁₂_p₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃),
  CategoryTheory.CategoryStruct.comp h.p₁₂ h₁₂.p₂ = h.p₂
-- Mathlib.Order.Concept
Concept.le_ofAttributes_iff : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {t : Set β} {c : Concept α β r},
  c ≤ Concept.ofAttributes r t ↔ t ⊆ c.intent
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.instCofibrationUnopOfFibrationOpposite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  {X Y : Cᵒᵖ} (f : X ⟶ Y) [HomotopicalAlgebra.Fibration f], HomotopicalAlgebra.Cofibration f.unop