mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.SetTheory.Ordinal.Univ
Cardinal.lift_univ : Cardinal.lift.{w, max (u + 1) v} Cardinal.univ.{u, v} = Cardinal.univ.{u, max v w}
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_eq_get!_get? : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β],
  t.WF → ∀ {a : α}, Std.DTreeMap.Internal.Impl.Const.get! t a = (Std.DTreeMap.Internal.Impl.Const.get? t a).get!
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- **Alias** of `MonoidAlgebra.mapRingHom`.

---

The ring homomorphism of monoid algebras induced by a homomorphism of the base rings.  -/
MonoidAlgebra.mapRangeRingHom : {R : Type u_3} →
  {S : Type u_4} →
    (M : Type u_6) →
      [inst : Semiring R] →
        [inst_1 : Semiring S] → [inst_2 : Monoid M] → (R →+* S) → MonoidAlgebra R M →+* MonoidAlgebra S M
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.false_elim : ∀ {σs : List (Type u)} {P : Std.Do.SPred σs}, ⌜False⌝ ⊢ₛ P
-- Mathlib.LinearAlgebra.Projectivization.Independence
Projectivization.Dependent.mk : ∀ {ι : Type u_1} {K : Type u_2} {V : Type u_3} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (f : ι → V) (hf : ∀ (i : ι), f i ≠ 0),
  ¬LinearIndependent K f → Projectivization.Dependent fun i => Projectivization.mk K (f i) ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
_private.Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ.0.WeierstrassCurve.exists_variableChange_of_char_two_of_j_ne_zero : ∀ {F : Type u_1} [inst : Field F] [IsSepClosed F] (E E' : WeierstrassCurve F) [CharP F 2] [E.IsCharTwoJNeZeroNF]
  [E'.IsCharTwoJNeZeroNF], E.a₆ = E'.a₆ → ∃ C, C • E = E'
-- Mathlib.Combinatorics.Quiver.ConnectedComponent
Quiver.IsStronglyConnected.isStronglyConnected_symmetrify : ∀ {V : Type u_2} [inst : Quiver V], Quiver.IsStronglyConnected V → Quiver.IsStronglyConnected (Quiver.Symmetrify V)
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.shiftFunctorAdd'_eq : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (a b c : ℤ)
  (h : a + b = c),
  CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b c h = CochainComplex.shiftFunctorAdd' C a b c h
-- Mathlib.Algebra.Group.Shrink
Shrink.instIsRightCancelMul : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Mul α] [IsRightCancelMul α], IsRightCancelMul (Shrink.{v, u_2} α)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKeyD_insert_le_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {fallback : α}, (cmp ((t.insert k v).minKeyD fallback) k).isLE = true
-- Mathlib.Order.Disjointed
disjointed_of_isMin : ∀ {α : Type u_1} {ι : Type u_2} [inst : GeneralizedBooleanAlgebra α] [inst_1 : Preorder ι]
  [inst_2 : LocallyFiniteOrderBot ι] (f : ι → α) {i : ι}, IsMin i → disjointed f i = f i
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
/-- the successor of an object  -/
CategoryTheory.SmallObject.SuccStruct.succ : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.SmallObject.SuccStruct C → C → C
-- Mathlib.Algebra.Group.Prod
MulEquiv.coe_prodComm_symm : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N], ⇑MulEquiv.prodComm.symm = Prod.swap
-- Lean.Message
Lean.MessageLog.append : Lean.MessageLog → Lean.MessageLog → Lean.MessageLog
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
ComplexShape.Embedding.mono_liftExtend_f_iff : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {K : HomologicalComplex C c'} {L : HomologicalComplex C c}
  [inst_3 : e.IsRelIff] (φ : K.restriction e ⟶ L) (hφ : e.HasLift φ) {i' : ι'} {i : ι},
  e.f i = i' → (CategoryTheory.Mono ((e.liftExtend φ hφ).f i') ↔ CategoryTheory.Mono (φ.f i))
-- Mathlib.Data.Sym.Basic
Sym.coe_erase : ∀ {α : Type u_1} {n : ℕ} [inst : DecidableEq α] {s : Sym α n.succ} {a : α} (h : a ∈ s), ↑(s.erase a h) = (↑s).erase a
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- The morphism `⦋1⦌ ⟶ ⦋n⦌` that picks out the edge spanning the interval from `j` to `j + l`.  -/
SimplexCategory.intervalEdge : {n : ℕ} → (j l : ℕ) → j + l ≤ n → ({ len := 1 } ⟶ { len := n })
-- Mathlib.Topology.Covering.Quotient
IsQuotientCoveringMap.fiberEquivGroup_eq_iff : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hf : IsQuotientCoveringMap f G) {x : X} (e e' : ↑(f ⁻¹' {x})) (g : G),
  (hf.fiberEquivGroup e) e' = g ↔ ↑e' = g • ↑e
