mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
/-- See note [comp_of_eq lemmas]  -/
ContMDiffAt.comp_of_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] {E'' : Type u_8} [inst_9 : NormedAddCommGroup E''] [inst_10 : NormedSpace 𝕜 E'']
  {H'' : Type u_9} [inst_11 : TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10}
  [inst_12 : TopologicalSpace M''] [inst_13 : ChartedSpace H M] [inst_14 : ChartedSpace H' M']
  [inst_15 : ChartedSpace H'' M''] {f : M → M'} {n : WithTop ℕ∞} {g : M' → M''} {x : M} {y : M'},
  ContMDiffAt I' I'' n g y → ContMDiffAt I I' n f x → f x = y → ContMDiffAt I I'' n (g ∘ f) x
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearIsometryEquiv.adjoint_eq_symm : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {H : Type u_5} [inst_1 : NormedAddCommGroup H] [inst_2 : InnerProductSpace 𝕜 H]
  [inst_3 : CompleteSpace H] {K : Type u_6} [inst_4 : NormedAddCommGroup K] [inst_5 : InnerProductSpace 𝕜 K]
  [inst_6 : CompleteSpace K] (e : H ≃ₗᵢ[𝕜] K), ContinuousLinearMap.adjoint ↑↑e = ↑↑e.symm
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.norm_toLp_one : ∀ {p : ENNReal} {ι : Type u_2} [hp : Fact (1 ≤ p)] [inst : Fintype ι] {β : Type u_5}
  [inst_1 : SeminormedAddCommGroup β],
  p ≠ ⊤ → ∀ [inst_2 : One β], ‖WithLp.toLp p 1‖ = ↑↑(Fintype.card ι) ^ (1 / p).toReal * ‖1‖
-- Lean.Elab.PreDefinition.Structural.Eqns
Lean.Elab.Structural.eqnInfoExt : Lean.MapDeclarationExtension Lean.Elab.Structural.EqnInfo
-- Mathlib.Analysis.Convex.Integral
/-- **Jensen's inequality**: if a function `g : E → ℝ` is convex and continuous on a convex closed
set `s`, `μ` is a finite non-zero measure on `α`, and `f : α → E` is a function sending
`μ`-a.e. points to `s`, then the value of `g` at the average value of `f` is less than or equal to
the average value of `g ∘ f` provided that both `f` and `g ∘ f` are integrable. See also
`ConvexOn.map_centerMass_le` for a finite sum version of this lemma.  -/
ConvexOn.map_average_le : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} {g : E → ℝ} [MeasureTheory.IsFiniteMeasure μ]
  [NeZero μ],
  ConvexOn ℝ s g →
    ContinuousOn g s →
      IsClosed s →
        (∀ᵐ (x : α) ∂μ, f x ∈ s) →
          MeasureTheory.Integrable f μ →
            MeasureTheory.Integrable (g ∘ f) μ → g (⨍ (x : α), f x ∂μ) ≤ ⨍ (x : α), g (f x) ∂μ
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_lt_aleph0_iff : ∀ {o : Ordinal.{u_1}}, o.cof < Cardinal.aleph0 ↔ o.cof ≤ 1
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.hasEqualizers : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C],
  CategoryTheory.Limits.HasEqualizers C
