mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.p₁₂_p₂_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃) {Z : C}
  (h_1 : X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.p₁₂ (CategoryTheory.CategoryStruct.comp h₁₂.p₂ h_1) =
    CategoryTheory.CategoryStruct.comp h.p₂ h_1
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_eq_self : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] {a : R},
  Int.fract a = a ↔ 0 ≤ a ∧ a < 1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  (t.insertIfNew k v).isEmpty = false
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_inter_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → (m₁ ∩ m₂).get? k = m₁.get? k
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.mul'.eq_def : ∀ (p : Lean.Grind.Linarith.Poly) (k : ℤ),
  p.mul' k =
    match p with
    | Lean.Grind.Linarith.Poly.nil => Lean.Grind.Linarith.Poly.nil
    | Lean.Grind.Linarith.Poly.add k' v p => Lean.Grind.Linarith.Poly.add (k * k') v (p.mul' k)
-- Lean.Compiler.IR.Basic
/-- Function identifier  -/
Lean.IR.FunId : Type
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.finiteIndex : ∀ {S : Type u_1} [inst : CommRing S] [IsDedekindDomain S] [Module.Free ℤ S] [Module.Finite ℤ S] {I : Ideal S},
  I ≠ ⊥ → (Submodule.toAddSubgroup I).FiniteIndex
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.mkSyntaxQuotation : Lean.Syntax → Lean.Name → Lean.Elab.TermElabM Lean.Syntax
-- Mathlib.Probability.Moments.CovarianceBilin
ProbabilityTheory.covarianceBilin_self_nonneg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] {μ : MeasureTheory.Measure E} (x : E), 0 ≤ ((ProbabilityTheory.covarianceBilin μ) x) x
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.SignedMeasure.toJordanDecomposition_eq_of_eq_add_withDensity : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : MeasureTheory.SignedMeasure α} {f : α → ℝ}
  (hf : Measurable f) (hfi : MeasureTheory.Integrable f μ)
  (htμ : MeasureTheory.VectorMeasure.MutuallySingular t μ.toENNRealVectorMeasure),
  s = t + μ.withDensityᵥ f →
    s.toJordanDecomposition =
      { posPart := t.toJordanDecomposition.posPart + μ.withDensity fun x => ENNReal.ofReal (f x),
        negPart := t.toJordanDecomposition.negPart + μ.withDensity fun x => ENNReal.ofReal (-f x), posPart_finite := ⋯,
        negPart_finite := ⋯, mutuallySingular := ⋯ }
-- Mathlib.Algebra.Free
FreeAddMagma.traverse_pure' : ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β), traverse F ∘ pure = fun x => pure <$> F x
-- Mathlib.Topology.Order.Priestley
exists_isClopen_upper_of_not_le : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α] [PriestleySpace α] {x y : α},
  ¬x ≤ y → ∃ U, IsClopen U ∧ IsUpperSet U ∧ x ∈ U ∧ y ∉ U
-- Mathlib.Tactic.TacticAnalysis
/-- The option, of type `Lean.Option Bool`, that controls whether the pass is enabled.  -/
Mathlib.TacticAnalysis.Entry.optionName : Mathlib.TacticAnalysis.Entry → Lean.Name
-- Mathlib.Order.Category.HeytAlg
HeytAlg.ofHom_apply : ∀ {X Y : Type u} [inst : HeytingAlgebra X] [inst_1 : HeytingAlgebra Y] (f : HeytingHom X Y) (x : X),
  (CategoryTheory.ConcreteCategory.hom (HeytAlg.ofHom f)) x = f x
-- Std.Sat.AIG.Basic
/-- The `decls` `Array` can never be empty, see `hconst`.
 -/
Std.Sat.AIG.hzero : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] (self : Std.Sat.AIG α), 0 < self.decls.size
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.den_mem_deg : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] {𝒜 : ι → σ} {x : Submonoid A}
  (f : HomogeneousLocalization 𝒜 x), f.den ∈ 𝒜 f.deg
