mathlib-initiative/mathlib-types huggingface dataset:
-- Init.GrindInstances.Ring.UInt
Lean.Grind.instCommRingUInt32 : Lean.Grind.CommRing UInt32
-- Mathlib.Topology.MetricSpace.Bounded
/-- The **Heine–Borel theorem**: In a proper space, the closure of a bounded set is compact.  -/
Bornology.IsBounded.isCompact_closure : ∀ {α : Type u} {s : Set α} [inst : PseudoMetricSpace α] [ProperSpace α], Bornology.IsBounded s → IsCompact (closure s)
-- Mathlib.Algebra.Group.End
/-- A stronger version of `mul_left_injective`  -/
Equiv.mul_swap_involutive : ∀ {α : Type u_4} [inst : DecidableEq α] (i j : α), Function.Involutive fun x => x * Equiv.swap i j
-- Std.Tactic.BVDecide.LRAT.Actions
Std.Tactic.BVDecide.LRAT.Action.addRat : {β : Type u} →
  {α : Type v} → ℕ → β → Std.Sat.Literal α → Array ℕ → Array (ℕ × Array ℕ) → Std.Tactic.BVDecide.LRAT.Action β α
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.swapLeft_apply' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ) (a : β × α) (s : Set γ),
  (κ.swapLeft a) s = (κ a.swap) s
-- Mathlib.Algebra.MvPolynomial.Coeff
/-- A monomial in two variables equals `C a * X 0 ^ d 0 * X 1 ^ d 1`.  -/
MvPolynomial.monomial_fin_two : ∀ {R : Type u_1} [inst : CommSemiring R] (d : Fin 2 →₀ ℕ) (a : R),
  (MvPolynomial.monomial d) a = MvPolynomial.C a * MvPolynomial.X 0 ^ d 0 * MvPolynomial.X 1 ^ d 1
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.initialIsoIsInitial_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasInitial C] {P : C}
  (t : CategoryTheory.Limits.IsInitial P), (CategoryTheory.Limits.initialIsoIsInitial t).inv = t.to (⊥_ C)
-- Mathlib.CategoryTheory.Adjunction.Triple
/-- For an adjoint triple `F ⊣ G ⊣ H` where `F` and `H` are fully faithful, the natural
transformation `H.op ⟶ F.op` obtained from the dual adjoint triple `H.op ⊣ G.op ⊣ F.op` is
dual to the natural transformation `F ⟶ H`.  -/
CategoryTheory.Adjunction.Triple.leftToRight_op : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [inst_2 : F.Full] [inst_3 : F.Faithful]
  [inst_4 : H.Full] [inst_5 : H.Faithful], t.op.leftToRight = CategoryTheory.NatTrans.op t.leftToRight
