mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.Products.prop_of_isGood_of_contained : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I]
  {l : Profinite.NobelingProof.Products I} (o : Ordinal.{u}),
  Profinite.NobelingProof.Products.isGood C l →
    Profinite.NobelingProof.contained C o → ∀ i ∈ ↑l, Profinite.NobelingProof.ord I i < o
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
/-- If `K` is a compact set in an R₁ space and `s ⊇ K` is a Borel measurable superset,
then `s` includes the closure of `K` as well.  -/
IsCompact.closure_subset_measurableSet : ∀ {γ : Type u_3} [inst : TopologicalSpace γ] [inst_1 : MeasurableSpace γ] [BorelSpace γ] [R1Space γ] {K s : Set γ},
  IsCompact K → MeasurableSet s → K ⊆ s → closure K ⊆ s
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.gc : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  GaloisConnection (Algebra.adjoin R) SetLike.coe
-- Mathlib.Order.Filter.Basic
Filter.NeBot.nonempty_of_mem : ∀ {α : Type u} {f : Filter α}, f.NeBot → ∀ {s : Set α}, s ∈ f → s.Nonempty
-- Mathlib.Tactic.Push.Attr
Mathlib.Tactic.Push.instToStringHead : ToString Mathlib.Tactic.Push.Head
-- Mathlib.Probability.Process.Predictable
/-- **Alias** of `MeasureTheory.IsStronglyPredictable.iff_measurable_add_one`.

---

A discrete process `u` is predictable iff `u (n + 1)` is `𝓕 n`-measurable for all `n` and
`u 0` is `𝓕 0`-measurable.  -/
MeasureTheory.IsPredictable.iff_measurable_add_one : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {E : Type u_3} [inst : TopologicalSpace E] {𝓕 : MeasureTheory.Filtration ℕ m}
  {u : ℕ → Ω → E},
  MeasureTheory.IsStronglyPredictable 𝓕 u ↔
    MeasureTheory.StronglyMeasurable (u 0) ∧ ∀ (n : ℕ), MeasureTheory.StronglyMeasurable (u (n + 1))
-- Init.Data.Iterators.Consumers.Monadic.Partial
Std.IterM.Partial.mk : {α : Type w} → {m : Type w → Type w'} → {β : Type w} → Std.IterM m β → Std.IterM.Partial m β
-- Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
CategoryTheory.ObjectProperty.instAdditiveLocalizedFunctorFullSubcategoryTrWInverseImageιTriangulatedLocalizerMorphism : ∀ {C : Type u_1} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} D₁] [inst_2 : CategoryTheory.Category.{v_4, u_4} D₂]
  (A B : CategoryTheory.ObjectProperty C) [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  [inst_4 : CategoryTheory.HasShift C ℤ] [inst_5 : CategoryTheory.Preadditive C]
  [inst_6 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_7 : CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C] [inst_9 : A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms]
  (L₁ : CategoryTheory.Functor A.FullSubcategory D₁) (L₂ : CategoryTheory.Functor C D₂)
  [inst_12 : L₁.IsLocalization (B.inverseImage A.ι).trW] [inst_13 : L₂.IsLocalization B.trW]
  [inst_14 : CategoryTheory.Preadditive D₁] [inst_15 : CategoryTheory.Preadditive D₂] [L₁.Additive] [L₂.Additive],
  ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Additive
-- Mathlib.Topology.Sheaves.Points
Opens.instIsThinPointOpensGrothendieckTopology : ∀ {X : Type u} [inst : TopologicalSpace X], Quiver.IsThin (Opens.grothendieckTopology X).Point
-- Mathlib.NumberTheory.Real.GoldenRatio
/-- As expected, the Fibonacci sequence is a solution of `fibRec`.  -/
Real.fib_isSol_fibRec : ∀ {α : Type u_1} [inst : CommSemiring α], Real.fibRec.IsSolution fun x => ↑(Nat.fib x)
-- Mathlib.Data.ZMod.Basic
ZMod.inv_one : ∀ (n : ℕ), 1⁻¹ = 1
-- Mathlib.Algebra.Symmetrized
SymAlg.sym_inv : ∀ {α : Type u_1} [inst : Inv α] (a : α), SymAlg.sym a⁻¹ = (SymAlg.sym a)⁻¹
-- Mathlib.Data.Finsupp.Weight
Finsupp.finite_of_nat_weight_eq : ∀ {σ : Type u_1} [Finite σ] (w : σ → ℕ), (∀ (x : σ), w x ≠ 0) → ∀ (n : ℕ), {d | (Finsupp.weight w) d = n}.Finite
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.AttrKind.norm.inj : ∀ {post inv post_1 inv_1 : Bool},
  Lean.Meta.Grind.AttrKind.norm post inv = Lean.Meta.Grind.AttrKind.norm post_1 inv_1 → post = post_1 ∧ inv = inv_1
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.mk.sizeOf_spec : ∀ {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} (map : X ⟶ Y)
  (comm :
    autoParam (CategoryTheory.CategoryStruct.comp A.ι map = CategoryTheory.CategoryStruct.comp φ B.ι)
      SSet.RelativeMorphism.comm._autoParam),
  sizeOf { map := map, comm := comm } = 1 + sizeOf map + sizeOf comm
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.isEmpty_inter_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → m₂.isEmpty = true → (m₁ ∩ m₂).isEmpty = true
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₃_app_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D}
  (μ : CategoryTheory.MonoidalCategory.curriedTensorPre F ⟶ CategoryTheory.MonoidalCategory.curriedTensorPost F)
  (X₁ X₂ X₃ : C),
  (((CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₃ μ).app X₁).app X₂).app X₃ =
    (μ.app X₁).app (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ X₃)
