mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.shortComplexMap_τ₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) {i' j' k' l' : ι}
  (f₁' : i' ⟶ j') (f₂' : j' ⟶ k') (f₃' : k' ⟶ l')
  (α : CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₃ f₁' f₂' f₃') (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.shortComplexMap._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.shortComplexMap._auto_3),
  (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂).τ₃ =
    (X.H n₂).map (CategoryTheory.ComposableArrows.homMk₁ (α.app 0) (α.app 1) ⋯)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey!_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α] {l : List (α × β)}
  {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (Std.ExtDTreeMap.Const.ofList l cmp).getKey! k' = k
-- Mathlib.MeasureTheory.Measure.Stieltjes
/-- Length of an interval. This is the largest monotone function which correctly measures all
intervals.  -/
StieltjesFunction.length : {R : Type u_1} → [inst : LinearOrder R] → [inst_1 : TopologicalSpace R] → StieltjesFunction R → Set R → ENNReal
-- Std.Data.ExtTreeSet.Basic
Std.ExtTreeSet.instDecidableMem : {α : Type u} →
  {cmp : α → α → Ordering} → [inst : Std.TransCmp cmp] → {m : Std.ExtTreeSet α cmp} → {a : α} → Decidable (a ∈ m)
-- Lean.Parser.Extra
Lean.Parser.withPositionAfterLinebreak.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Lean.Meta.Tactic.Grind.Main
/-- When `Config.revert := false`, we preprocess the hypotheses, and add them to the `grind` state.
It starts at `goal.nextDeclIdx`. If `num?` is `some num`, then at most `num` local declarations are processed.
Otherwise, all remaining local declarations are processed.

Remark: this function assumes the local context does not contains holes with `none` in `decls`.
 -/
Lean.Meta.Grind.processHypotheses : Lean.Meta.Grind.Goal → optParam (Option ℕ) none → Lean.Meta.Grind.GrindM Lean.Meta.Grind.Goal
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.monoLM_eq_of_scalars : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n₁ n₂ : ℕ∞} {K₁ K₂ : TopologicalSpace.Compacts E} (𝕜' : Type u_5)
  [inst_7 : NontriviallyNormedField 𝕜'] [inst_8 : NormedSpace 𝕜' F] [inst_9 : SMulCommClass ℝ 𝕜' F],
  ⇑(ContDiffMapSupportedIn.monoLM 𝕜) = ⇑(ContDiffMapSupportedIn.monoLM 𝕜')
-- Mathlib.Data.Finset.Image
Finset.image_subset_image : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s₁ s₂ : Finset α},
  s₁ ⊆ s₂ → Finset.image f s₁ ⊆ Finset.image f s₂
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- A variant of `IsConjRoot.eq_zero`, only assuming `IsDomain R`,
`IsTorsionFree R A` and `Function.Injective (algebraMap R A)` instead of `Field R`. If `x` is a
conjugate root of `0`, then `x = 0`.
 -/
IsConjRoot.eq_zero_of_injective : ∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDomain S]
  [IsDomain R] [Module.IsTorsionFree R S] {x : S}, IsConjRoot R 0 x → Function.Injective ⇑(algebraMap R S) → x = 0
-- Aesop.Rule
Aesop.Safety : Type
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Cell.get?.match_1.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Option ((a : α) × β a) → Sort u_3) (p : (a : α) × β a)
  (h_1 : some p = none → motive none) (h_2 : (p_1 : (a : α) × β a) → some p = some p_1 → motive (some p_1)),
  (match h : some p with
    | none => h_1 h
    | some p_1 => h_2 p_1 h) =
    h_2 p ⋯
-- Init.Data.List.Nat.Range
List.erase_range' : ∀ {s n i : ℕ},
  (List.range' s n).erase i = List.range' s (min n (i - s)) ++ List.range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))
