mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Fin.Basic
/-- `fin_omega` is a preprocessor for `omega` to handle inequalities in `Fin`.
It rewrites all hypotheses and the goal, turning statements about addition, subtraction and
inequalities in `Fin n` into statements that `omega` can use/solve.
Note that this involves a lot of case splitting, so may be slow.
 -/
Fin.tacticFin_omega : Lean.ParserDescr
-- Mathlib.Data.Seq.Computation
_private.Mathlib.Data.Seq.Computation.0.Computation.Bind.f.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : Computation α ⊕ Computation β → Sort u_3) (ca : Computation α)
  (h_1 : (ca : Computation α) → motive (Sum.inl ca)) (h_2 : (cb : Computation β) → motive (Sum.inr cb)),
  (match Sum.inl ca with
    | Sum.inl ca => h_1 ca
    | Sum.inr cb => h_2 cb) =
    h_1 ca
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.exists_large_sphere_aux : ∀ (n d : ℕ),
  ∃ k ∈ Finset.range (n * (d - 1) ^ 2 + 1), ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(Behrend.sphere n d k).card
-- Mathlib.CategoryTheory.ComposableArrows.Four
CategoryTheory.ComposableArrows.fourδ₃Toδ₂_app_one : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂)
  (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₂₃ : i₁ ⟶ i₃) (f₃₄ : i₂ ⟶ i₄) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃)
  (h₃₄ : CategoryTheory.CategoryStruct.comp f₃ f₄ = f₃₄),
  (CategoryTheory.ComposableArrows.fourδ₃Toδ₂ f₁ f₂ f₃ f₄ f₂₃ f₃₄ h₂₃ h₃₄).app 1 =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃₄).obj 1)
-- Mathlib.Topology.DiscreteSubset
isDiscrete_univ_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X], IsDiscrete Set.univ ↔ DiscreteTopology X
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
/-- A functor taking a colimit on each fiber of a functor `G : Grothendieck F ⥤ H`.  -/
CategoryTheory.Limits.fiberwiseColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F : CategoryTheory.Functor C CategoryTheory.Cat} →
      {H : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} H] →
          (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) →
            [∀ {X Y : C} (f : X ⟶ Y),
                  CategoryTheory.Limits.HasColimit
                    ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] →
              CategoryTheory.Functor C H
-- Mathlib.Topology.Hom.Open
ContinuousOpenMapClass.map_open : ∀ {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} {inst : TopologicalSpace α}
  {inst_1 : TopologicalSpace β} {inst_2 : FunLike F α β} [self : ContinuousOpenMapClass F α β] (f : F), IsOpenMap ⇑f
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.instAddZeroClass : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Monoid G] →
          [inst_1 : Ring R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : TopologicalSpace V] →
                [inst_4 : IsTopologicalAddGroup V] →
                  [inst_5 : Module R V] →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : TopologicalSpace W] →
                        [inst_8 : IsTopologicalAddGroup W] →
                          [inst_9 : Module R W] →
                            {π₁ : ContRepresentation R G V} →
                              {π₂ : ContRepresentation R G W} → AddZeroClass (ContIntertwiningMap π₁ π₂)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.length_takeUntil : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] (p : G.Walk u v) (h : w ∈ p.support),
  (p.takeUntil w h).length = List.idxOf w p.support
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.coroot.eq_1 : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] (α : LieModule.Weight K (↥H) L),
  LieAlgebra.IsKilling.coroot α =
    2 •
      (α ((LieAlgebra.IsKilling.cartanEquivDual H).symm (LieModule.Weight.toLinear K (↥H) L α)))⁻¹ •
        (LieAlgebra.IsKilling.cartanEquivDual H).symm (LieModule.Weight.toLinear K (↥H) L α)
