mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.WithDensity
ProbabilityTheory.Kernel.withDensity_zero : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β)
  [inst : ProbabilityTheory.IsSFiniteKernel κ], κ.withDensity 0 = 0
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.instEpiLeftHomologyπ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology], CategoryTheory.Epi S.leftHomologyπ
-- Mathlib.CategoryTheory.Sites.Whiskering
CategoryTheory.GrothendieckTopology.Cover.multicospanComp_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {B : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} B] {J : CategoryTheory.GrothendieckTopology C}
  (F : CategoryTheory.Functor A B) (P : CategoryTheory.Functor Cᵒᵖ A) {X : C} (S : J.Cover X)
  (X_1 : CategoryTheory.Limits.WalkingMulticospan S.shape),
  (CategoryTheory.GrothendieckTopology.Cover.multicospanComp F P S).hom.app X_1 =
    (match X_1 with
      | CategoryTheory.Limits.WalkingMulticospan.left a => CategoryTheory.Iso.refl (F.obj (P.obj (Opposite.op a.Y)))
      | CategoryTheory.Limits.WalkingMulticospan.right a =>
        CategoryTheory.Iso.refl (F.obj (P.obj (Opposite.op a.r.Z)))).hom
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.K'.elim.eq_1 : ∀ (a b c d : List Turing.PartrecToTM2.Γ'), Turing.PartrecToTM2.K'.elim a b c d Turing.PartrecToTM2.K'.main = a
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcConnectParams.mk.sizeOf_spec : ∀ (uri : Lean.Lsp.DocumentUri), sizeOf { uri := uri } = 1 + sizeOf uri
-- Mathlib.Topology.Separation.GDelta
/-- A T₆ space is a perfectly normal T₀ space.  -/
T6Space : (X : Type u) → [TopologicalSpace X] → Prop
-- Mathlib.Topology.Algebra.Order.Floor
continuousOn_floor : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] [inst_3 : TopologicalSpace α] (n : ℤ),
  ContinuousOn (fun x => ↑⌊x⌋) (Set.Ico (↑n) (↑n + 1))
