mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
/-- Pre-composition by a *fixed* continuous linear map as a continuous linear map.

Note that in non-normed space it is not always true that composition is continuous
in both variables, so we have to fix one of them.  -/
ContinuousLinearMap.precomp : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    {𝕜₃ : Type u_3} →
      [inst : NormedField 𝕜₁] →
        [inst_1 : NormedField 𝕜₂] →
          [inst_2 : NormedField 𝕜₃] →
            {σ : 𝕜₁ →+* 𝕜₂} →
              {τ : 𝕜₂ →+* 𝕜₃} →
                {ρ : 𝕜₁ →+* 𝕜₃} →
                  [RingHomCompTriple σ τ ρ] →
                    {E : Type u_4} →
                      {F : Type u_5} →
                        (G : Type u_6) →
                          [inst_4 : AddCommGroup E] →
                            [inst_5 : Module 𝕜₁ E] →
                              [inst_6 : AddCommGroup F] →
                                [inst_7 : Module 𝕜₂ F] →
                                  [inst_8 : AddCommGroup G] →
                                    [inst_9 : Module 𝕜₃ G] →
                                      [inst_10 : TopologicalSpace E] →
                                        [inst_11 : TopologicalSpace F] →
                                          [inst_12 : TopologicalSpace G] →
                                            [inst_13 : IsTopologicalAddGroup G] →
                                              [inst_14 : ContinuousConstSMul 𝕜₃ G] →
                                                [RingHomSurjective σ] →
                                                  [RingHomIsometric σ] → (E →SL[σ] F) → (F →SL[τ] G) →L[𝕜₃] E →SL[ρ] G
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.lowerCentralSeries_zero_eq_bot_iff : ∀ {G : Type u_1} [inst : AddGroup G], ⊤.lowerCentralSeries 1 = ⊥ ↔ IsAddCommutative G
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.monotone_map : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {f : F}, Monotone (Submonoid.map f)
-- Init.Data.Range.Lemmas
_private.Init.Data.Range.Lemmas.0.Std.Legacy.Range.size_eq : ∀ {i : ℕ} (r : Std.Legacy.Range),
  i < r.stop → (r.stop - i + r.step - 1) / r.step = (r.stop - (i + r.step) + r.step - 1) / r.step + 1
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioc_subset_Ioc_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {a₁ a₂ b₁ b₂ : α}, a₁ < b₁ → (Set.Ioc a₁ b₁ ⊆ Set.Ioc a₂ b₂ ↔ b₁ ≤ b₂ ∧ a₂ ≤ a₁)
-- Mathlib.CategoryTheory.LiftingProperties.Adjunction
CategoryTheory.Adjunction.hasLiftingProperty_iff : ∀ {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} {F : CategoryTheory.Functor D C}
  (adj : G ⊣ F) {A B : C} {X Y : D} (i : A ⟶ B) (p : X ⟶ Y),
  CategoryTheory.HasLiftingProperty (G.map i) p ↔ CategoryTheory.HasLiftingProperty i (F.map p)
-- Mathlib.Logic.Function.Basic
Function.update_injective : ∀ {α : Sort u} {β : α → Sort v} [inst : DecidableEq α] (f : (a : α) → β a) (a' : α),
  Function.Injective (Function.update f a')
-- Mathlib.SetTheory.Ordinal.Veblen
/-- The gamma function enumerates the fixed points of `veblen · 0`.

Of particular importance is `Γ₀ = gamma 0`, the Feferman-Schütte ordinal. 

Conventions for notations in identifiers:

 * The recommended spelling of `Γ_ ` in identifiers is `gamma`. -/
Ordinal.termΓ_ : Lean.ParserDescr
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.C_eq_algebraMap : ∀ (R : Type u) (σ : Type u_1) [inst : CommSemiring R], MvPolynomial.C = algebraMap R (MvPolynomial σ R)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.insertManyIfNew_eq_foldl : ∀ {α : Type u} {β : α → Type v} {x : Ord α} {l : List ((a : α) × β a)} {t : Std.DTreeMap.Internal.Impl α β}
  (h : t.Balanced),
  ↑(t.insertManyIfNew l h) =
    List.foldl
      (fun acc x_1 =>
        match x_1 with
        | ⟨k, v⟩ => Std.DTreeMap.Internal.Impl.insertIfNew! k v acc)
      t l
-- Mathlib.RingTheory.Bialgebra.Convolution
BialgHom.convOne_def : ∀ {R : Type u_1} {A : Type u_2} {C : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring C]
  [inst_3 : Bialgebra R A] [inst_4 : Bialgebra R C],
  1 = WithConv.toConv ((Bialgebra.unitBialgHom R A).comp (Bialgebra.counitBialgHom R C))
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect.0.Std.IterM.toArray.go_eq.match_1.eq_2 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Mathlib.Algebra.Polynomial.Eval.SMul
Polynomial.eval_smul : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : SMulZeroClass S R] [IsScalarTower S R R] (s : S)
  (p : Polynomial R) (x : R), Polynomial.eval x (s • p) = s • Polynomial.eval x p
-- Mathlib.Analysis.Calculus.DiffContOnCl
DiffContOnCl.differentiableOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E},
  DiffContOnCl 𝕜 f s → DifferentiableOn 𝕜 f s
