mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.mapEquiv_apply : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : TopologicalSpace M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : TopologicalSpace N]
  [inst_6 : Module R N] (f : M ≃L[R] N) (s : ClosedSubmodule R M),
  ↑((ClosedSubmodule.mapEquiv f) s) = Submodule.map ↑↑f ↑s
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∉ m₁ → (m₁ ∪ m₂).getKey? k = m₂.getKey? k
-- Mathlib.Data.DFinsupp.Multiset
DFinsupp.toMultiset_single : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (n : ℕ), (DFinsupp.toMultiset fun₀ | a => n) = Multiset.replicate n a
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_comp' : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p]
  [ContinuousMapZero.UniqueHom R A] (g f : R → R) (a : A),
  autoParam (ContinuousOn g (f '' quasispectrum R a)) cfcₙ_comp'._auto_1 →
    autoParam (g 0 = 0) cfcₙ_comp'._auto_3 →
      autoParam (ContinuousOn f (quasispectrum R a)) cfcₙ_comp'._auto_5 →
        autoParam (f 0 = 0) cfcₙ_comp'._auto_7 →
          autoParam (p a) cfcₙ_comp'._auto_9 → cfcₙ (fun x => g (f x)) a = cfcₙ g (cfcₙ f a)
-- Batteries.Tactic.Alias
/-- Environment extension for registering aliases  -/
Batteries.Tactic.Alias.aliasExt : Lean.MapDeclarationExtension Batteries.Tactic.Alias.AliasInfo
-- Std.Data.TreeMap.Raw.Slice
Std.TreeMap.Raw.instSliceableRioSlice : {α : Type u} →
  {β : Type v} →
    (cmp : autoParam (α → α → Ordering) Std.TreeMap.Raw.instSliceableRioSlice._auto_1) →
      Std.Rio.Sliceable (Std.TreeMap.Raw α β cmp) α (Std.DTreeMap.Internal.Const.RioSlice α β)
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.prod_ite_mem : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : DecidableEq ι] (s t : Finset ι) (f : ι → M),
  (∏ i ∈ s, if i ∈ t then f i else 1) = ∏ i ∈ s ∩ t, f i
