mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.mapArrowRight_comp_assoc : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {f₁ : CategoryTheory.Arrow C₁}
  {f₂ f₂' : CategoryTheory.Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) (sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom)
  {f₂'' : CategoryTheory.Arrow C₂} (sq₁₂'' : F.PushoutObjObj f₁.hom f₂''.hom) (sq : f₂ ⟶ f₂') (sq' : f₂' ⟶ f₂'')
  {Z : CategoryTheory.Arrow C₃} (h : CategoryTheory.Arrow.mk sq₁₂''.ι ⟶ Z),
  CategoryTheory.CategoryStruct.comp (sq₁₂.mapArrowRight sq₁₂' sq)
      (CategoryTheory.CategoryStruct.comp (sq₁₂'.mapArrowRight sq₁₂'' sq') h) =
    CategoryTheory.CategoryStruct.comp (sq₁₂.mapArrowRight sq₁₂'' (CategoryTheory.CategoryStruct.comp sq sq')) h
-- Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp
factorization_one : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] [inst_2 : NormalizationMonoid α]
  [inst_3 : DecidableEq α], factorization 1 = 0
-- Mathlib.Order.Category.DistLat
_private.Mathlib.Order.Category.DistLat.0.DistLat.Hom.mk.injEq : ∀ {X Y : DistLat} (hom' hom'_1 : LatticeHom ↑X ↑Y), ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.lcomp_apply' : ∀ {R : Type u_1} {S : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] {M : Type u_5} {M₂ : Type u_6} {N : Type u_7}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : AddCommMonoid N] [inst_5 : Module R M]
  [inst_6 : Module R M₂] [inst_7 : Module S N] [inst_8 : Module R N] [inst_9 : SMulCommClass R S N] (f : M →ₗ[R] M₂)
  (g : M₂ →ₗ[R] N), (LinearMap.lcomp S N f) g = g ∘ₗ f
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.instNSMul : {α : Type u_2} →
  [inst : AddMonoid α] → [inst_1 : Preorder α] → [AddLeftMono α] → [AddRightMono α] → SMul ℕ (NonemptyInterval α)
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
/-- The degree `[L : D]` of `L` over the decomposition field `D` equals the product of the
ramification index and the inertia degree of `p` in `B`.
 -/
IsDecompositionField.rank_left : ∀ (A : Type u_1) (K : Type u_2) (L : Type u_3) {B : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra A B] {p : Ideal A} (P : Ideal B) [P.LiesOver p]
  [FiniteDimensional K L] [inst_8 : MulSemiringAction Gal(L/K) B] [IsGaloisGroup Gal(L/K) A B] [IsDedekindDomain A]
  [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [Ring.HasFiniteQuotients A] [P.IsMaximal]
  (D : Type u_5) [inst_16 : Field D] [inst_17 : Algebra D L] [IsDecompositionField K L P D],
  p ≠ ⊥ → Module.finrank D L = p.ramificationIdxIn B * p.inertiaDegIn B
-- Mathlib.Data.Finset.Basic
/-- After filtering out everything that does not equal a given value, at most that value remains.

This is equivalent to `filter_eq` with the equality the other way.
 -/
Finset.filter_eq' : ∀ {β : Type u_2} [inst : DecidableEq β] (s : Finset β) (b : β), {a ∈ s | a = b} = if b ∈ s then {b} else ∅
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.induction_on : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] [inst_1 : DecidableEq ι]
  {motive : (DirectSum ι fun i => β i) → Prop} (x : DirectSum ι fun i => β i),
  motive 0 →
    (∀ (i : ι) (x : β i), motive ((DirectSum.of β i) x)) →
      (∀ (x y : DirectSum ι fun i => β i), motive x → motive y → motive (x + y)) → motive x
-- Mathlib.Data.Finset.NatAntidiagonal
Finset.Nat.antidiagonal.fst_lt : ∀ {n : ℕ} {kl : ℕ × ℕ}, kl ∈ Finset.HasAntidiagonal.antidiagonal n → kl.1 < n + 1
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
Submodule.instCoeAffineSubspace : {k : Type u_1} →
  {V : Type u_2} →
    [inst : Ring k] → [inst_1 : AddCommGroup V] → [inst_2 : Module k V] → Coe (Submodule k V) (AffineSubspace k V)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.instDecidableEqBVBinOp : DecidableEq Std.Tactic.BVDecide.BVBinOp
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
IsSemilinearSet.exists_fg_eq_subtypeVal₂ : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s₁ s₂ : Set M},
  IsSemilinearSet s₁ →
    IsSemilinearSet s₂ →
      ∃ P s₁' s₂', P.FG ∧ IsSemilinearSet s₁' ∧ s₁ = Subtype.val '' s₁' ∧ IsSemilinearSet s₂' ∧ s₂ = Subtype.val '' s₂'
-- Aesop.Percent
Aesop.Percent.δ : Aesop.Percent
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.support_single_subset : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {a : Γ} {r : R},
  ((HahnSeries.single a) r).support ⊆ {a}
-- Mathlib.CategoryTheory.Category.Factorisation
/-- The morphism out of the factorisation midpoint.  -/
CategoryTheory.Factorisation.π : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → {f : X ⟶ Y} → (self : CategoryTheory.Factorisation f) → self.mid ⟶ Y
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.destruct_some_of_destruct_tail_some : ∀ {α : Type u} {s : Stream'.WSeq α} {a : α × Stream'.WSeq α}, some a ∈ s.tail.destruct → ∃ a', some a' ∈ s.destruct
-- Mathlib.Topology.Order.OrderClosed
Dense.exists_lt : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] [NoMinOrder α] {s : Set α},
  Dense s → ∀ (x : α), ∃ y ∈ s, y < x
-- Batteries.Data.Array.Match
/-- Returns the size of the prefix table  -/
Array.PrefixTable.size : {α : Type u_1} → Array.PrefixTable α → ℕ
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.stoppedValue_lowerCrossingTime : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n : ℕ} {ω : Ω},
  MeasureTheory.lowerCrossingTime a b f N n ω ≠ N →
    MeasureTheory.stoppedValue f (fun ω => ↑(MeasureTheory.lowerCrossingTime a b f N n ω)) ω ≤ a
-- Mathlib.Data.Finset.Fold
Finset.fold_image : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op]
  {f : α → β} {b : β} [inst : DecidableEq α] {g : γ → α} {s : Finset γ},
  Set.InjOn g ↑s → Finset.fold op b f (Finset.image g s) = Finset.fold op b (f ∘ g) s
