mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Star.StarAlgHom
/-- `Function.eval` as a `StarAlgHom`.  -/
Pi.evalStarAlgHom : {ι : Type u_1} →
  (R : Type u_2) →
    (A : ι → Type u_3) →
      (j : ι) →
        [inst : CommSemiring R] →
          [inst_1 : (i : ι) → Semiring (A i)] →
            [inst_2 : (i : ι) → Algebra R (A i)] → [inst_3 : (i : ι) → Star (A i)] → ((i : ι) → A i) →⋆ₐ[R] A j
-- Mathlib.MeasureTheory.VectorMeasure.WithDensityVec
MeasureTheory.VectorMeasure.withDensity_congr : ∀ {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {f g : X → E} {B : E →L[ℝ] F →L[ℝ] G},
  f =ᵐ[μ.variation] g → μ.withDensity f B = μ.withDensity g B
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.sup_limZero : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {f g : CauSeq α abs},
  f.LimZero → g.LimZero → (f ⊔ g).LimZero
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_insert_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {a fallback : α}
  {b : β a}, (t.insert a b).getKeyD a fallback = a
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithTop.sSup_of_top_mem : ∀ {α : Type u_1} [inst : LE α] [inst_1 : SupSet α] {s : Set (WithTop α)}, ⊤ ∈ s → sSup s = ⊤
-- Mathlib.Algebra.DirectSum.Algebra
Algebra.directSumGAlgebra_toFun_apply : ∀ {ι : Type uι} {R : Type u_1} {A : Type u_2} [inst : AddMonoid ι] [inst_1 : CommSemiring R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] (a : R), DirectSum.GAlgebra.toFun a = (↑↑(algebraMap R A)).toFun a
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.ext_iff : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] {x y : DirectSum ι β},
  x = y ↔ ∀ (i : ι), x i = y i
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- `incl` is fully faithful, which means that `(X ⟶ Y) ≃ (incl(X) ⟶ incl(Y))`.  -/
CategoryTheory.Limits.FormalCoproduct.fullyFaithfulIncl : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (CategoryTheory.Limits.FormalCoproduct.incl C).FullyFaithful
-- Mathlib.NumberTheory.Bertrand
/-- A refined version of the `Bertrand.main_inequality` below.
This is not best possible: it actually holds for 464 ≤ x.
 -/
Bertrand.real_main_inequality : ∀ {x : ℝ}, 512 ≤ x → x * (2 * x) ^ √(2 * x) * 4 ^ (2 * x / 3) ≤ 4 ^ x
-- Mathlib.Topology.Connected.PathConnected
/-- Every connected component is a union of path connected components  -/
biUnion_connectedComponent_pathComponent_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x : X), ⋃ y ∈ connectedComponent x, pathComponent y = connectedComponent x
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
CategoryTheory.JointlyReflectMonomorphisms.mono_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3}
  [inst_1 : (i : I) → CategoryTheory.Category.{u_5, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)},
  CategoryTheory.JointlyReflectMonomorphisms F →
    ∀ [∀ (i : I), (F i).PreservesMonomorphisms] {X Y : C} (f : X ⟶ Y),
      CategoryTheory.Mono f ↔ ∀ (i : I), CategoryTheory.Mono ((F i).map f)
-- Mathlib.Tactic.Order.ToInt
Mathlib.Tactic.Order.ToInt.toInt_inf_toInt_eq_toInt : ∀ {α : Type u_1} [inst : LinearOrder α] {n : ℕ} (val : Fin n → α) (i j k : Fin n),
  min (Mathlib.Tactic.Order.ToInt.toInt val i) (Mathlib.Tactic.Order.ToInt.toInt val j) =
      Mathlib.Tactic.Order.ToInt.toInt val k ↔
    min (val i) (val j) = val k