-- Init.Data.UInt.Lemmas
UInt8.ofBitVec_neg : ∀ (b : BitVec 8), { toBitVec := -b } = -{ toBitVec := b }
-- Mathlib.Topology.Algebra.Monoid
Filter.Tendsto.val_units : ∀ {ι : Type u_1} {N : Type u_4} [inst : TopologicalSpace N] [inst_1 : Monoid N] [inst_2 : ContinuousMul N]
  [inst_3 : T2Space N] {f : ι → Nˣ} {r₁ r₂ : N} {l : Filter ι} [inst_4 : l.NeBot]
  (h₁ : Filter.Tendsto (fun x => ↑(f x)) l (nhds r₁)) (h₂ : Filter.Tendsto (fun x => ↑(f x)⁻¹) l (nhds r₂)),
  ↑(h₁.units h₂) = r₁
-- Mathlib.Data.Finset.NatDivisors
/-- Products of divisors taken from coprime naturals are unique.  -/
Nat.Coprime.mul_injOn_divisors : ∀ {m n : ℕ}, m.Coprime n → Set.InjOn (fun p => p.1 * p.2) ↑(m.divisors ×ˢ n.divisors)
-- Lean.Data.OpenDecl
Lean.OpenDecl.instToString : ToString Lean.OpenDecl
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.smulLeftCLM_apply : ∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NontriviallyNormedField 𝕜]
  [inst_5 : NormedAlgebra ℝ 𝕜] [inst_6 : NormedSpace 𝕜 F] {g : E → 𝕜},
  Function.HasTemperateGrowth g → ∀ (f : SchwartzMap E F), ⇑((SchwartzMap.smulLeftCLM F g) f) = fun x => g x • f x
-- Mathlib.GroupTheory.Nilpotent
/-- A sequence of subgroups of `G` is a descending central series if `H 0` is `G` and
`⁅H n, G⁆ ⊆ H (n + 1)` for all `n`. Note that we do not require that `H n = {1}` for some `n`.  -/
Subgroup.IsDescendingCentralSeries : {G : Type u_1} → [inst : Group G] → (ℕ → Subgroup G) → Prop
-- Init.Data.ByteArray.Basic
ByteArray.instDecidableEq : DecidableEq ByteArray
-- Mathlib.Order.Interval.Finset.Nat
Nat.Ioc_eq_range' : ∀ (a b : ℕ), Finset.Ioc a b = { val := ↑(List.range' (a + 1) (b - a)), nodup := ⋯ }
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic
analyticAt_comp_iff_of_deriv_ne_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜} [CompleteSpace 𝕜] [CharZero 𝕜] {E : Type u_2}
  [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {g : 𝕜 → E},
  AnalyticAt 𝕜 f x → deriv f x ≠ 0 → (AnalyticAt 𝕜 (g ∘ f) x ↔ AnalyticAt 𝕜 g (f x))
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_filter_not_mul_prod_filter : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] (s : Finset ι) (p : ι → Prop) [inst_1 : DecidablePred p]
  [inst_2 : (x : ι) → Decidable ¬p x] (f : ι → M), (∏ x ∈ s with ¬p x, f x) * ∏ x ∈ s with p x, f x = ∏ x ∈ s, f x
-- Mathlib.Geometry.Convex.Cone.Face.Basic
PointedCone.IsFaceOf.rfl : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {C : PointedCone R M}, C.IsFaceOf C
-- Mathlib.CategoryTheory.ObjectProperty.Equivalence
CategoryTheory.ObjectProperty.essSurj_ιOfLE_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : CategoryTheory.ObjectProperty C} (h : P ≤ Q),
  (CategoryTheory.ObjectProperty.ιOfLE h).EssSurj ↔ Q ≤ P.isoClosure
