mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_union_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ ∪ m₂)[k]? = m₁[k]?
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.map_one : ∀ {α : Type u} [inst : One α] {β : Type u_1} (f : α → β), WithBot.map f 1 = ↑(f 1)
-- Mathlib.Data.Finsupp.Order
Finsupp.decidableLE : {ι : Type u_1} →
  {α : Type u_3} →
    [inst : AddCommMonoid α] →
      [inst_1 : PartialOrder α] → [CanonicallyOrderedAdd α] → [DecidableLE α] → DecidableLE (ι →₀ α)
-- Mathlib.RingTheory.MvPowerSeries.Inverse
MvPowerSeries.inv.aux.eq_def : ∀ {σ : Type u_1} {R : Type u_2} [inst : Ring R] (a : R) (φ : MvPowerSeries σ R) (x : σ →₀ ℕ),
  MvPowerSeries.inv.aux a φ x =
    have n := x;
    if n = 0 then a
    else
      -a *
        ∑ x ∈ Finset.HasAntidiagonal.antidiagonal n,
          if x_1 : x.2 < n then (MvPowerSeries.coeff x.1) φ * MvPowerSeries.inv.aux a φ x.2 else 0
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.leftUnitor_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] (P : C),
  (CategoryTheory.Limits.coprod.leftUnitor P).inv = CategoryTheory.Limits.coprod.inr
-- Mathlib.Algebra.Notation.Defs
ite_mul : ∀ {α : Type u_2} (P : Prop) [inst : Decidable P] [inst_1 : Mul α] (a b c : α),
  (if P then a else b) * c = if P then a * c else b * c
-- Mathlib.Topology.Instances.ENNReal.Lemmas
Filter.Tendsto.edist : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] {f g : β → α} {x : Filter β} {a b : α},
  Filter.Tendsto f x (nhds a) →
    Filter.Tendsto g x (nhds b) → Filter.Tendsto (fun x => edist (f x) (g x)) x (nhds (edist a b))
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.logMap_expMapBasis : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.realSpace K),
  NumberField.mixedEmbedding.logMap
        (NumberField.mixedEmbedding.mixedSpaceOfRealSpace (↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis x)) ∈
      ZSpan.fundamentalDomain
        (Module.Basis.ofZLatticeBasis ℝ (NumberField.Units.unitLattice K) (NumberField.Units.basisUnitLattice K)) ↔
    ∀ (w : NumberField.InfinitePlace K), w ≠ NumberField.Units.dirichletUnitTheorem.w₀ → x w ∈ Set.Ico 0 1
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.instMonoidalLocalizedMonoidalToMonoidalCategory : {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 ε).Monoidal
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
tateComplexConnectData_d₀ : ∀ {R G : Type u} [inst : CommRing R] [inst_1 : Group G] [inst_2 : Fintype G] (M : Rep.{u, u, u} R G),
  (tateComplexConnectData M).d₀ = M.tateNorm
-- Mathlib.RingTheory.Polynomial.Nilpotent
Polynomial.isUnit_iff' : ∀ {R : Type u_1} [inst : CommRing R] {P : Polynomial R},
  IsUnit P ↔ IsUnit (Polynomial.eval 0 P) ∧ IsNilpotent (P /ₘ Polynomial.X)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_filter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] {f : α → β → Bool} {k fallback : α} (h : m.WF),
  (Std.HashMap.Raw.filter f m).getKeyD k fallback = ((m.getKey? k).pfilter fun x h' => f x m[x]).getD fallback
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- Translates of a block form a block system  -/
AddAction.IsBlock.isBlockSystem : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] {B : Set X}
  [hGX : AddAction.IsPretransitive G X],
  AddAction.IsBlock G B → B.Nonempty → AddAction.IsBlockSystem G (Set.range fun g => g +ᵥ B)
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_one_add : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {b : H} [inst_1 : AddCommMonoidWithOne G]
  [inst_2 : Add H] [AddConstMapClass F G H 1 b] (f : F) (x : G), f (1 + x) = f x + b
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- The parts cover everything  -/
OrderedFinpartition.cover : ∀ {n : ℕ} (self : OrderedFinpartition n) (x : Fin n), ∃ m, x ∈ Set.range (self.emb m)
-- Mathlib.RingTheory.Extension.Cotangent.Basis
/-- Version of `Algebra.Generators.exists_presentation_of_free_cotangent` taking a basis instead
of a `Module.Free` assumption.
Note that the basis `b₀` only serves as a way of saying
that `I/I²` is free of rank `σ`, which gives more definitional control over `σ`.
If this does not matter, use `Algebra.Generators.exists_presentation_of_free_cotangent` instead.
 -/
