mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.IsometricSMul
nndist_neg_neg : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoMetricSpace G] [IsIsometricVAdd G G] [IsIsometricVAdd Gᵃᵒᵖ G]
  (a b : G), nndist (-a) (-b) = nndist a b
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k k' : α} {v : β},
  Array.find? (fun a => a.1 == k) (Std.DHashMap.Const.toArray m) = some (k', v) ↔
    m.getKey? k = some k' ∧ Std.DHashMap.Const.get? m k = some v
-- Mathlib.CategoryTheory.Localization.Trifunctor
/-- The natural isomorphism `F₁' ≅ F₂'` of trifunctors induced by a
natural isomorphism `e : F₁ ≅ F₂` when `Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁'`
and `Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂'` hold.  -/
CategoryTheory.Localization.lift₃NatIso : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {D₁ : Type u_6} →
        {D₂ : Type u_7} →
          {D₃ : Type u_8} →
            {E : Type u_13} →
              [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_6} D₁] →
                      [inst_4 : CategoryTheory.Category.{v_5, u_7} D₂] →
                        [inst_5 : CategoryTheory.Category.{v_6, u_8} D₃] →
                          [inst_6 : CategoryTheory.Category.{v_13, u_13} E] →
                            (L₁ : CategoryTheory.Functor C₁ D₁) →
                              (L₂ : CategoryTheory.Functor C₂ D₂) →
                                (L₃ : CategoryTheory.Functor C₃ D₃) →
                                  (W₁ : CategoryTheory.MorphismProperty C₁) →
                                    (W₂ : CategoryTheory.MorphismProperty C₂) →
                                      (W₃ : CategoryTheory.MorphismProperty C₃) →
                                        [L₁.IsLocalization W₁] →
                                          [L₂.IsLocalization W₂] →
                                            [L₃.IsLocalization W₃] →
                                              [W₁.ContainsIdentities] →
                                                [W₂.ContainsIdentities] →
                                                  [W₃.ContainsIdentities] →
                                                    (F₁ F₂ :
                                                        CategoryTheory.Functor C₁
                                                          (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) →
                                                      (F₁' F₂' :
                                                          CategoryTheory.Functor D₁
                                                            (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) →
                                                        [CategoryTheory.Localization.Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₁
                                                              F₁'] →
                                                          [CategoryTheory.Localization.Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₂
                                                                F₂'] →
                                                            (F₁ ≅ F₂) → (F₁' ≅ F₂')
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearMap.transvection.comp_of_left_eq_apply : ∀ {R : Type u_1} {V : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid V] [inst_2 : Module R V]
  {f : Module.Dual R V} {v w x : V},
  f w = 0 → (LinearMap.transvection f v) ((LinearMap.transvection f w) x) = (LinearMap.transvection f (v + w)) x
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.ShouldCanonResult.canonInst.sizeOf_spec : sizeOf Lean.Meta.Sym.Canon.ShouldCanonResult.canonInst✝ = 1
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Max α] [inst_1 : Bot α] [inst_2 : Max β] [inst_3 : Bot β]
  [inst_4 : Max γ] [inst_5 : Bot γ] (f : SupBotHom β γ) (g : SupBotHom α β) (a : α), (f.comp g) a = f (g a)
-- Mathlib.Algebra.Colimit.Ring
Ring.DirectLimit.lift_of' : ∀ {ι : Type u_1} [inst : Preorder ι] {G : ι → Type u_2} [inst_1 : (i : ι) → CommRing (G i)]
  {f : (i j : ι) → i ≤ j → G i → G j},
  Ring.DirectLimit.lift G f (Ring.DirectLimit G f) (Ring.DirectLimit.of G f) ⋯ = RingHom.id (Ring.DirectLimit G f)
-- Mathlib.Analysis.Complex.CoveringMap
Polynomial.isCoveringMapOn_eval : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [ProperSpace 𝕜] (p : Polynomial 𝕜),
  IsCoveringMapOn (fun x => Polynomial.eval x p)
    ((fun x => Polynomial.eval x p) '' {k | Polynomial.eval k (Polynomial.derivative p) = 0})ᶜ
-- Mathlib.Analysis.Asymptotics.SpecificAsymptotics
/-- If `f : 𝕜 → E` is bounded in a punctured neighborhood of `a`, then `f(x) = o((x - a)⁻¹)` as
`x → a`, `x ≠ a`.  -/
Filter.IsBoundedUnder.isLittleO_sub_self_inv : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : Norm E] {a : 𝕜} {f : 𝕜 → E},
  Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (nhdsWithin a {a}ᶜ) (norm ∘ f) →
    f =o[nhdsWithin a {a}ᶜ] fun x => (x - a)⁻¹
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.selfLeftAction_actionHomRight : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (x x_1 x_2 : C) (f : x_1 ⟶ x_2),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight x f =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft x f
-- Mathlib.NumberTheory.ModularForms.LFunction
ModularForm.weakFEPair_g₀ : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1}
  [inst_1 : FunLike F UpperHalfPlane ℂ] (f : F) [inst_2 : ModularFormClass F Γ k],
  (ModularForm.weakFEPair hk f).g₀ =
    UpperHalfPlane.valueAtInfty
      ⇑(ModularForm.translate f
          (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S)))
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.RightUnitorBimod.inv_hom_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C] {R S : CategoryTheory.Mon C} (P : Bimod R S),
  CategoryTheory.CategoryStruct.comp (Bimod.RightUnitorBimod.inv P) (Bimod.RightUnitorBimod.hom P) =
    CategoryTheory.CategoryStruct.id P.X
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
MonCat.FilteredColimits.M.mk_surjective : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat)
  (m : MonCat.FilteredColimits.M F), ∃ j x, MonCat.FilteredColimits.M.mk F ⟨j, x⟩ = m