-- Init.Data.Range.Polymorphic.UInt
UInt32.upwardEnumerableLT_ofBitVec : ∀ {x y : BitVec 32},
  Std.PRange.UpwardEnumerable.LT { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LT x y
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.copy_eq : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} (f : ↑(GenLoop N X x)) {g : (N → ↑unitInterval) → X}
  (h : g = ⇑f), GenLoop.copy f g h = f
-- Mathlib.CategoryTheory.Subobject.WellPowered
CategoryTheory.small_subobject : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v, u₁} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u₁} C]
  [CategoryTheory.WellPowered.{w, v, u₁} C] (X : C), Small.{w, max u₁ v} (CategoryTheory.Subobject X)
-- Mathlib.CategoryTheory.Sites.LeftExact
CategoryTheory.SheafOfTypes.finitary_extensive : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [CategoryTheory.HasSheafify J (Type w)], CategoryTheory.FinitaryExtensive (CategoryTheory.Sheaf J (Type w))
-- Init.Data.Float.Float
/-- Computes the base-10 logarithm of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`log10`.
 -/
Float.log10 : Float → Float
-- Mathlib.Order.Category.Semilat
SemilatInfCat.dual_map : ∀ {x x_1 : SemilatInfCat} (a : InfTopHom x.X x_1.X), SemilatInfCat.dual.map a = InfTopHom.dual a
-- Mathlib.Probability.Process.Stopping
MeasureTheory.StronglyAdapted.stronglyMeasurable_stoppedProcess_of_discrete : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : TopologicalSpace β]
  [TopologicalSpace.PseudoMetrizableSpace β] [inst_2 : Nonempty ι] [inst_3 : LinearOrder ι]
  [inst_4 : TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] [inst_7 : MeasurableSpace ι]
  [BorelSpace ι] {f : MeasureTheory.Filtration ι m} {u : ι → Ω → β} {τ : Ω → WithTop ι} [DiscreteTopology ι],
  MeasureTheory.StronglyAdapted f u →
    MeasureTheory.IsStoppingTime f τ → ∀ (n : ι), MeasureTheory.StronglyMeasurable (MeasureTheory.stoppedProcess u τ n)
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
lt_iff_exists_mul : ∀ {α : Type u} [inst : MulOneClass α] [inst_1 : PartialOrder α] [CanonicallyOrderedMul α] {a b : α}
  [MulLeftStrictMono α], a < b ↔ ∃ c > 1, b = a * c
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_filter_key_eq_length_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {f : α → Bool} {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ((List.filter (fun p => f p.fst) l).length = l.length ↔
      ∀ (a : α) (h : Std.Internal.List.containsKey a l = true), f (Std.Internal.List.getKey a l h) = true)
-- Mathlib.Probability.Process.Adapted
MeasureTheory.IsStronglyProgressive.mul : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] {u v : ι → Ω → β} [inst_2 : MeasurableSpace ι] [inst_3 : Mul β]
  [ContinuousMul β],
  MeasureTheory.IsStronglyProgressive f u →
    MeasureTheory.IsStronglyProgressive f v → MeasureTheory.IsStronglyProgressive f fun i ω => u i ω * v i ω
-- Mathlib.Topology.MetricSpace.IsometricSMul
isometry_add_right : ∀ {M : Type u} [inst : Add M] [inst_1 : PseudoEMetricSpace M] [IsIsometricVAdd Mᵃᵒᵖ M] (a : M), Isometry fun x => x + a
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Icc.mk_zero : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] (h : 0 ∈ Set.Icc 0 1),
  ⟨0, h⟩ = 0
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.sectionsMap_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M : PresheafOfModules R} (s : M.sections), PresheafOfModules.sectionsMap (CategoryTheory.CategoryStruct.id M) s = s
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.image_ι_comp_eq_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} {f : P ⟶ Q}
  {R : C} {g : Q ⟶ R},
  CategoryTheory.CategoryStruct.comp f g = 0 →
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.image.ι f) g = 0
-- Mathlib.Topology.Order.LawsonTopology
/-- Predicate for an ordered topological space to be equipped with its Lawson topology.