-- Mathlib.Order.InitialSeg
/-- An initial segment embedding between the `<` relations of two partial orders is an order
embedding.  -/
InitialSeg.toOrderEmbedding : {α : Type u_1} → {β : Type u_2} → [inst : PartialOrder α] → [inst_1 : PartialOrder β] → (α ≤i β) → α ↪o β
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.inv : ∀ {α : Type u} [inst : DivisionMonoid α] {a : α}, IsUnit a → IsUnit a⁻¹
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Matrix.charpoly.univ_map_map : ∀ {R : Type u_1} {S : Type u_2} (n : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Fintype n]
  [inst_3 : DecidableEq n] (f : R →+* S),
  Polynomial.map (MvPolynomial.map f) (Matrix.charpoly.univ R n) = Matrix.charpoly.univ S n
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
/-- Given `W : J ⥤ Type w` and `F : J ⥤ C`, this is the type of cones for
the functor `CategoryOfElements.π W ⋙ F : W.Elements ⥤ C`.  -/
CategoryTheory.Limits.WeightedCone : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        CategoryTheory.Functor J (Type w) → CategoryTheory.Functor J C → Type (max (max (max u w) u') v')
-- Mathlib.Topology.Subpath
/-- Concatenating zero paths yields the constant path (the identity of `Path.trans`).  -/
Path.concat_zero : ∀ {X : Type u_1} [inst : TopologicalSpace X] (p : Fin 1 → X) (F : (k : Fin 0) → Path (p k.castSucc) (p k.succ)),
  Path.concat p F = Path.refl (p 0)
-- Mathlib.Data.PNat.Factors
PrimeMultiset.coePNat_prime : ∀ (v : PrimeMultiset), ∀ p ∈ v.toPNatMultiset, p.Prime
-- Mathlib.Topology.LocallyFinsupp
/-- Restriction as a group morphism  -/
Function.locallyFinsuppWithin.restrictMonoidHom : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {U : Set X} →
      {Y : Type u_2} →
        [inst_1 : AddCommGroup Y] →
          {V : Set X} → V ⊆ U → Function.locallyFinsuppWithin U Y →+ Function.locallyFinsuppWithin V Y
-- Mathlib.RingTheory.Noetherian.Basic
isNoetherian_of_fg_of_noetherian : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Submodule R M)
  [I : IsNoetherianRing R], N.FG → IsNoetherian R ↥N
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulC.go : Lean.Grind.CommRing.Poly → ℕ → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.instInfOpenAddSubgroup : {G : Type u_1} → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → Min (OpenAddSubgroup G)
-- Mathlib.Analysis.Convex.EGauge
egauge_le_one : ∀ (𝕜 : Type u_1) [inst : NormedDivisionRing 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {s : Set E} {x : E}, x ∈ s → egauge 𝕜 s x ≤ 1
-- Init.System.IO
IO.RealWorld.nonemptyType : NonemptyType
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.mem_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → (k ∈ t₁ ↔ k ∈ t₂)
-- Mathlib.GroupTheory.GroupAction.Support
AddAction.Supports.eq_1 : ∀ (G : Type u_1) {α : Type u_3} {β : Type u_4} [inst : VAdd G α] [inst_1 : VAdd G β] (s : Set α) (b : β),
  AddAction.Supports G s b = ∀ (g : G), (∀ ⦃a : α⦄, a ∈ s → g +ᵥ a = a) → g +ᵥ b = b
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.one_mul : {R : Type u} → [inst : Rack R] → (a : Rack.PreEnvelGroup R) → Rack.PreEnvelGroupRel' R (Rack.PreEnvelGroup.unit.mul a) a
-- Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
_private.Mathlib.Analysis.SpecificLimits.ArithmeticGeometric.0.arithGeom.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Std.Data.DHashMap.Basic
/-- Computes the intersection of the given hash maps. The result will only contain entries from the first map.

This function always iterates through the smaller map, so the expected runtime is
`O(min(m₁.size, m₂.size))`.
 -/
Std.DHashMap.inter : {α : Type u} →
  {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Std.DHashMap α β → Std.DHashMap α β → Std.DHashMap α β
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
SSet.Truncated.HomotopyCategory.descOfTruncation_obj_mk : ∀ {X : SSet.Truncated 2} {C : Type u} [inst : CategoryTheory.SmallCategory C]
  (φ : X ⟶ (SSet.truncation 2).obj (CategoryTheory.nerve C))
  (x : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ })),
  (SSet.Truncated.HomotopyCategory.descOfTruncation φ).obj (SSet.Truncated.HomotopyCategory.mk x) =
    CategoryTheory.nerveEquiv
      ((CategoryTheory.ConcreteCategory.hom (φ.app (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }))) x)