-- Mathlib.Order.Heyting.Basic
sdiff_sdiff_left : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, (a \ b) \ c = a \ (b ⊔ c)
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.mk.inj : ∀ {R : Type u_1} {inst : CommRing R} {I : Ideal R} {M : Type u_3} {inst_1 : AddCommGroup M} {inst_2 : Module R M}
  {N : ℕ → Submodule R M} {mono : ∀ (i : ℕ), N (i + 1) ≤ N i} {smul_le : ∀ (i : ℕ), I • N i ≤ N (i + 1)}
  {N_1 : ℕ → Submodule R M} {mono_1 : ∀ (i : ℕ), N_1 (i + 1) ≤ N_1 i} {smul_le_1 : ∀ (i : ℕ), I • N_1 i ≤ N_1 (i + 1)},
  { N := N, mono := mono, smul_le := smul_le } = { N := N_1, mono := mono_1, smul_le := smul_le_1 } → N = N_1
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.IsLeftKanExtension.mk : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  {F' : CategoryTheory.Functor D H} {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  {α : F ⟶ L.comp F'},
  Nonempty (CategoryTheory.StructuredArrow.IsUniversal (CategoryTheory.Functor.LeftExtension.mk F' α)) →
    F'.IsLeftKanExtension α
-- Init.Data.List.Scan.Lemmas
List.scanrM_reverse : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} {as : List α} [inst : Monad m] [LawfulMonad m]
  {f : α → β → m β}, List.scanrM f init as.reverse = List.reverse <$> List.scanlM (flip f) init as
-- Init.Data.UInt.Lemmas
UInt32.toFin_sub : ∀ (a b : UInt32), (a - b).toFin = a.toFin - b.toFin
-- Mathlib.NumberTheory.PythagoreanTriples
/-- A Pythagorean triple `x, y, z` is “classified” if there exist integers `k, m, n` such that
either
* `x = k * (m ^ 2 - n ^ 2)` and `y = k * (2 * m * n)`, or
* `x = k * (2 * m * n)` and `y = k * (m ^ 2 - n ^ 2)`.  -/
PythagoreanTriple.IsClassified : {x y z : ℤ} → PythagoreanTriple x y z → Prop
-- Mathlib.Order.SuccPred.Archimedean
/-- If `a ≤ b` then one can get to `a` from `b` by iterating `succ`  -/
IsSuccArchimedean.exists_succ_iterate_of_le : ∀ {α : Type u_3} {inst : Preorder α} {inst_1 : SuccOrder α} [self : IsSuccArchimedean α] {a b : α},
  a ≤ b → ∃ n, Order.succ^[n] a = b
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
/-- A version of `conditionallyCompleteLatticeOfsInf` when we already know that `α` is a lattice.

This should only be used when it is both hard and unnecessary to provide `sSup` explicitly.  -/
conditionallyCompleteLatticeOfLatticeOfsInf : (α : Type u_5) →
  [H1 : Lattice α] →
    [inst : InfSet α] → (∀ (s : Set α), BddBelow s → s.Nonempty → IsGLB s (sInf s)) → ConditionallyCompleteLattice α
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
LowerSemicontinuous.measurable : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α]
  [inst : TopologicalSpace δ] [OpensMeasurableSpace δ] {f : δ → α}, LowerSemicontinuous f → Measurable f
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
Mathlib.Tactic.Monoidal.Context.mk.sizeOf_spec : ∀ (level₂ level₁ : Lean.Level) (C : Q(Type level₁)) (instCat : Q(CategoryTheory.Category.{level₂, level₁} «$C»))
  (instMonoidal? : Option Q(CategoryTheory.MonoidalCategory «$C»)),
  sizeOf { level₂ := level₂, level₁ := level₁, C := C, instCat := instCat, instMonoidal? := instMonoidal? } =
    1 + sizeOf level₂ + sizeOf level₁ + sizeOf C + sizeOf instCat + sizeOf instMonoidal?
