mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Search
/-- Finds the position of the first match of the pattern `pattern` in a slice `s` that is
strictly before `pos`. If there is no such match `none` is returned.

This function is generic over all currently supported patterns except
`String`/`String.Slice`.

Examples:

* `(("ab1c".endPos.prev (by decide)).revFind? Char.isAlpha).map (·.get!) == some 'b'`

* `"abc".startPos.revFind? Char.isAlpha == none`
 -/
String.Pos.revFind? : {ρ : Type} →
  {σ : String.Slice → Type} →
    [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
      [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] →
        {s : String} → s.Pos → (pattern : ρ) → [String.Slice.Pattern.ToBackwardSearcher pattern σ] → Option s.Pos
-- Init.Internal.Order.MonadTail
Lean.Order.instMonadTailBaseIO : Lean.Order.MonadTail BaseIO
-- Batteries.Data.UInt
USize.ext_iff : ∀ {x y : USize}, x = y ↔ x.toNat = y.toNat
-- Mathlib.Topology.EMetricSpace.Diam
Metric.ediam_iUnion_mem_option : ∀ {X : Type u_2} [inst : PseudoEMetricSpace X] {ι : Type u_3} (o : Option ι) (s : ι → Set X),
  Metric.ediam (⋃ i ∈ o, s i) = ⨆ i ∈ o, Metric.ediam (s i)
-- Mathlib.CategoryTheory.Monad.Limits
/-- The forgetful functor from the Eilenberg-Moore category for a monad creates any colimit
which the monad itself preserves.
 -/
CategoryTheory.Monad.forgetCreatesColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} →
      {J : Type u} →
        [inst_1 : CategoryTheory.Category.{v, u} J] →
          (D : CategoryTheory.Functor J T.Algebra) →
            [CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] →
              [CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] →
                CategoryTheory.CreatesColimit D T.forget
-- Mathlib.Order.Hom.CompleteLattice
map_iSup : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Sort u_6} [inst : FunLike F α β] [inst_1 : SupSet α]
  [inst_2 : SupSet β] [sSupHomClass F α β] (f : F) (g : ι → α), f (⨆ i, g i) = ⨆ i, f (g i)
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.Rel.below.lie_self : ∀ {R : Type u} {X : Type v} [inst : CommRing R]
  {motive : (a a_1 : FreeNonUnitalNonAssocAlgebra R X) → FreeLieAlgebra.Rel R X a a_1 → Prop}
  (a : FreeNonUnitalNonAssocAlgebra R X), FreeLieAlgebra.Rel.below ⋯
-- Mathlib.Data.Finsupp.Basic
Finsupp.filter_apply_neg : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (p : α → Prop) [inst_1 : DecidablePred p] (f : α →₀ M) {a : α},
  ¬p a → (Finsupp.filter p f) a = 0
-- Mathlib.RingTheory.Etale.Finite
/-- If `Ω` is a separably closed field, the category of finite étale `Ω`-algebras is
anti-equivalent to `FintypeCat`.  -/
CommAlgCat.FiniteEtale.equivOfIsSepClosed : (Ω : Type u) → [inst : Field Ω] → [IsSepClosed Ω] → (CommAlgCat.FiniteEtale Ω)ᵒᵖ ≌ FintypeCat
-- Mathlib.Analysis.Fourier.AddCircle
/-- **Alias** of the reverse direction of `MeasureTheory.memLp_haarAddCircle_iff`. -/
MeasureTheory.MemLp.haarAddCircle : ∀ {T : ℝ} [hT : Fact (0 < T)] {f : AddCircle T → ℂ} {p : ENNReal},
  MeasureTheory.MemLp f p MeasureTheory.volume → MeasureTheory.MemLp f p AddCircle.haarAddCircle
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.rightAdjointUniq_inv_app : ∀ {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 G' : CategoryTheory.Functor D C}
  (adj1 : F ⊣ G) (adj2 : F ⊣ G') (x : D),
  (adj1.rightAdjointUniq adj2).inv.app x = (adj2.rightAdjointUniq adj1).hom.app x
-- Mathlib.Probability.Martingale.OptionalStopping
/-- Given a submartingale `f` and bounded stopping times `τ` and `π` such that `τ ≤ π`, the
expectation of `stoppedValue f τ` is less than or equal to the expectation of `stoppedValue f π`.
This is the forward direction of the optional stopping theorem.  -/
MeasureTheory.Submartingale.expected_stoppedValue_mono : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0}
  {τ π : Ω → ℕ∞} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E]
  [inst_3 : PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] [ClosedIciTopology E]
  [MeasureTheory.SigmaFiniteFiltration μ 𝒢] {f : ℕ → Ω → E},
  MeasureTheory.Submartingale f 𝒢 μ →
    MeasureTheory.IsStoppingTime 𝒢 τ →
      MeasureTheory.IsStoppingTime 𝒢 π →
        τ ≤ π →
          ∀ {N : ℕ},
            (∀ (ω : Ω), π ω ≤ ↑N) →
              ∫ (x : Ω), MeasureTheory.stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), MeasureTheory.stoppedValue f π x ∂μ
