mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
/-- The edge given by a `1`-simplex.  -/
SSet.Truncated.Edge.mk' : {X : SSet.Truncated 2} →
  (s : X.obj (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.Edge._proof_2 })) →
    SSet.Truncated.Edge
      ((CategoryTheory.ConcreteCategory.hom
          (X.map (SimplexCategory.Truncated.δ₂ 1 SSet.Truncated.Edge._proof_1 SSet.Truncated.Edge._proof_3).op))
        s)
      ((CategoryTheory.ConcreteCategory.hom
          (X.map (SimplexCategory.Truncated.δ₂ 0 SSet.Truncated.Edge._proof_1 SSet.Truncated.Edge._proof_3).op))
        s)
-- Init.Data.Char.Lemmas
Char.notLTAntisymm : Std.Antisymm fun x1 x2 => ¬x1 < x2
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.alter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : t₁.WF) (h₂ : t₂.WF),
  t₁.Equiv t₂ →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      (Std.DTreeMap.Internal.Impl.alter k f t₁ ⋯).impl.Equiv (Std.DTreeMap.Internal.Impl.alter k f t₂ ⋯).impl
-- Mathlib.Topology.UniformSpace.UniformApproximation
/-- If `Fₙ` tends uniformly to `f`, and `gₙ` tends to `x`, then `Fₙ gₙ` tends to `f x`.  -/
TendstoUniformly.tendsto_comp : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {x : α} {p : Filter ι} {g : ι → α},
  TendstoUniformly F f p →
    ContinuousAt f x → Filter.Tendsto g p (nhds x) → Filter.Tendsto (fun n => F n (g n)) p (nhds (f x))
-- Init.Data.Nat.Lemmas
/-- See `exists_lt_succ_right'` for a variant where `p` takes the bound as an argument.  -/
Nat.exists_lt_succ_right : ∀ {n : ℕ} {p : ℕ → Prop}, (∃ m < n + 1, p m) ↔ (∃ m < n, p m) ∨ p n
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformFun.edist_le : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace β] {f g : UniformFun α β} {C : ENNReal},
  edist f g ≤ C ↔ ∀ (x : α), edist (UniformFun.toFun f x) (UniformFun.toFun g x) ≤ C
-- Mathlib.NumberTheory.Height.Basic
Height.mulHeight_ne_zero : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : ι → K),
  Height.mulHeight x ≠ 0
