mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Vector.Lemmas
Vector.getElem_flatMap : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {m : ℕ} {xs : Vector α n} {f : α → Vector β m} {i : ℕ} (hi : i < n * m),
  (xs.flatMap f)[i] = (f xs[i / m])[i % m]
-- Mathlib.Data.Nat.Fib.Zeckendorf
Nat.zeckendorf_of_pos : ∀ {n : ℕ}, 0 < n → n.zeckendorf = n.greatestFib :: (n - Nat.fib n.greatestFib).zeckendorf
-- Mathlib.Probability.HasLaw
ProbabilityTheory.hasLaw_congr : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X Y : Ω → 𝓧}
  {μ : MeasureTheory.Measure 𝓧} {P : MeasureTheory.Measure Ω},
  X =ᵐ[P] Y → (ProbabilityTheory.HasLaw X μ P ↔ ProbabilityTheory.HasLaw Y μ P)
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.log_strictMono : StrictMono ENNReal.log
-- Mathlib.AlgebraicGeometry.Sites.Pretopology
/-- The Grothendieck topology on the category of schemes induced by the pretopology defined by
`P`-covers.  -/
AlgebraicGeometry.Scheme.grothendieckTopology : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme → CategoryTheory.GrothendieckTopology AlgebraicGeometry.Scheme
-- Mathlib.Analysis.SpecialFunctions.Sqrt
DifferentiableAt.sqrt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E},
  DifferentiableAt ℝ f x → f x ≠ 0 → DifferentiableAt ℝ (fun y => √(f y)) x
-- Mathlib.LinearAlgebra.Dual.BaseChange
Module.Dual.congr_symm_apply_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {V : Type u_2} [inst_1 : AddCommMonoid V] [inst_2 : Module R V] {W : Type u_3}
  [inst_3 : AddCommMonoid W] [inst_4 : Module R W] (e : V ≃ₗ[R] W) (a : W →ₗ[R] R) (x : V),
  ((Module.Dual.congr e).symm a) x = a (e x)
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.atomic_emb : ∀ (n : ℕ), (OrderedFinpartition.atomic n).emb = fun m x => m
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.succ_le_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.PRange.InfinitelyUpwardEnumerable α] {a b : α},
  Std.PRange.UpwardEnumerable.LE (Std.PRange.succ a) b ↔ Std.PRange.UpwardEnumerable.LT a b
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.throw_MonadExcept : ∀ {m : Type u → Type v} {ε : Type u_1} {α : Type u} {e : ε} {ps : Std.Do.PostShape} {Q : Std.Do.PostCond α ps}
  [inst : MonadExceptOf ε m] [inst_1 : Std.Do.WP m ps], ⦃(Std.Do.wp (MonadExceptOf.throw e)).apply Q⦄ throw e ⦃Q⦄
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
_private.Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum.0.ZMod.χ₄.match_1.eq_1 : ∀ (motive : ZMod 4 → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 2) (h_3 : Unit → motive 1)
  (h_4 : Unit → motive 3),
  (match 0 with
    | 0 => h_1 ()
    | 2 => h_2 ()
    | 1 => h_3 ()
    | 3 => h_4 ()) =
    h_1 ()
-- Mathlib.GroupTheory.OrderOfElement
mem_multiples_iff_mem_zmultiples : ∀ {G : Type u_1} [inst : AddGroup G] {x y : G} [Finite G], y ∈ AddSubmonoid.multiples x ↔ y ∈ AddSubgroup.zmultiples x
-- Mathlib.Data.Multiset.Dedup
Multiset.subset_dedup' : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, s ⊆ t.dedup ↔ s ⊆ t
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normal_in_normalizer : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, (H.addSubgroupOf (AddSubgroup.normalizer ↑H)).Normal
-- Mathlib.RingTheory.Extension.Generators
/-- If `algebraMap R S` is surjective, the empty type generates `S`.  -/
Algebra.Generators.ofSurjectiveAlgebraMap : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] → Function.Surjective ⇑(algebraMap R S) → Algebra.Generators R S PEmpty.{w + 1}
-- Mathlib.LinearAlgebra.Matrix.Invertible
Matrix.transpose_invOf : ∀ {n : Type u_2} {α : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring α] (A : Matrix n n α)
  [inst_3 : Invertible A] [inst_4 : Invertible A.transpose], (⅟A).transpose = ⅟A.transpose
