mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.mk.inj : ∀ {toList : List DyckStep} {count_U_eq_count_D : List.count DyckStep.U toList = List.count DyckStep.D toList}
  {count_D_le_count_U :
    ∀ (i : ℕ), List.count DyckStep.D (List.take i toList) ≤ List.count DyckStep.U (List.take i toList)}
  {toList_1 : List DyckStep} {count_U_eq_count_D_1 : List.count DyckStep.U toList_1 = List.count DyckStep.D toList_1}
  {count_D_le_count_U_1 :
    ∀ (i : ℕ), List.count DyckStep.D (List.take i toList_1) ≤ List.count DyckStep.U (List.take i toList_1)},
  { toList := toList, count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U } =
      { toList := toList_1, count_U_eq_count_D := count_U_eq_count_D_1, count_D_le_count_U := count_D_le_count_U_1 } →
    toList = toList_1
-- Mathlib.Analysis.Real.Sqrt
ContinuousAt.sqrt : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℝ} {x : α}, ContinuousAt f x → ContinuousAt (fun x => √(f x)) x
-- Mathlib.ModelTheory.Syntax
/-- A bijection between terms with constants and terms with extra variables.  -/
FirstOrder.Language.Term.constantsVarsEquivLeft : {L : FirstOrder.Language} →
  {α : Type u'} → {β : Type v'} → {γ : Type u_1} → (L.withConstants γ).Term (α ⊕ β) ≃ L.Term ((γ ⊕ α) ⊕ β)
-- Mathlib.Topology.Separation.Hausdorff
Pi.t2Space : ∀ {X : Type u_1} {Y : X → Type v} [inst : (a : X) → TopologicalSpace (Y a)] [∀ (a : X), T2Space (Y a)],
  T2Space ((a : X) → Y a)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- Get the value of a `BVExpr.var` from an `Assignment`.
 -/
Std.Tactic.BVDecide.BVExpr.Assignment.get : Std.Tactic.BVDecide.BVExpr.Assignment → ℕ → Std.Tactic.BVDecide.BVExpr.PackedBitVec
-- Mathlib.ModelTheory.Syntax
/-- The equality of two terms as a first-order formula.  -/
FirstOrder.Language.Term.equal : {L : FirstOrder.Language} → {α : Type u'} → L.Term α → L.Term α → L.Formula α
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.mem_top : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {x : A}, x ∈ ⊤
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∉ t₂ → (t₁ ∩ t₂).getKey? k = none
-- Mathlib.AlgebraicGeometry.Normalization
/-- The sections of the relative normalization on the preimage of an affine open is isomorphic to
the integral closure.  -/
AlgebraicGeometry.Scheme.Hom.normalizationObjIso : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    [inst : AlgebraicGeometry.QuasiCompact f] →
      [inst_1 : AlgebraicGeometry.QuasiSeparated f] →
        {U : Y.Opens} →
          AlgebraicGeometry.IsAffineOpen U →
            ((AlgebraicGeometry.Scheme.Hom.normalization f).presheaf.obj
                (Opposite.op
                  ((TopologicalSpace.Opens.map (AlgebraicGeometry.Scheme.Hom.fromNormalization f).base).obj U)) ≅
              CommRingCat.of
                ↥(integralClosure ↑(Y.presheaf.obj (Opposite.op U))
                    ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U)))))
-- Batteries.Data.UInt
instLawfulOrdUInt16 : Std.LawfulOrd UInt16
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.bounds_bddBelow : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {f : E →SL[σ₁₂] F},
  BddBelow {c | 0 ≤ c ∧ ∀ (x : E), ‖f x‖ ≤ c * ‖x‖}
-- Std.Do.WP.SimpLemmas
Std.Do.WP.set_MonadStateOf : ∀ {m : Type u → Type v} {σ : Type u} {n : Type u → Type u_1} {x : σ} {ps : Std.Do.PostShape}
  {Q : Std.Do.PostCond PUnit.{u + 1} ps} [inst : MonadStateOf σ m] [inst_1 : MonadLift m n] [inst_2 : Std.Do.WP n ps],
  (Std.Do.wp (set x)).apply Q = (Std.Do.wp (MonadLift.monadLift (set x))).apply Q