-- Mathlib.RingTheory.Etale.Finite
CommAlgCat.FiniteEtale.finiteSpec_obj_obj : ∀ (k : Type u) [inst : Field k] (R : (CommAlgCat.FiniteEtale k)ᵒᵖ),
  ((CommAlgCat.FiniteEtale.finiteSpec k).obj R).obj = PrimeSpectrum ↑(Opposite.unop R).obj
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_inter_le_size_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  (t₁ ∩ t₂).size ≤ t₁.size
-- Lean.Elab.DefView
Lean.Elab.BodyProcessedSnapshot.mk.sizeOf_spec : ∀ (toSnapshot : Lean.Language.Snapshot) (state : Lean.Elab.Term.SavedState) (value : Lean.Expr)
  (moreSnaps : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)),
  sizeOf { toSnapshot := toSnapshot, state := state, value := value, moreSnaps := moreSnaps } =
    1 + sizeOf toSnapshot + sizeOf state + sizeOf value + sizeOf moreSnaps
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.Scheme.OpenCover.affineRefinement.eq_1 : ∀ {X : AlgebraicGeometry.Scheme} (𝓤 : X.OpenCover),
  𝓤.affineRefinement =
    { I₀ := (CategoryTheory.Precoverage.ZeroHypercover.bind 𝓤 fun j => (𝓤.X j).affineCover).I₀,
      X := fun j => (fun x => Classical.choose ⋯) j.snd,
      f := (CategoryTheory.Precoverage.ZeroHypercover.bind 𝓤 fun j => (𝓤.X j).affineCover).f,
      idx :=
        AlgebraicGeometry.Scheme.Cover.idx
          (CategoryTheory.Precoverage.ZeroHypercover.bind 𝓤 fun j => (𝓤.X j).affineCover),
      covers := ⋯, map_prop := ⋯ }
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_cons : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [inst : AddCommMonoid M] {f : ι → M} (h : a ∉ s),
  ∑ x ∈ Finset.cons a s h, f x = f a + ∑ x ∈ s, f x
-- Mathlib.Tactic.ClickSuggestions.SectionState
/-- `key` is used for sorting and comparing theorems.  -/
Mathlib.Tactic.ClickSuggestions.Result.key : {α : Type} → Mathlib.Tactic.ClickSuggestions.Result α → α
-- Mathlib.Algebra.Notation.Support
Function.support_nonempty_iff : ∀ {ι : Type u_1} {M : Type u_3} [inst : Zero M] {f : ι → M}, (Function.support f).Nonempty ↔ f ≠ 0
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.facePairComplIso_hom_ι_assoc : ∀ {n : ℕ} (i j : Fin (n + 3)) (h : i < j) {Z : SSet} (h_1 : SSet.stdSimplex.obj { len := n + 2 } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.facePairComplIso i j h).hom
      (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.face {i, j}ᶜ).ι h_1) =
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ (i.castPred ⋯))
      (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) h_1)
