mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} [inst_2 : Inhabited (β k)], (t₁ ∪ t₂).get! k = t₂.getD k (t₁.get! k)
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.ExprsEqualUpToIdsM : Type → Type
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_alter_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k : α} {f : Option β → Option β},
  (m.alter k f).getKey! k = if (f m[k]?).isSome = true then k else default
-- Mathlib.LinearAlgebra.Matrix.Rank
/-- TODO: prove this in greater generality.  -/
Matrix.rank_conjTranspose : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Fintype n] [inst_1 : Fintype m] [inst_2 : Field R]
  [inst_3 : PartialOrder R] [inst_4 : StarRing R] [StarOrderedRing R] (A : Matrix m n R), A.conjTranspose.rank = A.rank
-- Lean.Meta.Sym.Offset
Lean.Meta.Sym.Offset.add.inj : ∀ {e : Lean.Expr} {k : ℕ} {e_1 : Lean.Expr} {k_1 : ℕ},
  Lean.Meta.Sym.Offset.add e k = Lean.Meta.Sym.Offset.add e_1 k_1 → e = e_1 ∧ k = k_1
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
/-- The unit for the left Kan lift `f₊ g`.  -/
CategoryTheory.Bicategory.lanLiftUnit : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      (f : b ⟶ a) →
        (g : c ⟶ a) →
          [inst_1 : CategoryTheory.Bicategory.HasLeftKanLift f g] →
            g ⟶ CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lanLift f g) f
-- Mathlib.Tactic.DefEqAbuse
_private.Mathlib.Tactic.DefEqAbuse.0.Lean.MessageData.VisitStep.ascend.inj : ∀ {α : Type u_1} {returning returning_1 : Option α},
  Lean.MessageData.VisitStep.ascend✝ returning = Lean.MessageData.VisitStep.ascend✝ returning_1 →
    returning = returning_1
-- Mathlib.MeasureTheory.Group.Integral
MeasureTheory.Integrable.comp_div_right : ∀ {G : Type u_4} {F : Type u_6} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.Measure G}
  [inst_2 : Group G] [MeasurableMul G] {f : G → F} [μ.IsMulRightInvariant],
  MeasureTheory.Integrable f μ → ∀ (g : G), MeasureTheory.Integrable (fun t => f (t / g)) μ
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompPointIso_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  (X : CategoryTheory.Functor AugmentedSimplexCategoryᵒᵖ C),
  AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompPointIso.inv.app X =
    CategoryTheory.CategoryStruct.id (X.obj (Opposite.op CategoryTheory.WithInitial.star))
-- Mathlib.RingTheory.FilteredAlgebra.Basic
IsRingFiltration.mk : ∀ {ι : Type u_1} {R : Type u_2} {σ : Type u_3} [inst : AddMonoid ι] [inst_1 : PartialOrder ι] [inst_2 : Preorder σ]
  [inst_3 : Semiring R] [inst_4 : SetLike σ R] {F : ι → σ} {F_lt : outParam (ι → σ)}
  [toIsFiltration : IsFiltration F F_lt] [toGradedMonoid : SetLike.GradedMonoid F], IsRingFiltration F F_lt
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.mem_toList_iff_getKey?_eq_some_and_get?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {v : β}, (k, v) ∈ Std.DTreeMap.Const.toList t ↔ t.getKey? k = some k ∧ Std.DTreeMap.Const.get? t k = some v
-- Mathlib.Algebra.ContinuedFractions.Basic
GenContFract.instInhabitedPair.default : {α : Type u_1} → [Inhabited α] → GenContFract.Pair α
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasurableEmbedding.eLpNorm_map_measure : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {β : Type u_8} {mβ : MeasurableSpace β} {f : α → β}
  {g : β → ε},
  MeasurableEmbedding f → MeasureTheory.eLpNorm g p (MeasureTheory.Measure.map f μ) = MeasureTheory.eLpNorm (g ∘ f) p μ
