mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.postcomp_ι : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} (c : F.CoconeTypes)
  {T : Type w₂} (φ : c.pt → T), (c.postcomp φ).ι = fun j => φ ∘ c.ι j
-- Init.Data.Float.Model.Float32
/-- Converts a `Nat` to a `Float32.Model`, returning positive zero on zero.  -/
Float32.Model.ofNat : ℕ → Float32.Model
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithInitial.opEquiv.match_3.splitter : (C : Type u_1) →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    (motive : (x y : (CategoryTheory.WithInitial C)ᵒᵖ) → (Opposite.unop y ⟶ Opposite.unop x) → (x ⟶ y) → Sort u_3) →
      (x y : (CategoryTheory.WithInitial C)ᵒᵖ) →
        (f : Opposite.unop y ⟶ Opposite.unop x) →
          (x_1 : x ⟶ y) →
            ((x y : C) →
                (f :
                    Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of y)) ⟶
                      Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of x))) →
                  (x_2 :
                      Opposite.op (CategoryTheory.WithInitial.of x) ⟶ Opposite.op (CategoryTheory.WithInitial.of y)) →
                    motive (Opposite.op (CategoryTheory.WithInitial.of x))
                      (Opposite.op (CategoryTheory.WithInitial.of y)) f x_2) →
              ((a : C) →
                  (x :
                      Opposite.unop (Opposite.op CategoryTheory.WithInitial.star) ⟶
                        Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of a))) →
                    (x_2 :
                        Opposite.op (CategoryTheory.WithInitial.of a) ⟶ Opposite.op CategoryTheory.WithInitial.star) →
                      motive (Opposite.op (CategoryTheory.WithInitial.of a))
                        (Opposite.op CategoryTheory.WithInitial.star) x x_2) →
                ((x :
                      Opposite.unop (Opposite.op CategoryTheory.WithInitial.star) ⟶
                        Opposite.unop (Opposite.op CategoryTheory.WithInitial.star)) →
                    (x_2 : Opposite.op CategoryTheory.WithInitial.star ⟶ Opposite.op CategoryTheory.WithInitial.star) →
                      motive (Opposite.op CategoryTheory.WithInitial.star) (Opposite.op CategoryTheory.WithInitial.star)
                        x x_2) →
                  motive x y f x_1
-- Aesop.RuleSet.Filter
Aesop.RuleFilter.matchesBuilder : Aesop.RuleFilter → Aesop.BuilderName → Bool
-- Init.Data.String.Termination
String.Slice.Pos.le_iff_remainingBytes_le : ∀ {s : String.Slice} (p q : s.Pos), p ≤ q ↔ q.remainingBytes ≤ p.remainingBytes
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.trans_refl : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (e : X ≃ᵈ Y),
  e.trans (DilationEquiv.refl Y) = e
-- Mathlib.Order.Minimal
Minimal.not_prop_of_lt : ∀ {α : Type u_2} {P : α → Prop} {x y : α} [inst : Preorder α], Minimal P x → y < x → ¬P y
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.comp_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {φ' : S₂ ⟶ S₃} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData}
  {h₃ : S₃.HomologyData} (ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂)
  (ψ' : CategoryTheory.ShortComplex.HomologyMapData φ' h₂ h₃), (ψ.comp ψ').right = ψ.right.comp ψ'.right
-- Mathlib.Data.FunLike.Group
FunLike.leftCancelMonoid.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Mul F] [inst_2 : One F]
  [inst_3 : Pow F ℕ] [inst_4 : LeftCancelMonoid β] [inst_5 : IsOneApply F α β] [inst_6 : IsMulApply F α β]
  [inst_7 : IsPowApply ℕ F α β], FunLike.leftCancelMonoid = Function.Injective.leftCancelMonoid (fun f => ⇑f) ⋯ ⋯ ⋯ ⋯
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Unitary.path.congr_simp : ∀ {A : Type u_1} [inst : CStarAlgebra A] (u v : ↥(unitary A)) (huv : ‖↑v - ↑u‖ < 2),
  Unitary.path u v huv = Unitary.path u v huv
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.nullMeasurableSet_vadd : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ],
  MeasureTheory.IsAddFundamentalDomain G s μ → ∀ (g : G), MeasureTheory.NullMeasurableSet (g +ᵥ s) μ