Algebra.Generators.exists_presentation_of_basis_cotangent : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.FinitePresentation R S] {α : Type u_4} (P : Algebra.Generators R S α) [Finite α] {σ : Type u_5}
  (b₀ : Module.Basis σ S P.toExtension.Cotangent),
  ∃ P' b, P'.val ∘ Sum.inr = P.val ∧ ∀ (r : Unit ⊕ σ), b r = Algebra.Extension.Cotangent.mk ⟨P'.relation r, ⋯⟩
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.reindex_val : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} (P : Algebra.Generators R S ι') (e : ι ≃ ι'), (P.reindex e).val = P.val ∘ ⇑e
-- Mathlib.Algebra.Group.ULift
ULift.vadd_down : ∀ {α : Type u} {β : Type v} [inst : VAdd β α] (a : ULift.{w, u} α) (b : β), (b +ᵥ a).down = b +ᵥ a.down
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.ker_incl : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M), N.incl.ker = ⊥
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.triangle_inv_assoc : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈}
  {C'' : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'}
  {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''}
  {Z : CategoryTheory.Limits.CatCospanTransform F G F'' G''} (h : ψ.comp φ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (ψ.associator (CategoryTheory.Limits.CatCospanTransform.id F' G') φ).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight ψ.rightUnitor.hom φ) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ φ.leftUnitor.hom)
      h
-- Mathlib.FieldTheory.Relrank
IntermediateField.relrank_dvd_rank_bot : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A B : IntermediateField F E),
  A.relrank B ∣ Module.rank F ↥B
-- Mathlib.FieldTheory.CardinalEmb
Field.Emb.Cardinal.filtration_apply : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] [inst_3 : Algebra.IsAlgebraic F E]
  (i : WithTop (Module.rank F E).ord.ToType),
  Field.Emb.Cardinal.filtration i =
    WithTop.recTopCoe ⊤
      (fun x =>
        IntermediateField.adjoin F
          ((fun a => (Field.Emb.Cardinal.wellOrderedBasis F E) (Field.Emb.Cardinal.leastExt F E a)) '' Set.Iio x))
      i
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.even_zsmul_periodic : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddGroup α] [inst_1 : InvolutiveNeg β],
  Function.Antiperiodic f c → ∀ (n : ℤ), Function.Periodic f ((2 * n) • c)
-- Mathlib.Data.Bool.Count
List.IsChain.count_false_eq_count_true : ∀ {l : List Bool}, List.IsChain (fun x1 x2 => x1 ≠ x2) l → Even l.length → List.count false l = List.count true l
-- Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
/-- The special-value formula `Γ(1/2) = √π`, which is equivalent to the Gaussian integral.  -/
Complex.Gamma_one_half_eq : Complex.Gamma (1 / 2) = ↑Real.pi ^ (1 / 2)
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.HeapNode.toHeap.go.eq_1 : ∀ {α : Type u_1} (a : ℕ) (a_1 : Batteries.BinomialHeap.Imp.Heap α),
  Batteries.BinomialHeap.Imp.HeapNode.toHeap.go Batteries.BinomialHeap.Imp.HeapNode.nil a a_1 = a_1
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.balRight.match_1.congr_eq_3 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (l : RBTree.RBNode α)
  (h_1 :
    (a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.black a x b))
  (h_2 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.black b y c)))
  (h_3 : (l : RBTree.RBNode α) → motive l) (l_1 : RBTree.RBNode α),
  l = l_1 →
    (∀ (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α),
        l_1 = RBTree.RBNode.node RBTree.RBColor.black a x b → False) →
      (∀ (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α),
          l_1 = RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.black b y c) → False) →
        (match l with
          | RBTree.RBNode.node RBTree.RBColor.black a x b => h_1 a x b
          | RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.black b y c) => h_2 a x b y c
          | l => h_3 l) ≍
          h_3 l_1
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.first?_eq_match_step : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β] [inst_2 : Std.IteratorLoop α m m]
  [LawfulMonad m] [Std.Iterators.Productive α m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β},
  it.first? = do
    let __do_lift ← it.step
    match ↑__do_lift.inflate with
      | Std.IterStep.yield it out => pure (some out)
      | Std.IterStep.skip it' => it'.first?
      | Std.IterStep.done => pure none
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- The angle ∡AAB at a point.  -/
EuclideanGeometry.oangle_self_left : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  (p₁ p₂ : P), EuclideanGeometry.oangle p₁ p₁ p₂ = 0
-- Mathlib.Data.Nat.PSub
_private.Mathlib.Data.Nat.PSub.0.Nat.ppred.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Geometry.Diffeology.Basic
/-- The D-topology that the diffeology built from this structure will use. Can be overwritten
to allow for better definitional equalities.  -/
DiffeologicalSpace.CorePlotsOn.dTopology : {X : Type u_1} → DiffeologicalSpace.CorePlotsOn X → TopologicalSpace X
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.length_simple_mul_ne : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W) (i : B),
  cs.length (cs.simple i * w) ≠ cs.length w