-- Mathlib.Data.Fin.Fin2
/-- Use type class inference to infer the boundedness proof, so that we can directly convert a
`Nat` into a `Fin2 n`. This supports notation like `&1 : Fin 3`.  -/
Fin2.ofNat' : {n : ℕ} → (m : ℕ) → [Fin2.IsLT m n] → Fin2 n
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.addHaar_parallelepiped : ∀ {ι : Type u_2} {G : Type u_3} [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : NormedAddCommGroup G]
  [inst_3 : NormedSpace ℝ G] [inst_4 : MeasurableSpace G] [inst_5 : BorelSpace G] (b : Module.Basis ι ℝ G) (v : ι → G),
  b.addHaar (parallelepiped v) = ENNReal.ofReal |b.det v|
-- Mathlib.Algebra.Homology.ShortComplex.ShortExact
CategoryTheory.ShortComplex.shortExact_iff_op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C), S.ShortExact ↔ S.op.ShortExact
-- Mathlib.Algebra.Homology.TotalComplexShift
HomologicalComplex₂.totalShift₁XIso.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [inst_2 : K.HasTotal (ComplexShape.up ℤ)]
  (n n' : ℤ) (h : n + x = n'), K.totalShift₁XIso x n n' h = K.totalShift₁XIso x n n' h
-- Lean.Widget.InteractiveGoal
Lean.Widget.instRpcEncodableInteractiveGoal : Lean.Server.RpcEncodable Lean.Widget.InteractiveGoal
-- Mathlib.Algebra.Order.Group.Abs
abs_eq_neg_self : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {a : G}, |a| = -a ↔ a ≤ 0
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Set.toFinset_add : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] (s t : Set α) [inst_2 : Fintype ↑s] [inst_3 : Fintype ↑t]
  [inst_4 : Fintype ↑(s + t)], (s + t).toFinset = s.toFinset + t.toFinset
-- Mathlib.Analysis.InnerProductSpace.LinearMap
InnerProductSpace.norm_rankOne : ∀ {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (x : E) (y : F),
  ‖((InnerProductSpace.rankOne 𝕜) x) y‖ = ‖x‖ * ‖y‖
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanDeclIdent.mk : Lean.Name → Lean.Name → Lean.Lsp.LeanDeclIdent
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
inv_mabs_le_inv : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α] [MulLeftMono α] (a : α), |a|ₘ⁻¹ ≤ a⁻¹
-- Mathlib.Order.Interval.Set.WithBotTop
WithBot.range_coe : ∀ {α : Type u_1} [inst : Preorder α], Set.range WithBot.some = Set.Ioi ⊥
-- Init.System.FilePath
System.FilePath.mk.inj : ∀ {toString toString_1 : String}, { toString := toString } = { toString := toString_1 } → toString = toString_1
-- Mathlib.CategoryTheory.Subobject.FactorThru
CategoryTheory.Subobject.factors_left_of_factors_add : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  {P : CategoryTheory.Subobject Y} (f g : X ⟶ Y), P.Factors (f + g) → P.Factors g → P.Factors f
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.enum_zero_eq_bot : ∀ {o : Ordinal.{u_1}} (ho : 0 < o),
  (Ordinal.enum fun x1 x2 => x1 < x2) ⟨0, ⋯⟩ =
    have H := Ordinal.toTypeOrderBot ⋯;
    ⊥
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The sup of the directions of two nonempty affine subspaces with empty intersection is less than
the direction of their sup.  -/
AffineSubspace.sup_direction_lt_of_nonempty_of_inter_empty : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {s₁ s₂ : AffineSubspace k P},
  (↑s₁).Nonempty → (↑s₂).Nonempty → ↑s₁ ∩ ↑s₂ = ∅ → s₁.direction ⊔ s₂.direction < (s₁ ⊔ s₂).direction
