mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.ShrinkingLemma
ShrinkingLemma.PartialRefinement.ext : ∀ {ι : Type u_1} {X : Type u_2} {inst : TopologicalSpace X} {u : ι → Set X} {s : Set X} {p : Set X → Prop}
  {x y : ShrinkingLemma.PartialRefinement u s p}, x.toFun = y.toFun → x.carrier = y.carrier → x = y
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.HasRingHomProperty.iff_appLE : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P Q] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  P f ↔
    ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U),
      Q (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e))
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.ge_of_isGE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (X : C) (n : ℤ) [t.IsGE X n], t.ge n X
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.ofAlgEquiv.congr_simp : ∀ {S : Type u_5} [inst : CommRing S] (I : Ideal S) [inst_1 : IsAdicComplete I S],
  AdicCompletion.ofAlgEquiv I = AdicCompletion.ofAlgEquiv I
-- Init.Data.SInt.Lemmas
Int64.toInt32_ofNat' : ∀ {n : ℕ}, (Int64.ofNat n).toInt32 = Int32.ofNat n
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_le_mul_iff_of_ge : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : PartialOrder α] [MulLeftStrictMono α] [MulRightStrictMono α]
  {a₁ a₂ b₁ b₂ : α}, a₁ ≤ a₂ → b₁ ≤ b₂ → (a₂ * b₂ ≤ a₁ * b₁ ↔ a₁ = a₂ ∧ b₁ = b₂)
-- Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] (H : J.OneHypercoverFamily) (P : CategoryTheory.Functor Cᵒᵖ A),
  (∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (CategoryTheory.Limits.IsLimit (E.multifork P))) →
    ∀ [H.IsGenerating] {X : C},
      ∀ S ∈ J X,
        ∀ {T : A} {x y : T ⟶ P.obj (Opposite.op X)},
          (∀ ⦃Y : C⦄ (f : Y ⟶ X),
              S.arrows f →
                CategoryTheory.CategoryStruct.comp x (P.map f.op) = CategoryTheory.CategoryStruct.comp y (P.map f.op)) →
            x = y
-- Mathlib.Topology.Sets.Closeds
/-- The closure of a set, as an element of `TopologicalSpace.Closeds`.  -/
TopologicalSpace.Closeds.closure : {α : Type u_2} → [inst : TopologicalSpace α] → Set α → TopologicalSpace.Closeds α
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.mk_pow : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : Monoid γ] [inst_3 : ContinuousMul γ] (f : α → γ) (hf : MeasureTheory.AEStronglyMeasurable f μ) (n : ℕ),
  MeasureTheory.AEEqFun.mk f hf ^ n = MeasureTheory.AEEqFun.mk (f ^ n) ⋯
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_le : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : Preorder β] [OrderClosedTopology β] [TopologicalSpace.PseudoMetrizableSpace β] {f g : α → β},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.NullMeasurableSet {a | f a ≤ g a} μ
-- Mathlib.Algebra.Lie.Engel
/-- Engel's theorem.  -/
LieAlgebra.isNilpotent_iff_forall : ∀ {R : Type u₁} {L : Type u₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [IsNoetherian R L],
  LieRing.IsNilpotent L ↔ ∀ (x : L), IsNilpotent ((LieAlgebra.ad R L) x)
-- Mathlib.Algebra.Order.Group.Defs
/-- **Alias** of `lt_of_mul_lt_mul_left'`. -/
OrderedCommGroup.lt_of_mul_lt_mul_left : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LT α] [MulLeftReflectLT α] {a b c : α}, a * b < a * c → b < c
-- Mathlib.CategoryTheory.Subfunctor.Image
CategoryTheory.Subfunctor.preimage_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C (Type w)}
  (G : CategoryTheory.Subfunctor F) (p : F' ⟶ F) (n : C),
  (G.preimage p).obj n = ⇑(CategoryTheory.ConcreteCategory.hom (p.app n)) ⁻¹' G.obj n
-- Lean.Elab.BuiltinNotation
/-- Returns whether or not this cdot is for the given `HygieneInfo` name;
if no hygiene info is given, then matches any cdot, no matter its hygieneInfo.
 -/
Lean.Elab.Term.isCDotForInfo : Lean.Syntax → Option Lean.Name → Bool
-- Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
CochainComplex.homologySequenceδ_quotient_mapTriangle_obj_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ)) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) {Z : C}
  (h_1 :
    ((HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0).shift n₁).obj
        ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).mapTriangle.obj T).obj₁ ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      ((HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0).homologySequenceδ
        ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).mapTriangle.obj T) n₀ n₁ h)
      h_1 =
    CategoryTheory.CategoryStruct.comp
      ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n₀).hom.app T.obj₃)
      (CategoryTheory.CategoryStruct.comp
        ((HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap T.mor₃ n₀ n₁ ⋯)
        (CategoryTheory.CategoryStruct.comp
          ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n₁).inv.app T.obj₁) h_1))
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Tactic.ComputeAsymptotics.BasisExtension.insert.inj : ∀ {basis : Tactic.ComputeAsymptotics.Basis} {f : ℝ → ℝ} {ex : Tactic.ComputeAsymptotics.BasisExtension basis}
  {f_1 : ℝ → ℝ} {ex_1 : Tactic.ComputeAsymptotics.BasisExtension basis},
  Tactic.ComputeAsymptotics.BasisExtension.insert f ex = Tactic.ComputeAsymptotics.BasisExtension.insert f_1 ex_1 →
    f = f_1 ∧ ex = ex_1