-- Mathlib.Data.Real.Basic
Real.instDistribLattice : DistribLattice ℝ
-- Init.Grind.Module.Envelope
_private.Init.Grind.Module.Envelope.0.Lean.Grind.IntModule.OfNatModule.rel.eq_1 : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] (h : Equivalence (Lean.Grind.IntModule.OfNatModule.r α))
  (q₁ q₂ : Lean.Grind.IntModule.OfNatModule.Q α),
  Lean.Grind.IntModule.OfNatModule.rel✝ h q₁ q₂ =
    q₁.liftOn₂ q₂ (fun a₁ a₂ => Lean.Grind.IntModule.OfNatModule.r α a₁ a₂) ⋯
-- Std.Do.WP.Monad
_private.Std.Do.WP.Monad.0.Std.Do.PredTrans.pushOption.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((a : α) → motive (some a)) → (Unit → motive none) → motive x
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.cylinder.map_ι₀_mapHomologicalComplexObjIso_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (F : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel] {D : Type u_3}
  [inst_3 : CategoryTheory.Category.{v_2, u_3} D] [inst_4 : CategoryTheory.Preadditive D]
  (H : CategoryTheory.Functor C D) [inst_5 : H.Additive]
  [inst_6 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (F.X i) (F.X i)]
  [inst_7 :
    HomologicalComplex.HasHomotopyCofiber
      (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id F) (-CategoryTheory.CategoryStruct.id F))]
  [inst_8 :
    ∀ (i : ι),
      CategoryTheory.Limits.HasBinaryBiproduct (((H.mapHomologicalComplex c).obj F).X i)
        (((H.mapHomologicalComplex c).obj F).X i)]
  [inst_9 :
    HomologicalComplex.HasHomotopyCofiber
      (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id ((H.mapHomologicalComplex c).obj F))
        (-CategoryTheory.CategoryStruct.id ((H.mapHomologicalComplex c).obj F)))]
  [inst_10 :
    HomologicalComplex.HasHomotopyCofiber
      ((H.mapHomologicalComplex c).map
        (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id F) (-CategoryTheory.CategoryStruct.id F)))]
  (hc : ∀ (j : ι), ∃ i, c.Rel i j) {Z : HomologicalComplex D c} (h : ((H.mapHomologicalComplex c).obj F).cylinder ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((H.mapHomologicalComplex c).map (HomologicalComplex.cylinder.ι₀ F))
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.mapHomologicalComplexObjIso F H hc).hom h) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.ι₀ ((H.mapHomologicalComplex c).obj F)) h
-- Init.Data.Slice.Operations
/-- Allocates a new array that contains the elements of the slice.  -/
Std.Slice.toArray : {γ : Type u_1} →
  {α β : Type u_2} → [Std.ToIterator (Std.Slice γ) Id α β] → [Std.Iterator α Id β] → Std.Slice γ → Array β
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {f : α → Bool} {k : α}
  {h : k ∈ Std.TreeSet.filter f t}, (Std.TreeSet.filter f t).get k h = t.get k ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- `f` is the coequalizer  -/
CategoryTheory.RegularEpi.isColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        (self : CategoryTheory.RegularEpi f) → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ f ⋯)
-- Mathlib.NumberTheory.ModularForms.Basic
/-- **Alias** of `FunLike.coeMonoidHom`. -/
CuspForm.coeHom : (F : Type u_1) →
  (α : Type u_2) →
    (β : Type u_3) →
      [inst : FunLike F α β] →
        [inst_1 : MulOne F] → [inst_2 : MulOneClass β] → [IsOneApply F α β] → [IsMulApply F α β] → F →* α → β
-- Mathlib.Data.Set.Lattice
Set.subset_iInter₂_iff : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} {s : Set α} {t : (i : ι) → κ i → Set α},
  s ⊆ ⋂ i, ⋂ j, t i j ↔ ∀ (i : ι) (j : κ i), s ⊆ t i j