-- Mathlib.Topology.Constructions.SumProd
Filter.Eventually.prod_nhds : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {p : X → Prop} {q : Y → Prop}
  {x : X} {y : Y},
  (∀ᶠ (x : X) in nhds x, p x) → (∀ᶠ (y : Y) in nhds y, q y) → ∀ᶠ (z : X × Y) in nhds (x, y), p z.1 ∧ q z.2
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.Const.alter.eq_1 : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (a : α) (f : Option β → Option β) (size : ℕ)
  (buckets : Array (Std.DHashMap.Internal.AssocList α fun x => β))
  (hm : 0 < { size := size, buckets := buckets }.buckets.size),
  Std.DHashMap.Internal.Raw₀.Const.alter ⟨{ size := size, buckets := buckets }, hm⟩ a f =
    match Std.DHashMap.Internal.mkIdx buckets.size hm (hash a) with
    | ⟨i, h⟩ =>
      let bkt := buckets[i];
      if Std.DHashMap.Internal.AssocList.contains a bkt = true then
        let buckets' := buckets.uset i Std.DHashMap.Internal.AssocList.nil h;
        let bkt' := Std.DHashMap.Internal.AssocList.Const.alter a f bkt;
        have size' := if Std.DHashMap.Internal.AssocList.contains a bkt' = true then size else size - 1;
        ⟨{ size := size', buckets := buckets'.uset i bkt' ⋯ }, ⋯⟩
      else
        match f none with
        | none => ⟨{ size := size, buckets := buckets }, hm⟩
        | some b =>
          have size' := size + 1;
          let buckets' := buckets.uset i (Std.DHashMap.Internal.AssocList.cons a b bkt) h;
          Std.DHashMap.Internal.Raw₀.expandIfNecessary ⟨{ size := size', buckets := buckets' }, ⋯⟩
-- Init.Data.Vector.Lemmas
Vector.toArray_mapIdx : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : ℕ → α → β} {xs : Vector α n},
  (Vector.mapIdx f xs).toArray = Array.mapIdx f xs.toArray
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
/-- Given an abelian category `C`, a sequence of complex shapes `c : ℤ → ComplexShape κ`
and a starting page `r₀ : ℤ`, a spectral sequence involves pages which are homological
complexes and isomorphisms saying that the homology of a page identifies to the next page.  -/
CategoryTheory.SpectralSequence : (C : Type u_1) →
  [inst : CategoryTheory.Category.{u_3, u_1} C] →
    [CategoryTheory.Abelian C] → {κ : Type u_2} → (ℤ → ComplexShape κ) → ℤ → Type (max (max u_1 u_2) u_3)
-- Init.Data.UInt.Lemmas
UInt16.toFin_ofNatLT : ∀ {n : ℕ} (hn : n < UInt16.size), (UInt16.ofNatLT n hn).toFin = ⟨n, hn⟩
-- Init.Data.UInt.Lemmas
UInt32.toUInt64_div : ∀ (a b : UInt32), (a / b).toUInt64 = a.toUInt64 / b.toUInt64
-- Mathlib.Data.Bool.Basic
Bool.toNat_le_toNat : ∀ {b₀ b₁ : Bool}, b₀ ≤ b₁ → b₀.toNat ≤ b₁.toNat
-- Mathlib.MeasureTheory.Group.Arithmetic
measurableSMul₂_iterateAddAct : ∀ {α : Type u_2} {x : MeasurableSpace α} {f : α → α}, MeasurableVAdd₂ (IterateAddAct f) α ↔ Measurable f
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.LeftExtension.w : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  {s t : CategoryTheory.Bicategory.LeftExtension f g} (η : s ⟶ t),
  CategoryTheory.CategoryStruct.comp s.unit
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.StructuredArrow.Hom.right η)) =
    t.unit
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.gcd_cons : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
  {f : β → α} {b : β} (h : b ∉ s), (Finset.cons b s h).gcd f = gcd (f b) (s.gcd f)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get!_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] [inst_2 : Inhabited α]
  {a : α}, ∅.get! a = default
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
/-- The negative of a harmonic function is harmonic.
 -/
InnerProductSpace.HarmonicOnNhd.neg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {s : Set E},
  InnerProductSpace.HarmonicOnNhd f s → InnerProductSpace.HarmonicOnNhd (-f) s
-- Mathlib.RingTheory.WittVector.WittPolynomial
constantCoeff_xInTermsOfW : ∀ (p : ℕ) (R : Type u_1) [inst : CommRing R] [hp : Fact (Nat.Prime p)] [inst_1 : Invertible ↑p] (n : ℕ),
  MvPolynomial.constantCoeff (xInTermsOfW p R n) = 0
-- Mathlib.Algebra.GCDMonoid.Basic
/-- Define `NormalizedGCDMonoid` on a structure just from the `lcm` and its properties.  -/
normalizedGCDMonoidOfLCM : {α : Type u_1} →
  [inst : CommMonoidWithZero α] →
    [IsCancelMulZero α] →
      [inst_2 : NormalizationMonoid α] →
        [DecidableEq α] →
          (lcm : α → α → α) →
            (∀ (a b : α), a ∣ lcm a b) →
              (∀ (a b : α), b ∣ lcm a b) →
                (∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a) →
                  (∀ (a b : α), normalize (lcm a b) = lcm a b) → NormalizedGCDMonoid α