-- Mathlib.Order.Monotone.Basic
monotone_toDual_comp_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone (⇑OrderDual.toDual ∘ f) ↔ Antitone f
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate the expression `η ⊗ θ` into a normalized form.  -/
Mathlib.Tactic.BicategoryLike.evalHorizontalComp : {ρ : Type} →
  [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
    [Mathlib.Tactic.BicategoryLike.MonadNormalExpr (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
      [Mathlib.Tactic.BicategoryLike.MkEval (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
        [Mathlib.Tactic.BicategoryLike.MonadMor₁ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
          Mathlib.Tactic.BicategoryLike.NormalExpr →
            Mathlib.Tactic.BicategoryLike.NormalExpr →
              Mathlib.Tactic.BicategoryLike.CoherenceM ρ Mathlib.Tactic.BicategoryLike.Eval.Result
-- Mathlib.Algebra.Group.Pi.Lemmas
MulHom.piMap_apply : ∀ {ι : Type u_1} {M : ι → Type u_3} {N : ι → Type u_4} [inst : (i : ι) → Mul (M i)] [inst_1 : (i : ι) → Mul (N i)]
  (g : (i : ι) → M i →ₙ* N i) (x : (i : ι) → M i) (i : ι), (MulHom.piMap g) x i = (g i) (x i)
-- Mathlib.CategoryTheory.Quotient
/-- The original functor factors through the induced functor.  -/
CategoryTheory.Quotient.lift.isLift : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (r : HomRel C) →
      {D : Type u_2} →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          (F : CategoryTheory.Functor C D) →
            (H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂) →
              (CategoryTheory.Quotient.functor r).comp (CategoryTheory.Quotient.lift r F H) ≅ F
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.of_subsingleton : ∀ {M : Type u_1} [Subsingleton M] [inst : Monoid M] (a b : M), Associated a b
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- The equivalence relation on tuples of left fractions with the same denominator
for a morphism property `W`. The fact it is an equivalence relation is not
formalized, but it would follow easily from `LeftFraction₂.map_eq_iff`.  -/
CategoryTheory.MorphismProperty.LeftFraction₂Rel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → W.LeftFraction₂ X Y → W.LeftFraction₂ X Y → Prop
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toListRev_filterMapM_mapM : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
  [inst_6 : Monad o] [inst_7 : MonadAttach o] [LawfulMonad o] [WeaklyLawfulMonadAttach o] [inst_10 : MonadLiftT m n]
  [inst_11 : MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → n γ} {g : γ → o (Option δ)} {it : Std.IterM m β},
  (Std.IterM.filterMapM g (Std.IterM.mapM f it)).toListRev =
    (Std.IterM.filterMapM
        (fun b => do
          let __do_lift ← liftM (f b)
          g __do_lift)
        it).toListRev
-- Mathlib.Data.List.Basic
List.exists_mem_cons_of_exists : ∀ {α : Type u} {p : α → Prop} {a : α} {l : List α}, (∃ x ∈ l, p x) → ∃ x ∈ a :: l, p x
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trNormal.eq_7 : ∀ (x : Turing.PartrecToTM2.Cont') (f : Turing.ToPartrec.Code),
  Turing.PartrecToTM2.trNormal f.fix x = Turing.PartrecToTM2.trNormal f (Turing.PartrecToTM2.Cont'.fix f x)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See also `le_inv_of_le_inv₀` for a one-sided implication with one fewer assumption.  -/
le_inv_comm₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀]
  {a b : G₀}, 0 < a → 0 < b → (a ≤ b⁻¹ ↔ b ≤ a⁻¹)
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.FunctorialFactorizationData.fac_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  (self : W₁.FunctorialFactorizationData W₂) {Z : CategoryTheory.Functor (CategoryTheory.Arrow C) C}
  (h : CategoryTheory.Arrow.rightFunc ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.i (CategoryTheory.CategoryStruct.comp self.p h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Arrow.leftToRight h
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {k fallback : α}, k ∉ t₁ → (t₁ ∩ t₂).getKeyD k fallback = fallback
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.withBRecOnArgs.go.go2 : Lean.Meta.IndPredBelow.Context✝ →
  Array Lean.Expr → Lean.Name → Array Lean.Expr → ℕ → Array Lean.Expr → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.List.Find
List.lookup_eq_findSome? : ∀ {α : Type u_2} [inst : BEq α] {β : Type u_1} {l : List (α × β)} {k : α},
  List.lookup k l = List.findSome? (fun p => if (k == p.1) = true then some p.2 else none) l
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
CategoryTheory.Limits.Concrete.prodEquiv_apply_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] (X₁ X₂ : C)
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct X₁ X₂]
  [inst_4 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X₁ X₂) (CategoryTheory.forget C)]
  (x : CategoryTheory.ToType (X₁ ⨯ X₂)),
  ((CategoryTheory.Limits.Concrete.prodEquiv X₁ X₂) x).1 =
    (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.fst) x
-- Mathlib.Algebra.Group.Action.Defs
AddSemigroupAction.ext_iff : ∀ {G : Type u_9} {P : Type u_10} {inst : AddSemigroup G} {x y : AddSemigroupAction G P}, x = y ↔ VAdd.vadd = VAdd.vadd
-- Mathlib.Tactic.Determinant.Bird.Meta
/-- The ring instance and evaluator context parsed by `reifyBirdDet`.  -/
Mathlib.Tactic.Determinant.ReifiedBirdDet : Type
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.toList_eq_nil_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.toList = [] ↔ t = ∅
-- Init.Data.Int.Linear
/-- Normalizes the given polynomial by fusing monomial and constants.  -/
Int.Internal.Linear.Poly.norm : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.bin.sizeOf_spec : ∀ {w : ℕ} (lhs : Std.Tactic.BVDecide.BVExpr w) (op : Std.Tactic.BVDecide.BVBinOp) (rhs : Std.Tactic.BVDecide.BVExpr w),
  sizeOf (lhs.bin op rhs) = 1 + sizeOf w + sizeOf lhs + sizeOf op + sizeOf rhs
-- Lean.Server.FileSource
Lean.Lsp.FileSource : Type → Type
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.Intro.intro : ∀ {σs : List (Type u)} {P Q H T : Std.Do.SPred σs}, (Q ∧ H ⊣⊢ₛ P) → (P ⊢ₛ T) → Q ⊢ₛ H → T
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {X : C} →
        [toMonObj : CategoryTheory.MonObj X] →
          (inv : X ⟶ X) →
            autoParam
                (CategoryTheory.CategoryStruct.comp
                    (CategoryTheory.CartesianMonoidalCategory.lift inv (CategoryTheory.CategoryStruct.id X))
                    CategoryTheory.MonObj.mul =
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X)
                    CategoryTheory.MonObj.one)
                CategoryTheory.GrpObj.left_inv._autoParam →
              autoParam
                  (CategoryTheory.CategoryStruct.comp
                      (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id X) inv)
                      CategoryTheory.MonObj.mul =
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X)
                      CategoryTheory.MonObj.one)
                  CategoryTheory.GrpObj.right_inv._autoParam →
                CategoryTheory.GrpObj X
-- Mathlib.Analysis.Analytic.Constructions
formalMultilinearSeries_geometric.eq_1 : ∀ (𝕜 : Type u_2) [inst : NontriviallyNormedField 𝕜] (A : Type u_7) [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  (n : ℕ), formalMultilinearSeries_geometric 𝕜 A n = ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.IsImage.isOpen_iff : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y},
  e.IsImage s t → (IsOpen (e.source ∩ s) ↔ IsOpen (e.target ∩ t))
-- Mathlib.Algebra.CharP.Basic
CharP.natCast_eq_natCast : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} [IsRightCancelAdd R], ↑a = ↑b ↔ a ≡ b [MOD p]
-- Mathlib.Condensed.Light.Sequence
_private.Mathlib.Condensed.Light.Sequence.0.InternalProjectivityProof.mem_fibres_iff : ∀ {S : Type u_1} {T : Type u_2} {X : Type u_3} (π : T → S × Option X) (σ : Option X → S → T) (t : T),
  t ∈ InternalProjectivityProof.fibres✝ π σ ↔ (π t).2 = none ∨ ∃ x s, σ (some x) s = t
-- Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
/-- Any category with pushouts and initial object has binary coproducts.  -/
hasBinaryCoproducts_of_hasInitial_and_pushouts : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C]
  [CategoryTheory.Limits.HasPushouts C], CategoryTheory.Limits.HasBinaryCoproducts C
-- Mathlib.Topology.Separation.Regular
/-- Given two distinct points in a T₂.₅ space, their filters of closed neighborhoods are
disjoint.  -/
T25Space.t2_5 : ∀ {X : Type u} {inst : TopologicalSpace X} [self : T25Space X] ⦃x y : X⦄,
  x ≠ y → Disjoint ((nhds x).lift' closure) ((nhds y).lift' closure)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.exists : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {P : AddMonoidAlgebra R M → Prop},
  (∃ p, P p) ↔ ∃ q, P (AddMonoidAlgebra.ofCoeff q)
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.fst_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) (v : V × W), (Representation.IntertwiningMap.fst A ρ σ) v = v.1
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k₁ k₂ : α}
  (h' : cmp k₁ k₂ = Ordering.eq) (h₁ : k₁ ∈ t), t.get k₁ h₁ = t.get k₂ ⋯
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_iff_forall_not_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → (t.isEmpty = true ↔ ∀ (a : α), a ∉ t)
-- Mathlib.Data.Finsupp.Basic
Finsupp.support_curry : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] [inst_1 : DecidableEq α] (f : α × β →₀ M),
  f.curry.support = Finset.image Prod.fst f.support
-- Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv
CategoryTheory.Functor.IsDenseSubsite.isIso_ranCounit_app_of_isDenseSubsite : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D)
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) {A : Type w}
  [inst_2 : CategoryTheory.Category.{w', w} A]
  [inst_3 : ∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A]
  [CategoryTheory.Functor.IsDenseSubsite J K G] (Y : CategoryTheory.Sheaf J A) (U : C) (X : A),
  CategoryTheory.IsIso
    ((CategoryTheory.yoneda.map ((G.op.ranCounit.app Y.obj).app (Opposite.op U))).app (Opposite.op X))
-- Batteries.Lean.Meta.UnusedNames
Lean.Name.MatchUpToIndexSuffix.suffixMatch.sizeOf_spec : ∀ (i : ℕ), sizeOf (Lean.Name.MatchUpToIndexSuffix.suffixMatch i) = 1 + sizeOf i
-- ProofWidgets.Data.Html
ProofWidgets.Html.element.injEq : ∀ (a : String) (a_1 : Array (String × Lean.Json)) (a_2 : Array ProofWidgets.Html) (a_3 : String)
  (a_4 : Array (String × Lean.Json)) (a_5 : Array ProofWidgets.Html),
  (ProofWidgets.Html.element a a_1 a_2 = ProofWidgets.Html.element a_3 a_4 a_5) = (a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.opEquiv_functor : ∀ {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), (CategoryTheory.Comma.opEquiv L R).functor = CategoryTheory.Comma.opFunctor L R
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.forIn'_eq_forIn'_rcc : ∀ {α : Type u} {r : Std.Ric α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLeast? α] [inst_6 : Std.Rxc.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [inst_8 : Monad m] [LawfulMonad m] {γ : Type u}
  {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f = forIn' (Std.PRange.UpwardEnumerable.least...=r.upper) init fun a ha acc => f a ⋯ acc
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- `MonoidAlgebra.single` as an `AddMonoidHom`.

TODO: Rename to `singleAddMonoidHom`.  -/
MonoidAlgebra.singleAddHom : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → M → R →+ MonoidAlgebra R M
-- Mathlib.Data.Finset.Union
Finset.mem_biUnion : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} [inst : DecidableEq β] {b : β},
  b ∈ s.biUnion t ↔ ∃ a ∈ s, b ∈ t a
-- Mathlib.Algebra.GroupWithZero.Units.Equiv
Equiv.mulLeft₀_symm_apply : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] (a : G₀) (ha : a ≠ 0),
  ⇑(Equiv.symm (Equiv.mulLeft₀ a ha)) = fun x => a⁻¹ * x
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Bundle.mdifferentiableWithinAt_proj : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E]
  {s : Set (Bundle.TotalSpace F E)} {p : Bundle.TotalSpace F E}, MDiffAt[s] Bundle.TotalSpace.proj p
-- Mathlib.Order.OmegaCompletePartialOrder
/-- The supremum of iterating a function on x arbitrary often is smaller than any prefixed point.

A prefixed point is a value `a` with `f a ≤ a`.  -/
OmegaCompletePartialOrder.fixedPoints.ωSup_iterate_le_prefixedPoint : ∀ {α : Type u_2} [inst : OmegaCompletePartialOrder α] (f : α →𝒄 α) (x : α) (h : x ≤ f x) {a : α},
  f a ≤ a → x ≤ a → OmegaCompletePartialOrder.ωSup (OmegaCompletePartialOrder.fixedPoints.iterateChain (↑f) x h) ≤ a
-- Mathlib.Algebra.Module.SpanRank
Submodule.spanRank_map_le : ∀ {R : Type u_1} {S : Type u_2} {M N : Type u} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S}
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : Module S N]
  [inst_6 : RingHomSurjective σ] (f : M →ₛₗ[σ] N) (p : Submodule R M), (Submodule.map f p).spanRank ≤ p.spanRank
