mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.touchpoint_notMem_affineSpan_of_ne : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs →
    ∀ {i j : Fin (n + 1)}, i ≠ j → s.touchpoint signs i ∉ affineSpan ℝ (Set.range (s.faceOpposite j).points)
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.coe_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] (s : Finset α) (t : Finset β),
  ↑(s • t) = ↑s • ↑t
-- Mathlib.Data.Finmap
Finmap.mem_lookup_iff : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {s : Finmap β} {a : α} {b : β a},
  b ∈ Finmap.lookup a s ↔ ⟨a, b⟩ ∈ s.entries
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α fun x => Unit} [EquivBEq α] [LawfulHashable α]
  {l : List α} {k k' : α},
  (k == k') = true →
    k ∉ m →
      List.Pairwise (fun a b => (a == b) = false) l →
        k ∈ l →
          ∀ {h : k' ∈ Std.DHashMap.Const.insertManyIfNewUnit m l},
            (Std.DHashMap.Const.insertManyIfNewUnit m l).getKey k' h = k
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.norm_map_insertNth_le : ∀ {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 Ei G) {i : Fin (n + 1)}
  (x : Ei i) (m : (j : Fin n) → Ei (i.succAbove j)), ‖f (i.insertNth x m)‖ ≤ ‖f‖ * ‖x‖ * ∏ i_1, ‖m i_1‖
-- Mathlib.CategoryTheory.Subfunctor.Image
/-- Given a morphism `p : F' ⟶ F` of type-valued functors and `G : Subfunctor F`,
this is the morphism from the preimage of `G` by `p` to `G`.  -/
CategoryTheory.Subfunctor.fromPreimage : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F F' : CategoryTheory.Functor C (Type w)} →
      (G : CategoryTheory.Subfunctor F) → (p : F' ⟶ F) → (G.preimage p).toFunctor ⟶ G.toFunctor
-- Init.Data.SInt.Lemmas
Int64.lt_irrefl : ∀ {a : Int64}, ¬a < a
-- Init.Data.SInt.Lemmas
instAssociativeInt16HMul : Std.Associative fun x1 x2 => x1 * x2
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.contains_maxD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {fallback : α}, t.contains (t.maxD fallback) = true
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.piLIE_apply_apply : ∀ (𝕜 : Type u) (E : Type wE) {ι : Type v} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : Fintype ι] {ι' : Type u_1} [inst_4 : Fintype ι'] {F : ι' → Type u_2}
  [inst_5 : (i' : ι') → SeminormedAddCommGroup (F i')] [inst_6 : (i' : ι') → NormedSpace 𝕜 (F i')]
  (a : (i : ι') → E [⋀^ι]→L[𝕜] F i) (m : (i : ι) → (fun x => E) i) (i : ι'),
  ((ContinuousAlternatingMap.piLIE 𝕜 E) a) m i = (a i) m
-- Init.Data.Int.Gcd
Int.gcd_left_eq_iff : ∀ {a a' b : ℤ}, a.gcd b = a'.gcd b ↔ ∀ (c : ℤ), c ∣ b → (c ∣ a ↔ c ∣ a')
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.bilinearComp_apply : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
  {E' : Type u_11} {F' : Type u_12} [inst_9 : SeminormedAddCommGroup E'] [inst_10 : SeminormedAddCommGroup F']
  {𝕜₁' : Type u_13} {𝕜₂' : Type u_14} [inst_11 : NontriviallyNormedField 𝕜₁'] [inst_12 : NontriviallyNormedField 𝕜₂']
  [inst_13 : NormedSpace 𝕜₁' E'] [inst_14 : NormedSpace 𝕜₂' F'] {σ₁' : 𝕜₁' →+* 𝕜} {σ₁₃' : 𝕜₁' →+* 𝕜₃} {σ₂' : 𝕜₂' →+* 𝕜₂}
  {σ₂₃' : 𝕜₂' →+* 𝕜₃} [inst_15 : RingHomCompTriple σ₁' σ₁₃ σ₁₃'] [inst_16 : RingHomCompTriple σ₂' σ₂₃ σ₂₃']
  [inst_17 : RingHomIsometric σ₂₃] [inst_18 : RingHomIsometric σ₁₃'] [inst_19 : RingHomIsometric σ₂₃']
  (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (gE : E' →SL[σ₁'] E) (gF : F' →SL[σ₂'] F) (x : E') (y : F'),
  ((f.bilinearComp gE gF) x) y = (f (gE x)) (gF y)
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
_private.Mathlib.CategoryTheory.Triangulated.SpectralObject.0.CategoryTheory.ComposableArrows.Precomp.map.match_1.eq_1 : ∀ {n : ℕ} (motive : (x x_1 : Fin (n + 1 + 1)) → x ≤ x_1 → Sort u_1) (isLt isLt_1 : 0 < n + 1 + 1)
  (x : ⟨0, isLt⟩ ≤ ⟨0, isLt_1⟩)
  (h_1 : (isLt isLt_2 : 0 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨0, isLt_2⟩) → motive ⟨0, isLt⟩ ⟨0, isLt_2⟩ x)
  (h_2 :
    (isLt : 0 < n + 1 + 1) → (isLt_2 : 1 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨1, isLt_2⟩) → motive ⟨0, isLt⟩ ⟨1, isLt_2⟩ x)
  (h_3 :
    (isLt : 0 < n + 1 + 1) →
      (j : ℕ) → (hj : j + 2 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨j + 2, hj⟩) → motive ⟨0, isLt⟩ ⟨j.succ.succ, hj⟩ x)
  (h_4 :
    (i : ℕ) →
      (hi : i + 1 < n + 1 + 1) →
        (j : ℕ) → (hj : j + 1 < n + 1 + 1) → (hij : ⟨i + 1, hi⟩ ≤ ⟨j + 1, hj⟩) → motive ⟨i.succ, hi⟩ ⟨j.succ, hj⟩ hij),
  (match ⟨0, isLt⟩, ⟨0, isLt_1⟩, x with
    | ⟨0, isLt⟩, ⟨0, isLt_2⟩, x => h_1 isLt isLt_2 x
    | ⟨0, isLt⟩, ⟨1, isLt_2⟩, x => h_2 isLt isLt_2 x
    | ⟨0, isLt⟩, ⟨j.succ.succ, hj⟩, x => h_3 isLt j hj x
    | ⟨i.succ, hi⟩, ⟨j.succ, hj⟩, hij => h_4 i hi j hj hij) =
    h_1 isLt isLt_1 x
-- Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
groupAddGroupEquivalence_inverse : groupAddGroupEquivalence.inverse = AddGrpCat.toGrp
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.mul_eq_eval : ∀ {M : Type u_1} [inst : GroupWithZero M] {l₁ l₂ l : Mathlib.Tactic.FieldSimp.NF M} {x₁ x₂ : M},
  x₁ = l₁.eval → x₂ = l₂.eval → l₁.eval * l₂.eval = l.eval → x₁ * x₂ = l.eval
-- Mathlib.Topology.Separation.Basic
exists_open_singleton_of_finite : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] [Finite X] [Nonempty X], ∃ x, IsOpen {x}
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.instAddLeftMono : AddLeftMono ℚ
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instNonUnitalNonAssocRing : {X : Type u_1} →
  {Y : Type u_2} → [inst : TopologicalSpace X] → [NonUnitalNonAssocRing Y] → NonUnitalNonAssocRing (LocallyConstant X Y)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.toBiconeFunctor_obj_pt : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} (b : CategoryTheory.Limits.BinaryBicone X Y),
  (CategoryTheory.Limits.BinaryBicone.toBiconeFunctor.obj b).pt = b.pt
-- Mathlib.LinearAlgebra.Dimension.Constructions
rank_fun : ∀ {R : Type u} [inst : Semiring R] [StrongRankCondition R] {M η : Type u} [inst_2 : Fintype η]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [Module.Free R M],
  Module.rank R (η → M) = ↑(Fintype.card η) * Module.rank R M
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.IsAdmissible.nil : ∀ (m : ℕ), SimplexCategoryGenRel.IsAdmissible m []
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.any_toList : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] {p : α → β → Bool},
  m.WF → (m.toList.any fun x => p x.1 x.2) = m.any p
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0.Stmt.inhabited : (Γ : Type u_1) → [Inhabited Γ] → Inhabited (Turing.TM0.Stmt Γ)
-- Qq.Typ
Qq.instBEqQuoted : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
-- Init.Data.Slice.List.Lemmas
ListSlice.mkSlice_rcc_eq_mkSlice_rco : ∀ {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ},
  (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = Std.Rco.Sliceable.mkSlice xs lo...hi + 1
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get!_eq_getD_default : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited α] {a : α}, m.get! a = m.getD a default
-- Mathlib.RingTheory.Ideal.GoingUp
/-- `comap (algebraMap R S)` is a surjection from the prime spec of `R` to prime spec of `S`.
`hP : (algebraMap R S).ker ≤ P` is a slight generalization of the extension being injective  -/
Ideal.exists_ideal_over_prime_of_isIntegral_of_isDomain : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDomain S]
  [Algebra.IsIntegral R S] (P : Ideal R) [P.IsPrime],
  RingHom.ker (algebraMap R S) ≤ P → ∃ Q, Q.IsPrime ∧ Ideal.comap (algebraMap R S) Q = P
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.val_neg_add : ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} (h : IsAddUnit a), ↑(-h.addUnit) + a = 0
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
/-- Given `G : M.GeneratingSections`, we naturally obtain `M.LocalGeneratorsData` using the
trivial cover of `C`.  -/
SheafOfModules.GeneratingSections.localGeneratorsData : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] →
            [inst_3 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] →
              [CategoryTheory.Limits.HasBinaryProducts C] →
                [inst_5 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] →
                  {M : SheafOfModules R} → M.GeneratingSections → M.LocalGeneratorsData
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey_eq_get_getKey? : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h : m.WF) {a : α} {h' : a ∈ m}, m.getKey a h' = (m.getKey? a).get ⋯
-- Mathlib.Condensed.Light.Sequence
_private.Mathlib.Condensed.Light.Sequence.0.InternalProjectivityProof.y_apply : ∀ {S : Type u_1} {T : Type u_2} {X : Type u_3} (π : T → S × OnePoint X) (x : ↑(InternalProjectivityProof.S'✝ π)),
  InternalProjectivityProof.y✝ π x = (π ↑(↑x OnePoint.infty)).1
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.simprocs : Lean.Option Bool
-- Init.Data.String.Defs
/-- Encodes a string in UTF-8 as an array of bytes.
 -/
String.toUTF8 : String → ByteArray
-- Mathlib.Dynamics.PeriodicPts.Defs
/-- `(period m a) • m` fixes `a`.  -/
AddAction.nsmul_period_vadd : ∀ {α : Type v} {M : Type u} [inst : AddMonoid M] [inst_1 : AddAction M α] (m : M) (a : α),
  AddAction.period m a • m +ᵥ a = a
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Real.binEntropy_zero : Real.binEntropy 0 = 0
-- Mathlib.GroupTheory.Coxeter.Basic
_private.Mathlib.GroupTheory.Coxeter.Basic.0.CoxeterSystem.alternatingWord.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (m : ℕ) → motive m.succ),
  (match 0 with
    | 0 => h_1 ()
    | m.succ => h_2 m) =
    h_1 ()
-- Mathlib.Analysis.Normed.Affine.AddTorsor
nndist_right_midpoint : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 V]
  [inst_5 : Invertible 2] (p₁ p₂ : P), nndist p₂ (midpoint 𝕜 p₁ p₂) = ‖2‖₊⁻¹ * nndist p₁ p₂
-- Mathlib.Data.Set.Lattice.Image
Set.kernImage_union_preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {t : Set β},
  Set.kernImage f (s ∪ f ⁻¹' t) = Set.kernImage f s ∪ t
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.Trie.node.injEq : ∀ {α : Type} (values : Array α) (star : Option Lean.Meta.RefinedDiscrTree.TrieIndex)
  (labelledStars : Std.HashMap ℕ Lean.Meta.RefinedDiscrTree.TrieIndex)
  (children : Std.HashMap Lean.Meta.RefinedDiscrTree.Key Lean.Meta.RefinedDiscrTree.TrieIndex)
  (pending : Array (Lean.Meta.RefinedDiscrTree.LazyEntry × α)) (values_1 : Array α)
  (star_1 : Option Lean.Meta.RefinedDiscrTree.TrieIndex)
  (labelledStars_1 : Std.HashMap ℕ Lean.Meta.RefinedDiscrTree.TrieIndex)
  (children_1 : Std.HashMap Lean.Meta.RefinedDiscrTree.Key Lean.Meta.RefinedDiscrTree.TrieIndex)
  (pending_1 : Array (Lean.Meta.RefinedDiscrTree.LazyEntry × α)),
  ({ values := values, star := star, labelledStars := labelledStars, children := children, pending := pending } =
      { values := values_1, star := star_1, labelledStars := labelledStars_1, children := children_1,
        pending := pending_1 }) =
    (values = values_1 ∧ star = star_1 ∧ labelledStars = labelledStars_1 ∧ children = children_1 ∧ pending = pending_1)
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.Iterator.extract.eq_1 : ∀ (a : String) (a_1 : String.Pos.Raw) (b : String) (b_1 : String.Pos.Raw),
  { s := a, i := a_1 }.extract { s := b, i := b_1 } =
    if (decide (a ≠ b) || decide (a_1 > b_1)) = true then "" else String.Pos.Raw.extract a a_1 b_1
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- The inner product of two vectors, divided by the product of their
norms, has value 1 if and only if they are nonzero and one is
a positive multiple of the other.  -/
real_inner_div_norm_mul_norm_eq_one_iff : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F),
  inner ℝ x y / (‖x‖ * ‖y‖) = 1 ↔ x ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • x
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isSeparator_unop_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : Cᵒᵖ),
  CategoryTheory.IsSeparator (Opposite.unop G) ↔ CategoryTheory.IsCoseparator G
