mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Option.Basic
Option.casesOn'_none_coe : ∀ {α : Type u_1} {β : Type u_2} (f : Option α → β) (o : Option α), o.casesOn' (f none) (f ∘ fun a => some a) = f o
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey!_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited α] {l : List (α × β)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → (Std.ExtDHashMap.Const.ofList l).getKey! k' = k
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.appLE.congr_simp : ∀ {X Y : AlgebraicGeometry.Scheme} (f f_1 : X ⟶ Y) (e_f : f = f_1) (U : Y.Opens) (V : X.Opens)
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
  AlgebraicGeometry.Scheme.Hom.appLE f U V e = AlgebraicGeometry.Scheme.Hom.appLE f_1 U V ⋯
-- Mathlib.Topology.Order.LocalExtr
IsLocalMin.eq_1 : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] (f : α → β) (a : α),
  IsLocalMin f a = IsMinFilter f (nhds a) a
-- Init.Data.String.Lemmas.Basic
String.Slice.Pos.slice_eq_endPos : ∀ {s : String.Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁}, p₁.slice p₀ p₁ h ⋯ = (s.slice p₀ p₁ ⋯).endPos
-- Mathlib.CategoryTheory.Sites.Precoverage
/-- A precoverage is stable under composition if the indexed composition
of coverings is again a covering.
Use `Precoverage.comp_mem_coverings` for less universe restrictions.
Note: This is stronger than the analogous requirement for a `Pretopology`, because
this is in general not equal to a `Presieve.bind`.  -/
CategoryTheory.Precoverage.IsStableUnderComposition : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Precoverage C → Prop
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
GaloisConnection.cof_le : ∀ {α γ : Type u} [inst : Preorder α] [inst_1 : Preorder γ] {f : γ → α} {g : α → γ},
  GaloisConnection f g → Order.cof γ ≤ Order.cof α
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.num.sizeOf_spec : ∀ (v : ℕ), sizeOf (Nat.Internal.Linear.Expr.num v) = 1 + sizeOf v
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.toArrowArrowFunctor_obj_right_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  (CategoryTheory.Square.toArrowArrowFunctor.obj sq).right.hom = sq.f₂₄
-- Lean.Setup
Lean.instInhabitedModuleHeader : Inhabited Lean.ModuleHeader
-- Mathlib.Data.Finset.PImage
Finset.pimage_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α →. β} [inst_1 : (x : α) → Decidable (f x).Dom]
  {s t : Finset α}, s ⊆ t → Finset.pimage f s ⊆ Finset.pimage f t
-- Mathlib.Algebra.CharP.Two
/-- The only hypotheses required to build a `CharP R 2` instance are `1 ≠ 0` and `2 = 0`.  -/
CharTwo.of_one_ne_zero_of_two_eq_zero : ∀ {R : Type u_1} [inst : AddMonoidWithOne R], 1 ≠ 0 → 2 = 0 → CharP R 2
-- Mathlib.Algebra.Notation.Support
Function.mulSupport_eq_preimage : ∀ {ι : Type u_1} {M : Type u_3} [inst : One M] (f : ι → M), Function.mulSupport f = f ⁻¹' {1}ᶜ
-- Mathlib.RingTheory.RootsOfUnity.Basic
rootsOfUnity.coe_pow : ∀ {R : Type u_4} {k : ℕ} [inst : CommMonoid R] (ζ : ↥(rootsOfUnity k R)) (m : ℕ), ↑↑(ζ ^ m) = ↑↑ζ ^ m
-- Mathlib.GroupTheory.OrderOfElement
orderOf_neg_one : ∀ {R : Type u_6} [inst : Ring R] [Nontrivial R], orderOf (-1) = if ringChar R = 2 then 1 else 2
-- Mathlib.GroupTheory.Abelianization.Defs
Abelianization.ker_of : ∀ (G : Type u) [inst : Group G], Abelianization.of.ker = commutator G
-- Mathlib.Data.Nat.BinaryRec
Nat.bit_true_apply : ∀ (n : ℕ), Nat.bit true n = 2 * n + 1
-- Lean.Meta.Sym.Offset
/-- Converts the given expression into an offset.
Assumptions:
- `e` has type `Nat`.
- standard instances are used for `OfNat Nat n` and `HAdd Nat Nat Nat`.
 -/