-- Mathlib.Algebra.GroupWithZero.Defs
MonoidWithZero.toZero : {M₀ : Type u} → [self : MonoidWithZero M₀] → Zero M₀
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.mem_ofLe : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  {K K' : LieSubalgebra R L} (h : K ≤ K') (x : ↥K'), x ∈ LieSubalgebra.ofLe h ↔ ↑x ∈ K
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_emptyc : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {a : α}, ∅[a]? = none
-- Lean.Data.Lsp.Capabilities
/-- Whether the client in general supports change annotations on text edits.  -/
Lean.Lsp.WorkspaceEditClientCapabilities.changeAnnotationSupport? : Lean.Lsp.WorkspaceEditClientCapabilities → Option Lean.Lsp.ChangeAnnotationSupport
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ {X : C} (f : X ⟶ (CategoryTheory.shiftFunctor C 1).obj T.obj₁),
      CategoryTheory.CategoryStruct.comp f ((CategoryTheory.shiftFunctor C 1).map T.mor₁) = 0 →
        ∃ g, f = CategoryTheory.CategoryStruct.comp g T.mor₃
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonTextDocumentEdit : Lean.FromJson Lean.Lsp.TextDocumentEdit
-- Mathlib.Algebra.Group.Defs
IsCyclic.mk : ∀ {G : Type u} [inst : Pow G ℤ], (∃ g, Function.Surjective fun x => g ^ x) → IsCyclic G
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.ccSc_X₃ : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' : κ) (i₀ i₁ i₂ i₃ i₃' : ι) (hi₀ : i₀ = data.i₀ r pq' ⋯)
  (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯) (hi₃' : i₃' = data.i₃ r' pq' ⋯)
  (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq')
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.ccSc._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.ccSc._auto_3),
  (CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.ccSc X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃ i₃'
        hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' hn₁ hn₂).X₃ =
    X.E (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯
-- Mathlib.Topology.Path
Path.ofLine_extend : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (γ : Path x y), Path.ofLine ⋯ ⋯ ⋯ = γ
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- Orbit-stabilizer theorem.  -/
AddAction.orbitEquivQuotientStabilizer : (G : Type u) →
  {X : Type v} →
    [inst : AddGroup G] → [inst_1 : AddAction G X] → (b : X) → ↑(AddAction.orbit G b) ≃ G ⧸ AddAction.stabilizer G b
-- Lean.Meta.LitValues
/-- Return `some b` if `e` is the boolean literal `true` or `false`.  -/
_private.Lean.Meta.LitValues.0.Lean.Meta.getBoolLit? : Lean.Expr → Option Bool
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Simprocs.mk.injEq : ∀ (pre post : Lean.Meta.Simp.SimprocTree) (simprocNames erased : Lean.PHashSet Lean.Name)
  (pre_1 post_1 : Lean.Meta.Simp.SimprocTree) (simprocNames_1 erased_1 : Lean.PHashSet Lean.Name),
  ({ pre := pre, post := post, simprocNames := simprocNames, erased := erased } =
      { pre := pre_1, post := post_1, simprocNames := simprocNames_1, erased := erased_1 }) =
    (pre = pre_1 ∧ post = post_1 ∧ simprocNames = simprocNames_1 ∧ erased = erased_1)
-- Mathlib.Data.Nat.Log
Nat.clog_le_of_le_pow : ∀ {b x y : ℕ}, x ≤ b ^ y → Nat.clog b x ≤ y
-- Mathlib.Data.Multiset.Bind
Multiset.map_bind : ∀ {α : Type u_1} {β : Type v} {γ : Type u_2} (m : Multiset α) (n : α → Multiset β) (f : β → γ),
  Multiset.map f (m.bind n) = m.bind fun a => Multiset.map f (n a)
-- Lean.Level
Lean.Level.instantiateParams : Lean.Level → List Lean.Name → List Lean.Level → Lean.Level
-- Init.Data.List.Nat.Sum
List.mul_length_le_sum_of_min?_eq_some_nat : ∀ {x : ℕ} {xs : List ℕ}, xs.min? = some x → x * xs.length ≤ xs.sum
-- Mathlib.Geometry.Manifold.ContMDiffMFDeriv
/-- The function that sends `x` to the `y`-derivative of `f (x, y)` at `g (x)` is `C^m` at `x₀`,
where the derivative is taken as a continuous linear map.
We have to assume that `f` is `C^n` at `(x₀, g(x₀))` for `n ≥ m + 1` and `g` is `C^m` at `x₀`.
We have to insert a coordinate change from `x₀` to `x` to make the derivative sensible.
This result is used to show that maps into the 1-jet bundle and cotangent bundle are `C^n`.
`ContMDiffAt.mfderiv_const` is a special case of this.
 -/
ContMDiffAt.mfderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {m n : WithTop ℕ∞} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  [Js : IsManifold J 1 N] [Is : IsManifold I 1 M] [I's : IsManifold I' 1 M'] {x₀ : N} (f : N → M → M') (g : N → M),
  ContMDiffAt (J.prod I) I' n (Function.uncurry f) (x₀, g x₀) →
    ContMDiffAt J I m g x₀ →
      m + 1 ≤ n →
        ContMDiffAt J (modelWithCornersSelf 𝕜 (E →L[𝕜] E')) m
          (inTangentCoordinates I I' g (fun x => f x (g x)) (fun x => mfderiv% (f x) (g x)) x₀) x₀
-- Init.Data.Array.DecidableEq
_private.Init.Data.Array.DecidableEq.0.Array.isEqvAux.eq_2 : ∀ {α : Type u} (xs ys : Array α) (hsz : xs.size = ys.size) (p : α → α → Bool) (i : ℕ) (h : i + 1 ≤ xs.size),
  xs.isEqvAux ys hsz p i.succ h = (p xs[i] ys[i] && xs.isEqvAux ys hsz p i ⋯)
-- Mathlib.RepresentationTheory.Coinduced
Rep.instPreservesProjectiveObjectsSubtypeMemSubgroupResFunctorSubtype : ∀ {k : Type u} [inst : CommRing k] {G : Type w} [inst_1 : Group G] (S : Subgroup G),
  (Rep.resFunctor S.subtype).PreservesProjectiveObjects
-- Init.Data.Array.Monadic
Array.filterMapM_wfParam : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Array α}
  {f : α → m (Option β)}, Array.filterMapM f (wfParam xs) = Array.filterMapM f xs.attach.unattach
-- Aesop.Search.Expansion
Aesop.RuleResult.succeeded.injEq : ∀ (newRapps newRapps_1 : Array Aesop.RappRef),
  (Aesop.RuleResult.succeeded newRapps = Aesop.RuleResult.succeeded newRapps_1) = (newRapps = newRapps_1)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.symm_mapDomainAddEquiv : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Mul M] [inst_2 : Mul N] (e : M ≃ N),
  (MonoidAlgebra.mapDomainAddEquiv R e).symm = MonoidAlgebra.mapDomainAddEquiv R e.symm
-- Mathlib.GroupTheory.OrderOfElement
/-- **Alias** of the reverse direction of `isOfFinAddOrder_neg_iff`.

---

Inverses of elements of finite additive order
have finite additive order.  -/
IsOfFinAddOrder.neg : ∀ {G : Type u_1} [inst : AddGroup G] {x : G}, IsOfFinAddOrder x → IsOfFinAddOrder (-x)
-- Init.Data.List.MinMax
List.max_eq_head : ∀ {α : Type u} [inst : Max α] {l : List α} (hl : l ≠ []), List.Pairwise (fun a b => a ⊔ b = a) l → l.max hl = l.head hl
-- Init.Data.Vector.Basic
/-- Swap two elements of a vector using `Fin` indices.

This will perform the update destructively provided that the vector has a reference count of 1.
 -/
Vector.swap : {α : Type u_1} →
  {n : ℕ} →
    Vector α n → (i j : ℕ) → autoParam (i < n) Vector.swap._auto_1 → autoParam (j < n) Vector.swap._auto_3 → Vector α n
-- Mathlib.Analysis.Calculus.FDeriv.Prod
differentiable_fst : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F],
  Differentiable 𝕜 Prod.fst
-- Mathlib.NumberTheory.FactorisationProperties
/-- `n : ℕ` is _abundant_ if the sum of the proper divisors of `n` is greater than `n`.  -/
Nat.Abundant : ℕ → Prop
-- Mathlib.NumberTheory.ModularForms.LFunction
ModularForm.L.eq_1 : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1}
  [inst_1 : FunLike F UpperHalfPlane ℂ] (f : F) [inst_2 : ModularFormClass F Γ k] (s : ℂ),
  ModularForm.L hk f s = ModularForm.Λ hk f s * (2 / s.Gammaℂ)
-- Mathlib.LinearAlgebra.Matrix.IsDiag
Matrix.isDiag_transpose_iff : ∀ {α : Type u_1} {n : Type u_4} [inst : Zero α] {A : Matrix n n α}, A.transpose.IsDiag ↔ A.IsDiag
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic.0.tacticMap_simp : Lean.ParserDescr
-- Init.GrindInstances.ToInt
Lean.Grind.instDivUSizeUintNumBits : Lean.Grind.ToInt.Div USize (Lean.Grind.IntInterval.uint System.Platform.numBits)
-- Mathlib.Topology.Connected.PathConnected
/-- Use path-connectedness to build a path between two points.  -/
PathConnectedSpace.somePath : {X : Type u_1} → [inst : TopologicalSpace X] → [PathConnectedSpace X] → (x y : X) → Path x y
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- If `M` and `N` are linearly disjoint, if `N` is flat, then for any family of
`R`-linearly independent elements `{ m_i }` of `M`, and any family of
`R`-linearly independent elements `{ n_j }` of `N`, the family `{ m_i * n_j }` in `S` is
also `R`-linearly independent.  -/
Submodule.LinearDisjoint.linearIndependent_mul_of_flat_right : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {M N : Submodule R S},
  M.LinearDisjoint N →
    ∀ [Module.Flat R ↥N] {κ : Type u_1} {ι : Type u_2} {m : κ → ↥M} {n : ι → ↥N},
      LinearIndependent R m → LinearIndependent R n → LinearIndependent R fun i => ↑(m i.1) * ↑(n i.2)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
/-- The type (I) simplex reconstructed from a type (II) simplex.  -/
SSet.prodStdSimplex.pairingCore.IsType₂.type₁ : {m : ℕ} →
  {k : Fin (m + 1)} →
    {n : ℕ} →
      {x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N} →
        SSet.prodStdSimplex.pairingCore.IsType₂ x → {d : ℕ} → x.dim = d → SSet.prodStdSimplex.pairingCore.Type₁ k n
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.toAddCommGroup.eq_1 : ∀ {G : Type u_3} [inst : AddCommGroup G] (H : AddSubgroup G), H.toAddCommGroup = AddSubgroupClass.toAddCommGroup H
-- Mathlib.RingTheory.Jacobson.Ring
/-- If `R` is a Jacobson ring, then maximal ideals in the localization at `y`
correspond to maximal ideals in the original ring `R` that don't contain `y`  -/
IsLocalization.orderIsoOfMaximal : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        (y : R) →
          [inst_2 : Algebra R S] →
            [IsLocalization.Away y S] → [IsJacobsonRing R] → { p // p.IsMaximal } ≃o { p // p.IsMaximal ∧ y ∉ p }
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeTR_go_eq : ∀ {α : Type u_1} {le : α → α → Bool} {l₁ l₂ acc : List α},
  List.MergeSort.Internal.mergeTR.go✝ le l₁ l₂ acc = acc.reverse ++ l₁.merge l₂ le
-- Mathlib.Order.Interval.Finset.Defs
OrderIso.locallyFiniteOrderBot.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrderBot β]
  (f : α ≃o β),
  f.locallyFiniteOrderBot =
    { finsetIio := fun a => Finset.map { toEquiv := f.symm.toEquiv, map_rel_iff' := ⋯ }.toEmbedding (Finset.Iio (f a)),
      finsetIic := fun a => Finset.map { toEquiv := f.symm.toEquiv, map_rel_iff' := ⋯ }.toEmbedding (Finset.Iic (f a)),
      finset_mem_Iic := ⋯, finset_mem_Iio := ⋯ }
-- Mathlib.Data.Seq.Defs
/-- The length of a terminating sequence.  -/
Stream'.Seq.length : {α : Type u} → (s : Stream'.Seq α) → s.Terminates → ℕ
-- Mathlib.Data.Nat.Init
Nat.strong_induction_on : ∀ {p : ℕ → Prop} (n : ℕ), (∀ (n : ℕ), (∀ m < n, p m) → p n) → p n
-- Init.Data.List.Range
List.range'.eq_2 : ∀ (x x_1 n : ℕ), List.range' x n.succ x_1 = x :: List.range' (x + x_1) n x_1
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.encodeCode.eq_2 : Nat.Partrec.Code.succ.encodeCode = 1
-- Mathlib.Computability.TuringMachine.StackTuringMachine
/-- Given a set `S` of states, `SupportsStmt S q` means that `q` only jumps to states in `S`.  -/
Turing.TM2.SupportsStmt : {K : Type u_1} → {Γ : K → Type u_2} → {Λ : Type u_3} → {σ : Type u_4} → Finset Λ → Turing.TM2.Stmt Γ Λ σ → Prop
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
/-- The constant factor occurring in the conclusion of `eLpNorm_le_eLpNorm_fderiv_one`.
It only depends on `E`, `μ` and `p`.  -/
MeasureTheory.eLpNormLESNormFDerivOneConst : {E : Type u_5} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      [inst_2 : MeasurableSpace E] →
        [BorelSpace E] → [FiniteDimensional ℝ E] → (μ : MeasureTheory.Measure E) → [μ.IsAddHaarMeasure] → ℝ → NNReal
-- Mathlib.Algebra.Group.Hom.Defs
MulHom.comp_apply : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (g : N →ₙ* P)
  (f : M →ₙ* N) (x : M), (g.comp f) x = g (f x)
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
HomotopicalAlgebra.bifibrantObjects_le_fibrantObject : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_4 : CategoryTheory.Limits.HasTerminal C],
  HomotopicalAlgebra.bifibrantObjects C ≤ HomotopicalAlgebra.fibrantObjects C
-- Mathlib.Tactic.ModCases
/-- The successor case decomposes `∃ z, b ≤ z < n ∧ a ≡ z (mod n)` into
`a ≡ b (mod n) ∨ ∃ z, b+1 ≤ z < n ∧ a ≡ z (mod n)`,
and the `a ≡ b (mod n) → p` case becomes a subgoal.
 -/
Mathlib.Tactic.ModCases.IntMod.onModCases_succ : {p : Sort u_1} →
  {n : ℕ} →
    {a : ℤ} →
      (b : ℕ) →
        (a ≡ OfNat.ofNat b [ZMOD OfNat.ofNat n] → p) →
          Mathlib.Tactic.ModCases.IntMod.OnModCases n a (b.add 1) p → Mathlib.Tactic.ModCases.IntMod.OnModCases n a b p
-- Lean.Parser.Command
/-- No-op parser used as syntax kind for attaching remaining whitespace at the end of the input.  -/
Lean.Parser.Command.eoi : Lean.Parser.Parser
-- ProofWidgets.Data.Html
/-- An `element "tag" attrs children` represents `<tag {...attrs}>{...children}</tag>`.  -/
ProofWidgets.Html.element : String → Array (String × Lean.Json) → Array ProofWidgets.Html → ProofWidgets.Html
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_lt_zpow_right₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀]
  {m n : ℤ}, 1 < a → m < n → a ^ m < a ^ n
-- Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
ModuleCat.projectiveDimension_eq_of_semiLinearEquiv : ∀ {R : Type u} [inst : Ring R] [Small.{v, u} R] {R' : Type u'} [inst_2 : Ring R'] [Small.{v', u'} R'] (e : R ≃+* R')
  {M : ModuleCat R} {N : ModuleCat R'} (e' : ↑M ≃ₛₗ[↑e] ↑N),
  CategoryTheory.projectiveDimension M = CategoryTheory.projectiveDimension N
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Split.nondegComplexFunctor_map_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.SimplicialObject.Split C} (Φ : S₁ ⟶ S₂) (n : ℕ),
  (CategoryTheory.SimplicialObject.Split.nondegComplexFunctor.map Φ).f n = Φ.f n
-- Mathlib.CategoryTheory.Limits.Cones
/-- The opposite cocone of the image of a cone is the image of the opposite cocone.  -/
CategoryTheory.Functor.mapConeOp : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            {F : CategoryTheory.Functor J C} →
              (G : CategoryTheory.Functor C D) →
                (t : CategoryTheory.Limits.Cone F) → (G.mapCone t).op ≅ G.op.mapCocone t.op
-- Mathlib.Topology.Order
isClosed_induced_iff : ∀ {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] {s : Set α} {f : α → β},
  IsClosed s ↔ ∃ t_1, IsClosed t_1 ∧ f ⁻¹' t_1 = s
-- Mathlib.CategoryTheory.Limits.Shapes.KernelPair
/-- The data expressing that `(a, b)` is a kernel pair is subsingleton.  -/
CategoryTheory.IsKernelPair.instSubsingleton : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R X Y : C} (f : X ⟶ Y) (a b : R ⟶ X),
  Subsingleton (CategoryTheory.IsKernelPair f a b)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.instIsTransLe : IsTrans ZFSet.{u_1} fun x1 x2 => x1 ⊆ x2
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonWorkspaceSymbolParams : Lean.FromJson Lean.Lsp.WorkspaceSymbolParams
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.simprocDeclExt : Lean.PersistentEnvExtension Lean.Meta.Simp.SimprocDecl Lean.Meta.Simp.SimprocDecl Lean.Meta.Simp.SimprocDeclExtState
-- Mathlib.Data.Set.SMulAntidiagonal
Set.smulAntidiagonal_mono_right : ∀ {G : Type u_1} {P : Type u_2} [inst : SMul G P] {s : Set G} {t₁ t₂ : Set P} {a : P},
  t₁ ⊆ t₂ → s.smulAntidiagonal t₁ a ⊆ s.smulAntidiagonal t₂ a
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.shape : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (self : HomologicalComplex V c) (i j : ι),
  ¬c.Rel i j → self.d i j = 0
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.support_weights_eq_singleton : ∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] {M : Type u_9} {w : Convexity.StdSimplex R M} {x : M}
  [inst_2 : IsStrictOrderedRing R], w.weights.support = {x} ↔ w = Convexity.StdSimplex.single x
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalAddSubgroup.toOpenAddSubgroup : {G : Type u} → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → OpenNormalAddSubgroup G → OpenAddSubgroup G
-- Mathlib.Data.Fintype.Quotient
Equiv.subtypeQuotientEquivQuotientSubtype.eq_1 : ∀ {α : Sort u_1} (p₁ : α → Prop) {s₁ : Setoid α} {s₂ : Setoid (Subtype p₁)} (p₂ : Quotient s₁ → Prop)
  (hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧) (h : ∀ (x y : Subtype p₁), s₂ x y ↔ s₁ ↑x ↑y),
  Equiv.subtypeQuotientEquivQuotientSubtype p₁ p₂ hp₂ h =
    { toFun := fun a => Quotient.hrecOn (motive := fun x => p₂ x → Quotient s₂) (↑a) (fun a h => ⟦⟨a, ⋯⟩⟧) ⋯ ⋯,
      invFun := fun a => a.liftOn (fun a => ⟨⟦↑a⟧, ⋯⟩) ⋯, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- If `b` is a binary bicone such that `b.snd` is a cokernel of `b.inl`, then `b` is a bilimit
bicone.  -/
CategoryTheory.Limits.BinaryBicone.isBilimitOfCokernelSnd : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} →
        (b : CategoryTheory.Limits.BinaryBicone X Y) → CategoryTheory.Limits.IsColimit b.inlCokernelCofork → b.IsBilimit