-- Mathlib.Geometry.Group.Growth.QuotientInter
Finset.card_nsmul_quotient_add_nsmul_inter_addSubgroup_le : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {H : AddSubgroup G}
  [inst_2 : DecidablePred fun x => x ∈ H] [inst_3 : H.Normal] {A : Finset G} {m n : ℕ},
  (Finset.image (⇑(QuotientAddGroup.mk' H)) (m • A)).card * {x ∈ n • A | x ∈ H}.card ≤ ((m + n) • A).card
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory}
  {f g : X ⟶ Y}, f = g ↔ f.hom = g.hom
-- Mathlib.Algebra.Ring.Basic
noZeroDivisors_iff_isDomain_or_subsingleton : ∀ (α : Type u_3) [inst : Ring α], NoZeroDivisors α ↔ IsDomain α ∨ Subsingleton α
-- Init.Data.Nat.Div.Basic
Nat.div_lt_self : ∀ {n k : ℕ}, 0 < n → 1 < k → n / k < n
-- Mathlib.Data.Vector3
vectorAllP_iff_forall : ∀ {α : Type u_1} {n : ℕ} (p : α → Prop) (v : Vector3 α n), VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
threeGPFree_insert_of_lt : ∀ {α : Type u_2} [inst : CommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelMonoid α] {s : Set α} {a : α},
  (∀ i ∈ s, i < a) →
    (ThreeGPFree (insert a s) ↔ ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b)
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.mem_transvections : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {f : Module.Dual R V}
  {v : V} (hfv : f v = 0), LinearEquiv.transvection hfv ∈ LinearEquiv.transvections R V
-- Mathlib.Logic.Equiv.Defs
Equiv.permCongr_symm : ∀ {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β'), e.permCongr.symm = e.symm.permCongr
-- Mathlib.Topology.Algebra.UniformConvergence
UniformFun.toFun_pow : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Pow β M] (c : M) (f : UniformFun α β),
  UniformFun.toFun (f ^ c) = UniformFun.toFun f ^ c
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁)
  (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃)
  (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
  (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f),
  CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).inv (F.mapComp' f₀₁ f₁₃ f ⋯).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom
        (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv))
-- Init.Data.List.Nat.TakeDrop
/-- Taking the first `l₁.length + i` elements in `l₁ ++ l₂` is the same as appending the first
`i` elements of `l₂` to `l₁`.  -/
List.take_length_add_append : ∀ {α : Type u_1} {l₁ l₂ : List α} (i : ℕ), List.take (l₁.length + i) (l₁ ++ l₂) = l₁ ++ List.take i l₂
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.coe_sup : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s t : TopologicalSpace.CompactOpens α), ↑(s ⊔ t) = ↑s ∪ ↑t
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.isometry : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), Isometry ⇑e
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.codeSupp'_supports : ∀ {S : Finset Turing.PartrecToTM2.Λ'} {c : Turing.ToPartrec.Code} {k : Turing.PartrecToTM2.Cont'},
  Turing.PartrecToTM2.codeSupp c k ⊆ S → Turing.PartrecToTM2.Supports (Turing.PartrecToTM2.codeSupp' c k) S
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.quotMapOfEquivQuotMapCMapMk_mk : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (f : Polynomial R) (x : AdjoinRoot f),
  (AdjoinRoot.quotMapOfEquivQuotMapCMapMk I f) ((Ideal.Quotient.mk (Ideal.map (AdjoinRoot.of f) I)) x) =
    (Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (Ideal.span {f})) (Ideal.map Polynomial.C I))) x
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.isOpenEmbedding_mk_symm : ∀ {M : Type u_1} [inst : TopologicalSpace M], Topology.IsOpenEmbedding ⇑DomAddAct.mk.symm
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.nat_add_eq : ∀ {a : Cardinal.{u_1}} (n : ℕ), Cardinal.aleph0 ≤ a → ↑n + a = a
-- Mathlib.RingTheory.ChainOfDivisors
map_prime_of_factor_orderIso : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {N : Type u_2} [inst_2 : CommMonoidWithZero N]
  [UniqueFactorizationMonoid N] [inst_4 : UniqueFactorizationMonoid M] {m p : Associates M} {n : Associates N},
  n ≠ 0 →
    ∀ (hp : p ∈ UniqueFactorizationMonoid.normalizedFactors m) (d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)), Prime ↑(d ⟨p, ⋯⟩)
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.size_merge : ∀ {α : Type u_1} (le : α → α → Bool) {s₁ s₂ : Batteries.PairingHeapImp.Heap α},
  s₁.NoSibling → s₂.NoSibling → (Batteries.PairingHeapImp.Heap.merge le s₁ s₂).size = s₁.size + s₂.size
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
CategoryTheory.ObjectProperty.IsClosedUnderFiniteProducts.mk' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C}
  [CategoryTheory.Limits.HasFiniteProducts C] [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})]
  [P.IsClosedUnderBinaryProducts], P.IsClosedUnderFiniteProducts