-- Mathlib.Combinatorics.SetFamily.Compression.Down
/-- `a`-down-compressing `𝒜` means removing `a` from the elements of `𝒜` that contain it, when the
resulting Finset is not already in `𝒜`.  -/
Down.compression : {α : Type u_1} → [DecidableEq α] → α → Finset (Finset α) → Finset (Finset α)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.init.eq_1 : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (q : (i : Fin (n + 1)) → α i) (i : Fin n), Fin.init q i = q i.castSucc
-- Mathlib.RingTheory.Localization.LocalizationLocalization
IsLocalization.localization_localization_exists_of_eq : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] (N : Submonoid S) (T : Type u_3) [inst_3 : CommSemiring T] [inst_4 : Algebra R T]
  [inst_5 : Algebra S T] [IsScalarTower R S T] [IsLocalization M S] [IsLocalization N T] (x y : R),
  (algebraMap R T) x = (algebraMap R T) y → ∃ c, ↑c * x = ↑c * y
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.π_natTransTruncGEOfLE_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) (X : C) {Z : C} (h_1 : (t.truncGE b).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.truncGEπ a).app X)
      (CategoryTheory.CategoryStruct.comp ((t.natTransTruncGEOfLE a b h).app X) h_1) =
    CategoryTheory.CategoryStruct.comp ((t.truncGEπ b).app X) h_1
-- Std.Data.DTreeMap.Internal.Operations
/-- A tuple of a key-value pair and a tree.  -/
Std.DTreeMap.Internal.Impl.RawView : (α : Type u) → (α → Type v) → Type (max u v)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_inter_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, (m₁.inter m₂).contains k = true ↔ m₁.contains k = true ∧ m₂.contains k = true
-- Mathlib.Topology.UniformSpace.UniformConvergence
TendstoUniformlyOn.mono : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s s' : Set α}
  {p : Filter ι}, TendstoUniformlyOn F f p s → s' ⊆ s → TendstoUniformlyOn F f p s'
-- Std.Data.TreeSet.Raw.Basic
Std.TreeSet.Raw.Equiv.mk : ∀ {α : Type u} {cmp : α → α → Ordering} {m₁ m₂ : Std.TreeSet.Raw α cmp}, m₁.inner.Equiv m₂.inner → m₁.Equiv m₂
-- Mathlib.Data.List.SplitBy
List.splitBy_append : ∀ {α : Type u_1} {r : α → α → Bool} {l m : List α},
  (∀ x ∈ l.getLast?, ∀ y ∈ m.head?, r x y = false) → List.splitBy r (l ++ m) = List.splitBy r l ++ List.splitBy r m
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- A structure giving a chosen right adjoint of a 1-morphism `left`.  -/
CategoryTheory.Bicategory.RightAdjoint : {B : Type u₁} → [inst : CategoryTheory.Bicategory B] → {a b : B} → (a ⟶ b) → Type (max v₁ w₁)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {f : (a : α) → β a → Bool}
  {l : List ((a : α) × β a)} {k : α} (hl : Std.Internal.List.DistinctKeys l)
  (h : Std.Internal.List.containsKey k (List.filter (fun p => f p.fst p.snd) l) = true),
  Std.Internal.List.getValueCast k (List.filter (fun p => f p.fst p.snd) l) h = Std.Internal.List.getValueCast k l ⋯