-- Mathlib.Topology.Connected.TotallyDisconnected
TotallyDisconnectedSpace.mk : ∀ {α : Type u} [inst : TopologicalSpace α], IsTotallyDisconnected Set.univ → TotallyDisconnectedSpace α
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.zipWithTR.go.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (motive : List α → List β → Array γ → Sort u_4) (x : List α)
  (x_1 : List β) (acc : Array γ)
  (h_1 : (a : α) → (as : List α) → (b : β) → (bs : List β) → (acc : Array γ) → motive (a :: as) (b :: bs) acc)
  (h_2 : (x : List α) → (x_2 : List β) → (acc : Array γ) → motive x x_2 acc),
  (∀ (a : α) (as : List α) (b : β) (bs : List β), x = a :: as → x_1 = b :: bs → False) →
    (match x, x_1, acc with
      | a :: as, b :: bs, acc => h_1 a as b bs acc
      | x, x_3, acc => h_2 x x_3 acc) =
      h_2 x x_1 acc
-- Mathlib.Analysis.Convex.Cone.Dual
/-- The inner dual cone of a singleton is given by the preimage of the positive cone under the
linear map `p x`.  -/
ProperCone.dual_singleton : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : TopologicalSpace R] [inst_4 : ClosedIciTopology R] [inst_5 : AddCommGroup M] [inst_6 : Module R M]
  [inst_7 : TopologicalSpace M] [inst_8 : AddCommGroup N] [inst_9 : Module R N] [inst_10 : TopologicalSpace N]
  {p : M →ₗ[R] N →ₗ[R] R} [inst_11 : p.IsContPerfPair] [inst_12 : IsTopologicalRing R] [inst_13 : OrderClosedTopology R]
  (x : M), ProperCone.dual p {x} = ProperCone.comap (p.toContPerfPair x) (ProperCone.positive R R)
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.startsWith_string_eq_startsWith_toSlice : ∀ {pat : String} {s : String.Slice}, s.startsWith pat = s.startsWith pat.toSlice
-- Mathlib.Order.Bounds.Image
IsGreatest.isLeast_image2_of_isLeast : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β} {a : α} {b : β},
  (∀ (b : β), Antitone (Function.swap f b)) →
    (∀ (a : α), Monotone (f a)) → IsGreatest s a → IsLeast t b → IsLeast (Set.image2 f s t) (f a b)
-- Mathlib.Analysis.Analytic.Constructions
analyticWithinAt_const : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {v : F} {s : Set E} {x : E},
  AnalyticWithinAt 𝕜 (fun x => v) s x