Lean.Meta.Sym.toOffset : Lean.Expr → Lean.Meta.Sym.Offset
-- Init.Data.Vector.Perm
Vector.instTransPerm : {α : Type u_1} → {n : ℕ} → Trans Vector.Perm Vector.Perm Vector.Perm
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k fallback : α}, k ∉ m₂ → (m₁ ∪ m₂).getKeyD k fallback = m₁.getKeyD k fallback
-- Std.Data.TreeSet.Raw.Basic
/-- Inserts multiple elements into the tree set by iterating over the given collection and calling
`insert`. If the same element (with respect to `cmp`) appears multiple times, the first occurrence
takes precedence.

Note: this precedence behavior is true for `TreeSet` and `TreeSet.Raw`. The `insertMany` function on
`TreeMap`, `DTreeMap`, `TreeMap.Raw` and `DTreeMap.Raw` behaves differently: it will prefer the last
appearance.
 -/
Std.TreeSet.Raw.insertMany : {α : Type u} →
  {cmp : α → α → Ordering} → {ρ : Type u_1} → [ForIn Id ρ α] → Std.TreeSet.Raw α cmp → ρ → Std.TreeSet.Raw α cmp
-- Mathlib.Topology.Closure
Filter.HasBasis.lift'_closure : ∀ {X : Type u} [inst : TopologicalSpace X] {ι : Sort v} {l : Filter X} {p : ι → Prop} {s : ι → Set X},
  l.HasBasis p s → (l.lift' closure).HasBasis p fun i => closure (s i)
-- Lean.Message
Lean.SerialMessage.mk.inj : ∀ {toBaseMessage : Lean.BaseMessage String} {kind : Lean.Name} {toBaseMessage_1 : Lean.BaseMessage String}
  {kind_1 : Lean.Name},
  { toBaseMessage := toBaseMessage, kind := kind } = { toBaseMessage := toBaseMessage_1, kind := kind_1 } →
    toBaseMessage = toBaseMessage_1 ∧ kind = kind_1
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.instInfSet : {C : Type u} → [inst : CategoryTheory.Groupoid C] → InfSet (CategoryTheory.Subgroupoid C)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
CategoryTheory.MonoidalCategory.DayConvolution.unit_app_braiding_hom_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory V] [inst_5 : CategoryTheory.BraidedCategory V]
  (F G : CategoryTheory.Functor C V) [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution F G]
  [inst_7 : CategoryTheory.MonoidalCategory.DayConvolution G F] (x y : C) {Z : V}
  (h :
    (CategoryTheory.MonoidalCategory.DayConvolution.convolution G F).obj
        (CategoryTheory.MonoidalCategoryStruct.tensorObj x y) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (x, y))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.MonoidalCategory.DayConvolution.braiding F G).hom.app
          (CategoryTheory.MonoidalCategoryStruct.tensorObj x y))
        h) =
    CategoryTheory.CategoryStruct.comp (β_ (F.obj x) (G.obj y)).hom
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit G F).app (y, x))
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.MonoidalCategory.DayConvolution.convolution G F).map (β_ y x).hom) h))
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.guard.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.MeasureTheory.Integral.Regular
/-- In a locally compact regular space with an inner regular measure, the measure of a compact
set `k` is the infimum of the integrals of compactly supported functions equal to `1` on `k`.  -/
IsCompact.measure_eq_biInf_integral_hasCompactSupport : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [BorelSpace X] {k : Set X},
  IsCompact k →
    ∀ (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.InnerRegularCompactLTTop]
      [LocallyCompactSpace X] [RegularSpace X],
      μ k =
        ⨅ f,
          ⨅ (_ : Continuous f),
            ⨅ (_ : HasCompactSupport f), ⨅ (_ : Set.EqOn f 1 k), ⨅ (_ : 0 ≤ f), ENNReal.ofReal (∫ (x : X), f x ∂μ)
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instMulOneClass : {α : Type u_1} → [MulOneClass α] → MulOneClass αᵃᵒᵖ
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- The range of a morphism of algebras is a fintype, if the domain is a fintype.

