mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Parser.Term
Lean.Parser.Term.forall : Lean.Parser.Parser
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get_union_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [inst : Std.TransCmp cmp] (h₁ : t₁.WF)
  (h₂ : t₂.WF) {k : α} (not_mem : k ∉ t₂) {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂).get k h' = t₁.get k ⋯
-- Mathlib.LinearAlgebra.Matrix.Stochastic
Matrix.mem_colStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {M : Matrix n n R},
  M ∈ Matrix.colStochastic R n ↔ (∀ (i j : n), 0 ≤ M i j) ∧ Matrix.vecMul 1 M = 1
-- Init.Data.String.Lemmas.FindPos
String.Pos.prevn_zero : ∀ {s : String} {p : s.Pos}, p.prevn 0 = p
-- Std.Time.Date.Unit.Weekday
Std.Time.Weekday.instInhabitedOrdinal : Inhabited Std.Time.Weekday.Ordinal
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
/-- A completely pseudometrizable T0 space is completely metrizable.  -/
TopologicalSpace.IsCompletelyMetrizableSpace_of_isCompletelyPseudoMetrizableSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace X] [T0Space X],
  TopologicalSpace.IsCompletelyMetrizableSpace X
-- Std.Http.Data.Status
/-- 206 Partial Content
 -/
Std.Http.Status.partialContent : Std.Http.Status
-- Init.Data.String.Basic
String.toList_empty : "".toList = []
-- Init.Data.BitVec.Lemmas
/-- Sign extending to a larger bitwidth depends on the msb.
If the msb is false, then the result equals the original value.
If the msb is true, then we add a value of `(2^v - 2^w)`, which arises from the sign extension.  -/
_private.Init.Data.BitVec.Lemmas.0.BitVec.toNat_signExtend_of_le : ∀ {w : ℕ} (x : BitVec w) {v : ℕ},
  w ≤ v → (BitVec.signExtend v x).toNat = x.toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₃₂_comp_d₂₁ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupHomology.d₃₂ A) (groupHomology.d₂₁ A) = 0
-- Init.Data.Option.Attach
OptionT.instLawfulMonadAttachOfLawfulMonad : ∀ {m : Type u_1 → Type u_2} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m] [LawfulMonadAttach m],
  LawfulMonadAttach (OptionT m)
-- Mathlib.NumberTheory.Divisors
Nat.divisors_subset_properDivisors : ∀ {n m : ℕ}, n ≠ 0 → m ∣ n → m ≠ n → m.divisors ⊆ n.properDivisors
-- Init.Data.Order.Ord
List.instOrientedCmpCompareLex : ∀ {α : Type u_1} {cmp : α → α → Ordering} [Std.OrientedCmp cmp], Std.OrientedCmp (List.compareLex cmp)
-- Mathlib.Order.Lattice
Subtype.mk_inf_mk : ∀ {α : Type u} [inst : SemilatticeInf α] {P : α → Prop} (Pinf : ∀ ⦃x y : α⦄, P x → P y → P (x ⊓ y)) {x y : α} (hx : P x)
  (hy : P y), ⟨x, hx⟩ ⊓ ⟨y, hy⟩ = ⟨x ⊓ y, ⋯⟩
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.ext_norm_arg : ∀ {x y : ℂ}, ‖x‖ = ‖y‖ → x.arg = y.arg → x = y
-- Mathlib.Data.Set.Functor
Set.eq_univ_of_coe_eq : ∀ {α : Type u} {β : Set α} {γ : Set ↑β},
  (do
        let a ← γ
        pure ↑a) =
      β →
    γ = Set.univ
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
le_csInf : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α}, s.Nonempty → (∀ b ∈ s, a ≤ b) → a ≤ sInf s
-- Mathlib.Data.Fin.Tuple.Basic
Fin.removeNth_update : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (p : Fin (n + 1)) (x : α p) (f : (j : Fin (n + 1)) → α j),
  p.removeNth (Function.update f p x) = p.removeNth f
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get_modify_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : β → β} {h : k ∈ Std.DHashMap.Const.modify m k f},
  Std.DHashMap.Const.get (Std.DHashMap.Const.modify m k f) k h = f (Std.DHashMap.Const.get m k ⋯)
-- Init.Data.Int.Basic
/-- Power of an integer to a natural number, usually accessed via the `^` operator.

