mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.BigOperators.Group.Finset.Sigma
/-- The sum over a sigma type equals the sum of the fiberwise sums. For rewriting
in the reverse direction, use `Finset.sum_sigma`  -/
Finset.sum_sigma' : ∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] {σ : α → Type u_6} (s : Finset α) (t : (a : α) → Finset (σ a))
  (f : (a : α) → σ a → β), ∑ a ∈ s, ∑ s ∈ t a, f a s = ∑ x ∈ s.sigma t, f x.fst x.snd
-- Mathlib.CategoryTheory.Abelian.Refinements
CategoryTheory.ShortComplex.exact_iff_exact_up_to_refinements : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C),
  S.Exact ↔
    ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂),
      CategoryTheory.CategoryStruct.comp x₂ S.g = 0 →
        ∃ A' π,
          ∃ (_ : CategoryTheory.Epi π),
            ∃ x₁, CategoryTheory.CategoryStruct.comp π x₂ = CategoryTheory.CategoryStruct.comp x₁ S.f
-- Mathlib.Algebra.Ring.Hom.Defs
RingHomClass.toMonoidWithZeroHomClass : ∀ {F : Type u_5} {α : outParam (Type u_6)} {β : outParam (Type u_7)} [inst : NonAssocSemiring α]
  [inst_1 : NonAssocSemiring β] [inst_2 : FunLike F α β] [self : RingHomClass F α β], MonoidWithZeroHomClass F α β
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.isSplitMono_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (s : S.Splitting), CategoryTheory.IsSplitMono S.f
-- Mathlib.RingTheory.Ideal.Pointwise
Ideal.smul_bot : ∀ {M : Type u_1} {R : Type u_3} [inst : Monoid M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] (a : M),
  a • ⊥ = ⊥
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.ext : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R]
  (A B : Matrix.SpecialLinearGroup n R), (∀ (i j : n), ↑A i j = ↑B i j) → A = B
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.domExtend_source : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  {s : Set B} (e : Bundle.Pretrivialization F fun z => proj ↑z) [inst_2 : Nonempty (Z → F)],
  e.domExtend.source = Subtype.val '' e.source
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.isWeightedHomogeneous_of_isEmpty : ∀ (R : Type u_1) {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] [IsEmpty σ]
  (w : σ → M) (f : MvPolynomial σ R), MvPolynomial.IsWeightedHomogeneous w f 0
-- Mathlib.Analysis.Normed.Group.Constructions
/-- Product of normed groups, using the sup norm.  -/
Prod.normedAddGroup : {E : Type u_2} → {F : Type u_3} → [NormedAddGroup E] → [NormedAddGroup F] → NormedAddGroup (E × F)
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution'.mk.inj : ∀ {K : Type u_1} {inst : Field K} {ζ : K} {hζ : IsPrimitiveRoot ζ 3} {a b c : NumberField.RingOfIntegers K}
  {u : (NumberField.RingOfIntegers K)ˣ} {ha : ¬hζ.toInteger - 1 ∣ a} {hb : ¬hζ.toInteger - 1 ∣ b} {hc : c ≠ 0}
  {coprime : IsCoprime a b} {hcdvd : hζ.toInteger - 1 ∣ c} {H : a ^ 3 + b ^ 3 = ↑u * c ^ 3}
  {a_1 b_1 c_1 : NumberField.RingOfIntegers K} {u_1 : (NumberField.RingOfIntegers K)ˣ} {ha_1 : ¬hζ.toInteger - 1 ∣ a_1}
  {hb_1 : ¬hζ.toInteger - 1 ∣ b_1} {hc_1 : c_1 ≠ 0} {coprime_1 : IsCoprime a_1 b_1} {hcdvd_1 : hζ.toInteger - 1 ∣ c_1}
  {H_1 : a_1 ^ 3 + b_1 ^ 3 = ↑u_1 * c_1 ^ 3},
  { a := a, b := b, c := c, u := u, ha := ha, hb := hb, hc := hc, coprime := coprime, hcdvd := hcdvd, H := H } =
      { a := a_1, b := b_1, c := c_1, u := u_1, ha := ha_1, hb := hb_1, hc := hc_1, coprime := coprime_1,
        hcdvd := hcdvd_1, H := H_1 } →
    a = a_1 ∧ b = b_1 ∧ c = c_1 ∧ u = u_1