-- Lean.Data.Lsp.Basic
/-- The identifier of the actual command handler.  -/
Lean.Lsp.Command.command : Lean.Lsp.Command → String
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisorAt.mod_add : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I)
  (f f' : PowerSeries A) [inst_1 : IsAdicComplete I A], H.mod (f + f') = H.mod f + H.mod f'
-- Mathlib.Algebra.Order.Group.Lattice
div_inf : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] [MulLeftMono α] [MulRightMono α] (a b c : α),
  c / (a ⊓ b) = c / a ⊔ c / b
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.of.injEq : ∀ (carrier : Type u) [str : MeasurableSpace carrier] (carrier_1 : Type u) (str_1 : MeasurableSpace carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.cast.eq_1 : ∀ {ι : Type u_9} {M : ι → Type u_10} [inst : (i : ι) → Mul (M i)] {i j : ι} (h : i = j),
  MulEquiv.cast h = { toEquiv := Equiv.cast ⋯, map_mul' := ⋯ }
-- Mathlib.RingTheory.PowerSeries.WellKnown
PowerSeries.invOneSubPow.eq_1 : ∀ (S : Type u_1) [inst : CommRing S], PowerSeries.invOneSubPow S 0 = 1
-- Mathlib.Data.Finset.Image
/-- Variant of `Finset.image_inj` under an `InjOn` rather than `Injective` hypothesis.  -/
Finset.image_eq_image_iff_of_injOn : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s s₁ s₂ : Finset α},
  Set.InjOn f ↑s → s₁ ⊆ s → s₂ ⊆ s → (Finset.image f s₁ = Finset.image f s₂ ↔ s₁ = s₂)
-- Lean.Meta.Basic
/-- Replace occurrences of the free variables `fvars` in `e` with `vs`.
Similar to `Expr.replaceFVars`, but handles metavariables correctly.
 -/
Lean.Expr.replaceFVarsM : Lean.Expr → Array Lean.Expr → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
/-- The points of a face of a simplex are given by `mono_of_fin`.  -/
Affine.Simplex.face_points : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} (s : Affine.Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1)
  (i : Fin (m + 1)), (s.face h).points i = s.points ((fs.orderEmbOfFin h) i)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.coe_coe_fst : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] (e' : Bundle.Trivialization F Bundle.TotalSpace.proj) {b : B}
  {y : E b}, b ∈ e'.baseSet → (↑e' ⟨b, y⟩).1 = b
-- Mathlib.Algebra.Group.Hom.Basic
negAddMonoidHom_apply : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a : α), negAddMonoidHom a = -a
-- Mathlib.CategoryTheory.Category.RelCat
CategoryTheory.RelCat.Hom.rel_id_apply₂ : ∀ {X : CategoryTheory.RelCat} (x y : X), (x, y) ∈ (CategoryTheory.CategoryStruct.id X).rel ↔ x = y
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey?_modify_self : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} {k : α}
  {f : β → β}, (Std.DTreeMap.Const.modify t k f).getKey? k = if k ∈ t then some k else none
-- Lean.Meta.Tactic.Grind.Arith.Simproc
Lean.Meta.Grind.Arith.normNatSubInst : Lean.Meta.Simp.DSimproc
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.instOneValueGroup : (A : Type u) →
  [inst : CommRing A] → (K : Type v) → [inst_1 : Field K] → [inst_2 : Algebra A K] → One (ValuationRing.ValueGroup A K)
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.RepresentableBy.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C}
  [inst_1 : SizeOf C] (homEquiv : {X : C} → (X ⟶ Y) ≃ F.obj (Opposite.op X))
  (homEquiv_comp :
    autoParam
      (∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y),
        homEquiv (CategoryTheory.CategoryStruct.comp f g) =
          (CategoryTheory.ConcreteCategory.hom (F.map f.op)) (homEquiv g))
      CategoryTheory.Functor.RepresentableBy.homEquiv_comp._autoParam),
  sizeOf { homEquiv := homEquiv, homEquiv_comp := homEquiv_comp } = 1