-- Mathlib.Data.Real.Basic
Real.instIsStrictOrderedRing : IsStrictOrderedRing ℝ
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.minKey!_modifyKey : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] [inst_4 : Inhabited α]
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : β → β},
      (Std.Internal.List.Const.modifyKey k f l).isEmpty = false →
        Std.Internal.List.minKey! (Std.Internal.List.Const.modifyKey k f l) =
          if (Std.Internal.List.minKey! l == k) = true then k else Std.Internal.List.minKey! l
-- Mathlib.CategoryTheory.ObjectProperty.InheritedFromHom
CategoryTheory.ObjectProperty.InheritedFromTarget.of_hom_of_target : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {P : CategoryTheory.ObjectProperty C}
  {Q : CategoryTheory.MorphismProperty C} [self : P.InheritedFromTarget Q] {X Y : C} (f : X ⟶ Y), Q f → P Y → P X
-- Init.Data.SInt.Lemmas
Int8.toInt64_ofNat' : ∀ {n : ℕ}, ↑n ≤ Int8.maxValue.toInt → (Int8.ofNat n).toInt64 = Int64.ofNat n
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max!_empty : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α], ∅.max! = default
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
/-- For `n ≠ 0`, `DihedralGroup n` represents the symmetry group of the regular `n`-gon.
`r i` represents the rotations of the `n`-gon by `2πi/n`, and `sr i` represents the reflections of
the `n`-gon. `DihedralGroup 0` corresponds to the infinite dihedral group.
 -/