-- Mathlib.Topology.Category.TopCommRingCat
TopCommRingCat.instConcreteCategorySubtypeRingHomαContinuousCoe : CategoryTheory.ConcreteCategory TopCommRingCat fun R S => { f // Continuous ⇑f }
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.continuous_arcsin : Continuous Real.arcsin
-- Mathlib.Analysis.Fourier.Notation
FourierModule.toFourierTransform : {R : Type u_5} →
  {E : Type u_6} →
    {F : outParam (Type u_7)} →
      [inst : Add E] →
        [inst_1 : Add F] → [inst_2 : SMul R E] → [inst_3 : SMul R F] → FourierModule R E F → FourierTransform E F
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Subalgebra.instUnique : {R : Type u} → [inst : CommSemiring R] → Unique (Subalgebra R R)
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Module.Flat.iff_flat_tensorProduct : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (S : Type u_1)
  [inst_3 : CommRing S] [inst_4 : Algebra R S] [Module.FaithfullyFlat R S],
  Module.Flat S (TensorProduct R S M) ↔ Module.Flat R M
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.max?.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (h_1 : Unit → motive RBTree.RBNode.nil)
  (h_2 : (c : RBTree.RBColor) → (l : RBTree.RBNode α) → (v : α) → motive (RBTree.RBNode.node c l v RBTree.RBNode.nil))
  (h_3 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.node c l v r)),
  (match RBTree.RBNode.nil with
    | RBTree.RBNode.nil => h_1 ()
    | RBTree.RBNode.node c l v RBTree.RBNode.nil => h_2 c l v
    | RBTree.RBNode.node c l v r => h_3 c l v r) =
    h_1 ()
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.length_eq_zero_iff : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, p.length = 0 ↔ p.Nil
-- Mathlib.CategoryTheory.Preadditive.LeftExact
/-- A functor between preadditive categories preserves the coequalizer of two
morphisms if it preserves all cokernels.  -/
CategoryTheory.Functor.preservesCoequalizer_of_preservesCokernels : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [F.PreservesZeroMorphisms] [CategoryTheory.Limits.HasBinaryBiproducts C]
  [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F] {X Y : C}
  (f g : X ⟶ Y), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) F
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.assoc_tmul : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (m : M) (n : N) (p : P), (TensorProduct.assoc R M N P) (m ⊗ₜ[R] n ⊗ₜ[R] p) = m ⊗ₜ[R] (n ⊗ₜ[R] p)
-- Mathlib.Combinatorics.Quiver.Path.Vertices
Quiver.Path.vertices_nil : ∀ {V : Type u_1} [inst : Quiver V] (a : V), Quiver.Path.nil.vertices = [a]
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.ofRat_sub : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (x y : β),
  CauSeq.Completion.ofRat (x - y) = CauSeq.Completion.ofRat x - CauSeq.Completion.ofRat y
-- Mathlib.RingTheory.FreeCommRing
FreeRing.coe_neg : ∀ {α : Type u} (x : FreeRing α), ↑(-x) = -↑x
-- Mathlib.Algebra.Divisibility.Hom
MulHom.map_dvd : ∀ {M : Type u_1} {N : Type u_2} [inst : Semigroup M] [inst_1 : Semigroup N] (f : M →ₙ* N) {a b : M}, a ∣ b → f a ∣ f b
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_iff_forall_isSome_getEntry? : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [ReflBEq α] {l : List ((a : α) × β a)},
  l.isEmpty = true ↔ ∀ (a : α), (Std.Internal.List.getEntry? a l).isSome = false
