mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.LRAT.Parser
Std.Tactic.BVDecide.LRAT.Parser.Binary.manyTillNegOrZero : {α : Type} → Std.Internal.Parsec.ByteArray.Parser α → Std.Internal.Parsec.ByteArray.Parser (Array α)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeLeftOpOfConeEquiv_functor_map_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J Cᵒᵖ} {X Y : (CategoryTheory.Limits.Cone F)ᵒᵖ} (f : X ⟶ Y),
  (CategoryTheory.Limits.coconeLeftOpOfConeEquiv.functor.map f).hom = f.unop.hom.unop
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.ShiftSequence.leftComp_sequence : ∀ {C : Type u_1} {D : Type u_2} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} A]
  {F : CategoryTheory.Functor C A} {π : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D A} (e : π.comp H ≅ F)
  (M : Type u_4) [inst_3 : AddMonoid M] [inst_4 : CategoryTheory.HasShift C M] [inst_5 : CategoryTheory.HasShift D M]
  [inst_6 : π.CommShift M] [inst_7 : H.ShiftSequence M] (n : M),
  CategoryTheory.Functor.ShiftSequence.sequence F n = π.comp (H.shift n)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instIsTopologicalAddGroup : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F], IsTopologicalAddGroup (SchwartzMap E F)
-- Mathlib.Probability.Decision.Risk.Defs
ProbabilityTheory.minimaxRisk_zero : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} [Nonempty 𝓨] (ℓ : Θ → 𝓨 → ENNReal), ProbabilityTheory.minimaxRisk ℓ 0 = 0
-- Mathlib.Control.ULiftable
/-- for specific reader monads, this function helps to create a uliftable instance  -/
ReaderT.uliftable' : {s : Type u₀} →
  {s' : Type u₁} →
    {m : Type u₀ → Type u_5} →
      {m' : Type u₁ → Type u_6} → [ULiftable m m'] → s ≃ s' → ULiftable (ReaderT s m) (ReaderT s' m')
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.ofList_cons : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {k : α} {v : β k} {tl : List ((a : α) × β a)},
  Std.DTreeMap.ofList (⟨k, v⟩ :: tl) cmp = (∅.insert k v).insertMany tl
-- Mathlib.Algebra.Group.Subgroup.Finite
Subgroup.instFintypeSubtypeMemOfDecidablePred : {G : Type u_1} → [inst : Group G] → (K : Subgroup G) → [DecidablePred fun x => x ∈ K] → [Fintype G] → Fintype ↥K
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.deleteVerts_inter_verts_set_right_eq : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {s : Set V}, G'.deleteVerts (s ∩ G'.verts) = G'.deleteVerts s
-- Mathlib.Tactic.Linter.UnusedInstancesInType
/-- Whether the parameter appears in a proof in the type.  -/
_private.Mathlib.Tactic.Linter.UnusedInstancesInType.0.Mathlib.Linter.UnusedInstancesInType.Parameter.appearsInTypeProof : Mathlib.Linter.UnusedInstancesInType.Parameter✝ → Bool
-- Mathlib.Order.UpperLower.Basic
IsLowerSet.not_bddBelow : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} [NoMinOrder α], IsLowerSet s → s.Nonempty → ¬BddBelow s
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.Hom.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {F : CategoryTheory.Functor C C}
  {V₀ V₁ : CategoryTheory.Endofunctor.Coalgebra F} {x y : V₀.Hom V₁}, x = y ↔ x.f = y.f
-- Lean.Environment
/-- Type check given declaration and add it to the environment  -/
Lean.Kernel.Environment.addDeclCore : Lean.Kernel.Environment →
  USize → USize → Lean.Declaration → Option IO.CancelToken → Except Lean.Kernel.Exception Lean.Kernel.Environment
