mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.swap_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  Function.Surjective ⇑(AddMonoid.Coprod.swap M N)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.size_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α},
  List.Pairwise (fun a b => (a == b) = false) l → (Std.ExtDHashMap.Const.unitOfList l).size = l.length
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_le_one : ∀ {a : ENNReal}, a⁻¹ ≤ 1 ↔ 1 ≤ a
-- Batteries.Data.String.Lemmas
String.Pos.Raw.Valid.le_rawEndPos : ∀ {s : String} {p : String.Pos.Raw}, String.Pos.Raw.Valid s p → p ≤ s.rawEndPos
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
_private.Mathlib.MeasureTheory.Function.LpSpace.Basic.0.MeasureTheory.Lp.coeFn_LpToLpOfMeasureLeSMulₗ : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {ν : MeasureTheory.Measure α} {c : ENNReal} (hc : c ≠ ⊤)
  (h : μ ≤ c • ν) (f : ↥(MeasureTheory.Lp E p ν)), ↑↑((MeasureTheory.Lp.LpToLpOfMeasureLeSMulₗ✝ hc h) f) =ᵐ[μ] ↑↑f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- The duality equivalence `WalkingCospanᵒᵖ ≌ WalkingSpan`  -/
CategoryTheory.Limits.walkingCospanOpEquiv : CategoryTheory.Limits.WalkingCospanᵒᵖ ≌ CategoryTheory.Limits.WalkingSpan
-- Mathlib.Order.WithBot
WithTop.toDual_apply_coe : ∀ {α : Type u_1} (a : α), WithTop.toDual ↑a = ↑(OrderDual.toDual a)
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintLabelPart.tooltip? : Lean.Elab.InlayHintLabelPart → Option String
-- Mathlib.Algebra.Exact.Basic
LinearMap.exact_of_comp_eq_zero_of_ker_le_range : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P}, g ∘ₗ f = 0 → g.ker ≤ f.range → Function.Exact ⇑f ⇑g
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.eq_of_one_to_two' : ∀ (f : { len := 1 } ⟶ { len := 2 }),
  f = SimplexCategory.δ 0 ∨
    f = SimplexCategory.δ 1 ∨ f = SimplexCategory.δ 2 ∨ ∃ a, f = { len := 1 }.const { len := 2 } a
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normalCore_eq_iInf_map_conj : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.normalCore = ⨅ g, Subgroup.map (↑(MulAut.conj g)) H
-- Mathlib.AlgebraicTopology.SimplicialNerve
/-- A path from `i` to `j` in a linear order `J` is a subset of the interval `[i, j]` in `J` containing
the endpoints.
 -/
CategoryTheory.SimplicialThickening.Path : {J : Type u_1} → [LinearOrder J] → J → J → Type u_1
-- Mathlib.CategoryTheory.Presentable.Directed
/-- The union of a `κ`-bounded family of `κ`-bounded diagrams.  -/
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.iSup : {J : Type w} →
  [inst : CategoryTheory.SmallCategory J] →
    {κ : Cardinal.{w}} →
      [Fact κ.IsRegular] →
        {ι : Type u_1} →
          (ι → CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ) →
            HasCardinalLT ι κ → CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ
-- Mathlib.Order.Monotone.Basic
StrictMonoOn.le_iff_le : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictMonoOn f s → ∀ {a b : α}, a ∈ s → b ∈ s → (f a ≤ f b ↔ a ≤ b)
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
CategoryTheory.Mono.of_binaryCoproductDisjoint_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.BinaryCoproductDisjoint X Y]
  {Z : C} (f : X ⟶ Z) {g : Y ⟶ Z} (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk f g)),
  CategoryTheory.Mono g
-- Mathlib.Order.Notation
/-- Heyting negation `￢` 

Conventions for notations in identifiers:

 * The recommended spelling of `￢` in identifiers is `hnot`. -/
