mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
/-- The section `cotangentCompAwaySec` is indeed a section of the canonical map `J/J² → K/K²`.  -/
Algebra.Generators.map_comp_cotangentCompAwaySec : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (g : S) [inst_7 : IsLocalization.Away g T] (P : Algebra.Generators R S ι)
  {x : ((Algebra.Generators.localizationAway T g).comp P).toExtension.Cotangent},
  (Algebra.Extension.Cotangent.map ((Algebra.Generators.localizationAway T g).ofComp P).toExtensionHom) x =
      Algebra.Generators.cMulXSubOneCotangent T g →
    Algebra.Extension.Cotangent.map ((Algebra.Generators.localizationAway T g).ofComp P).toExtensionHom ∘ₗ
        Algebra.Generators.cotangentCompAwaySec g P x =
      LinearMap.id
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The first part of the third cosimplicial identity  -/
CategoryTheory.CosimplicialObject.δ_comp_σ_self_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
  {i : Fin (n + 1)} {Z : C} (h : X.obj { len := n } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) (CategoryTheory.CategoryStruct.comp (X.σ i) h) = h
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.pow_smul_mem_closure_smul : ∀ {M : Type u_3} [inst : Monoid M] {N : Type u_7} [inst_1 : CommMonoid N] [inst_2 : MulAction M N] [IsScalarTower M N N]
  (r : M) (s : Set N) {x : N}, x ∈ Submonoid.closure s → ∃ n, r ^ n • x ∈ Submonoid.closure (r • s)
-- Lean.Meta.ProdN
/-- Given expressions `eᵢ`, return the tuple `(e₁, e₂, …, eₙ)` and its type `t₁ × t₂ × … × tₙ`.
For `n = 0`, return `PUnit.unit` with the given level + 1.
 -/
Lean.Meta.mkProdMkN : Array Lean.Expr → Lean.Level → Lean.MetaM (Lean.Expr × Lean.Expr)
-- Lean.Expr
/-- Used for `Type u`, `Sort u`, and `Prop`:
- `Prop` is represented as `.sort .zero`,
- `Sort u` as ``.sort (.param `u)``, and
- `Type u` as ``.sort (.succ (.param `u))``
 -/
Lean.Expr.sort : Lean.Level → Lean.Expr
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_nonneg : ∀ {b x : ℝ}, 1 < b → 1 ≤ x → 0 ≤ Real.logb b x
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.not_isCircuit_nil : ∀ {V : Type u} {G : SimpleGraph V} {u : V}, ¬SimpleGraph.Walk.nil.IsCircuit
-- Mathlib.Order.Filter.Partial
Filter.PTendsto.eq_1 : ∀ {α : Type u} {β : Type v} (f : α →. β) (l₁ : Filter α) (l₂ : Filter β),
  Filter.PTendsto f l₁ l₂ = (Filter.pmap f l₁ ≤ l₂)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.of_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y)
  [CategoryTheory.IsIso f], AlgebraicGeometry.SheafedSpace.IsOpenImmersion f
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.map_eq_one_iff : ∀ {β : Type v} {α : Type u_1} {f : α → β} {v : WithTop α} [inst : One β], WithTop.map f v = 1 ↔ ∃ x, v = ↑x ∧ f x = 1
-- Mathlib.RingTheory.SimpleModule.Isotypic
IsIsotypicOfType.of_isSimpleModule : ∀ (R : Type u_2) (M : Type u) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSimpleModule R M],
  IsIsotypicOfType R M M
-- Mathlib.CategoryTheory.Sites.Point.Presheaf
CategoryTheory.GrothendieckTopology.isConservative_pointsBot : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C],
  (CategoryTheory.GrothendieckTopology.pointsBot C).IsConservativeFamilyOfPoints