DihedralGroup : ℕ → Type
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_Ico_eq_integral_Ioo' : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} [inst_2 : PartialOrder X] {x y : X},
  μ {x} = 0 → ∫ (t : X) in Set.Ico x y, f t ∂μ = ∫ (t : X) in Set.Ioo x y, f t ∂μ
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
/-- A functor to the category of monoid objects can be translated as a monoid object
in the functor category.  -/
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          CategoryTheory.Functor C (CategoryTheory.Mon D) → CategoryTheory.Mon (CategoryTheory.Functor C D)
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.instValuationRingInteger : ∀ {K : Type v} {Γ : Type w} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ),
  ValuationRing ↥v.integer
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- A splitting of an extension `S` is `N`-conjugate to another iff there exists `n : N` such
that the section homomorphism is a conjugate of the other section homomorphism by `S.inl n`.  -/
AddGroupExtension.IsAddConj : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : AddGroup N] →
        [inst_1 : AddGroup E] → [inst_2 : AddGroup G] → (S : AddGroupExtension N E G) → S.Splitting → S.Splitting → Prop
-- Mathlib.LinearAlgebra.QuadraticForm.Signature
_private.Mathlib.LinearAlgebra.QuadraticForm.Signature.0.QuadraticForm.posDef_spanSubset : ∀ {𝕜 : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] {ι : Type u_5} [inst_2 : Fintype ι] {w : ι → 𝕜}
  [IsStrictOrderedRing 𝕜] (s : Set ι),
  (∀ i ∈ s, 0 < w i) → ((QuadraticMap.weightedSumSquares 𝕜 w).restrict (Pi.spanSubset 𝕜 s)).PosDef
-- Init.Data.Option.Lemmas
Option.not_some_le_none : ∀ {α : Type u_1} [inst : LE α] {a : α}, ¬some a ≤ none
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.b₆_of_isCharThreeJNeZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF], W.b₆ = 4 * W.a₆
-- Mathlib.Data.ENat.Basic
ENat.lt_one_iff_eq_zero : ∀ {n : ℕ∞}, n < 1 ↔ n = 0
-- Init.Data.Sum.Lemmas
Sum.Lex.mono_right : ∀ {β : Type u_1} {s₁ s₂ : β → β → Prop} {α : Type u_2} {r : α → α → Prop} {x y : α ⊕ β},
  (∀ (a b : β), s₁ a b → s₂ a b) → Sum.Lex r s₁ x y → Sum.Lex r s₂ x y
-- Mathlib.Order.SuccPred.Basic
instPredOrderOrderDualOfSuccOrder : {α : Type u_1} → [inst : Preorder α] → [SuccOrder α] → PredOrder αᵒᵈ
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.truncFinset_truncFinset : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {s t : Finset (σ →₀ ℕ)},
  s ⊆ t →
    ∀ (p : MvPowerSeries σ R),
      (MvPowerSeries.truncFinset R s) ↑((MvPowerSeries.truncFinset R t) p) = (MvPowerSeries.truncFinset R s) p
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- If the product comparison morphism is an iso, its inverse is natural in both argument.  -/
CategoryTheory.CartesianMonoidalCategory.prodComparison_inv_natural_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 A' B' : C}
  [inst_4 : CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B)] (f : A ⟶ A')
  (g : B ⟶ B') [inst_5 : CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.prodComparison F A' B')] {Z : D}
  (h : F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj A' B') ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.inv (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B))
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map f) (F.map g))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.inv (CategoryTheory.CartesianMonoidalCategory.prodComparison F A' B')) h)
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Cauchy–Schwarz inequality for real inner products.  -/
real_inner_mul_inner_self_le : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F),
  inner ℝ x y * inner ℝ x y ≤ inner ℝ x x * inner ℝ y y
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get_insertIfNew : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k a : α} {v : β} {h₁ : a ∈ t.insertIfNew k v},
  Std.ExtDTreeMap.Const.get (t.insertIfNew k v) a h₁ =
    if h₂ : cmp k a = Ordering.eq ∧ k ∉ t then v else Std.ExtDTreeMap.Const.get t a ⋯