-- Mathlib.Topology.Connected.Basic
isPreconnected_iff_preconnectedSpace : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α}, IsPreconnected s ↔ PreconnectedSpace ↑s
-- Mathlib.NumberTheory.Real.GoldenRatio
/-- Relationship between the Fibonacci Sequence, the conjugate of the golden ratio,
and its exponents.  -/
Real.goldenConj_mul_fib_succ_add_fib : ∀ (n : ℕ), Real.goldenConj * ↑(Nat.fib (n + 1)) + ↑(Nat.fib n) = Real.goldenConj ^ (n + 1)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.applyCell_eq_apply_toListModel : ∀ {α : Type u} {β : α → Type v} {δ : Type w} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : BEq α]
  [inst_3 : Std.LawfulBEqOrd α] {k : α} {l : Std.DTreeMap.Internal.Impl α β},
  l.Ordered →
    ∀
      {f :
        (c : Std.DTreeMap.Internal.Cell α β (compare k)) →
          (Std.DTreeMap.Internal.Impl.contains' (compare k) l = true → c.contains = true) → δ}
      (g :
        (ll : List ((a : α) × β a)) →
          (Std.DTreeMap.Internal.Impl.contains' (compare k) l = true → Std.Internal.List.containsKey k ll = true) → δ),
      (∀ (c : Std.DTreeMap.Internal.Cell α β (compare k))
          (hc : Std.DTreeMap.Internal.Impl.contains' (compare k) l = true → c.contains = true),
          f c hc = g c.inner.toList ⋯) →
        (∀ (l₁ l₂ : List ((a : α) × β a))
            (h : Std.DTreeMap.Internal.Impl.contains' (compare k) l = true → Std.Internal.List.containsKey k l₁ = true),
            Std.Internal.List.DistinctKeys l₁ → ∀ (hP : l₁.Perm l₂), g l₁ h = g l₂ ⋯) →
          (∀ (l₁ l₂ : List ((a : α) × β a))
              (h :
                Std.DTreeMap.Internal.Impl.contains' (compare k) l = true →
                  Std.Internal.List.containsKey k (l₁ ++ l₂) = true)
              (h' : Std.Internal.List.containsKey k l₂ = false), g (l₁ ++ l₂) h = g l₁ ⋯) →
            Std.DTreeMap.Internal.Impl.applyCell k l f = g l.toListModel ⋯
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_max : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {he : t ≠ ∅},
  t.get? (t.max he) = some (t.max he)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt8.reduceLT : Lean.Meta.Simp.Simproc