-- Lean.Meta.Constructions.SparseCasesOn
Lean.Meta.SparseCasesOnInfo.insterestingCtors : Lean.Meta.SparseCasesOnInfo → Array Lean.Name
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α}
  {h' : a ∈ t.erase k}, (t.erase k)[a] = t[a]
-- Mathlib.ModelTheory.PartialEquiv
/-- Given a partial equivalence which has the whole structure as domain and
as codomain, returns the corresponding equivalence.  -/
FirstOrder.Language.PartialEquiv.toEquivOfEqTop : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type w'} →
      [inst : L.Structure M] → [inst_1 : L.Structure N] → {f : L.PartialEquiv M N} → f.dom = ⊤ → f.cod = ⊤ → L.Equiv M N
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
Finset.hasSum_support : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (s : Finset β) (f : β → α)
  (L : optParam (SummationFilter ↑↑s) (SummationFilter.unconditional ↑↑s)) [L.HasSupport]
  [inst_3 : DecidablePred fun x => x ∈ L.support],
  HasSum (f ∘ Subtype.val) (∑ b ∈ Finset.map (Function.Embedding.subtype fun x => x ∈ ↑s) L.support.toFinset, f b) L
-- Mathlib.FieldTheory.Relrank
Subfield.lift_relrank_map_map : ∀ {E : Type v} [inst : Field E] {L : Type w} [inst_1 : Field L] (A B : Subfield E) (f : E →+* L),
  Cardinal.lift.{v, w} ((Subfield.map f A).relrank (Subfield.map f B)) = Cardinal.lift.{w, v} (A.relrank B)
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.Monic.def : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.Monic ↔ p.leadingCoeff = 1
-- Batteries.Control.Nondet.Basic
/-- Find the value of a monadic function on the first alternative in a nondeterministic value
where the function succeeds.
 -/
Nondet.firstM : {σ : Type} →
  {m : Type → Type} →
    [AlternativeMonad m] → [inst : Lean.MonadBacktrack σ m] → {α β : Type} → Nondet m α → (α → m (Option β)) → m β
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
le_iff_exists_add' : ∀ {α : Type u} [inst : AddCommMagma α] [inst_1 : Preorder α] [CanonicallyOrderedAdd α] {a b : α}, a ≤ b ↔ ∃ c, b = c + a
-- Init.Data.String.Lemmas.Pattern.Split.Basic
/-- Splits a slice `s` into subslices from a list of `SearchStep s`.

This is an intermediate step in the verification. The equivalence of
`String.Slice.splitToSubslice` and `splitFromSteps` is pure "iteratorology", while
the equivalence of `splitFromSteps` and `split` is the actual correctness proof for the
splitting routine.
 -/
_private.Init.Data.String.Lemmas.Pattern.Split.Basic.0.String.Slice.Pattern.Model.splitFromSteps : {s : String.Slice} → s.Pos → List (String.Slice.Pattern.SearchStep s) → List s.Subslice
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor_obj_hom : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor T D) (Y : D) (X : T)
  (Y_1 : CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.proj F Y) X),
  ((CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor F Y X).obj Y_1).hom = Y_1.left.hom
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.mulEquivOfLocalizations_left_inv : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) (k : N ≃* P),
  f.mulEquivOfLocalizations (f.ofMulEquivOfLocalizations k) = k
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.minD_le_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, k ∈ t → ∀ {fallback : α}, (cmp (t.minD fallback) k).isLE = true
-- Mathlib.NumberTheory.Fermat
Nat.two_mul_fermatNumber_sub_one_sq_le_fermatNumber_sq : ∀ (n : ℕ), 2 * (n.fermatNumber - 1) ^ 2 ≤ (n + 1).fermatNumber ^ 2
-- Mathlib.Logic.Equiv.PartialEquiv
Equiv.toPartialEquiv_target : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β), e.toPartialEquiv.target = Set.univ
-- Batteries.Data.Fin.Coding
Fin.encodeBool_decodeBool : ∀ (x : Fin 2), Fin.encodeBool (Fin.decodeBool x) = x
-- Mathlib.RingTheory.Ideal.UFD
UniqueFactorizationMonoid.isPrincipal_of_height_eq_one : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [UniqueFactorizationMonoid R] {p : Ideal R} [p.IsPrime],
  p.height = 1 → Submodule.IsPrincipal p