-- Mathlib.Logic.Function.Iterate
Function.iterate_succ : ∀ {α : Type u} (f : α → α) (n : ℕ), f^[n.succ] = f^[n] ∘ f
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : Cᵒᵖ ⥤ D` creates limits, then `F.rightOp : C ⥤ Dᵒᵖ` creates colimits.  -/
CategoryTheory.Limits.createsColimitsOfSizeRightOp : {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.CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] →
            CategoryTheory.CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.rightOp
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.sign_prodCongrRight : ∀ {α : Type u} [inst : DecidableEq α] {β : Type v} [inst_1 : Fintype α] [inst_2 : DecidableEq β] [inst_3 : Fintype β]
  (σ : α → Equiv.Perm β), Equiv.Perm.sign (Equiv.prodCongrRight σ) = ∏ k, Equiv.Perm.sign (σ k)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast_alterKey_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (k : α) (f : Option (β k) → Option (β k))
  (l : List ((a : α) × β a)) (hl : Std.Internal.List.DistinctKeys l)
  (hc : Std.Internal.List.containsKey k (Std.Internal.List.alterKey k f l) = true),
  Std.Internal.List.getValueCast k (Std.Internal.List.alterKey k f l) hc =
    (f (Std.Internal.List.getValueCast? k l)).get ⋯
-- Mathlib.Algebra.Ring.Idempotent
isIdempotentElem_iff_one_sub_mul_self : ∀ {R : Type u_1} [inst : NonAssocRing R] {a : R}, IsIdempotentElem a ↔ (1 - a) * a = 0
-- Init.Data.Option.Lemmas
Option.max_le : ∀ {α : Type u_1} [inst : LE α] [inst_1 : Max α],
  (∀ (x y z : α), x ⊔ y ≤ z ↔ x ≤ z ∧ y ≤ z) → ∀ {a b c : Option α}, a ⊔ b ≤ c ↔ a ≤ c ∧ b ≤ c
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.natDegree_eraseLead_le_of_nextCoeff_eq_zero : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f.nextCoeff = 0 → f.eraseLead.natDegree ≤ f.natDegree - 2
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.instContinuousLineDeriv : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : AddCommGroup F]
  [inst_3 : Module ℂ F] [inst_4 : TopologicalSpace F] [inst_5 : IsTopologicalAddGroup F]
  [inst_6 : ContinuousConstSMul ℂ F], ContinuousLineDeriv E (TemperedDistribution E F) (TemperedDistribution E F)
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.id_apply : ∀ (R : Type u_1) (E₁ : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid E₁] [inst_2 : PartialOrder E₁]
  [inst_3 : Module R E₁] (x : E₁), (PositiveLinearMap.id R E₁) x = x
-- Mathlib.Data.Vector.Basic
List.Vector.get_set_eq_if : ∀ {α : Type u_1} {n : ℕ} {v : List.Vector α n} {i j : Fin n} (a : α), (v.set i a).get j = if i = j then a else v.get j
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.Iterator.Monadic.step.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (next : α) (h_1 : Unit → motive none)
  (h_2 : (next : α) → motive (some next)),
  (match some next with
    | none => h_1 ()
    | some next => h_2 next) =
    h_2 next
-- Mathlib.Analysis.SpecialFunctions.Log.Summable
Complex.multipliable_of_summable_log : ∀ {ι : Type u_1} {f : ι → ℂ}, (Summable fun i => Complex.log (f i)) → Multipliable f
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.allM_pure : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {p : β → Bool},
  Std.Iter.allM (fun x => pure (p x)) it = pure (Std.Iter.all (fun x => p x) it)
-- Lean.DocString.Parser
/-- Parenthesizer for `ifVersoModuleDocs`—parenthesizes according to the underlying parenthesizers.
 -/
Lean.Doc.Parser.ifVersoModuleDocs.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Limits.Final.Connected
CategoryTheory.initial_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  [CategoryTheory.IsConnected C], (CategoryTheory.Prod.snd C D).Initial
-- Std.Http.Data.Status
Std.Http.instBEqCustomStatus.beq : Std.Http.CustomStatus → Std.Http.CustomStatus → Bool
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Bundle.mdifferentiableWithinAt_zeroSection : ∀ (𝕜 : Type u_1) {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E]
  [inst_11 : (x : B) → AddCommMonoid (E x)] [inst_12 : (x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {t : Set B}
  {x : B}, MDiffAt[t] (Bundle.zeroSection F E) x
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.mem_toAddSubgroup : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {s : NonUnitalSubring R} {x : R}, x ∈ s.toAddSubgroup ↔ x ∈ s
-- Mathlib.FieldTheory.JacobsonNoether
/-- If `D` is a purely inseparable extension of `k` with characteristic `p`,
then for every element `a` of `D`, there exists a natural number `n`
such that `a ^ (p ^ n)` is contained in `k`.  -/
JacobsonNoether.exists_pow_mem_center_of_inseparable : ∀ {D : Type u_1} [inst : DivisionRing D] [Algebra.IsAlgebraic (↥(Subring.center D)) D] (p : ℕ) [hchar : ExpChar D p]
  (a : D), (∀ (x : D), IsSeparable (↥(Subring.center D)) x → x ∈ Subring.center D) → ∃ n, a ^ p ^ n ∈ Subring.center D
-- Mathlib.NumberTheory.Fermat
/-- `Fₙ = 2^(2^n)+1` is prime if `3^(2^(2^n-1)) = -1 mod Fₙ` (**Pépin's test**).  -/
Nat.pepin_primality : ∀ (n : ℕ), 3 ^ 2 ^ (2 ^ n - 1) = -1 → Nat.Prime n.fermatNumber
-- Mathlib.Data.Int.ModEq
/-- To cancel a common factor `c` from a `ModEq` we must divide the modulus `m` by `gcd m c`.  -/
Int.ModEq.cancel_right_div_gcd : ∀ {m a b c : ℤ}, 0 < m → a * c ≡ b * c [ZMOD m] → a ≡ b [ZMOD m / ↑(m.gcd c)]
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
/-- The spheres `s₁` and `s₂` are externally tangent at the point `p`.  -/
EuclideanGeometry.Sphere.IsExtTangentAt : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] →
          [NormedAddTorsor V P] → EuclideanGeometry.Sphere P → EuclideanGeometry.Sphere P → P → Prop
-- Mathlib.Logic.Equiv.Sum
Equiv.sumEmpty_apply_inl : ∀ {α : Type u_9} {β : Type u_10} [inst : IsEmpty β] (a : α), (Equiv.sumEmpty α β) (Sum.inl a) = a
-- Init.Data.ByteArray.Basic
ByteArray.forIn.loop : {β : Type v} →
  {m : Type v → Type w} → [Monad m] → (as : ByteArray) → (UInt8 → β → m (ForInStep β)) → (i : ℕ) → i ≤ as.size → β → m β
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.of_toArray_perm : ∀ {α : Type u} {β : α → Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β}, t₁.toArray.Perm t₂.toArray → t₁.Equiv t₂
-- Mathlib.MeasureTheory.Measure.Restrict
mem_map_indicator_ae_iff_of_zero_notMem : ∀ {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → β}
  [inst_1 : Zero β] {t : Set β}, 0 ∉ t → (t ∈ Filter.map (s.indicator f) (MeasureTheory.ae μ) ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.entryAtIdx.match_3.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.Balanced → (x_2 : ℕ) → x_2 < x.size → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α β) →
        (x_1 : x.Balanced) →
          (x_2 : ℕ) →
            (x_3 : x_2 < x.size) →
              ((size : ℕ) →
                  (k : α) →
                    (v : β k) →
                      (l' r' : Std.DTreeMap.Internal.Impl α β) →
                        (hl : (Std.DTreeMap.Internal.Impl.inner size k v l' r').Balanced) →
                          (n : ℕ) →
                            (h : n < (Std.DTreeMap.Internal.Impl.inner size k v l' r').size) →
                              motive (Std.DTreeMap.Internal.Impl.inner size k v l' r') hl n h) →
                motive x x_1 x_2 x_3
-- Init.While
Lean.Loop.mk : Lean.Loop
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the largest key that is less than the given key,
returning `fallback` if no such key exists.
 -/
Std.TreeMap.Raw.getKeyLTD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → α → α
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.toFun_eq_coe : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (f : NormedAddGroupHom V₁ V₂), f.toFun = ⇑f
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.ordConnectedComponent_eq : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} {x y : α},
  Set.uIcc x y ⊆ s → s.ordConnectedComponent x = s.ordConnectedComponent y
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_of_isEmpty : ∀ {α : Type u_1} [IsEmpty α], Nat.card α = 0
-- Aesop.Search.Expansion
Aesop.SafeRulesResult.failed.sizeOf_spec : ∀ (postponed : Array Aesop.PostponedSafeRule), sizeOf (Aesop.SafeRulesResult.failed postponed) = 1 + sizeOf postponed
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- A single point is cospherical.  -/
EuclideanGeometry.cospherical_singleton : ∀ {P : Type u_2} [inst : MetricSpace P] (p : P), EuclideanGeometry.Cospherical {p}
-- Std.Http.Data.Request
/-- The request-line of an HTTP request.
 -/
Std.Http.Request.Builder.line : Std.Http.Request.Builder → Std.Http.Request.Head
-- Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
/-- Second part of the First Main Theorem of Value Distribution Theory, quantitative version: If `f` is
meromorphic on the complex plane, then the characteristic functions (for value `⊤`) of `f` and
`f - a₀` differ at most by `log⁺ ‖a₀‖ + log 2`.
 -/
ValueDistribution.abs_characteristic_sub_characteristic_shift_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a₀ : E} {f : ℂ → E} {r : ℝ},
  Meromorphic f →
    |ValueDistribution.characteristic f ⊤ r - ValueDistribution.characteristic (fun x => f x - a₀) ⊤ r| ≤
      ‖a₀‖.posLog + Real.log 2
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_filter_key_eq_size_iff : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] {f : α → Bool},
  (↑m).WF →
    ((↑(Std.DHashMap.Internal.Raw₀.filter (fun k x => f k) m)).size = (↑m).size ↔
      ∀ (k : α) (h : m.contains k = true), f (m.getKey k h) = true)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
/-- The equivalence between the points on an elliptic curve `W` in affine coordinates satisfying a
predicate and the set of pairs `⟨x, y⟩` satisfying `W.Equation x y` with zero.  -/
WeierstrassCurve.Affine.pointEquivSubtype : {R : Type r} →
  [inst : CommRing R] →
    {W' : WeierstrassCurve.Affine R} →
      [inst_1 : Nontrivial R] →
        [inst_2 : WeierstrassCurve.IsElliptic W'] →
          {p : W'.Point → Prop} →
            p WeierstrassCurve.Affine.Point.zero →
              { P // p P } ≃ WithZero { xy // ∃ (h : W'.Equation xy.1 xy.2), p (WeierstrassCurve.Affine.Point.mk h) }
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.BuilderOption.transparency : Lean.Meta.TransparencyMode → Bool → Aesop.Frontend.BuilderOption
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_subset : ∀ {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [inst : CommMonoid M] {f : ι → M},
  s₁ ⊆ s₂ → (∀ x ∈ s₂, x ∉ s₁ → f x = 1) → ∏ x ∈ s₁, f x = ∏ x ∈ s₂, f x
-- Mathlib.Topology.GDelta.MetrizableSpace
instT6SpaceOfMetrizableSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [TopologicalSpace.MetrizableSpace X], T6Space X
-- Mathlib.Order.CompleteBooleanAlgebra
CompletelyDistribLattice.toBiheytingAlgebra : {α : Type u} → [self : CompletelyDistribLattice α] → BiheytingAlgebra α
-- Mathlib.Tactic.Ring.RingNF
_private.Mathlib.Tactic.Ring.RingNF.0.Mathlib.Tactic.RingNF.instEvalTermBehaviorIfUnchanged.evalTerm : Lean.Term → Lean.Elab.TermElabM (Mathlib.Tactic.BehaviorIfUnchanged × Lean.Expr)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.pushforward_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (R : CategoryTheory.Presieve X),
  CategoryTheory.Presieve.pushforward (CategoryTheory.CategoryStruct.id X) R = R
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.lintegral_traj : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {a : ℕ} (x₀ : (i : ↥(Finset.Iic a)) → X ↑i)
  {f : ((n : ℕ) → X n) → ENNReal},
  Measurable f →
    ∫⁻ (x : (n : ℕ) → X n), f x ∂(ProbabilityTheory.Kernel.traj κ a) x₀ =
      ∫⁻ (x : (n : ℕ) → X n), f (Function.updateFinset x (Finset.Iic a) x₀) ∂(ProbabilityTheory.Kernel.traj κ a) x₀
-- Mathlib.Logic.Equiv.Multiset
Denumerable.raise.eq_1 : ∀ (x : ℕ), Denumerable.raise [] x = []
-- Init.Data.Vector.Lemmas
Vector.mem_setIfInBounds : ∀ {α : Type u_1} {n i : ℕ} {xs : Vector α n} {a : α}, i < n → a ∈ xs.setIfInBounds i a
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
/-- The Lebesgue integral is zero iff the function is a.e. zero.

The measurability assumption is necessary, otherwise there are counterexamples: for instance, the
conclusion fails if `f` is the characteristic function of a Vitali set.  -/
MeasureTheory.lintegral_eq_zero_iff' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  AEMeasurable f μ → (∫⁻ (a : α), f a ∂μ = 0 ↔ f =ᵐ[μ] 0)
-- Mathlib.Order.Filter.IndicatorFunction
mulIndicator_union_eventuallyEq : ∀ {α : Type u_1} {M : Type u_3} [inst : Monoid M] {s t : Set α} {f : α → M} {l : Filter α},
  (∀ᶠ (a : α) in l, a ∉ s ∩ t) → (s ∪ t).mulIndicator f =ᶠ[l] s.mulIndicator f * t.mulIndicator f
-- Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
AbsoluteValue.IsAdmissible.toIsEuclidean : ∀ {R : Type u_1} [inst : EuclideanDomain R] {abv : AbsoluteValue R ℤ} (self : abv.IsAdmissible), abv.IsEuclidean
-- Std.Async.Basic
/-- Converts `Promise` into `Async`.
 -/
Std.Async.Async.ofPromise : {α : Type} →
  IO (IO.Promise (Except IO.Error α)) →
    optParam String "the promise linked to the Async was dropped" → Std.Async.Async α
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.recOn_one : ∀ {α : Type u_1} {motive : FreeMonoid α → Sort u_6} (one : motive 1)
  (of_mul : (x : α) → (xs : FreeMonoid α) → motive xs → motive (FreeMonoid.of x * xs)),
  FreeMonoid.recOn 1 one of_mul = one
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.support_pow_le : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (σ : Equiv.Perm α) (n : ℕ), (σ ^ n).support ⊆ σ.support
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.category : (P : TopCat → Prop) → CategoryTheory.Category.{u, u + 1} (CompHausLike P)
-- Lean.Data.Lsp.TextSync
Lean.Lsp.instFromJsonSaveOptions.fromJson : Lean.Json → Except String Lean.Lsp.SaveOptions
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.mk_surjective : ∀ {α : Type u_1} [inst : Group α] {s : Subgroup α}, Function.Surjective QuotientGroup.mk
-- Init.Data.List.Monadic
List.forIn'.loop.eq_2 : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : List α)
  (f : (a : α) → a ∈ as → β → m (ForInStep β)) (b : β) (a : α) (as'_1 : List α) (h : ∃ bs, bs ++ a :: as'_1 = as),
  List.forIn'.loop as f (a :: as'_1) b h = do
    let __do_lift ← f a ⋯ b
    match __do_lift with
      | ForInStep.done b => pure b
      | ForInStep.yield b =>
        have this := ⋯;
        List.forIn'.loop as f as'_1 b this
-- Mathlib.Combinatorics.Enumerative.DoubleCounting
Finset.prod_prod_bipartiteAbove_eq_prod_prod_bipartiteBelow : ∀ {R : Type u_1} {α : Type u_2} {β : Type u_3} (r : α → β → Prop) {s : Finset α} {t : Finset β} [inst : CommMonoid R]
  (f : α → β → R) [inst_1 : (a : α) → (b : β) → Decidable (r a b)],
  ∏ a ∈ s, ∏ b ∈ Finset.bipartiteAbove r t a, f a b = ∏ b ∈ t, ∏ a ∈ Finset.bipartiteBelow r s b, f a b
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k k' : α} {v : β},
      Array.find? (fun a => decide (cmp a.1 k = Ordering.eq)) (Std.DTreeMap.Raw.Const.toArray t) = some (k', v) ↔
        t.getKey? k = some k' ∧ Std.DTreeMap.Raw.Const.get? t k = some v
-- Mathlib.FieldTheory.RatFunc.Basic
/-- Lift a monoid with zero homomorphism `R[X] →*₀ G₀` to a `R⟮X⟯ →*₀ G₀`
on the condition that `φ` maps non-zero-divisors to non-zero-divisors,
by mapping both the numerator and denominator and quotienting them.  -/
RatFunc.liftMonoidWithZeroHom : {G₀ : Type u_1} →
  {R : Type u_3} →
    [inst : CommGroupWithZero G₀] →
      [inst_1 : CommRing R] →
        (φ : Polynomial R →*₀ G₀) →
          nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors G₀) → RatFunc R →*₀ G₀
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.C_pow : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (a : R) (n : ℕ), MvPolynomial.C (a ^ n) = MvPolynomial.C a ^ n
-- Mathlib.Topology.Separation.GDelta
instT6SpaceElem : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} [T6Space X], T6Space ↑s
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RccSliceData.mk.injEq : ∀ {α : Type u} {β : Type v} [inst : Ord α] (treeMap : Std.DTreeMap.Internal.Impl α fun x => β) (range : Std.Rcc α)
  (treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => β) (range_1 : Std.Rcc α),
  ({ treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 }) =
    (treeMap = treeMap_1 ∧ range = range_1)
-- Lean.Meta.ExprLens
/-- Run the given `replace` function to replace the expression at the subexpression position. If the subexpression is below a binder
the bound variables will be appropriately instantiated with free variables and reabstracted after the replacement.
If the subexpression is invalid or points to a type then this will throw.  -/
Lean.Meta.replaceSubexpr : {M : Type → Type} →
  [Monad M] →
    [MonadLiftT Lean.MetaM M] →
      [MonadControlT Lean.MetaM M] →
        [Lean.MonadError M] → (Lean.Expr → M Lean.Expr) → Lean.SubExpr.Pos → Lean.Expr → M Lean.Expr
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- `getStained! stx` expects `stx` to be an argument of a node of `SyntaxNodeKind`
`Lean.Parser.Tactic.location`.
Typically, we apply `getStained!` to the output of `getLocs`.

It returns the `HashSet` of `Stained` determined by the locations in `stx`.

The only difference with `getStained stx`, is that `getStained!` never returns `{}`:
if `getStained stx = {}`, then `getStained' stx = {.goal}`.