-- Mathlib.RingTheory.AdicCompletion.Basic
IsHausdorff.of_map : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : CommRing S] [inst_4 : Module S M] {J : Ideal S} [inst_5 : Algebra R S]
  [IsScalarTower R S M], Ideal.map (algebraMap R S) I ≤ J → ∀ [IsHausdorff J M], IsHausdorff I M
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.UnitaryGroup.mul_apply : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v} [inst_2 : CommRing α] [inst_3 : StarRing α]
  (A B : ↥(Matrix.unitaryGroup n α)), ↑(A * B) = ↑A * ↑B
-- Batteries.Control.LawfulMonadState
LawfulMonadStateOf.seqLeft_get : ∀ {σ : Type u_1} {m : Type u_1 → Type u_2} [inst : Monad m] [inst_1 : MonadStateOf σ m] [LawfulMonadStateOf σ m]
  {α : Type u_1} (mx : m α), mx <* get = mx
-- Mathlib.Algebra.Group.InjSurj
Function.Surjective.commMonoid.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₂] [inst_1 : One M₂] [inst_2 : Pow M₂ ℕ] [inst_3 : CommMonoid M₁]
  (f : M₁ → M₂) (hf : Function.Surjective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y)
  (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n),
  Function.Surjective.commMonoid f hf one mul npow =
    { toMonoid := Function.Surjective.monoid f hf one mul npow, mul_comm := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
/-- `Cofork.ofπ π w` is a colimit cocone if and only if `Fork.ofι π.op w'` in the opposite
category is a limit cone.  -/
CategoryTheory.Limits.Cofork.isColimitOfπEquivIsLimitOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y P : C} →
      {f g : X ⟶ Y} →
        (π π' : Y ⟶ P) →
          (w : CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π) →
            (w' : CategoryTheory.CategoryStruct.comp π'.op f.op = CategoryTheory.CategoryStruct.comp π'.op g.op) →
              π = π' →
                CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ π w) ≃
                  CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι π'.op w')
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.functorP_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y),
  CategoryTheory.ShortComplex.SnakeInput.functorP.map f =
    CategoryTheory.Limits.pullback.map X.L₁.g X.v₀₁.τ₃ Y.L₁.g Y.v₀₁.τ₃ f.f₁.τ₂ f.f₀.τ₃ f.f₁.τ₃ ⋯ ⋯
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isLongestMatchAtChain_of_ofSliceTo : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {p : s.Pos}
  {startPos endPos : (s.sliceTo p).Pos},
  String.Slice.Pattern.Model.IsLongestMatchAtChain pat (String.Slice.Pos.ofSliceTo startPos)
      (String.Slice.Pos.ofSliceTo endPos) →
    String.Slice.Pattern.Model.IsLongestMatchAtChain pat startPos endPos
-- Mathlib.Data.Sign.Basic
sign_pow : ∀ {α : Type u} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (x : α) (n : ℕ),
  SignType.sign (x ^ n) = SignType.sign x ^ n
-- Std.Time.Date.Unit.Month
/-- Gets the number of days in a month.
 -/
Std.Time.Month.Ordinal.days : Bool → Std.Time.Month.Ordinal → Std.Time.Day.Ordinal
-- Mathlib.Analysis.Subadditive
Subadditive.lim.eq_1 : ∀ {u : ℕ → ℝ} (_h : Subadditive u), _h.lim = sInf ((fun n => u n / ↑n) '' Set.Ici 1)
-- Mathlib.Algebra.Module.Presentation.DirectSum
Module.Presentation.directSum_var : ∀ {A : Type u} [inst : Ring A] {ι : Type w} [inst_1 : DecidableEq ι] {M : ι → Type v}
  [inst_2 : (i : ι) → AddCommGroup (M i)] [inst_3 : (i : ι) → Module A (M i)]
  (pres : (i : ι) → Module.Presentation A (M i)) (i : ι) (g : (pres i).G),
  (Module.Presentation.directSum pres).var ⟨i, g⟩ = (DirectSum.lof A ι M i) ((pres i).var g)