-- Mathlib.CategoryTheory.Action.Basic
Action.mkIso_hom_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {M N : Action V G}
  (f : M.V ≅ N.V)
  (comm :
    autoParam
      (∀ (g : G), CategoryTheory.CategoryStruct.comp (M.ρ g) f.hom = CategoryTheory.CategoryStruct.comp f.hom (N.ρ g))
      Action.mkIso._auto_1),
  (Action.mkIso f comm).hom.hom = f.hom
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.evalAt_coe : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Monoid G] [inst_7 : ContMDiffMul I (↑⊤) G] (g : G)
  (X : LeftInvariantDerivation I G), (Derivation.evalAt g) ↑X = (LeftInvariantDerivation.evalAt g) X
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_castSuccEmb_uIcc : ∀ {n : ℕ} (i j : Fin n), Finset.map Fin.castSuccEmb (Finset.uIcc i j) = Finset.uIcc i.castSucc j.castSucc
-- Mathlib.Topology.Category.LightProfinite.AsLimit
LightProfinite.proj_comp_transitionMapLE' : ∀ (S : LightProfinite) {n m : ℕ} (h : n ≤ m),
  ⇑(CategoryTheory.ConcreteCategory.hom (S.transitionMapLE h)) ∘ ⇑(CategoryTheory.ConcreteCategory.hom (S.proj m)) =
    ⇑(CategoryTheory.ConcreteCategory.hom (S.proj n))
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_functor_obj_ι_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) [inst_1 : CategoryTheory.Limits.HasCoproduct I.left]
  [inst_2 : CategoryTheory.Limits.HasCoproduct I.right] (K : CategoryTheory.Limits.Multicofork I)
  (X : CategoryTheory.Limits.WalkingParallelPair),
  (I.multicoforkEquivSigmaCofork.functor.obj K).ι.app X =
    CategoryTheory.Limits.WalkingParallelPair.rec
      (CategoryTheory.CategoryStruct.comp
        (I.sndSigmaMapOfIsColimit (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Discrete.functor I.right))
          (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor I.left)))
        (CategoryTheory.Limits.Cofan.IsColimit.desc
          (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor I.right)) K.π))
      (CategoryTheory.Limits.Cofan.IsColimit.desc
        (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor I.right)) K.π)
      X
-- Mathlib.Data.Matrix.Block
/-- `Matrix.blockDiagonal' M` turns `M : Π i, Matrix (m i) (n i) α` into a
`Σ i, m i`-by-`Σ i, n i` block matrix which has the entries of `M` along the diagonal
and zero elsewhere.

This is the dependently-typed version of `Matrix.blockDiagonal`.  -/
Matrix.blockDiagonal' : {o : Type u_4} →
  {m' : o → Type u_7} →
    {n' : o → Type u_8} →
      {α : Type u_12} →
        [DecidableEq o] → [Zero α] → ((i : o) → Matrix (m' i) (n' i) α) → Matrix ((i : o) × m' i) ((i : o) × n' i) α
-- Mathlib.Topology.EMetricSpace.Defs
Subtype.image_eball : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {p : α → Prop} (a : { a // p a }) (r : ENNReal),
  Subtype.val '' Metric.eball a r = Metric.eball (↑a) r ∩ {a | p a}
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
SimplyConnectedSpace.instSubsingletonFundamentalGroup : ∀ {X : Type u_3} [inst : TopologicalSpace X] [SimplyConnectedSpace X] (x : X), Subsingleton (FundamentalGroup X x)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Term.realize.eq_1 : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} (v : α → M) (k : α),
  FirstOrder.Language.Term.realize v (FirstOrder.Language.var k) = v k
-- Init.Data.Sum.Lemmas
_private.Init.Data.Sum.Lemmas.0.Sum.getRight?.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : α ⊕ β → Sort u_3) (b : β) (h_1 : (b : β) → motive (Sum.inr b))
  (h_2 : (val : α) → motive (Sum.inl val)),
  (match Sum.inr b with
    | Sum.inr b => h_1 b
    | Sum.inl val => h_2 val) =
    h_1 b
-- Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
/-- If `p` doesn't divide the exponent of `θ`, then `(ℤ / pℤ)[X] / (minpoly θ) ≃+* 𝓞 K / p(𝓞 K)`.
 -/
RingOfIntegers.ZModXQuotSpanEquivQuotSpan : {K : Type u_1} →
  [inst : Field K] →
    [NumberField K] →
      {θ : NumberField.RingOfIntegers K} →
        {p : ℕ} →
          [inst_2 : Fact (Nat.Prime p)] →
            ¬p ∣ RingOfIntegers.exponent θ →
              Polynomial (ZMod p) ⧸ Ideal.span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)} ≃+*
                NumberField.RingOfIntegers K ⧸ Ideal.span {↑p}
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
linearIndependent_inl_union_inr' : ∀ {ι : Type u'} {ι' : Type u_1} {R : Type u_2} {M : Type u_4} {M' : Type u_5} [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] {v : ι → M}
  {v' : ι' → M'},
  LinearIndependent R v →
    LinearIndependent R v' → LinearIndependent R (Sum.elim (⇑(LinearMap.inl R M M') ∘ v) (⇑(LinearMap.inr R M M') ∘ v'))