HNot.hnot : {α : Type u_1} → [self : HNot α] → α → α
-- Mathlib.Tactic.Nontriviality.Core
Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim : ∀ {p : Prop} {α : Type u}, (Subsingleton α → p) → (Nontrivial α → p) → p
-- Lean.Class
Lean.ClassEntry.mk.injEq : ∀ (name : Lean.Name) (outParams outLevelParams : Array ℕ) (name_1 : Lean.Name) (outParams_1 outLevelParams_1 : Array ℕ),
  ({ name := name, outParams := outParams, outLevelParams := outLevelParams } =
      { name := name_1, outParams := outParams_1, outLevelParams := outLevelParams_1 }) =
    (name = name_1 ∧ outParams = outParams_1 ∧ outLevelParams = outLevelParams_1)
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- The linarith monad extends an exceptional monad with a `LinarithData` state.
An exception produces a contradictory `PComp`.
 -/
Mathlib.Tactic.Linarith.LinarithM : Type → Type
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- An intermediate field is closed under scalar multiplication.  -/
IntermediateField.smul_mem : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  {y : L}, y ∈ S → ∀ {x : K}, x • y ∈ S
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.MutualClosure.FixPoint.isModified : Lean.Elab.Term.MutualClosure.FixPoint.M Bool
-- Mathlib.Order.Fin.Tuple
Fin.snocOrderIso_apply : ∀ {n : ℕ} (α : Fin (n + 1) → Type u_2) [inst : (i : Fin (n + 1)) → LE (α i)]
  (f : α (Fin.last n) × ((i : Fin n) → α i.castSucc)) (x : Fin (n + 1)), (Fin.snocOrderIso α) f x = Fin.snoc f.2 f.1 x
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.deleteEdges_spanningCoe_eq : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (s : Set (Sym2 V)),
  G'.spanningCoe.deleteEdges s = (G'.deleteEdges s).spanningCoe
-- Mathlib.Tactic.Simps.Basic
Simps.Config.mk.injEq : ∀ (isSimp : Bool) (attrs : Array Lean.Elab.Attribute) (simpRhs dsimpLhs : Bool)
  (typeMd rhsMd : Lean.Meta.TransparencyMode) (fullyApplied : Bool) (notRecursive : List Lean.Name) (debug : Bool)
  (nameStem : Option String) (isSimp_1 : Bool) (attrs_1 : Array Lean.Elab.Attribute) (simpRhs_1 dsimpLhs_1 : Bool)
  (typeMd_1 rhsMd_1 : Lean.Meta.TransparencyMode) (fullyApplied_1 : Bool) (notRecursive_1 : List Lean.Name)
  (debug_1 : Bool) (nameStem_1 : Option String),
  ({ isSimp := isSimp, attrs := attrs, simpRhs := simpRhs, dsimpLhs := dsimpLhs, typeMd := typeMd, rhsMd := rhsMd,
        fullyApplied := fullyApplied, notRecursive := notRecursive, debug := debug, nameStem := nameStem } =
      { isSimp := isSimp_1, attrs := attrs_1, simpRhs := simpRhs_1, dsimpLhs := dsimpLhs_1, typeMd := typeMd_1,
        rhsMd := rhsMd_1, fullyApplied := fullyApplied_1, notRecursive := notRecursive_1, debug := debug_1,
        nameStem := nameStem_1 }) =
    (isSimp = isSimp_1 ∧
      attrs = attrs_1 ∧
        simpRhs = simpRhs_1 ∧
          dsimpLhs = dsimpLhs_1 ∧
            typeMd = typeMd_1 ∧
              rhsMd = rhsMd_1 ∧
                fullyApplied = fullyApplied_1 ∧ notRecursive = notRecursive_1 ∧ debug = debug_1 ∧ nameStem = nameStem_1)
