mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.ULift
ULift.vadd.eq_1 : ∀ {α : Type u} {β : Type v} [inst : VAdd β α], ULift.vadd = { vadd := fun n x => { down := n +ᵥ x.down } }
-- Mathlib.Algebra.Module.Injective
Module.Baer.ExtensionOf.mk : {R : Type u} →
  [inst : Ring R] →
    {Q : Type v} →
      [inst_1 : AddCommGroup Q] →
        [inst_2 : Module R Q] →
          {M : Type u_1} →
            {N : Type u_2} →
              [inst_3 : AddCommGroup M] →
                [inst_4 : AddCommGroup N] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module R N] →
                      {i : M →ₗ[R] N} →
                        {f : M →ₗ[R] Q} →
                          (toLinearPMap : N →ₗ.[R] Q) →
                            (le : i.range ≤ toLinearPMap.domain) →
                              (∀ (m : M), f m = ↑toLinearPMap ⟨i m, ⋯⟩) → Module.Baer.ExtensionOf i f
-- Mathlib.CategoryTheory.Shift.SingleFunctorsLift
CategoryTheory.SingleFunctors.lift.shiftIso.congr_simp : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{u_5, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_6, u_2} D] [inst_2 : CategoryTheory.Category.{u_7, u_3} E] {A : Type u_4}
  [inst_3 : AddMonoid A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : CategoryTheory.HasShift E A]
  {F : CategoryTheory.SingleFunctors C E A} {G : CategoryTheory.Functor D E} [inst_6 : G.CommShift A] [inst_7 : G.Full]
  [inst_8 : G.Faithful] {Φ : A → CategoryTheory.Functor C D} (hΦ hΦ_1 : (a : A) → (Φ a).comp G ≅ F.functor a),
  hΦ = hΦ_1 →
    ∀ (n a a' : A) (h : n + a = a'),
      CategoryTheory.SingleFunctors.lift.shiftIso hΦ n a a' h =
        CategoryTheory.SingleFunctors.lift.shiftIso hΦ_1 n a a' h
-- Mathlib.Data.Fin.Basic
Fin.coe_int_sub_eq_mod : ∀ {n : ℕ} (u v : Fin n), ↑↑(u - v) = (↑↑u - ↑↑v) % ↑n
-- Lean.Meta.Tactic.Grind.MarkNestedSubsingletons
_private.Lean.Meta.Tactic.Grind.MarkNestedSubsingletons.0.Lean.Meta.Grind.markNestedProof : Lean.Expr → Lean.Meta.Grind.M✝ Lean.Expr
-- Lean.Linter.Init
/-- If `linterOption` is enabled, print a linter warning message at the position determined by `stx`.

Whether a linter option is enabled or not is determined by the following sequence:
1. If it is set, then the value determines whether or not it is enabled.
2. Otherwise, if `linter.all` is set, then its value determines whether or not the option is enabled.
3. Otherwise, if any of the linter sets containing the option is enabled, it is enabled.
  (Only enabled linter sets are considered: explicitly disabling a linter set
  will revert the linters it contains to their default behavior.)
4. Otherwise, the default value determines whether or not it is enabled.
 -/
