mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : MulOneClass α] [inst_4 : MulOneClass β] [inst_5 : MulOneClass γ] {g : β →*o γ} {f₁ f₂ : α →*o β},
  Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Init.Data.Nat.Basic
Nat.mul_le_mul_right_iff : ∀ {n m k : ℕ}, 0 < k → (n * k ≤ m * k ↔ n ≤ m)
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.rnDeriv_withDensity_rnDeriv : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν], μ.AbsolutelyContinuous ν → μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) =ᵐ[μ] μ.rnDeriv ν
-- Mathlib.Analysis.Calculus.Deriv.Add
derivWithin_add : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {x : 𝕜} {s : Set 𝕜},
  DifferentiableWithinAt 𝕜 f s x →
    DifferentiableWithinAt 𝕜 g s x → derivWithin (f + g) s x = derivWithin f s x + derivWithin g s x
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.instMonoidalOfBraided : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → (CategoryTheory.Center.ofBraided C).Monoidal
-- Mathlib.Analysis.Convex.Gauge
/-- `gauge s` as a seminorm when `s` is balanced, convex and absorbent.  -/
gaugeSeminorm : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : AddCommGroup E] →
      [inst_1 : Module ℝ E] →
        {s : Set E} →
          [inst_2 : RCLike 𝕜] →
            [inst_3 : Module 𝕜 E] → [IsScalarTower ℝ 𝕜 E] → Balanced 𝕜 s → Convex ℝ s → Absorbent ℝ s → Seminorm 𝕜 E
-- Mathlib.Algebra.Group.Units.Equiv
/-- Extra simp lemma that `dsimp` can use. `simp` will never use this.  -/
Equiv.mulLeft_symm_apply : ∀ {G : Type u_5} [inst : Group G] (a : G), ⇑(Equiv.symm (Equiv.mulLeft a)) = fun x => a⁻¹ * x
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Unitary.openPartialHomeomorph_target : ∀ {A : Type u_1} [inst : CStarAlgebra A], Unitary.openPartialHomeomorph.target = Metric.ball 0 Real.pi
-- Mathlib.CategoryTheory.MorphismProperty.Concrete
CategoryTheory.MorphismProperty.instIsMultiplicativeSurjective : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type u_2}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC],
  (CategoryTheory.MorphismProperty.surjective C).IsMultiplicative
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_app_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasProducts A]
  {P : CategoryTheory.Functor Cᵒᵖ A} {M : A} [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  (f : Φ.presheafFiber.obj P ⟶ M) (X : C) (x : Φ.fiber.obj X) {Z : A} (h : M ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((Φ.skyscraperPresheafHomEquiv f).app (Opposite.op X))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun x => M) x) h) =
    CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x P) (CategoryTheory.CategoryStruct.comp f h)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.map_id : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp},
  Std.ExtDTreeMap.map (fun x v => v) t = t
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.resolveLValLoop : Lean.Elab.Term.LVal → Lean.Expr → Lean.Expr → Bool → Lean.Elab.TermElabM (Lean.Expr × Lean.Elab.Term.LValResolution)
-- Init.Control.Option
OptionT.instMonad : {m : Type u → Type v} → [Monad m] → Monad (OptionT m)
-- Mathlib.Algebra.Group.Ext
AddMonoid.ext : ∀ {M : Type u} ⦃m₁ m₂ : AddMonoid M⦄, HAdd.hAdd = HAdd.hAdd → m₁ = m₂
-- Lean.Meta.InferType
_private.Lean.Meta.InferType.0.Lean.Meta.inferProjType : Lean.Name → ℕ → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
/-- Multiplicative functions  -/
ArithmeticFunction.IsMultiplicative : {R : Type u_1} → [inst : MonoidWithZero R] → ArithmeticFunction R → Prop
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.zpow_add_one : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  {A : Matrix n' n' R}, IsUnit A.det → ∀ (n : ℤ), A ^ (n + 1) = A ^ n * A
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The affine span of a set of points is the smallest affine subspace containing those points.
(Actually defined here in terms of spans in modules.)  -/
affineSpan : (k : Type u_1) →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] → [inst_2 : Module k V] → [inst_3 : AddTorsor V P] → Set P → AffineSubspace k P
-- Mathlib.Topology.Compactness.Compact
Prod.noncompactSpace_left : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [NoncompactSpace X] [Nonempty Y],
  NoncompactSpace (X × Y)