-- Init.Data.Float.Float
/-- Strict inequality of floating-point numbers. Typically used via the `<` operator.
 -/
Float.lt : Float → Float → Bool
-- Mathlib.AlgebraicGeometry.Geometrically.Basic
/-- `P` holds geometrically for `f` if and only if all fibers are geometrically `P`.  -/
AlgebraicGeometry.geometrically_iff_forall_fiberToSpecResidueField : ∀ {P : CategoryTheory.ObjectProperty AlgebraicGeometry.Scheme} {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  AlgebraicGeometry.geometrically P f ↔
    ∀ (y : ↥Y), AlgebraicGeometry.geometrically P (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField f y)
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.instMonoid : {R : Type u_1} →
  {A : Type u_2} →
    [inst : Monoid R] →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : DistribMulAction R A] → [inst_3 : Star A] → Monoid (A →⋆ₙₐ[R] A)
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.CorepresentableBy.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {F : CategoryTheory.Functor C (Type v)} {X : C}
  {homEquiv : {Y : C} → (X ⟶ Y) ≃ F.obj Y}
  {homEquiv_comp :
    autoParam
      (∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y),
        homEquiv (CategoryTheory.CategoryStruct.comp f g) =
          (CategoryTheory.ConcreteCategory.hom (F.map g)) (homEquiv f))
      CategoryTheory.Functor.CorepresentableBy.homEquiv_comp._autoParam}
  {homEquiv_1 : {Y : C} → (X ⟶ Y) ≃ F.obj Y}
  {homEquiv_comp_1 :
    autoParam
      (∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y),
        homEquiv_1 (CategoryTheory.CategoryStruct.comp f g) =
          (CategoryTheory.ConcreteCategory.hom (F.map g)) (homEquiv_1 f))
      CategoryTheory.Functor.CorepresentableBy.homEquiv_comp._autoParam},
  { homEquiv := homEquiv, homEquiv_comp := homEquiv_comp } =
      { homEquiv := homEquiv_1, homEquiv_comp := homEquiv_comp_1 } →
    homEquiv = homEquiv_1
-- Lean.DocString.Parser
/-- Ordered lists may have two styles of indicator, with trailing dots or parentheses.
 -/
Lean.Doc.Parser.OrderedListType : Type
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.IsTopCompl.closedComplemented : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M}, Submodule.IsTopCompl p q → p.ClosedComplemented
-- Mathlib.RingTheory.IsGaloisGroup.Basic
IsGaloisGroup.instSMulCommClassQuotientSubgroupSubtypeMemIntermediateFieldOfSMulDistribClassOfIsScalarTower : ∀ (G : Type u_1) [inst : Group G] {K : Type u_2} {L : Type u_3} [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] (F : IntermediateField K L) (N : Subgroup G)
  [inst_5 : N.Normal] [inst_6 : IsGaloisGroup (↥N) (↥F) L] [SMulCommClass G K L] [inst_8 : MulSemiringAction G ↥F]
  [SMulDistribClass G (↥F) L] [IsScalarTower G (G ⧸ N) ↥F], SMulCommClass (G ⧸ N) K ↥F
-- Mathlib.RingTheory.HahnSeries.Basic
/-- The order of a nonzero Hahn series `x` is a minimal element of `Γ` where `x` has a
nonzero coefficient, the order of 0 is 0.  -/
HahnSeries.order : {Γ : Type u_1} → {R : Type u_3} → [inst : PartialOrder Γ] → [inst_1 : Zero R] → [Zero Γ] → HahnSeries Γ R → Γ
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.Icc_add_one_left_eq_Ioc_of_not_isMax : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Add α]
  [SuccAddOrder α] {a : α}, ¬IsMax a → ∀ (b : α), Finset.Icc (a + 1) b = Finset.Ioc a b
