mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.add_of_Y_ne' : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ x₂ y₁ y₂ : F}
  {h₁ : W.Nonsingular x₁ y₁} {h₂ : W.Nonsingular x₂ y₂} (hy : y₁ ≠ W.negY x₂ y₂),
  WeierstrassCurve.Affine.Point.some x₁ y₁ h₁ + WeierstrassCurve.Affine.Point.some x₂ y₂ h₂ =
    -WeierstrassCurve.Affine.Point.some (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
        ⋯
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.mkCommaObject_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor (CategoryTheory.WithInitial C) D),
  (CategoryTheory.WithInitial.mkCommaObject F).left = F.obj CategoryTheory.WithInitial.star
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_filter_key : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → Bool} {k fallback : α},
  (Std.ExtHashMap.filter (fun k x => f k) m).getKeyD k fallback = (Option.filter f (m.getKey? k)).getD fallback
-- Lean.Declaration
Lean.ConstantVal.mk.injEq : ∀ (name : Lean.Name) (levelParams : List Lean.Name) (type : Lean.Expr) (name_1 : Lean.Name)
  (levelParams_1 : List Lean.Name) (type_1 : Lean.Expr),
  ({ name := name, levelParams := levelParams, type := type } =
      { name := name_1, levelParams := levelParams_1, type := type_1 }) =
    (name = name_1 ∧ levelParams = levelParams_1 ∧ type = type_1)
-- Std.Sync.StreamMap
/-- Register a new async stream with the given name
 -/
Std.StreamMap.register : {α t β : Type} → [BEq α] → [Std.Async.IO.AsyncStream t β] → Std.StreamMap α β → α → t → Std.StreamMap α β
-- Mathlib.Algebra.NoZeroSMulDivisors.Pi
Pi.noZeroSMulDivisors : ∀ {I : Type u} {f : I → Type v} (α : Type u_1) [inst : Semiring α] [IsDomain α] [inst_2 : (i : I) → AddCommGroup (f i)]
  [inst_3 : (i : I) → Module α (f i)] [∀ (i : I), NoZeroSMulDivisors α (f i)], NoZeroSMulDivisors α ((i : I) → f i)
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.instLocallyCompactSpaceCarrierI : LocallyCompactSpace ↑TopCat.I
-- Std.Time.Time.Unit.Nanosecond
/-- Converts an `Ordinal` to an `Offset`.
 -/
Std.Time.Nanosecond.Ordinal.toOffset : Std.Time.Nanosecond.Ordinal → Std.Time.Nanosecond.Offset
-- Std.Internal.Do.WP.Basic
/-- `ExceptT` lifts a `WPMonad` instance by adding an exception postcondition layer.  -/
Std.Internal.Do.ExceptT.instWPMonad : {m : Type u → Type z} →
  {EPred : Type u_1} →
    {ε : Type u} →
      {Pred : Type v} →
        [inst : Monad m] →
          [inst_1 : Std.Internal.Do.Assertion Pred] →
            [inst_2 : Std.Internal.Do.Assertion EPred] →
              [Std.Internal.Do.WPMonad m Pred EPred] →
                Std.Internal.Do.WPMonad (ExceptT ε m) Pred (EPost.Cons✝ (ε → Pred) EPred)
-- Lean.HeadIndex
Lean.instInhabitedHeadIndex : Inhabited Lean.HeadIndex
-- Lean.Parser.Do
Lean.Parser.Term.doReturn.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Data.PFunctor.Multivariate.W
MvPFunctor.WPath.root.inj : ∀ {n : ℕ} {P : MvPFunctor.{u} (n + 1)} {a : P.A} {f : P.last.B a → P.last.W} {i : Fin2 n} {c c_1 : P.drop.B a i},
  MvPFunctor.WPath.root a f i c = MvPFunctor.WPath.root a f i c_1 → c = c_1
-- Mathlib.CategoryTheory.Functor.Currying
/-- A version of `CategoryTheory.whiskeringRight` for bifunctors, obtained by uncurrying,
applying `whiskeringRight` and currying back
 -/