-- Mathlib.NumberTheory.Ostrowski
_private.Mathlib.NumberTheory.Ostrowski.0.tendsto_nat_rpow_inv : Filter.Tendsto (fun k => ↑k ^ (↑k)⁻¹) Filter.atTop (nhds 1)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
SimplexCategoryGenRel.δ_comp_σ_of_le_assoc : ∀ {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)},
  i ≤ j.castSucc →
    ∀ {Z : SimplexCategoryGenRel} (h : SimplexCategoryGenRel.mk (n + 1) ⟶ Z),
      CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.δ i.castSucc)
          (CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.σ j.succ) h) =
        CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.σ j)
          (CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.δ i) h)
-- Mathlib.Combinatorics.Graph.Delete
Graph.restrict_mono_right : ∀ {α : Type u_1} {β : Type u_2} {F F₀ : Set β} (G : Graph α β), F₀ ⊆ F → G.restrict F₀ ≤ G.restrict F
-- Mathlib.Topology.Algebra.GroupWithZero
/-- If a function converges to a nonzero value, its inverse converges to the inverse of this value.
We use the name `Filter.Tendsto.inv₀` as `Filter.Tendsto.inv` is already used in multiplicative
topological groups.  -/
Filter.Tendsto.inv₀ : ∀ {α : Type u_1} {G₀ : Type u_3} [inst : Zero G₀] [inst_1 : Inv G₀] [inst_2 : TopologicalSpace G₀] [ContinuousInv₀ G₀]
  {l : Filter α} {f : α → G₀} {a : G₀},
  Filter.Tendsto f l (nhds a) → a ≠ 0 → Filter.Tendsto (fun x => (f x)⁻¹) l (nhds a⁻¹)
-- Lean.Parser.Term
Lean.Parser.Term.declName.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Order.Partition.Basic
Partition.rel_le_iff_le : ∀ {α : Type u_1} {u : Set α} {P Q : Partition u}, P.Rel ≤ Q.Rel ↔ P ≤ Q
-- Mathlib.RingTheory.NormalClosure
_private.Mathlib.RingTheory.NormalClosure.0.Ring.termT : Lean.ParserDescr
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.Comma.costructuredArrowSndProj_obj : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) (b : B) (X : CategoryTheory.CostructuredArrow (CategoryTheory.Comma.snd L R) b),
  (CategoryTheory.Comma.costructuredArrowSndProj L R b).obj X =
    CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp X.left.hom (R.map X.hom))
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightIso_counitIso_hom_app_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ : CategoryTheory.Functor B T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : R₁ ≅ R₂) (X : CategoryTheory.MorphismProperty.Comma L R₂ P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapRightIso L e).counitIso.hom.app X).right =
    CategoryTheory.CategoryStruct.id X.right
-- Mathlib.RingTheory.FractionalIdeal.Operations
Units.submodule_isFractional : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [IsLocalization S P] (I : (Submodule R P)ˣ), IsFractional S ↑I
-- Mathlib.CategoryTheory.Limits.Types.Pullbacks
CategoryTheory.Limits.Types.isPullback_iff : ∀ {X₁ X₂ X₃ X₄ : Type u} (t : X₁ ⟶ X₂) (r : X₂ ⟶ X₄) (l : X₁ ⟶ X₃) (b : X₃ ⟶ X₄),
  CategoryTheory.IsPullback t l r b ↔
    CategoryTheory.CategoryStruct.comp t r = CategoryTheory.CategoryStruct.comp l b ∧
      (∀ (x₁ y₁ : (fun X => X) X₁),
          (CategoryTheory.ConcreteCategory.hom t) x₁ = (CategoryTheory.ConcreteCategory.hom t) y₁ ∧
              (CategoryTheory.ConcreteCategory.hom l) x₁ = (CategoryTheory.ConcreteCategory.hom l) y₁ →
            x₁ = y₁) ∧
        ∀ (x₂ : (fun X => X) X₂) (x₃ : (fun X => X) X₃),
          (CategoryTheory.ConcreteCategory.hom r) x₂ = (CategoryTheory.ConcreteCategory.hom b) x₃ →
            ∃ x₁, (CategoryTheory.ConcreteCategory.hom t) x₁ = x₂ ∧ (CategoryTheory.ConcreteCategory.hom l) x₁ = x₃
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.ofDarts_darts : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : ¬p.Nil),
  SimpleGraph.Walk.ofDarts p.darts ⋯ ⋯ = p.copy ⋯ ⋯
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.limIsoFlipCompWhiskerLim_inv_app_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  (X : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X_1 : K),
  (CategoryTheory.Limits.limIsoFlipCompWhiskerLim.inv.app X).app X_1 =
    (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation X X_1).inv