-- Init.Data.List.Lemmas
List.getLast_cons : ∀ {α : Type u_1} {a : α} {l : List α} (h : l ≠ []), (a :: l).getLast ⋯ = l.getLast h
-- Mathlib.Algebra.Ring.Opposite
MulOpposite.instNonAssocRing : {R : Type u_1} → [NonAssocRing R] → NonAssocRing Rᵐᵒᵖ
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.addSubgroupOf_bot_eq_top : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.addSubgroupOf ⊥ = ⊤
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.denoteSAsRing.eq_def : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (x : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.Expr.denoteSAsRing ctx x =
    match x with
    | Lean.Grind.CommRing.Expr.num k => OfNat.ofNat k.natAbs
    | Lean.Grind.CommRing.Expr.natCast k => OfNat.ofNat k
    | Lean.Grind.CommRing.Expr.var v => ↑(Lean.Grind.CommRing.Var.denote ctx v)
    | a.add b => Lean.Grind.CommRing.Expr.denoteSAsRing ctx a + Lean.Grind.CommRing.Expr.denoteSAsRing ctx b
    | a.mul b => Lean.Grind.CommRing.Expr.denoteSAsRing ctx a * Lean.Grind.CommRing.Expr.denoteSAsRing ctx b
    | a.pow k => Lean.Grind.CommRing.Expr.denoteSAsRing ctx a ^ k
    | a.sub b => 0
    | a.neg => 0
    | Lean.Grind.CommRing.Expr.intCast k => 0
-- Lean.Elab.DeprecatedArg
Lean.Elab.DeprecatedArgEntry.oldArg : Lean.Elab.DeprecatedArgEntry → Lean.Name
-- Mathlib.CategoryTheory.Category.TwoP
pointedToTwoPSnd_map_hom_toFun : ∀ {X Y : Pointed} (f : X ⟶ Y) (a : Option X.X), (pointedToTwoPSnd.map f).hom.toFun a = Option.map f.toFun a
-- Mathlib.NumberTheory.FunctionField
FunctionField.FiniteDimensional.adjoin_X : ∀ {F : Type u_3} {K : Type u_4} [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra (RatFunc F) K]
  [FunctionField F K], FiniteDimensional (↥F⟮RatFunc.X⟯) K
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.Preadditive.add.eq_1 : ∀ {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] [inst_2 : CategoryTheory.Preadditive C]
  {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : W.HasLeftCalculusOfFractions] {X Y : C} {X' Y' : D} (eX : L.obj X ≅ X') (eY : L.obj Y ≅ Y')
  (f₁ f₂ : X' ⟶ Y'),
  CategoryTheory.Localization.Preadditive.add W eX eY f₁ f₂ =
    (CategoryTheory.Localization.Preadditive.homEquiv eX eY).symm
      (CategoryTheory.Localization.Preadditive.add' W ((CategoryTheory.Localization.Preadditive.homEquiv eX eY) f₁)
        ((CategoryTheory.Localization.Preadditive.homEquiv eX eY) f₂))
-- Mathlib.RingTheory.DedekindDomain.SelmerGroup
IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroToFun.eq_1 : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type v} [inst_2 : Field K] [inst_3 : Algebra R K]
  [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (x : Kˣ),
  v.valuationOfNeZeroToFun x =
    Multiplicative.ofAdd
      (-↑((Associates.mk v.asIdeal).count
              (Associates.mk (Ideal.span {(IsLocalization.sec (nonZeroDivisors R) ↑x).1})).factors) -
        -↑((Associates.mk v.asIdeal).count
              (Associates.mk (Ideal.span {↑(IsLocalization.sec (nonZeroDivisors R) ↑x).2})).factors))
-- Mathlib.Algebra.Order.Positive.Ring
Positive.addLeftCancelSemigroup : {M : Type u_3} →
  [inst : AddLeftCancelMonoid M] → [inst_1 : Preorder M] → [AddLeftStrictMono M] → AddLeftCancelSemigroup { x // 0 < x }
-- Mathlib.RingTheory.Spectrum.Prime.Polynomial
/-- Let `A` be an `R`-algebra.
`𝔭 : Spec R` is in the image of `D(f) ⊆ Spec S`
if and only if `f` is not nilpotent on `κ(𝔭) ⊗ A`.  -/
PrimeSpectrum.mem_image_comap_basicOpen : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (f : A)
  (x : PrimeSpectrum R),
  x ∈ PrimeSpectrum.comap (algebraMap R A) '' ↑(PrimeSpectrum.basicOpen f) ↔
    ¬IsNilpotent ((algebraMap A (TensorProduct R A x.asIdeal.ResidueField)) f)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.default_def : ∀ {V : Type u} (G : SimpleGraph V) (v : V), default = SimpleGraph.Walk.nil
-- Mathlib.Order.BoundedOrder.Basic
BoundedOrder.toOrderBot : {α : Type u} → {inst : LE α} → [self : BoundedOrder α] → OrderBot α
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finset.sum_apply' : ∀ {α : Type u_1} {ι : Type u_2} {A : Type u_4} [inst : AddCommMonoid A] {s : Finset α} {f : α → ι →₀ A} (i : ι),
  (∑ k ∈ s, f k) i = ∑ k ∈ s, (f k) i
-- Mathlib.Data.ENNReal.Operations
/-- Weaker version of `ENNReal.eq_sub_of_add_eq` assuming that `b = a + c` itself is finite rather
than `c`.  -/
ENNReal.eq_sub_of_add_eq' : ∀ {a b c : ENNReal}, b ≠ ⊤ → a + c = b → a = b - c
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.rightUnitor_naturality_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} (η : f ⟶ g) {Z : a ⟶ b} (h : g ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.id b))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor g).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor f).hom
      (CategoryTheory.CategoryStruct.comp η h)
-- Lean.Elab.WhereFinally
Lean.Elab.WhereFinallyView : Type
-- Mathlib.Data.Ordmap.Invariants
Ordnode.findMax_dual : ∀ {α : Type u_1} (t : Ordnode α), t.dual.findMax = t.findMin
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.map_id : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β),
  κ.map id = κ
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.con_ker_mk : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddCon.ker AddMonoid.Coprod.mk = AddMonoid.coprodCon M N
-- Mathlib.Analysis.Normed.Affine.AddTorsor
nndist_homothety_center : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜),
  nndist ((AffineMap.homothety p₁ c) p₂) p₁ = ‖c‖₊ * nndist p₁ p₂
-- Mathlib.LinearAlgebra.Projectivization.Subspace
Submodule.mk_mem_projectivization_iff : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (s : Submodule K V) {v : V} (hv : v ≠ 0), Projectivization.mk K v hv ∈ Submodule.projectivization s ↔ v ∈ s
-- Std.Data.Iterators.Combinators.Monadic.DropWhile
/-- Internal implementation detail of the iterator library.  -/
Std.Iterators.Types.DropWhile.inner : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)} →
        Std.Iterators.Types.DropWhile α m β P → Std.IterM m β
