mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Slice
String.Slice.RevSplitIterator.instIteratorOfPure.eq_1 : ∀ {ρ : Type} {ρ_1 : ρ} {σ : String.Slice → Type}
  [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [inst_1 : String.Slice.Pattern.ToBackwardSearcher ρ_1 σ] {m : Type → Type u_1} {s : String.Slice} [inst_2 : Pure m],
  String.Slice.RevSplitIterator.instIteratorOfPure =
    {
      IsPlausibleStep := fun x x_1 =>
        match x, x_1 with
        | { internalState := String.Slice.RevSplitIterator.operating currPos s_1 },
          Std.IterStep.yield { internalState := String.Slice.RevSplitIterator.operating currPos_1 s' } out =>
          s'.IsPlausibleSuccessorOf s_1
        | { internalState := String.Slice.RevSplitIterator.operating currPos s },
          Std.IterStep.yield { internalState := String.Slice.RevSplitIterator.atEnd } out => True
        | { internalState := String.Slice.RevSplitIterator.operating currPos s_1 },
          Std.IterStep.skip { internalState := String.Slice.RevSplitIterator.operating currPos_1 s' } =>
          s'.IsPlausibleSuccessorOf s_1
        | { internalState := String.Slice.RevSplitIterator.operating currPos s },
          Std.IterStep.skip { internalState := String.Slice.RevSplitIterator.atEnd } => False
        | { internalState := String.Slice.RevSplitIterator.operating currPos s }, Std.IterStep.done => True
        | { internalState := String.Slice.RevSplitIterator.atEnd }, Std.IterStep.yield it out => False
        | { internalState := String.Slice.RevSplitIterator.atEnd }, Std.IterStep.skip it => False
        | { internalState := String.Slice.RevSplitIterator.atEnd }, Std.IterStep.done => True,
      step := fun x =>
        match x with
        | { internalState := String.Slice.RevSplitIterator.operating currPos searcher } =>
          match h : searcher.step with
          | ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.matched startPos endPos), hps⟩ =>
            have slice := s.slice! endPos currPos;
            let nextIt := { internalState := String.Slice.RevSplitIterator.operating startPos searcher' };
            pure (Std.Shrink.deflate ⟨Std.IterStep.yield nextIt slice, ⋯⟩)
          | ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.rejected startPos endPos), hps⟩ =>
            pure
              (Std.Shrink.deflate
                ⟨Std.IterStep.skip { internalState := String.Slice.RevSplitIterator.operating currPos searcher' }, ⋯⟩)
          | ⟨Std.IterStep.skip searcher', hps⟩ =>
            pure
              (Std.Shrink.deflate
                ⟨Std.IterStep.skip { internalState := String.Slice.RevSplitIterator.operating currPos searcher' }, ⋯⟩)
          | ⟨Std.IterStep.done, property⟩ =>
            if currPos ≠ s.startPos then
              have slice := s.sliceTo currPos;
              pure
                (Std.Shrink.deflate
                  ⟨Std.IterStep.yield { internalState := String.Slice.RevSplitIterator.atEnd } slice, ⋯⟩)
            else pure (Std.Shrink.deflate ⟨Std.IterStep.done, ⋯⟩)
        | { internalState := String.Slice.RevSplitIterator.atEnd } => pure (Std.Shrink.deflate ⟨Std.IterStep.done, ⋯⟩) }
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.isVanKampenColimit_of_isEmpty : ∀ {J : Type v'} [inst : CategoryTheory.Category.{u', v'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasStrictInitialObjects C] [IsEmpty J] {F : CategoryTheory.Functor J C}
  (c : CategoryTheory.Limits.Cocone F) (hc : CategoryTheory.Limits.IsColimit c), CategoryTheory.IsVanKampenColimit c
-- Lean.Declaration
Lean.mkQuotValEx : Lean.Name → List Lean.Name → Lean.Expr → Lean.QuotKind → Lean.QuotVal
-- Mathlib.Data.Fin.Tuple.Basic
/-- Adding an element at the beginning of an `n`-tuple, to get an `n+1`-tuple.  -/
Fin.cons : {n : ℕ} → {α : Fin (n + 1) → Sort u} → α 0 → ((i : Fin n) → α i.succ) → (i : Fin (n + 1)) → α i
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.toList_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp}, t.keysArray.toList = t.keys
-- Mathlib.ModelTheory.Semantics
_private.Mathlib.ModelTheory.Semantics.0.FirstOrder.Language.Term.restrictVarLeft.match_1.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u_4} {β : Type u_6} [inst : DecidableEq α] {γ : Type u_3}
  (motive : (x : L.Term (α ⊕ γ)) → (↥x.varFinsetLeft → β) → Sort u_5) (a : α)
  (f : ↥(FirstOrder.Language.var (Sum.inl a)).varFinsetLeft → β)
  (h_1 :
    (a : α) →
      (f : ↥(FirstOrder.Language.var (Sum.inl a)).varFinsetLeft → β) → motive (FirstOrder.Language.var (Sum.inl a)) f)
  (h_2 :
    (a : γ) →
      (_f : ↥(FirstOrder.Language.var (Sum.inr a)).varFinsetLeft → β) → motive (FirstOrder.Language.var (Sum.inr a)) _f)
  (h_3 :
    (l : ℕ) →
      (F : L.Functions l) →
        (ts : Fin l → L.Term (α ⊕ γ)) →
          (f : ↥(FirstOrder.Language.func F ts).varFinsetLeft → β) → motive (FirstOrder.Language.func F ts) f),
  (match FirstOrder.Language.var (Sum.inl a), f with
    | FirstOrder.Language.var (Sum.inl a), f => h_1 a f
    | FirstOrder.Language.var (Sum.inr a), _f => h_2 a _f
    | FirstOrder.Language.func F ts, f => h_3 l F ts f) =
    h_1 a f
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
CategoryTheory.additive_coyonedaObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (X : C),
  (CategoryTheory.preadditiveCoyonedaObj X).Additive
-- Init.Data.SInt.Basic
instAndOpInt16 : AndOp Int16
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.isClopen_fiber : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {f : X → Y},
  IsLocallyConstant f → ∀ (y : Y), IsClopen {x | f x = y}
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.coprod_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) {X Y : C}
  (f : X ⟶ Y),
  (CategoryTheory.FunctorToTypes.coprod F G).map f =
    TypeCat.ofHom
      (Sum.map ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ⇑(CategoryTheory.ConcreteCategory.hom (G.map f)))
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.comapDomain_add : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] (f : M → N) (hf : Function.Injective f)
  (x y : MonoidAlgebra R N),
  MonoidAlgebra.comapDomain f hf (x + y) = MonoidAlgebra.comapDomain f hf x + MonoidAlgebra.comapDomain f hf y
-- Mathlib.Analysis.Calculus.Deriv.AffineMap
AffineMap.deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (f : 𝕜 →ᵃ[𝕜] E) {x : 𝕜}, deriv (⇑f) x = f.linear 1
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the angle between two vectors is `-π / 2`, the second vector is nonzero.  -/
Orientation.right_ne_zero_of_oangle_eq_neg_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(-Real.pi / 2) → y ≠ 0
-- Aesop.RuleTac.Apply
Aesop.RuleTac.applyTerm : Lean.Term → Lean.Meta.TransparencyMode → Aesop.RuleTac
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.flatMapTR.go.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → List β) (a : Array β), List.flatMapTR.go✝ f [] a = a.toList
-- Mathlib.Analysis.InnerProductSpace.GramMatrix
/-- Inequality `‖f x‖ ≤ ‖f‖ * ‖x‖` lifted to Gram matrices.  -/
Matrix.posSemidef_opNorm_smul_gram_sub_gram : ∀ {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {F : Type u_5} [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  (v : n → E) (f : E →L[𝕜] F), (‖f‖ ^ 2 • Matrix.gram 𝕜 v - Matrix.gram 𝕜 (⇑f ∘ v)).PosSemidef
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.ofHom_comp : ∀ {R : Type u} [inst : CommRing R] {X Y Z : Type v} [inst_1 : CommRing X] [inst_2 : Algebra R X] [inst_3 : CommRing Y]
  [inst_4 : Algebra R Y] [inst_5 : CommRing Z] [inst_6 : Algebra R Z] (f : X →ₐ[R] Y) (g : Y →ₐ[R] Z),
  CommAlgCat.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (CommAlgCat.ofHom f) (CommAlgCat.ofHom g)
-- Mathlib.NumberTheory.LSeries.Basic
LSeries_zero : LSeries 0 = 0
-- Mathlib.GroupTheory.Transfer
/-- The transfer transversal as a function. Given a `⟨g⟩`-orbit `q₀, g • q₀, ..., g ^ (m - 1) • q₀`
in `G ⧸ H`, an element `g ^ k • q₀` is mapped to `g ^ k • g₀` for a fixed choice of
representative `g₀` of `q₀`.  -/
Subgroup.transferFunction : {G : Type u_1} → [inst : Group G] → (H : Subgroup G) → G → G ⧸ H → G
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.of_forall_getKey_eq_of_forall_constGet?_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      (∀ (k : α) (hk : Std.DTreeMap.Internal.Impl.contains k t₁ = true)
          (hk' : Std.DTreeMap.Internal.Impl.contains k t₂ = true), t₁.getKey k hk = t₂.getKey k hk') →
        (∀ (k : α), Std.DTreeMap.Internal.Impl.Const.get? t₁ k = Std.DTreeMap.Internal.Impl.Const.get? t₂ k) →
          t₁.Equiv t₂
-- Mathlib.Algebra.Free
FreeAddSemigroup.pure_seq : ∀ {α β : Type u} {f : α → β} {x : FreeAddSemigroup α}, pure f <*> x = f <$> x
-- Mathlib.NumberTheory.Pell
/-- An alternative form of the equation, suitable for rewriting `x^2`.  -/
Pell.Solution₁.prop_x : ∀ {d : ℤ} (a : Pell.Solution₁ d), a.x ^ 2 = 1 + d * a.y ^ 2
-- Init.Data.Array.Extract
Array.lt_of_extract_ne_empty : ∀ {α : Type u_1} {i j : ℕ} {as : Array α}, as.extract i j ≠ #[] → i < min j as.size
-- Mathlib.Tactic.Hint
/-- Run all tactics registered using `register_hint`.
Print a "Try these:" suggestion for each of the successful tactics.

If one tactic succeeds and closes the goal, we don't look at subsequent tactics.
 -/
Mathlib.Tactic.Hint.hint : Lean.Syntax → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Algebra.Order.Antidiag.Nat
Nat.image_piFinTwoEquiv_finMulAntidiag : ∀ {n : ℕ}, Finset.image (⇑(piFinTwoEquiv fun x => ℕ)) (Nat.finMulAntidiag 2 n) = n.divisorsAntidiagonal
-- Mathlib.CategoryTheory.Limits.MorphismProperty
CategoryTheory.CostructuredArrow.closedUnderLimitsOfShape_walkingCospan : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) {A : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A] {L : CategoryTheory.Functor A T}
  [CategoryTheory.Limits.HasPullbacks A] [CategoryTheory.Limits.HasPullbacks T]
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan L] (X : T)
  [P.IsStableUnderComposition] [P.IsStableUnderBaseChange] [P.HasOfPostcompProperty P],
  (CategoryTheory.MorphismProperty.costructuredArrowObj L P).IsClosedUnderLimitsOfShape
    CategoryTheory.Limits.WalkingCospan
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Empty
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.Empty.0.Std.IterM.toArray_eq_match_step.match_1.eq_3 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.size_union_of_not_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (∀ a ∈ t₁, a ∉ t₂) → (t₁ ∪ t₂).size = t₁.size + t₂.size
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instSub : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] → [inst_1 : Ring R] → (v : Valuation R Γ₀) → Sub (WithVal v)
-- Mathlib.Order.RelIso.Basic
RelEmbedding.wellFounded : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (x : r ↪r s), WellFounded s → WellFounded r
-- Lean.Meta.Canonicalizer
Lean.Meta.Canonicalizer.instInhabitedExprVisited.default : Lean.Meta.Canonicalizer.ExprVisited
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.mk.inj : ∀ {𝕜 : Type u_1} {inst : NontriviallyNormedField 𝕜} {E : Type u_2} {inst_1 : NormedAddCommGroup E}
  {inst_2 : NormedSpace 𝕜 E} {H : Type u_3} {inst_3 : TopologicalSpace H} {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  {inst_4 : TopologicalSpace G} {inst_5 : ChartedSpace H G} {inst_6 : Monoid G} {inst_7 : ContMDiffMul I (↑⊤) G}
  {toDerivation :
    Derivation 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤)}
  {left_invariant'' :
    ∀ (g : G), (hfdifferential ⋯) ((Derivation.evalAt 1) toDerivation) = (Derivation.evalAt g) toDerivation}
  {toDerivation_1 :
    Derivation 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤)}
  {left_invariant''_1 :
    ∀ (g : G), (hfdifferential ⋯) ((Derivation.evalAt 1) toDerivation_1) = (Derivation.evalAt g) toDerivation_1},
  { toDerivation := toDerivation, left_invariant'' := left_invariant'' } =
      { toDerivation := toDerivation_1, left_invariant'' := left_invariant''_1 } →
    toDerivation = toDerivation_1
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.comap_iInf : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  {ι : Sort u_9} (f : M →ₛₗ[σ₁₂] M₂) (p : ι → Submodule R₂ M₂),
  Submodule.comap f (⨅ i, p i) = ⨅ i, Submodule.comap f (p i)
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.u_comm_of_l_comm : ∀ {X : Type u_2} [inst : PartialOrder X] {Y : Type u_3} [inst_1 : Preorder Y] {Z : Type u_4} [inst_2 : Preorder Z]
  {W : Type u_5} [inst_3 : Preorder W] {lYX : X → Y} {uXY : Y → X},
  GaloisConnection lYX uXY →
    ∀ {lWZ : Z → W} {uZW : W → Z},
      GaloisConnection lWZ uZW →
        ∀ {lWY : Y → W} {uYW : W → Y},
          GaloisConnection lWY uYW →
            ∀ {lZX : X → Z} {uXZ : Z → X},
              GaloisConnection lZX uXZ → (∀ (x : X), lWZ (lZX x) = lWY (lYX x)) → ∀ {w : W}, uXZ (uZW w) = uXY (uYW w)
-- Mathlib.Data.Fin.Rev
Fin.rev_bijective : ∀ {n : ℕ}, Function.Bijective Fin.rev
-- Mathlib.Analysis.Complex.TaylorSeries
/-- **Alias** of `Complex.hasSum_taylorSeries_on_eball`.

---

A function that is complex differentiable on the open ball of radius `r ≤ ∞` around `c`
is given by evaluating its Taylor series at `c` on this open ball.  -/
Complex.hasSum_taylorSeries_on_emetric_ball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] ⦃f : ℂ → E⦄ ⦃c : ℂ⦄
  ⦃r : ENNReal⦄,
  DifferentiableOn ℂ f (Metric.eball c r) →
    ∀ ⦃z : ℂ⦄, z ∈ Metric.eball c r → HasSum (fun n => (↑n.factorial)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.SelectM.State.mk : Array Lean.Meta.Tactic.TryThis.Suggestion → Array Lean.Meta.Grind.EMatchTheorem → Lean.Meta.Grind.SelectM.State✝
-- Mathlib.Data.DFinsupp.Order
DFinsupp.instOrderedSub : ∀ {ι : Type u_1} (α : ι → Type u_2) [inst : (i : ι) → AddCommMonoid (α i)] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : ∀ (i : ι), CanonicallyOrderedAdd (α i)] [inst_3 : (i : ι) → Sub (α i)]
  [inst_4 : ∀ (i : ι), OrderedSub (α i)], OrderedSub (Π₀ (i : ι), α i)