-- Mathlib.GroupTheory.Schreier
card_dvd_exponent_pow_rank' : ∀ (G : Type u_1) [inst : CommGroup G] [inst_1 : Group.FG G] {n : ℕ},
  (∀ (g : G), g ^ n = 1) → Nat.card G ∣ n ^ Group.rank G
-- Mathlib.FieldTheory.IsPerfectClosure
IsPRadical.pow_mem' : ∀ {K : Type u_1} {L : Type u_2} {inst : CommSemiring K} {inst_1 : CommSemiring L} {i : K →+* L} {p : ℕ}
  [self : IsPRadical i p] (x : L), ∃ n y, i y = x ^ p ^ n
-- Mathlib.Algebra.Group.Basic
sub_nsmul : ∀ {G : Type u_3} [inst : AddGroup G] (a : G) {m n : ℕ}, n ≤ m → (m - n) • a = m • a + -(n • a)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.forIn_eq_forIn_toArray : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {δ : Type w} {m' : Type w → Type w'} {β : Type v}
  {m : Std.DHashMap.Raw α fun x => β} [inst_2 : Monad m'] [LawfulMonad m'] {f : α → β → δ → m' (ForInStep δ)}
  {init : δ},
  m.WF → Std.DHashMap.Raw.forIn f init m = forIn (Std.DHashMap.Raw.Const.toArray m) init fun a b => f a.1 a.2 b
-- Aesop.Script.StructureDynamic
Aesop.Script.DynStructureM.Context.mk.inj : ∀ {steps steps_1 : Lean.PHashMap Lean.MVarId (ℕ × Aesop.Script.Step)},
  { steps := steps } = { steps := steps_1 } → steps = steps_1
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.of_mul_eq_one : ∀ {M : Type u_1} [inst : Monoid M] [IsDedekindFiniteMonoid M] {a : M} (b : M), a * b = 1 → IsUnit a
-- Mathlib.Algebra.BigOperators.Finprod
/-- A set `s` is nonempty if the sum of some function over `s` is not equal to `0`.  -/
nonempty_of_finsum_mem_ne_zero : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {s : Set α},
  ∑ᶠ (i : α) (_ : i ∈ s), f i ≠ 0 → s.Nonempty
-- Mathlib.Probability.Process.Adapted
MeasureTheory.stronglyAdapted_const' : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {β : ι → Type u_3}
  [inst_1 : (i : ι) → TopologicalSpace (β i)] (f : MeasureTheory.Filtration ι m) (x : (i : ι) → β i),
  MeasureTheory.StronglyAdapted f fun i x_1 => x i
-- Lean.Meta.DiscrTree.Main
Lean.Meta.DiscrTree.Key.arity : Lean.Meta.DiscrTree.Key → ℕ
-- Mathlib.Data.List.Infix
List.IsPrefix.flatMap : ∀ {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α},
  l₁ <+: l₂ → ∀ (f : α → List β), List.flatMap f l₁ <+: List.flatMap f l₂
-- Init.Internal.Order.Basic
Lean.Order.csup_le : ∀ {α : Sort u} [inst : Lean.Order.CCPO α] {x : α} {c : α → Prop} (hc : Lean.Order.chain c),
  (∀ (y : α), c y → Lean.Order.PartialOrder.rel y x) → Lean.Order.PartialOrder.rel (Lean.Order.CCPO.csup hc) x
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.coreToInt.sizeOf_spec : ∀ (a b toIntThm : Lean.Expr) (lhs rhs : Int.Internal.Linear.Expr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.coreToInt a b toIntThm lhs rhs) =
    1 + sizeOf a + sizeOf b + sizeOf toIntThm + sizeOf lhs + sizeOf rhs
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- Specialization of `Finset.prod_bij` that automatically fills in most arguments.

See `Fintype.prod_bijective` for the version where `s` and `t` are `univ`.  -/
Finset.prod_bijective : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : CommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M}
  {g : κ → M} (e : ι → κ),
  Function.Bijective e → (∀ (i : ι), i ∈ s ↔ e i ∈ t) → (∀ i ∈ s, f i = g (e i)) → ∏ i ∈ s, f i = ∏ i ∈ t, g i