-- Mathlib.LinearAlgebra.Dimension.Finite
/-- A (finite-dimensional) space that is a subsingleton has zero `finrank`.  -/
Module.finrank_zero_of_subsingleton : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R]
  [Subsingleton M], Module.finrank R M = 0
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.mk : {α : Type u_2} →
  (toFilter : Filter α) → toFilter.NeBot → (∀ (g : Filter α), g.NeBot → g ≤ toFilter → toFilter ≤ g) → Ultrafilter α
-- Mathlib.Topology.MetricSpace.Completion
Isometry.isometry_mapRingHom : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : Ring α] [inst_2 : IsTopologicalRing α]
  [inst_3 : IsUniformAddGroup α] [inst_4 : Ring β] [inst_5 : PseudoMetricSpace β] [inst_6 : IsUniformAddGroup β]
  [inst_7 : IsTopologicalRing β] {f : α →+* β} (h : Isometry ⇑f), Isometry ⇑h.mapRingHom
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurableSet_range_inr : ∀ {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} [inst : MeasurableSpace α], MeasurableSet (Set.range Sum.inr)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.nhds_basis_closedBall_inv_nat_pos : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α},
  (nhds x).HasBasis (fun n => 0 < n) fun n => Metric.closedBall x (1 / ↑n)
-- Mathlib.LinearAlgebra.DirectSum.TensorProduct
TensorProduct.directSumLeft_symm_of : ∀ (R : Type u) [inst : CommSemiring R] (S : Type u_1) [inst_1 : Semiring S] [inst_2 : Algebra R S] {ι₁ : Type v₁}
  [inst_3 : DecidableEq ι₁] {M₁ : ι₁ → Type w₁} {M₂' : Type w₂'} [inst_4 : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)]
  [inst_5 : AddCommMonoid M₂'] [inst_6 : (i₁ : ι₁) → Module R (M₁ i₁)] [inst_7 : Module R M₂']
  [inst_8 : (i₁ : ι₁) → Module S (M₁ i₁)] [inst_9 : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)] {i : ι₁}
  (x : TensorProduct R (M₁ i) M₂'),
  (TensorProduct.directSumLeft R S M₁ M₂').symm ((DirectSum.of (fun i => TensorProduct R (M₁ i) M₂') i) x) =
    (LinearMap.rTensor M₂' (DirectSum.lof R ι₁ M₁ i)) x
-- Init.Data.Bool
false_eq_decide_iff : ∀ {p : Prop} [h : Decidable p], false = decide p ↔ ¬p
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get_eq_getElem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {a : α} {h : a ∈ t}, t.get a h = t[a]
-- Mathlib.CategoryTheory.Linear.LinearFunctor
CategoryTheory.Functor.linear_of_full_essSurj_comp : ∀ {R : Type u_1} [inst : Semiring R] {C : Type u_2} {D : Type u_3} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Category.{v_2, u_3} D] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : CategoryTheory.Preadditive D] [inst_5 : CategoryTheory.Linear R C] [inst_6 : CategoryTheory.Linear R D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Linear R F] {E : Type u_4}
  [inst_8 : CategoryTheory.Category.{v_3, u_4} E] [inst_9 : CategoryTheory.Preadditive E]
  [inst_10 : CategoryTheory.Linear R E] (G : CategoryTheory.Functor D E) [F.Full] [F.EssSurj]
  [CategoryTheory.Functor.Linear R (F.comp G)], CategoryTheory.Functor.Linear R G
