mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Category.TopCat.Yoneda
CategoryTheory.Limits.piComparison.eq_1 : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : β → C)
  [inst_2 : CategoryTheory.Limits.HasProduct f] [inst_3 : CategoryTheory.Limits.HasProduct fun b => G.obj (f b)],
  CategoryTheory.Limits.piComparison G f = CategoryTheory.Limits.Pi.lift fun b => G.map (CategoryTheory.Limits.Pi.π f b)
-- Lean.Parser.Extra
Lean.ppDedentIfGrouped.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Sites.Closed
/-- The presheaf sending each object to the type of sieves on it. This will turn out to be a
subobject classifier for the category of presheaves.  -/
CategoryTheory.Functor.sieves : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor Cᵒᵖ (Type (max v u))
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- This lemma is superseded by `unifIntegrable_of` which do not require `C` to be positive.  -/
MeasureTheory.unifIntegrable_of' : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {p : ENNReal},
  1 ≤ p →
    p ≠ ⊤ →
      ∀ {f : ι → α → β},
        (∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)) →
          (∀ (ε : ℝ),
              0 < ε →
                ∃ C,
                  0 < C ∧
                    ∀ (i : ι), MeasureTheory.eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε) →
            MeasureTheory.UnifIntegrable f p μ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_insertManyIfNewUnit!_list : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {l : List α} {k : α},
      Std.DTreeMap.Internal.Impl.Const.get? (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l)) k =
        if k ∈ t ∨ l.contains k = true then some () else none
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.filter_equiv_self_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {f : α → Bool},
  t.WF → ((Std.TreeSet.Raw.filter f t).Equiv t ↔ ∀ (a : α) (h : a ∈ t), f (t.get a h) = true)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
/-- Find values that match `e` in `d`.
* If `unify == true` then metavariables in `e` can be assigned.
* If `matchRootStar == true` then we allow metavariables at the root to unify.
  Set this to `false` to avoid getting excessively many results.
 -/
Lean.Meta.RefinedDiscrTree.getMatch : {α : Type} →
  Lean.Meta.RefinedDiscrTree α →
    Lean.Expr → Bool → Bool → Lean.MetaM (Lean.Meta.RefinedDiscrTree.MatchResult α × Lean.Meta.RefinedDiscrTree α)