-- Mathlib.Algebra.Ring.GeomSum
geom_sum_succ : ∀ {R : Type u_1} [inst : Semiring R] {x : R} {n : ℕ},
  ∑ i ∈ Finset.range (n + 1), x ^ i = x * ∑ i ∈ Finset.range n, x ^ i + 1
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.below.left_distrib : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R]
  {motive : (a a_1 : FreeAlgebra.Pre R X) → FreeAlgebra.Rel R X a a_1 → Prop} {a b c : FreeAlgebra.Pre R X},
  FreeAlgebra.Rel.below ⋯
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctor.comp_obj : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {D : Type u₃}
  [inst_2 : CategoryTheory.Bicategory D] (F : CategoryTheory.StrictlyUnitaryLaxFunctor B C)
  (G : CategoryTheory.StrictlyUnitaryLaxFunctor C D) (X : B), (F.comp G).obj X = G.obj (F.obj X)
-- Mathlib.Topology.Constructions
Filter.Tendsto.finSnoc : ∀ {Y : Type v} {n : ℕ} {A : Fin (n + 1) → Type u_9} [inst : (i : Fin (n + 1)) → TopologicalSpace (A i)]
  {f : Y → (j : Fin n) → A j.castSucc} {g : Y → A (Fin.last n)} {l : Filter Y} {x : (j : Fin n) → A j.castSucc}
  {y : A (Fin.last n)},
  Filter.Tendsto f l (nhds x) →
    Filter.Tendsto g l (nhds y) → Filter.Tendsto (fun a => Fin.snoc (f a) (g a)) l (nhds (Fin.snoc x y))
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.zpow'_mul : ∀ {α : Type u_1} [inst : GroupWithZero α] (a : α) (m n : ℤ),
  Mathlib.Tactic.FieldSimp.zpow' a (m * n) = Mathlib.Tactic.FieldSimp.zpow' (Mathlib.Tactic.FieldSimp.zpow' a m) n
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.isEmpty_filter_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {f : α → β → Bool},
  (Std.DTreeMap.filter f t).isEmpty = true ↔
    ∀ (k : α) (h : k ∈ t), f (t.getKey k h) (Std.DTreeMap.Const.get t k h) = false
-- Mathlib.Order.Hom.BoundedLattice
instCoeTCSupBotHomOfSupBotHomClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Max α] →
          [inst_2 : Max β] → [inst_3 : Bot α] → [inst_4 : Bot β] → [SupBotHomClass F α β] → CoeTC F (SupBotHom α β)