-- Mathlib.Data.Set.Finite.Lattice
Set.Finite.iInf_biSup_of_monotone : ∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [inst : Preorder ι'] [Nonempty ι'] [IsCodirectedOrder ι']
  [inst_3 : Order.Coframe α] {s : Set ι},
  s.Finite → ∀ {f : ι → ι' → α}, (∀ i ∈ s, Monotone (f i)) → ⨅ j, ⨆ i ∈ s, f i j = ⨆ i ∈ s, ⨅ j, f i j
-- Lean.Environment
Lean.AsyncBranch.noConfusionType : Sort v✝ → Lean.AsyncBranch → Lean.AsyncBranch → Sort v✝
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.stepAux.eq_def : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Inhabited Γ] (x : Turing.TM1.Stmt Γ Λ σ) (x_1 : σ)
  (x_2 : Turing.Tape Γ),
  Turing.TM1.stepAux x x_1 x_2 =
    match x, x_1, x_2 with
    | Turing.TM1.Stmt.move d q, v, T => Turing.TM1.stepAux q v (Turing.Tape.move d T)
    | Turing.TM1.Stmt.write a q, v, T => Turing.TM1.stepAux q v (Turing.Tape.write (a T.head v) T)
    | Turing.TM1.Stmt.load s q, v, T => Turing.TM1.stepAux q (s T.head v) T
    | Turing.TM1.Stmt.branch p q₁ q₂, v, T =>
      bif p T.head v then Turing.TM1.stepAux q₁ v T else Turing.TM1.stepAux q₂ v T
    | Turing.TM1.Stmt.goto l, v, T => { l := some (l T.head v), var := v, Tape := T }
    | Turing.TM1.Stmt.halt, v, T => { l := none, var := v, Tape := T }
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray.folder : {n : ℕ} →
  Option (Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool) →
    Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) →
      Option (Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.Presentation.mapRelations_mapGenerators_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C']
  {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat}
  [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat]
  {M : SheafOfModules R} (P : M.Presentation) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S))
  [inst_6 :
    CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁,
        max (max (u + 1) u₂) v₂}
      F]
  (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) {Z : SheafOfModules S} (h : F.obj M ⟶ Z),
  CategoryTheory.CategoryStruct.comp (P.mapRelations F η) (CategoryTheory.CategoryStruct.comp (P.mapGenerators F η) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Data.Seq.Basic
Stream'.Seq.zipWith_nil_left : ∀ {α : Type u} {β : Type v} {γ : Type w} {f : α → β → γ} {s : Stream'.Seq β},
  Stream'.Seq.zipWith f Stream'.Seq.nil s = Stream'.Seq.nil