-- Mathlib.GroupTheory.Order.Min
Monoid.minOrder_eq_top_iff : ∀ {G : Type u_1} [inst : CommGroup G], Monoid.minOrder G = ⊤ ↔ IsMulTorsionFree G
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.toCycle.eq_1 : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (f : Equiv.Perm α) (hf : f.IsCycle),
  f.toCycle hf =
    Finset.univ.val.recOn (Quot.mk ⇑(List.IsRotated.setoid α) []) (fun x x_1 l => if f x = x then l else ↑(f.toList x))
      ⋯
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.all_toList : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α]
  {p : (a : α) → β a → Bool}, m.WF → (m.toList.all fun x => p x.fst x.snd) = m.all p
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueD_eq_fallback : ∀ {α : Type u} {β : Type v} [inst : BEq α] {l : List ((_ : α) × β)} {a : α} {fallback : β},
  Std.Internal.List.containsKey a l = false → Std.Internal.List.getValueD a l fallback = fallback
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocIso_hom_naturality : ∀ {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}
  [self : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {c₁ c₂ c₃ c₄ : C} {d₁ d₂ : D} (f : c₁ ⟶ c₂)
  (g : c₃ ⟶ c₄) (h : d₁ ⟶ d₂),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom
        (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) h)
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c₂ c₄ d₂).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c₁ c₃ d₁).hom
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom g h))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_congr : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {a b : α} {fallback : β},
      compare a b = Ordering.eq →
        Std.DTreeMap.Internal.Impl.Const.getD t a fallback = Std.DTreeMap.Internal.Impl.Const.getD t b fallback
-- Batteries.Data.List.Lemmas
/-- **Alias** of `List.getElem?_set_of_lt'`. -/
List.get?_set_of_lt' : ∀ {α : Type u_1} (a : α) {m n : ℕ} (l : List α), m < l.length → (l.set m a)[n]? = if m = n then some a else l[n]?
-- Lean.Data.OpenDecl
/-- Data for representing `open` commands  -/
Lean.OpenDecl : Type
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.matchAt?_eq_matchAt?_beq : ∀ {c : Char} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.matchAt? c pos = String.Slice.Pattern.Model.matchAt? (fun x => x == c) pos
-- Mathlib.Analysis.Fourier.AddCircle
fourierCoeff.const_smul : ∀ {T : ℝ} [hT : Fact (0 < T)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E]
  (f : AddCircle T → E) (c : ℂ) (n : ℤ), fourierCoeff (c • f) n = c • fourierCoeff f n
-- Mathlib.Topology.MetricSpace.IsometricSMul
nndist_vadd : ∀ {M : Type u} {X : Type w} [inst : PseudoMetricSpace X] [inst_1 : VAdd M X] [IsIsometricVAdd M X] (c : M) (x y : X),
  nndist (c +ᵥ x) (c +ᵥ y) = nndist x y
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
StrictAnti.mul_const_of_neg : ∀ {R : Type u} {α : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] {a : R} [inst_2 : Preorder α] {f : α → R}
  [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R],
  StrictAnti f → a < 0 → StrictMono fun x => f x * a