-- Init.Control.StateCps
StateCpsT.runK_modify : ∀ {σ : Type u} {m : Type u → Type v} {β : Type u} (f : σ → σ) (s : σ) (k : PUnit.{u + 1} → σ → m β),
  (modify f).runK s k = k PUnit.unit (f s)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Icc_mul_Icc : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : LinearOrder α] [IsOrderedMonoid α] [MulLeftReflectLE α]
  [ExistsMulOfLE α] {a b c d : α}, a ≤ b → c ≤ d → Set.Icc a b * Set.Icc c d = Set.Icc (a * c) (b * d)
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Localization.mulEquivOfQuotient.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N), Localization.mulEquivOfQuotient f = (Localization.monoidOf S).mulEquivOfLocalizations f
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
/-- If the topology of `X` is coinduced by a continuous function whose domain is
compactly generated, then so is `X`.  -/
compactlyGeneratedSpace_of_coinduced : ∀ {X : Type u} [tX : TopologicalSpace X] {Y : Type u} [tY : TopologicalSpace Y] [CompactlyGeneratedSpace X] {f : X → Y},
  Continuous f → tY = TopologicalSpace.coinduced f tX → CompactlyGeneratedSpace Y
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.Const.unitOfList_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {l : List α},
  Std.DHashMap.Raw.Const.unitOfList l =
    ↑↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.ihom.instIsLeftAdjointTensorLeft : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (A : C)
  [CategoryTheory.Closed A], (CategoryTheory.MonoidalCategory.tensorLeft A).IsLeftAdjoint
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
NNReal.ball_zero_eq_Ico' : ∀ (c : NNReal), Metric.ball 0 ↑c = Set.Ico 0 c
-- Mathlib.SetTheory.Ordinal.Veblen
/-- **Alias** of `Ordinal.lt_gamma_zero`.

---

`Γ₀` is the limit of `0`, `veblen 0 0`, `veblen (veblen 0 0) 0`, …  -/
Ordinal.lt_gamma0 : ∀ {o : Ordinal.{u}}, o < Ordinal.gamma 0 ↔ ∃ n, o < (fun a => Ordinal.veblen a 0)^[n] 0
-- Std.Time.Zoned.Database.Windows
/-- Retrieves the timezone rules, including all transitions, for a given timezone identifier.
 -/
Std.Time.Database.Windows.getZoneRules : String → IO Std.Time.TimeZone.ZoneRules
-- Aesop.Rule
Aesop.instInhabitedUnfoldRule.default : Aesop.UnfoldRule
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.mem_cycles₂_iff : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (x : G × G →₀ ↑A),
  x ∈ groupHomology.cycles₂ A ↔
    (x.sum fun g a => (fun₀ | g.2 => (A.ρ g.1⁻¹) a) + fun₀ | g.1 => a) = x.sum fun g a => fun₀ | g.1 * g.2 => a
-- Mathlib.MeasureTheory.Integral.MeanInequalities
ENNReal.funMulInvSnorm.eq_1 : ∀ {α : Type u_1} [inst : MeasurableSpace α] (f : α → ENNReal) (p : ℝ) (μ : MeasureTheory.Measure α) (a : α),
  ENNReal.funMulInvSnorm f p μ a = f a * ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p))⁻¹
-- Init.Prelude
Lean.TSyntax.mk : {ks : Lean.SyntaxNodeKinds} → Lean.Syntax → Lean.TSyntax ks
-- Mathlib.Algebra.Quaternion
Quaternion.self_add_star : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), a + star a = 2 * ↑a.re
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.neg_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F},
  P 2 ≠ 0 → W.neg P = P 2 • ![P 0 / P 2 ^ 2, W.toAffine.negY (P 0 / P 2 ^ 2) (P 1 / P 2 ^ 3), 1]
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.spanningCoe_le : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph), G'.spanningCoe ≤ G
-- Mathlib.NumberTheory.SmoothNumbers
/-- We establish the bijection from `ℕ × factoredNumbers s` to `factoredNumbers (s ∪ {p})`
given by `(e, n) ↦ p^e * n` when `p ∉ s` is a prime. See `Nat.factoredNumbers_insert` for
when `p` is not prime.  -/
Nat.equivProdNatFactoredNumbers : {s : Finset ℕ} → {p : ℕ} → Nat.Prime p → p ∉ s → ℕ × ↑(Nat.factoredNumbers s) ≃ ↑(Nat.factoredNumbers (insert p s))
-- Aesop.RuleTac.Basic
Aesop.CasesTarget.decl.inj : ∀ {decl decl_1 : Lean.Name}, Aesop.CasesTarget.decl decl = Aesop.CasesTarget.decl decl_1 → decl = decl_1
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_neg : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] {x : R},
  Int.fract x ≠ 0 → Int.fract (-x) = 1 - Int.fract x