The Lawson topology is defined as the meet of `Topology.lower` and the `Topology.scott`.
 -/
Topology.IsLawson : (α : Type u_1) → [Preorder α] → [TopologicalSpace α] → Prop
-- Mathlib.GroupTheory.Submonoid.Center
Submonoid.center.commMonoid.eq_1 : ∀ {M : Type u_1} [inst : Monoid M],
  Submonoid.center.commMonoid = { toMonoid := (Submonoid.center M).toMonoid, mul_comm := ⋯ }
-- Mathlib.Topology.Order.MonotoneConvergence
tendsto_atBot_of_monotone : ∀ {ι : Type u_3} {α : Type u_4} [inst : Preorder ι] [inst_1 : TopologicalSpace α]
  [inst_2 : ConditionallyCompleteLinearOrder α] [OrderTopology α] {f : ι → α},
  Monotone f → Filter.Tendsto f Filter.atBot Filter.atBot ∨ ∃ l, Filter.Tendsto f Filter.atBot (nhds l)
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.SplitEpi.comp_section_ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z}
  (sef : CategoryTheory.SplitEpi f) (seg : CategoryTheory.SplitEpi g),
  (sef.comp seg).section_ = CategoryTheory.CategoryStruct.comp seg.section_ sef.section_
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
HomotopyCategory.Plus.instEssSurjPlusQuotient : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C],
  (HomotopyCategory.Plus.quotient C).EssSurj
-- Mathlib.RingTheory.Unramified.Basic
Algebra.FormallyUnramified.lift_unique' : ∀ {R : Type v} [inst : CommRing R] {A : Type u} [inst_1 : CommRing A] [inst_2 : Algebra R A] {B : Type w}
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [Algebra.FormallyUnramified R A] {C : Type u_1} [inst_6 : Ring C]
  [inst_7 : Algebra R C] (f : B →ₐ[R] C),
  IsNilpotent (RingHom.ker ↑f) → ∀ (g₁ g₂ : A →ₐ[R] B), f.comp g₁ = f.comp g₂ → g₁ = g₂
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonPlainTermGoalParams.fromJson : Lean.Json → Except String Lean.Lsp.PlainTermGoalParams
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.ofHom_hom : ∀ {X Y : PartOrdEmb} (f : X ⟶ Y), PartOrdEmb.ofHom (PartOrdEmb.Hom.hom f) = f
-- Mathlib.RingTheory.PowerSeries.WellKnown
/-- Given a natural number `d : ℕ` and a commutative ring `S`, `PowerSeries.invOneSubPow S d` is the
multiplicative inverse of `(1 - X) ^ d` in `S⟦X⟧ˣ`. When `d` is `0`, `PowerSeries.invOneSubPow S d`
will just be `1`. When `d` is positive, `PowerSeries.invOneSubPow S d` will be the power series
`mk fun n => Nat.choose (d - 1 + n) (d - 1)`.
 -/