-- Lean.Meta.Tactic.Grind.Intro
_private.Lean.Meta.Tactic.Grind.Intro.0.Lean.Meta.Grind.IntroResult.done.sizeOf_spec : ∀ (goal : Lean.Meta.Grind.Goal), sizeOf (Lean.Meta.Grind.IntroResult.done✝ goal) = 1 + sizeOf goal
-- Std.Internal.Do.Order.Basic
/-- Pointwise characterization of `⊤` on a function lattice.  -/
Lean.Order.top_apply : ∀ {σ : Type v} {β : Type w} [inst : Lean.Order.CompleteLattice β] (s : σ), Lean.Order.top s = Lean.Order.top
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
IsContMDiffRiemannianBundle.mk : ∀ {EB : Type u_1} [inst : NormedAddCommGroup EB] [inst_1 : NormedSpace ℝ EB] {HB : Type u_2}
  [inst_2 : TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞} {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],
  (∃ g,
      (ContMDiff IB (IB.prod (modelWithCornersSelf ℝ (F →L[ℝ] F →L[ℝ] ℝ))) n fun b => ⟨b, g b⟩) ∧
        ∀ (x : B) (v w : E x), inner ℝ v w = ((g x) v) w) →
    IsContMDiffRiemannianBundle IB n F E
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.ae_eq_comp' : ∀ {α : Type u_2} {β : Type u_3} {δ : Type u_4} {m0 : MeasurableSpace α} [inst : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → β} {g g' : β → δ},
  AEMeasurable f μ → g =ᵐ[ν] g' → (MeasureTheory.Measure.map f μ).AbsolutelyContinuous ν → g ∘ f =ᵐ[μ] g' ∘ f
-- Mathlib.Order.Filter.AtTopBot.Tendsto
Filter.tendsto_atTop_of_monotone_of_subseq : ∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [inst : Preorder ι] [inst_1 : Preorder α] {u : ι → α} {φ : ι' → ι},
  Monotone u →
    ∀ {l : Filter ι'} [l.NeBot], Filter.Tendsto (u ∘ φ) l Filter.atTop → Filter.Tendsto u Filter.atTop Filter.atTop
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
HopfAlgCat.toBialgHom_id : ∀ {R : Type u} [inst : CommRing R] {M : HopfAlgCat R},
  HopfAlgCat.Hom.toBialgHom (CategoryTheory.CategoryStruct.id M) = BialgHom.id R M.carrier
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.conj_conj_symm : ∀ {R₁' : Type u_12} {R₂' : Type u_13} {M₁' : Type u_20} {M₂' : Type u_21} [inst : CommSemiring R₁']
  [inst_1 : CommSemiring R₂'] [inst_2 : AddCommMonoid M₁'] [inst_3 : AddCommMonoid M₂'] [inst_4 : Module R₁' M₁']
  [inst_5 : Module R₂' M₂'] {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} [inst_6 : RingHomInvPair σ₁'₂' σ₂'₁']
  [inst_7 : RingHomInvPair σ₂'₁' σ₁'₂'] (e : M₁' ≃ₛₗ[σ₁'₂'] M₂') (f : Module.End R₂' M₂'), e.conj (e.symm.conj f) = f
-- Init.System.IO
IO.instOrdTaskState : Ord IO.TaskState
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerve.edgeMk_edge : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {x y : C} (f : x ⟶ y),
  (CategoryTheory.nerve.edgeMk f).edge = CategoryTheory.ComposableArrows.mk₁ f
-- Mathlib.Computability.Encoding
Computability.Γ'.bit.inj : ∀ {b b_1 : Bool}, Computability.Γ'.bit b = Computability.Γ'.bit b_1 → b = b_1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, (t₁ ∩ t₂).getKey! k = if k ∈ t₂ then t₁.getKey! k else default
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasPosAssignment.eq_2 : Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg.hasPosAssignment = false
-- Mathlib.Order.Interval.Finset.Defs
WithBot.Ico_bot_coe : ∀ (α : Type u_1) [inst : PartialOrder α] [inst_1 : OrderBot α] [inst_2 : LocallyFiniteOrder α] (a : α),
  Finset.Ico ⊥ ↑a = Finset.insertNone (Finset.Iio a)
-- Mathlib.Algebra.Group.Prod
subAddMonoidHom_apply : ∀ {α : Type u_6} [inst : SubtractionCommMonoid α] (a : α × α), subAddMonoidHom a = a.1 - a.2
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.of_apply : ∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] {G : ι → Type w} [inst_1 : (i : ι) → L.Structure (G i)]
  {f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)} [inst_2 : IsDirectedOrder ι]
  [inst_3 : DirectedSystem G fun i j h => ⇑(f i j h)] [inst_4 : Nonempty ι] {i : ι} {x : G i},
  (FirstOrder.Language.DirectLimit.of L ι G f i) x = ⟦FirstOrder.Language.Structure.Sigma.mk f i x⟧
-- Mathlib.Order.Irreducible
/-- **Alias** of the reverse direction of `supPrime_toDual`. -/
InfPrime.dual : ∀ {α : Type u_2} [inst : SemilatticeInf α] {a : α}, InfPrime a → SupPrime (OrderDual.toDual a)
-- Mathlib.Analysis.InnerProductSpace.Completion
SeparationQuotient.instInnerProductSpace : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] → [InnerProductSpace 𝕜 E] → InnerProductSpace 𝕜 (SeparationQuotient E)
-- Mathlib.LinearAlgebra.Dimension.Free
/-- **Alias** of `Module.nonempty_linearEquiv_iff_rank_eq`.

---

Two vector spaces are isomorphic if and only if they have the same dimension.  -/
LinearEquiv.nonempty_equiv_iff_rank_eq : ∀ {R : Type u} {M M₁ : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  [inst_4 : AddCommMonoid M₁] [inst_5 : Module R M₁] [Module.Free R M₁] [StrongRankCondition R],
  Nonempty (M ≃ₗ[R] M₁) ↔ Module.rank R M = Module.rank R M₁
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
IsAbsoluteValue.abv_eq_zero : ∀ {S : Type u_5} [inst : Semiring S] [inst_1 : PartialOrder S] {R : Type u_6} [inst_2 : Semiring R] (abv : R → S)
  [IsAbsoluteValue abv] {x : R}, abv x = 0 ↔ x = 0
-- Init.Data.Array.Attach
Array.mem_pmap_of_mem : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {xs : Array α} {H : ∀ a ∈ xs, p a} {a : α}
  (h : a ∈ xs), f a ⋯ ∈ Array.pmap f xs H
-- Mathlib.Logic.Relation
Std.Symm.flip_eq : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Symm r], flip r = r
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.shortAddLongRoot_eq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N)
  [inst_5 : P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R],
  RootPairing.EmbeddedG2.shortAddLongRoot P = RootPairing.EmbeddedG2.shortRoot P + RootPairing.EmbeddedG2.longRoot P