-- Mathlib.Data.Finset.Fold
Finset.fold_image_idem : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op]
  {f : α → β} {b : β} [inst : DecidableEq α] {g : γ → α} {s : Finset γ} [hi : Std.IdempotentOp op],
  Finset.fold op b f (Finset.image g s) = Finset.fold op b (f ∘ g) s
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.root_reflectionPerm : ∀ {ι : 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.root ((P.reflectionPerm i) j) = (P.reflection i) (P.root j)
-- Mathlib.SetTheory.Cardinal.Ordinal
Ordinal.IsInitial.isPrincipal_add : ∀ {o : Ordinal.{u_1}}, o.IsInitial → Ordinal.omega0 ≤ o → Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) o
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDerivWithin_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜} (f : 𝕜 → F),
  iteratedDerivWithin n (-f) s x = -iteratedDerivWithin n f s x
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.mkMonoidHom_apply : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : MulOneClass M] [inst_2 : ContinuousMul M] (a : M),
  SeparationQuotient.mkMonoidHom a = SeparationQuotient.mk a
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.isEquivalence : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} (A : Type u') [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A], (F.sheafPushforwardContinuous A J₀ J).IsEquivalence
-- Mathlib.RingTheory.IdealFilter.Basic
IdealFilter.IsTorsionQuot.anti_right : ∀ {A : Type u_1} [inst : Ring A] {F : IdealFilter A} {I J K : Ideal A},
  J ≤ K → F.IsTorsionQuot I K → F.IsTorsionQuot I J
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.instIsEquivalenceActionTopModuleCatFromActionTopModFunc : ∀ {k : Type u} {G : Type v} [inst : TopologicalSpace k] [inst_1 : Ring k] [inst_2 : Monoid G],
  TopRep.fromActionTopModFunc.IsEquivalence
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.mapAlgHom.eq_1 : ∀ {R : Type u_1} {A : Type u_4} {B : Type u_5} (M : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : AddMonoid M] (f : A →ₐ[R] B),
  AddMonoidAlgebra.mapAlgHom M f = { toRingHom := AddMonoidAlgebra.mapRingHom M ↑f, commutes' := ⋯ }
-- Std.Internal.Do.WP.Frame
/-- `x` frames the resource `F` with respect to the operator `op : R → Pred → Pred`: `op F ·` commutes
into the postcondition of `wp x` for every postcondition.

For the meet `op = (· ⊓ ·)` with `R = Pred` and stateful `Pred`, this means running `x` preserves the
state identified by `F`. Other operators take a simpler resource, e.g. a cost counter `R = Nat`.
 -/
Std.Internal.Do.WP.Frames : {Prog : Type u} →
  {Value : Type v} →
    {Pred : Type w} →
      {EPred : Type z} →
        [inst : Std.Internal.Do.Assertion Pred] →
          [inst_1 : Std.Internal.Do.Assertion EPred] →
            [Std.Internal.Do.WP Prog Value Pred EPred] → {R : Type t} → (R → Pred → Pred) → Prog → R → Prop
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_le_lpNorm_add_lpNorm_sub' : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f g : α → E},
  MeasureTheory.MemLp g p μ →
    1 ≤ p → MeasureTheory.lpNorm f p μ ≤ MeasureTheory.lpNorm g p μ + MeasureTheory.lpNorm (f - g) p μ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_filter_eq_false_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → Bool} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl.isEmpty = false ↔
    ∃ k, ∃ (h : Std.DTreeMap.Internal.Impl.contains k t = true), f k (t.get k h) = true
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- The set of self-adjoint endomorphisms of a module with bilinear map is a submodule. (In fact
it is a Jordan subalgebra.)  -/
LinearMap.selfAdjointSubmodule : {R : Type u_1} →
  {M : Type u_5} →
    {M₂ : Type u_7} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommGroup M₂] → [inst_4 : Module R M₂] → (M →ₗ[R] M →ₗ[R] M₂) → Submodule R (Module.End R M)
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
/-- An `R`-linear homomorphism of graded algebras, denoted `𝒜 →ₐᵍ[R] ℬ`.  -/
«term_→ₐᵍ[_]_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_def : ∀ (x y : ℝ), x ^ y = (↑x ^ ↑y).re
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀_map_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] {X Y : ChainComplex C ℕ} (f : X ⟶ Y) (Δ : SimplexCategoryᵒᵖ),
  (AlgebraicTopology.DoldKan.Γ₀.map f).app Δ =
    (AlgebraicTopology.DoldKan.Γ₀.splitting X).desc Δ fun A =>
      CategoryTheory.CategoryStruct.comp (f.f (Opposite.unop A.fst).len)
        (((AlgebraicTopology.DoldKan.Γ₀.splitting Y).cofan Δ).inj A)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.eqToHom_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {X Y : CategoryTheory.CostructuredArrow S T} (h : X = Y),
  (CategoryTheory.eqToHom h).left = CategoryTheory.eqToHom ⋯
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.map_bot : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : NonUnitalSemiring A] [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : NonUnitalSemiring B]
  [inst_6 : StarRing B] [inst_7 : Module R B] [inst_8 : FunLike F A B] [inst_9 : NonUnitalAlgHomClass F R A B]
  [inst_10 : StarHomClass F A B] [inst_11 : IsScalarTower R A A] [inst_12 : SMulCommClass R A A]
  [inst_13 : StarModule R A] [inst_14 : IsScalarTower R B B] [inst_15 : SMulCommClass R B B] [inst_16 : StarModule R B]
  (f : F), NonUnitalStarSubalgebra.map f ⊥ = ⊥
-- Init.Data.List.Basic
/-- The arguments of `splitBy.loop l b g gs` represent the following:

- `l : List α` are the elements which we still need to split.
- `b : α` is the previous element for which a comparison was performed.
- `r : List α` is the group currently being assembled, in **reverse order**.
- `acc : List (List α)` is all of the groups that have been completed, in **reverse order**.
 -/
List.splitBy.loop : {α : Type u} → (α → α → Bool) → List α → α → List α → List (List α) → List (List α)
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.instReprArgSpec.repr.match_1.eq_2 : ∀ (motive : Lean.Doc.ArgSpec✝ → Sort u_1) (a : Lean.Name) (a_1 a_2 : Lean.Expr)
  (h_1 : (a : Lean.Name) → (a_3 : Lean.Expr) → motive (Lean.Doc.ArgSpec.positional✝ a a_3))
  (h_2 : (a : Lean.Name) → (a_3 a_4 : Lean.Expr) → motive (Lean.Doc.ArgSpec.named✝ a a_3 a_4))
  (h_3 : (a : Lean.Name) → (a_3 : Lean.Expr) → motive (Lean.Doc.ArgSpec.many✝ a a_3))
  (h_4 : (a : Lean.Name) → (a_3 : Bool) → motive (Lean.Doc.ArgSpec.flag✝ a a_3)),
  (match Lean.Doc.ArgSpec.named✝ a a_1 a_2 with
    | Lean.Doc.ArgSpec.positional✝ a a_3 => h_1 a a_3
    | Lean.Doc.ArgSpec.named✝ a a_3 a_4 => h_2 a a_3 a_4
    | Lean.Doc.ArgSpec.many✝ a a_3 => h_3 a a_3
    | Lean.Doc.ArgSpec.flag✝ a a_3 => h_4 a a_3) =
    h_2 a a_1 a_2
-- Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
AlgebraicGeometry.FormallyUnramified.instIsSeparableCarrierResidueFieldCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfLocallyOfFiniteType : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.FormallyUnramified f]
  [AlgebraicGeometry.LocallyOfFiniteType f] (x : ↥X), Algebra.IsSeparable ↑(Y.residueField (f x)) ↑(X.residueField x)
-- Init.Data.List.Lemmas
List.append_eq_replicate_iff : ∀ {α : Type u_1} {n : ℕ} {l₁ l₂ : List α} {a : α},
  l₁ ++ l₂ = List.replicate n a ↔
    l₁.length + l₂.length = n ∧ l₁ = List.replicate l₁.length a ∧ l₂ = List.replicate l₂.length a
-- Mathlib.Data.NNReal.Defs
/-- If `Γ₀ˣ` is nontrivial and `f : Γ₀ →*₀ ℝ≥0` is strictly monotone, then for any positive
real `r`, there exists `d : Γ₀ˣ` with `f d < r`.  -/
Real.exists_lt_of_strictMono : ∀ {Γ₀ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ₀] [h : Nontrivial Γ₀ˣ] {f : Γ₀ →*₀ NNReal},
  StrictMono ⇑f → ∀ {r : ℝ}, 0 < r → ∃ d, ↑(f ↑d) < r
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.TakeWhile.0.Std.Iter.step_takeWhile.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : true = true → motive true) (h_2 : true = false → motive false),
  (match hP : true with
    | true => h_1 hP
    | false => h_2 hP) =
    h_1 ⋯
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.equiv_block_det : ∀ {m : Type u_3} {R : Type v} [inst : CommRing R] [inst_1 : DecidableEq m] [inst_2 : Fintype m] (M : Matrix m m R)
  {p q : m → Prop} [inst_3 : DecidablePred p] [inst_4 : DecidablePred q],
  (∀ (x : m), q x ↔ p x) → (M.toSquareBlockProp p).det = (M.toSquareBlockProp q).det
-- Mathlib.Topology.MetricSpace.HolderNorm
/-- The `r`-Hölder (semi-)norm in `ℝ≥0∞` of a function `f` is the least non-negative real
number `C` for which `f` is `r`-Hölder continuous with constant `C`. This is `∞` if no such
non-negative real exists.  -/
eHolderNorm : {X : Type u_1} → {Y : Type u_2} → [PseudoEMetricSpace X] → [PseudoEMetricSpace Y] → NNReal → (X → Y) → ENNReal
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- A `FiniteGrp` when given the discrete topology can be considered as a profinite group.  -/
ProfiniteGrp.ofFiniteGrp : FiniteGrp.{u_1} → ProfiniteGrp.{u_1}
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
IsBaseChange.linearMapRightBaseChangeEquiv.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_4} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {P : Type u_5} [inst_7 : AddCommMonoid P] [inst_8 : Module R P] [inst_9 : Module S P] [inst_10 : IsScalarTower R S P]
  [inst_11 : Module.Free R M] [inst_12 : Module.Finite R M] {ε : N →ₗ[R] P} (ibc : IsBaseChange S ε),
  IsBaseChange.linearMapRightBaseChangeEquiv M ibc =
    LinearEquiv.ofBijective (IsBaseChange.linearMapRightBaseChangeHom S M ε) ⋯
-- Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  {N : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} N] (p : CategoryTheory.Functor N C)
  [inst_3 : CategoryTheory.InitiallySmall N] {J : CategoryTheory.GrothendieckTopology C}
  [inst_4 : CategoryTheory.IsCofiltered N]
  (hp :
    ∀ ⦃X : C⦄,
      ∀ R ∈ J X,
        ∀ ⦃U : N⦄ (f : p.obj U ⟶ X),
          ∃ Y g,
            ∃ (_ : R.arrows g),
              ∃ V q a, CategoryTheory.CategoryStruct.comp a g = CategoryTheory.CategoryStruct.comp (p.map q) f)
  {A : Type u''} [inst_5 : CategoryTheory.Category.{v'', u''} A]
  [inst_6 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] {P Q : CategoryTheory.Functor Cᵒᵖ A} (g : P ⟶ Q)
  (U : N),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered p hp U P)
      ((CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered p hp).presheafFiber.map g) =
    CategoryTheory.CategoryStruct.comp (g.app (Opposite.op (p.obj U)))
      (CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered p hp U Q)
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iInter_div_subset : ∀ {α : Type u_2} {ι : Sort u_5} [inst : Div α] (s : ι → Set α) (t : Set α), (⋂ i, s i) / t ⊆ ⋂ i, s i / t
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.setInterior_reindex : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (I : Set k) {m n : ℕ} (s : Affine.Simplex k P n) (e : Fin (n + 1) ≃ Fin (m + 1)),
  Affine.Simplex.setInterior I (s.reindex e) = Affine.Simplex.setInterior I s
-- Mathlib.Algebra.Order.Ring.Defs
IsOrderedRing.toMulPosMono : ∀ {R : Type u_1} {inst : Semiring R} {inst_1 : PartialOrder R} [self : IsOrderedRing R], MulPosMono R
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.coeff_restriction : ∀ {R : Type u} [inst : Ring R] {p : Polynomial R} {n : ℕ}, ↑(p.restriction.coeff n) = p.coeff n
-- Init.Data.Nat.Lemmas
Nat.eq_div_of_mul_eq_left : ∀ {c a b : ℕ}, c ≠ 0 → a * c = b → a = b / c
-- Mathlib.Algebra.Lie.Graded
/-- The Lie derivation on a graded Lie algebra that scalar-multiplies by an additive function of
the degree.  -/
LieDerivation.ofGrading : {ι : Type u_1} →
  {R : Type u_3} →
    {L : Type u_4} →
      [inst : DecidableEq ι] →
        [inst_1 : AddCommMonoid ι] →
          [inst_2 : CommRing R] →
            [inst_3 : LieRing L] →
              [inst_4 : LieAlgebra R L] →
                (ℒ : ι → Submodule R L) → [GradedLieAlgebra ℒ] → (ι →+ R) → LieDerivation R L L
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.isSemisimple_ad_of_mem_isCartanSubalgebra : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L] [FiniteDimensional K L]
  {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L]
  [PerfectField K] {x : L}, x ∈ H → ((LieAlgebra.ad K L) x).IsSemisimple
-- Mathlib.Analysis.Analytic.Linear
LinearIsometryEquiv.analyticWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E ≃ₗᵢ[𝕜] F)
  (s : Set E) (x : E), AnalyticWithinAt 𝕜 (⇑f) s x
-- Mathlib.Topology.Connected.TotallyDisconnected
exists_isClopen_of_totally_separated : ∀ {α : Type u_3} [inst : TopologicalSpace α] [TotallySeparatedSpace α],
  Pairwise fun x1 x2 => ∃ U, IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ
-- Mathlib.NumberTheory.Padics.AddChar
PadicInt.addChar_of_value_at_one_def : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : NormedRing R] [inst_2 : Algebra ℤ_[p] R]
  [inst_3 : IsBoundedSMul ℤ_[p] R] [inst_4 : IsUltrametricDist R] [inst_5 : CompleteSpace R] {r : R}
  (hr : Filter.Tendsto (fun x => r ^ x) Filter.atTop (nhds 0)), (PadicInt.addChar_of_value_at_one r hr) 1 = 1 + r
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.hasFPowerSeriesOnBall_derivWeierstrassPExcept : ∀ (L : PeriodPair) (l₀ x : ℂ) (r : NNReal),
  0 < r →
    Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ →
      HasFPowerSeriesOnBall (L.derivWeierstrassPExcept l₀) (L.derivWeierstrassPExceptSeries l₀ x) x ↑r
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
/-- A zero object is in particular terminal.  -/
CategoryTheory.Limits.IsZero.isTerminal : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} → CategoryTheory.Limits.IsZero X → CategoryTheory.Limits.IsTerminal X
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithLower.ofLower_le_ofLower : ∀ {α : Type u_1} [inst : Preorder α] {x y : Topology.WithLower α},
  Topology.WithLower.ofLower x ≤ Topology.WithLower.ofLower y ↔ x ≤ y