-- Mathlib.Algebra.Field.Subfield.Basic
/-- The subfield generated by a set includes the set.  -/
Subfield.subset_closure : ∀ {K : Type u} [inst : DivisionRing K] {s : Set K}, s ⊆ ↑(Subfield.closure s)
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.removeAssignment : Bool → Std.Tactic.BVDecide.LRAT.Internal.Assignment → Std.Tactic.BVDecide.LRAT.Internal.Assignment
-- Mathlib.Order.Category.PartOrd
PartOrd.str : (self : PartOrd) → PartialOrder ↑self
-- Mathlib.Topology.Inseparable
inseparable_iff_mem_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, Inseparable x y ↔ x ∈ closure {y} ∧ y ∈ closure {x}
-- Mathlib.Geometry.Convex.Set
Convexity.IsConvexSet.iUnion : ∀ {R : Type u_3} {X : Type u_5} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {ι : Sort u_7} {s : ι → Set X},
  Directed (fun x1 x2 => x1 ⊆ x2) s → (∀ (i : ι), Convexity.IsConvexSet R (s i)) → Convexity.IsConvexSet R (⋃ i, s i)
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartAlgebra.congr_simp : ∀ (R : Type u_1) (A : Type u_2) (L : Type u_3) [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L]
  [inst_3 : LieRingModule L A] [inst_4 : LieRinehartRing A L] [inst_5 : CommRing R] [inst_6 : Algebra R A]
  [inst_7 : LieAlgebra R L], LieRinehartAlgebra R A L = LieRinehartAlgebra R A L
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- The weighted sum is independent of the base point when the sum of
the weights is 0.  -/
Finset.weightedVSubOfPoint_eq_of_sum_eq_zero : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P),
  ∑ i ∈ s, w i = 0 → ∀ (b₁ b₂ : P), (s.weightedVSubOfPoint p b₁) w = (s.weightedVSubOfPoint p b₂) w
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.karoubiUniversal.eq_1 : ∀ (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] [inst_2 : CategoryTheory.IsIdempotentComplete D],
  CategoryTheory.Idempotents.karoubiUniversal C D =
    (CategoryTheory.Idempotents.karoubiUniversal₂ C D).trans
      (CategoryTheory.Idempotents.toKaroubi D).asEquivalence.symm.congrRight
-- Mathlib.Topology.Order.Compact
IsCompact.sInf_mem : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [ClosedIicTopology α]
  {s : Set α}, IsCompact s → s.Nonempty → sInf s ∈ s
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.comp_right_inj : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] {P : Type u_1}
  [inst_2 : L.Structure P] (h : L.Equiv M N) (f g : L.Equiv N P), f.comp h = g.comp h ↔ f = g
-- Mathlib.Tactic.Translate.TagUnfoldBoundary
/-- The `insert_cast foo := ...` command should be used when the translation of some
definition `foo` is not definitionally equal to the translation of its value.
It requires a proof that these two are equal. For example,

```
to_dual_insert_cast Monotone := by grind
```

If the definition is a type, you should use `insert_cast_fun` instead.

The command internally generates an unfolding theorem for `foo`, and a translation of this theorem.
When type checking a term requires the definition `foo` to be unfolded, then in order to translate
that term, a `cast` is first inserted into the term using this unfolding theorem.
As a result, type checking the term won't anymore require unfolding `foo`, so the term
can be safely translated.  -/
Mathlib.Tactic.Translate.elabInsertCast : Lean.Ident → Lean.Term → Mathlib.Tactic.Translate.TranslateData → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Probability.Process.LocalProperty
/-- If `q` is a stable property and `p` implies `q` locally, then `p` locally implies
`q` locally.  -/
ProbabilityTheory.IsStable.locally_induction : ∀ {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : ConditionallyCompleteLinearOrderBot ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι]
  {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} {p q : (ι → Ω → E) → Prop} [SecondCountableTopology ι]
  [MeasureTheory.IsFiniteMeasure P] [DenselyOrdered ι] [NoMaxOrder ι] [inst_7 : Zero E] [𝓕.IsRightContinuous],
  ProbabilityTheory.IsStable 𝓕 q →
    (∀ (Y : ι → Ω → E), p Y → ProbabilityTheory.Locally q 𝓕 Y P) →
      ProbabilityTheory.Locally p 𝓕 X P → ProbabilityTheory.Locally q 𝓕 X P
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.cycleOf_ne_one_iff_mem_cycleFactorsFinset : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} {x : α},
  g.cycleOf x ≠ 1 ↔ g.cycleOf x ∈ g.cycleFactorsFinset