Lean.Linter.logLintIf : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadLog m] →
      [Lean.AddMessageContext m] →
        [Lean.MonadOptions m] → [Lean.MonadEnv m] → Lean.Option Bool → Lean.Syntax → Lean.MessageData → m Unit
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.differentiableOn_derivWeierstrassPExcept : ∀ (L : PeriodPair) (l₀ : ℂ), DifferentiableOn ℂ (L.derivWeierstrassPExcept l₀) (↑L.lattice \ {l₀})ᶜ
-- Mathlib.AlgebraicTopology.SimplicialSet.Subdivision
/-- The natural isomorphism `stdSimplex ⋙ sd ≅ SimplexCategory.sd`.  -/
SSet.stdSimplex.sdIso : CategoryTheory.Functor.comp SSet.stdSimplex SSet.sd ≅ SimplexCategory.sd
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.of_sub_left : ∀ {α : Type u_2} [inst : Sub α] {f g : Filter α}, (f - g).NeBot → f.NeBot
-- Init.Data.Slice.Array.Lemmas
Array.toArray_mkSlice_roi : ∀ {α : Type u_1} {xs : Array α} {lo : ℕ}, Std.Slice.toArray (Std.Roi.Sliceable.mkSlice xs lo<...*) = xs.drop (lo + 1)
-- Mathlib.Algebra.Ring.BooleanRing
OrderIso.asBoolAlgAsBoolRing_symm_apply : ∀ (α : Type u_4) [inst : BooleanAlgebra α] (a : α),
  (RelIso.symm (OrderIso.asBoolAlgAsBoolRing α)) a = toBoolAlg (toBoolRing a)
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.copy_eq : ∀ {K : Type u} [inst : DivisionRing K] (S : Subfield K) (s : Set K) (hs : s = ↑S), S.copy s hs = S
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.equivHomotopy_apply_of_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} {φ₁ φ₂ : F ⟶ G} (h : φ₁ = φ₂),
  ↑((CochainComplex.HomComplex.Cochain.equivHomotopy φ₁ φ₂) (Homotopy.ofEq h)) = 0
-- Mathlib.Condensed.Light.Monoidal
LightCondensed.instMonoidalClosedSheafLightProfiniteCoherentTopologyModuleCat : (R : Type u) →
  [inst : CommRing R] →
    CategoryTheory.MonoidalClosed (CategoryTheory.Sheaf (CategoryTheory.coherentTopology LightProfinite) (ModuleCat R))
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.star_mulVec : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalSemiring α] [inst_1 : Fintype n] [inst_2 : StarRing α]
  (M : Matrix m n α) (v : n → α), star (M.mulVec v) = Matrix.vecMul (star v) M.conjTranspose
-- Lean.Hygiene
Lean.NameSanitizerState.mk.injEq : ∀ (options : Lean.Options) (nameStem2Idx : Lean.NameMap ℕ) (userName2Sanitized : Lean.NameMap Lean.Name)
  (options_1 : Lean.Options) (nameStem2Idx_1 : Lean.NameMap ℕ) (userName2Sanitized_1 : Lean.NameMap Lean.Name),
  ({ options := options, nameStem2Idx := nameStem2Idx, userName2Sanitized := userName2Sanitized } =
      { options := options_1, nameStem2Idx := nameStem2Idx_1, userName2Sanitized := userName2Sanitized_1 }) =
    (options = options_1 ∧ nameStem2Idx = nameStem2Idx_1 ∧ userName2Sanitized = userName2Sanitized_1)
