mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.SpreadingOut
/-- Given `S`-schemes `X Y`, a point `x : X`, and an `S`-morphism `φ : Spec 𝒪_{X, x} ⟶ Y`,
we may spread it out to an `S`-morphism `f : U ⟶ Y`
provided that `Y` is locally of finite type over `S` and
`X` is "germ-injective" at `x` (e.g. when it's integral or locally Noetherian).

TODO: The condition on `X` is unnecessary when `Y` is locally of finite presentation.
 -/
AlgebraicGeometry.spread_out_of_isGermInjective' : ∀ {X Y S : AlgebraicGeometry.Scheme} (sX : X ⟶ S) (sY : Y ⟶ S) [AlgebraicGeometry.LocallyOfFiniteType sY] {x : ↥X}
  [X.IsGermInjectiveAt x] (φ : AlgebraicGeometry.Spec (X.presheaf.stalk x) ⟶ Y),
  CategoryTheory.CategoryStruct.comp φ sY = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) sX →
    ∃ U,
      ∃ (hxU : x ∈ U),
        ∃ f,
          φ = CategoryTheory.CategoryStruct.comp (U.fromSpecStalkOfMem x hxU) f ∧
            CategoryTheory.CategoryStruct.comp f sY = CategoryTheory.CategoryStruct.comp U.ι sX
-- Mathlib.Data.Sign.Defs
SignType.instLE : LE SignType
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Pseudofunctor.rightZigzag_map : ∀ {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),
  CategoryTheory.Bicategory.rightZigzag
      (CategoryTheory.CategoryStruct.comp (F.mapId a).inv
        (CategoryTheory.CategoryStruct.comp (F.map₂ adj.unit) (F.mapComp f g).hom))
      (CategoryTheory.CategoryStruct.comp (F.mapComp g f).inv
        (CategoryTheory.CategoryStruct.comp (F.map₂ adj.counit) (F.mapId b).hom)) =
    CategoryTheory.bicategoricalComp (CategoryTheory.Bicategory.whiskerLeft (F.map g) (F.mapId a).inv)
      (CategoryTheory.CategoryStruct.comp (F.mapComp g (CategoryTheory.CategoryStruct.id a)).inv
        (CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.rightZigzag adj.unit adj.counit))
          (CategoryTheory.bicategoricalComp (F.mapComp (CategoryTheory.CategoryStruct.id b) g).hom
            (CategoryTheory.Bicategory.whiskerRight (F.mapId b).hom (F.map g)))))
-- Mathlib.Topology.Algebra.FilterBasis
/-- The topological space structure coming from an additive group filter basis.  -/
AddGroupFilterBasis.topology : {G : Type u} → [inst : AddGroup G] → AddGroupFilterBasis G → TopologicalSpace G
-- Mathlib.Topology.UniformSpace.Closeds
UniformContinuous.compacts_map : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β}
  (hf : UniformContinuous f), UniformContinuous (TopologicalSpace.Compacts.map f ⋯)
-- Init.Data.Array.Attach
Array.pmap_pmap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {p : α → Prop} {q : β → Prop} {g : (a : α) → p a → β}
  {f : (b : β) → q b → γ} {xs : Array α} (H₁ : ∀ a ∈ xs, p a) (H₂ : ∀ a ∈ Array.pmap g xs H₁, q a),
  Array.pmap f (Array.pmap g xs H₁) H₂ = Array.pmap (fun a h => f (g (↑a) h) ⋯) xs.attach ⋯
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
/-- Predicate stating that the first non-zero exponent is positive.  -/
Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos : Tactic.ComputeAsymptotics.UnitMonomial → Prop
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.num_C : ∀ {K : Type u} [inst : Field K] (c : K), (RatFunc.C c).num = Polynomial.C c
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instNSMul.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddMonoid β]
  [inst_3 : ContinuousAdd β],
  ContinuousMap.instNSMul = { smul := fun n f => { toFun := n • ⇑f, continuous_toFun := ⋯ } }