-- Mathlib.Topology.Constructions
/-- **Alias** of the reverse direction of `continuousAt_codRestrict_iff`. -/
ContinuousAt.codRestrict : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {t : Set Y}
  (h1 : ∀ (x : X), f x ∈ t) {x : X}, ContinuousAt f x → ContinuousAt (Set.codRestrict f t h1) x
-- Mathlib.Data.Finsupp.Weight
Finsupp.finite_of_nat_weight_lt : ∀ {σ : Type u_1} [Finite σ] (w : σ → ℕ), (∀ (x : σ), w x ≠ 0) → ∀ (n : ℕ), {d | (Finsupp.weight w) d < n}.Finite
-- Init.Data.Nat.Lemmas
Nat.pow_right_comm : ∀ (a m n : ℕ), (a ^ m) ^ n = (a ^ n) ^ m
-- Mathlib.Topology.Connected.Clopen
IsClopen.connectedComponent_subset : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α} {x : α}, IsClopen s → x ∈ s → connectedComponent x ⊆ s
-- Mathlib.RingTheory.KrullDimension.Basic
Ideal.mem_minimalPrimes_of_krullDimLE_zero : ∀ {R : Type u_1} [inst : CommSemiring R] [Ring.KrullDimLE 0 R] (I : Ideal R) [I.IsPrime], I ∈ minimalPrimes R
-- Lean.DocString.Types
Lean.Doc.Part.mk.sizeOf_spec : ∀ {i : Type u} {b : Type v} {p : Type w} [inst : SizeOf i] [inst_1 : SizeOf b] [inst_2 : SizeOf p]
  (title : Array (Lean.Doc.Inline i)) (titleString : String) (metadata : Option p)
  (content : Array (Lean.Doc.Block i b)) (subParts : Array (Lean.Doc.Part i b p)),
  sizeOf
      { title := title, titleString := titleString, metadata := metadata, content := content, subParts := subParts } =
    1 + sizeOf title + sizeOf titleString + sizeOf metadata + sizeOf content + sizeOf subParts
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- The universal property of a cartesian `⊗` as an equivalence.  -/
CategoryTheory.CartesianMonoidalCategory.liftEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {T X Y : C} → (T ⟶ X) × (T ⟶ Y) ≃ (T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
-- Mathlib.Data.EReal.Inv
EReal.instMulPosReflectLT : MulPosReflectLT EReal
-- Mathlib.Order.CompleteBooleanAlgebra
Order.Coframe.MinimalAxioms.mk : ∀ {α : Type u} [inst : CompleteLattice α],
  (∀ (a : α) (s : Set α), ⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s) → Order.Coframe.MinimalAxioms α
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec.toSheafedSpace_obj : ∀ (R : CommRingCatᵒᵖ),
  AlgebraicGeometry.Spec.toSheafedSpace.obj R = AlgebraicGeometry.Spec.sheafedSpaceObj (Opposite.unop R)
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.replicateCol_apply : ∀ {m : Type u_2} {α : Type v} {ι : Type u_6} (w : m → α) (i : m) (j : ι), Matrix.replicateCol ι w i j = w i
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_insertIfNew!_le_minKey! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF →
    t.isEmpty = false →
      ∀ {k : α} {v : β k}, (compare (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).minKey! t.minKey!).isLE = true
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min?_le_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k km : α} (hc : k ∈ t),
  t.min?.get ⋯ = km → (cmp km k).isLE = true
