mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.inv_prodComparison_map_snd_assoc : ∀ {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) (A B : C)
  [inst_4 : CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B)] {Z : D}
  (h : F.obj B ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.inv (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B))
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.SemiCartesianMonoidalCategory.snd A B)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd (F.obj A) (F.obj B)) h
-- Mathlib.Algebra.Group.WithOne.Basic
WithOne.instInvolutiveInv.eq_1 : ∀ {α : Type u} [inst : InvolutiveInv α], WithOne.instInvolutiveInv = { toInv := WithOne.instInv, inv_inv := ⋯ }
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.compContinuousLinearMap.congr_simp : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} {G : Type x} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E]
  [inst_6 : AddCommMonoid F] [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F]
  [inst_10 : ContinuousConstSMul 𝕜 F] [inst_11 : AddCommMonoid G] [inst_12 : Module 𝕜 G] [inst_13 : TopologicalSpace G]
  [inst_14 : ContinuousAdd G] [inst_15 : ContinuousConstSMul 𝕜 G] (p p_1 : FormalMultilinearSeries 𝕜 F G),
  p = p_1 →
    ∀ (u u_1 : E →L[𝕜] F), u = u_1 → ∀ (n : ℕ), p.compContinuousLinearMap u n = p_1.compContinuousLinearMap u_1 n
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftIso.eq_1 : ∀ {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] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂),
  CategoryTheory.Comma.mapLeftIso R i =
    { functor := CategoryTheory.Comma.mapLeft R i.inv, inverse := CategoryTheory.Comma.mapLeft R i.hom,
      unitIso :=
        (CategoryTheory.Comma.mapLeftId L₁ R).symm ≪≫
          CategoryTheory.Comma.mapLeftEq R (CategoryTheory.CategoryStruct.id L₁)
              (CategoryTheory.CategoryStruct.comp i.hom i.inv) ⋯ ≪≫
            CategoryTheory.Comma.mapLeftComp R i.hom i.inv,
      counitIso :=
        (CategoryTheory.Comma.mapLeftComp R i.inv i.hom).symm ≪≫
          CategoryTheory.Comma.mapLeftEq R (CategoryTheory.CategoryStruct.comp i.inv i.hom)
              (CategoryTheory.CategoryStruct.id L₂) ⋯ ≪≫
            CategoryTheory.Comma.mapLeftId L₂ R,
      functor_unitIso_comp := ⋯ }
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
eq_one_of_mul_le_one_right : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : PartialOrder α] [MulRightMono α] {a b : α},
  1 ≤ a → 1 ≤ b → a * b ≤ 1 → b = 1
-- Init.Data.List.TakeDrop
List.splitAt.eq_1 : ∀ {α : Type u} (n : ℕ) (l : List α), List.splitAt n l = List.splitAt.go l l n []
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.instLawfulBackwardPatternModelForallCharProp : ∀ {p : Char → Prop} [inst : DecidablePred p], String.Slice.Pattern.Model.LawfulBackwardPatternModel p
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
AlgebraicGeometry.IsImmersion.isStableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.IsImmersion
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
AddChar.doubleDualEmb_injective : ∀ {α : Type u_1} [inst : AddCommGroup α] [Finite α], Function.Injective ⇑AddChar.doubleDualEmb
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiffOn_finprod : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {s : Set M} {f : ι → M → G},
  (LocallyFinite fun i => Function.mulSupport (f i)) →
    (∀ (i : ι), ContMDiffOn I' I n (f i) s) → ContMDiffOn I' I n (fun x => ∏ᶠ (i : ι), f i x) s
-- Mathlib.MeasureTheory.Constructions.Cylinders
/-- The cylinders of a product space indexed by `ℕ` can be seen as depending on the first
coordinates.  -/
MeasureTheory.measurableCylinders_nat : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)],
  MeasureTheory.measurableCylinders X = ⋃ a, ⋃ S, ⋃ (_ : MeasurableSet S), {MeasureTheory.cylinder (Finset.Iic a) S}
-- Std.Http.Data.Response
/-- The response status-line information.
 -/