-- Init.WF
Acc.transGen : ∀ {α : Sort u_1} {r : α → α → Prop} {a : α}, Acc r a → Acc (Relation.TransGen r) a
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
/-- Given a morphism of simplicial sets `f : X ⟶ Y` whose
range is `≤ B` for some `B : Y.Subcomplex`, this is the
induced morphism `X ⟶ B`.  -/
SSet.Subcomplex.lift : {X Y : SSet} → (f : X ⟶ Y) → {B : Y.Subcomplex} → SSet.Subcomplex.range f ≤ B → (X ⟶ B.toSSet)
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
/-- An equivalence between the "proxy type" `CategoryTheory.Limits.WalkingMulticospan.proxyType` and `CategoryTheory.Limits.WalkingMulticospan`. The proxy type is a reducible definition that represents the inductive type using `Unit`, `PLift`, `Sigma`, `Empty`, and `Sum` (and whatever other inductive types appear within the inductive type), and the intended use is to define typeclass instances uses pre-existing instances on these. (Generated by the `proxy_equiv%` elaborator.) -/
CategoryTheory.Limits.WalkingMulticospan.proxyTypeEquiv : (J : CategoryTheory.Limits.MulticospanShape) → J.L ⊕ J.R ≃ CategoryTheory.Limits.WalkingMulticospan J
-- Mathlib.Analysis.Normed.Group.Constructions
/-- The $L^1$ norm is less than the $L^\infty$ norm scaled
by the cardinality.  -/
Pi.sum_norm_apply_le_norm : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddGroup (G i)]
  (f : (i : ι) → G i), ∑ i, ‖f i‖ ≤ Fintype.card ι • ‖f‖
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.grindPatternCnstrs.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.RamificationInertia.Inertia
/-- **Alias** of `Ideal.inertiaDeg_eq_of_isMaximal`. -/
Ideal.inertiaDeg'_eq_of_isMaximal : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  (q : Ideal S) [inst_3 : q.LiesOver p] [p.IsMaximal] [q.IsMaximal], q.inertiaDeg R = Module.finrank (R ⧸ p) (S ⧸ q)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.ValueGroupWithZero.mk_eq_valuation : ∀ {K : Type u_3} [inst : DivisionRing K] [inst_1 : ValuativeRel K] (x : K) (y : ↥(ValuativeRel.posSubmonoid K)),
  ValuativeRel.ValueGroupWithZero.mk x y = (ValuativeRel.valuation K) (x / ↑y)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.pushoutIsoOpPullback_inv_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Z) (g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushout f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutIsoOpPullback f g).inv.unop
      (CategoryTheory.Limits.pullback.fst f.unop g.unop) =
    (CategoryTheory.Limits.pushout.inl f g).unop
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.instT2Space : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4}
  {F : Type u_5} [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜₂ F]
  [inst_6 : TopologicalSpace E] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F] [ContinuousSMul 𝕜₁ E]
  [T2Space F], T2Space (E →SL[σ] F)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α (fun x => Unit) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  Std.ExtDTreeMap.Const.get? (Std.ExtDTreeMap.Const.insertManyIfNewUnit t l) k =
    if k ∈ t ∨ l.contains k = true then some () else none
-- Mathlib.RingTheory.LocalRing.Module
/-- If `M` is of finite presentation over a local ring `(R, 𝔪, k)` such that
`𝔪 ⊗ M → M` is injective, then every family of elements that is a `k`-basis of
`k ⊗ M` is an `R`-basis of `M`.  -/
Module.exists_basis_of_basis_baseChange : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsLocalRing R] [Module.FinitePresentation R M] {ι : Type u_5} (v : ι → M),
  LinearIndependent (IsLocalRing.ResidueField R) (⇑((TensorProduct.mk R (IsLocalRing.ResidueField R) M) 1) ∘ v) →
    Submodule.span (IsLocalRing.ResidueField R)
          (Set.range (⇑((TensorProduct.mk R (IsLocalRing.ResidueField R) M) 1) ∘ v)) =
        ⊤ →
      Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype (IsLocalRing.maximalIdeal R))) →
        ∃ b, ∀ (i : ι), b i = v i
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.pseudofunctor_left_unitality : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Modules.pullbackComp f (CategoryTheory.CategoryStruct.id Y)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (AlgebraicGeometry.Scheme.Modules.pullbackId Y).hom
          (AlgebraicGeometry.Scheme.Modules.pullback f))
        (AlgebraicGeometry.Scheme.Modules.pullback f).leftUnitor.hom) =
    CategoryTheory.eqToHom ⋯
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.congr_trans_rTensor : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : AddCommMonoid S] [inst_6 : Module R M] [inst_7 : Module R N] [inst_8 : Module R S] [inst_9 : Module R P]
  [inst_10 : Module R Q] (f' : P ≃ₗ[R] S) (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q),
  TensorProduct.congr f g ≪≫ₗ LinearEquiv.rTensor Q f' = TensorProduct.congr (f ≪≫ₗ f') g
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.comp_reflectsColimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} {E : Type u₃}
  [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E)
  [CategoryTheory.Limits.ReflectsColimit K F] [CategoryTheory.Limits.ReflectsColimit (K.comp F) G],
  CategoryTheory.Limits.ReflectsColimit K (F.comp G)