-- Lean.Meta.Match.SolveOverlap
_private.Lean.Meta.Match.SolveOverlap.0.Lean.Meta.Match.injectionAnyCandidate? : Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.Expr))
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.coe_mul : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module A V] (ρ : Representation A G V) (f g : ρ.IntertwiningMap ρ),
  (f * g).toLinearMap = f.toLinearMap * g.toLinearMap
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
instAlgebraQuotientIdealResidueField : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → [inst_1 : I.IsPrime] → Algebra (R ⧸ I) I.ResidueField
-- Lean.Elab.Declaration
_private.Lean.Elab.Declaration.0.Lean.Elab.Command.isMutualPreambleCommand : Lean.Syntax → Bool
-- Lean.Meta.Tactic.Grind.PP
_private.Lean.Meta.Tactic.Grind.PP.0.Lean.Meta.Grind.ppThresholds : Lean.Grind.Config → Lean.Meta.Grind.M✝ Unit
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueD_congr : ∀ {α : Type u} {β : Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {a b : α} {fallback : β},
  (a == b) = true → Std.Internal.List.getValueD a l fallback = Std.Internal.List.getValueD b l fallback
-- Init.System.ST
/-- A restricted version of `IO` in which mutable state and exceptions are the only side effects.

It is possible to run `EST` computations in a non-monadic context using `runEST`.
 -/
EST : Type → Type → Type → Type
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
/-- Conjugation in `G` as a morphism. This is the map `(x, y) ↦ x * y * x⁻¹`,
see `CategoryTheory.GrpObj.lift_conj_eq_mul_mul_inv`.  -/
CategoryTheory.GrpObj.conj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (G : C) → [CategoryTheory.GrpObj G] → CategoryTheory.MonoidalCategoryStruct.tensorObj G G ⟶ G
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape.colimitsOfShape_le : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} (P : CategoryTheory.ObjectProperty C) (J : Type u')
  {inst_1 : CategoryTheory.Category.{v', u'} J} [self : P.IsClosedUnderColimitsOfShape J], P.colimitsOfShape J ≤ P
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_append_of_containsKey_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α},
  Std.Internal.List.containsKey a l' = false → Std.Internal.List.getKey? a (l ++ l') = Std.Internal.List.getKey? a l
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.isEmpty_takeEndWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] [inst_2 : String.Slice.Pattern.BackwardPattern pat]
  [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat] {s : String.Slice},
  (s.takeEndWhile pat).isEmpty = !s.endsWith pat
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.fixedPoints : ∀ (G : Type u_1) (L : Type u_4) [inst : Group G] [inst_1 : Field L] [inst_2 : MulSemiringAction G L] [Finite G]
  [FaithfulSMul G L], IsGaloisGroup G (↥(FixedPoints.subfield G L)) L
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.coneOfIsRightKanExtension_pt : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : L.comp F' ⟶ F) [inst_3 : F'.IsRightKanExtension α] (c : CategoryTheory.Limits.Cone F),
  (F'.coneOfIsRightKanExtension α c).pt = c.pt
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn_stringSlice : ∀ {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {Pred EPred : Type (max u₁ u₂)} [inst : Monad m]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {s : String.Slice} {init : β} {f : Char → β → m (ForInStep β)}
  (inv : Std.Internal.Do.StringSliceInvariant s β Pred) {epost : EPred},
  (∀ (pos : s.Pos) (b : β) (h : pos ≠ s.endPos),
      ⦃ inv pos b ⦄ f (pos.get h) b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv (pos.next h) b'
        | ForInStep.done b' => inv s.endPos b';
        epost ⦄) →
    ⦃ inv s.startPos init ⦄ forIn s init f ⦃ fun b => inv s.endPos b; epost ⦄
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.characteristic_iff_le_map : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G},
  H.Characteristic ↔ ∀ (ϕ : G ≃+ G), H ≤ AddSubgroup.map ϕ.toAddMonoidHom H
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.lowerBoundP?.eq_1 : ∀ {α : Type u_1} {cmp : α → α → Ordering} (t : RBTree.RBSet α cmp) (cut : α → Ordering),
  t.lowerBoundP? cut = RBTree.RBNode.lowerBound? cut ↑t
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.outerMeasure_exists_open : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] {A : Set G},
  μ.outerMeasure A ≠ ⊤ → ∀ {ε : NNReal}, ε ≠ 0 → ∃ U, A ⊆ ↑U ∧ μ.outerMeasure ↑U ≤ μ.outerMeasure A + ↑ε
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_comp₂ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace δ] [inst_2 : TopologicalSpace β] [inst_3 : TopologicalSpace γ] (g : β → γ → δ)
  (hg : Continuous (Function.uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ),
  ↑(MeasureTheory.AEEqFun.comp₂ g hg f₁ f₂) =ᵐ[μ] fun a => g (↑f₁ a) (↑f₂ a)
-- Init.Data.List.Pairwise
List.getElem?_inj : ∀ {α : Type u_1} {i j : ℕ} {l : List α}, i < l.length → l.Nodup → (l[i]? = l[j]? ↔ i = j)
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.formatMonthShort : Std.Time.DateFormatSymbols → Std.Time.Month.Ordinal → String
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.inv_hom_id_toNatTrans_app : ∀ {X Y : CategoryTheory.Cat} {F G : X ⟶ Y} (e : F ≅ G) (A : ↑X),
  CategoryTheory.CategoryStruct.comp (e.inv.toNatTrans.app A) (e.hom.toNatTrans.app A) =
    CategoryTheory.CategoryStruct.id (G.toFunctor.obj A)
-- Init.Data.SInt.Basic
instLEInt64 : LE Int64
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_subset_zero_on_sdiff : ∀ {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [inst : AddCommMonoid M] {f g : ι → M} [inst_1 : DecidableEq ι],
  s₁ ⊆ s₂ → (∀ x ∈ s₂ \ s₁, g x = 0) → (∀ x ∈ s₁, f x = g x) → ∑ i ∈ s₁, f i = ∑ i ∈ s₂, g i
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.monadLift_StateT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α σ : Type u} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] (x : m α)
  (Q : Std.Do.PostCond α (Std.Do.PostShape.arg σ ps)),
  ⦃fun s => (Std.Do.wp x).apply (fun a => Q.1 a s, Q.2)⦄ MonadLift.monadLift x ⦃Q⦄