CategoryTheory.Functor.whiskeringRight₂ : (B : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} B] →
    (C : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C] →
        (D : Type u₃) →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} D] →
            (E : Type u₄) →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} E] →
                CategoryTheory.Functor (CategoryTheory.Functor C (CategoryTheory.Functor D E))
                  (CategoryTheory.Functor (CategoryTheory.Functor B C)
                    (CategoryTheory.Functor (CategoryTheory.Functor B D) (CategoryTheory.Functor B E)))
-- Mathlib.RingTheory.WittVector.Frobenius
WittVector.coeff_frobeniusFun : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] (x : WittVector p R) (n : ℕ),
  x.frobeniusFun.coeff n = (MvPolynomial.aeval x.coeff) (WittVector.frobeniusPoly p n)
-- Mathlib.LinearAlgebra.Matrix.Bilinear
mulRightLinearMap.congr_simp : ∀ (l : Type u_1) {m : Type u_2} {n : Type u_3} (R : Type u_5) {A : Type u_6} [inst : Fintype m] [inst_1 : Semiring R]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : Module R A] [inst_4 : IsScalarTower R A A] (Y Y_1 : Matrix m n A),
  Y = Y_1 → mulRightLinearMap l R Y = mulRightLinearMap l R Y_1
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
/-- If the product comparison map for `G` at `(X,Y)` is an isomorphism, then `G` preserves the
pair of `(X,Y)`.
 -/
CategoryTheory.Limits.PreservesLimitPair.of_iso_prod_comparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) (X Y : C) [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Y]
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct (G.obj X) (G.obj Y)]
  [i : CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison G X Y)],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X Y) G
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_of_isEmpty : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {f : X → E} {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} [IsEmpty X],
  ∫ᵛ (x : X), f x ∂[B; μ] = 0