-- Init.Data.Array.Lemmas
Array.empty_of_isEmpty : ∀ {α : Type u_1} {xs : Array α}, xs.isEmpty = true → xs = #[]
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- Two isomorphisms `G ≃+ G'` of additive groups are equal if and only if they agree
on a generator of `G`.  -/
AddEquiv.eq_iff_eq_on_generator : ∀ {G : Type u_2} {G' : Type u_3} [inst : AddGroup G] [inst_1 : AddGroup G'] {g : G},
  (∀ (x : G), x ∈ AddSubgroup.zmultiples g) → ∀ (f₁ f₂ : G ≃+ G'), f₁ = f₂ ↔ f₁ g = f₂ g
-- Mathlib.Data.Finite.Prod
/-- `image2 f s t` is `Fintype` if `s` and `t` are.  -/
Set.fintypeImage2 : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      [DecidableEq γ] →
        (f : α → β → γ) →
          (s : Set α) → (t : Set β) → [hs : Fintype ↑s] → [ht : Fintype ↑t] → Fintype ↑(Set.image2 f s t)
-- Mathlib.Topology.Separation.Basic
compl_singleton_mem_nhdsSet_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {x : X} {s : Set X}, {x}ᶜ ∈ nhdsSet s ↔ x ∉ s
-- Mathlib.Analysis.ConstantSpeed
/-- If both `f` and `f ∘ φ` have unit speed (on `Icc 0 t` and `Icc 0 s` respectively)
and `φ` monotonically maps `Icc 0 s` onto `Icc 0 t`, then `φ` is the identity on `Icc 0 s`
 -/
unique_unit_speed_on_Icc_zero : ∀ {E : Type u_2} [inst : PseudoEMetricSpace E] {f : ℝ → E} {s t : ℝ},
  0 ≤ s →
    0 ≤ t →
      ∀ {φ : ℝ → ℝ},
        MonotoneOn φ (Set.Icc 0 s) →
          φ '' Set.Icc 0 s = Set.Icc 0 t →
            HasUnitSpeedOn (f ∘ φ) (Set.Icc 0 s) → HasUnitSpeedOn f (Set.Icc 0 t) → Set.EqOn φ id (Set.Icc 0 s)
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
/-- The quadratic form on the augmented vector space `M × R` sending `v + r•e0` to `Q v - r^2`.  -/
CliffordAlgebra.EquivEven.Q' : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → QuadraticForm R M → QuadraticForm R (M × R)
-- Mathlib.Topology.Algebra.Ring.Basic
NonUnitalSubring.topologicalClosure_minimal : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NonUnitalRing R] [inst_2 : IsSemitopologicalRing R]
  (s : NonUnitalSubring R) {t : NonUnitalSubring R}, s ≤ t → IsClosed ↑t → s.topologicalClosure ≤ t
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  (X : CategoryTheory.Functor AugmentedSimplexCategoryᵒᵖ C),
  (AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso.hom.app X).left =
    CategoryTheory.CategoryStruct.id
      (X.obj
        (match CategoryTheory.WithTerminal.incl.obj (Opposite.op { len := 0 }) with
        | CategoryTheory.WithTerminal.of x => Opposite.op (CategoryTheory.WithInitial.of (Opposite.unop x))
        | CategoryTheory.WithTerminal.star => Opposite.op CategoryTheory.WithInitial.star))
-- Std.Data.Iterators.Combinators.Monadic.Zip
_private.Std.Data.Iterators.Combinators.Monadic.Zip.0.Option.SomeLtNone.lt.match_1.eq_2 : ∀ {β : Type u_2} {α : Type u_1} (motive : Option α → Option β → Sort u_3) (val : α)
  (h_1 : (x : Option β) → motive none x) (h_2 : (val : α) → motive (some val) none)
  (h_3 : (x : α) → (y : β) → motive (some x) (some y)),
  (match some val, none with
    | none, x => h_1 x
    | some val, none => h_2 val
    | some x, some y => h_3 x y) =
    h_2 val