-- Lean.Message
Lean.MessageData.ofOriginatingSyntax.injEq : ∀ (a : Lean.Syntax) (a_1 : Lean.MessageData) (a_2 : Lean.Syntax) (a_3 : Lean.MessageData),
  (Lean.MessageData.ofOriginatingSyntax a a_1 = Lean.MessageData.ofOriginatingSyntax a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Probability.Kernel.Composition.MeasureComp
MeasureTheory.Measure.compProd_deterministic : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  [MeasureTheory.SFinite μ] {f : α → β} (hf : Measurable f),
  μ.compProd (ProbabilityTheory.Kernel.deterministic f hf) = MeasureTheory.Measure.map (fun a => (a, f a)) μ
-- Init.Data.Array.Basic
/-- Prepends an array to a list. The elements of the array are at the beginning of the resulting list.

Equivalent to `as.toList ++ l`.

Examples:
* `#[1, 2].toListAppend [3, 4] = [1, 2, 3, 4]`
* `#[1, 2].toListAppend [] = [1, 2]`
* `#[].toListAppend [3, 4, 5] = [3, 4, 5]`
 -/
Array.toListAppend : {α : Type u} → Array α → List α → List α
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.toListModel_insertListₘ : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α fun x => β} {l : List (α × β)},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    (Std.DHashMap.Internal.toListModel (↑(Std.DHashMap.Internal.Raw₀.Const.insertListₘ m l)).buckets).Perm
      (Std.Internal.List.insertListConst (Std.DHashMap.Internal.toListModel (↑m).buckets) l)
-- Mathlib.GroupTheory.Submonoid.Center
/-- The center of an additive magma is isomorphic to the center of its opposite.  -/
AddSubsemigroup.centerToAddOpposite : {M : Type u_2} → [inst : Add M] → ↥(AddSubsemigroup.center M) ≃+ ↥(AddSubsemigroup.center Mᵃᵒᵖ)
-- Init.Grind.Interactive
/-- A variant of `cases` that provides a code-action for selecting one of the candidate case-splits
available in the `grind` state.
 -/
Lean.Parser.Tactic.Grind.casesTrace : Lean.ParserDescr
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.skipPrefix?_char_eq_skipPrefix?_beq : ∀ {c : Char} {s : String.Slice}, s.skipPrefix? c = s.skipPrefix? fun x => x == c
-- Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
CategoryTheory.MorphismProperty.IsInvertedBy.map_iff : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  (W : CategoryTheory.MorphismProperty C₁) (F : CategoryTheory.Functor C₁ C₂) (G : CategoryTheory.Functor C₂ C₃),
  (W.map F).IsInvertedBy G ↔ W.IsInvertedBy (F.comp G)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.toArray_eq_if_roo : ∀ {α : Type u} {r : Std.Rco α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.Rxo.IsAlwaysFinite α]
  [Std.PRange.LawfulUpwardEnumerableLT α],
  r.toArray = if r.lower < r.upper then #[r.lower] ++ (r.lower<...r.upper).toArray else #[]
-- Mathlib.Data.Ordmap.Invariants
Ordnode.dual_node4L : ∀ {α : Type u_1} (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α),
  (l.node4L x m y r).dual = r.dual.node4R y m.dual x l.dual
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_subset_Ico_iff : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b₁ b₂ : α}, a₁ ≤ b₁ → (Set.Icc a₁ b₁ ⊆ Set.Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂)
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.detp.eq_1 : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] (s : ℤˣ)
  (A : Matrix n n R), Matrix.detp s A = ∑ σ ∈ Equiv.Perm.ofSign s, ∏ k, A k (σ k)
-- Lean.Meta.Constructions.SparseCasesOn
_private.Lean.Meta.Constructions.SparseCasesOn.0.Lean.Meta.SparseCasesOnKey.ctors : Lean.Meta.SparseCasesOnKey✝ → Array Lean.Name
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse_obj_laxMonoidal_ε : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.Mon C),
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A) =
    CategoryTheory.MonObj.one
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
AlgebraicGeometry.Proj.instLocallyOfFiniteTypeToSpecZeroOfFiniteTypeSubtypeMemOfNatNat : ∀ {σ : Type u_1} {A : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] [Algebra.FiniteType (↥(𝒜 0)) A],
  AlgebraicGeometry.LocallyOfFiniteType (AlgebraicGeometry.Proj.toSpecZero 𝒜)
