mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.ContinuousMap.CocompactMap
CocompactMap.comp_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] (f : CocompactMap β γ) (g : CocompactMap α β) (a : α), (f.comp g) a = f (g a)
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.ElementaryEmbedding.instFunLike : {L : FirstOrder.Language} →
  {M : Type u_1} →
    {N : Type u_2} → [inst : L.Structure M] → [inst_1 : L.Structure N] → FunLike (L.ElementaryEmbedding M N) M N
-- Mathlib.Logic.Equiv.Prod
Equiv.prodUnique_apply : ∀ {α : Type u_9} {β : Type u_10} [inst : Unique β] (x : α × β), (Equiv.prodUnique α β) x = x.1
-- Mathlib.FieldTheory.Finite.GaloisField
FiniteField.splits_X_pow_card_sub_X : ∀ (p : ℕ) [h_prime : Fact (Nat.Prime p)] {K : Type u_1} [inst : Field K] [inst_1 : Fintype K]
  [inst_2 : Algebra (ZMod p) K],
  (Polynomial.map (algebraMap (ZMod p) K) (Polynomial.X ^ Fintype.card K - Polynomial.X)).Splits
-- Init.Data.String.Basic
String.get!_eq_get : ∀ (s : String) (p : String.Pos.Raw), String.Pos.Raw.get! s p = String.Pos.Raw.get s p
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
/-- The cocone corresponding to `F.ColimitType`.  -/
CategoryTheory.Functor.coconeTypes : {J : Type u} → [inst : CategoryTheory.Category.{v, u} J] → (F : CategoryTheory.Functor J (Type w₀)) → F.CoconeTypes
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.j_of_isCharTwoJNeZeroNF_of_char_two : ∀ {F : Type u_2} [inst : Field F] (W : WeierstrassCurve F) [inst_1 : W.IsElliptic] [W.IsCharTwoJNeZeroNF] [CharP F 2],
  W.j = 1 / W.a₆
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
/-- Constructor for paths of length `2` from two paths of length `1`.  -/
SSet.Truncated.Path.mk₂ : {n : ℕ} → {X : SSet.Truncated (n + 1)} → (p q : X.Path 1) → p.vertex 1 = q.vertex 0 → X.Path 2
-- Lean.Parser.Basic
/-- The `lineEq` parser requires that the current token is on the same line as the saved position
(see `withPosition`). This can be used to ensure that composite tokens are not "broken up" across
different lines. For example, `else if` is parsed using `lineEq` to ensure that the two tokens
are on the same line.