-- Mathlib.Data.Rel
Function.graph_inj : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β}, Function.graph f = Function.graph g ↔ f = g
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
/-- Compact covering of a `σ`-compact topological space as
`MeasureTheory.Measure.FiniteSpanningSetsIn`.  -/
MeasureTheory.Measure.finiteSpanningSetsInCompact : {α : Type u_1} →
  [inst : TopologicalSpace α] →
    [SigmaCompactSpace α] →
      {x : MeasurableSpace α} →
        (μ : MeasureTheory.Measure α) →
          [MeasureTheory.IsLocallyFiniteMeasure μ] → μ.FiniteSpanningSetsIn {K | IsCompact K}
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.sigmaCofan_pt : ∀ {ι : Type v} (α : ι → TopCat), (TopCat.sigmaCofan α).pt = TopCat.of ((i : ι) × ↑(α i))
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {fallback : β k}, k ∉ t₂ → (t₁ ∪ t₂).getD k fallback = t₁.getD k fallback
-- Init.GrindInstances.ToInt
Lean.Grind.instMulInt8SintOfNatNat : Lean.Grind.ToInt.Mul Int8 (Lean.Grind.IntInterval.sint 8)
-- Lean.Server.FileWorker.Utils
/-- A document bundled with processing information. Turned into `EditableDocument` as soon as the
reporter task has been started.
 -/
Lean.Server.FileWorker.EditableDocumentCore : Type
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_right_hom : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D T) (Y : T) (X : D)
  (Y_1 : CategoryTheory.StructuredArrow Y ((CategoryTheory.Under.forget X).comp F)),
  ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse F Y X).obj Y_1).right.hom = Y_1.hom
-- Mathlib.Algebra.Star.Subalgebra
StarAlgHomClass.toStarAlgHom.congr_simp : ∀ {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B]
  [inst_7 : FunLike F A B] [inst_8 : AlgHomClass F R A B] [inst_9 : StarHomClass F A B] (f f_1 : F), f = f_1 → ↑f = ↑f_1
-- Mathlib.Data.Set.Card
Set.sep_of_ncard_eq : ∀ {α : Type u_1} {s : Set α} {a : α} {P : α → Prop},
  {x | x ∈ s ∧ P x}.ncard = s.ncard → a ∈ s → autoParam s.Finite Set.sep_of_ncard_eq._auto_1 → P a