-- Mathlib.Data.Rat.Defs
Rat.divInt_eq_zero : ∀ {a b : ℤ}, b ≠ 0 → (Rat.divInt a b = 0 ↔ a = 0)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.minKey_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF → t₂.WF → ∀ (h : t₁.Equiv t₂) (h' : t₁.isEmpty = false), t₁.minKey h' = t₂.minKey ⋯
-- Mathlib.Data.ZMod.Defs
Fin.instHPowNatOfNeZero_mathlib : (n : ℕ) → [NeZero n] → HPow (Fin n) ℕ (Fin n)
-- Init.GrindInstances.Ring.UInt
UInt8.instOfNat.eq_1 : ∀ {n : ℕ}, UInt8.instOfNat = { ofNat := UInt8.ofNat n }
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getEntryGE_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {k : α} {he : ∃ a ∈ t₁, (compare a k).isGE = true},
  Std.DTreeMap.Internal.Impl.getEntryGE k t₁ ⋯ he = Std.DTreeMap.Internal.Impl.getEntryGE k t₂ ⋯ ⋯
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.mk.injEq : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : Semiring R] [inst_1 : Semiring R₂] {σ₁₂ : R →+* R₂} {E : Type u_11}
  {E₂ : Type u_12} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (toLinearMap : E →ₛₗ[σ₁₂] E₂) (norm_map' : ∀ (x : E), ‖toLinearMap x‖ = ‖x‖)
  (toLinearMap_1 : E →ₛₗ[σ₁₂] E₂) (norm_map'_1 : ∀ (x : E), ‖toLinearMap_1 x‖ = ‖x‖),
  ({ toLinearMap := toLinearMap, norm_map' := norm_map' } =
      { toLinearMap := toLinearMap_1, norm_map' := norm_map'_1 }) =
    (toLinearMap = toLinearMap_1)
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.aleph_ofNat_eq_lift : ∀ {c : Cardinal.{u}} {n : ℕ} [inst : n.AtLeastTwo],
  Cardinal.aleph (OfNat.ofNat n) = Cardinal.lift.{v, u} c ↔ Cardinal.aleph (OfNat.ofNat n) = c
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_ite_zero : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] (s : Finset ι) (p : ι → Prop)
  [inst_2 : DecidablePred p],
  (∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j) →
    ∀ (a : M), (s.expect fun i => if p i then a else 0) = if ∃ i ∈ s, p i then (↑s.card)⁻¹ • a else 0
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.Truncated.HomotopyCategory.subsingleton_hom : ∀ (X : SSet.Truncated 2)
  [Unique (X.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 }))]
  [Subsingleton (X.obj (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.ι0₂._proof_5 }))]
  (x y : X.HomotopyCategory), Subsingleton (x ⟶ y)
-- Mathlib.LinearAlgebra.Dimension.Constructions
/-- The rank of the direct sum is the sum of the ranks.  -/
rank_directSum : ∀ (R : Type u) [inst : Semiring R] [StrongRankCondition R] {ι : Type v} (M : ι → Type w)
  [inst_2 : (i : ι) → AddCommMonoid (M i)] [inst_3 : (i : ι) → Module R (M i)] [∀ (i : ι), Module.Free R (M i)],
  Module.rank R (DirectSum ι fun i => M i) = Cardinal.sum fun i => Module.rank R (M i)
-- Init.Data.Vector.Attach
_private.Init.Data.Vector.Attach.0.Vector.pmapImpl.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {P : α → Prop} (f : (a : α) → P a → β) (xs : Vector α n) (H : ∀ a ∈ xs, P a),
  Vector.pmapImpl f xs H =
    Vector.map
      (fun x =>
        match x with
        | ⟨x, h'⟩ => f x h')
      (xs.attachWith P H)
-- Mathlib.Condensed.Discrete.Module
CondensedMod.LocallyConstant.instFullModuleCatSheafCompHausCoherentTopologyConstantSheaf : ∀ (R : Type (u + 1)) [inst : Ring R],
  (CategoryTheory.constantSheaf (CategoryTheory.coherentTopology CompHaus) (ModuleCat R)).Full
-- Mathlib.Computability.Primrec.Basic
Nat.Primrec.casesOn' : ∀ {f g : ℕ → ℕ},
  Nat.Primrec f → Nat.Primrec g → Nat.Primrec (Nat.unpaired fun z n => Nat.casesOn n (f z) fun y => g (Nat.pair z y))