-- Lean.Meta.Match.Basic
Lean.Meta.Match.MatcherResult.mk.inj : ∀ {matcher : Lean.Expr} {counterExamples : Array Lean.Meta.Match.CounterExample} {unusedAltIdxs : List ℕ}
  {addMatcher : Lean.MetaM Unit} {matcher_1 : Lean.Expr} {counterExamples_1 : Array Lean.Meta.Match.CounterExample}
  {unusedAltIdxs_1 : List ℕ} {addMatcher_1 : Lean.MetaM Unit},
  { matcher := matcher, counterExamples := counterExamples, unusedAltIdxs := unusedAltIdxs, addMatcher := addMatcher } =
      { matcher := matcher_1, counterExamples := counterExamples_1, unusedAltIdxs := unusedAltIdxs_1,
        addMatcher := addMatcher_1 } →
    matcher = matcher_1 ∧
      counterExamples = counterExamples_1 ∧ unusedAltIdxs = unusedAltIdxs_1 ∧ addMatcher = addMatcher_1
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
/-- If `L/K` and `ψ : K →+* ℂ`, then the type of `ComplexEmbedding.Extension L ψ` consists of all
`φ : L →+* ℂ` such that `φ.comp (algebraMap K L) = ψ`.  -/
NumberField.ComplexEmbedding.Extension : {K : Type u_3} → (L : Type u_4) → [inst : Field K] → [inst_1 : Field L] → (K →+* ℂ) → [Algebra K L] → Type (max 0 u_4)
-- Mathlib.Topology.Maps.Proper.Basic
/-- If `X` is a compact topological space, then `Prod.snd : X × Y → Y` is a proper map.  -/
isProperMap_snd_of_compactSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [CompactSpace X],
  IsProperMap Prod.snd
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.abs_det_fderiv_expMapBasis : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.realSpace K),
  |(NumberField.mixedEmbedding.fundamentalCone.fderiv_expMapBasis K x).det| =
    Real.exp (x NumberField.Units.dirichletUnitTheorem.w₀ * ↑(Module.finrank ℚ K)) *
            (∏ w, ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis x ↑w)⁻¹ *
          2⁻¹ ^ NumberField.InfinitePlace.nrComplexPlaces K *
        ↑(Module.finrank ℚ K) *
      NumberField.Units.regulator K
-- Mathlib.Tactic.Ring.Basic
/-- Add two rational number expressions. If the result is zero, returns a proof of this fact.  -/
Mathlib.Tactic.Ring.RingCompute.add : {u : Lean.Level} →
  {α : Q(Type u)} →
    (sα : Q(CommSemiring «$α»)) →
      {a b : Q(«$α»)} →
        Mathlib.Tactic.Ring.RatCoeff a →
          Mathlib.Tactic.Ring.RatCoeff b →
            Lean.MetaM
              (Mathlib.Tactic.Ring.Common.Result Mathlib.Tactic.Ring.RatCoeff q(«$a» + «$b») ×
                Option Q(Mathlib.Meta.NormNum.IsNat («$a» + «$b») 0))
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.toRatCDF_of_isRatStieltjesPoint : ∀ {α : Type u_1} {f : α → ℚ → ℝ} {a : α},
  ProbabilityTheory.IsRatStieltjesPoint f a → ∀ (q : ℚ), ProbabilityTheory.toRatCDF f a q = f a q
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.of_tensor : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] {X Y : Type u} [inst_2 : AddCommGroup X]
  [inst_3 : AddCommGroup Y] [inst_4 : Module k X] [inst_5 : Module k Y] (σ : Representation k G X)
  (ρ : Representation k G Y), Rep.of (σ.tprod ρ) = CategoryTheory.MonoidalCategoryStruct.tensorObj (Rep.of σ) (Rep.of ρ)