-- Mathlib.Analysis.Convex.AmpleSet
/-- The union of two ample sets is ample.  -/
AmpleSet.union : ∀ {F : Type u_1} [inst : AddCommGroup F] [inst_1 : Module ℝ F] [inst_2 : TopologicalSpace F] {s t : Set F},
  AmpleSet s → AmpleSet t → AmpleSet (s ∪ t)
-- Mathlib.Data.Set.MemPartition
disjoint_memPartition : ∀ {α : Type u_1} (f : ℕ → Set α) (n : ℕ) {u v : Set α},
  u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
-- Init.Data.Order.Classes
Std.LawfulOrderMax.toMaxEqOr : ∀ {α : Type u} {inst : Max α} {inst_1 : LE α} [self : Std.LawfulOrderMax α], Std.MaxEqOr α
-- Lean.Compiler.ExternAttr
Lean.ExternEntry.inline.sizeOf_spec : ∀ (backend : Lean.Name) (pattern : String),
  sizeOf (Lean.ExternEntry.inline backend pattern) = 1 + sizeOf backend + sizeOf pattern
-- Mathlib.Topology.Algebra.FilterBasis
ModuleFilterBasis.mk.sizeOf_spec : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : TopologicalSpace R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : SizeOf R] [inst_5 : SizeOf M] (toAddGroupFilterBasis : AddGroupFilterBasis M)
  (smul' : ∀ {U : Set M}, U ∈ toAddGroupFilterBasis.sets → ∃ V ∈ nhds 0, ∃ W ∈ toAddGroupFilterBasis.sets, V • W ⊆ U)
  (smul_left' :
    ∀ (x₀ : R) {U : Set M},
      U ∈ toAddGroupFilterBasis.sets → ∃ V ∈ toAddGroupFilterBasis.sets, V ⊆ (fun x => x₀ • x) ⁻¹' U)
  (smul_right' : ∀ (m₀ : M) {U : Set M}, U ∈ toAddGroupFilterBasis.sets → ∀ᶠ (x : R) in nhds 0, x • m₀ ∈ U),
  sizeOf
      { toAddGroupFilterBasis := toAddGroupFilterBasis, smul' := smul', smul_left' := smul_left',
        smul_right' := smul_right' } =
    1 + sizeOf toAddGroupFilterBasis
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.prodOpEquiv_functor_obj : ∀ (C : Type u₃) [inst : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [inst_1 : CategoryTheory.Category.{v₄, u₄} D]
  (X : (C × D)ᵒᵖ),
  (CategoryTheory.prodOpEquiv C).functor.obj X = (Opposite.op (Opposite.unop X).1, Opposite.op (Opposite.unop X).2)
-- Std.Sat.CNF.Basic
Std.Sat.CNF.Internal.mem_iff : ∀ {α : Type u_1} {c : Std.Sat.CNF.Clause α} {f : Std.Sat.CNF α}, c ∈ f ↔ c ∈ f.clauses
-- Init.Data.SInt.Lemmas
Int8.toInt_bmod : ∀ (x : Int8), x.toInt.bmod 256 = x.toInt
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instNonUnitalCommSemiringOfNonUnitalRingHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → NonUnitalCommSemiring (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] →
                      NonUnitalCommSemiring (DirectLimit G f)
-- Mathlib.Algebra.Notation.Support
Function.support_along_fiber_subset : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : Zero M] (f : ι × κ → M) (i : ι),
  (Function.support fun j => f (i, j)) ⊆ Prod.snd '' Function.support f
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
isTranscendenceBasis_iff_maximal : ∀ {R : Type u_3} {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {s : Set A},
  IsTranscendenceBasis R Subtype.val ↔ Maximal (AlgebraicIndepOn R id) s
-- Mathlib.Tactic.Ring.Common
/-- Evaluate the product of two coefficients.  -/
Mathlib.Tactic.Ring.Common.RingCompute.mul : {u : Lean.Level} →
  {α : Q(Type u)} →
    {BaseType : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompute BaseType sα →
          {x y : Q(«$α»)} →
            BaseType x → BaseType y → Lean.MetaM (Mathlib.Tactic.Ring.Common.Result BaseType q(«$x» * «$y»))
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.ae_restrict_iff : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {p : α → Prop},
  MeasurableSet {x | p x} → ((∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → p x)
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.pi_bot : ∀ {ι : Type u_4} {M : ι → Type u_5} [inst : (i : ι) → MulOneClass (M i)], (Submonoid.pi Set.univ fun i => ⊥) = ⊥
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
prod_mem_nonZeroDivisors_of_mem_nonZeroDivisors : ∀ {M₀ : Type u_1} [inst : CommMonoidWithZero M₀] {ι : Type u_2} {s : Finset ι} {f : ι → M₀},
  (∀ i ∈ s, f i ∈ nonZeroDivisors M₀) → ∏ i ∈ s, f i ∈ nonZeroDivisors M₀
-- Mathlib.Topology.Separation.Basic
specializes_iff_not_disjoint : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] {x y : X}, x ⤳ y ↔ ¬Disjoint (nhds x) (nhds y)
-- Mathlib.Logic.Encodable.Basic
Encodable.decode₂.eq_1 : ∀ (α : Type u_3) [inst : Encodable α] (n : ℕ),
  Encodable.decode₂ α n = (Encodable.decode n).bind (Option.guard fun a => decide (Encodable.encode a = n))
-- Mathlib.Logic.Function.Basic
Function.surjective_of_right_cancellable_Prop : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, (∀ (g₁ g₂ : β → Prop), g₁ ∘ f = g₂ ∘ f → g₁ = g₂) → Function.Surjective f
-- Mathlib.Algebra.Ring.Parity
odd_add_two : ∀ {α : Type u_2} [inst : Ring α] {a : α}, Odd (a + 2) ↔ Odd a
-- Mathlib.Topology.Connected.TotallyDisconnected
/-- A space is totally disconnected if all of its connected components are singletons.  -/
TotallyDisconnectedSpace : (α : Type u) → [TopologicalSpace α] → Prop
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.toList_of_add : ∀ {α : Type u_1} (x : α) (xs : FreeAddMonoid α),
  FreeAddMonoid.toList (FreeAddMonoid.of x + xs) = x :: FreeAddMonoid.toList xs
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.map_fst_toArray_eq_keysArray : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp},
  Array.map Prod.fst (Std.DTreeMap.Const.toArray t) = t.keysArray
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Prequotient.of.injEq : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (j : J) (x : ↑(F.obj j))
  (j_1 : J) (x_1 : ↑(F.obj j_1)),
  (RingCat.Colimits.Prequotient.of j x = RingCat.Colimits.Prequotient.of j_1 x_1) = (j = j_1 ∧ x ≍ x_1)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.inclHomEquiv_apply_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) (Y : CategoryTheory.Limits.FormalCoproduct C)
  (f : (CategoryTheory.Limits.FormalCoproduct.incl C).obj X ⟶ Y),
  ((CategoryTheory.Limits.FormalCoproduct.inclHomEquiv X Y) f).fst = f.f PUnit.unit
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.fold_eq_foldl_keysArray : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {δ : Type w}
  {f : δ → α → δ} {init : δ}, m.WF → Std.DHashMap.Raw.fold (fun d a x => f d a) init m = Array.foldl f init m.keysArray
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
/-- Variant of `mlieBracketWithin_congr_set` where one requires the sets to coincide only in
the complement of a point.  -/
VectorField.mlieBracketWithin_congr_set' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s t : Set M} {x : M} {V W : (x : M) → TangentSpace I x}
  (y : M), s =ᶠ[nhdsWithin x {y}ᶜ] t → VectorField.mlieBracketWithin I V W s x = VectorField.mlieBracketWithin I V W t x
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instCofibrationICofibrationsTrivialFibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  {X Y : C} (f : X ⟶ Y)
  (h : (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) f),
  HomotopicalAlgebra.Cofibration h.i
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MRefinePat.tuple : List Lean.Parser.Tactic.MRefinePat → Lean.Parser.Tactic.MRefinePat
-- Mathlib.RingTheory.Polynomial.Pochhammer
Nat.cast_descFactorial : ∀ (S : Type u_1) [inst : Semiring S] (a b : ℕ),
  ↑(a.descFactorial b) = Polynomial.eval (↑(a - (b - 1))) (ascPochhammer S b)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.abs_det_completeBasis_equivFunL_symm : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  |(↑(NumberField.mixedEmbedding.fundamentalCone.completeBasis K).equivFunL.symm).det| =
    ↑(Module.finrank ℚ K) * NumberField.Units.regulator K
-- Mathlib.Topology.Algebra.Monoid
Specializes.add : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Add M] [ContinuousAdd M] {a b c d : M},
  a ⤳ b → c ⤳ d → (a + c) ⤳ (b + d)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_filterMap : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w}
  [inst : Std.TransOrd α] [inst_1 : Std.LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} {k : α} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl.getKey? k =
    (t.getKey? k).pfilter fun x h' => (f x (t.get x ⋯)).isSome
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.liftAux_eq : ∀ (R : Type u_1) {X : Type u_2} [inst : CommSemiring R] {A : Type u_3} [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (f : X → A), FreeAlgebra.liftAux✝ R f = (FreeAlgebra.lift R) f
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.mgf_pos' : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ},
  μ ≠ 0 → MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ → 0 < ProbabilityTheory.mgf X μ t
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValue?_map : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [EquivBEq α] {f : α → β → γ} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α},
      Std.Internal.List.getValue? k (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l) =
        Option.pmap (fun v h => f (Std.Internal.List.getKey k l h) v) (Std.Internal.List.getValue? k l) ⋯
-- Std.Time.Format.Modifier
Std.Time.OffsetZ.noConfusionType : Sort v✝ → Std.Time.OffsetZ → Std.Time.OffsetZ → Sort v✝
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.piLinearMap_apply_apply_apply : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₁' : ι → Type v₁'} {M₂ : Type v₂} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → AddCommMonoid (M₁' i)] [inst_6 : (i : ι) → Module R (M₁' i)]
  (g : MultilinearMap R M₁' M₂) (a : (i : ι) → (fun i => M₁ i →ₗ[R] M₁' i) i) (m : (i : ι) → M₁ i),
  ((MultilinearMap.piLinearMap g) a) m = g fun i => (a i) (m i)