-- Mathlib.Order.OrderIsoNat
RelIso.ofSurjective.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f f_1 : r ↪r s) (e_f : f = f_1)
  (H : Function.Surjective ⇑f), RelIso.ofSurjective f H = RelIso.ofSurjective f_1 ⋯
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.FullyFaithful.mapGrp.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] (hF : F.FullyFaithful),
  hF.mapGrp =
    { preimage := fun {X Y} f => CategoryTheory.Grp.homMk' (hF.mapMon.preimage f.hom), map_preimage := ⋯,
      preimage_map := ⋯ }
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.smul_coe_apply : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K] (σ : Gal(K/k))
  (w : NumberField.InfinitePlace K) (x : K), ↑(SMul.smul σ w) x = ↑w (σ.symm x)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.keyAtIdx_eq_getElem_fst : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} (htb : t.Balanced) {i : ℕ} {h : i < t.size},
  t.keyAtIdx htb i h = t.toListModel[i].fst
-- Mathlib.Combinatorics.Graph.Basic
Graph.bouquet_isLink : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {e : β} (v : α) (edgeSet : Set β),
  (Graph.bouquet v edgeSet).IsLink e x y ↔ e ∈ edgeSet ∧ x = v ∧ y = v
-- Mathlib.Topology.Algebra.Module.Equiv
Fin.consEquivL_apply : ∀ {n : ℕ} (R : Type u_4) (M : Fin n.succ → Type u_5) [inst : Semiring R]
  [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : (i : Fin n.succ) → Module R (M i)]
  [inst_3 : (i : Fin n.succ) → TopologicalSpace (M i)] (a : M 0 × ((i : Fin n) → M i.succ)) (i : Fin (n + 1)),
  (Fin.consEquivL R M) a i = Fin.cons a.1 a.2 i
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.replaceFTR.go.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Array α → Sort u_2) (acc : Array α) (h_1 : (acc : Array α) → motive [] acc)
  (h_2 : (x : α) → (xs : List α) → (acc : Array α) → motive (x :: xs) acc),
  (match [], acc with
    | [], acc => h_1 acc
    | x :: xs, acc => h_2 x xs acc) =
    h_1 acc
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.compl_of_one_sub_one : ∀ (α : Type u_1) (V : Type u_2) [inst : AddGroup α] [inst_1 : One α] [inst_2 : DecidableEq V] [inst_3 : DecidableEq α],
  (Matrix.of 1 - 1).compl = 0
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.union.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t₁ t₁_1 : Std.ExtTreeSet α cmp),
  t₁ = t₁_1 → ∀ (t₂ t₂_1 : Std.ExtTreeSet α cmp), t₂ = t₂_1 → t₁.union t₂ = t₁_1.union t₂_1
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
CompactlySupportedContinuousMap.integralPositiveLinearMap.congr_simp : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [inst_2 : OpensMeasurableSpace X]
  (μ μ_1 : MeasureTheory.Measure X) (e_μ : μ = μ_1) [inst_3 : MeasureTheory.IsFiniteMeasureOnCompacts μ],
  CompactlySupportedContinuousMap.integralPositiveLinearMap μ =
    CompactlySupportedContinuousMap.integralPositiveLinearMap μ_1
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
/-- The data of a morphism `free I ⟶ M` from a free sheaf of modules is
equivalent to the data of a family `I → M.sections` of sections of `M`.  -/
SheafOfModules.freeHomEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] →
            (M : SheafOfModules R) → {I : Type u} → (SheafOfModules.free I ⟶ M) ≃ (I → M.sections)
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
CategoryTheory.Limits.IsTerminal.isIso_from : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictTerminalObjects C] {I : C}
  (hI : CategoryTheory.Limits.IsTerminal I) {A : C} (f : I ⟶ A), CategoryTheory.IsIso f
-- Batteries.Data.Fin.Coding
Fin.encodeFun.eq_2 : ∀ {n : ℕ} (m : ℕ) (f : Fin (m + 1) → Fin n), Fin.encodeFun f = ⟨n * ↑(Fin.encodeFun fun k => f k.succ) + ↑(f 0), ⋯⟩
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
MeasureTheory.Lp.norm_constL_le : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α)
  [inst : NormedAddCommGroup E] [inst_1 : MeasureTheory.IsFiniteMeasure μ] (𝕜 : Type u_3)
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : Fact (1 ≤ p)],
  ‖MeasureTheory.Lp.constL p μ 𝕜‖ ≤ μ.real Set.univ ^ (1 / p.toReal)
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v))
  (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) (X : Cᵒᵖ),
  (CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf A F).obj X =
    CategoryTheory.OverPresheafAux.YonedaCollection F (Opposite.unop X)