-- Mathlib.LinearAlgebra.RootSystem.Reduced
RootPairing.pairingIn_one_four_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_5)
  (i j : ι) [Finite ι] [CharZero R] [IsDomain R] [Module.IsTorsionFree R M] [inst_9 : CommRing S]
  [inst_10 : Algebra S R] [FaithfulSMul S R] [inst_12 : P.IsValuedIn S] [Module.IsTorsionFree R N],
  P.pairingIn S i j = 1 ∧ P.pairingIn S j i = 4 ↔ P.root j = 2 • P.root i
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.units_smul_v : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {R : Type u_1}
  [inst_2 : Ring R] [inst_3 : CategoryTheory.Linear R C] {F G : CochainComplex C ℤ} {n : ℤ} (k : Rˣ)
  (z : CochainComplex.HomComplex.Cochain F G n) (p q : ℤ) (hpq : p + n = q), (k • z).v p q hpq = k • z.v p q hpq
-- Mathlib.Util.Simp
/-- `Qq` version of `Lean.Meta.Simp.Methods.discharge?`, which avoids having to use `~q` matching
on the proof expression returned by `discharge?`

`dischargeQ? (a : Q(Prop))` attempts to prove `a` using the discharger, returning
`some (pf : Q(a))` if a proof is found and `none` otherwise.  -/
Lean.Meta.Simp.Methods.dischargeQ? : Lean.Meta.Simp.Methods → (a : Q(Prop)) → Lean.Meta.SimpM (Option Q(«$a»))
-- Mathlib.Analysis.Calculus.FDeriv.Pow
/-- Eta-expanded form of `fderiv_pow'` -/
fderiv_fun_pow' : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAlgebra 𝕜 𝔸] [inst_4 : NormedSpace 𝕜 E] {f : E → 𝔸} {x : E} (n : ℕ),
  DifferentiableAt 𝕜 f x →
    fderiv 𝕜 (fun i => f i ^ n) x = ∑ i ∈ Finset.range n, MulOpposite.op (f x ^ i) • f x ^ (n.pred - i) • fderiv 𝕜 f x
-- Mathlib.Topology.MetricSpace.Pseudo.Pi
dist_pi_le_iff' : ∀ {β : Type u_2} {X : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (X b)] [Nonempty β]
  {f g : (b : β) → X b} {r : ℝ}, dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.instSMulCommClass' : ∀ {R' : Type u'} {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] {S : NonUnitalSubalgebra R A} [inst_3 : Semiring R'] [inst_4 : SMul R' R] [inst_5 : Module R' A]
  [inst_6 : IsScalarTower R' R A] [SMulCommClass R' R A], SMulCommClass R' R ↥S
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.reflectionPerm_eq_reflectionPerm_iff_of_span : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i j : ι),
  P.reflectionPerm i = P.reflectionPerm j ↔
    ∀ x ∈ Submodule.span R (Set.range ⇑P.root), (P.reflection i) x = (P.reflection j) x