-- Init.Core
Task.pure.inj : ∀ {α : Type u} {get get_1 : α}, { get := get } = { get := get_1 } → get = get_1
-- Mathlib.Tactic.Conv
/-- `conv_rhs => cs` runs the `conv` tactic sequence `cs` on the right hand side of the target.

In general, for an `n`-ary operator as the target, it traverses into the last argument.
It is a synonym for `conv => arg -1; cs`.

* `conv_rhs at h => cs` runs `cs` on the right hand side of hypothesis `h`.
* `conv_rhs in pat => cs` first looks for a subexpression matching `pat` (see the `pattern`
  conv tactic) and then traverses into the right hand side of this subexpression.
  This syntax also supports the `occs` clause for the pattern.
 -/
Mathlib.Tactic.Conv.convRHS : Lean.ParserDescr
-- Mathlib.GroupTheory.Perm.Fin
support_finRotate : ∀ {n : ℕ}, (finRotate (n + 2)).support = Finset.univ
-- Mathlib.Analysis.Complex.Norm
/-- The norm of a complex Cauchy sequence, as a real Cauchy sequence.  -/
Complex.cauSeqNorm : (CauSeq ℂ fun x => ‖x‖) → CauSeq ℝ abs
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
SSet.Subcomplex.Pairing.rank_lt : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} [inst : P.IsRegular] {x y : ↑P.II},
  P.AncestralRel x y → P.rank x < P.rank y
-- Mathlib.GroupTheory.Divisible
AddGroup.divisibleByNatOfDivisibleByInt.eq_1 : ∀ (A : Type u_1) [inst : AddGroup A] [inst_1 : DivisibleBy A ℤ],
  AddGroup.divisibleByNatOfDivisibleByInt A = { div := fun a n => DivisibleBy.div a ↑n, div_zero := ⋯, div_cancel := ⋯ }
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_norm_eq_lintegral_enorm : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {P : Type u_7} [inst : NormedAddCommGroup P]
  {f : α → P}, MeasureTheory.AEStronglyMeasurable f μ → ∫ (x : α), ‖f x‖ ∂μ = (∫⁻ (x : α), ‖f x‖ₑ ∂μ).toReal
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.piSplitLE_lt : ∀ {ι : Type u_6} {X : ι → Type u_8} {i : ι} [inst : PartialOrder ι] [inst_1 : DecidableEq ι]
  {f : InverseSystem.piLT X i × X i} {j : ι} (hj : j < i), InverseSystem.piSplitLE f ⟨j, ⋯⟩ = f.1 ⟨j, hj⟩
-- Mathlib.Topology.Connected.TotallyDisconnected
TotallySeparatedSpace.of_discrete : ∀ (α : Type u_3) [inst : TopologicalSpace α] [DiscreteTopology α], TotallySeparatedSpace α
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.maxEntry.congr_simp : ∀ {α : Type u} {β : Type v} (t t_1 : Std.DTreeMap.Internal.Impl α fun x => β) (e_t : t = t_1) (h : t.isEmpty = false),
  Std.DTreeMap.Internal.Impl.Const.maxEntry t h = Std.DTreeMap.Internal.Impl.Const.maxEntry t_1 ⋯
-- Mathlib.Order.CompleteBooleanAlgebra
iSup_symmDiff_le : ∀ {α : Type u} {ι : Sort w} [inst : CompleteBooleanAlgebra α] {f : ι → α} [Nonempty ι] {a : α},
  symmDiff (⨆ i, f i) a ≤ ⨆ i, symmDiff (f i) a