-- Mathlib.Algebra.Polynomial.Sequence
/-- `S i` has strictly monotone degree.  -/
Polynomial.Sequence.degree_strictMono : ∀ {R : Type u_1} [inst : Semiring R] (S : Polynomial.Sequence R), StrictMono (Polynomial.degree ∘ ↑S)
-- Mathlib.Algebra.Order.AddGroupWithTop
add_left_strictMono_of_ne_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommMonoidWithTop α] {b : α}, b ≠ ⊤ → StrictMono fun x => x + b
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_of_mem_union_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₁ ∪ m₂ → k ∉ m₁ → k ∈ m₂
-- Mathlib.NumberTheory.LSeries.HurwitzZeta
/-- Meromorphic continuation of the series `∑' (n : ℕ), exp (2 * π * I * a * n) / n ^ s`.  See
`hasSum_expZeta_of_one_lt_re` for the relation to the Dirichlet series.  -/
HurwitzZeta.expZeta : UnitAddCircle → ℂ → ℂ
-- Mathlib.Data.Nat.Cast.SetInterval
Nat.image_cast_int_Ioo : ∀ (a b : ℕ), Nat.cast '' Set.Ioo a b = Set.Ioo ↑a ↑b
-- Mathlib.Algebra.Homology.TotalComplexShift
/-- The isomorphism `((shiftFunctor₁ C x).obj K).total (up ℤ) ≅ (K.total (up ℤ))⟦x⟧`
expressing the compatibility of the total complex with the shift on the first indices.
This isomorphism does not involve signs.  -/
HomologicalComplex₂.totalShift₁Iso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) →
        (x : ℤ) →
          [inst_2 : K.HasTotal (ComplexShape.up ℤ)] →
            ((HomologicalComplex₂.shiftFunctor₁ C x).obj K).total (ComplexShape.up ℤ) ≅
              (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) x).obj
                (K.total (ComplexShape.up ℤ))
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G' : Type u_7} {G'' : Type u_8}
  [inst : NormedAddCommGroup G''] [inst_1 : PartialOrder G''] [IsOrderedAddMonoid G''] [inst_3 : NormedSpace ℝ G'']
  [inst_4 : NormedAddCommGroup G'] [inst_5 : PartialOrder G'] [IsOrderedAddMonoid G'] [inst_7 : NormedSpace ℝ G']
  {T : Set α → G' →L[ℝ] G''} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x) →
    ∀ {f g : ↥(α →₁ₛ[μ] G')},
      f ≤ g →
        (MeasureTheory.L1.SimpleFunc.setToL1SCLM α G' μ hT) f ≤ (MeasureTheory.L1.SimpleFunc.setToL1SCLM α G' μ hT) g
-- Mathlib.AlgebraicTopology.SimplicialObject.Op
/-- The functor `opFunctor : SimplicialObject C ⥤ SimplicialObject C`
as an equivalence of categories.  -/
SimplicialObject.opEquivalence : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] → CategoryTheory.SimplicialObject C ≌ CategoryTheory.SimplicialObject C
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.compProd.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ : MeasureTheory.Measure α)
  (κ : ProbabilityTheory.Kernel α β),
  μ.compProd κ = ((ProbabilityTheory.Kernel.const Unit μ).compProd (ProbabilityTheory.Kernel.prodMkLeft Unit κ)) ()
-- Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
MeasureTheory.eLpNorm_add_lt_top : ∀ {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε]
  {p : ENNReal} {μ : MeasureTheory.Measure α} {f g : α → ε},
  MeasureTheory.MemLp f p μ → MeasureTheory.MemLp g p μ → MeasureTheory.eLpNorm (f + g) p μ < ⊤
-- Mathlib.Geometry.Manifold.Notation
/-- Delaborator for `MDifferentiableOn` using the custom elaborator, and special-casing
arguments that can use the `T%` elaborator.  -/
Manifold.delabMDifferentiableOn : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Data.Stream.Init
Stream'.odd_eq : ∀ {α : Type u} (s : Stream' α), s.odd = s.tail.even
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcKeepAliveParams.uri : Lean.Lsp.RpcKeepAliveParams → Lean.Lsp.DocumentUri
-- Mathlib.Analysis.Calculus.FDeriv.WithLp
PiLp.hasStrictFDerivAt_apply : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → NormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] [Finite ι] (p : ENNReal)
  [Fact (1 ≤ p)] (f : PiLp p E) (i : ι), HasStrictFDerivAt (fun f => f.ofLp i) (PiLp.proj p E i) f
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
/-- The obvious bijection between `Πʳ i, [R i, A i]_[⊥]` and `Π i, R i` is a homeomorphism.  -/
RestrictedProduct.homeoBot : {ι : Type u_1} →
  {R : ι → Type u_2} →
    {A : (i : ι) → Set (R i)} →
      [inst : (i : ι) → TopologicalSpace (R i)] → ((i : ι) → R i) ≃ₜ RestrictedProduct (fun i => R i) (fun i => A i) ⊥