PowerSeries.invOneSubPow : (S : Type u_1) → [inst : CommRing S] → ℕ → (PowerSeries S)ˣ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List ((a : α) × β a)}
  {k k' fallback : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
      k ∈ List.map Sigma.fst l → (Std.DTreeMap.Raw.ofList l cmp).getKeyD k' fallback = k
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.toList_filter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {f : (a : α) → β a → Bool},
  (Std.DHashMap.filter f m).toList.Perm (List.filter (fun p => f p.fst p.snd) m.toList)
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- Restrict a ring homomorphism with a left inverse to a ring isomorphism to its
`RingHom.range`.  -/
RingEquiv.ofLeftInverse' : {R : Type u} →
  {S : Type v} →
    [inst : NonUnitalRing R] →
      [inst_1 : NonUnitalRing S] → {g : S → R} → {f : R →ₙ+* S} → Function.LeftInverse g ⇑f → R ≃+* ↥f.range
-- Mathlib.Order.RelIso.Basic
/-- A relation isomorphism is also a relation isomorphism between complemented relations.  -/
RelIso.compl : {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → r ≃r s → rᶜ ≃r sᶜ
-- Mathlib.LinearAlgebra.Prod
LinearMap.range_inr : ∀ (R : Type u) (M : Type v) (M₂ : Type w) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], (LinearMap.inr R M M₂).range = (LinearMap.fst R M M₂).ker
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.constant : Lean.Lsp.CompletionItemKind
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- `∏ i ∈ Nat.divisors n, cyclotomic i R = X ^ n - 1`.  -/
Polynomial.prod_cyclotomic_eq_X_pow_sub_one : ∀ {n : ℕ},
  0 < n → ∀ (R : Type u_1) [inst : CommRing R], ∏ i ∈ n.divisors, Polynomial.cyclotomic i R = Polynomial.X ^ n - 1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
/-- The canonical isomorphism `(X₁ ⨿[Z₁] X₂) ⨿[Z₂] X₃ ≅ X₁ ⨿[Z₁] (X₂ ⨿[Z₂] X₃)`.  -/
CategoryTheory.Limits.pushoutAssoc : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ Z₁ Z₂ : C} →
      (g₁ : Z₁ ⟶ X₁) →
        (g₂ : Z₁ ⟶ X₂) →
          (g₃ : Z₂ ⟶ X₂) →
            (g₄ : Z₂ ⟶ X₃) →
              [inst_1 : CategoryTheory.Limits.HasPushout g₁ g₂] →
                [inst_2 : CategoryTheory.Limits.HasPushout g₃ g₄] →
                  [inst_3 :
                      CategoryTheory.Limits.HasPushout
                        (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄] →
                    [inst_4 :
                        CategoryTheory.Limits.HasPushout g₁
                          (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))] →
                      CategoryTheory.Limits.pushout
                          (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄ ≅
                        CategoryTheory.Limits.pushout g₁
                          (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
/-- The obvious map `PullbackCone f g → PushoutCocone f.op g.op`  -/
CategoryTheory.Limits.PullbackCone.op : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : C} →
      {f : X ⟶ Z} → {g : Y ⟶ Z} → CategoryTheory.Limits.PullbackCone f g → CategoryTheory.Limits.PushoutCocone f.op g.op
-- Mathlib.Topology.Algebra.ConstMulAction
closure_vadd : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddGroup G] [inst_2 : AddAction G α]
  [ContinuousConstVAdd G α] (c : G) (s : Set α), closure (c +ᵥ s) = c +ᵥ closure s
-- Mathlib.SetTheory.ZFC.Ordinal
Ordinal.toZFSet_subset_toZFSet_iff : ∀ {a b : Ordinal.{u_1}}, a.toZFSet ⊆ b.toZFSet ↔ a ≤ b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_of_contains_filterMap : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w} [Std.TransOrd α]
  {f : (a : α) → β a → Option (γ a)} {k : α} (h : t.WF),
  Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl = true →
    Std.DTreeMap.Internal.Impl.contains k t = true
-- Mathlib.Data.Setoid.Basic
/-- The supremum of a set of equivalence relations is the equivalence closure of the
supremum of the set's image under the map to the underlying binary operation.  -/
Setoid.sSup_def : ∀ {α : Type u_1} {s : Set (Setoid α)}, sSup s = Relation.EqvGen.setoid (sSup (@Setoid.r α '' s))
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.inf_apply : ∀ {E : Type u_3} [inst : AddCommGroup E] (p q : AddGroupSeminorm E) (x : E), (p ⊓ q) x = ⨅ y, p y + q (x - y)
-- Init.Data.SInt.Lemmas
Int64.ofIntTruncate_int32ToInt : ∀ (x : Int32), Int64.ofIntClamp x.toInt = x.toInt64
-- Mathlib.RingTheory.HahnSeries.Summable
/-- A parametrized family of Hahn series.  -/
HahnSeries.SummableFamily.toFun : {Γ : Type u_8} →
  {R : Type u_9} →
    [inst : PartialOrder Γ] →
      [inst_1 : AddCommMonoid R] → {α : Type u_7} → HahnSeries.SummableFamily Γ R α → α → HahnSeries Γ R