-- Mathlib.Data.Int.Bitwise
Int.ldiff.eq_1 : ∀ (m n : ℕ), (Int.ofNat m).ldiff (Int.ofNat n) = ↑(m.ldiff n)
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.Adjunction.mapCommGrp_unit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.CartesianMonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (a : F ⊣ G) [inst_6 : F.Braided]
  [inst_7 : G.Braided],
  a.mapCommGrp.unit =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.mapCommGrpIdIso.inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.mapCommGrpNatTrans a.unit)
        CategoryTheory.Functor.mapCommGrpCompIso.hom)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey_eq_iff_mem_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {he : t.isEmpty = false} {km : α}, t.minKey he = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkCoyonedaEquiv_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X Y : Cᵒᵖ}
  {P : CategoryTheory.Functor C (Type w)} (f : CategoryTheory.shrinkCoyoneda.{w, v, u}.obj X ⟶ P) (g : Y ⟶ X),
  (CategoryTheory.ConcreteCategory.hom (P.map g.unop)) (CategoryTheory.shrinkCoyonedaEquiv f) =
    CategoryTheory.shrinkCoyonedaEquiv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.shrinkCoyoneda.{w, v, u}.map g) f)
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.smul_singleton : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s : Finset α} (b : β),
  s • {b} = Finset.image (fun x => x • b) s
-- Mathlib.Util.Superscript
/-- The parser `subscript(term)` parses a subscript. Basic usage is:
```
local syntax:arg term:max subscript(term) : term
local macro_rules | `($a:term $i:subscript) => `($a $i)
```
Given a notation like this, the expression `(a)ᵢ` parses and expands to `a i`. (Either parentheses
or a whitespace as in `a ᵢ` is required, because `aᵢ` is considered as an identifier.)

Note that because of Unicode limitations, not many characters can actually be typed inside the
subscript, so this should not be used for complex expressions. Legal subscript characters:
```
₀₁₂₃₄₅₆₇₈₉ₐₑₕᵢⱼₖₗₘₙₒₚᵣₛₜᵤᵥₓᴀʙᴄᴅᴇꜰɢʜɪᴊᴋʟᴍɴᴏᴘꞯʀꜱᴛᴜᴠᴡʏᴢᵦᵧᵨᵩᵪ₊₋₌₍₎
```
 -/
Mathlib.Tactic.subscript : Lean.Parser.Parser → Lean.Parser.Parser
-- Init.Grind.Interactive
Lean.Parser.Tactic.Grind.«grind_filterGen<=_» : Lean.ParserDescr
-- Mathlib.Order.CompleteLattice.PiLex
Pi.Lex.sInf_apply_le : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → CompleteLinearOrder (α i)]
  [inst_2 : WellFoundedLT ι] {s : Set (Lex ((i : ι) → (fun i => α i) i))} {i : ι}
  {e : Lex ((i : ι) → (fun i => α i) i)}, e ∈ s → (∀ j < i, e j = sInf s j) → sInf s i ≤ e i