-- Mathlib.CategoryTheory.Limits.FullSubcategory
/-- If `P` is closed under limits of shape `J`, then the inclusion creates such limits.  -/
CategoryTheory.Limits.createsLimitFullSubcategoryInclusionOfClosed : (J : Type w) →
  [inst : CategoryTheory.Category.{w', w} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (P : CategoryTheory.ObjectProperty C) →
          [P.IsClosedUnderLimitsOfShape J] →
            (F : CategoryTheory.Functor J P.FullSubcategory) →
              [CategoryTheory.Limits.HasLimit (F.comp P.ι)] → CategoryTheory.CreatesLimit F P.ι
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.isEmpty_takeWhile_dropWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice}, ((s.dropWhile pat).takeWhile pat).isEmpty = true
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.Term.varFinset.match_1.splitter : {L : FirstOrder.Language} →
  {α : Type u_3} →
    (motive : L.Term α → Sort u_4) →
      (x : L.Term α) →
        ((i : α) → motive (FirstOrder.Language.var i)) →
          ((l : ℕ) → (_f : L.Functions l) → (ts : Fin l → L.Term α) → motive (FirstOrder.Language.func _f ts)) →
            motive x
-- Mathlib.Order.LiminfLimsup
Filter.limsInf_bot : ∀ {α : Type u_1} [inst : CompleteLattice α], ⊥.limsInf = ⊤
-- Mathlib.Topology.Algebra.Group.TopologicalAbelianization
TopologicalAbelianization.commGroup : (G : Type u_1) →
  [inst : Group G] →
    [inst_1 : TopologicalSpace G] → [inst_2 : IsTopologicalGroup G] → CommGroup (TopologicalAbelianization G)
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
/-- In a `NonPreadditiveAbelian` category, an epi is the cokernel of its kernel. More precisely:
If `f` is an epimorphism and `s` is some limit kernel cone on `f`, then `f` is a cokernel
of `Fork.ι s`.  -/
CategoryTheory.NonPreadditiveAbelian.epiIsCokernelOfKernel : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.NonPreadditiveAbelian C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          [CategoryTheory.Epi f] →
            (s : CategoryTheory.Limits.Fork f 0) →
              CategoryTheory.Limits.IsLimit s →
                CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ f ⋯)
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key in the tree map, returning `none` if the
map is empty.
 -/
Std.ExtTreeMap.maxEntry? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → Option (α × β)
-- Init.Data.SInt.Lemmas
Int64.ofBitVec_sdiv : ∀ (a b : BitVec 64), Int64.ofBitVec (a.sdiv b) = Int64.ofBitVec a / Int64.ofBitVec b
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.quotQuotEquivQuotSupₐ_toRingEquiv : ∀ (R : Type u) {A : Type u_1} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (I J : Ideal A),
  (DoubleQuot.quotQuotEquivQuotSupₐ R I J).toRingEquiv = DoubleQuot.quotQuotEquivQuotSup I J
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.hasColimit_iff_hasInitial_cocone : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C),
  CategoryTheory.Limits.HasColimit F ↔ CategoryTheory.Limits.HasInitial (CategoryTheory.Limits.Cocone F)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instDivInvOneMonoidOfMulOpposite.eq_1 : ∀ {M : Type u_1} [inst : DivInvOneMonoid Mᵐᵒᵖ], DomMulAct.instDivInvOneMonoidOfMulOpposite = inst