Std.Http.Response.Builder.line : Std.Http.Response.Builder → Std.Http.Response.Head
-- Mathlib.Analysis.Normed.MulAction
/-- Left multiplication is bounded.  -/
NonUnitalSeminormedRing.isBoundedSMul : ∀ {α : Type u_1} [inst : NonUnitalSeminormedRing α], IsBoundedSMul α α
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ResolvableCompletionItem : Type
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.coe_one : ∀ {α : Type u} [inst : PseudoEMetricSpace α], ⇑1 = id
-- Qq.Macro
Qq.Impl.MVarSynth.term.sizeOf_spec : ∀ (quotedType : Lean.Expr) (unquotedMVar : Lean.MVarId),
  sizeOf (Qq.Impl.MVarSynth.term quotedType unquotedMVar) = 1 + sizeOf quotedType + sizeOf unquotedMVar
-- Mathlib.Order.Basic
Pi.hnot_apply : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : (i : ι) → HNot (π i)] (x : (i : ι) → π i) (i : ι), (￢x) i = ￢x i
-- Mathlib.Data.Complex.Basic
Complex.instInhabited : Inhabited ℂ
-- Init.Data.List.Basic
List.reverseAux.eq_def : ∀ {α : Type u} (x x_1 : List α),
  x.reverseAux x_1 =
    match x, x_1 with
    | [], r => r
    | a :: l, r => l.reverseAux (a :: r)
-- Mathlib.SetTheory.ZFC.Rank
PSet.rank_congr : ∀ {x y : PSet.{u_1}}, x.Equiv y → x.rank = y.rank
-- Mathlib.FieldTheory.Perfect
MonoidHom.map_iterate_frobeniusEquiv_symm : ∀ {R : Type u_2} {S : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] (p : ℕ) [inst_2 : ExpChar R p]
  [inst_3 : PerfectRing R p] [inst_4 : ExpChar S p] [inst_5 : PerfectRing S p] (f : R →* S) (n : ℕ) (x : R),
  f ((⇑(frobeniusEquiv R p).symm)^[n] x) = (⇑(frobeniusEquiv S p).symm)^[n] (f x)
-- Mathlib.Analysis.Calculus.FDeriv.Linear
ContinuousLinearMap.fderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (f : E →L[𝕜] F) {x : E} [ContinuousAdd E] [ContinuousSMul 𝕜 E] [ContinuousAdd F]
  [ContinuousSMul 𝕜 F] [T2Space F], fderiv 𝕜 (⇑f) x = f
-- Mathlib.Data.QPF.Univariate.Basic
QPF.abs_map : ∀ {F : Type u → Type v} [self : QPF F] {α β : Type u} (f : α → β) (p : ↑(QPF.P F) α),
  QPF.abs ((QPF.P F).map f p) = f <$> QPF.abs p
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.mk_le_mk : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L M : Sublattice α} (hL_compl : ∀ {a : α}, a ∈ L.carrier → aᶜ ∈ L.carrier)
  (hL_bot : ⊥ ∈ L.carrier) (hM_compl : ∀ {a : α}, a ∈ M.carrier → aᶜ ∈ M.carrier) (hM_bot : ⊥ ∈ M.carrier),
  { toSublattice := L, compl_mem' := hL_compl, bot_mem' := hL_bot } ≤
      { toSublattice := M, compl_mem' := hM_compl, bot_mem' := hM_bot } ↔
    L ≤ M