Note that this instance can cause a diamond with `Subtype.fintype` if `B` is also a fintype.  -/
NonUnitalAlgHom.fintypeRange : {F : Type v'} →
  {R : Type u} →
    {A : Type v} →
      {B : Type w} →
        [inst : CommSemiring R] →
          [inst_1 : NonUnitalNonAssocSemiring A] →
            [inst_2 : Module R A] →
              [inst_3 : NonUnitalNonAssocSemiring B] →
                [inst_4 : Module R B] →
                  [inst_5 : FunLike F A B] →
                    [inst_6 : NonUnitalAlgHomClass F R A B] →
                      [Fintype A] → [DecidableEq B] → (φ : F) → Fintype ↥(NonUnitalAlgHom.range φ)
-- Mathlib.Analysis.Polynomial.Norm
Polynomial.supNorm_C : ∀ {A : Type u_1} [inst : SeminormedRing A] {a : A}, (Polynomial.C a).supNorm = ‖a‖
-- Init.Data.String.Lemmas.Iterate
_private.Init.Data.String.Lemmas.Iterate.0.String.foldr.eq_1 : ∀ {α : Type u} (f : Char → α → α) (init : α) (s : String), String.foldr f init s = String.Slice.foldr f init s.toSlice
-- Mathlib.Topology.Order.Hom.Esakia
PseudoEpimorphism.id_apply : ∀ {α : Type u_2} [inst : Preorder α] (a : α), (PseudoEpimorphism.id α) a = a
-- Mathlib.NumberTheory.Modular
ModularGroup.tendsto_abs_re_smul : ∀ (z : UpperHalfPlane) {p : Fin 2 → ℤ},
  IsCoprime (p 0) (p 1) → Filter.Tendsto (fun g => |(↑g • z).re|) Filter.cofinite Filter.atTop
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.size_filterMap_eq_size_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ},
  (Std.ExtDTreeMap.filterMap f t).size = t.size ↔
    ∀ (k : α) (h : k ∈ t), (f (t.getKey k h) (Std.ExtDTreeMap.Const.get t k h)).isSome = true