-- Batteries.Data.Fin.Basic
Fin.dfoldlM.loop.eq_def : ∀ {m : Type u_1 → Type u_2} [inst : Monad m] (n : ℕ) (α : Fin (n + 1) → Type u_1)
  (f : (i : Fin n) → α i.castSucc → m (α i.succ)) (i : ℕ) (h : i < n + 1) (x : α ⟨i, h⟩),
  Fin.dfoldlM.loop n α f i h x =
    if h' : i < n then f ⟨i, h'⟩ x >>= Fin.dfoldlM.loop n α f (i + 1) ⋯ else cast ⋯ (pure x)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- `evalOp(F)` restricted to the original category (via `incl`) is the original presheaf `F`.  -/
CategoryTheory.Limits.FormalCoproduct.evalOpCompInlIsoId : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    (A : Type u₁) →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_2 : CategoryTheory.Limits.HasProducts A] →
          (CategoryTheory.Limits.FormalCoproduct.evalOp C A).comp
              ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ (CategoryTheory.Limits.FormalCoproduct C)ᵒᵖ A).obj
                (CategoryTheory.Limits.FormalCoproduct.incl C).op) ≅
            CategoryTheory.Functor.id (CategoryTheory.Functor Cᵒᵖ A)
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.prodFun_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (φ : ImplicitFunctionData 𝕜 E F G) (x : E),
  φ.prodFun x = (φ.leftFun x, φ.rightFun x)
-- Init.Data.String.Basic
/-- Advances the position `p` `n` times.

If this would move `p` past the end of `s`, the result is `s.endPos`.
 -/
String.Slice.Pos.nextn : {s : String.Slice} → s.Pos → ℕ → s.Pos
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofCommaFstEquivalence_inverse : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C),
  (CategoryTheory.CostructuredArrow.ofCommaFstEquivalence F G c).inverse =
    CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse F G c
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.erase_empty : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {k : α}, ∅.erase k = ∅
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the smallest key that is greater than or equal to the
given key, returning `fallback` if no such key exists.
 -/
Std.ExtTreeMap.getKeyGED : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → α → α
-- Mathlib.Data.Multiset.Range
Multiset.coe_range : ∀ (n : ℕ), ↑(List.range n) = Multiset.range n
-- Mathlib.Algebra.Lie.SerreConstruction
CartanMatrix.Generators.E : {B : Type v} → B → CartanMatrix.Generators B
-- Mathlib.Algebra.Category.Ring.Colimits
/-- An inductive type representing all ring expressions (without Relations)
on a collection of types indexed by the objects of `J`.
 -/