-- Mathlib.Algebra.LinearRecurrence
/-- The dimension of `E.solSpace` is `E.order`.  -/
LinearRecurrence.solSpace_rank : ∀ {R : Type u_1} [inst : CommRing R] [StrongRankCondition R] (E : LinearRecurrence R),
  Module.rank R ↥E.solSpace = ↑E.order
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : C} [inst_1 : CategoryTheory.Abelian C]
  (hG : CategoryTheory.IsSeparator G) {X : C} (A : CategoryTheory.Subobject X),
  CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject hG A = if hA : A = ⊤ then ⊤ else ⋯.choose
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.separableSpace_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α],
  TopologicalSpace.SeparableSpace (TopologicalSpace.NonemptyCompacts α) ↔ TopologicalSpace.SeparableSpace α
-- Lean.Linter.UnusedVariables
Lean.Linter.UnusedVariables.FVarDefinition.mk.inj : ∀ {userName : Lean.Name} {stx : Lean.Syntax} {opts : Lean.Options} {aliases : Array Lean.FVarId}
  {userName_1 : Lean.Name} {stx_1 : Lean.Syntax} {opts_1 : Lean.Options} {aliases_1 : Array Lean.FVarId},
  { userName := userName, stx := stx, opts := opts, aliases := aliases } =
      { userName := userName_1, stx := stx_1, opts := opts_1, aliases := aliases_1 } →
    userName = userName_1 ∧ stx = stx_1 ∧ opts = opts_1 ∧ aliases = aliases_1
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.divXPowOrder_zero : ∀ {R : Type u_1} [inst : Semiring R], PowerSeries.divXPowOrder 0 = 0
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- Auxiliary construction to obtain the group structure on the limit of profinite groups.  -/
ProfiniteGrp.limitConePtAux : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J ProfiniteGrp.{max v u}) → Subgroup ((j : J) → ↑(F.obj j).toProfinite.toTop)
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Monad.comparisonForget_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (x : D),
  (CategoryTheory.Monad.comparisonForget h).hom.app x =
    CategoryTheory.CategoryStruct.id (((CategoryTheory.Monad.comparison h).comp h.toMonad.forget).obj x)
-- Std.Http.Data.URI.Parser
_private.Std.Http.Data.URI.Parser.0.Std.Http.URI.Parser.parseIPv4 : Std.Internal.Parsec.ByteArray.Parser Std.Net.IPv4Addr
-- Std.Data.DHashMap.Basic
Std.DHashMap.instDecidableMem : {α : Type u} →
  {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → {m : Std.DHashMap α β} → {a : α} → Decidable (a ∈ m)
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.MapSubtype.orderIso.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G),
  AddSubgroup.MapSubtype.orderIso H =
    { toFun := fun H' => ⟨AddSubgroup.map H.subtype H', ⋯⟩, invFun := fun sH' => (↑sH').addSubgroupOf H, left_inv := ⋯,
      right_inv := ⋯, map_rel_iff' := ⋯ }
-- Lean.Expr
/-- Return `true` if `e` contains any loose bound variables.

This is a constant time operation.  -/
Lean.Expr.hasLooseBVars : Lean.Expr → Bool
-- Batteries.Data.List.Lemmas
List.IsChain.pairwise : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α} [Trans R R R], List.IsChain R l → List.Pairwise R l
-- Mathlib.Logic.Embedding.Set
Function.Embedding.sumSet_apply : ∀ {α : Type u_1} {s t : Set α} (h : Disjoint s t) (a : ↑s ⊕ ↑t),
  (Function.Embedding.sumSet h) a = Sum.elim Subtype.val Subtype.val a