-- Mathlib.Algebra.Order.Monoid.TypeTags
Additive.isOrderedCancelAddMonoid : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedCancelMonoid α],
  IsOrderedCancelAddMonoid (Additive α)
-- Mathlib.Algebra.Module.LocalizedModule.Int
/-- A choice of a common multiple of the denominators of a finite set of fractions.  -/
IsLocalizedModule.commonDenomOfFinset : {R : Type u_1} →
  [inst : CommSemiring R] →
    (S : Submonoid R) →
      {M : Type u_2} →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            {M' : Type u_3} →
              [inst_3 : AddCommMonoid M'] →
                [inst_4 : Module R M'] → (f : M →ₗ[R] M') → [IsLocalizedModule S f] → Finset M' → ↥S
-- Init.Data.List.Sublist
List.append_sublist_append_left : ∀ {α : Type u_1} {l₁ l₂ : List α} (l : List α), (l ++ l₁).Sublist (l ++ l₂) ↔ l₁.Sublist l₂
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.bound_aux : ∀ {n d : ℕ}, d ≠ 0 → 2 ≤ n → ↑d ^ (n - 2) / ↑n ≤ ↑(rothNumberNat ((2 * d - 1) ^ n))
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.prod_map_ite : ∀ {α : Type u_2} {M : Type u_4} [inst : CommMonoid M] (p : α → Prop) [inst_1 : DecidablePred p] (f g : α → M)
  (l : List α),
  (List.map (fun a => if p a then f a else g a) l).prod =
    (List.map f (List.filter (fun b => decide (p b)) l)).prod * (List.map g (List.filter (fun a => decide ¬p a) l)).prod
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_zero : Real.log 0 = 0