-- Mathlib.RingTheory.SimpleModule.Basic
isSemisimpleModule_biSup_of_isSemisimpleModule_submodule : ∀ {ι : Type u_1} {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {s : Set ι} {p : ι → Submodule R M}, (∀ i ∈ s, IsSemisimpleModule R ↥(p i)) → IsSemisimpleModule R ↥(⨆ i ∈ s, p i)
-- Init.Data.UInt.Lemmas
UInt16.neg_mul : ∀ (a b : UInt16), -a * b = -(a * b)
-- Mathlib.MeasureTheory.Group.ModularCharacter
/-- The modular character homomorphism. The underlying function is `modularCharacterFun`, which is
`g ↦ μ (· * g⁻¹) / μ`, where `μ` is a left Haar measure.
 -/
MeasureTheory.Measure.modularCharacter : {G : Type u_1} →
  [inst : TopologicalSpace G] → [inst_1 : Group G] → [IsTopologicalGroup G] → [LocallyCompactSpace G] → G →* NNReal
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the largest key that is less than or equal to the
given key, returning `none` if no such key exists.
 -/
Std.TreeMap.getKeyLE? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → Option α
-- Mathlib.Algebra.MvPolynomial.PDeriv
MvPolynomial.pderiv_C_mul : ∀ {R : Type u} {σ : Type v} {a : R} [inst : CommSemiring R] {f : MvPolynomial σ R} {i : σ},
  (MvPolynomial.pderiv i) (MvPolynomial.C a * f) = MvPolynomial.C a * (MvPolynomial.pderiv i) f
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
  [inst_2 : SizeOf C] (φQ : h₁.Q ⟶ h₂.Q) (φH : h₁.H ⟶ h₂.H)
  (commp :
    autoParam (CategoryTheory.CategoryStruct.comp h₁.p φQ = CategoryTheory.CategoryStruct.comp φ.τ₂ h₂.p)
      CategoryTheory.ShortComplex.RightHomologyMapData.commp._autoParam)
  (commg' :
    autoParam (CategoryTheory.CategoryStruct.comp φQ h₂.g' = CategoryTheory.CategoryStruct.comp h₁.g' φ.τ₃)
      CategoryTheory.ShortComplex.RightHomologyMapData.commg'._autoParam)
  (commι :
    autoParam (CategoryTheory.CategoryStruct.comp φH h₂.ι = CategoryTheory.CategoryStruct.comp h₁.ι φQ)
      CategoryTheory.ShortComplex.RightHomologyMapData.commι._autoParam),
  sizeOf { φQ := φQ, φH := φH, commp := commp, commg' := commg', commι := commι } =
    1 + sizeOf φQ + sizeOf φH + sizeOf commp + sizeOf commg' + sizeOf commι
-- Mathlib.FieldTheory.IntermediateField.Basic
AlgHom.fieldRange_toSubfield : ∀ {K : Type u_1} {L : Type u_2} {L' : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field L']
  [inst_3 : Algebra K L] [inst_4 : Algebra K L'] (f : L →ₐ[K] L'), f.fieldRange.toSubfield = (↑f).fieldRange
-- Std.Data.HashMap.Lemmas
Std.HashMap.distinct_keys_toList : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  List.Pairwise (fun a b => (a.1 == b.1) = false) m.toList
-- Mathlib.Algebra.Group.Prod
Prod.instCancelCommMonoid.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : CancelCommMonoid M] [inst_1 : CancelCommMonoid N],
  Prod.instCancelCommMonoid = { toCommMonoid := Prod.instCommMonoid, toIsLeftCancelMul := ⋯ }
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.mk : {m : Type w → Type w'} → {α : Type w} → (Property : α → Prop) → m (Subtype Property) → Std.Iterators.PostconditionT m α
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instToJsonChangeAnnotationSupport.toJson : Lean.Lsp.ChangeAnnotationSupport → Lean.Json
-- Init.Data.List.MinMax
List.max?_replicate : ∀ {α : Type u_1} [inst : Max α] [Std.IdempotentOp max] {n : ℕ} {a : α},
  (List.replicate n a).max? = if n = 0 then none else some a
-- Mathlib.Topology.Category.TopCat.Yoneda
/-- A universe polymorphic "Yoneda presheaf" on `C` given by continuous maps into a topological space
`Y`.
 -/
ContinuousMap.yonedaPresheaf : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor C TopCat →
      (Y : Type w') → [TopologicalSpace Y] → CategoryTheory.Functor Cᵒᵖ (Type (max w w'))
-- Init.Data.Int.DivMod.Lemmas
Int.natCast_dvd_natCast : ∀ {m n : ℕ}, ↑m ∣ ↑n ↔ m ∣ n
-- Mathlib.Order.Filter.Prod
Filter.coprod_bot : ∀ {α : Type u_1} {β : Type u_2} (l : Filter α), l.coprod ⊥ = Filter.comap Prod.fst l
-- Mathlib.Algebra.Order.Positive.Ring
Positive.instAddSubtypeLtOfNat_mathlib : {M : Type u_1} → [inst : AddMonoid M] → [inst_1 : Preorder M] → [AddLeftStrictMono M] → Add { x // 0 < x }
-- Mathlib.NumberTheory.PrimeCounting
Nat.tendsto_primeCounting' : Filter.Tendsto Nat.primeCounting' Filter.atTop Filter.atTop
-- Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
/-- `Algebra.IsEffective R S` implies surjectivity of `codRestrictEqLocusPushoutCocone`.  -/
Algebra.codRestrictEqLocusPushoutCocone.surjective_of_isEffective : ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  Algebra.IsEffective R S → Function.Surjective ⇑(Algebra.codRestrictEqLocusPushoutCocone R S)
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_eq_lift : ∀ {x : Cardinal.{v}} {m : ℕ∞}, ↑m = Cardinal.lift.{u, v} x ↔ ↑m = x
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.IsSplitEpi.id_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [hf : CategoryTheory.IsSplitEpi f]
  {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.section_ f) (CategoryTheory.CategoryStruct.comp f h) = h
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
/-- Expressing uniform convergence using `dist`.  -/
Metric.tendstoUniformly_iff : ∀ {α : Type u} {β : Type v} {ι : Type u_1} [inst : PseudoMetricSpace α] {F : ι → β → α} {f : β → α} {p : Filter ι},
  TendstoUniformly F f p ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), dist (f x) (F n x) < ε
-- Mathlib.Control.Functor
Functor.Comp.mk.eq_1 : ∀ {F : Type u → Type w} {G : Type v → Type u} {α : Type v} (x : F (G α)), Functor.Comp.mk x = x
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
thickening_ball : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ ε : ℝ},
  0 < ε → 0 < δ → ∀ (x : E), Metric.thickening ε (Metric.ball x δ) = Metric.ball x (ε + δ)
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- An action of a monoid with zero `M₀` on a Type `A`, also with `0`, extends `MulAction` and
is compatible with `0` (both in `M₀` and in `A`), with `1 ∈ M₀`, and with associativity of
multiplication on the monoid `A`.  -/
MulActionWithZero : (M₀ : Type u_2) → (A : Type u_7) → [MonoidWithZero M₀] → [Zero A] → Type (max u_2 u_7)
-- Mathlib.Data.DFinsupp.NeLocus
DFinsupp.neLocus_zero_left : ∀ {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst_1 : (a : α) → DecidableEq (N a)]
  [inst_2 : (a : α) → Zero (N a)] (f : Π₀ (a : α), N a), DFinsupp.neLocus 0 f = f.support
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.ne_zero_of_isSuccLimit : ∀ {c : ℕ}, Order.IsSuccLimit c → c ≠ 0
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- A maximally acyclic graph is a tree. This is similar to `maximal_isAcyclic_iff_isTree` except
with `Nonempty V` as part of the iff rather than an assumption.  -/
SimpleGraph.isTree_iff_maximal_isAcyclic : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsTree ↔ Nonempty V ∧ Maximal SimpleGraph.IsAcyclic G
-- Mathlib.Algebra.Order.Floor.Defs
Int.gc_coe_floor : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α], GaloisConnection Int.cast Int.floor
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitBall.instSemigroup : {𝕜 : Type u_1} → [inst : NonUnitalSeminormedRing 𝕜] → Semigroup ↑(Metric.ball 0 1)
-- Mathlib.Algebra.Free
FreeAddSemigroup.instLawfulTraversable : LawfulTraversable FreeAddSemigroup
-- Mathlib.Algebra.Order.Module.Defs
smul_nonneg_iff_nonneg_of_pos_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulZeroClass α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [PosSMulMono α β] [PosSMulReflectLE α β], 0 < a → (0 ≤ a • b ↔ 0 ≤ b)
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.natCast_arg : ∀ {n : ℕ}, (↑n).arg = 0
-- Mathlib.Data.Nat.Fib.Basic
/-- `fib (n + 2)` is strictly monotone.  -/
Nat.fib_add_two_strictMono : StrictMono fun n => Nat.fib (n + 2)
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.Arrow.mapAugmentedCechNerve_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom]
  [inst_2 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback g.right (fun x => g.left) fun x => g.hom] (F : f ⟶ g),
  (CategoryTheory.Arrow.mapAugmentedCechNerve F).right = CategoryTheory.Arrow.Hom.right F