-- Mathlib.Data.Fintype.Pi
Finset.instSingleton.hcongr_1 : ∀ (α α' : Type u_1), α = α' → Finset.instSingleton ≍ Finset.instSingleton
-- Aesop.RuleTac.GoalDiff
/-- If `diff₁` is the difference between goals `g₁` and `g₂` and `diff₂` is the
difference between `g₂` and `g₃`, then `diff₁.comp diff₂` is the difference
between `g₁` and `g₃`.

We assume that a hypothesis which changed between `g₁` and `g₂` does not
change back, i.e. the hypothesis is still different between `g₁` and `g₃`, and
similar for the targets.
 -/
Aesop.GoalDiff.comp : Aesop.GoalDiff → Aesop.GoalDiff → Aesop.GoalDiff
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.functorToRepresentables_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁)))
  {X Y : P.Elementsᵒᵖ} (f : X ⟶ Y),
  (CategoryTheory.Presheaf.functorToRepresentables P).map f = CategoryTheory.uliftYoneda.{w, v₁, u₁}.map (↑f.unop).unop
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.instAddCommGroupHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} → {M₁ M₂ : PresheafOfModules R} → AddCommGroup (M₁ ⟶ M₂)
-- Mathlib.CategoryTheory.Functor.Derived.Adjunction
/-- An adjunction between functors induces an adjunction between the
corresponding left/right derived functors, when these derived
functors are *absolute*, i.e. they remain derived functors
after the post-composition with any functor.