-- Mathlib.Order.Interval.Set.ProjIcc
/-- **Alias** of `Set.OrdConnected.domRestrict`. -/
Set.OrdConnected.restrict : ∀ {α : Type u_1} [inst : LinearOrder α] {s t : Set α},
  s.OrdConnected → {x | t.domRestrict (fun x => x ∈ s) x}.OrdConnected
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- Lift a cf to a scf using the inclusion map.  -/
ContFract.instCoeSimpContFract : {α : Type u_1} → [inst : One α] → [inst_1 : Zero α] → [inst_2 : LT α] → Coe (ContFract α) (SimpContFract α)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.preimage_mul : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst_1 : Mul β] [inst_2 : FunLike F α β]
  [MulHomClass F α β] (m : F),
  Function.Injective ⇑m → ∀ {s t : Set β}, s ⊆ Set.range ⇑m → t ⊆ Set.range ⇑m → ⇑m ⁻¹' (s * t) = ⇑m ⁻¹' s * ⇑m ⁻¹' t
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValInt.mul : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {a b : ℤ}, a ≠ 0 → b ≠ 0 → padicValInt p (a * b) = padicValInt p a + padicValInt p b
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.NonnegCoeffs.below.add : ∀ {motive : (a : Lean.Grind.CommRing.Poly) → a.NonnegCoeffs → Prop} (a : ℤ) (m : Lean.Grind.CommRing.Mon)
  (p : Lean.Grind.CommRing.Poly) (a_1 : a ≥ 0) (a_2 : p.NonnegCoeffs),
  Lean.Grind.CommRing.Poly.NonnegCoeffs.below a_2 → motive p a_2 → Lean.Grind.CommRing.Poly.NonnegCoeffs.below ⋯
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
/-- Tricoloring of a cycle graph  -/
SimpleGraph.cycleGraph.tricoloring : (n : ℕ) → 2 ≤ n → (SimpleGraph.cycleGraph n).Coloring (Fin 3)
-- Mathlib.RingTheory.OreLocalization.Ring
OreLocalization.zsmul_eq_zsmul : ∀ {R : Type u_1} [inst : Ring R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : AddCommGroup X] [inst_3 : Module R X] (n : ℤ) (x : OreLocalization S X), n • x = n • x
-- Mathlib.Analysis.RCLike.Inner
RCLike.wInner_zero_right : ∀ {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [inst : Fintype ι] [inst_1 : RCLike 𝕜]
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → InnerProductSpace 𝕜 (E i)] (w : ι → ℝ)
  (f : (i : ι) → E i), ⟪f, 0⟫_[𝕜, w] = 0
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
IsLocalFrameOn.mk : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {ι : Type u_7} {n : WithTop ℕ∞}
  {s : ι → (x : M) → V x} {u : Set M},
  (∀ {x : M}, x ∈ u → LinearIndependent 𝕜 fun x_1 => s x_1 x) →
    (∀ {x : M}, x ∈ u → ⊤ ≤ Submodule.span 𝕜 (Set.range fun x_1 => s x_1 x)) →
      (∀ (i : ι), ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, s i x⟩) u) →
        IsLocalFrameOn I F n s u
-- Mathlib.Algebra.Homology.TotalComplexShift
/-- The isomorphism `(((shiftFunctor₁ C x).obj K).X a).X b ≅ (K.X a').X b` when `a' = a + x`.  -/
HomologicalComplex₂.shiftFunctor₁XXIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) →
        (a x a' : ℤ) → a' = a + x → (b : ℤ) → (((HomologicalComplex₂.shiftFunctor₁ C x).obj K).X a).X b ≅ (K.X a').X b
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.instPartialOrder : {α : Type u_2} → {β : Type u_3} → [inst : SupSet α] → {x : CompleteLattice β} → PartialOrder (sSupHom α β)
-- Mathlib.Topology.Algebra.InfiniteSum.Order
tsum_le_of_sum_le' : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : AddCommMonoid α] [inst_1 : Preorder α]
  [inst_2 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a₂ : α},
  0 ≤ a₂ → (∀ (s : Finset ι), ∑ i ∈ s, f i ≤ a₂) → ∑'[L] (i : ι), f i ≤ a₂
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
/-- If the product comparison maps of `G` at every pair `(X,Y)` is an
isomorphism, then `G` preserves binary products.  -/
CategoryTheory.Limits.preservesBinaryProducts_of_isIso_prodComparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) [inst_2 : CategoryTheory.Limits.HasBinaryProducts C]
  [inst_3 : CategoryTheory.Limits.HasBinaryProducts D]
  [i : ∀ {X Y : C}, CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison G X Y)],
  CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) G