-- Mathlib.RingTheory.WittVector.Defs
WittVector.instMul : {p : ℕ} → {R : Type u_1} → [hp : Fact (Nat.Prime p)] → [CommRing R] → Mul (WittVector p R)
-- Mathlib.Algebra.Order.Group.PosPart
Pi.posPart_def : ∀ {ι : Type u_2} {α : ι → Type u_3} [inst : (i : ι) → Lattice (α i)] [inst_1 : (i : ι) → AddGroup (α i)]
  (f : (i : ι) → α i), f⁺ = fun i => (f i)⁺
-- Mathlib.Topology.Algebra.Module.Determinant
ContinuousLinearMap.det_smulRight : ∀ {𝕜 : Type u_1} [inst : CommRing 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousMul 𝕜] (f : 𝕜 →L[𝕜] 𝕜) (v : 𝕜),
  (f.smulRight v).det = f 1 * v
-- Lean.Meta.CongrTheorems
_private.Lean.Meta.CongrTheorems.0.Lean.Meta.EqInfo.decSubsingleton.injEq : ∀ (lhs rhs lhs_1 rhs_1 : Lean.FVarId),
  (Lean.Meta.EqInfo.decSubsingleton✝ lhs rhs = Lean.Meta.EqInfo.decSubsingleton✝ lhs_1 rhs_1) =
    (lhs = lhs_1 ∧ rhs = rhs_1)
-- Mathlib.RepresentationTheory.Rep.Basic
/-- Given a `k`-linear `G`-representation `(V, ρ)` and a `G`-invariant `k`-submodule `W ≤ V`, this
is the representation induced on `V ⧸ W` by `ρ`.  -/
Rep.quotient : {k : Type u} →
  {G : Type v} →
    [inst : Ring k] →
      [inst_1 : Monoid G] →
        (A : Rep.{u_1, u, v} k G) →
          (W : Submodule k ↑A) → (∀ (g : G), W ≤ Submodule.comap (A.ρ g) W) → Rep.{u_1, u, v} k G
-- Aesop.Index
Aesop.Index.fold : {α : Type} → {σ : Type u_1} → Aesop.Index α → (σ → Aesop.Rule α → σ) → σ → σ
-- Mathlib.Order.Interval.Set.Basic
Set.Ici_top : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α], Set.Ici ⊤ = {⊤}
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.negY_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F},
  P 2 ≠ 0 → W.negY P / P 2 = W.toAffine.negY (P 0 / P 2) (P 1 / P 2)
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.mkDefaultMethodsCore : Lean.Meta.Simp.SimprocsArray → Lean.Meta.Simp.Methods
-- Lean.Data.Lsp.Window
Lean.Lsp.MessageType.error.sizeOf_spec : sizeOf Lean.Lsp.MessageType.error = 1
-- Lean.Meta.Tactic.Grind.ProveEq
/-- Ground terms from the `lhs` that have been abstracted so far.  -/
_private.Lean.Meta.Tactic.Grind.ProveEq.0.Lean.Meta.Grind.AbstractM.State.lhss : Lean.Meta.Grind.AbstractM.State✝ → Array Lean.Expr
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
OrdinalApprox.lfpApprox_add_one : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α},
  x ≤ f x → ∀ (a : Ordinal.{u}), OrdinalApprox.lfpApprox f x (a + 1) = f (OrdinalApprox.lfpApprox f x a)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyι_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] {Z : C}
  (h : S₂.opcycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ)
      (CategoryTheory.CategoryStruct.comp S₂.homologyι h) =
    CategoryTheory.CategoryStruct.comp S₁.homologyι
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap φ) h)
-- Mathlib.Algebra.Regular.SMul
/-- The `0` element is not `M`-regular, on a non-trivial module.  -/
IsSMulRegular.not_zero : ∀ {R : Type u_1} {M : Type u_3} [inst : MonoidWithZero R] [inst_1 : Zero M] [inst_2 : MulActionWithZero R M]
  [nM : Nontrivial M], ¬IsSMulRegular M 0