-- Mathlib.Algebra.Homology.DifferentialObject
CategoryTheory.DifferentialObject.objEqToHom_d : ∀ {β : Type u_1} [inst : AddCommGroup β] {b : β} {V : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} V]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) {x y : β} (h : x = y),
  CategoryTheory.CategoryStruct.comp (X.objEqToHom h) (X.d y) =
    CategoryTheory.CategoryStruct.comp (X.d x) (X.objEqToHom ⋯)
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.prod_mono_right : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
  (s : NonUnitalSubring R), Monotone fun t => s.prod t
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.top_mul : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] {b : WithTop α}, b ≠ 0 → ⊤ * b = ⊤
-- Mathlib.Analysis.InnerProductSpace.Spectrum
LinearMap.IsSymmetric.orthogonalFamily_eigenspaces' : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E},
  T.IsSymmetric →
    OrthogonalFamily 𝕜 (fun μ => ↥(Module.End.eigenspace T (↑T 1 μ))) fun μ =>
      (Module.End.eigenspace T (↑T 1 μ)).subtypeₗᵢ
-- Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Ideal.eq_bot_of_minimalPrimes_eq_empty : ∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R}, I.minimalPrimes = ∅ → I = ⊤
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
/-- A function is $C^{k+(0)}$ at a point if and only if it is $C^k$ at the point.  -/
ContDiffPointwiseHolderAt.zero_exponent_iff : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {k : ℕ} {f : E → F} {a : E}, ContDiffPointwiseHolderAt k 0 f a ↔ ContDiffAt ℝ (↑k) f a
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.transportIso_inv_fiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  (x : CategoryTheory.Grothendieck F) {c : C} (α : x.base ≅ c),
  (x.transportIso α).inv.fiber = CategoryTheory.CategoryStruct.id ((F.map α.hom).toFunctor.obj x.fiber)
-- Init.Prelude
Nat.div_rec_lemma : ∀ {x y : ℕ}, 0 < y ∧ y ≤ x → x - y < x
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- The sum and difference of two vectors are orthogonal if and only
if they have the same norm.  -/
real_inner_add_sub_eq_zero_iff : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F),
  inner ℝ (x + y) (x - y) = 0 ↔ ‖x‖ = ‖y‖
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.basisOfBasisRight.eq_1 : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {A B : Subalgebra R S} (H : A.LinearDisjoint B) (H' : A ⊔ B = ⊤) {ι : Type u_1} (b : Module.Basis ι R ↥B),
  H.basisOfBasisRight H' b = (Module.Basis.baseChange (↥A) b).map ↑(H.mulMapLeftOfSupEqTop H')
-- Mathlib.Logic.Function.Basic
Pi.map_update : ∀ {ι : Sort u_1} [inst : DecidableEq ι] {α : ι → Sort u_2} {β : ι → Sort u_3} {f : (i : ι) → α i → β i}
  (g : (i : ι) → α i) (i : ι) (a : α i), Pi.map f (Function.update g i a) = Function.update (Pi.map f g) i (f i a)
-- Lean.Parser.Term
/-- `letDecl` matches the body of a let declaration `let f x1 x2 := e`,
`let pat := e` (where `pat` is an arbitrary term) or `let f | pat1 => e1 | pat2 => e2 ...`
(a pattern matching declaration), except for the `let` keyword itself.
`let rec` declarations are not handled here.  -/
Lean.Parser.Term.letDecl : Lean.Parser.Parser
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn'_rci : ∀ {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] [inst_4 : LE α]
  [inst_5 : Std.PRange.UpwardEnumerable α] [inst_6 : Std.Rxi.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] [inst_8 : Std.PRange.LawfulUpwardEnumerableLE α] {xs : Std.Rci α}
  {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Std.Internal.Do.Invariant xs.toList β Pred)
  {epost : EPred},
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f cur ⋯ b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'
        | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b';
        epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init ⦄ forIn' xs init f ⦃ fun b =>
      inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b; epost ⦄