-- Std.Http.Protocol.H1.Parser
/-- Returns `true` if `name` (compared case-insensitively) is a field that MUST NOT appear in HTTP/1.1
trailer sections per RFC 9112 §6.5. Forbidden fields are those required for message framing
(`content-length`, `transfer-encoding`), routing (`host`), or connection management (`connection`).
 -/
_private.Std.Http.Protocol.H1.Parser.0.Std.Http.Protocol.H1.isForbiddenTrailerField : String → Bool
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_union_of_not_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (∀ a ∈ m₁, a ∉ m₂) → (m₁ ∪ m₂).size = m₁.size + m₂.size
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatIso.op_isoWhiskerRight : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E]
  {H : CategoryTheory.Functor D E} (α : F ≅ G),
  CategoryTheory.NatIso.op (CategoryTheory.Functor.isoWhiskerRight α H) =
    G.opComp H ≪≫ CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.NatIso.op α) H.op ≪≫ (F.opComp H).symm
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.mkAppS₁₀ : {m : Type → Type} →
  [Lean.Meta.Sym.Internal.MonadShareCommon m] →
    [Monad m] →
      Lean.Expr →
        Lean.Expr →
          Lean.Expr →
            Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.GroupTheory.GroupAction.IterateAct
IterateMulAct.instMulAction.eq_1 : ∀ {α : Type u_1} {f : α → α},
  IterateMulAct.instMulAction = { smul := fun n x => f^[n.val] x, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.Condensed.Light.Sequence
/-- Given a map `π : T → S ⨯ Option X` and maps `σ : Option X → S → T`,
`fibres` gives the set containing union of the images of `σ (Some x)`
for all `x : X`, together with the fibre over `None : Option X` of the
composition `T → S ⨯ Option X → Option X `.  -/
_private.Mathlib.Condensed.Light.Sequence.0.InternalProjectivityProof.fibres : {S : Type u_1} → {T : Type u_2} → {X : Type u_3} → (T → S × Option X) → (Option X → S → T) → Set T
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.AltExpr.funName : {σ : Type} → Lean.Elab.Term.Do.AltExpr σ → Lean.Syntax
-- Mathlib.Algebra.Group.Hom.Defs
IsDedekindFiniteMonoid.of_injective : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : MulOne M] [inst_1 : MulOne N] [inst_2 : FunLike F M N]
  [MonoidHomClass F M N] (f : F), Function.Injective ⇑f → ∀ [IsDedekindFiniteMonoid N], IsDedekindFiniteMonoid M
-- Init.Data.Order.Ord
Std.OrientedCmp.eq_comm : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] {a b : α}, cmp a b = Ordering.eq ↔ cmp b a = Ordering.eq
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey!_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (Std.ExtDTreeMap.Const.insertMany t l).getKey! k' = k
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasColimit_leftOp_of_hasLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J Cᵒᵖ) [CategoryTheory.Limits.HasLimit F], CategoryTheory.Limits.HasColimit F.leftOp
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonSemanticTokensLegend : Lean.FromJson Lean.Lsp.SemanticTokensLegend
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.restrict_univ : ∀ {α : Type u_1} (m : MeasureTheory.OuterMeasure α), (MeasureTheory.OuterMeasure.restrict Set.univ) m = m
-- Std.Http.Protocol.H1
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.BodyMode : Type
-- Mathlib.Topology.Separation.Regular
disjoint_nhdsSet_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] [RegularSpace X] {x : X} {s : Set X},
  Disjoint (nhdsSet s) (nhds x) ↔ x ∉ closure s
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.inter_p₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S)
  (F : CategoryTheory.PreOneHypercover S)
  [inst_1 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)]
  [inst_2 :
    ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b),
      CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i))
        (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))]
  (i j : (E.inter F.toPreZeroHypercover).I₀) (k : E.I₁ i.1 j.1 × F.I₁ i.2 j.2),
  (E.inter F).p₁ k =
    CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (E.p₁ k.1) (E.f i.1))
      (CategoryTheory.CategoryStruct.comp (F.p₁ k.2) (F.f i.2))
      (E.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm i).fst)
      (F.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm i).snd) (E.p₁ k.1) (F.p₁ k.2)
      (CategoryTheory.CategoryStruct.id S) ⋯ ⋯
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.toCompletion_mul : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K) (x y : v.Completion),
  (x * y).toCompletion = x.toCompletion * y.toCompletion
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblenWith_lt_veblenWith_veblenWith_iff : ∀ {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ a : Ordinal.{u}},
  Order.IsNormal f →
    o₂ ≤ o₁ →
      (Ordinal.veblenWith f o₂ a < Ordinal.veblenWith f o₁ (Ordinal.veblenWith f o₂ a) ↔ a < Ordinal.veblenWith f o₁ a)
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.comp.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.AddMonObj A] {M N O : CategoryTheory.AddMod D A} (f : M.Hom N) (g : N.Hom O),
  CategoryTheory.AddMod.comp f g = { hom := CategoryTheory.CategoryStruct.comp f.hom g.hom, isAddModHom := ⋯ }