(One actually only needs that `G' ⋙ F'` is the left derived functor of
`G ⋙ L₂ ⋙ F'` and that `F' ⋙ G'` is the right derived functor of
`F ⋙ L₁ ⋙ G'`).  -/
CategoryTheory.Adjunction.derived : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D₁ : Type u_3} →
      {D₂ : Type u_4} →
        [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} D₁] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] →
                {G : CategoryTheory.Functor C₁ C₂} →
                  {F : CategoryTheory.Functor C₂ C₁} →
                    (G ⊣ F) →
                      {L₁ : CategoryTheory.Functor C₁ D₁} →
                        {L₂ : CategoryTheory.Functor C₂ D₂} →
                          (W₁ : CategoryTheory.MorphismProperty C₁) →
                            (W₂ : CategoryTheory.MorphismProperty C₂) →
                              [inst_4 : L₁.IsLocalization W₁] →
                                [inst_5 : L₂.IsLocalization W₂] →
                                  {G' : CategoryTheory.Functor D₁ D₂} →
                                    {F' : CategoryTheory.Functor D₂ D₁} →
                                      (α : L₁.comp G' ⟶ G.comp L₂) →
                                        (β : F.comp L₁ ⟶ L₂.comp F') →
                                          [G'.IsLeftDerivedFunctor α W₁] →
                                            [F'.IsRightDerivedFunctor β W₂] →
                                              [(G'.comp F').IsLeftDerivedFunctor
                                                    (CategoryTheory.CategoryStruct.comp (L₁.associator G' F').inv
                                                      (CategoryTheory.Functor.whiskerRight α F'))
                                                    W₁] →
                                                [(F'.comp G').IsRightDerivedFunctor
                                                      (CategoryTheory.CategoryStruct.comp
                                                        (CategoryTheory.Functor.whiskerRight β G')
                                                        (L₂.associator F' G').hom)
                                                      W₂] →
                                                  G' ⊣ F'
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.sum_map_nsmul : ∀ {ι : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {m : Multiset ι} {f : ι → M} {n : ℕ},
  (Multiset.map (fun i => n • f i) m).sum = n • (Multiset.map f m).sum
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  [inst_1 : Inhabited (β k)], k ∈ m₂ → (m₁ \ m₂).get! k = default
-- Mathlib.Order.RelIso.Basic
RelIso.compl_symm_apply : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) (a : β),
  f.compl.symm a = EquivLike.inv f a
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectrum.spectralRadius_le_pow_nnnorm_pow_one_div : ∀ (𝕜 : Type u_1) {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [CompleteSpace A] (a : A) (n : ℕ), spectralRadius 𝕜 a ≤ ↑‖a ^ (n + 1)‖₊ ^ (1 / (↑n + 1)) * ↑‖1‖₊ ^ (1 / (↑n + 1))
-- Std.Data.String.ToInt
String.Slice.isInt_congr : ∀ {s t : String.Slice}, s.copy = t.copy → s.isInt = t.isInt
-- Mathlib.ModelTheory.Substructures
/-- The preimage of a substructure along a homomorphism is a substructure.  -/
FirstOrder.Language.Substructure.comap : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type u_1} → [inst : L.Structure M] → [inst_1 : L.Structure N] → L.Hom M N → L.Substructure N → L.Substructure M
-- Mathlib.Data.Set.Image
Codisjoint.preimage : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) {s t : Set β}, Codisjoint s t → Codisjoint (f ⁻¹' s) (f ⁻¹' t)
-- Mathlib.MeasureTheory.Measure.Restrict
/-- Two measures are equal if they have equal restrictions on a spanning collection of sets
(formulated using `Union`).  -/
MeasureTheory.Measure.ext_iff_of_iUnion_eq_univ : ∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α},
  ⋃ i, s i = Set.univ → (μ = ν ↔ ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i))
-- Init.Data.SInt.Lemmas
UInt16.toInt16_ofNatLT : ∀ {n : ℕ} (hn : n < UInt16.size), (UInt16.ofNatLT n hn).toInt16 = Int16.ofNat n
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Tactic.ComputeAsymptotics.Seq.gcorec.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (F F_1 : β → Option (α × γ × β)),
  F = F_1 →
    ∀ (op op_1 : γ → Stream'.Seq α → Stream'.Seq α) (e_op : op = op_1)
      [inst : Tactic.ComputeAsymptotics.Seq.FriendlyOperationClass op] (a a_1 : β),
      a = a_1 → Tactic.ComputeAsymptotics.Seq.gcorec F op a = Tactic.ComputeAsymptotics.Seq.gcorec F_1 op_1 a_1
-- Mathlib.Logic.Relation
Relation.EqvGen.eqvGen_mono : ∀ {α : Type u_1} {r r' : α → α → Prop}, r ≤ r' → Relation.EqvGen r ≤ Relation.EqvGen r'
-- Mathlib.Data.Finset.Image
Finset.canLift : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (c : α → β) (p : β → Prop) [CanLift β α c p],
  CanLift (Finset β) (Finset α) (Finset.image c) fun s => ∀ x ∈ s, p x
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.lift_unique' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F₁ F₂ : CategoryTheory.Functor (CategoryTheory.Quotient r) D),
  (CategoryTheory.Quotient.functor r).comp F₁ = (CategoryTheory.Quotient.functor r).comp F₂ → F₁ = F₂
-- Lean.Elab.BuiltinCommand
_private.Lean.Elab.BuiltinCommand.0.Lean.Elab.Command.throwUnnecessaryScopeName : Lean.Name → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.continuous_iff_from_discrete : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_3} [inst_1 : TopologicalSpace Y] [DiscreteTopology X]
  (f : OnePoint X → Y), Continuous f ↔ Filter.Tendsto (fun x => f ↑x) Filter.cofinite (nhds (f OnePoint.infty))
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
AffineSubspace.angle_coe : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} (p₁ p₂ p₃ : ↥s),
  EuclideanGeometry.angle ↑p₁ ↑p₂ ↑p₃ = EuclideanGeometry.angle p₁ p₂ p₃
-- Mathlib.Algebra.Category.Ring.Constructions
CommRingCat.isPushout_tensorProduct : ∀ (R A B : Type u) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B] [inst_3 : Algebra R A]
  [inst_4 : Algebra R B],
  CategoryTheory.IsPushout (CommRingCat.ofHom (algebraMap R A)) (CommRingCat.ofHom (algebraMap R B))
    (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom)
    (CommRingCat.ofHom Algebra.TensorProduct.includeRight.toRingHom)
-- Mathlib.Analysis.Analytic.Inverse
/-- If a a formal multilinear series has a positive radius of convergence, then its left inverse
also has a positive radius of convergence.  -/
FormalMultilinearSeries.radius_leftInv_pos_of_radius_pos : ∀ {𝕜 : 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]
  {p : FormalMultilinearSeries 𝕜 E F} {i : E ≃L[𝕜] F} {x : E},
  0 < p.radius → p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i → 0 < (p.leftInv i x).radius
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.Nat.isSemilinearSet_compl_of_isProperLinearSet : ∀ {ι : Type u_3} [Finite ι] {s : Set (ι → ℕ)}, IsProperLinearSet s → IsSemilinearSet sᶜ
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Reachable.nonempty_neighborSet_left : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, u ≠ v → G.Reachable u v → (G.neighborSet u).Nonempty
-- Mathlib.RingTheory.DedekindDomain.Factorization
FractionalIdeal.count_mono : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  {I J : FractionalIdeal (nonZeroDivisors R) K},
  I ≠ 0 → I ≤ J → FractionalIdeal.count K v J ≤ FractionalIdeal.count K v I
-- Mathlib.Order.Defs.PartialOrder
/-- `<` is decidable if `≤` is.  -/
decidableLTOfDecidableLE : {α : Type u_1} → [inst : Preorder α] → [DecidableLE α] → DecidableLT α
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] ⦃f g : α →*₀ β⦄,
  (∀ (x : α), f x = g x) → f = g
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.mem_of_mem_val_ofAddUnits : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubgroup (AddUnits M)) {y : AddUnits M}, ↑y ∈ S.ofAddUnits → y ∈ S
-- Mathlib.Computability.EpsilonNFA
εNFA.toNFA_correct : ∀ {α : Type u} {σ : Type v} (M : εNFA α σ), M.toNFA.accepts = M.accepts
-- Mathlib.Algebra.SkewMonoidAlgebra.Support
SkewMonoidAlgebra.support_single_mul : ∀ {k : Type u_1} {G : Type u_2} [inst : Monoid G] [inst_1 : Semiring k] [inst_2 : MulSemiringAction G k]
  (f : SkewMonoidAlgebra k G) [inst_3 : IsLeftCancelMul G] (r : k) (x : G),
  (∀ (y : k), r * x • y = 0 ↔ y = 0) →
    (SkewMonoidAlgebra.single x r * f).support = Finset.map (mulLeftEmbedding x) f.support
-- Std.Internal.Parsec.ByteArray
ByteArray.Iterator.curr'.congr_simp : ∀ (it it_1 : ByteArray.Iterator) (e_it : it = it_1) (h : it.hasNext = true), it.curr' h = it_1.curr' ⋯
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.toLinearEquiv_assocIsometry : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G],
  (TensorProduct.assocIsometry 𝕜 E F G).toLinearEquiv = TensorProduct.assoc 𝕜 E F G
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
/-- `rpow` variant of `List.prod_map_pow` for `ℝ≥0`  -/
NNReal.list_prod_map_rpow : ∀ (l : List NNReal) (r : ℝ), (List.map (fun x => x ^ r) l).prod = l.prod ^ r
-- Init.Data.Vector.Monadic
Vector.forM_append : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n n' : ℕ} [inst : Monad m] [LawfulMonad m] {xs : Vector α n}
  {ys : Vector α n'} {f : α → m PUnit.{u_1 + 1}},
  forM (xs ++ ys) f = do
    forM xs f
    forM ys f
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.comap_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (I : Z.IdealSheafData) (f : X ⟶ Y) (g : Y ⟶ Z),
  I.comap (CategoryTheory.CategoryStruct.comp f g) = (I.comap g).comap f
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_transpose_mul_self : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Fintype n] [inst_1 : Fintype m] [inst_2 : Field R]
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R] (A : Matrix m n R), (A.transpose * A).rank = A.rank
-- Mathlib.Topology.Algebra.ConstMulAction
/-- The quotient map by a group action is open, i.e. the quotient by a group
action is an open quotient.  -/
isOpenMap_quotient_mk'_add : ∀ {Γ : Type u_4} [inst : AddGroup Γ] {T : Type u_5} [inst_1 : TopologicalSpace T] [inst_2 : AddAction Γ T]
  [ContinuousConstVAdd Γ T], IsOpenMap Quotient.mk'
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.single_mem_span_single : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [Nontrivial R] {m : M} {s : Set M},
  AddMonoidAlgebra.single m 1 ∈ Submodule.span R ((fun x => AddMonoidAlgebra.single x 1) '' s) ↔ m ∈ s