-- Std.Data.Internal.List.Associative
Std.Internal.List.eraseKey_cons_of_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k k' : α} {v' : β k'},
  (k' == k) = false → Std.Internal.List.eraseKey k (⟨k', v'⟩ :: l) = ⟨k', v'⟩ :: Std.Internal.List.eraseKey k l
-- Mathlib.MeasureTheory.SetSemiring
/-- **Alias** of `MeasureTheory.IsSetSemiring.exists_finpartition_sdiff`. -/
MeasureTheory.IsSetSemiring.exists_finpartition_diff : ∀ {α : Type u_1} {C : Set (Set α)} {s t : Set α}, MeasureTheory.IsSetSemiring C → s ∈ C → t ∈ C → ∃ P, ↑P.parts ⊆ C
-- Lean.Environment
_private.Lean.Environment.0.Lean.PersistentEnvExtension.getModuleIREntries.unsafe_1 : {α β σ : Type} → [Inhabited σ] → Lean.PersistentEnvExtension α β σ → Lean.Environment → Lean.ModuleIdx → Array α
-- Mathlib.Order.Compare
Eq.cmp_eq_eq' : ∀ {α : Type u_1} [inst : LinearOrder α] {x y : α}, x = y → cmp y x = Ordering.eq
-- Mathlib.Algebra.CubicDiscriminant
Cubic.degree_of_a_ne_zero' : ∀ {R : Type u_1} {a b c d : R} [inst : Semiring R], a ≠ 0 → { a := a, b := b, c := c, d := d }.toPoly.degree = 3
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.ofGradedObject_X_d : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂)
  (X : CategoryTheory.GradedObject (I₁ × I₂) C) (d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂))
  (d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂'))
  (shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0)
  (shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0)
  (d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), CategoryTheory.CategoryStruct.comp (d₁ i₁ i₁' i₂) (d₁ i₁' i₁'' i₂) = 0)
  (d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), CategoryTheory.CategoryStruct.comp (d₂ i₁ i₂ i₂') (d₂ i₁ i₂' i₂'') = 0)
  (comm :
    ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂),
      CategoryTheory.CategoryStruct.comp (d₁ i₁ i₁' i₂) (d₂ i₁' i₂ i₂') =
        CategoryTheory.CategoryStruct.comp (d₂ i₁ i₂ i₂') (d₁ i₁ i₁' i₂'))
  (i₁ : I₁) (i₂ i₂' : I₂),
  ((HomologicalComplex₂.ofGradedObject c₁ c₂ X d₁ d₂ shape₁ shape₂ d₁_comp_d₁ d₂_comp_d₂ comm).X i₁).d i₂ i₂' =
    d₂ i₁ i₂ i₂'
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.HasImage.of_arrow_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  [h : CategoryTheory.Limits.HasImage f.hom] (sq : f ⟶ g) [CategoryTheory.IsIso sq],
  CategoryTheory.Limits.HasImage g.hom
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.hasFiniteIntegral_const_iff_enorm : ∀ {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : ENorm ε] {c : ε},
  ‖c‖ₑ ≠ ⊤ → (MeasureTheory.HasFiniteIntegral (fun x => c) μ ↔ ‖c‖ₑ = 0 ∨ MeasureTheory.IsFiniteMeasure μ)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.isEquiv : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₁ : Type u_3} {Γ₂ : Type u_4}
  [inst_2 : LinearOrderedCommMonoidWithZero Γ₁] [inst_3 : LinearOrderedCommMonoidWithZero Γ₂] (v₁ : Valuation R Γ₁)
  (v₂ : Valuation R Γ₂) [v₁.Compatible] [v₂.Compatible], v₁.IsEquiv v₂
-- Mathlib.FieldTheory.IsPerfectClosure
PerfectRing.lift_lift : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing K] [inst_1 : CommRing L]
  [inst_2 : CommRing M] [inst_3 : CommRing N] (i : K →+* L) (j : K →+* M) (g : L →+* N) (p : ℕ) [inst_4 : ExpChar M p]
  [inst_5 : ExpChar K p] [inst_6 : PerfectRing M p] [inst_7 : IsPRadical i p] [inst_8 : ExpChar L p]
  [inst_9 : ExpChar N p] [inst_10 : IsPRadical g p] [inst_11 : IsPRadical (g.comp i) p],
  PerfectRing.lift g (PerfectRing.lift i j p) p = PerfectRing.lift (g.comp i) j p
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
/-- `c.minpoly` is the minimal polynomial of the conjugates.  -/
ConjRootClass.minpoly : {K : Type u_1} →
  {L : Type u_2} → [inst : Field K] → [inst_1 : Field L] → [inst_2 : Algebra K L] → ConjRootClass K L → Polynomial K
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.instNontrivialMixedSpace : ∀ (K : Type u_1) [inst : Field K] [NumberField K], Nontrivial (NumberField.mixedEmbedding.mixedSpace K)
-- Mathlib.Topology.Algebra.Group.Defs
ContinuousWithinAt.neg : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Neg G]
  [ContinuousNeg G] {f : X → G} {s : Set X} {x : X}, ContinuousWithinAt f s x → ContinuousWithinAt (-f) s x