-- Mathlib.Data.Fintype.EquivFin
Infinite.instNontrivial : ∀ (α : Type u_4) [Infinite α], Nontrivial α
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithBot.instInfSet : {α : Type u_1} → [LE α] → [InfSet α] → InfSet (WithBot α)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.isComplete_ker : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₂ : Type u_6}
  [inst_2 : TopologicalSpace M₂] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R₂ M₂] {M' : Type u_9}
  [inst_5 : UniformSpace M'] [CompleteSpace M'] [inst_7 : AddCommMonoid M'] [inst_8 : Module R₁ M'] [T1Space M₂]
  (f : M' →SL[σ₁₂] M₂), IsComplete ↑(↑f).ker
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftEq_hom_app_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ : CategoryTheory.Functor A T} [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso] (l l' : L₁ ⟶ L₂) (h : l = l')
  (hl :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
      P (CategoryTheory.CategoryStruct.comp (l.app X.left) X.hom))
  (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapLeftEq R l l' h hl).hom.app X).left =
    CategoryTheory.CategoryStruct.id X.left
-- Std.Do.PostCond
/-- The “shape” of the postconditions that are used to reason about a monad.

A postcondition shape is an abstraction of many possible monadic effects, based on the structure of pure functions that can simulate them. The postcondition shape of a monad is given by its `WP` instance. This shape is used to determine both its `Assertion`s and its `PostCond`s.
 -/
Std.Do.PostShape : Type (u + 1)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
LinearOrderedCommGroupWithZero.toCommGroupWithZero : {α : Type u_3} → [self : LinearOrderedCommGroupWithZero α] → CommGroupWithZero α
-- Init.Data.Option.Basic
/-- Converts an optional value to a list with zero or one element.

Examples:
* `(some "value").toList = ["value"]`
* `none.toList = []`
 -/
Option.toList : {α : Type u_1} → Option α → List α
-- Mathlib.Analysis.Matrix.Order
/-- For `A` positive semidefinite, we have `x⋆ A x = 0` iff `A x = 0` (linear maps version).  -/
Matrix.PosSemidef.toLinearMap₂'_zero_iff : ∀ {𝕜 : Type u_1} {n : Type u_2} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : Matrix n n 𝕜},
  A.PosSemidef → ∀ (x : n → 𝕜), (((Matrix.toLinearMap₂' 𝕜) A) (star x)) x = 0 ↔ A.mulVec x = 0
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.lift_openEmbedding.congr_simp : ∀ {X : Type u_7} {X' : Type u_8} {Z : Type u_9} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace X']
  [inst_2 : TopologicalSpace Z] [inst_3 : Nonempty Z] {f f_1 : X → X'} (e_f : f = f_1)
  (e e_1 : OpenPartialHomeomorph X Z),
  e = e_1 → ∀ (hf : Topology.IsOpenEmbedding f), e.lift_openEmbedding hf = e_1.lift_openEmbedding ⋯
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.SimpleFunc.setToSimpleFunc_add : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (T : Set α → E →L[ℝ] F),
  MeasureTheory.FinMeasAdditive μ T →
    ∀ {f g : MeasureTheory.SimpleFunc α E},
      MeasureTheory.Integrable (⇑f) μ →
        MeasureTheory.Integrable (⇑g) μ →
          MeasureTheory.SimpleFunc.setToSimpleFunc T (f + g) =
            MeasureTheory.SimpleFunc.setToSimpleFunc T f + MeasureTheory.SimpleFunc.setToSimpleFunc T g
-- Init.Data.Int.DivMod.Lemmas
Int.mul_emod_mul_of_pos : ∀ {a : ℤ} (b c : ℤ), 0 < a → a * b % (a * c) = a * (b % c)
-- Mathlib.RingTheory.MvPolynomial
MvPolynomial.quotient_mk_comp_C_injective : ∀ (σ : Type u) (K : Type v) [inst : Field K] (I : Ideal (MvPolynomial σ K)),
  I ≠ ⊤ → Function.Injective ⇑((Ideal.Quotient.mk I).comp MvPolynomial.C)
-- Mathlib.Algebra.Ring.Subring.Basic
RingHom.eq_of_eqOn_set_dense : ∀ {R : Type u} [inst : NonAssocRing R] {S : Type v} [inst_1 : Semiring S] {s : Set R},
  Subring.closure s = ⊤ → ∀ {f g : R →+* S}, Set.EqOn (⇑f) (⇑g) s → f = g
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {B : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
        {T : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} T] →
            {L : CategoryTheory.Functor A T} →
              {R : CategoryTheory.Functor B T} →
                {P : CategoryTheory.MorphismProperty T} →
                  {Q : CategoryTheory.MorphismProperty A} →
                    {W : CategoryTheory.MorphismProperty B} →
                      {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} →
                        X.Hom Y → CategoryTheory.CommaMorphism X.toComma Y.toComma
-- Mathlib.Order.IsNormal
/-- If `f : α → α`, we can infer one of the hypotheses in
`exists_map_le_lt_map_succ_of_exists_ge`.  -/
Order.IsNormal.exists_map_le_lt_map_succ : ∀ {α : Type u_1} [inst : LinearOrder α] [WellFoundedLT α] [inst_2 : SuccOrder α] [NoMaxOrder α] [inst_4 : OrderBot α]
  {f : α → α} {x : α}, Order.IsNormal f → f ⊥ ≤ x → ∃ a, f a ≤ x ∧ x < f (Order.succ a)
-- Lean.Attributes
Lean.ensureAttrDeclIsMeta : Lean.Name → Lean.Name → Lean.AttributeKind → Lean.AttrM Unit
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_X_add_one_pow : ∀ (R : Type u_1) [inst : Semiring R] (n k : ℕ), ((Polynomial.X + 1) ^ n).coeff k = ↑(n.choose k)
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
/-- The integral of `ω` along `[a -[ℝ] b]`, as a function of `b`, has derivative `ω a` at `b = a`.
This is a `HasFDerivWithinAt` version assuming that `ω` is continuous within a convex set `s`
in a neighborhood of `a` within `s`.  -/
HasFDerivWithinAt.curveIntegral_segment_source' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F]
  [CompleteSpace F] {a : E} {s : Set E} {ω : E → E →L[𝕜] F},
  Convex ℝ s →
    (∀ᶠ (x : E) in nhdsWithin a s, ContinuousWithinAt ω s x) →
      a ∈ s → HasFDerivWithinAt (fun x => ∫ᶜ (x : E) in Path.segment a x, ω x) (ω a) s a
-- Init.Data.List.Sublist
List.isSuffixOf_replicate : ∀ {α : Type u_1} [inst : BEq α] {l : List α} {n : ℕ} {a : α},
  l.isSuffixOf (List.replicate n a) = (decide (l.length ≤ n) && l.all fun x => x == a)
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.nndist_eq : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  {f g : BoundedContinuousFunction α β}, nndist f g = sInf {C | ∀ (x : α), nndist (f x) (g x) ≤ C}
-- Mathlib.NumberTheory.LegendreSymbol.Basic
/-- The value of the Legendre symbol at `-a` is `χ₄ p` times the value at `a`.  -/
legendreSym.at_neg : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)], p ≠ 2 → ∀ (a : ℤ), legendreSym p (-a) = ZMod.χ₄ ↑p * legendreSym p a
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.δ_δ₀Iter' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  (i : Fin (n + 2)) (j : ℕ) {m : ℕ} (i' : Fin (m + 2))
  (h : autoParam (n + j = m) CategoryTheory.SimplicialObject.δ_δ₀Iter'._auto_1),
  autoParam (↑i' = ↑i + j) CategoryTheory.SimplicialObject.δ_δ₀Iter'._auto_3 →
    CategoryTheory.CategoryStruct.comp (X.δ i') (X.δ₀Iter j ⋯) =
      CategoryTheory.CategoryStruct.comp (X.δ₀Iter j ⋯) (X.δ i)
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- Addition `y ↦ y + x` as an `IsometryEquiv`.  -/
IsometryEquiv.addRight : {G : Type v} → [inst : AddGroup G] → [inst_1 : PseudoEMetricSpace G] → [IsIsometricVAdd Gᵃᵒᵖ G] → G → G ≃ᵢ G
-- Mathlib.CategoryTheory.Widesubcategory
CategoryTheory.WideSubcategory.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {_P : CategoryTheory.MorphismProperty C} → [inst_1 : _P.IsMultiplicative] → C → CategoryTheory.WideSubcategory _P
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
WittVector.RecursionMain.succNthDefiningPoly.eq_1 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : CommRing k] [inst_1 : CharP k p] (n : ℕ)
  (a₁ a₂ : WittVector p k) (bs : Fin (n + 1) → k),
  WittVector.RecursionMain.succNthDefiningPoly p n a₁ a₂ bs =
    Polynomial.X ^ p * Polynomial.C (a₁.coeff 0 ^ p ^ (n + 1)) -
        Polynomial.X * Polynomial.C (a₂.coeff 0 ^ p ^ (n + 1)) +
      Polynomial.C
        (a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
              WittVector.nthRemainder p n (fun v => bs v ^ p) (WittVector.truncateFun (n + 1) a₁) -
            a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) -
          WittVector.nthRemainder p n bs (WittVector.truncateFun (n + 1) a₂))
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_erase_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  (t.erase k).getKey? k = none