-- Mathlib.Topology.Algebra.ConstMulAction
isHomeomorph_smul : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [ContinuousConstSMul G α] (c : G), IsHomeomorph fun x => c • x
-- Mathlib.Logic.Function.Iterate
Function.Commute.self_iterate : ∀ {α : Type u} (f : α → α) (n : ℕ), Function.Commute f f^[n]
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.SubmersivePresentation.aeval_jacobianOfHasCoeffs : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ) (R₀ : Type u_5)
  [inst_4 : CommRing R₀] [inst_5 : Algebra R₀ R] [inst_6 : Algebra R₀ S] [inst_7 : IsScalarTower R₀ R S]
  [inst_8 : P.HasCoeffs R₀], (MvPolynomial.aeval P.val) (P.jacobianOfHasCoeffs R₀) = P.jacobian
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- The splitting of the short complex `S.op` deduced from a splitting of `S`.  -/
CategoryTheory.ShortComplex.Splitting.op : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] → {S : CategoryTheory.ShortComplex C} → S.Splitting → S.op.Splitting
-- Init.Core
if_neg : ∀ {c : Prop} {h : Decidable c}, ¬c → ∀ {α : Sort u} {t e : α}, (if c then t else e) = e
-- Mathlib.Data.Sigma.Order
Sigma.Lex.lt_def : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LT ι] [inst_1 : (i : ι) → LT (α i)] {a b : Σₗ (i : ι), α i},
  a < b ↔ a.fst < b.fst ∨ ∃ (h : a.fst = b.fst), h ▸ a.snd < b.snd
-- Init.Data.String.Pattern.String
_private.Init.Data.String.Pattern.String.0.String.Slice.Pattern.ForwardSliceSearcher.instIteratorIdSearchStep.match_1.eq_4 : ∀ (s : String.Slice) (motive : String.Slice.Pattern.ForwardSliceSearcher s → Sort u_1)
  (h_1 : (pos : s.Pos) → motive (String.Slice.Pattern.ForwardSliceSearcher.emptyBefore pos))
  (h_2 : (pos : s.Pos) → (h : pos ≠ s.endPos) → motive (String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos h))
  (h_3 :
    (needle : String.Slice) →
      (table : Vector ℕ needle.utf8ByteSize) →
        (ht : table = String.Slice.Pattern.ForwardSliceSearcher.buildTable needle) →
          (stackPos needlePos : String.Pos.Raw) →
            (hn : needlePos < needle.rawEndPos) →
              motive (String.Slice.Pattern.ForwardSliceSearcher.proper needle table ht stackPos needlePos hn))
  (h_4 : Unit → motive String.Slice.Pattern.ForwardSliceSearcher.atEnd),
  (match String.Slice.Pattern.ForwardSliceSearcher.atEnd with
    | String.Slice.Pattern.ForwardSliceSearcher.emptyBefore pos => h_1 pos
    | String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos h => h_2 pos h
    | String.Slice.Pattern.ForwardSliceSearcher.proper needle table ht stackPos needlePos hn =>
      h_3 needle table ht stackPos needlePos hn
    | String.Slice.Pattern.ForwardSliceSearcher.atEnd => h_4 ()) =
    h_4 ()
-- Mathlib.Order.Partition.Finpartition
Finpartition.mk.inj : ∀ {α : Type u_1} {inst : Lattice α} {inst_1 : OrderBot α} {a : α} {parts : Finset α} {supIndep : parts.SupIndep id}
  {sup_parts : parts.sup id = a} {bot_notMem : ⊥ ∉ parts} {parts_1 : Finset α} {supIndep_1 : parts_1.SupIndep id}
  {sup_parts_1 : parts_1.sup id = a} {bot_notMem_1 : ⊥ ∉ parts_1},
  { parts := parts, supIndep := supIndep, sup_parts := sup_parts, bot_notMem := bot_notMem } =
      { parts := parts_1, supIndep := supIndep_1, sup_parts := sup_parts_1, bot_notMem := bot_notMem_1 } →
    parts = parts_1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey!_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF → ∀ {k : α} {v : β}, (t.insert k v).minKey! = t.minKey?.elim k fun k' => if (cmp k k').isLE = true then k else k'
-- Mathlib.Algebra.Lie.Rank
LieAlgebra.finrank_engel : ∀ (K : Type u_7) {L : Type u_8} [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L]
  [inst_3 : Module.Finite K L] (x : L),
  Module.finrank K ↥(LieSubalgebra.engel K x) = (LinearMap.charpoly ((LieAlgebra.ad K L) x)).natTrailingDegree