-- Mathlib.Data.Set.Finite.Lemmas
Set.sUnion_finite_eq_univ : ∀ {X : Type u_1}, ⋃₀ {s | s.Finite} = Set.univ
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
/-- Structure expressing that a morphism `f : X ⟶ Y` in a category `C`
is a transfinite composition of shape `J` of morphisms in `W : MorphismProperty C`.  -/
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.MorphismProperty C →
      (J : Type w) →
        [inst_1 : LinearOrder J] →
          [SuccOrder J] → [OrderBot J] → [WellFoundedLT J] → {X Y : C} → (X ⟶ Y) → Type (max (max u v) w)
-- Mathlib.Analysis.Distribution.Support
Distribution.not_isVanishingOn_mono : ∀ {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [inst : FunLike F α β] [inst_1 : TopologicalSpace α]
  [inst_2 : Zero β] {f : F → V} [inst_3 : Zero V] ⦃s₁ s₂ : Set α⦄,
  s₁ ⊆ s₂ → ¬Distribution.IsVanishingOn f s₁ → ¬Distribution.IsVanishingOn f s₂
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionLiteralSupportValueSet.mk.injEq : ∀ (valueSet valueSet_1 : Array Lean.Lsp.CodeActionKind),
  ({ valueSet := valueSet } = { valueSet := valueSet_1 }) = (valueSet = valueSet_1)
-- Mathlib.Combinatorics.Matroid.Circuit
/-- The strong isCircuit elimination axiom. For any pair of distinct circuits `C₁, C₂` and all
`e ∈ C₁ ∩ C₂` and `f ∈ C₁ \ C₂`, there is a circuit `C` with `f ∈ C ⊆ (C₁ ∪ C₂) \ {e}`.  -/
Matroid.IsCircuit.strong_elimination : ∀ {α : Type u_1} {M : Matroid α} {e f : α} {C₁ C₂ : Set α},
  M.IsCircuit C₁ → M.IsCircuit C₂ → e ∈ C₁ → e ∈ C₂ → f ∈ C₁ → f ∉ C₂ → ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C ∧ f ∈ C
-- Mathlib.Algebra.Order.Interval.Set.Monoid
Set.Icc_add_bij : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M]
  (a b d : M), Set.BijOn (fun x => x + d) (Set.Icc a b) (Set.Icc (a + d) (b + d))
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.π_comp_H0Iso_hom_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : (Rep.coinvariantsFunctor k G).obj A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.π A 0)
      (CategoryTheory.CategoryStruct.comp (groupHomology.H0Iso A).hom h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.cyclesIso₀ A).hom
      (CategoryTheory.CategoryStruct.comp ((Rep.coinvariantsMk k G).app A) h)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.contains_insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List α} {k : α},
      (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).contains k = (m.contains k || l.contains k)
-- Mathlib.Topology.ContinuousMap.Defs
ContinuousMap.mk.injEq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (toFun : X → Y)
  (continuous_toFun : autoParam (Continuous toFun) ContinuousMap.continuous_toFun._autoParam) (toFun_1 : X → Y)
  (continuous_toFun_1 : autoParam (Continuous toFun_1) ContinuousMap.continuous_toFun._autoParam),
  ({ toFun := toFun, continuous_toFun := continuous_toFun } =
      { toFun := toFun_1, continuous_toFun := continuous_toFun_1 }) =
    (toFun = toFun_1)