This parser has arity 0 - it does not capture anything.  -/
Lean.Parser.checkLineEq : optParam String "checkLineEq" → Lean.Parser.Parser
-- Mathlib.Topology.Order
continuous_of_discreteTopology : ∀ {α : Type u_1} [inst : TopologicalSpace α] [DiscreteTopology α] {β : Type u_2} [inst_2 : TopologicalSpace β]
  {f : α → β}, Continuous f
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
/-- `f` is right homotopic to `g` iff `f - g` is righthomotopic to `0`.  -/
CategoryTheory.Arrow.RightHomotopy.equivSubZero : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {u v : CategoryTheory.Arrow V} →
        {f g : u ⟶ v} → CategoryTheory.Arrow.RightHomotopy f g ≃ CategoryTheory.Arrow.RightHomotopy (f - g) 0
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_modify_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {fallback : β} {f : β → β},
  Std.DHashMap.Const.getD (Std.DHashMap.Const.modify m k f) k fallback =
    (Option.map f (Std.DHashMap.Const.get? m k)).getD fallback
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.instInhabited : {n : ℕ} → Inhabited (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- Copy of a `ContDiffMapSupportedIn` with a new `toFun` equal to the old one. Useful to fix
definitional equalities.  -/
ContDiffMapSupportedIn.copy : {E : Type u_2} →
  {F : Type u_3} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] →
          [inst_3 : NormedSpace ℝ F] →
            {n : ℕ∞} →
              {K : TopologicalSpace.Compacts E} →
                (f : ContDiffMapSupportedIn E F n K) → (f' : E → F) → f' = ⇑f → ContDiffMapSupportedIn E F n K
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.zero : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D} (self : Homotopy f g) (i j : ι),
  ¬c.Rel j i → self.hom i j = 0
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.sheafBotEquivalence_inverse_map_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (A : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {X Y : CategoryTheory.Functor Cᵒᵖ A} (f : X ⟶ Y), ((CategoryTheory.sheafBotEquivalence A).inverse.map f).hom = f
-- Mathlib.Algebra.Free
FreeMagma.pure_seq : ∀ {α β : Type u} {f : α → β} {x : FreeMagma α}, pure f <*> x = f <$> x
-- Mathlib.Algebra.Group.Action.Sigma
Sigma.instVAddAssocClassOfVAdd : ∀ {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → VAdd M (α i)]
  [inst_1 : (i : ι) → VAdd N (α i)] [inst_2 : VAdd M N] [∀ (i : ι), VAddAssocClass M N (α i)],
  VAddAssocClass M N ((i : ι) × α i)
-- Mathlib.Data.Multiset.Bind
Multiset.bind_filter : ∀ {α : Type u_1} {β : Type v} (m : Multiset α) (p : α → Prop) (f : α → Multiset β) [inst : DecidablePred p],
  (Multiset.filter p m).bind f = m.bind fun a => if p a then f a else 0
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.volume_eq_prod : ∀ (α : Type u_4) (β : Type u_5) [inst : MeasureTheory.MeasureSpace α] [inst_1 : MeasureTheory.MeasureSpace β],
  MeasureTheory.volume = MeasureTheory.volume.prod MeasureTheory.volume
-- Mathlib.Analysis.RCLike.Basic
RCLike.ext_iff : ∀ {K : Type u_1} [inst : RCLike K] {z w : K}, z = w ↔ RCLike.re z = RCLike.re w ∧ RCLike.im z = RCLike.im w
-- Mathlib.RingTheory.RingHom.Flat
RingHom.Flat.eq_1 : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S), f.Flat = Module.Flat R S
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.symm_apply_apply : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} (φ : ρ.Equiv σ) (v : V), φ.symm (φ v) = v
-- Mathlib.Algebra.Order.Monovary
Antivary.add_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : AddCommGroup β] [inst_2 : LinearOrder β]
  [IsOrderedAddMonoid β] {f : ι → α} {g₁ g₂ : ι → β}, Antivary f g₁ → Antivary f g₂ → Antivary f (g₁ + g₂)
-- Mathlib.Logic.Function.Iterate
Function.iterate_fixed : ∀ {α : Type u} {f : α → α} {x : α}, f x = x → ∀ (n : ℕ), f^[n] x = x
-- Mathlib.Algebra.Category.Grp.Ulift
/-- The universe lift for commutative groups preserves limits of arbitrary size.
 -/
CommGrpCat.uliftFunctor_preservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, u, max u v, u + 1, max (u + 1) (v + 1)} CommGrpCat.uliftFunctor
-- Init.Data.UInt.Lemmas
UInt8.add_def : ∀ (a b : UInt8), a + b = { toBitVec := a.toBitVec + b.toBitVec }
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_eq_get! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] [inst_1 : Inhabited β],
  t.WF → ∀ {a : α}, Std.DTreeMap.Internal.Impl.Const.get! t a = t.get! a
-- Mathlib.Algebra.Lie.OfAssociative
LieSubalgebra.coe_ad : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (H : LieSubalgebra R L)
  (x y : ↥H), ↑(((LieAlgebra.ad R ↥H) x) y) = ((LieAlgebra.ad R L) ↑x) ↑y
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} [inst_2 : Inhabited (β k)], k ∉ t₁ → (t₁ ∪ t₂).get! k = t₂.get! k
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
/-- Makes an `EvalConfigItem` for the structure.
Supports structures with no parameters or universes.
 -/
Lean.Elab.ConfigEval.defEvalConfigItem : Option (Lean.TSyntax `Lean.Parser.Command.docComment) →
  Option (Lean.TSyntax `Lean.Parser.Command.visibility) →
    Lean.TSyntax `Lean.Parser.Term.attrKind →
      Lean.Syntax →
        Lean.Ident →
          Lean.Ident →
            Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder →
              Lean.Elab.ConfigEval.EvalConfigItemView → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- The leading exponent of a multiseries with non-empty basis. For `ms = []` it is `⊥`.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.leadingExp : {basis_hd : ℝ → ℝ} →
  {basis_tl : Tactic.ComputeAsymptotics.Basis} →
    Tactic.ComputeAsymptotics.MultiseriesExpansion (basis_hd :: basis_tl) → WithBot ℝ
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalTraceState : Lean.Elab.Tactic.Tactic
-- Init.Prelude
/-- Create array `#[a₁, a₂, a₃, a₄, a₅, a₆, a₇, a₈]`  -/
Array.mkArray8 : {α : Type u} → α → α → α → α → α → α → α → α → Array α
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_X : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] [Nontrivial R] {s : σ},
  m.degree (MvPolynomial.X s) = fun₀ | s => 1
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Basic
/-- The complex of functors whose behaviour pointwise takes an `R`-linear `G`-representation `M`
to the complex `M → C(G, M) → ⋯ → C(G, C(G,...,C(G, M))) → ⋯`
The `G`-invariant submodules of it is the homogeneous cochains (shifted by one).  -/
TopRep.resolution : {k : Type u_1} →
  {G : Type u_2} →
    [inst : Ring k] →
      [inst_1 : Group G] →
        [inst_2 : TopologicalSpace k] →
          [inst_3 : TopologicalSpace G] → [IsTopologicalGroup G] → TopRep k G → CochainComplex (TopRep k G) ℕ