-- Mathlib.Algebra.MonoidAlgebra.Support
MonoidAlgebra.support_coeff_mul_single_eq_image : ∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : Mul G] [inst_2 : DecidableEq G] (f : MonoidAlgebra k G)
  {r : k},
  (∀ (y : k), y * r = 0 ↔ y = 0) →
    ∀ {x : G},
      IsRightRegular x →
        (f * MonoidAlgebra.single x r).coeff.support = Finset.image (fun x_1 => x_1 * x) f.coeff.support
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.mem_ofFixingAddSubgroup_iff : ∀ (M : Type u_1) {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {s : Set α} {x : α},
  x ∈ SubAddAction.ofFixingAddSubgroup M s ↔ x ∉ s
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.dualAnnihilator_inj : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {W W' : Subspace K V},
  Submodule.dualAnnihilator W = Submodule.dualAnnihilator W' ↔ W = W'
-- Init.Notation
Lean.guardMsgsFilterAction : Lean.ParserDescr
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.map_S : ∀ {R : Type u_1} {R' : Type u_2} [inst : CommRing R] [inst_1 : CommRing R'] (f : R →+* R') (n : ℤ),
  Polynomial.map f (Polynomial.Chebyshev.S R n) = Polynomial.Chebyshev.S R' n
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.union_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ m₃ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₃.WF → m₂.Equiv m₃ → (m₁ ∪ m₂).Equiv (m₁ ∪ m₃)
-- Mathlib.Algebra.Notation.Defs
dite_sub : ∀ {α : Type u_2} (P : Prop) [inst : Decidable P] [inst_1 : Sub α] (a : P → α) (b : ¬P → α) (c : α),
  (if h : P then a h else b h) - c = if h : P then a h - c else b h - c
-- Lean.Elab.MutualInductive
Lean.Elab.Command.instInhabitedInductiveElabDescr.default : Lean.Elab.Command.InductiveElabDescr
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_eq_getD_getKey? : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a fallback : α}, m.getKeyD a fallback = (m.getKey? a).getD fallback
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.ofRightAdjoint.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] {G : CategoryTheory.Functor K D}
  {left : CategoryTheory.Functor (CategoryTheory.Limits.Cone F) (CategoryTheory.Limits.Cone G)}
  {right : CategoryTheory.Functor (CategoryTheory.Limits.Cone G) (CategoryTheory.Limits.Cone F)} (adj : left ⊣ right)
  {c : CategoryTheory.Limits.Cone G} (t : CategoryTheory.Limits.IsLimit c),
  CategoryTheory.Limits.IsLimit.ofRightAdjoint adj t =
    CategoryTheory.Limits.IsLimit.mkConeMorphism (fun s => (adj.homEquiv s c) (t.liftConeMorphism (left.obj s))) ⋯
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
trdeg_le_of_injective : ∀ {R : Type u_2} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {A' : Type v}
  [inst_3 : CommRing A'] [inst_4 : Algebra R A'] (f : A →ₐ[R] A'),
  Function.Injective ⇑f → Algebra.trdeg R A ≤ Algebra.trdeg R A'
-- Std.Do.SPred.Laws
Std.Do.SPred.bientails.trans : ∀ {σs : List (Type u)} {P Q R : Std.Do.SPred σs}, (P ⊣⊢ₛ Q) → (Q ⊣⊢ₛ R) → P ⊣⊢ₛ R
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.id_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.MonObj A] (M : CategoryTheory.Mod D A),
  M.id.hom = CategoryTheory.CategoryStruct.id M.X
-- Aesop.Script.Tactic
Aesop.Script.Tactic.structured : Aesop.Script.UTactic → Aesop.Script.STactic → Aesop.Script.Tactic
-- Mathlib.Order.SupIndep
Finset.SupIndep.antitone_fun : ∀ {α : Type u_1} {ι : Type u_3} [inst : Lattice α] [inst_1 : OrderBot α] {s : Finset ι} {f g : ι → α},
  (∀ x ∈ s, f x ≤ g x) → s.SupIndep g → s.SupIndep f
-- Init.Data.Int.Gcd
Int.lcm_one_right : ∀ (a : ℤ), a.lcm 1 = a.natAbs
-- Mathlib.RingTheory.RingHom.Surjective
/-- `M⁻¹R →+* M⁻¹S` is surjective if `R →+* S` is surjective.  -/
RingHom.surjective_localizationPreserves : RingHom.LocalizationPreserves fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f
-- Mathlib.Algebra.Group.Basic
SubtractionMonoid.toSubNegZeroMonoid : {α : Type u_1} → [SubtractionMonoid α] → SubNegZeroMonoid α
-- Init.Data.Array.Lemmas
Array.foldl_filterMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Option β} {g : γ → β → γ} {xs : Array α} {init : γ},
  Array.foldl g init (Array.filterMap f xs) =
    Array.foldl
      (fun x y =>
        match f y with
        | some b => g x b
        | none => x)
      init xs
-- Mathlib.Analysis.Normed.Group.Quotient
NormedAddGroupHom.norm_lift_le : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {N : Type u_3} [inst_1 : SeminormedAddCommGroup N]
  (S : AddSubgroup M) (f : NormedAddGroupHom M N) (hf : ∀ s ∈ S, f s = 0), ‖NormedAddGroupHom.lift S f hf‖ ≤ ‖f‖
-- Mathlib.RingTheory.Nilpotent.Lemmas
/-- The nilradical of a commutative semiring is the ideal of nilpotent elements.  -/
nilradical : (R : Type u_3) → [inst : CommSemiring R] → Ideal R
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.Nonsquare.mk : ∀ {x : ℕ}, (∀ (n : ℕ), x ≠ n * n) → Zsqrtd.Nonsquare x
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- The machine configuration translation.  -/
Turing.TM1to1.trCfg : {Γ : Type u_1} →
  {Λ : Type u_2} →
    {σ : Type u_3} →
      {n : ℕ} →
        (enc : Γ → List.Vector Bool n) →
          [inst : Inhabited Γ] →
            enc default = List.Vector.replicate n false →
              Turing.TM1.Cfg Γ Λ σ → Turing.TM1.Cfg Bool (Turing.TM1to1.Λ' Γ Λ σ) σ
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- An inductive constructor for `ℕ`-indexed cochain complexes.

You provide explicitly the first two differentials,
then a function which takes two differentials and the fact they compose to zero,
and returns the next object, its differential, and the fact it composes appropriately to zero.

See also `mk'`, which only sees the previous differential in the inductive step.
 -/
CochainComplex.mk : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      (X₀ X₁ X₂ : V) →
        (d₀ : X₀ ⟶ X₁) →
          (d₁ : X₁ ⟶ X₂) →
            CategoryTheory.CategoryStruct.comp d₀ d₁ = 0 →
              ((S : CategoryTheory.ShortComplex V) →
                  (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' CategoryTheory.CategoryStruct.comp S.g d₂ = 0) →
                CochainComplex V ℕ
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndep_comap_mem_iff : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : ι → Set Ω},
  ProbabilityTheory.iIndep (fun i => MeasurableSpace.comap (fun x => x ∈ f i) ⊤) μ ↔ ProbabilityTheory.iIndepSet f μ
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
/-- Completely evaluate a `LazyEntry`.  -/
Lean.Meta.RefinedDiscrTree.LazyEntry.toList : Lean.Meta.RefinedDiscrTree.LazyEntry →
  optParam (List Lean.Meta.RefinedDiscrTree.Key) [] → Lean.MetaM (List Lean.Meta.RefinedDiscrTree.Key)
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.zeroEquiv_naturality : ∀ {R : Type u} [inst : CommRing R] {M : Type u_1} {N : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M →ₗ[R] N),
  ↑(exteriorPower.zeroEquiv R N) ∘ₗ exteriorPower.map 0 f = ↑(exteriorPower.zeroEquiv R M)
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion_neg : ∀ {α : Type u_2} {ι : Sort u_5} [inst : Neg α] (s : ι → Set α), -⋃ i, s i = ⋃ i, -s i
-- Mathlib.Algebra.Order.Ring.Ordering.Basic
RingPreordering.support_ne_top : ∀ {R : Type u_1} [inst : CommRing R] (P : RingPreordering R) [inst_1 : P.HasIdealSupport], P.support ≠ ⊤
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeGroup.reduceCyclically.cons_append : ∀ {α : Type u} [inst : DecidableEq α] {a b : α × Bool} (L : List (α × Bool)),
  FreeGroup.reduceCyclically (a :: (L ++ [b])) =
    if b.1 = a.1 ∧ (!b.2) = a.2 then FreeGroup.reduceCyclically L else a :: L ++ [b]
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.SMulInvariantMeasure.zero : ∀ {M : Type v} {α : Type w} [inst : MeasurableSpace α] [inst_1 : SMul M α], MeasureTheory.SMulInvariantMeasure M α 0
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.powerSeriesEquivSubring_apply : ∀ (K : Type u_2) [inst : Field K] (f : PowerSeries K),
  (LaurentSeries.powerSeriesEquivSubring K) f = ⟨(HahnSeries.ofPowerSeries ℤ K) f, ⋯⟩
-- Mathlib.Algebra.Field.Shrink
Shrink.instRatCast : {α : Type u_1} → [inst : Small.{v, u_1} α] → [RatCast α] → RatCast (Shrink.{v, u_1} α)
-- Mathlib.Logic.Equiv.Prod
/-- `Empty` type is a left absorbing element for type product up to an equivalence.  -/
Equiv.emptyProd : (α : Type u_9) → Empty × α ≃ Empty
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
/-- If `g` is surjective, then `lTensor Q g` is surjective  -/
LinearMap.lTensor_surjective : ∀ {R : Type u_1} [inst : CommSemiring R] {N : Type u_3} {P : Type u_4} (Q : Type u_5) [inst_1 : AddCommMonoid N]
  [inst_2 : AddCommMonoid P] [inst_3 : AddCommMonoid Q] [inst_4 : Module R N] [inst_5 : Module R P]
  [inst_6 : Module R Q] {g : N →ₗ[R] P}, Function.Surjective ⇑g → Function.Surjective ⇑(LinearMap.lTensor Q g)
-- Init.Grind.Ring.Basic
/-- The zeroth power of any element is one.  -/
Lean.Grind.Semiring.pow_zero : ∀ {α : Type u} [self : Lean.Grind.Semiring α] (a : α), a ^ 0 = 1
-- Mathlib.Logic.Encodable.Basic
_private.Mathlib.Logic.Encodable.Basic.0.Directed.sequence.match_3.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
/-- Construct a cover in the `P`-qc topology from a quasi-compact cover in the `P`-topology.  -/
AlgebraicGeometry.Scheme.Cover.ofQuasiCompactCover : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {S : AlgebraicGeometry.Scheme} →
    (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S) →
      [qc : AlgebraicGeometry.QuasiCompactCover 𝒰.toPreZeroHypercover] →
        AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.propQCPrecoverage P) S
-- Lean.Expr
Lean.instEmptyCollectionFVarIdMap : {α : Type} → EmptyCollection (Lean.FVarIdMap α)
-- Init.Data.List.Basic
/-- Returns the list of elements in `l` for which `p` returns `true`.

`O(|l|)`. This is a tail-recursive version of `List.filter`, used at runtime.

Examples:
* `[1, 2, 5, 2, 7, 7].filterTR (· > 2)  = [5, 7, 7]`
* `[1, 2, 5, 2, 7, 7].filterTR (fun _ => false) = []`
* `[1, 2, 5, 2, 7, 7].filterTR (fun _ => true) = * [1, 2, 5, 2, 7, 7]`
 -/
List.filterTR : {α : Type u} → (α → Bool) → List α → List α
-- Mathlib.GroupTheory.Perm.Option
Equiv.Perm.decomposeOption_symm_of_none_apply : ∀ {α : Type u_1} [inst : DecidableEq α] (e : Equiv.Perm α) (i : Option α),
  (Equiv.Perm.decomposeOption.symm (none, e)) i = Option.map (⇑e) i
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.type_preimage : ∀ {α β : Type u} (r : α → α → Prop) [inst : IsWellOrder α r] (f : β ≃ α), Ordinal.type (⇑f ⁻¹'o r) = Ordinal.type r
-- Mathlib.Analysis.Convex.Basic
Convex.affinity : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : CommSemiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s : Set E}, Convex 𝕜 s → ∀ (z : E) (c : 𝕜), Convex 𝕜 ((fun x => z + c • x) '' s)
-- Mathlib.Order.Notation
/-- Heyting negation 

Conventions for notations in identifiers:

 * The recommended spelling of `￢` in identifiers is `hnot`. -/
«term￢_» : Lean.ParserDescr
-- Mathlib.Topology.Algebra.Module.Complement
ContinuousLinearMap.IsIdempotentElem.eq_projectionL : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {f : M →L[R] M} (hf : IsIdempotentElem f), f = (↑f).range.projectionL (↑f).ker ⋯
-- Mathlib.CategoryTheory.Sites.Descent.IsPrestack
/-- The property that a pseudofunctor `F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat`
satisfies the descent property for morphisms, i.e. is a prestack.
(See the terminological note in the introduction of the file `Sites.Descent.IsPrestack`.)  -/
CategoryTheory.Pseudofunctor.IsPrestack : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat →
      CategoryTheory.GrothendieckTopology C → Prop
-- Std.Do.PostCond
/-- An assertion about the state fields for a monad whose postcondition shape is `ps`.

Concretely, this is an abbreviation for `SPred` applied to the `.arg`s in the given predicate shape, so all theorems about `SPred` apply.

Examples:
```lean example
example : Assertion (.arg ρ .pure) = (ρ → ULift Prop) := rfl
example : Assertion (.except ε .pure) = ULift Prop := rfl
example : Assertion (.arg σ (.except ε .pure)) = (σ → ULift Prop) := rfl
example : Assertion (.except ε (.arg σ .pure)) = (σ → ULift Prop) := rfl
```
 -/
Std.Do.Assertion : Std.Do.PostShape → Type u
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.IsFirstQuadrant.isZero₁ : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Abelian C}
  {Y : CategoryTheory.Abelian.SpectralObject C EInt} [self : Y.IsFirstQuadrant] (i j : EInt) (hij : i ≤ j),
  j ≤ WithBotTop.coe 0 →
    ∀ (n : ℤ),
      CategoryTheory.Limits.IsZero ((Y.H n).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hij)))
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.toOuterMeasure_apply_eq_one_iff : ∀ {α : Type u_1} (p : PMF α) (s : Set α), p.toOuterMeasure s = 1 ↔ p.support ⊆ s
-- Mathlib.Order.CompleteLattice.Defs
CompleteLinearOrder.toHImp : {α : Type u_8} → [self : CompleteLinearOrder α] → HImp α
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Power.beq' : Lean.Grind.CommRing.Power → Lean.Grind.CommRing.Power → Bool
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_insert : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h : t.WF) {k a : α} {v : β}
  {h₁ : Std.DTreeMap.Internal.Impl.contains a (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl = true},
  Std.DTreeMap.Internal.Impl.Const.get (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl a h₁ =
    if h₂ : compare k a = Ordering.eq then v else Std.DTreeMap.Internal.Impl.Const.get t a ⋯
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey!_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {v : β k},
      Std.Internal.List.minKey! (Std.Internal.List.insertEntryIfNew k v l) =
        (Std.Internal.List.minKey? l).elim k fun k' => if compare k k' = Ordering.lt then k else k'
-- Init.Data.Array.Range
/-- Replace `zipIdx` with a starting index `n+1` with `zipIdx` starting from `n`,
followed by a `map` increasing the indices by one.  -/
Array.zipIdx_succ : ∀ {α : Type u_1} {xs : Array α} {i : ℕ},
  xs.zipIdx (i + 1) =
    Array.map
      (fun x =>
        match x with
        | (a, j) => (a, j + 1))
      (xs.zipIdx i)
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coe_add : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (I J : FractionalIdeal S P), ↑(I + J) = ↑I + ↑J
-- Mathlib.Order.Heyting.Basic
inf_sdiff_sup_right : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, a \ c ⊓ (b ⊔ a) = a \ c
-- Init.Data.Nat.Bitwise.Lemmas
Nat.zero_and : ∀ (x : ℕ), 0 &&& x = 0
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
/-- If `d : MultispanIndex J C`, `c : Multicofork d` is a colimit multicofork,
and `F : C ⥤ D` is a functor which preserves the colimit of `d.multispan`,
then the multicofork `c.map F` is colimit.  -/
CategoryTheory.Limits.Multicofork.isColimitMapOfPreserves : {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] →
        {J : CategoryTheory.Limits.MultispanShape} →
          {d : CategoryTheory.Limits.MultispanIndex J C} →
            (c : CategoryTheory.Limits.Multicofork d) →
              (F : CategoryTheory.Functor C D) →
                [CategoryTheory.Limits.PreservesColimit d.multispan F] →
                  CategoryTheory.Limits.IsColimit c → CategoryTheory.Limits.IsColimit (c.map F)
-- Lean.Syntax
Lean.Syntax.TopDown : Type
-- Mathlib.RingTheory.Perfectoid.FontaineTheta
WittVector.ghostComponentModPPow_teichmuller_coeff : ∀ {R : Type u} [inst : CommRing R] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : Fact ¬IsUnit ↑p]
  [inst_3 : IsAdicComplete (Ideal.span {↑p}) R] (n : ℕ) (x : PreTilt R p),
  (WittVector.ghostComponentModPPow n) ((WittVector.teichmuller p) ((PreTilt.coeff n) x)) =
    (Ideal.Quotient.mk (Ideal.span {↑p} ^ (n + 1))) (PreTilt.untilt x)
-- Init.Control.Lawful.MonadLift.Instances
ExceptT.instLawfulMonadLiftExcept : ∀ {m : Type u → Type v} [inst : Monad m] [LawfulMonad m] {ε : Type u}, LawfulMonadLift (Except ε) (ExceptT ε m)
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.mem_span_pair : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x y z : M},
  z ∈ Submodule.span R {x, y} ↔ ∃ a b, a • x + b • y = z
-- Mathlib.Algebra.Category.Ring.Limits
/-- The forgetful functor from commutative rings to rings preserves all limits.
(That is, the underlying rings could have been computed instead as limits in the category of rings.)
 -/
CommRingCat.forget₂Ring_preservesLimitsOfSize : ∀ [UnivLE.{v, u}],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ CommRingCat RingCat)