-- Lean.Elab.Tactic.Omega.OmegaM
/-- Run an `OmegaM` computation, restoring the state afterwards depending on the result.  -/
Lean.Elab.Tactic.Omega.commitWhen : {α : Type} → Lean.Elab.Tactic.Omega.OmegaM (α × Bool) → Lean.Elab.Tactic.Omega.OmegaM α
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.mem_union_of_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, k ∈ m₂ → k ∈ m₁ ∪ m₂
-- Mathlib.GroupTheory.Coset.Basic
/-- `α ⧸ ⊥` is in bijection with `α`. See `QuotientGroup.quotientBot` for a multiplicative
version.  -/
QuotientGroup.quotientEquivSelf : (α : Type u_1) → [inst : Group α] → α ⧸ ⊥ ≃ α
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.toImage_ι : ∀ {X Y : SSet} (A : X.Subcomplex) (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (A.toImage f) (A.image f).ι = CategoryTheory.CategoryStruct.comp A.ι f
-- Lean.PrettyPrinter.Delaborator.Basic
_private.Lean.PrettyPrinter.Delaborator.Basic.0.Lean.PrettyPrinter.Delaborator.getUnusedName.bodyUsesSuggestion : Lean.Expr → Lean.LocalContext → Lean.Name → Bool
-- Mathlib.NumberTheory.Chebyshev
/-- Bound on the integral in `Chebyshev.primeCounting_eq_theta_div_log_add_integral`.  -/
Chebyshev.integral_theta_div_log_sq_isBigO : (fun x => ∫ (t : ℝ) in 2..x, Chebyshev.theta t / (t * Real.log t ^ 2)) =O[Filter.atTop] fun x => x / Real.log x ^ 2
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt.0.UInt16.fromExpr : Lean.Expr → Lean.Meta.SimpM (Option UInt16)
-- Std.Data.DTreeMap.Internal.Def
Std.DTreeMap.Internal.Impl.inner.injEq : ∀ {α : Type u} {β : α → Type v} (size : ℕ) (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β) (size_1 : ℕ)
  (k_1 : α) (v_1 : β k_1) (l_1 r_1 : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k v l r = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1) =
    (size = size_1 ∧ k = k_1 ∧ v ≍ v_1 ∧ l = l_1 ∧ r = r_1)
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.right_quotientAction' : ∀ {G : Type u} [inst : AddGroup G] (H : AddSubgroup G) [hH : H.Normal], AddAction.QuotientAction Gᵃᵒᵖ H
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.Pushforward.comp_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z)
  (ℱ : TopCat.Presheaf C X),
  (TopCat.Presheaf.pushforward C (CategoryTheory.CategoryStruct.comp f g)).obj ℱ =
    (TopCat.Presheaf.pushforward C g).obj ((TopCat.Presheaf.pushforward C f).obj ℱ)
-- Mathlib.Analysis.Normed.Group.Real
instENormENNReal : ENorm ENNReal
-- Init.Data.SInt.Bitwise
Int8.and_neg_one : ∀ {a : Int8}, a &&& -1 = a
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
/-- The image of a set `s` under a continuous linear equiv `f` has measure
equal to `μ s` times the absolute value of the determinant of `f`.  -/
MeasureTheory.Measure.addHaar_image_continuousLinearEquiv : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (f : E ≃L[ℝ] E) (s : Set E),
  μ (⇑f '' s) = ENNReal.ofReal |LinearMap.det ↑↑f| * μ s
-- Mathlib.Algebra.Group.Basic
mul_left_comm : ∀ {G : Type u_3} [inst : CommSemigroup G] (a b c : G), a * (b * c) = b * (a * c)
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.corootSpan_map_flip_toPerfPair : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [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),
  Submodule.map (↑P.flip.toPerfPair) (P.corootSpan R) = Submodule.span R (Set.range P.coroot')
-- Mathlib.Data.Nat.PSub
Nat.psub'.eq_1 : ∀ (m n : ℕ), m.psub' n = if n ≤ m then some (m - n) else none
-- Mathlib.Topology.Bornology.Absorbs
Absorbs.mono : ∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s₁ s₂ t₁ t₂ : Set α},
  Absorbs M s₁ t₁ → s₁ ⊆ s₂ → t₂ ⊆ t₁ → Absorbs M s₂ t₂
-- Mathlib.Algebra.Ring.GeomSum
Commute.geom_sum₂_succ_eq : ∀ {R : Type u_1} [inst : Ring R] {x y : R},
  Commute x y →
    ∀ {n : ℕ},
      ∑ i ∈ Finset.range (n + 1), x ^ i * y ^ (n - i) = x ^ n + y * ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)