-- Lean.Meta.DiscrTree.Main
/-- Reduce `e` until we get an irreducible term (modulo current reducibility setting) or the resulting term
is a bad key (see comment at `isBadKey`).
We use this method instead of `reduce` for root terms at `pushArgs`.  -/
_private.Lean.Meta.DiscrTree.Main.0.Lean.Meta.DiscrTree.reduceUntilBadKey : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.map.comp : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (g : β → γ) (x : FreeAddGroup α),
  (FreeAddGroup.map g) ((FreeAddGroup.map f) x) = (FreeAddGroup.map (g ∘ f)) x
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
Submodule.localized'_bot : ∀ {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Algebra R S] [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] (p : Submonoid R)
  [inst_9 : IsLocalization p S] (f : M →ₗ[R] N) [inst_10 : IsLocalizedModule p f], Submodule.localized' S p f ⊥ = ⊥
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.addPrehaar_pos : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G) {U : Set G},
  (interior U).Nonempty →
    ∀ {K : Set G} (h1K : IsCompact K),
      (interior K).Nonempty → 0 < MeasureTheory.Measure.haar.addPrehaar (↑K₀) U { carrier := K, isCompact' := h1K }
-- Init.Data.String.Lemmas.FindPos
String.offset_posLE_eq_self_iff : ∀ {s : String} {p : String.Pos.Raw}, (s.posLE p).offset = p ↔ String.Pos.Raw.IsValid s p
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDFAux.le_one : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → ℚ → ℝ},
  ProbabilityTheory.IsRatCondKernelCDFAux f κ ν → ∀ (a : α), ∀ᵐ (c : β) ∂ν a, ∀ (q : ℚ), f (a, c) q ≤ 1
-- Mathlib.Logic.Equiv.Option
Equiv.optionEquivSumPUnit_symm_inr : ∀ {α : Type u_4} (a : PUnit.{u_5 + 1}), (Equiv.optionEquivSumPUnit α).symm (Sum.inr a) = none
-- Mathlib.SetTheory.ZFC.PSet
PSet.mk.injEq : ∀ (α : Type u) (A : α → PSet.{u}) (α_1 : Type u) (A_1 : α_1 → PSet.{u}),
  (PSet.mk α A = PSet.mk α_1 A_1) = (α = α_1 ∧ A ≍ A_1)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.leftUnitor_inv_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G : CategoryTheory.Grp C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor G).inv.hom.hom =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor G.X).inv
-- Lean.Meta.Tactic.Simp.Types
/-- Executes `x` using a `MetaM` configuration for inferred from `Simp.Config`.
 -/
Lean.Meta.Simp.withSimpMetaConfig : {α : Type} → Lean.Meta.SimpM α → Lean.Meta.SimpM α
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.CompletionClientCapabilities.completionItem? : Lean.Lsp.CompletionClientCapabilities → Option Lean.Lsp.CompletionItemCapabilities
-- Init.Control.Id
/-- The identity monad has a `bind` operator.
 -/