-- Mathlib.Algebra.Ring.BooleanRing
instNonUnitalCommRingAsBoolRingOfGeneralizedBooleanAlgebra : {α : Type u_1} → [GeneralizedBooleanAlgebra α] → NonUnitalCommRing (AsBoolRing α)
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- Transfer a `MulActionObj` along isomorphisms.  -/
CategoryTheory.ModObj.ofIso : {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] →
            {M : C} →
              [inst_4 : CategoryTheory.MonObj M] →
                {X : D} →
                  {N : C} →
                    [inst_5 : CategoryTheory.MonObj N] →
                      (e₁ : M ≅ N) →
                        [CategoryTheory.IsMonHom e₁.hom] →
                          {Y : D} → (X ≅ Y) → [CategoryTheory.ModObj M X] → CategoryTheory.ModObj N Y
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.contains_max : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {he : t ≠ ∅},
  t.contains (t.max he) = true
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.continuous_toCompletion : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K),
  Continuous NumberField.InfinitePlace.Completion.toCompletion
-- Mathlib.Order.CountableSupClosed
CountableSupClosed.supClosed : ∀ {α : Type u_2} {s : Set α} [inst : SemilatticeSup α], CountableSupClosed s → SupClosed s
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Embedding.comp_refl : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G'),
  f.comp SimpleGraph.Embedding.refl = f
-- Mathlib.Topology.UniformSpace.Basic
instMinUniformSpace : {α : Type ua} → Min (UniformSpace α)
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
/-- The canonical functor `(C ⥤ D) ⥤ (Karoubi C ⥤ Karoubi D)`  -/
CategoryTheory.Idempotents.functorExtension₂ : (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] →
        CategoryTheory.Functor (CategoryTheory.Functor C D)
          (CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi C) (CategoryTheory.Idempotents.Karoubi D))
-- Mathlib.Data.List.Sort
StrictMono.sortedGT_listMap : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {l : List α},
  StrictMono f → ((List.map f l).SortedGT ↔ l.SortedGT)
-- Mathlib.Data.Seq.Basic
Stream'.Seq.take_zero : ∀ {α : Type u} {s : Stream'.Seq α}, Stream'.Seq.take 0 s = []
-- Mathlib.Combinatorics.Enumerative.Stirling
Nat.stirlingSecond_zero : Nat.stirlingSecond 0 0 = 1
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_inter_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₁ ∩ m₂ ↔ k ∈ m₁ ∧ k ∈ m₂
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- An `AddSubgroup` is closed under subtraction.  -/
AddSubgroup.sub_mem : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) {x y : G}, x ∈ H → y ∈ H → x - y ∈ H
-- Lean.Server.RequestCancellation
Lean.Server.RequestCancellation.noConfusionType : Sort v✝ → Lean.Server.RequestCancellation → Lean.Server.RequestCancellation → Sort v✝
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The point of the augmentation.  -/
CategoryTheory.CosimplicialObject.Augmented.point : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor (CategoryTheory.CosimplicialObject.Augmented C) C
-- Mathlib.Geometry.Convex.Cone.Face.Basic
/-- If the positive combination of points of a cone is in a face, then all the points are
in the face.  -/
PointedCone.IsFaceOf.mem_of_sum_smul_mem : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {C F : PointedCone R M} {ι : Type u_4} [inst_5 : Fintype ι]
  {f : ι → M} {c : ι → R},
  F.IsFaceOf C → (∀ (i : ι), f i ∈ C) → (∀ (i : ι), 0 ≤ c i) → ∑ i, c i • f i ∈ F → ∀ (i : ι), 0 < c i → f i ∈ F
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.comap_toSubmodule : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] (f : L →ₗ⁅R⁆ L') (J : LieIdeal R L'),
  ↑(LieIdeal.comap f J) = Submodule.comap ↑f ↑J
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesAt.radius_pos : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E}, HasFPowerSeriesAt f p x → 0 < p.radius
-- Batteries.Control.LawfulMonadState
/-- The continuation passing state monad variant `StateCpsT` always has lawful state instance.  -/
LawfulMonadStateOf.instStateCpsT : ∀ {σ : Type u_1} {m : Type u_1 → Type u_2}, LawfulMonadStateOf σ (StateCpsT σ m)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
lt_mul_right : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] {a b : M₀} [PosMulStrictMono M₀],
  0 < a → 1 < b → a < a * b