-- Mathlib.CategoryTheory.Monad.Limits
/-- A monadic functor creates any colimits of shapes it preserves.  -/
CategoryTheory.monadicCreatesColimitsOfShapeOfPreservesColimitsOfShape : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type u} →
          [inst_2 : CategoryTheory.Category.{v, u} J] →
            (R : CategoryTheory.Functor D C) →
              [CategoryTheory.MonadicRightAdjoint R] →
                [CategoryTheory.Limits.PreservesColimitsOfShape J R] → CategoryTheory.CreatesColimitsOfShape J R
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.ext : ∀ {x y : DyckWord}, ↑x = ↑y → x = y
-- Mathlib.Logic.Equiv.Defs
Equiv.comp_surjective : ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (f : α → β) (e : β ≃ γ), Function.Surjective (⇑e ∘ f) ↔ Function.Surjective f
-- Mathlib.MeasureTheory.Function.ConvergenceInDistribution
MeasureTheory.tendstoInDistribution_of_identDistrib : ∀ {ι : Type u_1} {E : Type u_2} {Ω' : Type u_3} {Ω : ι → Type u_5} {m : (i : ι) → MeasurableSpace (Ω i)}
  {μ : (i : ι) → MeasureTheory.Measure (Ω i)} [inst : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)]
  {m' : MeasurableSpace Ω'} {μ' : MeasureTheory.Measure Ω'} [inst_1 : MeasureTheory.IsProbabilityMeasure μ']
  {mE : MeasurableSpace E} {X : (i : ι) → Ω i → E} {Z : Ω' → E} {l : Filter ι} [inst_2 : TopologicalSpace E]
  [inst_3 : OpensMeasurableSpace E] (i : ι),
  (∀ (j : ι), ProbabilityTheory.IdentDistrib (X i) (X j) (μ i) (μ j)) →
    ProbabilityTheory.IdentDistrib (X i) Z (μ i) μ' → MeasureTheory.TendstoInDistribution X l Z μ μ'
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
/-- Casting a scientific literal via `ℚ≥0` is the same as casting directly.  -/
NNRat.cast_ofScientific : ∀ {K : Type u_1} [inst : NNRatCast K] (m : ℕ) (s : Bool) (e : ℕ),
  ↑(OfScientific.ofScientific m s e) = OfScientific.ofScientific m s e
-- Lean.Data.Lsp.Internal
Lean.Lsp.instFromJsonLeanImportClosureParams : Lean.FromJson Lean.Lsp.LeanImportClosureParams
-- Mathlib.AlgebraicGeometry.Limits
/-- This is true in general for finite discrete schemes. See below.  -/
AlgebraicGeometry.instIsAffineOfSubsingletonCarrierCarrierCommRingCat : ∀ {X : AlgebraicGeometry.Scheme} [Subsingleton ↥X], AlgebraicGeometry.IsAffine X