-- Mathlib.Logic.Embedding.Basic
/-- If `α₁ ≃ α₂` and `β₁ ≃ β₂`, then the type of embeddings `α₁ ↪ β₁`
is equivalent to the type of embeddings `α₂ ↪ β₂`.  -/
Equiv.embeddingCongr : {α : Sort u_1} → {β : Sort u_2} → {γ : Sort u_3} → {δ : Sort u_4} → α ≃ β → γ ≃ δ → (α ↪ γ) ≃ (β ↪ δ)
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteResidueField.mk_ratCast : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] (q : ℚ),
  ArchimedeanClass.FiniteResidueField.mk ↑q = ↑q
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.cancelAux.eq_4 : ∀ (r₁ r₂ : Nat.Internal.Linear.Poly) (fuel_2 k₁ : ℕ) (v₁ : Nat.Internal.Linear.Var)
  (m₁_2 : List (ℕ × Nat.Internal.Linear.Var)) (k₂ : ℕ) (v₂ : Nat.Internal.Linear.Var)
  (m₂_2 : List (ℕ × Nat.Internal.Linear.Var)),
  Nat.Internal.Linear.Poly.cancelAux fuel_2.succ ((k₁, v₁) :: m₁_2) ((k₂, v₂) :: m₂_2) r₁ r₂ =
    bif Nat.blt v₁ v₂ then Nat.Internal.Linear.Poly.cancelAux fuel_2 m₁_2 ((k₂, v₂) :: m₂_2) ((k₁, v₁) :: r₁) r₂
    else
      bif Nat.blt v₂ v₁ then Nat.Internal.Linear.Poly.cancelAux fuel_2 ((k₁, v₁) :: m₁_2) m₂_2 r₁ ((k₂, v₂) :: r₂)
      else
        bif k₁.blt k₂ then Nat.Internal.Linear.Poly.cancelAux fuel_2 m₁_2 m₂_2 r₁ ((k₂.sub k₁, v₁) :: r₂)
        else
          bif k₂.blt k₁ then Nat.Internal.Linear.Poly.cancelAux fuel_2 m₁_2 m₂_2 ((k₁.sub k₂, v₁) :: r₁) r₂
          else Nat.Internal.Linear.Poly.cancelAux fuel_2 m₁_2 m₂_2 r₁ r₂
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsExistential.brecOn : ∀ {L : FirstOrder.Language} {α : Type u'} {motive : {n : ℕ} → (a : L.BoundedFormula α n) → a.IsExistential → Prop}
  {n : ℕ} {a : L.BoundedFormula α n} (t : a.IsExistential),
  (∀ {n : ℕ} (a : L.BoundedFormula α n) (t : a.IsExistential),
      FirstOrder.Language.BoundedFormula.IsExistential.below t → motive a t) →
    motive a t
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubringClass.subtype_injective : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : SetLike S R] [hSR : NonUnitalSubringClass S R]
  (s : S), Function.Injective ⇑(NonUnitalSubringClass.subtype s)
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.addGroupSeminormClass : ∀ {E : Type u_3} [inst : AddGroup E], AddGroupSeminormClass (AddGroupSeminorm E) E ℝ
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.isoClosure_isoClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C),
  P.isoClosure.isoClosure = P.isoClosure
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
TensorProduct.finsuppLeft_smul' : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {N : Type u_4}
  [inst_7 : AddCommMonoid N] [inst_8 : Module R N] {ι : Type u_5} [inst_9 : DecidableEq ι] (s : S)
  (t : TensorProduct R (ι →₀ M) N),
  (TensorProduct.finsuppLeft R S M N ι) (s • t) = s • (TensorProduct.finsuppLeft R S M N ι) t
-- Mathlib.Topology.Category.CompHaus.Projective
CompHaus.projective_ultrafilter : ∀ (X : Type u_1), CategoryTheory.Projective (CompHaus.of (Ultrafilter X))
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_laxMonoidalToMon_obj_one : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (F : CategoryTheory.Mon C),
  CategoryTheory.MonObj.one =
    CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (CategoryTheory.CategoryStruct.id F.X)
-- Mathlib.Order.Minimal
Minimal.le : ∀ {α : Type u_2} {P : α → Prop} {x y : α} [inst : LinearOrder α], Minimal P x → P y → x ≤ y
-- Mathlib.ModelTheory.Syntax
/-- The sentence indicating that a basic relation symbol is transitive.  -/
FirstOrder.Language.Relations.transitive : {L : FirstOrder.Language} → L.Relations 2 → L.Sentence
-- Batteries.Classes.Order
Std.TransCmp.gt_of_gt_of_ge : ∀ {α : Type u_1} {cmp : α → α → Ordering} [Std.TransCmp cmp] {x y z : α},
  cmp x y = Ordering.gt → cmp y z ≠ Ordering.lt → cmp x z = Ordering.gt
-- Mathlib.Algebra.Order.Group.Opposite
AddOpposite.nonneg_unop : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] {a : αᵃᵒᵖ}, 0 ≤ AddOpposite.unop a ↔ 0 ≤ a