-- Mathlib.Order.Height
Set.exists_eq_chainHeight_of_chainHeight_ne_top : ∀ {α : Type u_1} (s : Set α) (r : α → α → Prop), s.chainHeight r ≠ ⊤ → ∃ t ⊆ s, t.encard = s.chainHeight r ∧ IsChain r t
-- Mathlib.Analysis.Calculus.FDeriv.Add
differentiableAt_const_add_iff : ∀ {𝕜 : 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] {f : E → F}
  {x : E} (c : F), DifferentiableAt 𝕜 (fun y => c + f y) x ↔ DifferentiableAt 𝕜 f x
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.mconv_withDensity_eq_mlconvolution : ∀ {G : Type u_3} [inst : Group G] {mG : MeasurableSpace G} [MeasurableMul₂ G] [MeasurableInv G]
  {μ : MeasureTheory.Measure G} [MeasureTheory.SFinite μ] [μ.IsMulLeftInvariant] {f g : G → ENNReal},
  Measurable f →
    Measurable g → (μ.withDensity f).mconv (μ.withDensity g) = μ.withDensity (MeasureTheory.mlconvolution f g μ)
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
tendstoLocallyUniformlyOn_iUnion : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {p : Filter ι} {ι' : Sort u_5} {S : ι' → Set α},
  (∀ (i : ι'), IsOpen (S i)) →
    (∀ (i : ι'), TendstoLocallyUniformlyOn F f p (S i)) → TendstoLocallyUniformlyOn F f p (⋃ i, S i)
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.optionEquivLeft.eq_1 : ∀ (R : Type u) (S₁ : Type v) [inst : CommSemiring R],
  MvPolynomial.optionEquivLeft R S₁ =
    AlgEquiv.ofAlgHom (MvPolynomial.aeval fun o => o.elim Polynomial.X fun s => Polynomial.C (MvPolynomial.X s))
      (Polynomial.aevalTower (MvPolynomial.rename some) (MvPolynomial.X none)) ⋯ ⋯
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.add_zero : ∀ {R : Type u_1} [inst : CommRing R] {σ : Type u_3} (F : FormalGroup R) {f : MvPowerSeries σ R},
  PowerSeries.HasSubst f → MvPowerSeries.subst ![f, 0] F.toPowerSeries = f
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- Following `Trie`s based on the `Key`.  -/
Lean.Meta.RefinedDiscrTree.Trie.children : {α : Type} →
  Lean.Meta.RefinedDiscrTree.Trie α → Std.HashMap Lean.Meta.RefinedDiscrTree.Key Lean.Meta.RefinedDiscrTree.TrieIndex
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
HasDerivWithinAt.cosh : ∀ {f : ℝ → ℝ} {f' x : ℝ} {s : Set ℝ},
  HasDerivWithinAt f f' s x → HasDerivWithinAt (fun x => Real.cosh (f x)) (Real.sinh (f x) * f') s x
-- Lean.Meta.Structure
_private.Lean.Meta.Structure.0.Lean.Meta.instantiateStructDefaultValueFn?.go? : {m : Type → Type} →
  [Monad m] →
    [MonadLiftT Lean.MetaM m] →
      (Lean.Name → m (Option Lean.Expr)) → Lean.NameSet → Lean.Expr → m (Option (Lean.NameSet × Lean.Expr))
-- Mathlib.Analysis.Calculus.Deriv.Add
hasDerivAt_neg : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜), HasDerivAt Neg.neg (-1) x
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.smul_apply : ∀ {M : Type u_1} {β : Type u_2} {α : Type u_3} [inst : SMul M α] (c : Mᵈᵐᵃ) (f : α → β) (a : α),
  (c • f) a = f (DomMulAct.mk.symm c • a)
-- Mathlib.Analysis.Calculus.Gradient.Basic
HasGradientAt.fderiv_apply : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x y : F}, HasGradientAt f f' x → (fderiv 𝕜 f x) y = inner 𝕜 f' y
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.coe_zero : ∀ (A : Type u_2) (B : Type u_3) [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B], ⇑0 = 0
-- Aesop.Index.Basic
Aesop.IndexingMode.hyps.sizeOf_spec : ∀ (keys : Array Lean.Meta.DiscrTree.Key), sizeOf (Aesop.IndexingMode.hyps keys) = 1 + sizeOf keys
-- Init.Data.Slice.Array.Lemmas
Array.toArray_mkSlice_ric : ∀ {α : Type u_1} {xs : Array α} {hi : ℕ},
  Std.Slice.toArray (Std.Ric.Sliceable.mkSlice xs *...=hi) = xs.extract 0 (hi + 1)
-- Mathlib.Topology.UniformSpace.Equiv
/-- See Note [custom simps projection]  -/
UniformEquiv.Simps.symm_apply : {α : Type u} → {β : Type u_1} → [inst : UniformSpace α] → [inst_1 : UniformSpace β] → α ≃ᵤ β → β → α
-- Init.Data.List.Monadic
List.zipWithM'.eq_1 : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type x} {γ : Type u} (f : α → β → m γ) (x_2 : α)
  (xs : List α) (y : β) (ys : List β),
  List.zipWithM' f (x_2 :: xs) (y :: ys) = do
    let z ← f x_2 y
    let zs ← List.zipWithM' f xs ys
    pure (z :: zs)
-- Mathlib.Analysis.InnerProductSpace.PiL2
FiniteDimensional.orthonormalBasisSingleton.eq_1 : ∀ (ι : Type u_1) (𝕜 : Type u_3) [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : Unique ι] (h : Module.finrank 𝕜 E = 1) (v : E)
  (hv : ‖v‖ = 1),
  FiniteDimensional.orthonormalBasisSingleton ι 𝕜 h v hv =
    (FiniteDimensional.basisSingleton ι h v ⋯).toOrthonormalBasis ⋯
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A weighted sum of pairwise subtractions, expressed as a subtraction of two `weightedVSub`
expressions.  -/
Finset.sum_smul_vsub_eq_weightedVSub_sub : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p₁ p₂ : ι → P),
  ∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i) = (s.weightedVSub p₁) w - (s.weightedVSub p₂) w