-- Mathlib.Condensed.Discrete.Colimit
/-- `lanPresheaf (locallyConstantPresheaf X)` as a light condensed set.
 -/
LightCondensed.lanLightCondSet : Type u → LightCondSet
-- Mathlib.Analysis.SumIntegralComparisons
MonotoneOn.integral_le_sum_Ico : ∀ {a b : ℕ} {f : ℝ → ℝ},
  a ≤ b → MonotoneOn f (Set.Icc ↑a ↑b) → ∫ (x : ℝ) in ↑a..↑b, f x ≤ ∑ i ∈ Finset.Ico a b, f ↑(i + 1)
-- Lean.LabelAttribute
/-- The collection of all current `LabelExtension`s, indexed by name.  -/
Lean.LabelExtensionMap : Type
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac_app : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesPointwiseLeftKanExtension F L]
  [inst_5 : L.HasPointwiseLeftKanExtension F] (a : A),
  CategoryTheory.CategoryStruct.comp (G.map ((L.pointwiseLeftKanExtensionUnit F).app a))
      ((G.pointwiseLeftKanExtensionCompIsoOfPreserves F L).hom.app (L.obj a)) =
    (L.pointwiseLeftKanExtensionUnit (F.comp G)).app a
-- Mathlib.ModelTheory.Syntax
/-- Take the disjunction of a finite set of formulas.

Note that this is an arbitrary formula defined using the axiom of choice. It is only well-defined up
to equivalence of formulas.  -/
FirstOrder.Language.BoundedFormula.iSup : {L : FirstOrder.Language} →
  {α : Type u'} → {β : Type v'} → {n : ℕ} → [Finite β] → (β → L.BoundedFormula α n) → L.BoundedFormula α n
-- Mathlib.Algebra.Module.Torsion.Basic
/-- An `S`-torsion module is a module whose `S`-torsion submodule is the full space.  -/
Submodule.isTorsion'_iff_torsion'_eq_top : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (S : Type u_3)
  [inst_3 : CommMonoid S] [inst_4 : DistribMulAction S M] [inst_5 : SMulCommClass S R M],
  Module.IsTorsion' M S ↔ Submodule.torsion' R M S = ⊤
-- Mathlib.Order.Compare
cmp_compares : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), (cmp a b).Compares a b
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.toPUnitIdEquiv_functor_iso : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A]
  {L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})}
  {R : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_2 + 1}) (CategoryTheory.Discrete PUnit.{u_1 + 1})},
  (CategoryTheory.Comma.toPUnitIdEquiv L R).functor = CategoryTheory.Comma.fst L R
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_filter!_le_size : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  {f : α → β → Bool}, t.WF → (Std.DTreeMap.Internal.Impl.filter! f t).size ≤ t.size
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int.0.Int.reduceBinIntNatOp : Lean.Name → (ℤ → ℕ → ℤ) → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.DStep
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.eqToHom_left : ∀ {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) (X Y : CategoryTheory.Comma L R) (H : X = Y),
  (CategoryTheory.eqToHom H).left = CategoryTheory.eqToHom ⋯
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- See also `div_le_div_iff` for a version that works for `LinearOrderedSemifield` with
additional assumptions.  -/
div_le_div_iff' : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : LE α] [MulLeftMono α] {a b c d : α}, a / b ≤ c / d ↔ a * d ≤ c * b
-- Mathlib.Analysis.Normed.Group.Uniform
LipschitzWith.norm_sub_le_of_le : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] {f : E → F}
  {C : NNReal} {a b : E} {r : ℝ}, LipschitzWith C f → ‖a - b‖ ≤ r → ‖f a - f b‖ ≤ ↑C * r