-- Mathlib.Order.BooleanAlgebra.Basic
disjoint_sdiff_iff_le : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], z ≤ y → x ≤ y → (Disjoint z (y \ x) ↔ z ≤ x)
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instSMul : {m : Type u_1} → {n : Type u_2} → {R : Type u_3} → {A : Type u_5} → [SMul R A] → SMul R (CStarMatrix m n A)
-- Init.Data.Array.FinRange
Array.finRange.eq_1 : ∀ (n : ℕ), Array.finRange n = Array.ofFn fun i => i
-- Mathlib.CategoryTheory.Galois.Topology
/-- The stabilizers of points in the fibers of Galois objects form a neighbourhood basis
of the identity in `Aut F`.  -/
CategoryTheory.PreGaloisCategory.nhds_one_has_basis_stabilizers : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F],
  (nhds 1).HasBasis (fun x => True) fun X => ↑(MulAction.stabilizer (CategoryTheory.Aut F) X.pt)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
SummableUniformlyOn.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] (f : ι → β → α) (s : Set β)
  [inst_1 : UniformSpace α], SummableUniformlyOn f s = Summable (⇑(UniformOnFun.ofFun {s}) ∘ f)
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
Std.Iter.toArray_flatMapAfterM : ∀ {α α₂ β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α Id β] [inst_5 : Std.Iterator α₂ m γ] [Std.Iterators.Finite α Id]
  [Std.Iterators.Finite α₂ m] {f : β → m (Std.IterM m γ)} {it₁ : Std.Iter β} {it₂ : Option (Std.IterM m γ)},
  (Std.Iter.flatMapAfterM f it₁ it₂).toArray =
    match it₂ with
    | none =>
      Array.flatten <$>
        (Std.Iter.mapM
            (fun b => do
              let __do_lift ← f b
              __do_lift.toArray)
            it₁).toArray
    | some it₂ => do
      let __do_lift ← it₂.toArray
      let __do_lift_1 ←
        Array.flatten <$>
            (Std.Iter.mapM
                (fun b => do
                  let __do_lift ← f b
                  __do_lift.toArray)
                it₁).toArray
      pure (__do_lift ++ __do_lift_1)
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.instFaithfulSMul : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [inst_2 : DecidableEq ι]
  [inst_3 : (i : ι) → DecidableEq (G i)], FaithfulSMul (Monoid.PushoutI φ) (Monoid.PushoutI.NormalWord d)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instSMulMonoidHom : {M : Type u_5} →
  {A : Type u_7} →
    {B : Type u_8} →
      [inst : Monoid M] → [inst_1 : Monoid A] → [MulDistribMulAction M A] → [inst : MulOneClass B] → SMul Mᵈᵐᵃ (A →* B)
-- Mathlib.Tactic.IntervalCases
/-- A `Methods` implementation for `ℕ`.
This tells `interval_cases` how to work on natural numbers.  -/
Mathlib.Tactic.IntervalCases.natMethods : Mathlib.Tactic.IntervalCases.Methods
-- Mathlib.RingTheory.TensorProduct.Basic
TensorProduct.Algebra.linearMap_comp_mul' : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B],
  Algebra.linearMap R (TensorProduct R A B) ∘ₗ LinearMap.mul' R R =
    TensorProduct.map (Algebra.linearMap R A) (Algebra.linearMap R B)