-- Mathlib.Algebra.WithConv
WithConv.ofConv_multisetSum : ∀ {A : Type u_2} [inst : AddCommMonoid A] (s : Multiset (WithConv A)),
  s.sum.ofConv = (Multiset.map WithConv.ofConv s).sum
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.neg_apply : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] (f : P →ᴬ[R] W) (x : P),
  (-f) x = -f x
-- Mathlib.CategoryTheory.Products.Bifunctor
CategoryTheory.Bifunctor.map_id : ∀ {C : Type u₁} {D : Type u₂} {E : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  (F : CategoryTheory.Functor (C × D) E) (X : C) (Y : D),
  F.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y)) =
    CategoryTheory.CategoryStruct.id (F.obj (X, Y))
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Split.State.mk.sizeOf_spec : ∀ (num : ℕ) (candidates : List Lean.Meta.Grind.SplitInfo) (added : Std.HashSet Lean.Meta.Grind.SplitInfo)
  (resolved : Lean.PHashSet Lean.Meta.Sym.ExprPtr) (trace : List Lean.Meta.Grind.CaseTrace)
  (lookaheads : List Lean.Meta.Grind.SplitInfo) (argPosMap : Std.HashMap (Lean.Expr × Lean.Expr) (List ℕ))
  (argsAt : Lean.PHashMap (Lean.Expr × ℕ) (List Lean.Meta.Grind.SplitArg)),
  sizeOf
      { num := num, candidates := candidates, added := added, resolved := resolved, trace := trace,
        lookaheads := lookaheads, argPosMap := argPosMap, argsAt := argsAt } =
    1 + sizeOf num + sizeOf candidates + sizeOf added + sizeOf resolved + sizeOf trace + sizeOf lookaheads +
        sizeOf argPosMap +
      sizeOf argsAt
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
/-- The property of objects of `Cᵒᵖ` corresponding to `P : ObjectProperty C`.  -/
CategoryTheory.ObjectProperty.op : {C : Type u} →
  [inst : CategoryTheory.CategoryStruct.{v, u} C] → CategoryTheory.ObjectProperty C → CategoryTheory.ObjectProperty Cᵒᵖ
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.BitVec.ite_same_then : ∀ {w : ℕ} (c : Bool) (t e : BitVec w), ((bif c then t else e) == t) = (c || t == e)
-- Mathlib.Algebra.Algebra.Basic
/-- If `A` is an `R`-algebra, it is also a `ULift R`-algebra. In particular, `Ulift A` is a
`ULift R` algebra. This is not an instance, because it causes a non-reducible diamond in the case
where `A = Ulift R`.  -/
ULift.algebra' : (R : Type u_1) →
  (A : Type u_2) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [Algebra R A] → Algebra (ULift.{u, u_1} R) A
-- Mathlib.Topology.Constructible
Topology.IsConstructible.sUnion : ∀ {X : Type u_2} [inst : TopologicalSpace X] {S : Set (Set X)},
  S.Finite → (∀ s ∈ S, Topology.IsConstructible s) → Topology.IsConstructible (⋃₀ S)