This means that tactics that do not have an explicit "`at`" in their syntax will be treated as
acting on the main goal.  -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.getStained! : Lean.Syntax → (optParam (Lean.Syntax → Bool) fun x => false) → Std.HashSet Mathlib.Linter.Flexible.Stained✝
-- Mathlib.Algebra.Ring.Opposite
AddOpposite.op_natCast : ∀ {R : Type u_1} [inst : NatCast R] (n : ℕ), AddOpposite.op ↑n = ↑n
-- Mathlib.Algebra.Group.Prod
mulMonoidHom_apply : ∀ {α : Type u_6} [inst : CommMonoid α] (a : α × α), mulMonoidHom a = mulMulHom.toFun a
-- Mathlib.CategoryTheory.Center.Preadditive
CategoryTheory.CatCenter.app_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (z₁ z₂ : CategoryTheory.CatCenter C) (X : C), (z₁ + z₂).app X = z₁.app X + z₂.app X
-- Mathlib.Algebra.Group.UniqueProds.Basic
_private.Mathlib.Algebra.Group.UniqueProds.Basic.0.instMulI.eq_1 : ∀ (G : Type u) (H : Type v) [inst : Mul G] [inst_1 : Mul H] (t : Bool), instMulI✝ G H t = Bool.rec ULift.mul ULift.mul t
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get_map : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {f : α → β → γ} {k : α} {h' : k ∈ Std.ExtDTreeMap.map f t},
  Std.ExtDTreeMap.Const.get (Std.ExtDTreeMap.map f t) k h' = f k (Std.ExtDTreeMap.Const.get t k ⋯)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_insertMany_list : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {l : List (α × β)}, (t.insertMany l).isEmpty = (t.isEmpty && l.isEmpty)
-- Mathlib.Topology.Order.IntermediateValue
ContinuousOn.image_Ici_of_monotoneOn : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a : α} {f : α → δ},
  ContinuousOn f (Set.Ici a) →
    MonotoneOn f (Set.Ici a) → Filter.Tendsto f Filter.atTop Filter.atTop → f '' Set.Ici a = Set.Ici (f a)
-- Mathlib.Algebra.Group.Pi.Basic
Pi.commSemigroup : {I : Type u} → {f : I → Type v₁} → [(i : I) → CommSemigroup (f i)] → CommSemigroup ((i : I) → f i)
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.uniqueDiffOn_image : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  (e : E ≃L[𝕜] F), UniqueDiffOn 𝕜 s → UniqueDiffOn 𝕜 (⇑e '' s)
-- Mathlib.RingTheory.Congruence.Basic
RingCon.nontrivial_iff : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R], Nontrivial (RingCon R) ↔ Nontrivial R