-- Mathlib.Algebra.Notation.Prod
Prod.fst_sub : ∀ {G : Type u_8} {H : Type u_9} [inst : Sub G] [inst_1 : Sub H] (a b : G × H), (a - b).1 = a.1 - b.1
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- The composition of `C^n` functions at points in domains is `C^n`.  -/
ContDiffWithinAt.comp_inter_of_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {s : Set E} {t : Set F} {g : F → G}
  {f : E → F} {y : F} (x : E),
  ContDiffWithinAt 𝕜 n g t y → ContDiffWithinAt 𝕜 n f s x → f x = y → ContDiffWithinAt 𝕜 n (g ∘ f) (s ∩ f ⁻¹' t) x
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.evalMonoidHom.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : MulOneClass Y] (x : X),
  LocallyConstant.evalMonoidHom x = (Pi.evalMonoidHom (fun a => Y) x).comp LocallyConstant.coeFnMonoidHom
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Algebra.intNorm_eq_norm : ∀ (A : Type u_1) (B : Type u_6) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : IsIntegrallyClosed A] [inst_4 : IsDomain A] [inst_5 : IsDomain B] [inst_6 : IsIntegrallyClosed B]
  [inst_7 : Algebra.IsIntegral A B] [inst_8 : Module.IsTorsionFree A B] [Module.Free A B] [Module.Finite A B],
  Algebra.intNorm A B = Algebra.norm A
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
/-- A matrix `M` is right-separating if for all `v ≠ 0`, there is a `w` with `v * M * w ≠ 0`.  -/
Matrix.SeparatingLeft : {m : Type u_1} →
  {n : Type u_2} → {R : Type u_3} → [NonUnitalNonAssocSemiring R] → [Finite m] → [Finite n] → Matrix m n R → Prop
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.merge_lemma : ∀ {a b c : ℕ}, 3 * a < b + c + 1 → b ≤ 3 * c → 2 * (a + b) ≤ 9 * c + 5
-- Mathlib.NumberTheory.ModularForms.Basic
SlashInvariantForm.prod.congr_simp : ∀ {ι : Type} {s s_1 : Finset ι} (e_s : s = s_1) {k : ι → ℤ} (m : ℤ) (hm : m = ∑ i ∈ s, k i)
  {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.HasDetPlusMinusOne] (f f_1 : (i : ι) → SlashInvariantForm Γ (k i)),
  f = f_1 → SlashInvariantForm.prod m hm f = SlashInvariantForm.prod m ⋯ f_1
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_add_eq_right_of_degree_lt : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.degree < q.degree → (p + q).natDegree = q.natDegree
-- Mathlib.CategoryTheory.Functor.Basic
CategoryTheory.Functor.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (obj : C → D) →
          (map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)) →
            autoParam (∀ (X : C), map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (obj X))
                CategoryTheory.Functor.map_id._autoParam →
              autoParam
                  (∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
                    map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (map f) (map g))
                  CategoryTheory.Functor.map_comp._autoParam →
                CategoryTheory.Functor C D
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.ofZeroDvd.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.ofZeroDvd c) = 1 + sizeOf c
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- Use as `letI := upgradeStandardBorel α` to endow a standard Borel space `α` with
a compatible Polish topology.

Warning: following this with `borelize α` will cause an error. Instead, one can
rewrite with `eq_borel_upgradeStandardBorel α`.
TODO: fix the corresponding bug in `borelize`.  -/
upgradeStandardBorel : (α : Type u_1) → [inst : MeasurableSpace α] → [h : StandardBorelSpace α] → UpgradedStandardBorel α
-- Mathlib.Topology.Semicontinuity.Defs
LowerSemicontinuousWithinAt.congr_of_eventuallyEq : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f g : α → β} {s : Set α} {a : α},
  LowerSemicontinuousWithinAt f s a → a ∈ s → f =ᶠ[nhdsWithin a s] g → LowerSemicontinuousWithinAt g s a
-- Mathlib.MeasureTheory.Function.AEEqFun.DomAct
DomMulAct.smul_aeeqFun_aeeq : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace β] [inst_2 : SMul M α] [inst_3 : MeasurableConstSMul M α]
  [inst_4 : MeasureTheory.SMulInvariantMeasure M α μ] (c : Mᵈᵐᵃ) (f : α →ₘ[μ] β),
  ↑(c • f) =ᵐ[μ] fun x => ↑f (DomMulAct.mk.symm c • x)
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.HasSeparator.hasSeparator : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} [self : CategoryTheory.HasSeparator C],
  ∃ G, CategoryTheory.IsSeparator G