-- Mathlib.Data.Seq.Defs
Stream'.Seq.instInhabited : {α : Type u} → Inhabited (Stream'.Seq α)
-- Init.Data.SInt.Lemmas
Int8.toInt_bmod_size : ∀ (a : Int8), a.toInt.bmod Int8.size = a.toInt
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : 𝕜 → 𝕜` is continuous on `s` and `f 0 = 0` and `a : X → A` is continuous and `a x`
satisfies the predicate `p` associated to `𝕜` and `s` is a common neighborhood of the quasispectra
of `a x` for all `x`, then `fun x ↦ cfcₙ f (a x)` is continuous.

This is weaker than `Continuous.cfcₙ` since it requires `f` to be continuous on a *neighborhood* of
the quasispectra, but in practice it is often easier to apply because `s` is not required to be
compact, nor does it require an indexed family of compact sets. This is proven using
`Continuous.cfcₙ` and `upperHemicontinuous_quasispectrum` to produce the necessary family of
compact sets.  -/
Continuous.cfcₙ_of_mem_nhdsSet : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A]
  [ContinuousStar A] [inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] [CompleteSpace A]
  [inst_9 : TopologicalSpace X] {s : Set 𝕜} (f : 𝕜 → 𝕜) {a : X → A},
  s ∈ nhdsSet (⋃ x, quasispectrum 𝕜 (a x)) →
    Continuous a →
      autoParam (∀ (x : X), p (a x)) Continuous.cfcₙ_of_mem_nhdsSet._auto_1 →
        autoParam (ContinuousOn f s) Continuous.cfcₙ_of_mem_nhdsSet._auto_3 →
          autoParam (f 0 = 0) Continuous.cfcₙ_of_mem_nhdsSet._auto_5 → Continuous fun x => cfcₙ f (a x)
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.hom_ofHom : ∀ {X Y : Type u} [inst : PartialOrder X] [inst_1 : PartialOrder Y] (f : X ↪o Y),
  PartOrdEmb.Hom.hom (PartOrdEmb.ofHom f) = f
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec_hom_app : ∀ (X : AlgebraicGeometry.Scheme) (X_1 : X.AffineZariskiSite),
  (AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec X).hom.app X_1 = ⋯.isoSpec.hom
-- Mathlib.Algebra.Lie.Abelian
LieModule.instIsTrivialOfSubsingleton : ∀ {L : Type u_1} {M : Type u_2} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M]
  [Subsingleton L], LieModule.IsTrivial L M
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.union_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → (t₁ ∪ t₃).Equiv (t₂ ∪ t₃)
-- Init.Classical
Classical.epsilon_spec_aux : ∀ {α : Sort u} (h : Nonempty α) (p : α → Prop), (∃ y, p y) → p (Classical.epsilon p)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cocycle.δ_eq_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} {n : ℤ} (z : CochainComplex.HomComplex.Cocycle F G n) (m : ℤ),
  CochainComplex.HomComplex.δ n m ↑z = 0
-- Mathlib.Data.NNReal.Defs
NNReal.coe_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], ↑(OfNat.ofNat n) = OfNat.ofNat n
-- Lean.Meta.WHNF
Lean.Meta.ReduceMatcherResult.partialApp : Lean.Meta.ReduceMatcherResult
-- Mathlib.Order.Cover
Bool.instDecidableRelWCovBy : DecidableRel fun x1 x2 => x1 ⩿ x2
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.compl_subset_compl : ∀ {α : Type u_1} {s t : Finset α} [inst : Fintype α] [inst_1 : DecidableEq α], sᶜ ⊆ tᶜ ↔ t ⊆ s
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A subalgebra of a seminormed commutative ring is also a seminormed commutative ring, with the
restriction of the norm.  -/
Subalgebra.seminormedCommRing : {𝕜 : Type u_5} →
  [inst : CommRing 𝕜] →
    {E : Type u_6} →
      [inst_1 : SeminormedCommRing E] → [inst_2 : Algebra 𝕜 E] → (s : Subalgebra 𝕜 E) → SeminormedCommRing ↥s
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.instHasColimits : ∀ {X : AlgebraicGeometry.Scheme}, CategoryTheory.Limits.HasColimits X.Modules
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Over.Hom.ext_iff : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T}
  [inst_1 : Q.IsMultiplicative] {A B : P.Over Q X} {f g : A ⟶ B}, f = g ↔ f.left = g.left