RingCat.Colimits.Prequotient : {J : Type v} → [inst : CategoryTheory.SmallCategory J] → CategoryTheory.Functor J RingCat → Type v
-- Mathlib.LinearAlgebra.AffineSpace.Basis
/-- Composition of an affine basis and an equivalence of index types.  -/
AffineBasis.reindex : {ι : Type u_1} →
  {ι' : Type u_2} →
    {k : Type u_5} →
      {V : Type u_6} →
        {P : Type u_7} →
          [inst : AddCommGroup V] →
            [inst_1 : AddTorsor V P] →
              [inst_2 : Ring k] → [inst_3 : Module k V] → AffineBasis ι k P → ι ≃ ι' → AffineBasis ι' k P
-- Mathlib.Data.List.NodupEquivFin
List.Nodup.getEquivOfForallMemList_apply : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (nd : l.Nodup) (h : ∀ (x : α), x ∈ l) (i : Fin l.length),
  (List.Nodup.getEquivOfForallMemList l nd h) i = l.get i
-- Mathlib.Data.Nat.Cast.Order.Field
Nat.one_div_cast_pos : ∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {n : ℕ}, n ≠ 0 → 0 < 1 / ↑n
-- Mathlib.Tactic.ClickSuggestions.Apply
Mathlib.Tactic.ClickSuggestions.instInhabitedApplyKey.default : Mathlib.Tactic.ClickSuggestions.ApplyKey
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Delaborates a function application in the standard mode, where implicit arguments are generally not
included, unless `pp.analysis.namedArg` is set at that argument.

This delaborator is where `app_unexpander`s and the structure instance unexpander are applied, if `unexpand` is true.
When `unexpand` is true, also considers opportunities for field notation, which takes priority over other unexpanders.

Assumes `numArgs ≤ paramKinds.size`.
 -/
Lean.PrettyPrinter.Delaborator.delabAppImplicitCore : Bool →
  ℕ →
    Lean.PrettyPrinter.Delaborator.Delab →
      Array Lean.PrettyPrinter.Delaborator.ParamKind → Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
/-- The derivative of `expMapBasis`, see `hasFDerivAt_expMapBasis`.
 -/
NumberField.mixedEmbedding.fundamentalCone.fderiv_expMapBasis : (K : Type u_1) →
  [inst : Field K] →
    [NumberField K] →
      NumberField.mixedEmbedding.realSpace K →
        NumberField.mixedEmbedding.realSpace K →L[ℝ] NumberField.mixedEmbedding.realSpace K
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.HeightOneSpectrum.adicAbv_natCast_le_one`.

---

The `v`-adic absolute value of a natural number is `≤ 1`.  -/
NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_natCast_le_one : ∀ (K : Type u_1) [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R] (n : ℕ), (NumberField.HeightOneSpectrum.adicAbv K v) ↑n ≤ 1
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.intValuation_def : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {r : R},
  v.intValuation r =
    if r = 0 then 0 else WithZero.exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors))
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Functor.pi_obj : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : I → Type u₂}
  [inst_1 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] (F : (i : I) → CategoryTheory.Functor (C i) (D i))
  (f : (i : I) → C i) (i : I), (CategoryTheory.Functor.pi F).obj f i = (F i).obj (f i)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.hasFPowerSeriesOnBall_weierstrassP : ∀ (L : PeriodPair) (x : ℂ) (r : NNReal),
  0 < r → Metric.closedBall x ↑r ⊆ (↑L.lattice)ᶜ → HasFPowerSeriesOnBall L.weierstrassP (L.weierstrassPSeries x) x ↑r
-- Mathlib.Data.Finset.NAry
Fintype.piFinset_image₂ : ∀ {ι : Type u_14} {α : ι → Type u_15} {β : ι → Type u_16} {γ : ι → Type u_17} [inst : DecidableEq ι]
  [inst_1 : Fintype ι] [inst_2 : (i : ι) → DecidableEq (γ i)] (f : (i : ι) → α i → β i → γ i)
  (s : (i : ι) → Finset (α i)) (t : (i : ι) → Finset (β i)),
  (Fintype.piFinset fun i => Finset.image₂ (f i) (s i) (t i)) =
    Finset.image₂ (fun a b i => f i (a i) (b i)) (Fintype.piFinset s) (Fintype.piFinset t)
-- Mathlib.CategoryTheory.Extensive
/-- In a finitary extensive category, all coproducts are van Kampen  -/
CategoryTheory.FinitaryExtensive.van_kampen' : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.FinitaryExtensive C] {X Y : C}
  (c : CategoryTheory.Limits.BinaryCofan X Y) (a : CategoryTheory.Limits.IsColimit c),
  CategoryTheory.IsVanKampenColimit c
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.gMulHom_apply_apply : ∀ {ι : Type u_1} (A : ι → Type u_2) [inst : Add ι] [inst_1 : (i : ι) → AddCommMonoid (A i)]
  [inst_2 : DirectSum.GNonUnitalNonAssocSemiring A] {i j : ι} (a : A i) (b : A j),
  ((DirectSum.gMulHom A) a) b = GradedMonoid.GMul.mul a b
-- Lean.Meta.Tactic.Grind.Split
_private.Lean.Meta.Tactic.Grind.Split.0.Lean.Meta.Grind.SplitCandidate.some.sizeOf_spec : ∀ (c : Lean.Meta.Grind.SplitInfo) (numCases : ℕ) (isRec tryPostpone : Bool),
  sizeOf (Lean.Meta.Grind.SplitCandidate.some✝ c numCases isRec tryPostpone) =
    1 + sizeOf c + sizeOf numCases + sizeOf isRec + sizeOf tryPostpone
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.SimprocDeclExtState.newEntries : Lean.Meta.Simp.SimprocDeclExtState → Lean.PHashMap Lean.Name (Array Lean.Meta.SimpTheoremKey)
-- Mathlib.Order.Interval.Set.Basic
Set.decidableMemIoi : {α : Type u_1} → [inst : Preorder α] → {b x : α} → [Decidable (b < x)] → Decidable (x ∈ Set.Ioi b)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.coe_refl' : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁], ⇑(ContinuousLinearEquiv.refl R₁ M₁) = id
-- Init.Data.Int.DivMod.Lemmas
Int.neg_mul_fmod_left : ∀ (a b : ℤ), (-(a * b)).fmod b = 0
-- Batteries.Data.UnionFind.Basic
/-- Root of a union-find node.  -/
Batteries.UnionFind.root : (self : Batteries.UnionFind) → Fin self.size → Fin self.size
-- Init.Data.Nat.Basic
Nat.sub_lt_sub_left : ∀ {k m n : ℕ}, k < m → k < n → m - n < m - k
-- Lean.Elab.Tactic.Basic
/-- A tactic is a function from syntax to an action in the tactic monad.

A given tactic syntax kind may have multiple `Tactic`s associated with it, all of which will be
attempted until one succeeds.
 -/
Lean.Elab.Tactic.Tactic : Type
-- Mathlib.Data.ENat.Basic
ENat.toNat_le_toNat : ∀ {m n : ℕ∞}, m ≤ n → n ≠ ⊤ → m.toNat ≤ n.toNat
-- Mathlib.Topology.Semicontinuity.Defs
lowerSemicontinuousWithinAt_univ_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {x : α},
  LowerSemicontinuousWithinAt f Set.univ x ↔ LowerSemicontinuousAt f x
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestRevMatchAtChain_iff : ∀ {pat s : String.Slice} {pos₁ pos₂ : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAtChain pat pos₁ pos₂ ↔
    ∃ (h : pos₁ ≤ pos₂), ∃ n, (s.slice pos₁ pos₂ h).copy = String.join (List.replicate n pat.copy)
-- Mathlib.Analysis.Normed.Module.WeakDual
/-- The weak-\* closure of a norm-bounded set is norm-bounded, because norm-closed balls
are weak-\* closed.  -/
WeakDual.isBounded_closure : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set (WeakDual 𝕜 E)}, Bornology.IsBounded s → Bornology.IsBounded (closure s)
-- Mathlib.Topology.UniformSpace.Equiv
/-- Uniform isomorphism between `α` and `β`  -/
UniformEquiv : (α : Type u_4) → (β : Type u_5) → [UniformSpace α] → [UniformSpace β] → Type (max u_4 u_5)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.darts_injective : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, Function.Injective SimpleGraph.Walk.darts
-- Lean.Meta.LetToHave
/-- When checking, makes sure that `r.type?` is of the form `Expr.sort _`.
 -/
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.ensureType : Lean.Meta.LetToHave.Result✝ → Lean.Meta.LetToHave.M✝ Lean.Meta.LetToHave.Result✝
-- Mathlib.Topology.VectorBundle.Basic
/-- This structure permits to define a vector bundle when trivializations are given as local
equivalences but there is not yet a topology on the total space or the fibers.
The total space is hence given a topology in such a way that there is a fiber bundle structure for
which the partial equivalences are also open partial homeomorphisms and hence vector bundle
trivializations. The topology on the fibers is induced from the one on the total space.

The field `exists_coordChange` is stated as an existential statement (instead of 3 separate
fields), since it depends on propositional information (namely `e e' ∈ pretrivializationAtlas`).
This makes it inconvenient to explicitly define a `coordChange` function when constructing a
`VectorPrebundle`.  -/
VectorPrebundle : (R : Type u_1) →
  {B : Type u_2} →
    (F : Type u_3) →
      (E : B → Type u_4) →
        [inst : NontriviallyNormedField R] →
          [inst_1 : (x : B) → AddCommMonoid (E x)] →
            [(x : B) → Module R (E x)] →
              [inst_3 : NormedAddCommGroup F] →
                [NormedSpace R F] →
                  [TopologicalSpace B] → [(x : B) → TopologicalSpace (E x)] → Type (max (max u_2 u_3) u_4)
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.isCentralVAdd : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] [inst_2 : VAdd αᵃᵒᵖ β] [IsCentralVAdd α β],
  IsCentralVAdd α (Finset β)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.toArray_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → t₁.toArray = t₂.toArray
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- The alternating group on 3 letters or more acts primitively  -/
alternatingGroup.isPreprimitive_of_three_le_card : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : DecidableEq α],
  3 ≤ Nat.card α → MulAction.IsPreprimitive (↥(alternatingGroup α)) α
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.empty_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {t : Set β}, ∅ +ᵥ t = ∅
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Augmented.toArrow_obj_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented C),
  (CategoryTheory.CosimplicialObject.Augmented.toArrow.obj X).left = X.left
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Presieve.FamilyOfElements.SieveCompatible.cone.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {P : CategoryTheory.Functor Cᵒᵖ A} {X : C} {S : CategoryTheory.Sieve X} {E : Aᵒᵖ}
  {x : CategoryTheory.Presieve.FamilyOfElements (P.comp (CategoryTheory.coyoneda.obj E)) S.arrows}
  (hx : x.SieveCompatible),
  hx.cone =
    { pt := Opposite.unop E, π := (CategoryTheory.Presheaf.conesEquivSieveCompatibleFamily P S E).invFun ⟨x, hx⟩ }
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.vanishingIdeal.eq_1 : ∀ {R : Type u} [inst : CommSemiring R] (t : Set (PrimeSpectrum R)), PrimeSpectrum.vanishingIdeal t = ⨅ x ∈ t, x.asIdeal
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- The angle between a vector and a nonnegative multiple of that vector is 0.  -/
Orientation.oangle_smul_right_self_of_nonneg : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x : V) {r : ℝ}, 0 ≤ r → o.oangle x (r • x) = 0
-- Aesop.Tree.State
Aesop.Goal.isProvenNoCache : Aesop.Goal → BaseIO Bool
-- Init.Data.Array.Lemmas
Array.sum_eq_sum_toList : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Zero α] {as : Array α}, as.toList.sum = as.sum
-- Mathlib.Algebra.Order.Archimedean.Basic
exists_rat_mem_uIoo : ∀ {K : Type u_4} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K},
  x ≠ y → ∃ q, ↑q ∈ Set.uIoo x y
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.transnumAuxSeq.eq_1 : ∀ (f : CircleDeg1Lift) (n : ℕ), f.transnumAuxSeq n = (f ^ 2 ^ n) 0 / 2 ^ n
-- Mathlib.RingTheory.Ideal.Colon
Submodule.colon_empty : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M}, N.colon ∅ = ⊤
-- Mathlib.ModelTheory.Order
FirstOrder.Language.instIsExpansionOnOrderLHomOfOrderedStructureOrder : ∀ {L : FirstOrder.Language} {M : Type w'} [inst : L.IsOrdered] [inst_1 : L.Structure M] [inst_2 : LE M]
  [L.OrderedStructure M] [inst_4 : FirstOrder.Language.order.Structure M]
  [FirstOrder.Language.order.OrderedStructure M], L.orderLHom.IsExpansionOn M
-- Mathlib.Algebra.Group.Prod
Prod.instAddZeroClass.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  Prod.instAddZeroClass = { toZero := Prod.instZero, toAdd := Prod.instAdd, zero_add := ⋯, add_zero := ⋯ }