-- Mathlib.Algebra.Category.MonCat.Limits
/-- The category of additive monoids has all limits.  -/
AddMonCat.hasLimitsOfSize : ∀ [UnivLE.{v, u}], CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} AddMonCat
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.archimedeanClassMk_omega_neg : ArchimedeanClass.mk Hyperreal.omega < 0
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.min'_one : ∀ {α : Type u_2} [inst : One α] [inst_1 : LinearOrder α], Finset.min' 1 ⋯ = 1
-- Mathlib.Algebra.Group.Basic
leftInverse_inv : ∀ (G : Type u_3) [inst : InvolutiveInv G], Function.LeftInverse (fun a => a⁻¹) fun a => a⁻¹
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.mem_toNonUnitalSubalgebra : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A] {S : NonUnitalStarSubalgebra R A} {x : A}, x ∈ S.toNonUnitalSubalgebra ↔ x ∈ S
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.PullbackCone.unop_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z}
  (c : CategoryTheory.Limits.PullbackCone f g), c.unop.pt = Opposite.unop c.pt
-- Mathlib.Algebra.Group.Basic
add_left_iterate : ∀ {M : Type u_4} [inst : AddMonoid M] (a : M) (n : ℕ), (fun x => a + x)^[n] = fun x => n • a + x
-- Lean.Data.Lsp.Basic
Lean.Lsp.MarkupKind.ofNat_ctorIdx : ∀ (x : Lean.Lsp.MarkupKind), Lean.Lsp.MarkupKind.ofNat x.ctorIdx = x
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.mk_vadd_of_tower_mk : ∀ {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [inst : SetLike S α] [inst_1 : VAdd M N] [inst_2 : VAdd M α]
  [inst_3 : AddMonoid N] [inst_4 : AddAction N α] [inst_5 : VAddMemClass S N α] [inst_6 : VAddAssocClass M N α] (s : S)
  (r : M) (x : α) (hx : x ∈ s), r +ᵥ ⟨x, hx⟩ = ⟨r +ᵥ x, ⋯⟩
-- Mathlib.CategoryTheory.MorphismProperty.Ind
/-- `ind` is idempotent if `P` implies finitely presentable.  -/
CategoryTheory.MorphismProperty.ind_ind : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C},
  P ≤ CategoryTheory.MorphismProperty.isFinitelyPresentable C →
    ∀ [CategoryTheory.LocallySmall.{w, v, u} C], P.ind.ind = P.ind