Id.hasBind : Bind Id
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.subsingleton_of_subsingleton : ∀ {M : Type u_1} [inst : Mul M] [Subsingleton (Subsemigroup M)], Subsingleton M
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsPosSemidef.isSymm : ∀ {R : Type u_1} {M : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {I₁ : R →+* R}
  [inst_3 : LE R] {B : M →ₛₗ[I₁] M →ₗ[R] R}, B.IsPosSemidef → B.IsSymm
-- Mathlib.LinearAlgebra.RootSystem.Defs
/-- This is the pairing between roots and coroots.  -/
RootPairing.pairing : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] → [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → RootPairing ι R M N → ι → ι → R
-- Mathlib.Analysis.Normed.Order.Lattice
/-- Let `α` be an `AddCommGroup` with a `Lattice` structure. A norm on `α` is *solid* if, for `a`
and `b` in `α`, with absolute values `|a|` and `|b|` respectively, `|a| ≤ |b|` implies `‖a‖ ≤ ‖b‖`.
 -/
HasSolidNorm : (α : Type u_1) → [NormedAddCommGroup α] → [Lattice α] → Prop
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_mul_const : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {L : Type u_6} [inst : RCLike L] (r : L)
  (f : α → L), ∫ (a : α), f a * r ∂μ = (∫ (a : α), f a ∂μ) * r
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey?_eraseKey_le_maxKey? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  {k km kme : α} {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ (hkme : Std.Internal.List.maxKey? (Std.Internal.List.eraseKey k l) = some kme),
      (Std.Internal.List.maxKey? l).get ⋯ = km → (compare kme km).isLE = true
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.isSuccPrelimit_aleph0 : Order.IsSuccPrelimit Cardinal.aleph0
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.cokernelSequenceCycles_X₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ),
  (X.cokernelSequenceCycles f g fg h n).X₁ = (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ f)
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- A subfamily of an orthonormal family (i.e., a composition with an injective map) is an
orthonormal family.  -/
Orthonormal.comp : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {ι' : Type u_5} {v : ι → E},
  Orthonormal 𝕜 v → ∀ (f : ι' → ι), Function.Injective f → Orthonormal 𝕜 (v ∘ f)
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.toNat_add : ∀ {c d : Cardinal.{u}},
  c < Cardinal.aleph0 → d < Cardinal.aleph0 → Cardinal.toNat (c + d) = Cardinal.toNat c + Cardinal.toNat d
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isSome_minKey?_insertIfNew! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α} {v : β k}, (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).minKey?.isSome = true
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
HasSum.hasSum_symmetricIco_of_hasSum_symmetricIcc : ∀ {α : Type u_1} {f : ℤ → α} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α] [ContinuousAdd α] {a : α},
  HasSum f a (SummationFilter.symmetricIcc ℤ) →
    Filter.Tendsto (fun N => -f ↑N) Filter.atTop (nhds 0) → HasSum f a (SummationFilter.symmetricIco ℤ)
-- Mathlib.Data.Fintype.Order
/-- A finite bounded distributive lattice is completely distributive.  -/
Fintype.toCompleteDistribLattice : (α : Type u_2) → [Fintype α] → [inst : DistribLattice α] → [BoundedOrder α] → CompleteDistribLattice α
-- Mathlib.FieldTheory.RatFunc.Valuation
RatFunc.inftyValuation_apply : ∀ (F : Type u_1) [inst : Field F] [inst_1 : DecidableEq (RatFunc F)] {x : RatFunc F},
  (RatFunc.inftyValuation F) x = RatFunc.inftyValuationDef F x
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.opOrderIso_symm_apply : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (I : TwoSidedIdeal Rᵐᵒᵖ),
  (RelIso.symm TwoSidedIdeal.opOrderIso) I = I.unop
-- Mathlib.Order.Filter.AtTopBot.Archimedean
Filter.Eventually.intCast_atTop : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] {p : R → Prop},
  (∀ᶠ (x : R) in Filter.atTop, p x) → ∀ᶠ (n : ℤ) in Filter.atTop, p ↑n
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.add_period : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c₁ c₂ : α} [inst : AddSemigroup α],
  Function.Periodic f c₁ → Function.Periodic f c₂ → Function.Periodic f (c₁ + c₂)
-- Mathlib.Analysis.Normed.Order.Hom.Basic
GroupSeminormClass.toSeminormedGroup.eq_1 : ∀ {F : Type u_1} {α : Type u_2} [inst : FunLike F α ℝ] [inst_1 : Group α] [inst_2 : GroupSeminormClass F α ℝ] (f : F),
  GroupSeminormClass.toSeminormedGroup f =
    { norm := ⇑f, toGroup := inst_1, dist := fun x y => f (x⁻¹ * y), dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯,
      edist_dist := ⋯, uniformity_dist := ⋯, cobounded_sets := ⋯, dist_eq := ⋯ }
-- Mathlib.Algebra.Group.Commute.Defs
/-- If `a` commutes with both `b` and `c`, then it commutes with their product.  -/
Commute.mul_right : ∀ {S : Type u_3} [inst : Semigroup S] {a b c : S}, Commute a b → Commute a c → Commute a (b * c)
-- Mathlib.Topology.Order.LeftRightNhds
mem_nhdsGT_iff_exists_mem_Ioc_Ioo_subset : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a u' : α} {s : Set α},
  a < u' → (s ∈ nhdsWithin a (Set.Ioi a) ↔ ∃ u ∈ Set.Ioc a u', Set.Ioo a u ⊆ s)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.dart_snd_mem_support_of_mem_darts : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {d : G.Dart}, d ∈ p.darts → d.toProd.2 ∈ p.support
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.compLinearMap_apply : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₁' : ι → Type v₁'} {M₂ : Type v₂} [inst : Semiring 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₂) (f : (i : ι) → M₁ i →ₗ[R] M₁' i) (m : (i : ι) → M₁ i),
  (g.compLinearMap f) m = g fun i => (f i) (m i)