-- Mathlib.RingTheory.PowerSeries.Trunc
PowerSeries.trunc_sub : ∀ {R : Type u_1} [inst : Ring R] (n : ℕ) (φ ψ : PowerSeries R),
  (PowerSeries.trunc n) (φ - ψ) = (PowerSeries.trunc n) φ - (PowerSeries.trunc n) ψ
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃'_map_app_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f : X ⟶ Y) (j X₃ : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃' C).map f).app j).app X₃ =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft j (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X₃)
-- Mathlib.Algebra.Category.MonCat.Limits
/-- A choice of limit cone for a functor into `CommMonCat`.
(Generally, you'll just want to use `limit F`.)
 -/
CommMonCat.limitCone : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J CommMonCat) →
      [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommMonCat)).sections] → CategoryTheory.Limits.Cone F
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_inv_same₀ : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  AEMeasurable f μ →
    (∀ᵐ (x : α) ∂μ, f x ≠ 0) → (∀ᵐ (x : α) ∂μ, f x ≠ ⊤) → ((μ.withDensity f).withDensity fun x => (f x)⁻¹) = μ
-- Init.Data.Array.Erase
Array.size_erase : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {a : α} {xs : Array α},
  (xs.erase a).size = if a ∈ xs then xs.size - 1 else xs.size