-- Mathlib.Order.CountableSupClosed
/-- **Alias** of the reverse direction of `countableSupClosed_preimage_ofDual`. -/
CountableInfClosed.dual : ∀ {α : Type u_2} [inst : LE α] {s : Set α}, CountableInfClosed s → CountableSupClosed (⇑OrderDual.ofDual ⁻¹' s)
-- Mathlib.Algebra.AddConstMap.Equiv
/-- A custom projection for `simps`.  -/
AddConstEquiv.Simps.symm_apply : {G : Type u_1} → {H : Type u_2} → [inst : Add G] → [inst_1 : Add H] → {a : G} → {b : H} → AddConstEquiv G H a b → H → G
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.mem_mk' : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {s : Set R} {sg : Subsemigroup R} (hg : ↑sg = s)
  {sa : AddSubmonoid R} (ha : ↑sa = s) {x : R}, x ∈ NonUnitalSubsemiring.mk' s sg hg sa ha ↔ x ∈ s
-- Mathlib.NumberTheory.LegendreSymbol.AddCharacter
AddChar.PrimitiveAddChar.mk.sizeOf_spec : ∀ {R : Type u} [inst : CommRing R] {R' : Type v} [inst_1 : Field R'] [inst_2 : SizeOf R] [inst_3 : SizeOf R'] (n : ℕ+)
  (char : AddChar R (CyclotomicField (↑n) R')) (prim : char.IsPrimitive),
  sizeOf { n := n, char := char, prim := prim } = 1 + sizeOf n + sizeOf char
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.EdgeLabeling.get_mk : ∀ {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} (f : (x y : V) → G.Adj x y → K)
  (f_symm : ∀ (x y : V) (H : G.Adj x y), f y x ⋯ = f x y H) (x y : V) (h : G.Adj x y),
  (SimpleGraph.EdgeLabeling.mk f f_symm).get x y h = f x y h
-- Mathlib.Algebra.Group.Defs
IsRightCancelAdd.mk : ∀ {G : Type u} [inst : Add G], (∀ (a : G), IsAddRightRegular a) → IsRightCancelAdd G
-- Mathlib.Algebra.Free
FreeSemigroup.mk_mul_mk : ∀ {α : Type u} (x y : α) (L1 L2 : List α),
  { head := x, tail := L1 } * { head := y, tail := L2 } = { head := x, tail := L1 ++ y :: L2 }
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.foldTR.loop.match_1.splitter : {α : Type u_2} →
  (n : ℕ) →
    (motive : (x : ℕ) → x ≤ n → α → Sort u_1) →
      (x : ℕ) →
        (x_1 : x ≤ n) →
          (x_2 : α) →
            ((h : 0 ≤ n) → (a : α) → motive 0 h a) →
              ((m : ℕ) → (h : m.succ ≤ n) → (a : α) → motive m.succ h a) → motive x x_1 x_2
-- Mathlib.Probability.BrownianMotion.Basic
ProbabilityTheory.IsPreBrownianReal.hasLaw_sub : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.IsPreBrownianReal B P →
    ∀ (s t : NNReal), ProbabilityTheory.HasLaw (B s - B t) (ProbabilityTheory.gaussianReal 0 (nndist ↑s ↑t)) P
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instSubQuotient : {R : Type u_1} → [inst : AddGroup R] → [inst_1 : Mul R] → (c : RingCon R) → Sub c.Quotient
-- Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits
/-- For `v ∈ K.vertsᶜ \ ErdosStone.filter`, since `v` is adjacent to fewer than `t`
vertices in at least one part of the complete equipartite subgraph, it follows that `v` is
adjacent to fewer than `#K.verts - (t' - t)` vertices in `K.verts`.

This is an auxiliary lemma for the Erdős-Stone theorem.  -/
_private.Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits.0.SimpleGraph.ErdosStone.degree_between_verts_lt_of_mem_sdiff : ∀ {n : ℕ} {G : SimpleGraph (Fin n)} [inst : DecidableRel G.Adj] {r t t' : ℕ} (K : G.CompleteEquipartiteSubgraph r t')
  {v : Fin n},
  v ∈ K.vertsᶜ \ SimpleGraph.ErdosStone.filter✝ K t →
    0 < t' → (SimpleGraph.between (↑K.verts) (↑K.verts)ᶜ G).degree v < K.verts.card - t' + t
-- Lean.Environment
_private.Lean.Environment.0.Lean.AsyncConst.mk.inj : ∀ {constInfo : Lean.AsyncConstantInfo} {exts? : Option (Task (Array Lean.EnvExtensionState))}
  {aconstsImpl : Task Dynamic} {isRealized : Bool} {constInfo_1 : Lean.AsyncConstantInfo}
  {exts?_1 : Option (Task (Array Lean.EnvExtensionState))} {aconstsImpl_1 : Task Dynamic} {isRealized_1 : Bool},
  { constInfo := constInfo, exts? := exts?, aconstsImpl := aconstsImpl, isRealized := isRealized } =
      { constInfo := constInfo_1, exts? := exts?_1, aconstsImpl := aconstsImpl_1, isRealized := isRealized_1 } →
    constInfo = constInfo_1 ∧ exts? = exts?_1 ∧ aconstsImpl = aconstsImpl_1 ∧ isRealized = isRealized_1
-- Mathlib.CategoryTheory.Category.Basic
/-- Postcompose an equation between morphisms by another morphism  -/
CategoryTheory.eq_whisker : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f g : X ⟶ Y},
  f = g → ∀ (h : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Cone.ofTrident_π : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C}
  (t : CategoryTheory.Limits.Trident fun j => F.map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j))
  (j : CategoryTheory.Limits.WalkingParallelFamily J),
  (CategoryTheory.Limits.Cone.ofTrident t).π.app j =
    CategoryTheory.CategoryStruct.comp (t.π.app j) (CategoryTheory.eqToHom ⋯)
-- Init.System.Uri
_private.Init.System.Uri.0.System.Uri.normalizeDriveExpression : String.Slice → String
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_leftUnitor_inv_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 : CategoryTheory.OplaxFunctor B C} (η : x ⟶ x_1) (a : B),
  (CategoryTheory.Bicategory.leftUnitor η).inv.as.app a = (CategoryTheory.Bicategory.leftUnitor (η.app a)).inv
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
ChevalleyThm.MvPolynomialC.numBound.eq_def : ∀ (k : ℕ) (D : ℕ → ℕ) (x : ℕ),
  ChevalleyThm.MvPolynomialC.numBound k D x =
    match x with
    | 0 => k
    | n.succ => ChevalleyThm.MvPolynomialC.numBound k D n * ChevalleyThm.MvPolynomialC.degBound k D n * D n
-- Mathlib.Order.Hom.Basic
OrderEmbedding.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : LE α] [inst_1 : LE β] [inst_2 : LE γ]
  [inst_3 : LE δ] (f : α ↪o β) (g : β ↪o γ) (h : γ ↪o δ), (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.le_induce_union_left : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {s s' : Set V}, G'.induce s ≤ G'.induce (s ∪ s')
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Iso.connectedComponentEquiv_trans : ∀ {V : Type u} {V' : Type v} {V'' : Type w} {G : SimpleGraph V} {G' : SimpleGraph V'} {G'' : SimpleGraph V''}
  (φ : G ≃g G') (φ' : G' ≃g G''),
  SimpleGraph.Iso.connectedComponentEquiv (RelIso.trans φ φ') =
    φ.connectedComponentEquiv.trans φ'.connectedComponentEquiv
-- Mathlib.Analysis.SpecificLimits.Basic
/-- The series `pow r` converges to `(1-r)⁻¹`. For `r < 1` the RHS is a finite number,
and for `1 ≤ r` the RHS equals `∞`.  -/
ENNReal.tsum_geometric : ∀ (r : ENNReal), ∑' (n : ℕ), r ^ n = (1 - r)⁻¹
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
TopCat.stdSimplexHomeomorphI_symm_zero : TopCat.stdSimplexHomeomorphI.symm 0 = stdSimplex.vertex 0
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.coe_toSubmonoid : ∀ {R : Type u} [inst : NonAssocRing R] (s : Subring R), ↑s.toSubmonoid = ↑s
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.mk.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] [inst_2 : SizeOf α]
  [inst_3 : SizeOf β] (toEquiv : α ≃ β) (isometry_toFun : Isometry toEquiv.toFun),
  sizeOf { toEquiv := toEquiv, isometry_toFun := isometry_toFun } = 1 + sizeOf toEquiv
-- Aesop.Tree.Data
Aesop.RappUnsafe.brecOn.eq : ∀ {motive_1 : Aesop.GoalUnsafe → Sort u} {motive_2 : Aesop.MVarClusterUnsafe → Sort u}
  {motive_3 : Aesop.RappUnsafe → Sort u} {motive_4 : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe → Sort u}
  {motive_5 : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe → Sort u}
  {motive_6 : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe → Sort u}
  {motive_7 : Array (IO.Ref Aesop.RappUnsafe) → Sort u} {motive_8 : Option (IO.Ref Aesop.RappUnsafe) → Sort u}
  {motive_9 : Array (IO.Ref Aesop.GoalUnsafe) → Sort u} {motive_10 : Array (IO.Ref Aesop.MVarClusterUnsafe) → Sort u}
  {motive_11 : List (IO.Ref Aesop.RappUnsafe) → Sort u} {motive_12 : List (IO.Ref Aesop.GoalUnsafe) → Sort u}
  {motive_13 : List (IO.Ref Aesop.MVarClusterUnsafe) → Sort u} (t : Aesop.RappUnsafe)
  (F_1 : (t : Aesop.GoalUnsafe) → t.below → motive_1 t) (F_2 : (t : Aesop.MVarClusterUnsafe) → t.below → motive_2 t)
  (F_3 : (t : Aesop.RappUnsafe) → t.below → motive_3 t)
  (F_4 : (t : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe) → Aesop.GoalUnsafe.below_1 t → motive_4 t)
  (F_5 : (t : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe) → Aesop.GoalUnsafe.below_2 t → motive_5 t)
  (F_6 : (t : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe) → Aesop.GoalUnsafe.below_3 t → motive_6 t)
  (F_7 : (t : Array (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_4 t → motive_7 t)
  (F_8 : (t : Option (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_5 t → motive_8 t)
  (F_9 : (t : Array (IO.Ref Aesop.GoalUnsafe)) → Aesop.GoalUnsafe.below_6 t → motive_9 t)
  (F_10 : (t : Array (IO.Ref Aesop.MVarClusterUnsafe)) → Aesop.GoalUnsafe.below_7 t → motive_10 t)
  (F_11 : (t : List (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_8 t → motive_11 t)
  (F_12 : (t : List (IO.Ref Aesop.GoalUnsafe)) → Aesop.GoalUnsafe.below_9 t → motive_12 t)
  (F_13 : (t : List (IO.Ref Aesop.MVarClusterUnsafe)) → Aesop.GoalUnsafe.below_10 t → motive_13 t),
  t.brecOn F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 F_10 F_11 F_12 F_13 =
    F_3 t (Aesop.RappUnsafe.brecOn.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 F_10 F_11 F_12 F_13).2
-- Mathlib.Topology.MetricSpace.Contracting
ContractingWith.dist_fixedPoint_le : ∀ {α : Type u_1} [inst : MetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) [inst_1 : Nonempty α]
  [inst_2 : CompleteSpace α] (x : α), dist x (ContractingWith.fixedPoint f hf) ≤ dist x (f x) / (1 - ↑K)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Pseudofunctor.mapAdjunction_counit : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {a b : B}
  {f : a ⟶ b} {g : b ⟶ a} (F : CategoryTheory.Pseudofunctor B C) (adj : CategoryTheory.Bicategory.Adjunction f g),
  (F.mapAdjunction adj).counit =
    CategoryTheory.CategoryStruct.comp (F.mapComp g f).inv
      (CategoryTheory.CategoryStruct.comp (F.map₂ adj.counit) (F.mapId b).hom)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.exists : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {P : MonoidAlgebra R M → Prop},
  (∃ p, P p) ↔ ∃ q, P (MonoidAlgebra.ofCoeff q)
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- Uniform convergence implies pointwise convergence.  -/
TendstoUniformlyOnFilter.tendsto_at : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {x : α}
  {p : Filter ι} {p' : Filter α},
  TendstoUniformlyOnFilter F f p p' → Filter.principal {x} ≤ p' → Filter.Tendsto (fun n => F n x) p (nhds (f x))
-- Lean.Meta.Tactic.Grind.OrderInsts
Lean.Meta.Grind.mkLawfulOrderLTInst? : Lean.Level → Lean.Expr → Option Lean.Expr → Option Lean.Expr → Lean.Meta.Grind.GoalM (Option Lean.Expr)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2.SupportsStmt.match_1.eq_2 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (motive : Turing.TM2.Stmt Γ Λ σ → Sort u_5) (k : K)
  (a : σ → Option (Γ k) → σ) (q : Turing.TM2.Stmt Γ Λ σ)
  (h_1 : (k : K) → (a : σ → Γ k) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.push k a q))
  (h_2 : (k : K) → (a : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.peek k a q))
  (h_3 : (k : K) → (a : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.pop k a q))
  (h_4 : (a : σ → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.load a q))
  (h_5 : (a : σ → Bool) → (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.branch a q₁ q₂))
  (h_6 : (l : σ → Λ) → motive (Turing.TM2.Stmt.goto l)) (h_7 : Unit → motive Turing.TM2.Stmt.halt),
  (match Turing.TM2.Stmt.peek k a q with
    | Turing.TM2.Stmt.push k a q => h_1 k a q
    | Turing.TM2.Stmt.peek k a q => h_2 k a q
    | Turing.TM2.Stmt.pop k a q => h_3 k a q
    | Turing.TM2.Stmt.load a q => h_4 a q
    | Turing.TM2.Stmt.branch a q₁ q₂ => h_5 a q₁ q₂
    | Turing.TM2.Stmt.goto l => h_6 l
    | Turing.TM2.Stmt.halt => h_7 ()) =
    h_2 k a q
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.reflectionPerm_eq_iff_smul_coroot : ∀ {ι : 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} {i j : ι},
  (P.reflectionPerm i) j = j ↔ P.pairing i j • P.coroot i = 0
-- Mathlib.Algebra.Group.Ext
CancelMonoid.ext_iff : ∀ {M : Type u_1} {m₁ m₂ : CancelMonoid M}, m₁ = m₂ ↔ HMul.hMul = HMul.hMul
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes right covariance.
The lemma assuming left covariance is `Left.add_pos_of_nonneg_of_pos`.  -/
Right.add_pos_of_nonneg_of_pos : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddRightMono α] {a b : α}, 0 ≤ a → 0 < b → 0 < a + b
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
MeasureTheory.lintegral_insert : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasurableSingletonClass α] {a : α}
  {s : Set α}, a ∉ s → ∀ (f : α → ENNReal), ∫⁻ (x : α) in insert a s, f x ∂μ = f a * μ {a} + ∫⁻ (x : α) in s, f x ∂μ
-- Mathlib.RepresentationTheory.Subrepresentation
Subrepresentation.subrepresentationSubmoduleOrderIso_symm_apply : ∀ {A : Type u_1} {G : Type u_2} {W : Type u_3} [inst : CommSemiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid W]
  [inst_3 : Module A W] {ρ : Representation A G W} (N : Submodule (MonoidAlgebra A G) ρ.asModule),
  (RelIso.symm Subrepresentation.subrepresentationSubmoduleOrderIso) N = Subrepresentation.ofSubmodule' N
-- Init.Data.String.Basic
String.Pos.eq_copy_sliceTo_append_get : ∀ {s : String} {pos : s.Pos} (h : pos ≠ s.endPos),
  s = (s.sliceTo pos).copy ++ String.singleton (pos.get h) ++ (s.sliceFrom (pos.next h)).copy