-- Mathlib.Analysis.Meromorphic.Basic
Meromorphic.deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} [CompleteSpace E], Meromorphic f → Meromorphic (deriv f)
-- Mathlib.Analysis.Asymptotics.TVS
/-- **Alias** of the reverse direction of `Asymptotics.isBigOTVS_iff_isBigO`. -/
Asymptotics.IsBigO.isBigOTVS : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : SeminormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E]
  [inst_4 : NormedSpace 𝕜 F] {f : α → E} {g : α → F} {l : Filter α}, f =O[l] g → f =O[𝕜; l] g
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.instLinear : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      [inst_2 : CategoryTheory.Preadditive C] →
        {R : Type u_1} →
          [inst_3 : Semiring R] →
            [inst_4 : CategoryTheory.Linear R C] →
              [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
                [∀ (n : ℤ), CategoryTheory.Functor.Linear R (CategoryTheory.shiftFunctor C n)] →
                  CategoryTheory.Linear R (CategoryTheory.Pretriangulated.Triangle C)
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.card_omega : ∀ (o : Ordinal.{u_1}), (Ordinal.omega o).card = Cardinal.aleph o
-- Mathlib.Analysis.Analytic.CPolynomialDef
FormalMultilinearSeries.changeOrigin_eval_of_finite : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ},
  (∀ (m : ℕ), n ≤ m → p m = 0) → ∀ (x y : E), (p.changeOrigin x).sum y = p.sum (x + y)
-- Mathlib.NumberTheory.Divisors
Int.divisors_zero : Int.divisors 0 = ∅
-- Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Homeomorph.unitBall_symm_apply : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (a : ↑(Metric.ball 0 1)),
  Homeomorph.unitBall.symm a = ↑(OpenPartialHomeomorph.univUnitBall.toHomeomorphSourceTarget.symm a)
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
SeminormFamily.comp.congr_simp : ∀ {𝕜 : Type u_2} {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} {ι : Type u_9} [inst : NormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : NormedField 𝕜₂] [inst_4 : AddCommGroup F]
  [inst_5 : Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂] (q q_1 : SeminormFamily 𝕜₂ F ι),
  q = q_1 → ∀ (f f_1 : E →ₛₗ[σ₁₂] F), f = f_1 → ∀ (a a_1 : ι), a = a_1 → q.comp f a = q_1.comp f_1 a_1
-- Mathlib.Algebra.Star.UnitaryStarAlgAut
Unitary.conjStarAlgAut.congr_simp : ∀ (S : Type u_1) (R : Type u_2) [inst : Semiring R] [inst_1 : StarMul R] [inst_2 : SMul S R]
  [inst_3 : IsScalarTower S R R] [inst_4 : SMulCommClass S R R], Unitary.conjStarAlgAut S R = Unitary.conjStarAlgAut S R
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.ι_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X : P.FullSubcategory},
  P.ι.obj X = X.obj
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- An Unoriented angle is unchanged by replacing the third point by one weakly further away on the
same ray.  -/
Wbtw.angle_eq_right : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₂ p₃ p : P} (p₁ : P),
  Wbtw ℝ p₂ p₃ p → p₃ ≠ p₂ → EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₁ p₂ p
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
/-- A functor preserves finite effective epimorphic families if it maps finite effective epimorphic
families to effective epimorphic families.
 -/
CategoryTheory.Functor.PreservesFiniteEffectiveEpiFamilies.preserves : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {D : Type u_2}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {F : CategoryTheory.Functor C D}
  [self : F.PreservesFiniteEffectiveEpiFamilies] {α : Type} [Finite α] {B : C} (X : α → C) (π : (a : α) → X a ⟶ B)
  [CategoryTheory.EffectiveEpiFamily X π], CategoryTheory.EffectiveEpiFamily (fun a => F.obj (X a)) fun a => F.map (π a)
-- Mathlib.GroupTheory.Nilpotent
/-- The nilpotency class of a product is the max of the nilpotency classes of the
factors.  -/
AddGroup.nilpotencyClass_sum : ∀ {G₁ : Type u_2} {G₂ : Type u_3} [inst : AddGroup G₁] [inst_1 : AddGroup G₂] [AddGroup.IsNilpotent G₁]
  [AddGroup.IsNilpotent G₂],
  AddGroup.nilpotencyClass (G₁ × G₂) = max (AddGroup.nilpotencyClass G₁) (AddGroup.nilpotencyClass G₂)