-- Mathlib.Logic.Function.CompTypeclasses
CompTriple.IsId.eq_id : ∀ {M : Type u_1} {σ : M → M} [self : CompTriple.IsId σ], σ = id
-- Init.Data.Int.Order
Int.mul_nonneg_of_nonpos_of_nonpos : ∀ {a b : ℤ}, a ≤ 0 → b ≤ 0 → 0 ≤ a * b
-- Lean.Widget.TaggedText
Lean.Widget.TaggedText.text.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (a : String), sizeOf (Lean.Widget.TaggedText.text a) = 1 + sizeOf a
-- Init.GrindInstances.Ring.UInt
Lean.Grind.instCommRingUInt16 : Lean.Grind.CommRing UInt16
-- Mathlib.Analysis.InnerProductSpace.ProdL2
OrthonormalBasis.prod_apply : ∀ {𝕜 : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {E : Type u_4} {F : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : Fintype ι₁] [inst_6 : Fintype ι₂] (v : OrthonormalBasis ι₁ 𝕜 E)
  (w : OrthonormalBasis ι₂ 𝕜 F) (i : ι₁ ⊕ ι₂),
  (v.prod w) i = Sum.elim (WithLp.toLp 2 ∘ ⇑(LinearMap.inl 𝕜 E F) ∘ ⇑v) (WithLp.toLp 2 ∘ ⇑(LinearMap.inr 𝕜 E F) ∘ ⇑w) i
-- Mathlib.Algebra.Order.AddGroupWithTop
add_left_injective_of_ne_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommMonoidWithTop α] (b : α), b ≠ ⊤ → Function.Injective fun x => x + b
-- Mathlib.RingTheory.HahnSeries.HEval
HahnSeries.SummableFamily.powerSeriesFamily_smul : ∀ {Γ : Type u_1} {R : Type u_3} {V : Type u_4} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : CommRing R] [inst_4 : CommRing V] [inst_5 : Algebra R V]
  {x : HahnSeries Γ V} (f : PowerSeries R) (r : R),
  HahnSeries.SummableFamily.powerSeriesFamily x (r • f) =
    (HahnSeries.single 0) r • HahnSeries.SummableFamily.powerSeriesFamily x f
-- Mathlib.Analysis.Calculus.Deriv.CompMul
hasDerivWithinAt_comp_mul_left_smul_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {c : 𝕜} {f : 𝕜 → E} {f' : E} {s : Set 𝕜} {x : 𝕜},
  HasDerivWithinAt (fun x => f (c * x)) (c • f') s x ↔ HasDerivWithinAt f f' (c • s) (c * x)
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.ι_comp_over : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (S : AlgebraicGeometry.Scheme) [inst : X.Over S],
  CategoryTheory.CategoryStruct.comp U.ι (X ↘ S) = ↑U ↘ S
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesMapIso'_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData),
  (CategoryTheory.ShortComplex.cyclesMapIso' e h₁ h₂).inv = CategoryTheory.ShortComplex.cyclesMap' e.inv h₂ h₁
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.TriangleIndexData.h₁ : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {J : Type u_4} [inst : Zero I₂] {r : I₁ × I₂ × I₃ → J}
  {π : I₁ × I₃ → J} (self : CategoryTheory.GradedObject.TriangleIndexData r π) (i₁ : I₁), self.p₁₂ (i₁, 0) = i₁
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Parallelogram law  -/
parallelogram_law : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {x y : E}, inner 𝕜 (x + y) (x + y) + inner 𝕜 (x - y) (x - y) = 2 * (inner 𝕜 x x + inner 𝕜 y y)
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.toBitVec_assemble₂Unchecked : ∀ {w x : UInt8},
  (ByteArray.utf8DecodeChar?.assemble₂Unchecked w x).toBitVec =
    BitVec.setWidth 32 (BitVec.setWidth 5 w.toBitVec ++ BitVec.setWidth 6 x.toBitVec)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_alter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k k' : α} {f : Option (β k) → Option (β k)},
  Std.DTreeMap.Internal.Impl.contains k' (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl =
    if compare k k' = Ordering.eq then (f (t.get? k)).isSome else Std.DTreeMap.Internal.Impl.contains k' t
-- Mathlib.Order.Category.PartOrd
PartOrd.inv_hom_apply : ∀ {X Y : PartOrd} (e : X ≅ Y) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_bijective : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ},
  f ∈ 𝒜 m →
    0 < m →
      Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec 𝒜 f))
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.ofCoeff_single : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M) (r : R),
  (AddMonoidAlgebra.ofCoeff fun₀ | m => r) = AddMonoidAlgebra.single m r
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k : α}
  {h : Std.Internal.List.containsKey k l = true}, Std.Internal.List.getEntry k l h ∈ l