-- Mathlib.Tactic.Module
Mathlib.Tactic.Module.NF.eval_algebraMap : ∀ {S : Type u_1} (R : Type u_2) {M : Type u_3} [inst : CommSemiring S] [inst_1 : Semiring R] [inst_2 : Algebra S R]
  [inst_3 : AddMonoid M] [inst_4 : SMul S M] [inst_5 : MulAction R M] [IsScalarTower S R M]
  (l : Mathlib.Tactic.Module.NF S M), (Mathlib.Tactic.Module.NF.algebraMap R l).eval = l.eval
-- Init.Data.UInt.Lemmas
UInt16.toFin.ofNat : ∀ {n : ℕ}, (UInt16.ofNat n).toFin = Fin.ofNat UInt16.size n
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.toAffine_smul : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} (P : Fin 3 → F) {u : F},
  IsUnit u → WeierstrassCurve.Jacobian.Point.toAffine W (u • P) = WeierstrassCurve.Jacobian.Point.toAffine W P
-- Mathlib.Order.Category.BoolAlg
BoolAlg.Iso.mk_inv : ∀ {α β : BoolAlg} (e : ↑α ≃o ↑β),
  (BoolAlg.Iso.mk e).inv =
    BoolAlg.ofHom
      (have __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
      { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.smul : {S : Type u'} →
  {R : Type u} →
    {M : Type v} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          {module_M : Module R M} →
            (p : Submodule R M) → [inst_2 : SMul S R] → [inst_3 : SMul S M] → [IsScalarTower S R M] → SMul S ↥p
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.mk_surjective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Subobject X),
  ∃ A i, ∃ (x : CategoryTheory.Mono i), S = CategoryTheory.Subobject.mk i
-- Mathlib.Topology.Algebra.MulAction
ContinuousVAdd.continuousConstVAdd : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : VAdd M X]
  [ContinuousVAdd M X], ContinuousConstVAdd M X
-- Mathlib.Data.Seq.Basic
Stream'.Seq.set.eq_1 : ∀ {α : Type u} (s : Stream'.Seq α) (n : ℕ) (a : α), s.set n a = s.update n fun x => a
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.homologyFunctor_additive : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CategoryWithHomology C], (CategoryTheory.ShortComplex.homologyFunctor C).Additive
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- Constructor for natural isomorphisms between functors out of `WalkingReflexivePair`.  -/
CategoryTheory.Limits.reflexivePair.mkNatIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C} →
      (e₀ :
          F.obj CategoryTheory.Limits.WalkingReflexivePair.zero ≅
            G.obj CategoryTheory.Limits.WalkingReflexivePair.zero) →
        (e₁ :
            F.obj CategoryTheory.Limits.WalkingReflexivePair.one ≅
              G.obj CategoryTheory.Limits.WalkingReflexivePair.one) →
          autoParam
              (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left) e₀.hom =
                CategoryTheory.CategoryStruct.comp e₁.hom (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left))
              CategoryTheory.Limits.reflexivePair.mkNatIso._auto_1 →
            autoParam
                (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right)
                    e₀.hom =
                  CategoryTheory.CategoryStruct.comp e₁.hom
                    (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right))
                CategoryTheory.Limits.reflexivePair.mkNatIso._auto_3 →
              autoParam
                  (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion)
                      e₁.hom =
                    CategoryTheory.CategoryStruct.comp e₀.hom
                      (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion))
                  CategoryTheory.Limits.reflexivePair.mkNatIso._auto_5 →
                (F ≅ G)
-- Mathlib.Data.Finset.Sups
/-- **Alias** of the forward direction of `Finset.compls_nonempty`. -/
Finset.Nonempty.of_compls : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {s : Finset α}, s.compls.Nonempty → s.Nonempty
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.prod_mono_set_of_one_le' : ∀ {ι : Type u_1} {N : Type u_5} [inst : CommMonoid N] [inst_1 : Preorder N] {f : ι → N} [MulLeftMono N],
  (∀ (x : ι), 1 ≤ f x) → Monotone fun s => ∏ x ∈ s, f x
-- Mathlib.CategoryTheory.Types.Basic
_private.Mathlib.CategoryTheory.Types.Basic.0.TypeCat.Hom.mk : {X Y : Type u} → TypeCat.Fun X Y → TypeCat.Hom X Y