-- Mathlib.Analysis.SpecialFunctions.Log.ERealExp
EReal.exp_eq_zero_iff : ∀ {x : EReal}, x.exp = 0 ↔ x = ⊥
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.lift₃_p₁ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Full] {A₁ A₂ A₃ : C} {X : D} {f₁ : F.obj A₁ ⟶ X}
  (hf₁ : F.relativelyRepresentable f₁) (f₂ : F.obj A₂ ⟶ X) (f₃ : F.obj A₃ ⟶ X)
  [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)] [inst_4 : F.Faithful] {Z : C} (x₁ : Z ⟶ A₁)
  (x₂ : Z ⟶ A₂) (x₃ : Z ⟶ A₃)
  (h₁₂ : CategoryTheory.CategoryStruct.comp (F.map x₁) f₁ = CategoryTheory.CategoryStruct.comp (F.map x₂) f₂)
  (h₁₃ : CategoryTheory.CategoryStruct.comp (F.map x₁) f₁ = CategoryTheory.CategoryStruct.comp (F.map x₃) f₃),
  CategoryTheory.CategoryStruct.comp (hf₁.lift₃ f₂ f₃ x₁ x₂ x₃ h₁₂ h₁₃)
      (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₁ hf₁ f₂ f₃) =
    x₁
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.genEigenspace_top : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Module.End R M)
  (μ : R), (f.genEigenspace μ) ⊤ = ⨆ k, (f.genEigenspace μ) ↑k
-- Mathlib.Algebra.Group.Commute.Units
AddCommute.isAddUnit_add_iff : ∀ {M : Type u_1} [inst : AddMonoid M] {a b : M}, AddCommute a b → (IsAddUnit (a + b) ↔ IsAddUnit a ∧ IsAddUnit b)
-- Mathlib.Data.Multiset.Replicate
Multiset.replicate_succ : ∀ {α : Type u_1} (a : α) (n : ℕ), Multiset.replicate (n + 1) a = a ::ₘ Multiset.replicate n a
-- Mathlib.Data.List.ProdSigma
List.mem_product : ∀ {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β} {a : α} {b : β}, (a, b) ∈ l₁ ×ˢ l₂ ↔ a ∈ l₁ ∧ b ∈ l₂
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.eq_norm0 : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] (lhs rhs : α), (lhs = rhs) = (lhs = rhs + ↑0)
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
GaloisConnection.u_ciInf : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α]
  [inst_1 : ConditionallyCompleteLattice β] [Nonempty ι] {l : α → β} {u : β → α},
  GaloisConnection l u → ∀ {f : ι → β}, BddBelow (Set.range f) → u (⨅ i, f i) = ⨅ i, u (f i)
-- Std.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.Equiv.forIn_eq : ∀ {α₁ α₂ β γ : Type w} {m : Type w → Type w'} [inst : Std.Iterator α₁ Id β] [inst_1 : Std.Iterator α₂ Id β]
  [Std.Iterators.Finite α₁ Id] [Std.Iterators.Finite α₂ Id] [inst_4 : Monad m] [LawfulMonad m]
  [inst_6 : Std.IteratorLoop α₁ Id m] [Std.LawfulIteratorLoop α₁ Id m] [inst_8 : Std.IteratorLoop α₂ Id m]
  [Std.LawfulIteratorLoop α₂ Id m] {init : γ} {f : β → γ → m (ForInStep γ)} {ita : Std.Iter β} {itb : Std.Iter β},
  ita.Equiv itb → forIn ita init f = forIn itb init f
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preBeth_add_one : ∀ (o : Ordinal.{u_1}), Cardinal.preBeth (o + 1) = 2 ^ Cardinal.preBeth o
-- Mathlib.Analysis.Analytic.Constructions
/-- Eta-expanded form of `AnalyticAt.smul`

---

Scalar multiplication of one analytic function by another.  -/
AnalyticAt.fun_smul : ∀ {𝕜 : 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] {A : Type u_7}
  [inst_5 : NormedRing A] [inst_6 : NormedAlgebra 𝕜 A] [inst_7 : Module A F] [IsBoundedSMul A F] [IsScalarTower 𝕜 A F]
  {f : E → A} {g : E → F} {z : E}, AnalyticAt 𝕜 f z → AnalyticAt 𝕜 g z → AnalyticAt 𝕜 (fun i => f i • g i) z
-- Mathlib.Data.Set.Card
/-- A tactic (for use in default params) that applies `Set.toFinite` to synthesize a `Set.Finite`
term.  -/
Set.tacticToFinite_tac : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.Flat.mk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  (∀ {U : Y.Opens},
      AlgebraicGeometry.IsAffineOpen U →
        ∀ {V : X.Opens},
          AlgebraicGeometry.IsAffineOpen V →
            ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
              (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).Flat) →
    AlgebraicGeometry.Flat f
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- Let `F : C₀ ⥤ C` be a dense subsite and `data : ∀ X, F.OneHypercoverDenseData J₀ J X`
be a family of structures. Let `G₀` be a sheaf on `C₀`. This is a sheaf on `C` which
extends `G₀` (see `OneHypercoverDenseData.essSurj.isSheafIso`).  -/
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.sheaf : {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] →
                  [CategoryTheory.Functor.IsDenseSubsite J₀ J F] →
                    ((X : C) → F.OneHypercoverDenseData J₀ J X) →
                      [CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] →
                        CategoryTheory.Sheaf J₀ A → CategoryTheory.Sheaf J A
-- Mathlib.Topology.Separation.Regular
normal_exists_closure_subset : ∀ {X : Type u_1} [inst : TopologicalSpace X] [NormalSpace X] {s t : Set X},
  IsClosed s → IsOpen t → s ⊆ t → ∃ u, IsOpen u ∧ s ⊆ u ∧ closure u ⊆ t
-- Mathlib.Algebra.Category.Semigrp.Basic
_private.Mathlib.Algebra.Category.Semigrp.Basic.0.AddMagmaCat.Hom.mk.injEq : ∀ {A B : AddMagmaCat} (hom' hom'_1 : ↑A →ₙ+ ↑B), ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.Data.List.Induction
List.reverseRecOn_nil : ∀ {α : Type u_1} {motive : List α → Sort u_2} (nil : motive [])
  (append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])),
  List.reverseRecOn [] nil append_singleton = nil