-- Init.Data.Array.Lemmas
Array.replace_replicate_self : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {n : ℕ} {b a : α},
  0 < n → (Array.replicate n a).replace a b = #[b] ++ Array.replicate (n - 1) a
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
Std.Iter.toArray_dropWhile_of_finite : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {P : β → Bool} [Std.Iterators.Finite α Id] {it : Std.Iter β},
  (Std.Iter.dropWhile P it).toArray = (List.dropWhile P it.toList).toArray
-- Mathlib.Algebra.Order.Hom.Ring
OrderIsoClass.toOrderIso.congr_simp : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] [inst_2 : EquivLike F α β]
  [inst_3 : OrderIsoClass F α β] (f f_1 : F), f = f_1 → ↑f = ↑f_1
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.exp_units_conj : ∀ {𝔸 : Type u_1} [inst : NormedRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] (y : 𝔸ˣ) (x : 𝔸),
  NormedSpace.exp (↑y * x * ↑y⁻¹) = ↑y * NormedSpace.exp x * ↑y⁻¹
-- Mathlib.Order.Atoms
IsCoatom.sup_eq_top_of_ne : ∀ {α : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderTop α] {a b : α}, IsCoatom a → IsCoatom b → a ≠ b → a ⊔ b = ⊤
-- Mathlib.CategoryTheory.Limits.Shapes.End
/-- Given `F : Jᵒᵖ ⥤ J ⥤ C`, this is the inclusion `(F.obj (op j)).obj j ⟶ coend F`
for any `j : J`.  -/
CategoryTheory.Limits.coend.ι : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) →
          [inst_2 : CategoryTheory.Limits.HasCoend F] →
            (j : J) → (F.obj (Opposite.op j)).obj j ⟶ CategoryTheory.Limits.coend F
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeOfConeLeftOp.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cone F.leftOp),
  CategoryTheory.Limits.coconeOfConeLeftOp c = { pt := Opposite.op c.pt, ι := CategoryTheory.NatTrans.removeLeftOp c.π }