-- Mathlib.NumberTheory.ModularForms.Cusps
Subgroup.periods.eq_1 : ∀ {R : Type u_1} [inst : Ring R] (𝒢 : Subgroup (GL (Fin 2) R)), 𝒢.periods = 𝒢.adjoinNegOne.strictPeriods
-- Mathlib.Analysis.Analytic.Basic
/-- The sum of a converging power series is continuous in its disk of convergence.  -/
FormalMultilinearSeries.continuousOn : ∀ {𝕜 : 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]
  {p : FormalMultilinearSeries 𝕜 E F} [CompleteSpace F], ContinuousOn p.sum (Metric.eball 0 p.radius)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.extract.sizeOf_spec : ∀ {w : ℕ} (start len : ℕ) (expr : Std.Tactic.BVDecide.BVExpr w),
  sizeOf (Std.Tactic.BVDecide.BVExpr.extract start len expr) = 1 + sizeOf w + sizeOf start + sizeOf len + sizeOf expr
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
CategoryTheory.Limits.PreservesColimit₂.of_preservesColimit₂_flip : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] {K₁ : CategoryTheory.Functor J₁ C₁}
  {K₂ : CategoryTheory.Functor J₂ C₂} (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C))
  [CategoryTheory.Limits.PreservesColimit₂ K₁ K₂ G], CategoryTheory.Limits.PreservesColimit₂ K₂ K₁ G.flip
-- Mathlib.CategoryTheory.Adjunction.Mates
/-- The mates equivalence commutes with this composition, essentially by `mateEquiv_vcomp`.  -/
CategoryTheory.conjugateEquiv_mateEquiv_vcomp : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] {G : CategoryTheory.Functor A C} {H : CategoryTheory.Functor B D}
  {L₁ : CategoryTheory.Functor A B} {R₁ : CategoryTheory.Functor B A} {L₂ : CategoryTheory.Functor A B}
  {R₂ : CategoryTheory.Functor B A} {L₃ : CategoryTheory.Functor C D} {R₃ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁)
  (adj₂ : L₂ ⊣ R₂) (adj₃ : L₃ ⊣ R₃) (α : L₂ ⟶ L₁) (β : CategoryTheory.TwoSquare G L₂ L₃ H),
  (CategoryTheory.mateEquiv adj₁ adj₃) (β.whiskerLeft α) =
    ((CategoryTheory.mateEquiv adj₂ adj₃) β).whiskerTop ((CategoryTheory.conjugateEquiv adj₁ adj₂) α)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.toPullback_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {i₁ i₂ : E.I₀}
  [inst_1 : CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)] (k : E.I₁ i₁ i₂) {Z : C} (h : E.X i₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (E.toPullback k)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (E.f i₁) (E.f i₂)) h) =
    CategoryTheory.CategoryStruct.comp (E.p₂ k) h
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.dblXYZ_X : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R), W'.dblXYZ P 0 = W'.dblX P
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.instZero : {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → Zero (β i)] → Zero (Π₀ (i : ι), β i)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_eq_getElem!_keysArray : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → t.minKey! = t.keysArray[0]!
-- Mathlib.Topology.Bornology.Absorbs
absorbs_iff_eventually_cobounded_mapsTo : ∀ {G₀ : Type u_1} {α : Type u_2} [inst : GroupWithZero G₀] [inst_1 : Bornology G₀] [inst_2 : MulAction G₀ α]
  {s t : Set α}, Absorbs G₀ s t ↔ ∀ᶠ (c : G₀) in Bornology.cobounded G₀, Set.MapsTo (fun x => c⁻¹ • x) t s
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtDHashMap α β), m = m_1 → ∀ (a a_1 : α), a = a_1 → m.getKey? a = m_1.getKey? a_1
-- Mathlib.Algebra.Group.Submonoid.Support
Submonoid.mem_mulSupport : ∀ {G : Type u_1} [inst : Group G] {M : Submonoid G} {x : G}, x ∈ M.mulSupport ↔ x ∈ M ∧ x⁻¹ ∈ M
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_alter_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] [inst_2 : Inhabited α] {k : α} {f : Option (β k) → Option (β k)},
  (t.alter k f).getKey! k = if (f (t.get? k)).isSome = true then k else default
-- Mathlib.Data.FunLike.Group
FunLike.addRightCancelSemigroup.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Add F]
  [inst_2 : AddRightCancelSemigroup β] [inst_3 : IsAddApply F α β],
  FunLike.addRightCancelSemigroup = Function.Injective.addRightCancelSemigroup (fun f => ⇑f) ⋯ ⋯