-- Aesop.Script.Step
Aesop.Script.LazyStep.erasePostStateAssignments : Aesop.Script.LazyStep → Array Lean.MVarId → Aesop.Script.LazyStep
-- Mathlib.Data.Matrix.Basis
Matrix.diag_eq_of_commute_single : ∀ {n : Type u_3} {α : Type u_7} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : Semiring α] {i j : n}
  {M : Matrix n n α}, Commute (Matrix.single i j 1) M → M i i = M j j
-- Mathlib.Order.Filter.Germ.Basic
Filter.const_eventuallyEq : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [l.NeBot] {a b : β}, ((fun x => a) =ᶠ[l] fun x => b) ↔ a = b
-- Mathlib.CategoryTheory.Limits.Preorder
Preorder.instHasBinaryProducts : ∀ {C : Type u} [inst : SemilatticeInf C], CategoryTheory.Limits.HasBinaryProducts C
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg.eq_1 : ∀ (x : ℂ),
  x.arg =
    if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ x.im then Real.arcsin ((-x).im / ‖x‖) + Real.pi else Real.arcsin ((-x).im / ‖x‖) - Real.pi
-- Mathlib.Dynamics.Flow
/-- The orbit of a point under a flow `ϕ` is invariant under `ϕ`.  -/
Flow.isInvariant_orbit : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddMonoid τ]
  (ϕ : Flow τ α) (x : α), IsInvariant ϕ.toFun (ϕ.orbit x)
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.n : Std.Time.GenericFormat.DateBuilder✝ → Option Std.Time.Nanosecond.Ordinal
-- Init.Data.Array.Attach
Array.any_subtype : ∀ {α : Type u_1} {stop : ℕ} {p : α → Prop} {xs : Array { x // p x }} {f : { x // p x } → Bool} {g : α → Bool},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → stop = xs.size → xs.any f 0 stop = xs.unattach.any g
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.norm_setToFun_le_mul_norm : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (f : ↥(MeasureTheory.Lp E 1 μ)),
  0 ≤ C → ‖MeasureTheory.setToFun μ T hT ↑↑f‖ ≤ C * ‖f‖
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropAt_of_mem_groupoid : ∀ {H : Type u_1} [inst : TopologicalSpace H] {G : StructureGroupoid H} {Q : (H → H) → Set H → H → Prop},
  G.LocalInvariantProp G Q →
    (∀ (y : H), Q id Set.univ y) →
      ∀ {f : OpenPartialHomeomorph H H}, f ∈ G → ∀ {x : H}, x ∈ f.source → ChartedSpace.LiftPropAt Q (↑f) x
-- Mathlib.Computability.TuringMachine.StackTuringMachine
/-- The TM2 model removes the tape entirely from the TM1 model,
replacing it with an arbitrary (finite) collection of stacks.
The operation `push` puts an element on one of the stacks,
and `pop` removes an element from a stack (and modifies the
internal state based on the result). `peek` modifies the
internal state but does not remove an element.  -/
Turing.TM2.Stmt : {K : Type u_1} → (K → Type u_2) → Type u_3 → Type u_4 → Type (max (max (max u_1 u_2) u_3) u_4)
-- Mathlib.Data.Nat.Cast.Order.Basic
Nat.mono_cast : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α],
  Monotone Nat.cast
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.ord_eq_iInf : ∀ (α : Type u), (Cardinal.mk α).ord = ⨅ r, Ordinal.type ↑r
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthSup_pow : ∀ {b : ENNReal}, (ExpGrowth.expGrowthSup fun n => b ^ n) = b.log
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The (unique) right homology map data associated to a morphism of short complexes that
are both equipped with right homology data.  -/
CategoryTheory.ShortComplex.rightHomologyMapData : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ : S₁ ⟶ S₂) →
          (h₁ : S₁.RightHomologyData) →
            (h₂ : S₂.RightHomologyData) → CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂
-- Mathlib.Topology.Algebra.MulAction
/-- Class `ContinuousSMul M X` says that the scalar multiplication `(•) : M → X → X`
is continuous in both arguments. We use the same class for all kinds of multiplicative actions,
including (semi)modules and algebras.  -/
ContinuousSMul : (M : Type u_1) → (X : Type u_2) → [SMul M X] → [TopologicalSpace M] → [TopologicalSpace X] → Prop
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.hsum_ofFinsupp : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  {f : α →₀ HahnSeries Γ R}, (HahnSeries.SummableFamily.ofFinsupp f).hsum = f.sum fun x => id
-- Mathlib.Topology.Homeomorph.Lemmas
Topology.IsCoinducing.connectedComponentsHomeomorph.congr_simp : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f f_1 : X → Y}
  (e_f : f = f_1) (hf : Topology.IsCoinducing f) (hf' : ∀ (y : Y), IsConnected (f ⁻¹' {y})),
  hf.connectedComponentsHomeomorph hf' = ⋯.connectedComponentsHomeomorph ⋯
-- Mathlib.Topology.Compactness.Compact
Filter.Tendsto.isCompact_insert_range_of_cofinite : ∀ {X : Type u} {ι : Type u_1} [inst : TopologicalSpace X] {f : ι → X} {x : X},
  Filter.Tendsto f Filter.cofinite (nhds x) → IsCompact (insert x (Set.range f))
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.Key.lam.sizeOf_spec : sizeOf Lean.Meta.RefinedDiscrTree.Key.lam = 1
-- Init.Grind.Config
/-- When `true` (default: `true`), uses procedure for handling associative (and commutative) operators.
 -/