-- Mathlib.Order.Category.BoolAlg
BoolAlg.instCoeSortType : CoeSort BoolAlg (Type u_1)
-- Init.Grind.Interactive
Lean.Parser.Tactic.Grind.grindFilter : Lean.ParserDescr
-- Init.Data.String.Basic
String.Slice.Pos.copy_eq_copy_sliceTo_append_get : ∀ {s : String.Slice} {pos : s.Pos} (h : pos ≠ s.endPos),
  s.copy = (s.sliceTo pos).copy ++ String.singleton (pos.get h) ++ (s.sliceFrom (pos.next h)).copy
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.logMap_eq_of_normAtPlace_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x y : NumberField.mixedEmbedding.mixedSpace K},
  (∀ (w : NumberField.InfinitePlace K),
      (NumberField.mixedEmbedding.normAtPlace w) x = (NumberField.mixedEmbedding.normAtPlace w) y) →
    NumberField.mixedEmbedding.logMap x = NumberField.mixedEmbedding.logMap y
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.lift_eq : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)) (x : M),
  (f.lift hg) (f x) = g x
-- Mathlib.NumberTheory.Pell
Pell.Solution₁.y_one : ∀ {d : ℤ}, Pell.Solution₁.y 1 = 0
-- Mathlib.Algebra.Group.Subgroup.Basic
Group.subset_conjugatesOfSet : ∀ {G : Type u_1} [inst : Group G] {s : Set G}, s ⊆ Group.conjugatesOfSet s
-- Mathlib.RingTheory.Nilpotent.GeometricallyReduced
/-- If all finitely generated subalgebras of `A` are geometrically reduced, then `A` is
geometrically reduced.  -/
Algebra.IsGeometricallyReduced.of_forall_fg : ∀ {k : Type u_1} {A : Type u_2} [inst : Field k] [inst_1 : Ring A] [inst_2 : Algebra k A],
  (∀ (B : Subalgebra k A), B.FG → Algebra.IsGeometricallyReduced k ↥B) → Algebra.IsGeometricallyReduced k A
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.toLaurent_reverse : ∀ {R : Type u_3} [inst : CommSemiring R] (p : Polynomial R),
  Polynomial.toLaurent p.reverse = LaurentPolynomial.invert (Polynomial.toLaurent p) * LaurentPolynomial.T ↑p.natDegree
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Given a morphism property `P` on a category `C` and an object `X : C`, this is the
subcategory of `CostructuredArrow F X` defined by `P` where morphisms satisfy `Q`.  -/
CategoryTheory.MorphismProperty.CostructuredArrow : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{u_3, u_1} C] →
      [inst_1 : CategoryTheory.Category.{u_4, u_2} D] →
        CategoryTheory.MorphismProperty D →
          CategoryTheory.MorphismProperty C → CategoryTheory.Functor C D → D → Type (max u_1 u_4)
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.IsSeparated.instRespectsIsoScheme : CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.IsSeparated
-- Mathlib.Topology.Connected.PathConnected
pathComponent.nonempty : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x : X), (pathComponent x).Nonempty
-- Mathlib.Order.Filter.Ker
Filter.ker_sSup : ∀ {α : Type u_2} (S : Set (Filter α)), (sSup S).ker = ⋃ f ∈ S, f.ker
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.interSmallerFn : {α : Type u} → {β : α → Type v} → [BEq α] → List ((a : α) × β a) → List ((a : α) × β a) → α → List ((a : α) × β a)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.j_eq_zero_iff_of_char_two : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [inst_1 : W.IsElliptic] [CharP R 2] [IsReduced R],
  W.j = 0 ↔ W.a₁ = 0