-- Batteries.Data.List.Matcher
/-- Find the start and end positions of the first infix sublist of `l` matching `m.pattern`,
or `none` if there is no such sublist.
 -/
List.Matcher.find? : {α : Type u_1} → [BEq α] → List.Matcher α → List α → Option (ℕ × ℕ)
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanDeclIdent.mk.injEq : ∀ (module decl module_1 decl_1 : Lean.Name),
  ({ module := module, decl := decl } = { module := module_1, decl := decl_1 }) = (module = module_1 ∧ decl = decl_1)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Zipper.cons.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} [inst : SizeOf α] [inst_1 : (a : α) → SizeOf (β a)] (k : α) (v : β k)
  (tree : Std.DTreeMap.Internal.Impl α β) (next : Std.DTreeMap.Internal.Zipper α β),
  sizeOf (Std.DTreeMap.Internal.Zipper.cons k v tree next) = 1 + sizeOf k + sizeOf v + sizeOf tree + sizeOf next
-- Mathlib.Order.CompleteLattice.Basic
Monotone.iSup_comp_eq : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : CompleteLattice α] [inst_1 : Preorder β] {f : β → α},
  Monotone f → ∀ {s : ι → β}, (∀ (x : β), ∃ i, x ≤ s i) → ⨆ x, f (s x) = ⨆ y, f y
-- Mathlib.Order.Filter.Cofinite
Filter.cofinite_eq_bot : ∀ {α : Type u_2} [Finite α], Filter.cofinite = ⊥
-- Mathlib.Algebra.Group.AddChar
MonoidHom.compAddChar_apply : ∀ {A : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddMonoid A] [inst_1 : Monoid M] [inst_2 : Monoid N] (f : M →* N)
  (φ : AddChar A M), ⇑(f.compAddChar φ) = ⇑f ∘ ⇑φ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_inter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Inhabited α]
  [Std.TransOrd α] (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α},
      (m₁.inter m₂ ⋯).getKey! k = if Std.DTreeMap.Internal.Impl.contains k m₂ = true then m₁.getKey! k else default
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : 𝕜 → 𝕜` is continuous on a compact set `s` and `f 0 = 0` and `a : X → A` is continuous
on `t : Set X`, and `a x` satisfies the predicate `p` associated to `𝕜` and has quasispectrum
contained in `s` for all `x ∈ t`, then `fun x ↦ cfcₙ f (a x)` is continuous on `t`.  -/
ContinuousOn.cfcₙ' : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A]
  [ContinuousStar A] [inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] [inst_8 : TopologicalSpace X]
  {s : Set 𝕜},
  IsCompact s →
    ∀ (f : 𝕜 → 𝕜) {a : X → A} {t : Set X},
      ContinuousOn a t →
        (∀ x ∈ t, quasispectrum 𝕜 (a x) ⊆ s) →
          (∀ x ∈ t, p (a x)) →
            autoParam (ContinuousOn f s) ContinuousOn.cfcₙ'._auto_1 →
              autoParam (f 0 = 0) ContinuousOn.cfcₙ'._auto_3 → ContinuousOn (fun x => cfcₙ f (a x)) t
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.addCommutator_bot_left : ∀ {G : Type u_1} [inst : AddGroup G] (H₁ : AddSubgroup G), ⁅⊥, H₁⁆ = ⊥
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.lmapDomain_linearCombination : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {α' : Type u_7} {M' : Type u_8} [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] {v : α → M} {v' : α' → M'}
  (f : α → α') (g : M →ₗ[R] M'),
  (∀ (i : α), g (v i) = v' (f i)) →
    Finsupp.linearCombination R v' ∘ₗ Finsupp.lmapDomain R R f = g ∘ₗ Finsupp.linearCombination R v
-- Mathlib.Algebra.Group.Basic
zpow_one_sub_natCast : ∀ {G : Type u_3} [inst : Group G] (a : G) (n : ℕ), a ^ (1 - ↑n) = a / a ^ n
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.OplaxTrans.naturality_id_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (self : CategoryTheory.Oplax.OplaxTrans F G) (a : B) {Z : F.obj a ⟶ G.obj a}
  (h : CategoryTheory.CategoryStruct.comp (self.app a) (CategoryTheory.CategoryStruct.id (G.obj a)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.id a))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapId a)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (self.app a))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (self.app a)).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (self.app a)).inv h))