-- Init.Data.Prod
Prod.swap_inj : ∀ {α : Type u_1} {β : Type u_2} {p q : α × β}, p.swap = q.swap ↔ p = q
-- Mathlib.Order.Interval.Finset.Defs
instLocallyFiniteOrderTopSubtypeLeOfDecidableLEOfLocallyFiniteOrder.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] {y : α} [inst_1 : DecidableLE α] [inst_2 : LocallyFiniteOrder α],
  instLocallyFiniteOrderTopSubtypeLeOfDecidableLEOfLocallyFiniteOrder =
    { finsetIoi := fun a => Finset.Ioc a ⟨y, ⋯⟩, finsetIci := fun a => Finset.Icc a ⟨y, ⋯⟩, finset_mem_Ici := ⋯,
      finset_mem_Ioi := ⋯ }
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.instIsGEObjEIntFunctorETruncLT : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (X : C) (n : ℤ) [t.IsGE X n]
  (i : EInt), t.IsGE ((t.eTruncLT.obj i).obj X) n
-- Mathlib.Tactic.ReduceModChar
/-- Given an expression `e`, determine whether it is a numeric expression in characteristic `n`,
and if so, reduce `e` modulo `n`.

This is not a `norm_num` plugin because it does not match on the syntax of `e`,
rather it matches on the type of `e`.