-- Mathlib.Data.List.Defs
/-- `andM xs` runs the actions in `xs`, returning true if all of them return
true. `andM` short-circuits, so if an action returns false, later actions are
not run.  -/
List.andM : {m : Type → Type v} → [Monad m] → List (m Bool) → m Bool
-- Init.Data.Rat.Lemmas
Rat.num_normalize : ∀ {num : ℤ} {den : ℕ} (den_nz : den ≠ 0), (Rat.normalize num den den_nz).num = num / ↑(num.natAbs.gcd den)
-- Init.Data.String.Lemmas.Splits
String.Pos.splits_prev_right : ∀ {s : String} (p : s.Pos) (hp : p ≠ s.startPos),
  p.Splits ((s.sliceTo (p.prev hp)).copy ++ String.singleton ((p.prev hp).get ⋯)) (s.sliceFrom p).copy
-- Std.Sat.AIG.If
Std.Sat.AIG.RefVec.ite : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} → (aig : Std.Sat.AIG α) → Std.Sat.AIG.RefVec.IfInput aig w → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.mul_mem_sup : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] {S T : NonUnitalStarSubalgebra R A} {x y : A}, x ∈ S → y ∈ T → x * y ∈ S ⊔ T
-- Mathlib.Data.Fin.Fin2
/-- The greatest value of `Fin2 (n+1)`.  -/
Fin2.last : {n : ℕ} → Fin2 (n + 1)
-- Mathlib.Algebra.Group.Defs
/-- A magma which `IsMulCommutative` is a `CommMagma`.

This is primarily used to deduce the bundled version from the unbundled one for commutative
subobjects in a noncommutative ambient type. As such this is only available inside the
`IsMulCommutative` scope so as to avoid deleterious effects to type class synthesis for bundled
commutativity.

See note [commutative subobjects].  -/
IsMulCommutative.instCommMagma : {M : Type u_2} → [inst : Mul M] → [IsMulCommutative M] → CommMagma M
-- Lean.PrettyPrinter.Delaborator.Attributes
/-- Marks a structure to be pretty printed using the anonymous constructor notation (`⟨a, b, c⟩`).  -/
Lean.ppUsingAnonymousConstructorAttr : Lean.TagAttribute
-- Mathlib.Probability.Process.Kolmogorov
ProbabilityTheory.IsAEKolmogorovProcess.p_pos : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω}
  [inst_1 : PseudoEMetricSpace E] {p q : ℝ} {M : NNReal} {P : MeasureTheory.Measure Ω} {X : T → Ω → E},
  ProbabilityTheory.IsAEKolmogorovProcess X P p q M → 0 < p
-- Std.Http.Data.Response
/-- Adds a single header to the response being built.
 -/
Std.Http.Response.Builder.header : Std.Http.Response.Builder → Std.Http.Header.Name → Std.Http.Header.Value → Std.Http.Response.Builder
-- Mathlib.Geometry.Manifold.Submersion
/-- The identity map is a submersion with complement `PUnit`.  -/
Manifold.IsSubmersionOfComplement.id : ∀ {𝕜 : Type u_1} {H : Type u_7} {E : Type u} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_11}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I n M],
  Manifold.IsSubmersionOfComplement PUnit.{u_15 + 1} I I n id
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.IsThreeCycle.sign : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α}, σ.IsThreeCycle → Equiv.Perm.sign σ = 1
-- Lean.Environment
Lean.OLeanEntries.mk.inj : ∀ {α : Type} {exported server «private» exported_1 server_1 private_1 : α},
  { exported := exported, server := server, «private» := «private» } =
      { exported := exported_1, server := server_1, «private» := private_1 } →
    exported = exported_1 ∧ server = server_1 ∧ «private» = private_1