-- Lean.Declaration
/-- Information for reducing a recursor  -/
Lean.RecursorRule : Type
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorAdd'_add_zero_hom_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (a : A) (X : C),
  (CategoryTheory.shiftFunctorAdd' C a 0 a ⋯).hom.app X =
    (CategoryTheory.shiftFunctorZero C A).inv.app ((CategoryTheory.shiftFunctor C a).obj X)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.add_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₁ z₁' : CochainComplex.HomComplex.Cochain F G n₁)
  (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂),
  (z₁ + z₁').comp z₂ h = z₁.comp z₂ h + z₁'.comp z₂ h
-- Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
CategoryTheory.SmallObject.SuccStruct.iterationFunctorObjSuccIso.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) {J : Type w}
  [inst_1 : LinearOrder J] [inst_2 : OrderBot J] [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C] (j : J) (hj : ¬IsMax j),
  Φ.iterationFunctorObjSuccIso j hj = Φ.iterationFunctorObjSuccIso j hj
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.isIso_actionHomRight : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (x : C) {y z : D} (f : y ⟶ z)
  [CategoryTheory.IsIso f],
  CategoryTheory.IsIso (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight x f)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LVal.fieldIdx : Lean.Syntax → ℕ → List Lean.Level → Lean.Elab.Term.LVal
-- Mathlib.Data.UInt
UInt8.toBitVec_natCast : ∀ (n : ℕ), (↑n).toBitVec = ↑n
-- Mathlib.NumberTheory.NumberField.Discriminant.Basic
NumberField.rootDiscr.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], NumberField.rootDiscr K = NumberField.rootDiscr K
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false} {km : α}, t.minKey he = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
_private.Mathlib.RingTheory.Ideal.Norm.RelNorm.0.Ideal.relNorm_map_algEquiv_aux : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] [inst_9 : IsDedekindDomain R] [inst_10 : IsDedekindDomain S] {T : Type u_4}
  [inst_11 : CommRing T] [inst_12 : IsDedekindDomain T] [inst_13 : IsIntegrallyClosed T] [inst_14 : Algebra R T]
  [inst_15 : Module.Finite R T] [inst_16 : Module.IsTorsionFree R T] (σ : S ≃ₐ[R] T) (I : Ideal S),
  (Ideal.relNorm R) (Ideal.map σ I) ≤ (Ideal.relNorm R) I
-- Mathlib.LinearAlgebra.SpecialLinearGroup
/-- The transpose of an element in `SpecialLinearGroup R V`.  -/
SpecialLinearGroup.dualMap : {R : Type u_1} →
  {V : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module R V] →
          [Module.Free R V] → [Module.Finite R V] → SpecialLinearGroup R V → SpecialLinearGroup R (Module.Dual R V)
-- Mathlib.GroupTheory.Perm.Option
Equiv.optionCongr_sign : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (e : Equiv.Perm α),
  Equiv.Perm.sign (Equiv.optionCongr e) = Equiv.Perm.sign e
-- Lean.Util.CollectAxioms
_private.Lean.Util.CollectAxioms.0.Lean.CollectAxioms.State.mk.sizeOf_spec : ∀ (seen : Lean.NameMap (Array Lean.Name)) (axioms : Lean.NameSet),
  sizeOf { seen := seen, axioms := axioms } = 1 + sizeOf seen + sizeOf axioms
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsTangentAt.radius_lt_dist_center : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {as : AffineSubspace ℝ P} {p q : P},
  s.IsTangentAt p as → q ∈ as → q ≠ p → s.radius < dist q s.center
-- Mathlib.Tactic.Zify
/-- A variant of `applySimpResultToProp` that cannot close the goal, but does not need a meta
variable and returns a tuple of a proof and the corresponding simplified proposition.  -/
Mathlib.Tactic.Zify.applySimpResultToProp' : Lean.Expr → Lean.Expr → Lean.Meta.Simp.Result → Lean.MetaM (Lean.Expr × Lean.Expr)
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
GromovHausdorff.candidatesBDist.congr_simp : ∀ (X : Type u) (Y : Type v) [inst : MetricSpace X] [inst_1 : CompactSpace X] [inst_2 : Nonempty X]
  [inst_3 : MetricSpace Y] [inst_4 : CompactSpace Y] [inst_5 : Nonempty Y],
  GromovHausdorff.candidatesBDist X Y = GromovHausdorff.candidatesBDist X Y
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
HomotopyCategory.Pretriangulated.complete_distinguished_triangle_morphism : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C]
  (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ))),
  T₁ ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C →
    T₂ ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C →
      ∀ (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂),
        CategoryTheory.CategoryStruct.comp T₁.mor₁ b = CategoryTheory.CategoryStruct.comp a T₂.mor₁ →
          ∃ c,
            CategoryTheory.CategoryStruct.comp T₁.mor₂ c = CategoryTheory.CategoryStruct.comp b T₂.mor₂ ∧
              CategoryTheory.CategoryStruct.comp T₁.mor₃
                  ((CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map a) =
                CategoryTheory.CategoryStruct.comp c T₂.mor₃
-- Mathlib.Topology.Order.NhdsSet
Iic_mem_nhdsSet_Iic : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b : α},
  a < b → Set.Iic b ∈ nhdsSet (Set.Iic a)