Use `matchAndNorm (expensive := true)` to do more work in finding the characteristic of
the type of `e`.
 -/
Tactic.ReduceModChar.matchAndNorm : optParam Bool false → Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.RefreshState.mk : Thunk ProofWidgets.Html → ℕ → Task (Option Unit) → ProofWidgets.RefreshComponent.RefreshState
-- Mathlib.Order.Filter.Finite
Filter.mem_iInf_finset : ∀ {α : Type u} {β : Type v} {s : Finset α} {f : α → Filter β} {t : Set β},
  t ∈ ⨅ a ∈ s, f a ↔ ∃ p, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ a ∈ s, p a
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instNeg : {m : Type u_1} → {n : Type u_2} → {A : Type u_5} → [Neg A] → Neg (CStarMatrix m n A)
-- Mathlib.Data.Set.Disjoint
Set.not_disjoint_iff_nonempty_inter : ∀ {α : Type u} {s t : Set α}, ¬Disjoint s t ↔ (s ∩ t).Nonempty
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.pushoutIsoUnopPullback_inv_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushout f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutIsoUnopPullback f g).inv.op
      (CategoryTheory.Limits.pullback.snd f.op g.op) =
    (CategoryTheory.Limits.pushout.inr f g).op
-- Mathlib.RingTheory.PrincipalIdealDomain
gcd_dvd_iff_exists : ∀ {R : Type u} [inst : CommRing R] [IsBezout R] [IsDomain R] [inst_3 : GCDMonoid R] (a b : R) {z : R},
  gcd a b ∣ z ↔ ∃ x y, z = a * x + b * y
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
Set.Countable.measurableSet : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α] {s : Set α}, s.Countable → MeasurableSet s
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.Chain.pair.congr_simp : ∀ {α : Type u_2} [inst : Preorder α] (a a_1 : α) (e_a : a = a_1) (b b_1 : α) (e_b : b = b_1) (hab : a ≤ b),
  OmegaCompletePartialOrder.Chain.pair a b hab = OmegaCompletePartialOrder.Chain.pair a_1 b_1 ⋯