Examples:
* `(2 : Int) ^ 4 = 16`
* `(10 : Int) ^ 0 = 1`
* `(0 : Int) ^ 10 = 0`
* `(-7 : Int) ^ 3 = -343`
 -/
Int.pow : ℤ → ℕ → ℤ
-- Mathlib.RingTheory.MvPowerSeries.Restricted
MvPowerSeries.IsRestricted.eq_1 : ∀ {R : Type u_1} [inst : NormedRing R] {σ : Type u_2} (c : σ → ℝ) (f : MvPowerSeries σ R),
  MvPowerSeries.IsRestricted c f =
    Filter.Tendsto (fun t => ‖(MvPowerSeries.coeff t) f‖ * t.prod fun x1 x2 => c x1 ^ x2) Filter.cofinite (nhds 0)
-- Mathlib.ModelTheory.ElementarySubstructures
FirstOrder.Language.ElementarySubstructure.coe_top : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M], ↑⊤ = Set.univ
-- Mathlib.Order.Filter.CountablyGenerated
/-- A countably generated filter admits a basis formed by an antitone sequence of sets.  -/
Filter.exists_antitone_basis : ∀ {α : Type u_1} (f : Filter α) [f.IsCountablyGenerated], ∃ x, f.HasAntitoneBasis x
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
/-- Implementation; see `nonempty_indParallelPairPresentation`.  -/
CategoryTheory.NonemptyParallelPairPresentationAux.ψ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} →
      (f g : A ⟶ B) →
        (P₁ : CategoryTheory.Limits.IndObjectPresentation A) →
          (P₂ : CategoryTheory.Limits.IndObjectPresentation B) →
            CategoryTheory.NonemptyParallelPairPresentationAux.F₁ f g P₁ P₂ ⟶
              CategoryTheory.NonemptyParallelPairPresentationAux.F₂ f g P₁ P₂
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.IsOrtho.prod : ∀ {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid P] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} {v w : M₁ × M₂},
  Q₁.IsOrtho v.1 w.1 → Q₂.IsOrtho v.2 w.2 → (Q₁.prod Q₂).IsOrtho v w
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas
/-- This is Lemma 2.6 from [Geck](Geck2017).  -/
RootPairing.chainBotCoeff_mul_chainTopCoeff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : CharZero R]
  [inst_2 : IsDomain R] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  {P : RootPairing ι R M N} [inst_7 : Finite ι] [inst_8 : P.IsCrystallographic] {b : P.Base} {i j k l m : ι}
  [P.IsReduced] [P.IsIrreducible],
  i ∈ b.support →
    j ∈ b.support →
      i ≠ j →
        P.root k + P.root i = P.root l →
          P.root k - P.root j = P.root m →
            P.root k + P.root i - P.root j ∈ Set.range ⇑P.root →
              (RootPairing.chainBotCoeff i m + 1) * (RootPairing.chainTopCoeff j k + 1) =
                (RootPairing.chainTopCoeff j l + 1) * (RootPairing.chainBotCoeff i k + 1)
-- Mathlib.Order.Interval.Set.Pi
Set.pi_univ_uIcc : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Lattice (α i)] (a b : (i : ι) → α i),
  (Set.univ.pi fun i => Set.uIcc (a i) (b i)) = Set.uIcc a b
-- Mathlib.Data.Set.Disjoint
Set.disjoint_of_subset : ∀ {α : Type u} {s₁ s₂ t₁ t₂ : Set α}, s₁ ⊆ s₂ → t₁ ⊆ t₂ → Disjoint s₂ t₂ → Disjoint s₁ t₁
-- Mathlib.Analysis.Seminorm
Seminorm.ball_add_ball_subset : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E]
  (p : Seminorm 𝕜 E) (r₁ r₂ : ℝ) (x₁ x₂ : E), p.ball x₁ r₁ + p.ball x₂ r₂ ⊆ p.ball (x₁ + x₂) (r₁ + r₂)
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.delete_comm : ∀ {α : Type u_1} (M : Matroid α) (D₁ D₂ : Set α), (M.delete D₁).delete D₂ = (M.delete D₂).delete D₁
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.RealizeConstantResult : Type
-- Mathlib.Analysis.Calculus.VectorField
VectorField.lieBracketWithin_of_isOpen : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W : E → E} {s : Set E} {x : E},
  IsOpen s → x ∈ s → VectorField.lieBracketWithin 𝕜 V W s x = VectorField.lieBracket 𝕜 V W x