-- Mathlib.LinearAlgebra.Dimension.Finrank
Module.one_lt_rank_of_one_lt_finrank : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  1 < Module.finrank R M → 1 < Module.rank R M
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
CategoryTheory.comp_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y Z : C}
  (f : X ⟶ Y) (g : Y ⟶ Z) (x : CategoryTheory.ToType X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.functor_map : ∀ {J K : Type u} [inst : LinearOrder J] [inst_1 : LinearOrder K] (f : J →o K)
  (i j : CategoryTheory.SimplicialThickening J),
  (CategoryTheory.SimplicialThickening.functor f).map i j =
    CategoryTheory.nerveMap (CategoryTheory.SimplicialThickening.functorMap f i j)
-- Mathlib.RingTheory.WittVector.Teichmuller
/-- The Teichmüller lift is set-theoretically right inverse to the constant coefficient map,
showing that the latter is surjective.  -/
WittVector.constantCoeff_surjective : ∀ (p : ℕ) {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R], Function.Surjective ⇑WittVector.constantCoeff
-- Mathlib.RingTheory.Ideal.Operations
Ideal.IsPrime.multiset_prod_map_le : ∀ {R : Type u} {ι : Type u_1} [inst : CommSemiring R] {s : Multiset ι} (f : ι → Ideal R) {P : Ideal R},
  P.IsPrime → ((Multiset.map f s).prod ≤ P ↔ ∃ i ∈ s, f i ≤ P)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKeyD_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β}
  {fallback : α},
  (t.insertIfNew k v).minKeyD fallback = t.minKey?.elim k fun k' => if cmp k k' = Ordering.lt then k else k'
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.ofValuation_apply : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀]
  (v : Valuation R (Multiplicative Γ₀ᵒᵈ)) (r : R),
  (AddValuation.ofValuation v) r = OrderDual.ofDual (Multiplicative.toAdd (v r))
-- Mathlib.RingTheory.MatrixAlgebra
kroneckerLinearEquiv_symm_kronecker : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {p : Type u_4} {R : Type u_5} [inst : CommSemiring R]
  [inst_1 : Fintype l] [inst_2 : Fintype m] [inst_3 : Fintype n] [inst_4 : Fintype p] [inst_5 : DecidableEq l]
  [inst_6 : DecidableEq m] [inst_7 : DecidableEq n] [inst_8 : DecidableEq p] (x : Matrix l m R) (y : Matrix n p R),
  (kroneckerLinearEquiv l m n p R).symm (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) x y) = x ⊗ₜ[R] y
-- Mathlib.Order.Hom.WithTopBot
WithBot.subtypeOrderIso_symm_apply : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] [inst_2 : DecidablePred fun x => x = ⊥] {a : α}
  (h : a ≠ ⊥), WithBot.subtypeOrderIso.symm a = ↑⟨a, h⟩
-- Mathlib.Order.Cover
WCovBy.of_image : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {a b : α} (f : α ↪o β), f a ⩿ f b → a ⩿ b
-- Mathlib.Probability.Kernel.Proper
/-- **Alias** of the forward direction of `ProbabilityTheory.Kernel.isProper_iff_restrict_eq_indicator_smul`. -/
ProbabilityTheory.Kernel.IsProper.restrict_eq_indicator_smul : ∀ {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : ProbabilityTheory.Kernel X X} (h𝓑𝓧 : 𝓑 ≤ 𝓧),
  π.IsProper → ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), (π.restrict ⋯) x = B.indicator (fun x => 1) x • π x
-- Mathlib.Order.Hom.CompleteLattice
/-- The proposition that a `sSupHom` commutes with arbitrary suprema/joins.  -/
CompleteLatticeHom.map_sSup' : ∀ {α : Type u_8} {β : Type u_9} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (self : CompleteLatticeHom α β)
  (s : Set α), self.toFun (sSup s) = sSup (self.toFun '' s)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.injective : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂), Function.Injective ⇑e
-- Init.Data.SInt.Basic
/-- Bitwise or for 8-bit signed integers. Usually accessed via the `|||` operator.

Each bit of the resulting integer is set if at least one of the corresponding bits of the input
integers is set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.
 -/
Int8.lor : Int8 → Int8 → Int8
-- Mathlib.Algebra.Lie.Nilpotent
LieSubmodule.isNilpotent_iff_exists_lcs_eq_bot : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [LieModule R L M]
  (N : LieSubmodule R L M), LieModule.IsNilpotent L ↥N ↔ ∃ k, LieSubmodule.lcs k N = ⊥