-- Lean.Parser.Command
Lean.Parser.Command.protected.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Topology.Algebra.Support
HasCompactMulSupport.comp_isClosedEmbedding : ∀ {α : Type u_2} {α' : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace α']
  [inst_2 : One β] {f : α → β},
  HasCompactMulSupport f → ∀ {g : α' → α}, Topology.IsClosedEmbedding g → HasCompactMulSupport (f ∘ g)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.forIn'_eq_match_step.match_1.eq_2 : ∀ {γ : Type u_1} (motive : ForInStep γ → Sort u_2) (c : γ) (h_1 : (c : γ) → motive (ForInStep.yield c))
  (h_2 : (c : γ) → motive (ForInStep.done c)),
  (match ForInStep.done c with
    | ForInStep.yield c => h_1 c
    | ForInStep.done c => h_2 c) =
    h_2 c
-- Mathlib.Algebra.Order.Hom.Monoid
/-- `0` is the homomorphism sending all elements to `0`.  -/
OrderAddMonoidHom.instZero : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] → [inst_1 : Preorder β] → [inst_2 : AddZeroClass α] → [inst_3 : AddZeroClass β] → Zero (α →+o β)
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.section_app_comp_hom_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject.Augmented C}
  (ed : X.ExtraDegeneracy) (n : SimplexCategoryᵒᵖ) {Z : C} (h : X.right ⟶ Z),
  CategoryTheory.CategoryStruct.comp (ed.section_.app n) (CategoryTheory.CategoryStruct.comp (X.hom.app n) h) = h
-- Mathlib.Data.Set.Pairwise.Basic
Set.pairwiseDisjoint_range_iff : ∀ {α : Type u_6} {β : Type u_7} {f : α → Set β},
  (Set.range f).PairwiseDisjoint id ↔ ∀ (x y : α), f x ≠ f y → Disjoint (f x) (f y)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- An auxiliary structure that witnesses the fact that `f` factors through an image object of `G`.
 -/
CategoryTheory.Presieve.CoverByImageStructure : {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] →
        CategoryTheory.Functor C D → {V U : D} → (V ⟶ U) → Type (max u_1 v_2)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift
_private.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift.0.AffineSubspace.shift.eq_1 : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : AddTorsor V P]
  [inst_3 : Module k V] (s : AffineSubspace k P) (c : P) (r : k),
  s.shift c r =
    if h : Nonempty ↥s then AffineSubspace.map (↑(AffineEquiv.constVAdd k P ((1 - r) • (c -ᵥ ↑h.some)))) s else ⊥
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.getResult : Lean.Meta.SynthInstance.SynthM (Option Lean.Meta.AbstractMVarsResult)
-- Mathlib.Data.Nat.Factorization.Basic
/-- If `p` is a prime factor of `a` then the power of `p` in `a` is the same that in `a * b`,
for any `b` coprime to `a`.  -/
Nat.factorization_eq_of_coprime_left : ∀ {p a b : ℕ}, a.Coprime b → p ∈ a.primeFactorsList → (a * b).factorization p = a.factorization p
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
_private.Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks.0.CategoryTheory.Limits.WidePullbackShape.mkCone.match_1.eq_1 : ∀ {J : Type u_1} (motive : CategoryTheory.Limits.WidePullbackShape J → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (j : J) → motive (some j)),
  (match none with
    | none => h_1 ()
    | some j => h_2 j) =
    h_1 ()
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.Types.binaryCoproductIso_inl_comp_hom : ∀ (X Y : Type u),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl
      (CategoryTheory.Limits.Types.binaryCoproductIso X Y).hom =
    TypeCat.ofHom Sum.inl
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
tangentMap_prodFst : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
  {p : TangentBundle (I.prod I') (M × M')}, tangentMap (I.prod I') I Prod.fst p = ⟨p.proj.1, p.snd.1⟩
-- Mathlib.Algebra.Order.Floor.Div
Finsupp.support_floorDiv_subset : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α]
  [inst_2 : AddCommMonoid β] [inst_3 : PartialOrder β] [inst_4 : SMulZeroClass α β] [inst_5 : FloorDiv α β] {f : ι →₀ β}
  {a : α}, (f ⌊/⌋ a).support ⊆ f.support
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.two_mul_arctan_inv_2_sub_arctan_inv_7 : 2 * Real.arctan 2⁻¹ - Real.arctan 7⁻¹ = Real.pi / 4
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsSubgraph.isLink_iff : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G H : Graph α β},
  H ≤ G → e ∈ H.edgeSet → (H.IsLink e x y ↔ G.IsLink e x y)
-- Mathlib.Topology.EMetricSpace.Weak
Option.ball_infty_of_pos : ∀ {α : Type u} [t : TopologicalSpace α] [m : WeakPseudoEMetricSpace α] {r : ENNReal},
  0 < r → Metric.eball none r = {none}
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.conjTranspose_zero : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} [inst : AddMonoid A] [inst_1 : StarAddMonoid A],
  CStarMatrix.conjTranspose 0 = 0