-- Mathlib.Order.Basic
/-- Transfer a `PartialOrder` on `β` to a `PartialOrder` on `α` using an injective
function `f : α → β`.

See also `Function.Injective.partialOrder` when only the proof fields need to be transferred.

See note [reducible non-instances].  -/
PartialOrder.lift : {α : Type u_2} → {β : Type u_3} → [PartialOrder β] → (f : α → β) → Function.Injective f → PartialOrder α
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.SameKeys.below.inner : ∀ {α : Type u} {β : α → Type v} {β' : α → Type u_1}
  {motive : (a : Std.DTreeMap.Internal.Impl α β) → (a_1 : Std.DTreeMap.Internal.Impl α β') → a.SameKeys a_1 → Prop}
  (sz : ℕ) (k : α) (v : β k) (v' : β' k) (r : Std.DTreeMap.Internal.Impl α β) (r' : Std.DTreeMap.Internal.Impl α β')
  (l : Std.DTreeMap.Internal.Impl α β) (l' : Std.DTreeMap.Internal.Impl α β') (a : r.SameKeys r') (a_1 : l.SameKeys l'),
  Std.DTreeMap.Internal.Impl.SameKeys.below a →
    motive r r' a →
      Std.DTreeMap.Internal.Impl.SameKeys.below a_1 → motive l l' a_1 → Std.DTreeMap.Internal.Impl.SameKeys.below ⋯
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.unit_pow : ∀ {M : Type u_1} [inst : Monoid M] {a : M} (h : IsUnit a) (n : ℕ), ⋯.unit = h.unit ^ n
-- Mathlib.CategoryTheory.Action.Limits
Action.functorCategoryEquivalence_additive : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.Preadditive V], (Action.functorCategoryEquivalence V G).functor.Additive
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
MulOpposite.toLinearEquiv_opLinearIsometryEquiv : ∀ {R : Type u_11} {H : Type u_12} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup H] [inst_2 : Module R H],
  (MulOpposite.opLinearIsometryEquiv R H).toLinearEquiv = MulOpposite.opLinearEquiv R
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- Constructing an affine map and coercing back to a function
produces the same map.  -/
AffineMap.coe_mk : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] (f : P1 → P2) (linear : V1 →ₗ[k] V2)
  (add : ∀ (p : P1) (v : V1), f (v +ᵥ p) = linear v +ᵥ f p), ⇑{ toFun := f, linear := linear, map_vadd' := add } = f
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {l : List α} {k : α} {fallback : Unit},
  (Std.HashMap.unitOfList l).getD k fallback = ()
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
CategoryTheory.Preadditive.RightFreyd.rightFunctor_obj : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] (X : V),
  (CategoryTheory.Preadditive.RightFreyd.rightFunctor V).obj X = CategoryTheory.Arrow.mk 0