-- Mathlib.RepresentationTheory.Maschke
/-- We define the conjugate of `π` by `g`, as a `k`-linear map.  -/
LinearMap.conjugate : {k : Type u_1} →
  [inst : CommRing k] →
    {G : Type u_2} →
      [inst_1 : Group G] →
        {V : Type u_3} →
          [inst_2 : AddCommGroup V] →
            [inst_3 : Module k V] →
              [inst_4 : Module (MonoidAlgebra k G) V] →
                [IsScalarTower k (MonoidAlgebra k G) V] →
                  {W : Type u_4} →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : Module k W] →
                        [inst_8 : Module (MonoidAlgebra k G) W] →
                          [IsScalarTower k (MonoidAlgebra k G) W] → (W →ₗ[k] V) → G → W →ₗ[k] V
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.LocQuiver.mk.sizeOf_spec : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C} [inst_1 : SizeOf C]
  [inst_2 : ⦃X Y : C⦄ → (x : X ⟶ Y) → SizeOf (W x)] (obj : C), sizeOf { obj := obj } = 1 + sizeOf obj
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cochainsMap_comp : ∀ {k : Type u} [inst : CommRing k] {G H K : Type u} [inst_1 : Group G] [inst_2 : Group H] [inst_3 : Group K]
  {A : Rep.{u, u, u} k K} {B : Rep.{u, u, u} k H} {C : Rep.{u, u, u} k G} (f : H →* K) (g : G →* H)
  (φ : Rep.res f A ⟶ B) (ψ : Rep.res g B ⟶ C),
  groupCohomology.cochainsMap (f.comp g) (CategoryTheory.CategoryStruct.comp ((Rep.resFunctor g).map φ) ψ) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsMap f φ) (groupCohomology.cochainsMap g ψ)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- underlying morphism between the carriers  -/