-- Mathlib.SetTheory.ZFC.PSet
PSet.mem_of_subset : ∀ {x y z : PSet.{u_1}}, x ⊆ y → z ∈ x → z ∈ y
-- Mathlib.Tactic.Linarith.Frontend
_private.Mathlib.Tactic.Linarith.Frontend.0.Mathlib.Tactic.elabLinarithConfig.evalConfigItem : Lean.Elab.ConfigEval.EvalConfigItem Mathlib.Tactic.Linarith.LinarithConfig
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
/-- Given a smooth commutative ring `R` and a manifold `M`, and an open neighbourhood `U` of a point
`x : M`, the evaluation-at-`x` map to `R` from smooth functions from  `U` to `R`.  -/
smoothSheafCommRing.evalAt : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_2} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_3} →
            [inst_3 : TopologicalSpace HM] →
              (IM : ModelWithCorners 𝕜 EM HM) →
                {E : Type u_4} →
                  [inst_4 : NormedAddCommGroup E] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      {H : Type u_5} →
                        [inst_6 : TopologicalSpace H] →
                          (I : ModelWithCorners 𝕜 E H) →
                            (M : Type u) →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace HM M] →
                                  (R : Type u) →
                                    [inst_9 : TopologicalSpace R] →
                                      [inst_10 : ChartedSpace H R] →
                                        [inst_11 : CommRing R] →
                                          [inst_12 : ContMDiffRing I (↑⊤) R] →
                                            (x : ↑(TopCat.of M)) →
                                              (U : TopologicalSpace.OpenNhds x) →
                                                (smoothSheafCommRing IM I M R).presheaf.obj (Opposite.op ↑U) ⟶
                                                  CommRingCat.of R
-- Mathlib.Tactic.Ring.Basic
Mathlib.Tactic.Ring.natCast_int : ∀ {R : Type u_2} [inst : CommRing R] (n : ℕ), ↑n.rawCast = n.rawCast
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instAlgebra : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      {R : Type u_5} →
        [inst_1 : CommSemiring R] → [inst_2 : Semiring Y] → [Algebra R Y] → Algebra R (LocallyConstant X Y)