-- Mathlib.Analysis.Complex.Exponential
_private.Mathlib.Analysis.Complex.Exponential.0.Nat.factorial.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.Data.Real.ConjExponents
Real.HolderConjugate.one_sub_inv_inv : ∀ {a : ℝ}, 0 < a → a < 1 → (1 - a)⁻¹.HolderConjugate a⁻¹
-- Mathlib.SetTheory.ZFC.PSet
PSet.mk : (α : Type u) → (α → PSet.{u}) → PSet.{u}
-- Mathlib.Order.Monotone.Basic
/-- An antitone function `f : ℕ → ℕ` which is constant after stabilising for the first time,
stabilises in at most `f 0` steps.

Compared to `WellFoundedLT.antitone_chain_condition`, this lemma requires the extra hypothesis
`hfstab` and only applies to `ℕ`-valued functions, but in return it gives an explicit bound on the
stabilisation index.  -/
Nat.stabilises_of_antitone : ∀ {f : ℕ → ℕ},
  Antitone f → (∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) → ∃ n ≤ f 0, ∀ (m : ℕ), n ≤ m → f m = f n
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functor_galoisConnection : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (X : C),
  GaloisConnection (CategoryTheory.Sieve.functorPushforward F) (CategoryTheory.Sieve.functorPullback F)
-- Mathlib.CategoryTheory.Functor.Trifunctor
CategoryTheory.bifunctorComp₂₃Functor_obj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)),
  CategoryTheory.bifunctorComp₂₃Functor.obj F = CategoryTheory.bifunctorComp₂₃FunctorObj F