-- Mathlib.LinearAlgebra.Matrix.Diagonal
Matrix.ker_diagonal_toLin' : ∀ {m : Type u_1} [inst : Fintype m] {K : Type u} [inst_1 : Semifield K] [inst_2 : DecidableEq m] (w : m → K),
  (Matrix.toLin' (Matrix.diagonal w)).ker = ⨆ i ∈ {i | w i = 0}, (LinearMap.single K (fun x => K) i).range
-- Mathlib.LinearAlgebra.Prod
LinearMap.prodEquiv_apply : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} (S : Type u_3) [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : AddCommMonoid M₃] [inst_5 : Module R M]
  [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module S M₂] [inst_9 : Module S M₃]
  [inst_10 : SMulCommClass R S M₂] [inst_11 : SMulCommClass R S M₃] (f : (M →ₗ[R] M₂) × (M →ₗ[R] M₃)),
  (LinearMap.prodEquiv S) f = f.1.prod f.2
-- Lean.Parser.Do
Lean.Parser.Term.doIfProp.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.Range.Polymorphic.PRange
Std.Roi.mk.injEq : ∀ {α : Type u} (lower lower_1 : α), (lower<...* = lower_1<...*) = (lower = lower_1)
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instDivisionRing : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] →
      [inst_1 : DivisionRing R] → (v : Valuation R Γ₀) → DivisionRing (WithVal v)
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.Try.focus : {α : Type} → Lean.Elab.Tactic.Try.TryTacticM α → Lean.Elab.Tactic.Try.TryTacticM α
-- Mathlib.Probability.ConditionalProbability
/-- The conditional probability measure of any finite measure on any set of positive measure
is a probability measure.  -/
ProbabilityTheory.cond_isProbabilityMeasure : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : Set Ω} [MeasureTheory.IsFiniteMeasure μ],
  μ s ≠ 0 → MeasureTheory.IsProbabilityMeasure μ[|s]
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Arrow.changeProp_obj_left : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q W : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] [inst_2 : W.IsMultiplicative] {P' Q' W' : CategoryTheory.MorphismProperty T}
  [inst_3 : Q'.IsMultiplicative] [inst_4 : W'.IsMultiplicative] (hPP' : P ≤ P') (hQQ' : Q ≤ Q') (hWW' : W ≤ W')
  (Y : P.Arrow Q W), ((CategoryTheory.MorphismProperty.Arrow.changeProp hPP' hQQ' hWW').obj Y).left = Y.left
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.toMvPolynomial_id : ∀ {R : Type u_1} {M₁ : Type u_2} {ι₁ : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M₁] [inst_2 : Module R M₁]
  [inst_3 : Fintype ι₁] [inst_4 : DecidableEq ι₁] (b₁ : Module.Basis ι₁ R M₁),
  LinearMap.toMvPolynomial b₁ b₁ LinearMap.id = MvPolynomial.X