-- Mathlib.CategoryTheory.Sites.Canonical
CategoryTheory.GrothendieckTopology.instFaithfulSheafTypeYoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical], J.yoneda.Faithful
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` reflects limits, then `F.unop : C ⥤ D` reflects colimits.  -/
CategoryTheory.Limits.reflectsColimits_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.ReflectsLimits F],
  CategoryTheory.Limits.ReflectsColimits F.unop
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.instMonoCyclesMapOfF : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K L : HomologicalComplex C c} (φ : K ⟶ L) (i : ι) [inst_2 : K.HasHomology i]
  [inst_3 : L.HasHomology i] [CategoryTheory.Mono (φ.f i)], CategoryTheory.Mono (HomologicalComplex.cyclesMap φ i)
-- Std.Data.ExtTreeSet.Basic
Std.ExtTreeSet.mk.sizeOf_spec : ∀ {α : Type u} {cmp : autoParam (α → α → Ordering) Std.ExtTreeSet._auto_1} [inst : SizeOf α]
  (inner : Std.ExtTreeMap α Unit cmp), sizeOf { inner := inner } = 1 + sizeOf inner
-- Mathlib.Analysis.Analytic.Composition
Composition.length_sigmaCompositionAux : ∀ {n : ℕ} (a : Composition n) (b : Composition a.length) (i : Fin b.length),
  (a.sigmaCompositionAux b ⟨↑i, ⋯⟩).length = b.blocksFun i
-- Mathlib.MeasureTheory.Measure.FiniteMeasureProd
MeasureTheory.FiniteMeasure.zero_prod : ∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_2} [inst_1 : MeasurableSpace β]
  (ν : MeasureTheory.FiniteMeasure β), MeasureTheory.FiniteMeasure.prod 0 ν = 0
-- Mathlib.Algebra.GroupWithZero.ULift
ULift.mulZeroOneClass : {α : Type u} → [MulZeroOneClass α] → MulZeroOneClass (ULift.{u_1, u} α)
-- Mathlib.Analysis.Normed.Algebra.Spectrum
/-- For `𝕜 = ℝ` or `𝕜 = ℂ`, `exp` maps the spectrum of `a` into the spectrum of `exp a`.  -/
spectrum.exp_mem_exp : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A] [CompleteSpace A]
  (a : A) {z : 𝕜}, z ∈ spectrum 𝕜 a → NormedSpace.exp z ∈ spectrum 𝕜 (NormedSpace.exp a)
-- Mathlib.Algebra.FreeMonoid.Basic
/-- A version of `List.casesOn` for `FreeAddMonoid` using `0` and
`FreeAddMonoid.of x + xs` instead of `[]` and `x :: xs`.  -/
FreeAddMonoid.casesOn : {α : Type u_1} →
  {motive : FreeAddMonoid α → Sort u_6} →
    (xs : FreeAddMonoid α) →
      motive 0 → ((x : α) → (xs : FreeAddMonoid α) → motive (FreeAddMonoid.of x + xs)) → motive xs
-- Mathlib.Analysis.Normed.Algebra.GelfandFormula
NormedRing.algEquivComplexOfComplete_symm_apply : ∀ {A : Type u_2} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [inst_2 : CompleteSpace A]
  (hA : ∀ {a : A}, IsUnit a ↔ a ≠ 0) (a : A), (NormedRing.algEquivComplexOfComplete hA).symm a = ⋯.some
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_sub_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y z : E), inner 𝕜 (x - y) z = inner 𝕜 x z - inner 𝕜 y z
-- Std.Http.Data.Method
/-- Submit data to be processed (e.g., form submission).
Source: https://httpwg.org/specs/rfc9110.html#section-9.3.3
 -/
Std.Http.Method.post : Std.Http.Method
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.instHasOfPostcompPropertyOppositeOpOfHasOfPrecompProperty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C)
  {W' : CategoryTheory.MorphismProperty C} [W.HasOfPrecompProperty W'], W.op.HasOfPostcompProperty W'.op
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_erase_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, (m.erase k)[k]? = none
-- Mathlib.RingTheory.OrderOfVanishing.Basic
/-- Zero-preserving monoid homomorphism from a nontrivial commutative ring `R` to `ℤᵐ⁰`.

Note that we cannot just use `fun x ↦ ord R x` without further assumptions on `R`.
This is because if R is finite length, then ord R 0 will be some non-top value,
meaning in this case `0` will not be mapped to `⊤`.
 -/
Ring.ordMonoidWithZeroHom : (R : Type u_1) → [inst : CommRing R] → [Nontrivial R] → R →*₀ WithZero (Multiplicative ℤ)
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.eval_tensorHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {f g h i : C}
  {η η' : f ⟶ g} {θ θ' : h ⟶ i}
  {ι : CategoryTheory.MonoidalCategoryStruct.tensorObj f h ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj g i},
  η = η' →
    θ = θ' →
      CategoryTheory.MonoidalCategoryStruct.tensorHom η' θ' = ι →
        CategoryTheory.MonoidalCategoryStruct.tensorHom η θ = ι
-- Mathlib.Computability.NFA
NFA.mem_evalFrom_iff_nonempty_path : ∀ {α : Type u} {σ : Type v} {M : NFA α σ} {s t : σ} {x : List α}, t ∈ M.evalFrom {s} x ↔ Nonempty (M.Path s t x)
-- Init.Data.SInt.Lemmas
Int8.toFin_toBitVec : ∀ (x : Int8), x.toBitVec.toFin = x.toUInt8.toFin
-- Mathlib.Combinatorics.SimpleGraph.Maps
Equiv.simpleGraph_trans : ∀ {V : Type u_1} {W : Type u_2} {X : Type u_3} (e₁ : V ≃ W) (e₂ : W ≃ X),
  (e₁.trans e₂).simpleGraph = e₁.simpleGraph.trans e₂.simpleGraph
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
InnerProductSpace.gramSchmidt.eq_1 : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι] (f : ι → E)
  (n : ι),
  InnerProductSpace.gramSchmidt 𝕜 f n = f n - ∑ i, (𝕜 ∙ InnerProductSpace.gramSchmidt 𝕜 f ↑i).starProjection (f n)
-- Init.Data.Vector.Lemmas
Vector.mem_empty_iff : ∀ {α : Type u_1} (a : α), a ∈ #v[] ↔ False
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.flip : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z}, CategoryTheory.IsPullback fst snd f g → CategoryTheory.IsPullback snd fst g f
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.Pointed.eq_1 : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] (C : ConvexCone R M), C.Pointed = (0 ∈ C)
-- Std.Time.Time.Unit.Basic
/-- Converts a `Second.Offset` to a `Nanosecond.Offset`.
 -/
Std.Time.Second.Offset.toNanoseconds : Std.Time.Second.Offset → Std.Time.Nanosecond.Offset
-- Mathlib.Algebra.Star.LinearMap
Module.End.mem_eigenspace_intrinsicStar_iff : ∀ {R : Type u_4} {V : Type u_5} [inst : CommRing R] [inst_1 : InvolutiveStar R] [inst_2 : AddCommGroup V]
  [inst_3 : StarAddMonoid V] [inst_4 : Module R V] [inst_5 : StarModule R V] (f : WithConv (Module.End R V)) (α : R)
  (x : V), x ∈ (star f).ofConv.eigenspace α ↔ star x ∈ f.ofConv.eigenspace (star α)
-- Mathlib.GroupTheory.QuotientGroup.Finite
/-- If `F` and `H` are finite such that `ker(G →+ H) ≤ im(F →+ G)`, then `G` is finite.  -/
AddGroup.fintypeOfKerLeRange : {F : Type u_1} →
  {G : Type u_2} →
    {H : Type u_3} →
      [inst : AddGroup F] →
        [inst_1 : AddGroup G] →
          [inst_2 : AddGroup H] → [Fintype F] → [Fintype H] → (f : F →+ G) → (g : G →+ H) → g.ker ≤ f.range → Fintype G
-- Init.Data.BitVec.Bitblast
/-- The number of bits in the numerator that are not yet processed  -/
BitVec.DivModState.wn : {w : ℕ} → BitVec.DivModState w → ℕ
-- Std.Sat.AIG.Basic
Std.Sat.AIG.instHashableDecl.hash : {α : Type} → [Hashable α] → Std.Sat.AIG.Decl α → UInt64
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
Finsupp.DegLex.orderBot : {α : Type u_1} → [inst : LinearOrder α] → OrderBot (DegLex (α →₀ ℕ))
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuouAt_inv_iff : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} {a : α} [inst_1 : PartialOrder β]
  [inst_2 : CommGroup β] [IsOrderedMonoid β], LowerSemicontinuousAt f⁻¹ a ↔ UpperSemicontinuousAt f a
-- Mathlib.Topology.Filter
Filter.tendsto_pure_self : ∀ {X : Type u_4} (l : Filter X), Filter.Tendsto pure l (nhds l)
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.parseLowerHex?.eq_1 : ∀ (s : String) (p : s.Pos) (acc : ℕ), Lean.parseLowerHex?✝ 0 s p acc = some (p, acc)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
AddEquiv.withBotCongr_toEquiv : ∀ {α : Type u} {β : Type v} [inst : Add α] [inst_1 : Add β] (e : α ≃+ β), ↑e.withBotCongr = (↑e).withBotCongr
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- One should usually use `MeasureTheory.Integrable.integrableOn` instead.  -/
MeasureTheory.Integrable.restrict : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_8} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {f : α → ε},
  MeasureTheory.Integrable f μ → ∀ {s : Set α}, MeasureTheory.Integrable f (μ.restrict s)
-- Mathlib.Order.CompleteLattice.Defs
le_sSup_iff_forall_lt : ∀ {α : Type u_1} [inst : CompleteLinearOrder α] {s : Set α} {l : α}, l ≤ sSup s ↔ ∀ b < l, ∃ a ∈ s, b < a
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.toIocMod_toReal : ∀ (θ : Real.Angle), toIocMod Real.two_pi_pos (-Real.pi) θ.toReal = θ.toReal
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.smul_def : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (f : M ≃ₗ[R] M)
  (a : M), f • a = f a