-- Mathlib.CategoryTheory.Subfunctor.Equalizer
CategoryTheory.Subfunctor.equalizer.lift_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F₁ F₂ : CategoryTheory.Functor C (Type w)}
  {A : CategoryTheory.Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) {G : CategoryTheory.Functor C (Type w)}
  (φ : G ⟶ A.toFunctor) (w : CategoryTheory.CategoryStruct.comp φ f = CategoryTheory.CategoryStruct.comp φ g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subfunctor.equalizer.lift f g φ w)
      (CategoryTheory.Subfunctor.equalizer.ι f g) =
    φ
-- Mathlib.GroupTheory.Finiteness
instFGFreeAddMonoidOfFinite : ∀ (α : Type u_3) [Finite α], AddMonoid.FG (FreeAddMonoid α)
-- Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap
ContinuousMap.aeStronglyMeasurable_restrict_mkD_of_uncurry : ∀ {X : Type u_1} {Y : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : TopologicalSpace Y]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [CompactSpace Y] {s : Set X} [inst_4 : TopologicalSpace X]
  [OpensMeasurableSpace X] [SecondCountableTopologyEither X C(Y, E)],
  MeasurableSet s →
    ∀ (f : X → Y → E) (g : C(Y, E)),
      ContinuousOn (Function.uncurry f) (s ×ˢ Set.univ) →
        MeasureTheory.AEStronglyMeasurable (fun x => ContinuousMap.mkD (f x) g) (μ.restrict s)
-- Mathlib.Probability.Kernel.Composition.Comp
ProbabilityTheory.Kernel.ae_null_of_comp_null : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel β γ} {a : α} {s : Set γ},
  ((η.comp κ) a) s = 0 → (fun x => (η x) s) =ᵐ[κ a] 0
-- Mathlib.Tactic.Subsingleton
/-- Closes the goal `g` whose target is an `Eq` or `HEq` by appealing to the fact that the types
are subsingletons.
Fails if it cannot find a way to do this.

Has support for showing `BEq` instances are equal if they have `LawfulBEq` instances.
 -/