-- Mathlib.RingTheory.GradedAlgebra.RingHom
/-- Composition of graded ring homomorphisms is associative.  -/
GradedRingHom.comp_assoc : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} {σ : Type u_6} {τ : Type u_7}
  {ψ : Type u_8} {ω : Type u_9} [inst : Semiring A] [inst_1 : Semiring B] [inst_2 : Semiring C] [inst_3 : Semiring D]
  [inst_4 : SetLike σ A] [inst_5 : SetLike τ B] [inst_6 : SetLike ψ C] [inst_7 : SetLike ω D] {𝒜 : ι → σ} {ℬ : ι → τ}
  {𝒞 : ι → ψ} {𝒟 : ι → ω} (h : 𝒞 →+*ᵍ 𝒟) (g : ℬ →+*ᵍ 𝒞) (f : 𝒜 →+*ᵍ ℬ), (h.comp g).comp f = h.comp (g.comp f)
-- Init.Data.Range.Polymorphic.UInt
USize.upwardEnumerableLE_ofBitVec : ∀ {x y : BitVec System.Platform.numBits},
  Std.PRange.UpwardEnumerable.LE { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LE x y
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- The supremum of a closed subspace and a finite dimensional subspace is closed.  -/
Submodule.isClosed_sup_finiteDimensional : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] [inst_5 : Module 𝕜 E] [ContinuousSMul 𝕜 E]
  (s t : Submodule 𝕜 E), IsClosed ↑s → ∀ [ht : FiniteDimensional 𝕜 ↥t], IsClosed ↑(s ⊔ t)
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalize'.eq_1 : ∀ (C : Type u),
  CategoryTheory.FreeMonoidalCategory.normalize' C =
    (CategoryTheory.FreeMonoidalCategory.normalize C).comp
      ((CategoryTheory.Functor.whiskeringRight
            ((CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C)
            ((CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C)
            (CategoryTheory.FreeMonoidalCategory C)).obj
        CategoryTheory.FreeMonoidalCategory.inclusion)
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.instAddCommGroup : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      {ι : Type u_4} →
        [inst : Ring R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : AddCommGroup N] →
                  [inst_5 : Module R N] →
                    [inst_6 : TopologicalSpace N] → [IsTopologicalAddGroup N] → AddCommGroup (M [⋀^ι]→L[R] N)
-- Init.Data.UInt.Lemmas
UInt8.lt_iff_le_and_ne : ∀ {a b : UInt8}, a < b ↔ a ≤ b ∧ a ≠ b
-- Init.Data.BitVec.Basic
BitVec.ofBool_append : ∀ {w : ℕ} (msb : Bool) (lsbs : BitVec w), BitVec.ofBool msb ++ lsbs = BitVec.cast ⋯ (BitVec.cons msb lsbs)
-- Mathlib.GroupTheory.SchurZassenhaus
/-- Do not use this lemma: It is made obsolete by `exists_right_complement'_of_coprime`  -/
_private.Mathlib.GroupTheory.SchurZassenhaus.0.Subgroup.SchurZassenhausInduction.step3 : ∀ {G : Type u} [inst : Group G] {N : Subgroup G} [N.Normal],
  (Nat.card ↥N).Coprime N.index →
    (∀ (G' : Type u) [inst : Group G'] [Finite G'],
        Nat.card G' < Nat.card G →
          ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H') →
      (∀ (H : Subgroup G), ¬N.IsComplement' H) →
        ∀ [Finite G] (K : Subgroup ↥N) [(Subgroup.map N.subtype K).Normal], K = ⊥ ∨ K = ⊤
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.pre_map_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {B : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C)
  (G : CategoryTheory.Functor C D) (S : D) {X Y : CategoryTheory.Comma (F.comp G) (CategoryTheory.Functor.fromPUnit S)}
  (f : X ⟶ Y), ((CategoryTheory.CostructuredArrow.pre F G S).map f).left = F.map f.left
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
/-- If a functor preserves coequalizers and the appropriate coproducts, it preserves colimits.  -/
CategoryTheory.Limits.preservesColimit_of_preservesCoequalizers_and_coproduct : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.SmallCategory J]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete J) C]
  [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ((p : J × J) × (p.1 ⟶ p.2))) C]
  [CategoryTheory.Limits.HasCoequalizers C] (G : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair G]
  [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) G]
  [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ((p : J × J) × (p.1 ⟶ p.2))) G],
  CategoryTheory.Limits.PreservesColimitsOfShape J G