-- Mathlib.RingTheory.Flat.Rank
RingHom.finrank_comp_left_of_bijective : ∀ {R : Type u_3} {S : Type u_4} {T : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  (f : R →+* S) (g : S →+* T),
  Function.Bijective ⇑g → f.Finite → f.Flat → ∀ (x : PrimeSpectrum R), (g.comp f).finrank x = f.finrank x
-- Mathlib.Algebra.Ring.TransferInstance
/-- Transfer `AddGroupWithOne` across an `Equiv`  -/
Equiv.addGroupWithOne : {α : Type u_1} → {β : Type u_2} → α ≃ β → [AddGroupWithOne β] → AddGroupWithOne α
-- Mathlib.Analysis.Convex.Topology
closedConvexHull_isClosed : ∀ (𝕜 : Type u_2) {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] (s : Set E),
  (closedConvexHull 𝕜).IsClosed s = (Convex 𝕜 s ∧ IsClosed s)
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_embedding_eq_arrow_of_lift_le : ∀ {α : Type u} {β' : Type v} [Infinite α],
  Cardinal.lift.{u, v} (Cardinal.mk β') ≤ Cardinal.lift.{v, u} (Cardinal.mk α) →
    Cardinal.mk (β' ↪ α) = Cardinal.mk (β' → α)
-- Mathlib.Algebra.Module.Torsion.Basic
/-- The additive `n`-torsion subgroup for an integer `n`, denoted as `A[n]`.  -/
AddSubgroup.torsionBy : (A : Type u_3) → [inst : AddCommGroup A] → ℤ → AddSubgroup A
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.map.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} {T : Submonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T)
  {Q : Type u_4} [inst_3 : CommMonoid Q] (k : T.LocalizationMap Q), f.map hy k = f.lift ⋯
-- Mathlib.Analysis.InnerProductSpace.GramMatrix
/-- In a normed space, linear independence of `v` is equivalent to positive definiteness of
`gram 𝕜 v`.  -/
Matrix.posDef_gram_iff_linearIndependent : ∀ {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [Finite n] {v : n → E}, (Matrix.gram 𝕜 v).PosDef ↔ LinearIndependent 𝕜 v
-- Mathlib.Algebra.Order.GroupWithZero.Basic
le_div_comm₀ : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀},
  0 < a → 0 < c → (a ≤ b / c ↔ c ≤ b / a)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.tensorObj_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G H : CategoryTheory.AddGrp C),
  CategoryTheory.AddMonObj.zero = CategoryTheory.AddMonObj.zero
-- Mathlib.Algebra.Ring.Subring.Basic
RingHom.eq_of_eqOn_set_top : ∀ {R : Type u} [inst : NonAssocRing R] {S : Type v} [inst_1 : Semiring S] {f g : R →+* S}, Set.EqOn ⇑f ⇑g ↑⊤ → f = g
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_filter!_of_getKey?_eq_some : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  {f : α → β → Bool} {k k' : α},
  t.WF →
    t.getKey? k = some k' →
      Std.DTreeMap.Internal.Impl.Const.get? (Std.DTreeMap.Internal.Impl.filter! f t) k =
        Option.filter (fun x => f k' x) (Std.DTreeMap.Internal.Impl.Const.get? t k)
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.maxKey? : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → Option α
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.congr_fun : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f g : α →ᵈ β},
  f = g → ∀ (x : α), f x = g x
-- Lean.Elab.Do.Basic
/-- Whether we are OK with generating the code of the continuation multiple times, e.g. in different
branches of a `match` or `if`.
 -/
Lean.Elab.Do.DoElemCont.kind : Lean.Elab.Do.DoElemCont → Lean.Elab.Do.DoElemContKind
-- Mathlib.Data.Fin.Fin2
/-- Use type class inference to infer the boundedness proof, so that we can directly convert a
`Nat` into a `Fin2 n`. This supports notation like `&1 : Fin 3`.  -/
_private.Mathlib.Data.Fin.Fin2.0.Fin2.«term&_» : Lean.ParserDescr
-- Lean.Parser.Syntax
Lean.Parser.Command.notation.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.polarSpaceCoord.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.polarSpaceCoord K = NumberField.mixedEmbedding.polarSpaceCoord K
-- Mathlib.GroupTheory.QuotientGroup.Defs
AddSubgroup.orderIsoAddCon.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G],
  AddSubgroup.orderIsoAddCon =
    { toFun := fun N => QuotientAddGroup.con ↑N, invFun := fun c => ⟨c.addSubgroup, ⋯⟩, left_inv := ⋯, right_inv := ⋯,
      map_rel_iff' := ⋯ }
-- Mathlib.Topology.ContinuousMap.Algebra
MonoidHom.compLeftContinuous_apply : ∀ (α : Type u_1) {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {γ : Type u_3}
  [inst_2 : Monoid β] [inst_3 : ContinuousMul β] [inst_4 : TopologicalSpace γ] [inst_5 : Monoid γ]
  [inst_6 : ContinuousMul γ] (g : β →* γ) (hg : Continuous ⇑g) (f : C(α, β)),
  (MonoidHom.compLeftContinuous α g hg) f = { toFun := ⇑g, continuous_toFun := hg }.comp f
-- Aesop.Tree.Data
Aesop.RappData.mk : {Goal MVarCluster : Type} →
  Aesop.RappId →
    IO.Ref Goal →
      Array (IO.Ref MVarCluster) →
        Aesop.NodeState →
          Bool →
            Aesop.RegularRule →
              Option (Array Aesop.Script.LazyStep) →
                Array Lean.MVarId →
                  Aesop.Percent →
                    Lean.Meta.SavedState →
                      Aesop.UnorderedArraySet Lean.MVarId →
                        Aesop.UnorderedArraySet Lean.MVarId → Aesop.RappData Goal MVarCluster
-- Mathlib.RingTheory.Norm.Transitivity
Algebra.Norm.Transitivity.cornerAddX.eq_1 : ∀ {S : Type u_2} {m : Type u_5} [inst : CommRing S] (M : Matrix m m S) [inst_1 : DecidableEq m] (k : m),
  Algebra.Norm.Transitivity.cornerAddX M k =
    (Matrix.diagonal fun i => if i = k then Polynomial.X else 0) + M.map ⇑Polynomial.C
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
/-- A star `R`-algebra `A` has a *continuous functional calculus* for elements satisfying the
property `p : A → Prop` if

+ for every such element `a : A` there is a star algebra homomorphism
  `cfcHom : C(spectrum R a, R) →⋆ₐ[R] A` sending the (restriction of) the identity map to `a`.
+ `cfcHom` is continuous and injective and the spectrum of the image of function `f` is its range.
+ `cfcHom` preserves the property `p`.
+ `p 0` is true, which ensures among other things that `p ≠ fun _ ↦ False`.

The property `p` is marked as an `outParam` so that the user need not specify it. In practice,

+ for `R := ℂ`, we choose `p := IsStarNormal`,
+ for `R := ℝ`, we choose `p := IsSelfAdjoint`,
+ for `R := ℝ≥0`, we choose `p := (0 ≤ ·)`.

Instead of directly providing the data we opt instead for a `Prop` class. In all relevant cases,
the continuous functional calculus is uniquely determined, and utilizing this approach
prevents diamonds or problems arising from multiple instances.  -/
ContinuousFunctionalCalculus : (R : Type u_1) →
  (A : Type u_2) →
    outParam (A → Prop) →
      [inst : CommSemiring R] →
        [inst_1 : StarRing R] →
          [inst_2 : MetricSpace R] →
            [IsTopologicalSemiring R] →
              [ContinuousStar R] → [inst_5 : Ring A] → [StarRing A] → [TopologicalSpace A] → [Algebra R A] → Prop
-- Mathlib.RingTheory.Ideal.Quotient.Defs
/-- If `I` is an ideal of a commutative ring `R`, if `q : R → R/I` is the quotient map, and if
`s ⊆ R` is a subset, then `q⁻¹(q(s)) = ⋃ᵢ(i + s)`, the union running over all `i ∈ I`.  -/
Ideal.Quotient.quotient_ring_saturate : ∀ {R : Type u} [inst : Ring R] {I : Ideal R} [inst_1 : I.IsTwoSided] (s : Set R),
  ⇑(Ideal.Quotient.mk I) ⁻¹' ⇑(Ideal.Quotient.mk I) '' s = ⋃ x, (fun y => ↑x + y) '' s
-- Mathlib.Data.Int.WithZero
WithZeroMulInt.toNNReal_neg_apply : ∀ {e : NNReal} (he : e ≠ 0) {x : WithZero (Multiplicative ℤ)} (hx : x ≠ 0),
  (WithZeroMulInt.toNNReal he) x = e ^ Multiplicative.toAdd (WithZero.unzero hx)