-- Lean.Parser.Term
Lean.Parser.Term.arrow.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.Hom.WithTopBot
/-- Adjoins a `⊥` and `⊤` to the domain of a `LatticeHom`.  -/
LatticeHom.withBotWithTop' : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Lattice α] →
      [inst_1 : Lattice β] → [inst_2 : BoundedOrder β] → LatticeHom α β → BoundedLatticeHom (WithBot (WithTop α)) β
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.cardSupp_add_le : ∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : AddMonoid R] (x y : HahnSeries Γ R),
  (x + y).cardSupp ≤ x.cardSupp + y.cardSupp
-- Mathlib.CategoryTheory.EpiMono
/-- When `f` is an epimorphism, `f ≫ g` is epic iff `g` is.  -/
CategoryTheory.epi_comp_iff_of_epi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) [CategoryTheory.Epi f] (g : Y ⟶ Z),
  CategoryTheory.Epi (CategoryTheory.CategoryStruct.comp f g) ↔ CategoryTheory.Epi g
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.ToBackwardSearcher.mk : {ρ : Type} →
  {pat : ρ} →
    {σ : outParam (String.Slice → Type)} →
      ((s : String.Slice) → Std.Iter (String.Slice.Pattern.SearchStep s)) →
        String.Slice.Pattern.ToBackwardSearcher pat σ
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- If `X ⟶ Y` is an open immersion of PresheafedSpaces, and `Y` is a SheafedSpace, we can
upgrade it into a morphism of SheafedSpaces.
 -/
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : AlgebraicGeometry.PresheafedSpace C} →
      (Y : AlgebraicGeometry.SheafedSpace C) →
        (f : X ⟶ Y.toPresheafedSpace) →
          [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] →
            AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpace Y f ⟶ Y
-- Init.Data.Nat.Gcd
Nat.gcd_add_right_left_of_dvd : ∀ {m k : ℕ} (n : ℕ), m ∣ k → (n + k).gcd m = n.gcd m
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.rootFormIn_isSymm : ∀ {ι : 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)
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [inst_7 : FaithfulSMul S R] [inst_8 : Module S M]
  [inst_9 : IsScalarTower S R M] [inst_10 : P.IsValuedIn S] [inst_11 : Fintype ι], LinearMap.IsSymm (P.RootFormIn S)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
SimpleGraph.instDecidableMemSupp : {V : Type u} →
  (G : SimpleGraph V) →
    [DecidableEq V] → [Fintype V] → [DecidableRel G.Adj] → (c : G.ConnectedComponent) → (v : V) → Decidable (v ∈ c.supp)