-- Mathlib.Algebra.Algebra.NonUnitalHom
/-- The inverse of a bijective morphism is a morphism.  -/
NonUnitalAlgHom.inverse' : {R : Type u} →
  {S : Type u₁} →
    [inst : Monoid R] →
      [inst_1 : Monoid S] →
        {φ : R →* S} →
          {A : Type v} →
            {B : Type w} →
              [inst_2 : NonUnitalNonAssocSemiring A] →
                [inst_3 : DistribMulAction R A] →
                  [inst_4 : NonUnitalNonAssocSemiring B] →
                    [inst_5 : DistribMulAction S B] →
                      {φ' : S →* R} →
                        (f : A →ₛₙₐ[φ] B) →
                          (g : B → A) →
                            Function.RightInverse ⇑φ' ⇑φ →
                              Function.LeftInverse g ⇑f → Function.RightInverse g ⇑f → B →ₛₙₐ[φ'] A
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : MulZeroOneClass α] [inst_4 : MulZeroOneClass β] [inst_5 : MulZeroOneClass γ] {g₁ g₂ : β →*₀o γ}
  {f : α →*₀o β}, Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.sq_sqrt : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] (a : A),
  autoParam (0 ≤ a) CFC.sq_sqrt._auto_1 → CFC.sqrt a ^ 2 = a
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.Embedding.instStructureWithConstants : {L : FirstOrder.Language} →
  {M : Type u_4} →
    [inst : L.Structure M] →
      {N : Type u_3} →
        [inst_1 : L.Structure N] → (_f : L.Embedding M N) → (_A : Set M) → L.Structure (_f.withConstants _A)
-- Mathlib.Topology.DiscreteQuotient
connectedComponentSetoid.eq_1 : ∀ (α : Type u_3) [inst : TopologicalSpace α],
  connectedComponentSetoid α = { r := fun x y => connectedComponent x = connectedComponent y, iseqv := ⋯ }
-- Mathlib.Tactic.Positivity.Core
_private.Mathlib.Tactic.Positivity.Core.0.Mathlib.Meta.Positivity.OrderRel.ne'.sizeOf_spec : sizeOf Mathlib.Meta.Positivity.OrderRel.ne'✝ = 1
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.map_comp : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T)
  {Q : Type u_4} [inst_3 : AddCommMonoid Q] {k : T.LocalizationMap Q},
  (f.map hy k).comp f.toAddMonoidHom = k.toAddMonoidHom.comp g
-- Lean.Meta.Basic
/-- Return true if the given metavariable is "read-only".
That is, its `depth` is different from the current metavariable context depth.
 -/