-- Lean.Data.FuzzyMatching
_private.Lean.Data.FuzzyMatching.0.Lean.FuzzyMatching.iterateLookaround : {α : Type u_1} → (Option Char → Char → Option Char → α) → String → Array α
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.sequenceΨ.eq_1 : ∀ {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) (f₁₂ : i ⟶ k)
  (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (f₂₃ : j ⟶ l)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁),
  X.sequenceΨ f₁ f₂ f₃ f₁₂ h₁₂ f₂₃ h₂₃ n₀ n₁ hn₁ =
    CategoryTheory.ComposableArrows.mk₃
      (X.cyclesMap f₁₂ f₃ f₂ f₃ (CategoryTheory.ComposableArrows.threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀)
      (X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁)
      (X.opcyclesMap f₁ f₂ f₁ f₂₃ (CategoryTheory.ComposableArrows.threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁)
-- Init.Data.UInt.Bitwise
instLawfulCommIdentityUInt16HOrOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 ||| x2) 0
-- Init.Data.UInt.Lemmas
USize.toUInt8_mul : ∀ (a b : USize), (a * b).toUInt8 = a.toUInt8 * b.toUInt8
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.get_eq_getValueCast : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {m : Std.DHashMap.Internal.Raw₀ α β} (hm : Std.DHashMap.Internal.Raw.WFImp ↑m) {a : α} {h : m.contains a = true},
  m.get a h = Std.Internal.List.getValueCast a (Std.DHashMap.Internal.toListModel (↑m).buckets) ⋯
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
/-- Category structure on the lax natural transformations between lax functors.

Note that this is a scoped instance in the `Lax.LaxTrans` namespace.  -/
CategoryTheory.Lax.LaxTrans.homCategory : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} → CategoryTheory.Category.{max u₁ w₂, max (max (max u₁ v₁) v₂) w₂} (F ⟶ G)
-- Init.Data.ByteArray.Lemmas
ByteArray.size_set! : ∀ (data : ByteArray) (i : ℕ) (v : UInt8), (data.set! i v).size = data.size
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
AlgebraicGeometry.Scheme.Hom.dense_smoothLocus_of_perfectField : ∀ {X : AlgebraicGeometry.Scheme} {K : Type u} [inst : Field K] [PerfectField K] [AlgebraicGeometry.IsReduced X]
  (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [inst_3 : AlgebraicGeometry.LocallyOfFinitePresentation f],
  Dense ↑(AlgebraicGeometry.Scheme.Hom.smoothLocus f)
-- Mathlib.Algebra.Homology.Homotopy
prevD.eq_1 : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (j : ι),
  prevD j = AddMonoidHom.mk' (fun f => CategoryTheory.CategoryStruct.comp (f j (c.prev j)) (D.d (c.prev j) j)) ⋯
-- Mathlib.Topology.UnitInterval
Set.Icc.le_convexComb : ∀ {a b : ℝ} {x y : ↑(Set.Icc a b)}, x ≤ y → ∀ (t : ↑unitInterval), x ≤ Set.Icc.convexComb x y t
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofFVarAliasInfo : Lean.Elab.FVarAliasInfo → Lean.Elab.Info
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₂ → (t₁ ∪ t₂).getKey? k = t₁.getKey? k
-- Mathlib.Topology.LocallyConstant.Basic
/-- A variant of `LocallyConstant.piecewise` where the two closed sets cover a subset.

TODO: Generalise this construction to `ContinuousMap`.  -/
LocallyConstant.piecewise' : {X : Type u_1} →
  {Z : Type u_3} →
    [inst : TopologicalSpace X] →
      {C₀ C₁ C₂ : Set X} →
        C₀ ⊆ C₁ ∪ C₂ →
          IsClosed C₁ →
            IsClosed C₂ →
              (f₁ : LocallyConstant (↑C₁) Z) →
                (f₂ : LocallyConstant (↑C₂) Z) →
                  [DecidablePred fun x => x ∈ C₁] →
                    (∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩) → LocallyConstant (↑C₀) Z
-- Init.Data.String.Lemmas.Basic
String.Slice.ext : ∀ {s t : String.Slice} (h : s.str = t.str),
  s.startInclusive.cast h = t.startInclusive → s.endExclusive.cast h = t.endExclusive → s = t
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Syntax location of recursive call  -/
Lean.Elab.WF.GuessLex.RecCallWithContext.ref : Lean.Elab.WF.GuessLex.RecCallWithContext → Lean.Syntax
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap α (fun x => Unit) cmp} {l : List α} {k : α}
  {h' : k ∈ Std.DTreeMap.Const.insertManyIfNewUnit t l},
  Std.DTreeMap.Const.get (Std.DTreeMap.Const.insertManyIfNewUnit t l) k h' = ()
-- Batteries.Data.List.Basic
List.foldrIdx_eq_foldrIdxTR : @List.foldrIdx = @List.foldrIdxTR
-- Init.Data.ToString.Extra
instToStringInt : ToString ℤ
-- Mathlib.Computability.TuringMachine.Computable
Turing.inhabitedTM2ComputableInTime : Inhabited (Turing.TM2ComputableInTime Computability.encodeBool Computability.encodeBool id)
-- Mathlib.CategoryTheory.Monoidal.Action.End
/-- Functor evaluation gives a right action of `C ⥤ C`.

Note that in the literature, this is defined as a left action, but mathlib's
monoidal structure on `C ⥤ C` is the monoidal opposite of the one usually
considered in the literature.  -/
CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.MonoidalCategory.MonoidalRightAction (CategoryTheory.Functor C C) C
-- Std.Do.Internal.Ensures.Def
/-- The bind-faithful equation: binding `x` and projecting agrees with binding `y`.  -/
Std.Do.Internal.ErasesTo.bind_eq : ∀ {α : Type u} {m : Type u → Type v} [inst : Bind m] {P : α → Prop} {x : m { b // P b }} {y : m α},
  Std.Do.Internal.ErasesTo x y →
    ∀ {β : Type u} (k : α → m β),
      (do
          let a ← x
          k ↑a) =
        y >>= k
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.cliqueSet_mono : ∀ {α : Type u_1} {G H : SimpleGraph α} {n : ℕ}, G ≤ H → G.cliqueSet n ⊆ H.cliqueSet n
-- Mathlib.RingTheory.Smooth.AdicCompletion
DoubleQuot.quotQuotEquivQuotOfLE.congr_simp : ∀ {R : Type u} [inst : CommRing R] {I J : Ideal R} (h : I ≤ J),
  DoubleQuot.quotQuotEquivQuotOfLE h = DoubleQuot.quotQuotEquivQuotOfLE h