-- Lean.Widget.InteractiveCode
Lean.Widget.DiffTag.wasInserted.sizeOf_spec : sizeOf Lean.Widget.DiffTag.wasInserted = 1
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.add_succ : ∀ (o₁ o₂ : Ordinal.{u_1}), o₁ + Order.succ o₂ = Order.succ (o₁ + o₂)
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
instIsContMDiffRiemannianBundleOfNatWithTopENat_1 : ∀ {EB : Type u_1} [inst : NormedAddCommGroup EB] [inst_1 : NormedSpace ℝ EB] {HB : Type u_2}
  [inst_2 : TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {B : Type u_3} [inst_3 : TopologicalSpace B]
  [inst_4 : ChartedSpace HB B] {F : Type u_4} [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace ℝ F]
  {E : B → Type u_5} [inst_7 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_8 : (x : B) → NormedAddCommGroup (E x)]
  [inst_9 : (x : B) → InnerProductSpace ℝ (E x)] [inst_10 : FiberBundle F E] [inst_11 : VectorBundle ℝ F E]
  [IsContMDiffRiemannianBundle IB 2 F E], IsContMDiffRiemannianBundle IB 1 F E
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
Int.reduceBNe : Lean.Meta.Simp.DSimproc
-- Mathlib.Computability.Partrec
Computable.nat_div2 : Computable Nat.div2
-- Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
/-- The values before the squashed position stay the same.  -/
GenContFract.squashGCF_nth_of_lt : ∀ {K : Type u_1} {n : ℕ} {g : GenContFract K} [inst : DivisionRing K] {m : ℕ},
  m < n → (g.squashGCF (n + 1)).s.get? m = g.s.get? m
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.End : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid A] → [inst_2 : Module R A] → [inst_3 : CoalgebraStruct R A] → Monoid (A →ₗc[R] A)
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.helper₅ : ∀ {w : UInt8}, ByteArray.utf8DecodeChar?.parseFirstByte w = ByteArray.utf8DecodeChar?.FirstByte.done → w < 128
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.foldM_filterMapWithPostcondition.match_1.splitter : {γ : Type u_1} →
  (motive : Option γ → Sort u_2) →
    (__x : Option γ) →
      ((c : γ) → motive (some c)) → ((x : Option γ) → (∀ (c : γ), x = some c → False) → motive x) → motive __x