-- Mathlib.Data.Finset.SDiff
Finset.sdiff_inter_self_right : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), s \ (t ∩ s) = s \ t
-- Init.PropLemmas
exists_eq_left : ∀ {α : Sort u_1} {p : α → Prop} {a' : α}, (∃ a, a = a' ∧ p a) ↔ p a'
-- Mathlib.Data.Bundle
Bundle.TotalSpace.range_mk : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} (b : B),
  Set.range (Bundle.TotalSpace.mk b) = Bundle.TotalSpace.proj ⁻¹' {b}
-- Mathlib.Topology.Separation.Hausdorff
T2Quotient.lift_mk : ∀ {X : Type u_3} {Y : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : T2Space Y]
  {f : X → Y} (hf : Continuous f) (x : X), T2Quotient.lift hf (T2Quotient.mk x) = f x
-- Mathlib.Algebra.Group.ULift
ULift.one_down : ∀ {α : Type u} [inst : One α], ULift.down 1 = 1
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.instIsLocalizationLocalizedMonoidalToMonoidalCategory : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit),
  (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).IsLocalization W
-- Mathlib.Algebra.Group.Defs
/-- A variant of `npowRec` which is a semigroup homomorphism from `ℕ₊` to `M`.
 -/
npowRec' : {M : Type u_2} → [One M] → [Mul M] → ℕ → M → M
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
/-- A simple sufficient condition for bounding `levyProkhorovEDist` between probability measures
from above. The condition involves only one of two natural bounds, the other bound is for free.  -/
MeasureTheory.levyProkhorovEDist_le_of_forall_le : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω]
  (μ ν : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν]
  (δ : ENNReal),
  (∀ (ε : ENNReal) (B : Set Ω), δ < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (Metric.thickening ε.toReal B) + ε) →
    MeasureTheory.levyProkhorovEDist μ ν ≤ δ
-- Lean.Elab.PreDefinition.PartialFixpoint.Eqns
Lean.Elab.PartialFixpoint.instInhabitedEqnInfo : Inhabited Lean.Elab.PartialFixpoint.EqnInfo
-- Mathlib.Algebra.Lie.Free
/-- If `α` is a type, and `R` is a commutative ring, then `FreeLieAlgebra R α` is
the free Lie algebra over `R` generated by `α`. This is a Lie algebra over `R`
equipped with a function `FreeLieAlgebra.of R : α → FreeLieAlgebra R α`
which has the following universal property: if `L` is any Lie algebra over `R`,
and `f : α → L` is any function, then this function is the composite of
`FreeLieAlgebra.of R` and a unique Lie algebra homomorphism
`FreeLieAlgebra.lift R f : FreeLieAlgebra R α →ₗ⁅R⁆ L`.

A typical element of `FreeLieAlgebra R α` is an `R`-linear combination of
formal brackets of elements of `α`. For example if `x` and `y` are terms of type `α`
and `a` and `b` are terms of type `R` then
`(3 * a * a) • ⁅⁅x, y⁆, x⁆ - (2 * b - 1) • ⁅y, x⁆` is a "typical" element of `FreeLieAlgebra R α`.
 -/
FreeLieAlgebra : (R : Type u) → Type v → [CommRing R] → Type (max u v)
-- Mathlib.GroupTheory.Coprod.Basic
/-- Isomorphism between `PUnit ∗ M` and `M`.  -/
MulEquiv.punitCoprod : (M : Type u_1) → [inst : Monoid M] → Monoid.Coprod PUnit.{u_4 + 1} M ≃* M
-- Lean.Meta.Sym.Pattern
/-- If `checkTypeMask? = some mask`, then we must check the type of pattern variable `i`
if `mask[i]` is true.
Moreover `mask.size == varTypes.size`.
See `mkCheckTypeMask`
 -/
Lean.Meta.Sym.Pattern.checkTypeMask? : Lean.Meta.Sym.Pattern → Option (Array Bool)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.zero_mem_nsmul : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] {s : Finset α} {n : ℕ}, 0 ∈ s → 0 ∈ n • s
-- Mathlib.Algebra.Group.Submonoid.MulAction
Submonoid.instMulActionSubtypeMem.eq_1 : ∀ {M' : Type u_1} {α : Type u_2} {S' : Type u_4} [inst : SetLike S' M'] (s : S') [inst_1 : Monoid M']
  [inst_2 : SubmonoidClass S' M'] [inst_3 : MulAction M' α],
  Submonoid.instMulActionSubtypeMem s = { toSMul := Submonoid.instSMulSubtypeMem s, mul_smul := ⋯, one_smul := ⋯ }