Lean.Grind.Config.ac : Lean.Grind.Config → Bool
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_inter_le_size_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  (t₁ ∩ t₂).size ≤ t₂.size
-- Init.Data.Dyadic.Basic
Dyadic.zero_ne_of : ∀ {n k : ℤ} {hn : n % 2 = 1}, 0 ≠ Dyadic.ofOdd n k hn
-- Mathlib.NumberTheory.MulChar.Basic
/-- When the domain has a zero, then the inverse of a multiplicative character `χ`,
applied to `a`, is `χ` applied to the inverse of `a`.  -/
MulChar.inv_apply : ∀ {R' : Type u_2} [inst : CommMonoidWithZero R'] {R : Type u_3} [inst_1 : CommMonoidWithZero R] (χ : MulChar R R')
  (a : R), χ⁻¹ a = χ (Ring.inverse a)
-- Mathlib.RingTheory.Etale.Descent
Algebra.Smooth.of_smooth_tensorProduct_of_faithfullyFlat : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Type u_3)
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [Module.FaithfullyFlat R T] [Algebra.Smooth T (TensorProduct R T S)],
  Algebra.Smooth R S
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.mkAuxName : Lean.Name → Lean.Elab.TermElabM Lean.Name
-- Mathlib.Algebra.Notation.Support
Pi.subsingleton_support_single : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Zero M] {i : ι} {a : M},
  (Function.support (Pi.single i a)).Subsingleton
-- Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
_private.Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities.0.MvPolynomial.NewtonIdentities.disjUnion_filter_pairs_eq_pairs : ∀ (σ : Type u_1) [inst : DecidableEq σ] [inst_1 : Fintype σ] (k : ℕ),
  {t ∈ MvPolynomial.NewtonIdentities.pairs✝ σ k | t.1.card < k}.disjUnion
      ({t ∈ MvPolynomial.NewtonIdentities.pairs✝ σ k | t.1.card = k}) ⋯ =
    MvPolynomial.NewtonIdentities.pairs✝ σ k
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.coe_add : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (f g : NormedAddGroupHom V₁ V₂), ⇑(f + g) = ⇑f + ⇑g
-- Init.Data.SInt.Lemmas
ISize.zero_mul : ∀ {a : ISize}, 0 * a = 0
-- Mathlib.Topology.Convenient.GeneratedBy
Topology.IsGeneratedBy.iff_le_generatedBy : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} {tY : TopologicalSpace Y},
  Topology.IsGeneratedBy X Y ↔ tY ≤ TopologicalSpace.generatedBy X
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
/-- The norm on a `NormedField`, as an `AbsoluteValue`.  -/
NormedField.toAbsoluteValue : (R : Type u_2) → [inst : NormedField R] → AbsoluteValue R ℝ
-- Mathlib.Order.Filter.Finite
Filter.mem_iInf' : ∀ {α : Type u} {ι : Type u_2} {s : ι → Filter α} {U : Set α},
  U ∈ ⨅ i, s i ↔
    ∃ I, I.Finite ∧ ∃ V, (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = Set.univ) ∧ U = ⋂ i ∈ I, V i ∧ U = ⋂ i, V i
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.mem_range_of_measure_ne_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {f : MeasureTheory.SimpleFunc α β} {x : β}
  {μ : MeasureTheory.Measure α}, μ (⇑f ⁻¹' {x}) ≠ 0 → x ∈ f.range