-- Mathlib.Data.Fintype.Perm
Fintype.card_perm : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α], Fintype.card (Equiv.Perm α) = (Fintype.card α).factorial
-- Lean.Util.ReplaceLevel
Lean.Expr.ReplaceLevelImpl.replaceUnsafeM : (Lean.Level → Option Lean.Level) → USize → Lean.Expr → Lean.Expr.ReplaceLevelImpl.ReplaceM Lean.Expr
-- Mathlib.NumberTheory.SelbergSieve
SelbergSieve.mk.inj : ∀ {toBoundingSieve : BoundingSieve} {level : ℝ} {one_le_level : 1 ≤ level} {toBoundingSieve_1 : BoundingSieve}
  {level_1 : ℝ} {one_le_level_1 : 1 ≤ level_1},
  { toBoundingSieve := toBoundingSieve, level := level, one_le_level := one_le_level } =
      { toBoundingSieve := toBoundingSieve_1, level := level_1, one_le_level := one_le_level_1 } →
    toBoundingSieve = toBoundingSieve_1 ∧ level = level_1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom.ext : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {inst : CategoryTheory.Category.{v₁, u₁} A}
  {inst_1 : CategoryTheory.Category.{v₂, u₂} B} {inst_2 : CategoryTheory.Category.{v₃, u₃} C}
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄}
  {inst_3 : CategoryTheory.Category.{v₄, u₄} X} {x y : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X}
  {x_1 y_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom X x y},
  x_1.fst = y_1.fst → x_1.snd = y_1.snd → x_1 = y_1
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Closure
SubMulAction.closure.eq_1 : ∀ (R : Type u_1) {M : Type u_2} [inst : SMul R M] (s : Set M), SubMulAction.closure R s = sInf {p | s ⊆ ↑p}
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.one_mem_pow : ∀ {α : Type u_2} [inst : Monoid α] {s : Set α} {n : ℕ}, 1 ∈ s → 1 ∈ s ^ n
-- Mathlib.RingTheory.Coalgebra.MonoidAlgebra
AddMonoidAlgebra.instCoalgebra.eq_1 : ∀ (R : Type u_1) [inst : CommSemiring R] (A : Type u_2) [inst_1 : Semiring A] (X : Type u_3) [inst_2 : Module R A]
  [inst_3 : Coalgebra R A], AddMonoidAlgebra.instCoalgebra R A X = Equiv.coalgebra R AddMonoidAlgebra.coeffEquiv
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instAddMonoid : {α : Type u_1} → [AddMonoid α] → AddMonoid αᵐᵒᵖ
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.average_zero_measure : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  (f : α → E), ⨍ (x : α), f x ∂0 = 0
-- Mathlib.Order.CompleteLattice.Basic
OrderIso.map_iSup₂ : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_6} [inst : CompleteLattice α]
  [inst_1 : CompleteLattice β] (f : α ≃o β) (x : (i : ι) → κ i → α), f (⨆ i, ⨆ j, x i j) = ⨆ i, ⨆ j, f (x i j)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMk₅_app_two : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 5}
  (app₀ : f.obj' 0 _proof_449✝ ⟶ g.obj' 0 _proof_449✝) (app₁ : f.obj' 1 _proof_450✝ ⟶ g.obj' 1 _proof_450✝)
  (app₂ : f.obj' 2 _proof_451✝ ⟶ g.obj' 2 _proof_451✝) (app₃ : f.obj' 3 _proof_452✝ ⟶ g.obj' 3 _proof_452✝)
  (app₄ : f.obj' 4 _proof_453✝ ⟶ g.obj' 4 _proof_453✝) (app₅ : f.obj' 5 _proof_454✝ ⟶ g.obj' 5 _proof_454✝)
  (w₀ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_450✝)
          app₁ =
        CategoryTheory.CategoryStruct.comp app₀
          (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_450✝))
      _auto_480✝)
  (w₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_451✝) app₂ =
        CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 _proof_246✝ _proof_451✝))
      _auto_482✝)
  (w₂ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_299✝ _proof_452✝) app₃ =
        CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 _proof_299✝ _proof_452✝))
      _auto_484✝)
  (w₃ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 3 4 _proof_364✝ _proof_453✝) app₄ =
        CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 _proof_364✝ _proof_453✝))
      _auto_486✝)
  (w₄ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 4 5 _proof_453✝ _proof_454✝) app₅ =
        CategoryTheory.CategoryStruct.comp app₄ (g.map' 4 5 _proof_453✝ _proof_454✝))
      _auto_488✝),
  (CategoryTheory.ComposableArrows.homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app
      ⟨2, CategoryTheory.ComposableArrows.homMk₅._proof_3⟩ =
    app₂
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.zsmul.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.zsmul = { smul := fun n a => ⟨n • ↑a, ⋯⟩ }
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey_modify_eq_maxKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α} {f : β → β} {he : (t.modify k f).isEmpty = false}, (t.modify k f).maxKey he = t.maxKey ⋯
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl : Lean.Compiler.LCNF.Purity → Type
-- Init.NotationExtra
/-- `{ a, b, c }` syntax, powered by the `Singleton` and `Insert` typeclasses. 

Conventions for notations in identifiers:

 * The recommended spelling of `{x}` in identifiers is `singleton`. -/
«term{_}» : Lean.ParserDescr
-- Lean.Parser.Command
Lean.Parser.Command.dumpAsyncEnvState.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.Compactness.Compact
isCompact_empty : ∀ {X : Type u} [inst : TopologicalSpace X], IsCompact ∅
-- Lean.Parser.Command
Lean.Parser.Command.namespace.formatter : Lean.PrettyPrinter.Formatter
-- Lean.Elab.Import
_private.Lean.Elab.Import.0.Lean.Elab.checkModuleNamePortability.go : Lean.Name → Lean.Parser.InputContext → String.Pos.Raw → Lean.Name → Lean.MessageLog → Lean.MessageLog
-- Mathlib.Topology.Order.Category.FrameAdjunction
/-- The type of points of a complete lattice `L`, where a *point* of a complete lattice is,
by definition, a frame homomorphism from `L` to `Prop`.  -/
Locale.PT : (L : Type u_1) → [CompleteLattice L] → Type (max u_1 0)