-- Mathlib.Algebra.GroupWithZero.Defs
IsLeftCancelMulZero.mk : ∀ {M₀ : Type u} [inst : Mul M₀] [inst_1 : Zero M₀], (∀ {a : M₀}, a ≠ 0 → IsLeftRegular a) → IsLeftCancelMulZero M₀
-- Mathlib.Topology.ContinuousMap.Basic
Topology.IsQuotientMap.lift_apply : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : C(X, Y)} (hf : Topology.IsQuotientMap ⇑f) (g : C(X, Z))
  (h : Function.FactorsThrough ⇑g ⇑f) (a : Y), (hf.lift g h) a = ((fun i => i.liftOn' ⇑g ⋯) ∘ ⇑hf.homeomorph.symm) a
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Poly.mul'_Nonneg : ∀ (p : Lean.Grind.Linarith.Poly) (k : ℕ), p.NonnegCoeffs → (p.mul' ↑k).NonnegCoeffs
-- Mathlib.Geometry.Euclidean.Sphere.SecondInter
/-- The distance between `secondInter` and the center equals the distance between the original
point and the center.  -/
EuclideanGeometry.Sphere.secondInter_dist : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (s : EuclideanGeometry.Sphere P) (p : P) (v : V),
  dist (s.secondInter p v) s.center = dist p s.center
-- Mathlib.Analysis.SpecialFunctions.NonIntegrable
/-- The function `fun x ↦ x⁻¹` is not integrable on any interval `[a, +∞)`.  -/
not_integrableOn_Ici_inv : ∀ {a : ℝ}, ¬MeasureTheory.IntegrableOn (fun x => x⁻¹) (Set.Ici a) MeasureTheory.volume
-- Std.Http.Data.Status
/-- 410 Gone
 -/
Std.Http.Status.gone : Std.Http.Status
-- Init.Data.UInt.Lemmas
BitVec.ofNatLT_uInt16ToNat : ∀ (n : UInt16), n.toNat#'⋯ = n.toBitVec
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.neg : ∀ {α : Type u_2} [inst : Neg α] {f : Filter α}, f.NeBot → (-f).NeBot
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Cokleisli.of_mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Comonad C) (c : C), { of := c }.of = c
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Arrow.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S : J.Cover X} {x y : S.Arrow}, x = y ↔ x.Y = y.Y ∧ x.f ≍ y.f
-- Mathlib.Algebra.QuadraticAlgebra.Defs
/-- Quadratic algebra over a type with fixed coefficient where $i^2 = a + bi$, implemented as
a structure with two fields, `re` and `im`. When `R` is a commutative ring, this is isomorphic to
`R[X]/(X^2-b*X-a)`.  -/
QuadraticAlgebra : (R : Type u) → R → R → Type u
-- Mathlib.Data.Fintype.Fin
Fin.Ioi_zero_eq_map : ∀ {n : ℕ}, Finset.Ioi 0 = Finset.map (Fin.succEmb n) Finset.univ
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  Module.IsTorsionFree R ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.eraseIdx.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → ℕ → Sort u_2) (head : α) (as : List α) (h_1 : (x : ℕ) → motive [] x)
  (h_2 : (head : α) → (as : List α) → motive (head :: as) 0)
  (h_3 : (a : α) → (as : List α) → (n : ℕ) → motive (a :: as) n.succ),
  (match head :: as, 0 with
    | [], x => h_1 x
    | head :: as, 0 => h_2 head as
    | a :: as, n.succ => h_3 a as n) =
    h_2 head as
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_alter_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {fallback : β k} {f : Option (β k) → Option (β k)}, (m.alter k f).getD k fallback = (f (m.get? k)).getD fallback
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.getEntryGT.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Ord α] (k : α)
  (motive : (x : Std.DTreeMap.Internal.Impl α fun x => β) → x.Ordered → (∃ a ∈ x, compare a k = Ordering.gt) → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl.leaf.Ordered) (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, compare a k = Ordering.gt)
  (h_1 :
    (x : Std.DTreeMap.Internal.Impl.leaf.Ordered) →
      (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, compare a k = Ordering.gt) →
        motive Std.DTreeMap.Internal.Impl.leaf x he)
  (h_2 :
    (size : ℕ) →
      (ky : α) →
        (y : β) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered) →
              (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, compare a k = Ordering.gt) →
                motive (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he),
  (match Std.DTreeMap.Internal.Impl.leaf, x, he with
    | Std.DTreeMap.Internal.Impl.leaf, x, he => h_1 x he
    | Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he => h_2 size ky y l r ho he) =
    h_1 x he
-- Lean.Data.KVMap
Lean.KVMap.insert : Lean.KVMap → Lean.Name → Lean.DataValue → Lean.KVMap
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α fun x => Unit} [EquivBEq α] [LawfulHashable α]
  {l : List α} {k : α}, k ∉ m → l.contains k = false → (Std.DHashMap.Const.insertManyIfNewUnit m l).getKey? k = none
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanLocationLink.mk : Lean.Lsp.LocationLink → Option Lean.Lsp.LeanDeclIdent → Bool → Lean.Lsp.LeanLocationLink
-- Mathlib.Data.List.Permutation
List.permutationsAux.rec.eq_1 : ∀ {α : Type u_1} {C : List α → List α → Sort v} (H0 : (is : List α) → C [] is)
  (H1 : (t : α) → (ts is : List α) → C ts (t :: is) → C is [] → C (t :: ts) is) (x : List α),
  List.permutationsAux.rec H0 H1 [] x = H0 x
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.exists_simpleFunc_forall_lintegral_sub_lt_of_pos : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  ∫⁻ (x : α), f x ∂μ ≠ ⊤ →
    ∀ {ε : ENNReal},
      ε ≠ 0 →
        ∃ φ,
          (∀ (x : α), ↑(φ x) ≤ f x) ∧
            ∀ (ψ : MeasureTheory.SimpleFunc α NNReal),
              (∀ (x : α), ↑(ψ x) ≤ f x) → (MeasureTheory.SimpleFunc.map ENNReal.ofNNReal (ψ - φ)).lintegral μ < ε
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.right_continuous' : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (self : StieltjesFunction R) (x : R),
  ContinuousWithinAt (↑self) (Set.Ici x) x