-- Mathlib.CategoryTheory.Monoidal.Transport
CategoryTheory.Monoidal.instMonoidalTransportedInverseSymmEquivalenceTransported : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          (e : C ≌ D) → (CategoryTheory.Monoidal.equivalenceTransported e).symm.inverse.Monoidal
-- Init.Data.Slice.Array.Lemmas
Array.array_mkSlice_rii : ∀ {α : Type u_1} {xs : Array α}, (Std.Rii.Sliceable.mkSlice xs *...*).array = xs
-- Qq.Match
_private.Qq.Match.0.Qq.liftsToDoItems : Array Qq.Lift✝ → Lean.MacroM (Array (Lean.TSyntax `Lean.Parser.Term.doSeqItem))
-- Mathlib.Algebra.Group.Hom.Defs
map_sub' : ∀ {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : SubNegMonoid G]
  [inst_2 : SubNegMonoid H] [AddHomClass F G H] (f : F), (∀ (a : G), f (-a) = -f a) → ∀ (a b : G), f (a - b) = f a - f b
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
/-- If `N` is a submodule in an algebra `S` over `R`,
there is the natural isomorphism of `R`-modules between
`i(R) ⊗[R] N` and `N` induced by multiplication in `S`, here `i : R → S` is the structure map.
This generalizes `TensorProduct.lid` as `i(R)` is not necessarily isomorphic to `R`.  -/
Submodule.lTensorOne : {R : Type u} →
  {S : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring S] → [inst_2 : Algebra R S] → (N : Submodule R S) → TensorProduct R ↥⊥ ↥N ≃ₗ[R] ↥N
-- Init.Data.Int.Order
Int.instLawfulOrderLeftLeaningMin : Std.LawfulOrderLeftLeaningMin ℤ
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.tensor.sizeOf_spec : ∀ {C : Type u} [inst : SizeOf C] {W X Y Z : CategoryTheory.FreeMonoidalCategory C} (f : W.Hom Y) (g : X.Hom Z),
  sizeOf (f.tensor g) = 1 + sizeOf W + sizeOf X + sizeOf Y + sizeOf Z + sizeOf f + sizeOf g
-- Mathlib.Order.Disjoint
/-- If `x` and `y` are to be complementary in an order, they should be disjoint.  -/
IsCompl.disjoint : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α] {x y : α}, IsCompl x y → Disjoint x y
-- Lean.Elab.PreDefinition.TerminationMeasure
_private.Lean.Elab.PreDefinition.TerminationMeasure.0.Lean.Elab.TerminationMeasure.delab.go.match_1.eq_2 : ∀ (motive : ℕ → Lean.TSyntaxArray `ident → Sort u_1) (i : ℕ) (vars : Lean.TSyntaxArray `ident)
  (h_1 : (vars : Lean.TSyntaxArray `ident) → motive 0 vars)
  (h_2 : (i : ℕ) → (vars : Lean.TSyntaxArray `ident) → motive i.succ vars),
  (match i.succ, vars with
    | 0, vars => h_1 vars
    | i.succ, vars => h_2 i vars) =
    h_2 i vars
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.ae_restrict_eq_bot : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.ae (μ.restrict s) = ⊥ ↔ μ s = 0
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.nat_mul_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : NonAssocSemiring α],
  Function.Periodic f c → ∀ (n : ℕ), f (↑n * c) = f 0
-- Std.Time.Format.Modifier
_private.Std.Time.Format.Modifier.0.Std.Time.parseNumberText : (Std.Time.Number ⊕ Std.Time.Text → Std.Time.Modifier) → String → Std.Internal.Parsec.String.Parser Std.Time.Modifier
-- Mathlib.RingTheory.Polynomial.HilbertPoly
_private.Mathlib.RingTheory.Polynomial.HilbertPoly.0.Polynomial.hilbertPoly.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((d : ℕ) → motive d.succ) → motive x
-- Mathlib.CategoryTheory.Equivalence.Symmetry
/-- The forward functor of the equivalence `(C ≌ D) ≌ (D ≌ C)ᵒᵖ`.  -/
CategoryTheory.Equivalence.symmEquivFunctor : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (D : Type u_2) → [inst_1 : CategoryTheory.Category.{v_2, u_2} D] → CategoryTheory.Functor (C ≌ D) (D ≌ C)ᵒᵖ
-- Init.Data.SInt.Bitwise
Int16.or_assoc : ∀ (a b c : Int16), a ||| b ||| c = a ||| (b ||| c)
-- Init.Data.Array.Lemmas
Array.append_left_eq_self : ∀ {α : Type u_1} {xs ys : Array α}, xs ++ ys = ys ↔ xs = #[]
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.coe_add : ∀ {R : Type u} [inst : NonAssocRing R] (s : Subring R) (x y : ↥s), ↑(x + y) = ↑x + ↑y
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.neg_h₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂),
  h.neg.h₀ = -h.h₀
-- Mathlib.CategoryTheory.UnivLE
UnivLE.witness : [UnivLE.{max u v, v}] → CategoryTheory.Functor (Type u) (Type v)
-- Mathlib.MeasureTheory.Group.Measure
/-- If the neutral element of a group is not isolated, then a Haar measure on this group has value
zero on singletons.

The additive version of this instance applies in particular to show that an additive Haar
measure on a nontrivial finite-dimensional real vector space has no atom.  -/
MeasureTheory.Measure.IsHaarMeasure.nullSingletonClass : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : TopologicalSpace G] [IsTopologicalGroup G]
  [BorelSpace G] [T1Space G] [WeaklyLocallyCompactSpace G] [(nhdsWithin 1 {1}ᶜ).NeBot] (μ : MeasureTheory.Measure G)
  [μ.IsHaarMeasure], MeasureTheory.NullSingletonClass μ
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin.0.Fin.Value.value : (self : Fin.Value✝) → Fin (Fin.Value.n✝ self)
-- Init.Data.String.Termination
/-- Type alias for `String.Slice.Pos` representing that the given position is expected to decrease
in recursive calls.  -/
String.Slice.Pos.Down : String.Slice → Type
-- Mathlib.MeasureTheory.Integral.CircleIntegral
continuous_circleMap : ∀ (c : ℂ) (R : ℝ), Continuous (circleMap c R)
-- Mathlib.Algebra.Torsor.Basic
div_mul_sdiv_comm : ∀ {G : Type u_1} {P : Type u_2} [inst : CommGroup G] [inst_1 : Torsor G P] (v₁ v₂ : G) (p₁ p₂ : P),
  v₁ / v₂ * (p₁ /ₛ p₂) = v₁ • p₁ /ₛ v₂ • p₂
-- Lean.ParserCompiler
/-- Translate an expression of type `Parser` into one of type `tyName`, tagging intermediary constants with
`ctx.combinatorAttr`. If `force` is `false`, refuse to do so for imported constants.  -/
Lean.ParserCompiler.compileParserExpr : {α : Type} → Lean.ParserCompiler.Context α → Bool → Bool → Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.Vector.MapIdx
Vector.mapIdx_eq_mapFinIdx : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : ℕ → α → β},
  Vector.mapIdx f xs = xs.mapFinIdx fun i a x => f i a
-- Mathlib.Topology.Semicontinuity.Defs
HasOpenLowerSectionsOn.const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {s : Set α} {z : Set β},
  HasOpenLowerSectionsOn (fun _x => z) s
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.mk.injEq : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] (asHomogeneousIdeal : HomogeneousIdeal 𝒜) (isPrime : asHomogeneousIdeal.toIdeal.IsPrime)
  (not_irrelevant_le : ¬HomogeneousIdeal.irrelevant 𝒜 ≤ asHomogeneousIdeal) (asHomogeneousIdeal_1 : HomogeneousIdeal 𝒜)
  (isPrime_1 : asHomogeneousIdeal_1.toIdeal.IsPrime)
  (not_irrelevant_le_1 : ¬HomogeneousIdeal.irrelevant 𝒜 ≤ asHomogeneousIdeal_1),
  ({ asHomogeneousIdeal := asHomogeneousIdeal, isPrime := isPrime, not_irrelevant_le := not_irrelevant_le } =
      { asHomogeneousIdeal := asHomogeneousIdeal_1, isPrime := isPrime_1, not_irrelevant_le := not_irrelevant_le_1 }) =
    (asHomogeneousIdeal = asHomogeneousIdeal_1)
-- Mathlib.AlgebraicGeometry.Sites.Representability
AlgebraicGeometry.Scheme.LocalRepresentability.glueData_f : ∀ {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type u)} {ι : Type u}
  {X : ι → AlgebraicGeometry.Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj}
  (hf : ∀ (i : ι), AlgebraicGeometry.IsOpenImmersion.presheaf (f i)) (i j : ι),
  (AlgebraicGeometry.Scheme.LocalRepresentability.glueData hf).f i j = ⋯.fst' (f j)
-- Mathlib.RingTheory.UniqueFactorizationDomain.Defs
WfDvdMonoid.isRelPrime_of_no_irreducible_factors : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [WfDvdMonoid α] {x y : α},
  ¬(x = 0 ∧ y = 0) → (∀ (z : α), Irreducible z → z ∣ x → ¬z ∣ y) → IsRelPrime x y
-- Mathlib.Algebra.Homology.DifferentialObject
CategoryTheory.DifferentialObject.eqToHom_f' : ∀ {β : Type u_1} [inst : AddCommGroup β] {b : β} {V : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} V]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V]
  {X Y : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)} (f : X ⟶ Y) {x y : β}
  (h : x = y),
  CategoryTheory.CategoryStruct.comp (X.objEqToHom h) (f.f y) =
    CategoryTheory.CategoryStruct.comp (f.f x) (Y.objEqToHom h)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {fallback : β k}, (t₁ ∪ t₂).getD k fallback = t₂.getD k (t₁.getD k fallback)
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- In probability theory, a family of measurable functions is uniformly integrable if it is
uniformly integrable in the measure theory sense and is uniformly bounded.  -/
MeasureTheory.UniformIntegrable : {α : Type u_1} →
  {β : Type u_2} →
    {ι : Type u_3} →
      [NormedAddCommGroup β] → {x : MeasurableSpace α} → (ι → α → β) → ENNReal → MeasureTheory.Measure α → Prop
-- Mathlib.Data.DFinsupp.Lex
/-- The linear order on `DFinsupp`s obtained by the colexicographic ordering.  -/
DFinsupp.Colex.linearOrder : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : (i : ι) → Zero (α i)] →
      [LinearOrder ι] → [(i : ι) → LinearOrder (α i)] → LinearOrder (Colex (Π₀ (i : ι), α i))
-- Mathlib.Topology.FiberBundle.Constructions
/-- A fiber bundle trivialization can be pulled back to a trivialization on the pullback bundle.  -/
Bundle.Trivialization.pullback : {B : Type u} →
  {F : Type v} →
    {E : B → Type w₁} →
      {B' : Type w₂} →
        [inst : TopologicalSpace B'] →
          [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] →
            [inst_2 : TopologicalSpace F] →
              [inst_3 : TopologicalSpace B] →
                [∀ (_b : B), Nonempty (E _b)] →
                  {K : Type U} →
                    [inst_5 : FunLike K B' B] →
                      [ContinuousMapClass K B' B] →
                        Bundle.Trivialization F Bundle.TotalSpace.proj →
                          (f : K) → Bundle.Trivialization F Bundle.TotalSpace.proj
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.IsLower.toContinuousInf : ∀ {α : Type u_1} [inst : CompleteLattice α] [inst_1 : TopologicalSpace α] [Topology.IsLower α], ContinuousInf α
-- Mathlib.Topology.Compactness.Lindelof
HereditarilyLindelofSpace.mk : ∀ {X : Type u_2} [inst : TopologicalSpace X], IsHereditarilyLindelof Set.univ → HereditarilyLindelofSpace X
-- Lean.Meta.DiscrTree.Main
/-- When `noIndexAtArgs := true`, `pushArgs` assumes function application arguments have a `no_index` annotation.
That is, `f a b` is indexed as it was `f (no_index a) (no_index b)`.
This feature is used when indexing local proofs in the simplifier. This is useful in examples like the one described on issue #2670.
In this issue, we have a local hypotheses `(h : ∀ p : α × β, f p p.2 = p.2)`, and users expect it to be applicable to
`f (a, b) b = b`. This worked in Lean 3 since no indexing was used. We can retrieve Lean 3 behavior by writing
`(h : ∀ p : α × β, f p (no_index p.2) = p.2)`, but this is very inconvenient when the hypotheses was not written by the user in first place.
For example, it was introduced by another tactic. Thus, when populating the discrimination tree explicit arguments provided to `simp` (e.g., `simp [h]`),
we use `noIndexAtArgs := true`. See comment: https://github.com/leanprover/lean4/issues/2670#issuecomment-1758889365
 -/
Lean.Meta.DiscrTree.mkPath : Lean.Expr → optParam Bool false → Lean.MetaM (Array Lean.Meta.DiscrTree.Key)
-- Init.Data.UInt.Lemmas
USize.instLawfulOrderLT : Std.LawfulOrderLT USize
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Internal implementation detail of the iterator library.  -/
Std.IteratorLoop.WithWF.acc : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Std.Iterator α m β] →
        {γ : Type x} →
          {PlausibleForInStep : β → γ → ForInStep γ → Prop} →
            {hwf : Std.IteratorLoop.WellFounded α m PlausibleForInStep} →
              Std.IteratorLoop.WithWF α m PlausibleForInStep hwf → γ
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- The functor `Opens X ⥤ Opens Y` associated with an open immersion `f : X ⟶ Y`.  -/
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : AlgebraicGeometry.PresheafedSpace C} →
      (f : X ⟶ Y) →
        [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] →
          CategoryTheory.Functor (TopologicalSpace.Opens ↑↑X) (TopologicalSpace.Opens ↑↑Y)