CategoryTheory.Endofunctor.Algebra.Hom.f : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C C} → {A₀ A₁ : CategoryTheory.Endofunctor.Algebra F} → A₀.Hom A₁ → (A₀.a ⟶ A₁.a)
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.instIsDTopologyCompatible : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] [inst_1 : NormedSpace ℝ X] [inst_2 : FiniteDimensional ℝ X],
  Diffeology.IsDTopologyCompatible X
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.mem_rootSet_of_ne : ∀ {T : Type w} [inst : CommRing T] {p : Polynomial T} {S : Type u_1} [IsDomain T] [inst_2 : CommRing S]
  [inst_3 : IsDomain S] [inst_4 : Algebra T S] [Module.IsTorsionFree T S],
  p ≠ 0 → ∀ {a : S}, a ∈ p.rootSet S ↔ (Polynomial.aeval a) p = 0
-- Lean.Parser.Term.Doc
_private.Lean.Parser.Term.Doc.0.Lean.Parser.Term.Doc.getRecommendedSpellingString.bullet : Lean.Parser.Term.Doc.RecommendedSpelling → String
-- Mathlib.Data.List.MinMax
List.minimum_ne_top_of_length_pos : ∀ {α : Type u_1} [inst : LinearOrder α] {l : List α}, 0 < l.length → l.minimum ≠ ⊤
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticForm.discr'.eq_1 : ∀ {R : Type u_3} {n : Type w} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] [inst_3 : Invertible 2]
  (Q : QuadraticForm R (n → R)), Q.discr' = Q.toMatrix'.det
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.Const.modify.eq_def : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (f : β → β) (t : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.modify k f t =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf => Std.DTreeMap.Internal.Impl.leaf
    | Std.DTreeMap.Internal.Impl.inner sz k' v' l r =>
      match compare k k' with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.inner sz k' v' (Std.DTreeMap.Internal.Impl.Const.modify k f l) r
      | Ordering.gt => Std.DTreeMap.Internal.Impl.inner sz k' v' l (Std.DTreeMap.Internal.Impl.Const.modify k f r)
      | Ordering.eq => Std.DTreeMap.Internal.Impl.inner sz k (f v') l r
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.Hom.toPartialMap_domain : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), (AlgebraicGeometry.Scheme.Hom.toPartialMap f).domain = ⊤
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpInd_smul' : ∀ {α : Type u_1} {F : Type u_2} {𝕜 : Type u_6} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {hm : m ≤ m0}
  [inst_3 : MeasureTheory.SigmaFinite (μ.trim hm)] [inst_4 : NormedSpace ℝ F] [SMulCommClass ℝ 𝕜 F] (c : 𝕜) (x : F),
  (MeasureTheory.condExpInd F hm μ s) (c • x) = c • (MeasureTheory.condExpInd F hm μ s) x
-- Mathlib.Tactic.Subsingleton
/-- `subsingleton` proves the main goal of the form `∀ a ... b, x = y` or `∀ a ... b, x ≍ y` using the
fact that the type(s) of `x` and `y` are *subsingletons* (a type with exactly zero or one elements).
If `subsingleton` cannot close the goal, it fails.

Techniques the `subsingleton` tactic can apply:
- proof irrelevance
- heterogeneous proof irrelevance (via `proof_irrel_heq`)
- using `Subsingleton` (via `Subsingleton.elim`)
- proving instances of the type `BEq α` are equal if they are both lawful
  (via `lawful_beq_subsingleton`)

* `subsingleton [inst1, inst2, ...]` can be used to add additional `Subsingleton` instances
  to the local context. This can be more flexible than
  `have := inst1; have := inst2; ...; subsingleton` since the tactic does not require that
  all placeholders be solved for.
 -/
Mathlib.Tactic.subsingletonStx : Lean.ParserDescr
-- Mathlib.MeasureTheory.SetAlgebra
MeasureTheory.IsSetAlgebra.union_mem : ∀ {α : Type u_1} {𝒜 : Set (Set α)}, MeasureTheory.IsSetAlgebra 𝒜 → ∀ ⦃s t : Set α⦄, s ∈ 𝒜 → t ∈ 𝒜 → s ∪ t ∈ 𝒜
-- Lean.Meta.ArgsPacker
_private.Lean.Meta.ArgsPacker.0.Lean.Meta.ArgsPacker.Mutual.pack.go.eq_def : ∀ (numFuncs fidx : ℕ) (arg : Lean.Expr) (i : ℕ) (type : Lean.Expr),
  Lean.Meta.ArgsPacker.Mutual.pack.go✝ numFuncs fidx arg i type =
    if i ≥ numFuncs - 1 then pure arg
    else do
      let __do_lift ← Lean.Meta.whnfD type
      __do_lift.withApp fun f args =>
          if (args.size == 2) = true then
            if (i == fidx) = true then pure (Lean.mkApp3 (Lean.mkConst `PSum.inl f.constLevels!) args[0]! args[1]! arg)
            else do
              let r ← Lean.Meta.ArgsPacker.Mutual.pack.go✝ numFuncs fidx arg (i + 1) args[1]!
              pure (Lean.mkApp3 (Lean.mkConst `PSum.inr f.constLevels!) args[0]! args[1]! r)
          else
            panicWithPosWithDecl "Lean.Meta.ArgsPacker"
              "_private.Lean.Meta.ArgsPacker.0.Lean.Meta.ArgsPacker.Mutual.pack.go" 276 8
              ("assertion violation: " ++ "args.size == 2\n        ")
-- Init.PropLemmas
Exists.nonempty : ∀ {α : Sort u_1} {p : α → Prop}, (∃ x, p x) → Nonempty α
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.forIn'_congr : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] [inst_2 : DecidableLE α] [inst_3 : Std.PRange.UpwardEnumerable α]
  [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α] [inst_5 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_6 : Std.Rxc.IsAlwaysFinite α] [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w}
  [inst_8 : Monad m] {γ : Type u} {init init' : γ} {r r' : Std.Roc α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)}
  {f' : (a : α) → a ∈ r' → γ → m (ForInStep γ)} (hr : r = r'),
  init = init' → (∀ (a : α) (m_1 : a ∈ r') (b : γ), f a ⋯ b = f' a m_1 b) → forIn' r init f = forIn' r' init' f'
-- Mathlib.Order.Filter.Map
Filter.push_pull : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (F : Filter α) (G : Filter β),
  Filter.map f (F ⊓ Filter.comap f G) = Filter.map f F ⊓ G
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.toOrderHom_id : ∀ {R : Type u_1} {E₁ : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid E₁] [inst_2 : PartialOrder E₁]
  [inst_3 : Module R E₁], (PositiveLinearMap.id R E₁).toOrderHom = OrderHom.id