-- Mathlib.Order.Monotone.Defs
monotoneOn_univ : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β}, MonotoneOn f Set.univ ↔ Monotone f
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.ιTensorObj₃_tensorHom_assoc : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.GradedObject I C}
  [inst_3 : X₂.HasTensor X₃] [inst_4 : X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)]
  [inst_5 : Y₂.HasTensor Y₃] [inst_6 : Y₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj Y₂ Y₃)]
  (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) {Z : C}
  (h_1 :
    CategoryTheory.GradedObject.Monoidal.tensorObj Y₁ (CategoryTheory.GradedObject.Monoidal.tensorObj Y₂ Y₃) j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.GradedObject.Monoidal.tensorHom f₁ (CategoryTheory.GradedObject.Monoidal.tensorHom f₂ f₃) j)
        h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (f₁ i₁)
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (f₂ i₂) (f₃ i₃)))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ Y₁ Y₂ Y₃ i₁ i₂ i₃ j h) h_1)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited β] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (m.insertMany l)[k]! = m[k]!
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.HeightOneSpectrum.one_lt_absNorm_nnreal`.

---

The norm of a maximal ideal as an element of `ℝ≥0` is `> 1`  -/
NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  [Module.Finite ℤ R] [inst_3 : Module.Free ℤ R], 1 < ↑(Ideal.absNorm v.asIdeal)
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ωScottContinuous.id : ∀ {α : Type u_2} [inst : OmegaCompletePartialOrder α], OmegaCompletePartialOrder.ωScottContinuous id
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.inv_hom_id_hom_assoc : ∀ {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] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] {F G : CategoryTheory.SingleFunctors C D A} (e : F ≅ G) (n : A)
  {Z : CategoryTheory.Functor C D} (h : G.functor n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.inv.hom n) (CategoryTheory.CategoryStruct.comp (e.hom.hom n) h) = h
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
CategoryTheory.MonoidalCategory.DayConvolution.hexagon_forward : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory V] [inst_5 : CategoryTheory.BraidedCategory V]
  (F G : CategoryTheory.Functor C V)
  [inst_6 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_7 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  (H : CategoryTheory.Functor C V) [inst_8 : CategoryTheory.MonoidalCategory.DayConvolution F G]
  [inst_9 : CategoryTheory.MonoidalCategory.DayConvolution G H]
  [inst_10 :
    CategoryTheory.MonoidalCategory.DayConvolution F (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H)]
  [inst_11 :
    CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H]
  [inst_12 : CategoryTheory.MonoidalCategory.DayConvolution H F]
  [inst_13 :
    CategoryTheory.MonoidalCategory.DayConvolution G (CategoryTheory.MonoidalCategory.DayConvolution.convolution H F)]
  [inst_14 :
    CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H) F]
  [inst_15 : CategoryTheory.MonoidalCategory.DayConvolution G F]
  [inst_16 :
    CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution G F) H]
  [inst_17 : CategoryTheory.MonoidalCategory.DayConvolution F H]
  [inst_18 :
    CategoryTheory.MonoidalCategory.DayConvolution G (CategoryTheory.MonoidalCategory.DayConvolution.convolution F H)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.associator F G H).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.DayConvolution.braiding F
            (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H)).hom
        (CategoryTheory.MonoidalCategory.DayConvolution.associator G H F).hom) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.DayConvolution.map
        (CategoryTheory.MonoidalCategory.DayConvolution.braiding F G).hom (CategoryTheory.CategoryStruct.id H))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.associator G F H).hom
        (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.CategoryStruct.id G)
          (CategoryTheory.MonoidalCategory.DayConvolution.braiding F H).hom))
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.Hom.mk : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {B : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
        {T : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} T] →
            {L : CategoryTheory.Functor A T} →
              {R : CategoryTheory.Functor B T} →
                {P : CategoryTheory.MorphismProperty T} →
                  {Q : CategoryTheory.MorphismProperty A} →
                    {W : CategoryTheory.MorphismProperty B} →
                      {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} →
                        (toCommaMorphism : CategoryTheory.CommaMorphism X.toComma Y.toComma) →
                          Q toCommaMorphism.left → W toCommaMorphism.right → X.Hom Y
-- Init.WF
PSigma.skipLeft : (α : Type u) → {β : Type v} → WellFoundedRelation β → WellFoundedRelation ((_ : α) ×' β)
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.coe_comp_addMonoidHom : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : AddZeroClass α] [inst_4 : AddZeroClass β] [inst_5 : AddZeroClass γ] (f : β →+o γ) (g : α →+o β),
  ↑(f.comp g) = (↑f).comp ↑g
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
/-- A characterisation of the connectedness of the Dynkin diagram for irreducible root pairings.  -/
RootPairing.Base.induction_on_cartanMatrix : ∀ {ι : 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} (b : P.Base)
  [inst_5 : P.IsCrystallographic] [CharZero R] [IsDomain R] [Finite ι] [P.IsReduced] [P.IsIrreducible]
  (p : ↥b.support → Prop) {i j : ↥b.support}, p i → (∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j) → p j
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.extend_coe : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H}, ↑(f.extend I) = ↑I ∘ ↑f
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.toSubgroup'_closure : ∀ {G : Type u_1} [inst : Group G] (S : Set (Additive G)),
  AddSubgroup.toSubgroup' (AddSubgroup.closure S) = Subgroup.closure (⇑Additive.ofMul ⁻¹' S)
-- Std.Time.Time.PlainTime
Std.Time.PlainTime.mk : Std.Time.Hour.Ordinal →
  Std.Time.Minute.Ordinal → Std.Time.Second.Ordinal true → Std.Time.Nanosecond.Ordinal → Std.Time.PlainTime
-- Lean.Server.FileWorker.SemanticHighlighting
Lean.Server.FileWorker.LeanSemanticToken.mk : Lean.Syntax → Lean.Lsp.SemanticTokenType → ℕ → Lean.Server.FileWorker.LeanSemanticToken
-- Mathlib.Analysis.Calculus.Deriv.Mul
DifferentiableAt.div_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_2} [inst_1 : NormedDivisionRing 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {c : 𝕜 → 𝕜'},
  DifferentiableAt 𝕜 c x → ∀ (d : 𝕜'), DifferentiableAt 𝕜 (fun x => c x / d) x
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.instCommRing : CommRing GaussianInt
-- Mathlib.Topology.Order
le_generateFrom : ∀ {α : Type u} {t : TopologicalSpace α} {g : Set (Set α)}, (∀ s ∈ g, IsOpen s) → t ≤ TopologicalSpace.generateFrom g
-- Init.Data.Rat.Lemmas
Rat.lt_iff_sub_pos : ∀ (a b : ℚ), a < b ↔ 0 < b - a
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
/-- Corecursor for `Cofix F`. The shape allows recursive calls to
look like recursive calls.  -/
MvQPF.Cofix.corec₁ : {n : ℕ} →
  {F : TypeVec.{u} (n + 1) → Type u} →
    [q : MvQPF F] →
      {α : TypeVec.{u} n} →
        {β : Type u} → ({X : Type u} → (MvQPF.Cofix F α → X) → (β → X) → β → F (α ::: X)) → β → MvQPF.Cofix F α
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.facets_bot : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E], ⊥.facets = ∅
-- Init.Control.Lawful.MonadLift.Instances
StateRefT'.instLawfulMonadLift : ∀ {ω σ : Type} {m : Type → Type} [inst : Monad m], LawfulMonadLift m (StateRefT' ω σ m)
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.TensorSigns.add_rel : ∀ {I : Type u_7} {inst : AddMonoid I} {c : ComplexShape I} [self : c.TensorSigns] (p q r : I),
  c.Rel p q → c.Rel (r + p) (r + q)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.zpow_eq_empty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : DivisionMonoid α] {s : Finset α} {n : ℤ}, s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0
-- Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso_hom_app_left_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T}
  {R : CategoryTheory.Functor D T} {C' : Type u₄} [inst_3 : CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅}
  [inst_4 : CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T']
  {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'}
  {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F)
  (β : R.comp F ⟶ F₂.comp R') [inst_6 : CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R')
  (X_1 :
    CategoryTheory.Comma (CategoryTheory.StructuredArrow.map₂ (CategoryTheory.CategoryStruct.id (L'.obj X.left)) α)
      (CategoryTheory.StructuredArrow.map₂ X.hom (CategoryTheory.inv β))),
  ((CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso α β X).hom.app X_1).left.right =
    CategoryTheory.CategoryStruct.id X_1.left.right
-- Aesop.Tree.Data
Aesop.MVarClusterData.mk : {Goal Rapp : Type} →
  Option (IO.Ref Rapp) → Array (IO.Ref Goal) → Bool → Aesop.NodeState → Aesop.MVarClusterData Goal Rapp
-- Mathlib.LinearAlgebra.Finsupp.Supported
/-- Interpret `Finsupp.filter s` as a linear map from `α →₀ M` to `supported M R s`.  -/
Finsupp.restrictDom : {α : Type u_1} →
  (M : Type u_2) →
    (R : Type u_5) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            (s : Set α) → [DecidablePred fun x => x ∈ s] → (α →₀ M) →ₗ[R] ↥(Finsupp.supported M R s)
-- Mathlib.Algebra.Group.Equiv.TypeTags
AddEquiv.additiveMultiplicative_apply : ∀ (G : Type u_2) [inst : AddZeroClass G] (a : Additive (Multiplicative G)),
  (AddEquiv.additiveMultiplicative G) a = Multiplicative.toAdd (Additive.toMul a)
-- Mathlib.Topology.Algebra.Monoid
Submonoid.continuousMul : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Monoid M] [ContinuousMul M] (S : Submonoid M), ContinuousMul ↥S
-- Mathlib.Probability.Distributions.Fernique
ProbabilityTheory.Fernique.measure_gt_normThreshold_le_rpow : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [SecondCountableTopology E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {a : ℝ}
  [MeasureTheory.IsProbabilityMeasure μ],
  MeasureTheory.Measure.map (⇑(ContinuousLinearMap.rotation (-(Real.pi / 4)))) (μ.prod μ) = μ.prod μ →
    2⁻¹ < μ {x | ‖x‖ ≤ a} →
      ∀ (n : ℕ),
        μ {x | ProbabilityTheory.Fernique.normThreshold a n < ‖x‖} ≤
          μ {x | ‖x‖ ≤ a} * ((1 - μ {x | ‖x‖ ≤ a}) / μ {x | ‖x‖ ≤ a}) ^ 2 ^ n
-- Lean.CoreM
/-- Info tree. We have the info tree here because we want to update it while adding attributes.  -/
Lean.Core.State.infoState : Lean.Core.State → Lean.Elab.InfoState
-- Init.Core
le_of_eq_of_le : ∀ {α : Type u_1} {a b c : α} [inst : LE α], a = b → b ≤ c → a ≤ c
-- Mathlib.Algebra.Group.Hom.Instances
instIsLeftCancelMulOneHom : ∀ {M : Type uM} {N : Type uN} [inst : One M] [inst_1 : MulOneClass N] [IsLeftCancelMul N], IsLeftCancelMul (OneHom M N)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rco_eq_append : ∀ {m n : ℕ}, m < n → (m...n).toList = (m...n - 1).toList ++ [n - 1]
-- Mathlib.ModelTheory.PartialEquiv
/-- The substructure which is the domain of the equivalence.  -/
FirstOrder.Language.PartialEquiv.dom : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type w'} → [inst : L.Structure M] → [inst_1 : L.Structure N] → L.PartialEquiv M N → L.Substructure M
-- Mathlib.Tactic.Abel
_private.Mathlib.Tactic.Abel.0.Mathlib.Tactic.Abel.instEvalExprAbelMode.evalExpr : Lean.Expr → Lean.MetaM Mathlib.Tactic.Abel.AbelMode
-- Mathlib.CategoryTheory.Groupoid
CategoryTheory.instIsGroupoidDiscrete : ∀ {I : Type u_1}, CategoryTheory.IsGroupoid (CategoryTheory.Discrete I)
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.colimitCoyonedaHomIsoLimitLeftOp_π_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (D : CategoryTheory.Functor I Cᵒᵖ) (F : CategoryTheory.Functor C (Type u₂))
  [inst_2 : CategoryTheory.Limits.HasColimit (D.comp CategoryTheory.coyoneda)]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))]
  (f : CategoryTheory.Limits.colimit (D.comp CategoryTheory.coyoneda) ⟶ F) (i : I),
  (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.Limits.limit.π (D.leftOp.comp (F.comp CategoryTheory.uliftFunctor.{u₁, u₂})) (Opposite.op i)))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimitCoyonedaHomIsoLimitLeftOp D F).hom) f) =
    {
      down :=
        (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.unop (D.obj i))))
          ((CategoryTheory.ConcreteCategory.hom
              ((CategoryTheory.Limits.colimit.ι (D.comp CategoryTheory.coyoneda) i).app (Opposite.unop (D.obj i))))
            (CategoryTheory.CategoryStruct.id (Opposite.unop (D.obj i)))) }
-- Init.Notation
/-- Auxiliary type used to represent syntax categories. We mainly use auxiliary
definitions with this type to attach doc strings to syntax categories.
 -/
Lean.Parser.Category : Type
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Real.norm_exp_I_mul_ofReal_sub_one_le : ∀ {x : ℝ}, ‖Complex.exp (Complex.I * ↑x) - 1‖ ≤ ‖x‖
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.isPrincipal_mul_omega0_opow_opow : ∀ (o : Ordinal.{u_1}), Ordinal.IsPrincipal (fun x1 x2 => x1 * x2) (Ordinal.omega0 ^ Ordinal.omega0 ^ o)