-- Mathlib.LinearAlgebra.Projectivization.Subspace
/-- The span of a set of points in projective space is a subspace.  -/
Projectivization.Subspace.span : {K : Type u_1} →
  {V : Type u_2} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → Set (Projectivization K V) → Projectivization.Subspace K V
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndepFun_iff_condIndepSet_preimage : ∀ {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {f : Ω → β} {g : Ω → β'}
  {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'},
  Measurable f →
    Measurable g →
      (ProbabilityTheory.CondIndepFun m' hm' f g μ ↔
        ∀ (s : Set β) (t : Set β'),
          MeasurableSet s → MeasurableSet t → ProbabilityTheory.CondIndepSet m' hm' (f ⁻¹' s) (g ⁻¹' t) μ)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAgainstOfIsStableUnderBaseChange : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C)
  [P.IsStableUnderBaseChange] (P' : CategoryTheory.MorphismProperty C), P.IsStableUnderBaseChangeAgainst P'
-- Mathlib.Algebra.Ring.Pi
Pi.constRingHom_apply : ∀ (α : Type u_1) (β : Type u_2) [inst : NonAssocSemiring β] (a : β) (a_1 : α),
  (Pi.constRingHom α β) a a_1 = Function.const α a a_1
-- Init.Prelude
/-- A portion of the syntax tree that is missing because of a parse error.

The indexing operator on `Syntax` also returns `Syntax.missing` when the index is out of bounds.
 -/
Lean.Syntax.missing : Lean.Syntax
-- Mathlib.Algebra.Ring.Action.Group
/-- Each element of the group defines a semiring isomorphism.  -/
MulSemiringAction.toRingEquiv : (G : Type u_1) → [inst : Group G] → (R : Type u_2) → [inst_1 : Semiring R] → [MulSemiringAction G R] → G →* R ≃+* R
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.div : ℤ → Lean.Meta.Grind.Arith.CommRing.EqCnstr → Lean.Meta.Grind.Arith.CommRing.EqCnstrProof
-- Mathlib.Data.Set.Defs
/-- `𝒫 s` is the set of all subsets of `s`.  -/
Set.powerset : {α : Type u} → Set α → Set (Set α)
-- Lean.Elab.DeclUtil
/-- Given two forall-expressions `type₁` and `type₂`, ensure the first `numParams` parameters are compatible, and
then execute `k` with the parameters and remaining types.  -/
Lean.Meta.forallTelescopeCompatible : {m : Type → Type u_1} →
  {α : Type} →
    [Monad m] →
      [MonadControlT Lean.MetaM m] → Lean.Expr → Lean.Expr → ℕ → (Array Lean.Expr → Lean.Expr → Lean.Expr → m α) → m α
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- `DivInvMonoid.Pow` is measurable.  -/
DivInvMonoid.measurableZPow : ∀ (G : Type u) [inst : DivInvMonoid G] [inst_1 : MeasurableSpace G] [MeasurableMul₂ G] [MeasurableInv G],
  MeasurablePow G ℤ
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.map_smul_of_tower : ∀ {A : Type u_2} [inst : Semiring A] [inst_1 : TopologicalSpace A] {B : Type u_3} [inst_2 : Semiring B]
  [inst_3 : TopologicalSpace B] {R : Type u_4} {S : Type u_5} [inst_4 : CommSemiring S] [inst_5 : SMul R A]
  [inst_6 : Algebra S A] [inst_7 : SMul R B] [inst_8 : Algebra S B] [MulActionHomClass (A →A[S] B) R A B]
  (f : A →A[S] B) (c : R) (x : A), f (c • x) = c • f x
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem_toList_roo : ∀ {m n i : ℕ} (_h : i < (m<...n).toList.length), (m<...n).toList[i] = m + 1 + i
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.vec3_eq : ∀ {α : Type u} {a₀ a₁ a₂ b₀ b₁ b₂ : α}, a₀ = b₀ → a₁ = b₁ → a₂ = b₂ → ![a₀, a₁, a₂] = ![b₀, b₁, b₂]
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants.inc : ∀ {pat s : String.Slice} {stackPos needlePos : String.Pos.Raw},
  String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants✝ pat s needlePos stackPos →
    ∀ (h₁ : needlePos < pat.rawEndPos) (h₂ : stackPos < s.rawEndPos),
      pat.getUTF8Byte needlePos h₁ = s.getUTF8Byte stackPos h₂ →
        String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants✝ pat s needlePos.inc stackPos.inc
-- Init.Data.SInt.Lemmas
Int64.toInt8_ofIntLE : ∀ {n : ℤ} (h₁ : Int64.minValue.toInt ≤ n) (h₂ : n ≤ Int64.maxValue.toInt), (Int64.ofIntLE n h₁ h₂).toInt8 = Int8.ofInt n
-- Mathlib.Algebra.Order.Ring.Ordering.Basic
RingPreordering.mem_mk' : ∀ {R : Type u_2} [inst : CommRing R] {P : Set R} {add : ∀ {x y : R}, x ∈ P → y ∈ P → x + y ∈ P}
  {mul : ∀ {x y : R}, x ∈ P → y ∈ P → x * y ∈ P} {sq : ∀ (x : R), x * x ∈ P} {neg_one : -1 ∉ P} {x : R},
  x ∈ RingPreordering.mk' P add mul sq neg_one ↔ x ∈ P
-- Init.Data.UInt.Lemmas
USize.lt_one_iff : ∀ {a : USize}, a < 1 ↔ a = 0
-- Batteries.Recycling.RBTree.Basic
/-- `O(n log n)`. Build a tree from an unsorted list by inserting them one at a time.  -/
RBTree.RBSet.ofList : {α : Type u_1} → List α → (cmp : α → α → Ordering) → RBTree.RBSet α cmp