Lean.MVarId.subsingleton : Lean.MVarId → optParam (Array (Lean.Term × Lean.Meta.AbstractMVarsResult)) #[] → Lean.MetaM Unit
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_alter_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k : α} {f : Option β → Option β},
  Std.DTreeMap.Internal.Impl.Const.get? (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl k =
    f (Std.DTreeMap.Internal.Impl.Const.get? t k)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.mkSubNat : Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.end_.map_comp_assoc : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_2 : CategoryTheory.Limits.HasEnd F]
  {F' : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_3 : CategoryTheory.Limits.HasEnd F'] (f : F ⟶ F')
  {F'' : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_4 : CategoryTheory.Limits.HasEnd F'']
  (g : F' ⟶ F'') {Z : C} (h : CategoryTheory.Limits.end_ F'' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.end_.map f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.end_.map g) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.end_.map (CategoryTheory.CategoryStruct.comp f g)) h
-- Init.Data.List.MinMaxOn
List.isSome_minOn?_of_mem : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α} {x : α},
  x ∈ xs → (List.minOn? f xs).isSome = true
-- Std.Data.DTreeMap.Iterator
Std.DTreeMap.valuesIter_toList : ∀ {α β : Type u_1} {cmp : α → α → Ordering} (m : Std.DTreeMap α (fun x => β) cmp), m.valuesIter.toList = m.values
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
hasSum_iff_hasSum : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {a : α} {g : γ → α},
  (∀ (u : Finset γ), ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∑ x ∈ u', g x = ∑ b ∈ v', f b) →
    (∀ (v : Finset β), ∃ u, ∀ (u' : Finset γ), u ⊆ u' → ∃ v', v ⊆ v' ∧ ∑ b ∈ v', f b = ∑ x ∈ u', g x) →
      (HasSum f a ↔ HasSum g a)
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.lambda_not_dvd_z : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [IsCyclotomicExtension {3} ℚ K],
  ¬hζ.toInteger - 1 ∣ FermatLastTheoremForThreeGen.Solution.z✝ S
-- Mathlib.MeasureTheory.OuterMeasure.Basic
MeasureTheory.OuterMeasure.ext : ∀ {α : Type u_1} {μ₁ μ₂ : MeasureTheory.OuterMeasure α}, (∀ (s : Set α), μ₁ s = μ₂ s) → μ₁ = μ₂
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
instIsCancelMulZero_1 : ∀ {α : Type u_1} [inst : LinearOrderedCommMonoidWithZero α], IsCancelMulZero α
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.toArray_filter : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} {f : α → β → Bool}
  (h : t.WF),
  Std.DTreeMap.Internal.Impl.Const.toArray (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl =
    Array.filter (fun p => f p.1 p.2) (Std.DTreeMap.Internal.Impl.Const.toArray t)
-- Init.Data.Array.Lex.Lemmas
Array.instAsymmLt : ∀ {α : Type u_1} [inst : LT α] [Std.Asymm fun x1 x2 => x1 < x2], Std.Asymm fun x1 x2 => x1 < x2
-- Mathlib.Algebra.Group.Pointwise.Finset.Interval
Finset.Ioi_mul_Ici_subset' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : PartialOrder α] [inst_2 : DecidableEq α] [MulLeftStrictMono α]
  [MulRightStrictMono α] [inst_5 : LocallyFiniteOrderTop α] (a b : α), Finset.Ioi a * Finset.Ici b ⊆ Finset.Ioi (a * b)
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.Additive.mk : ∀ {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] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D},
  autoParam (∀ {X Y : C} {f g : X ⟶ Y}, F.map (f + g) = F.map f + F.map g)
      CategoryTheory.Functor.Additive.map_add._autoParam →
    F.Additive
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.lup.eq_1 : ∀ (L : List (List (Option ℕ))) (p : ℕ × Nat.Partrec.Code) (n : ℕ),
  Nat.Partrec.Code.lup✝ L p n = do
    let l ← L[Encodable.encode p]?
    let o ← l[n]?
    o
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.smul_monomial : ∀ {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ ℕ} [inst : CommSemiring R] {S₁ : Type u_2} [inst_1 : SMulZeroClass S₁ R]
  (r : S₁), r • (MvPolynomial.monomial s) a = (MvPolynomial.monomial s) (r • a)
-- Lean.Parser.Command
Lean.Parser.Command.whereStructInst.formatter : Lean.PrettyPrinter.Formatter