-- Mathlib.Order.CompleteLattice.Defs
CompleteLattice.mk : {α : Type u_8} →
  [toLattice : Lattice α] →
    [toSupSet : SupSet α] →
      (∀ (s : Set α), IsLUB s (sSup s)) →
        [toInfSet : InfSet α] →
          (∀ (s : Set α), IsGLB s (sInf s)) → [toBoundedOrder : BoundedOrder α] → CompleteLattice α
-- Mathlib.Data.Multiset.Filter
Multiset.filter_attach : ∀ {α : Type u_1} (s : Multiset α) (p : α → Prop) [inst : DecidablePred p],
  Multiset.filter (fun a => p ↑a) s.attach = Multiset.map (Subtype.map id ⋯) (Multiset.filter p s).attach
-- Mathlib.Data.ENNReal.Operations
ENNReal.add_le_add_iff_right : ∀ {a b c : ENNReal}, a ≠ ⊤ → (b + a ≤ c + a ↔ b ≤ c)
-- Lean.Parser.Basic
Lean.Parser.categoryParserFnRef : IO.Ref Lean.Parser.CategoryParserFn
-- Std.Data.TreeMap.Raw.WF
Std.TreeMap.Raw.WF.union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {t₁ t₂ : Std.TreeMap.Raw α β cmp},
  t₁.WF → t₂.WF → (t₁ ∪ t₂).WF
-- Mathlib.Algebra.Lie.Engel
/-- *Engel's theorem*.

Note that this implies all traditional forms of Engel's theorem via
`LieModule.nontrivial_max_triv_of_isNilpotent`, `LieModule.isNilpotent_iff_forall`,
`LieAlgebra.isNilpotent_iff_forall`.  -/
LieAlgebra.isEngelian_of_isNoetherian : ∀ {R : Type u₁} {L : Type u₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [IsNoetherian R L],
  LieAlgebra.IsEngelian R L
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.limitConeOfUnique_isLimit_lift : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : Unique β] (f : β → C)
  (s : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor f)),
  (CategoryTheory.Limits.limitConeOfUnique f).isLimit.lift s = s.π.app default
-- Mathlib.Data.Set.Lattice.Image
Set.inj_on_iUnion_of_directed : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : ι → Set α},
  Directed (fun x1 x2 => x1 ⊆ x2) s → ∀ {f : α → β}, (∀ (i : ι), Set.InjOn f (s i)) → Set.InjOn f (⋃ i, s i)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.IsHomogeneous.top : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_5 : GradedRing 𝒜], Ideal.IsHomogeneous 𝒜 ⊤
-- Init.System.IOError
IO.Error.resourceExhausted.injEq : ∀ (filename : Option String) (osCode : UInt32) (details : String) (filename_1 : Option String) (osCode_1 : UInt32)
  (details_1 : String),
  (IO.Error.resourceExhausted filename osCode details = IO.Error.resourceExhausted filename_1 osCode_1 details_1) =
    (filename = filename_1 ∧ osCode = osCode_1 ∧ details = details_1)
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.injective_of_map_algebraMap_zero : ∀ {R : Type u_1} [inst : CommRing R] {M : Submonoid R} (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [IsLocalization M S] {T : Type u_4} [inst_4 : CommRing T] (f : S →+* T),
  (∀ (x : R), f ((algebraMap R S) x) = 0 → (algebraMap R S) x = 0) → Function.Injective ⇑f
-- Lean.Meta.Sym.SymM
/-- Cache for `getLevel` results, keyed by pointer equality.
 -/
Lean.Meta.Sym.State.getLevel : Lean.Meta.Sym.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Level