-- Batteries.Data.AssocList
Batteries.AssocList.beq.eq_def : ∀ {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst_1 : BEq β] (x x_1 : Batteries.AssocList α β),
  x.beq x_1 =
    match x, x_1 with
    | Batteries.AssocList.nil, Batteries.AssocList.nil => true
    | Batteries.AssocList.cons key value tail, Batteries.AssocList.nil => false
    | Batteries.AssocList.nil, Batteries.AssocList.cons key value tail => false
    | Batteries.AssocList.cons a b t, Batteries.AssocList.cons a' b' t' => a == a' && b == b' && t.beq t'
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.pOpcyclesNatTrans_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C]
  (S : CategoryTheory.ShortComplex C), (CategoryTheory.ShortComplex.pOpcyclesNatTrans C).app S = S.pOpcycles
-- Mathlib.Algebra.Exact.Basic
Function.Exact.iff_of_ladder_addEquiv : ∀ {X₁ : Type u_8} {X₂ : Type u_9} {X₃ : Type u_10} {Y₁ : Type u_11} {Y₂ : Type u_12} {Y₃ : Type u_13}
  [inst : AddCommMonoid X₁] [inst_1 : AddCommMonoid X₂] [inst_2 : AddCommMonoid X₃] [inst_3 : AddCommMonoid Y₁]
  [inst_4 : AddCommMonoid Y₂] [inst_5 : AddCommMonoid Y₃] (e₁ : X₁ ≃+ Y₁) (e₂ : X₂ ≃+ Y₂) (e₃ : X₃ ≃+ Y₃)
  {f₁₂ : X₁ →+ X₂} {f₂₃ : X₂ →+ X₃} {g₁₂ : Y₁ →+ Y₂} {g₂₃ : Y₂ →+ Y₃},
  g₁₂.comp ↑e₁ = (↑e₂).comp f₁₂ → g₂₃.comp ↑e₂ = (↑e₃).comp f₂₃ → (Function.Exact ⇑g₁₂ ⇑g₂₃ ↔ Function.Exact ⇑f₁₂ ⇑f₂₃)
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
OrderIso.map_csInf_of_directedOn' : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompletePartialOrderInf α]
  [inst_1 : ConditionallyCompletePartialOrderInf β] (e : α ≃o β) {s : Set α},
  DirectedOn (fun x1 x2 => x2 ≤ x1) s → s.Nonempty → BddBelow s → e (sInf s) = sInf (⇑e '' s)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.Φ_four : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R),
  W.Φ 4 = Polynomial.X * W.preΨ₄ ^ 2 * W.Ψ₂Sq - W.Ψ₃ * (W.preΨ₄ * W.Ψ₂Sq ^ 2 - W.Ψ₃ ^ 3)