-- Mathlib.NumberTheory.Divisors
_private.Mathlib.NumberTheory.Divisors.0.Int.divisorsAntidiag.match_1.splitter : (motive : ℤ → Sort u_1) → (x : ℤ) → ((n : ℕ) → motive (Int.ofNat n)) → ((n : ℕ) → motive (Int.negSucc n)) → motive x
-- Mathlib.CategoryTheory.Presentable.Finite
CategoryTheory.ObjectProperty.isFinitelyPresentable_eq_isCardinalPresentable : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.ObjectProperty.isFinitelyPresentable C = CategoryTheory.isCardinalPresentable C Cardinal.aleph0
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instInvOfContinuousInv.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Inv β]
  [inst_3 : ContinuousInv β],
  ContinuousMap.instInvOfContinuousInv = { inv := fun f => { toFun := (⇑f)⁻¹, continuous_toFun := ⋯ } }
-- Mathlib.Order.PropInstances
Pi.codisjoint_iff : ∀ {ι : Type u_1} {α' : ι → Type u_3} [inst : (i : ι) → PartialOrder (α' i)] [inst_1 : (i : ι) → OrderTop (α' i)]
  {f g : (i : ι) → α' i}, Codisjoint f g ↔ ∀ (i : ι), Codisjoint (f i) (g i)
-- Lean.Exception
/-- Internal exceptions that are not meant to be seen by users.
Examples: "postpone elaboration", "stuck at universe constraint", etc.
 -/
Lean.Exception.internal : Lean.InternalExceptionId → optParam Lean.KVMap { } → Lean.Exception
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.δFromOpcycles.congr_simp : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ : ℤ)
  (hn₁ : n₀ + 1 = n₁), X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁ = X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ : B} (f : b₀ ⟶ b₁) (X : ↑(F.obj b₀)),
  (F.mapComp' f (CategoryTheory.CategoryStruct.id b₁) f ⋯).inv.toNatTrans.app X =
    (F.mapId b₁).hom.toNatTrans.app ((F.map f).toFunctor.obj X)
-- Init.Data.Vector.Basic
Vector.instMembership : {α : Type u_1} → {n : ℕ} → Membership α (Vector α n)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
/-- A Weierstrass equation over the fraction field `K` is minimal if the (multiplicative) valuation
of its discriminant is maximal among all isomorphic integral Weierstrass equations.
We still use 'minimal' for the naming, so as to standardize the naming with Silverman's book.  -/
WeierstrassCurve.IsMinimal : (R : Type u_1) →
  [inst : CommRing R] →
    [inst_1 : IsDomain R] →
      [IsDiscreteValuationRing R] →
        {K : Type u_2} → [inst_3 : Field K] → [inst_4 : Algebra R K] → [IsFractionRing R K] → WeierstrassCurve K → Prop
-- Mathlib.CategoryTheory.Functor.Basic
/-- A functor preserves composition.  -/
CategoryTheory.Functor.map_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (self : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
  self.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (self.map f) (self.map g)
-- Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
/-- Given a family of maps `f : K → (j ⟶ j')` in a `κ`-filtered category `J`,
with `HasCardinalLT K κ`, this is an object of `J` where these morphisms
shall be equalized.  -/
CategoryTheory.IsCardinalFiltered.coeq : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {κ : Cardinal.{w}} →
      [hκ : Fact κ.IsRegular] →
        [CategoryTheory.IsCardinalFiltered J κ] → {K : Type v'} → {j j' : J} → (K → (j ⟶ j')) → HasCardinalLT K κ → J
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.iterate_succ : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {f' : Module.End R M} (n : ℕ), f' ^ (n + 1) = (f' ^ n) ∘ₗ f'
-- Init.Data.List.Perm
List.Perm.nodup : ∀ {α : Type u_1} {l l' : List α}, l.Perm l' → l.Nodup → l'.Nodup
-- Mathlib.LinearAlgebra.RootSystem.Chain
_private.Mathlib.LinearAlgebra.RootSystem.Chain.0.RootPairing.chainCoeff_reflectionPerm_left_aux : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  Set.Icc (-↑(RootPairing.chainTopCoeff i j)) ↑(RootPairing.chainBotCoeff i j) =
    Set.Icc (-↑(RootPairing.chainBotCoeff (-i) j)) ↑(RootPairing.chainTopCoeff (-i) j)
-- Mathlib.Algebra.Group.Commute.Units
AddUnits.addCommute_iff_neg_add_cancel : ∀ {M : Type u_1} [inst : AddMonoid M] {u : AddUnits M} {a : M}, AddCommute (↑u) a ↔ ↑(-u) + a + ↑u = a
-- Mathlib.Order.WellFounded
WellFounded.instIsWellFoundedOnFun : ∀ {α : Type u_1} {β : Type u_2} (r : β → β → Prop) (f : α → β) [IsWellFounded β r], IsWellFounded α (Function.onFun r f)
-- Init.MetaTypes
Lean.Meta.Simp.ConfigCtx : Type
-- Mathlib.Topology.Category.LightProfinite.Basic
instIsEquivalenceLightProfiniteLightDiagramLightProfiniteToLightDiagram : lightProfiniteToLightDiagram.IsEquivalence
-- Std.Time.Format
/-- Formats a `PlainTime` value into a 24-hour format string (`HH:mm:ss.SSSSSSSSS`).
 -/
Std.Time.PlainTime.toLeanTime24Hour : Std.Time.PlainTime → String
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.reindex_apply : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (b : Module.Basis ι R M) (e : ι ≃ ι') (i' : ι'), (b.reindex e) i' = b (e.symm i')
-- Mathlib.AlgebraicGeometry.Fiber
AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberToSpecResidueField : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↥X),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.asFiberHom f x)
      (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField f (f x)) =
    AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem_alter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] {k k' : α} {f : Option β → Option β} (h : m.WF) {hc : k' ∈ m.alter k f},
  (m.alter k f)[k'] = if heq : (k == k') = true then (f m[k]?).get ⋯ else m[k']
-- Std.Http.Data.URI.Basic
/-- Sets a query parameter, replacing all existing values for that key.
Both key and value will be automatically percent-encoded.
 -/
Std.Http.URI.Query.set : Std.Http.URI.Query → String → String → Std.Http.URI.Query
-- Mathlib.Algebra.Homology.HomologicalComplex
_private.Mathlib.Algebra.Homology.HomologicalComplex.0.ChainComplex.mkAux.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Topology.UniformSpace.Equiv
/-- `(α × β) × γ` is uniformly isomorphic to `α × (β × γ)`.  -/
UniformEquiv.prodAssoc : (α : Type u) →
  (β : Type u_1) →
    (γ : Type u_2) →
      [inst : UniformSpace α] → [inst_1 : UniformSpace β] → [inst_2 : UniformSpace γ] → (α × β) × γ ≃ᵤ α × β × γ
-- Init.Data.Option.Lemmas
Option.join_beq_none : ∀ {α : Type u_1} [inst : BEq α] {o : Option (Option α)}, (o.join == none) = (o == none || o == some none)
-- Lean.Compiler.IR.Basic
/-- Join point Declaration `block_j (xs) := e; b`  -/
Lean.IR.FnBody.jdecl : Lean.IR.JoinPointId → Array Lean.IR.Param → Lean.IR.FnBody → Lean.IR.FnBody → Lean.IR.FnBody
-- Mathlib.Algebra.Group.Subgroup.Basic
MonoidHom.liftOfRightInverseAux.congr_simp : ∀ {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [inst : Group G₁] [inst_1 : Group G₂] [inst_2 : Group G₃]
  (f f_1 : G₁ →* G₂) (e_f : f = f_1) (f_inv f_inv_1 : G₂ → G₁) (e_f_inv : f_inv = f_inv_1)
  (hf : Function.RightInverse f_inv ⇑f) (g g_1 : G₁ →* G₃) (e_g : g = g_1) (hg : f.ker ≤ g.ker),
  f.liftOfRightInverseAux f_inv hf g hg = f_1.liftOfRightInverseAux f_inv_1 ⋯ g_1 ⋯
-- Init.Data.List.Scan.Basic
/-- Fold a function `f` over the list from the right, returning the list of partial results.
```
scanr (+) 0 [1, 2, 3] = [6, 5, 3, 0]
```
 -/
List.scanr : {α : Type u_1} → {β : Type u_2} → (α → β → β) → β → List α → List β
-- Mathlib.ModelTheory.ElementarySubstructures
/-- An elementary substructure is one in which every formula applied to a tuple in the substructure
agrees with its value in the overall structure.  -/
FirstOrder.Language.ElementarySubstructure : (L : FirstOrder.Language) → (M : Type u_1) → [L.Structure M] → Type u_1
-- Init.System.IOError
IO.Error.illegalOperation.injEq : ∀ (osCode : UInt32) (details : String) (osCode_1 : UInt32) (details_1 : String),
  (IO.Error.illegalOperation osCode details = IO.Error.illegalOperation osCode_1 details_1) =
    (osCode = osCode_1 ∧ details = details_1)
-- Mathlib.Tactic.Linter.TextBased
/-- Creates `StyleError`s for bad usage of unicode characters.  -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.UnicodeLinter.findBadUnicodeAux : (s : String) →
  s.Pos → Char → optParam (Array Mathlib.Linter.TextBased.StyleError✝) #[] → Array Mathlib.Linter.TextBased.StyleError✝
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- The equalizer of a morphism with itself is isomorphic to the source.  -/
CategoryTheory.Limits.equalizer.isoSourceOfSelf : {C : Type u} →
  {X Y : C} → [inst : CategoryTheory.Category.{v, u} C] → (f : X ⟶ Y) → CategoryTheory.Limits.equalizer f f ≅ X
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
Lean.Meta.Grind.Arith.CommRing.getSubFn : {m : Type → Type} →
  [MonadLiftT Lean.MetaM m] →
    [Lean.MonadError m] →
      [Monad m] → [Lean.Meta.Sym.Arith.MonadCanon m] → [Lean.Meta.Grind.Arith.CommRing.MonadRing m] → m Lean.Expr
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- A `MulEquiv` that respects open sets is a `ContinuousMulEquiv`.  -/
MulEquiv.toContinuousMulEquiv : {G : Type u} →
  [inst : TopologicalSpace G] →
    {H : Type v} →
      [inst_1 : TopologicalSpace H] →
        [inst_2 : Mul G] → [inst_3 : Mul H] → (e : G ≃* H) → (∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) → G ≃ₜ* H
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.SignedMeasure.haveLebesgueDecomposition_smul_real : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α)
  [s.HaveLebesgueDecomposition μ] (r : ℝ), (r • s).HaveLebesgueDecomposition μ
-- Mathlib.Topology.Algebra.Valued.WithVal
/-- The order-preserving, multiplicative equivalence between the `ValueGroup₀` of the valuation
on `WithVal v` and the valuation `v`.  -/
WithVal.valueGroupOrderIso₀ : {Γ₀ : Type u_2} →
  [inst : LinearOrderedCommGroupWithZero Γ₀] →
    {R : Type u_3} →
      [inst_1 : Ring R] →
        (v : Valuation R Γ₀) →
          (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ ≃*o (MonoidWithZeroHom.ofClass v).ValueGroup₀
-- Init.Data.Array.Lex.Lemmas
Array.not_le : ∀ {α : Type u_1} [inst : LT α] {xs ys : Array α}, ¬xs ≤ ys ↔ ys < xs
-- Mathlib.Tactic.Sat.FromLRAT
Mathlib.Tactic.Sat.Clause.mk.sizeOf_spec : ∀ (lits : Array ℤ) (expr proof : Lean.Expr),
  sizeOf { lits := lits, expr := expr, proof := proof } = 1 + sizeOf lits + sizeOf expr + sizeOf proof
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_union_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k fallback : α}, k ∉ m₁ → (m₁ ∪ m₂).getKeyD k fallback = m₂.getKeyD k fallback
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
/-- `HasProdUniformlyOn f g s` means that the (potentially infinite) product `∏' i, f i b`
for `b : β` converges uniformly on `s` to `g`.  -/
HasProdUniformlyOn : {α : Type u_1} →
  {β : Type u_2} → {ι : Type u_3} → [CommMonoid α] → (ι → β → α) → (β → α) → Set β → [UniformSpace α] → Prop
-- Mathlib.Algebra.Group.Commute.Defs
IsAddLeftRegular.addCommute_add_left_iff : ∀ {S : Type u_3} [inst : AddSemigroup S] {a b : S}, IsAddLeftRegular a → (AddCommute (a + b) a ↔ AddCommute a b)
-- Mathlib.Combinatorics.Additive.ETransform
Finset.mulETransformLeft_one : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Group α] (x : Finset α × Finset α), Finset.mulETransformLeft 1 x = x
-- Mathlib.GroupTheory.Finiteness
/-- A canonically ordered and well-quasi-ordered additive monoid must be finitely
generated.  -/
AddCommMonoid.fg_of_wellQuasiOrderedLE : ∀ {M : Type u_5} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [WellQuasiOrderedLE M] [IsOrderedCancelAddMonoid M]
  [CanonicallyOrderedAdd M], AddMonoid.FG M
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.instEssSurjLocalizedMonoidalToMonoidalCategory : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit),
  (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).EssSurj
-- Init.Data.List.Scan.Lemmas
List.head_scanl : ∀ {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : β → α → β} (h : List.scanl f b l ≠ []),
  (List.scanl f b l).head h = b
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.instAddMonoid : {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → AddMonoid (β i)] → AddMonoid (Π₀ (i : ι), β i)
-- Std.Time.Zoned.RecurringRule
Std.Time.TimeZone.instReprTransitionSpec.repr : Std.Time.TimeZone.TransitionSpec → ℕ → Std.Format
-- Mathlib.Order.Bounds.Basic
lowerBounds_union : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, lowerBounds (s ∪ t) = lowerBounds s ∩ lowerBounds t
-- Mathlib.Algebra.Category.ModuleCat.FilteredColimits
ModuleCat.FilteredColimits.colimitMulAction : {R : Type u} →
  [inst : Ring R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.SmallCategory J] →
        [inst_2 : CategoryTheory.IsFiltered J] →
          (F : CategoryTheory.Functor J (ModuleCat R)) → MulAction R ↑(ModuleCat.FilteredColimits.M F)
-- Mathlib.Data.Finmap
Finmap.mem_union : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {s₁ s₂ : Finmap β}, a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ ∨ a ∈ s₂
-- Mathlib.Algebra.Quaternion
Quaternion.normSq_def : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), Quaternion.normSq a = (a * star a).re
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.keys_map : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w}
  {f : (a : α) → β a → γ a}, (Std.DHashMap.map f m).keys.Perm m.keys