Lean.MVarId.isReadOnly : Lean.MVarId → Lean.MetaM Bool
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_pos : ∀ {m : ℕ∞}, 0 < ↑m ↔ 0 < m
-- Init.Data.Array.Erase
Array.eraseIdx_set_gt : ∀ {α : Type u_1} {xs : Array α} {i j : ℕ} {a : α} (h : i < j) {w : j < xs.size},
  (xs.set i a ⋯).eraseIdx j ⋯ = (xs.eraseIdx j w).set i a ⋯
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
GradedTensorProduct.comm_coe_tmul_coe : ∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  [inst_9 : Module ι (Additive ℤˣ)] {i j : ι} (a : ↥(𝒜 i)) (b : ↥(ℬ j)),
  (GradedTensorProduct.comm 𝒜 ℬ) (↑a ᵍ⊗ₜ[R] ↑b) = (-1) ^ (j * i) • ↑b ᵍ⊗ₜ[R] ↑a
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.ResidueField.mapEquiv_trans : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : IsLocalRing R] [inst_2 : CommRing S]
  [inst_3 : IsLocalRing S] [inst_4 : CommRing T] [inst_5 : IsLocalRing T] (e₁ : R ≃+* S) (e₂ : S ≃+* T),
  IsLocalRing.ResidueField.mapEquiv (e₁.trans e₂) =
    (IsLocalRing.ResidueField.mapEquiv e₁).trans (IsLocalRing.ResidueField.mapEquiv e₂)
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile.0.Std.Iterators.Types.TakeWhile.instIterator.match_1.splitter : {m : Type u_1 → Type u_2} →
  {β : Type u_1} →
    {P : β → Std.Iterators.PostconditionT m (ULift.{u_1, 0} Bool)} →
      (out : β) →
        (motive : Subtype (P out).Property → Sort u_3) →
          (__do_lift : Subtype (P out).Property) →
            ((h' : (P out).Property { down := true }) → motive ⟨{ down := true }, h'⟩) →
              ((h' : (P out).Property { down := false }) → motive ⟨{ down := false }, h'⟩) → motive __do_lift
-- Mathlib.CategoryTheory.Bicategory.Coherence
CategoryTheory.FreeBicategory.normalizeIso.eq_2 : ∀ {B : Type u} [inst : Quiver B] {a : B} (x : B) (x_1 : Quiver.Path a x),
  CategoryTheory.FreeBicategory.normalizeIso x_1 (CategoryTheory.FreeBicategory.Hom.id x) =
    CategoryTheory.Bicategory.rightUnitor ((CategoryTheory.FreeBicategory.preinclusion B).map { as := x_1 })
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- `eval(F)` preserves arbitrary coproducts.  -/
CategoryTheory.Limits.FormalCoproduct.isColimitEvalMapCoconeCofan : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_2 : CategoryTheory.Limits.HasCoproducts A] →
          (J : Type w) →
            (f : J → CategoryTheory.Limits.FormalCoproduct C) →
              (F : CategoryTheory.Functor C A) →
                CategoryTheory.Limits.IsColimit
                  (((CategoryTheory.Limits.FormalCoproduct.eval C A).obj F).mapCocone
                    (CategoryTheory.Limits.FormalCoproduct.cofan J f))
-- Mathlib.Topology.EMetricSpace.PairReduction
/-- The underlying point of a `logSizeBallStruct` (typically a point in the underlying finite
set)  -/
PairReduction.logSizeBallStruct.point : {T : Type u_2} → PairReduction.logSizeBallStruct T → T
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.insertIfNew.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Raw α β) (a : α) (b : β a),
  m.insertIfNew a b = if h : 0 < m.buckets.size then ↑(Std.DHashMap.Internal.Raw₀.insertIfNew ⟨m, h⟩ a b) else m
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.isUnit_dblU_of_Y_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P Q : Fin 3 → F},
  W.Nonsingular P →
    P 2 ≠ 0 → Q 2 ≠ 0 → P 0 * Q 2 = Q 0 * P 2 → P 1 * Q 2 = Q 1 * P 2 → P 1 * Q 2 = W.negY Q * P 2 → IsUnit (W.dblU P)
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.face_nonDegenerateEquiv' : ∀ {n d : ℕ} (x : ↑((SSet.stdSimplex.obj { len := n }).nonDegenerate d)),
  SSet.stdSimplex.face ↑(SSet.stdSimplex.nonDegenerateEquiv' x) = SSet.Subcomplex.ofSimplex ↑x
-- Mathlib.Data.FunLike.IsApply
/-- `IsAddApply F α β` states for all `f g : F` and `x : α`, `(f + g) x = f x + g x`.  -/
IsAddApply : (F : Type u_1) → (α : outParam (Type u_2)) → (β : outParam (Type u_3)) → [FunLike F α β] → [Add β] → [Add F] → Prop
-- Mathlib.Order.Antichain
IsWeakAntichain.eq : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] {s : Set ((i : ι) → α i)} {a b : (i : ι) → α i},
  IsWeakAntichain s → a ∈ s → b ∈ s → StrongLT a b → a = b
-- Init.Data.List.Lemmas
List.reverse_flatMap : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β},
  (List.flatMap f l).reverse = List.flatMap (List.reverse ∘ f) l.reverse
-- Lean.Elab.PreDefinition.TerminationHint
/-- Here we record the number of parameters past the `:`. It is set by
`TerminationHints.rememberExtraParams` and used as follows:

* When we guess the termination measure in `GuessLex` and want to print it in surface-syntax
  compatible form.
* If there are fewer variables in the `termination_by` annotation than there are extra
  parameters, we know which parameters they should apply to (`TerminationBy.checkVars`).
 -/
Lean.Elab.TerminationHints.extraParams : Lean.Elab.TerminationHints → ℕ