mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Constructions
continuous_ofMul : ∀ {X : Type u} [inst : TopologicalSpace X], Continuous ⇑Additive.ofMul
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.val_toRootsOfUnity_coe : ∀ {M : Type u_1} [inst : CommMonoid M] {μ : M} {n : ℕ} [inst_1 : NeZero n] (h : IsPrimitiveRoot μ n),
  ↑↑h.toRootsOfUnity = μ
-- Std.Http.Protocol.H1.Writer
Std.Http.Protocol.H1.Writer.State.waitingForFlush.sizeOf_spec : sizeOf Std.Http.Protocol.H1.Writer.State.waitingForFlush = 1
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)} {k fallback : α},
  (List.map Sigma.fst l).contains k = false → (m.insertMany l).getKeyD k fallback = m.getKeyD k fallback
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.tsum_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [T2Space β]
  [inst_3 : AddCommMonoid β] [inst_4 : ContinuousAdd β] {γ : Type u_3} {f : γ → C(α, β)} {L : SummationFilter γ},
  Summable f L → ∀ [L.NeBot] (x : α), ∑'[L] (i : γ), (f i) x = (∑'[L] (i : γ), f i) x
-- Mathlib.Data.EReal.Basic
EReal.coe_ennreal_eq_one : ∀ {x : ENNReal}, ↑x = 1 ↔ x = 1
-- Mathlib.Algebra.Lie.Semisimple.Defs
LieAlgebra.IsSimple.non_abelian : ∀ (R : Type u_1) {L : Type u_2} {inst : CommRing R} {inst_1 : LieRing L} {inst_2 : LieAlgebra R L}
  [self : LieAlgebra.IsSimple R L], ¬IsLieAbelian L
-- Mathlib.Analysis.Calculus.Deriv.Inverse
HasDerivAt.hasFDerivAt_equiv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {f' x : 𝕜},
  HasDerivAt f f' x → ∀ (hf' : f' ≠ 0), HasFDerivAt f (↑((ContinuousLinearEquiv.unitsEquivAut 𝕜) (Units.mk0 f' hf'))) x
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Ioi_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a : α} (b : ↑(Set.Ioi a)), Subtype.val '' Set.Ioi b = Set.Ioi ↑b
-- Mathlib.GroupTheory.Subgroup.Centralizer
/-- The conjugation action of `N(H)` on `H`.  -/
Subgroup.instMulDistribMulActionSubtypeMemNormalizerCoe : {G : Type u_1} → [inst : Group G] → (H : Subgroup G) → MulDistribMulAction ↥(Subgroup.normalizer ↑H) ↥H
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnitInvariant_insertUnit : ∀ {n : ℕ} (assignments0 : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment)
  (assignments0_size : assignments0.size = n)
  (units : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)))
  (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (assignments_size : assignments.size = n)
  (foundContradiction : Bool) (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.InsertUnitInvariant assignments0 assignments0_size units assignments
      assignments_size →
    let update_res :=
      Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit (units, assignments, foundContradiction) l;
    have update_res_size := ⋯;
    Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.InsertUnitInvariant assignments0 assignments0_size update_res.1
      update_res.2.1 update_res_size
-- Mathlib.CategoryTheory.MorphismProperty.Retract
CategoryTheory.MorphismProperty.IsStableUnderRetracts.of_retract : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C}
  [self : P.IsStableUnderRetracts] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : CategoryTheory.RetractArrow f g),
  P g → P f
-- Lean.Elab.Tactic.BuiltinTactic
_private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven : Lean.Syntax → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.measurable_uncurry_gaussianPDF : Measurable fun x =>
  match x with
  | (μ, v, x) => ProbabilityTheory.gaussianPDF μ v x
-- Mathlib.ModelTheory.Order
FirstOrder.Language.Term.realize_lt : ∀ {L : FirstOrder.Language} {α : Type w} {M : Type w'} {n : ℕ} [inst : L.IsOrdered] [inst_1 : L.Structure M]
  [inst_2 : Preorder M] [L.OrderedStructure M] {t₁ t₂ : L.Term (α ⊕ Fin n)} {v : α → M} {xs : Fin n → M},
  (t₁.lt t₂).Realize v xs ↔
    FirstOrder.Language.Term.realize (Sum.elim v xs) t₁ < FirstOrder.Language.Term.realize (Sum.elim v xs) t₂
-- Mathlib.NumberTheory.FrobeniusNumber
/-- `ℕ` is a Noetherian `ℕ`-module, i.e., `ℕ` is a Noetherian semiring.  -/
Nat.instIsNoetherian : IsNoetherian ℕ ℕ
-- Init.Core
PULift.up.injEq : ∀ {α : Sort s} (down down_1 : α), ({ down := down } = { down := down_1 }) = (down = down_1)
-- Mathlib.Analysis.Real.Sqrt
Real.lt_sqrt_of_sq_lt : ∀ {x y : ℝ}, x ^ 2 < y → x < √y
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.del : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.FVarId →
    autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_15 →
      Lean.Compiler.LCNF.CodeDecl pu
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.map_b₄ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) {A : Type v} [inst_1 : CommRing A] (f : R →+* A),
  (W.map f).b₄ = f W.b₄
-- Mathlib.FieldTheory.AbelRuffini
IsSolvableByRad.base : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (α : F),
  IsSolvableByRad F ((algebraMap F E) α)
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.prod_Ioi_mul_eq_prod_Ici : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] {f : α → M} [inst_1 : PartialOrder α]
  [inst_2 : LocallyFiniteOrderTop α] (a : α), (∏ x > a, f x) * f a = ∏ x ≥ a, f x
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.takeUntil_first : ∀ {V : Type u} {G : SimpleGraph V} {v u : V} [inst : DecidableEq V] (p : G.Walk u v),
  p.takeUntil u ⋯ = SimpleGraph.Walk.nil
-- Mathlib.Order.Interval.Set.Disjoint
Set.iUnion_Ico_right : ∀ {α : Type v} [inst : Preorder α] [NoMaxOrder α] (a : α), ⋃ b, Set.Ico a b = Set.Ici a
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.copy_eq : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (V'' : Set V) (hV : V'' = G'.verts) (adj' : V → V → Prop)
  (hadj : adj' = G'.Adj), G'.copy V'' hV adj' hadj = G'
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.costructuredArrowMapCocone_pt : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor D H) (α : F ⟶ L.comp G)
  (Y : D), (L.costructuredArrowMapCocone F G α Y).pt = G.obj Y
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.leftUnitor_hom_apply : ∀ {X : TopCat} {x : ↑X} {p : PUnit.{u + 1}},
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom) (p, x) = x
-- Mathlib.LinearAlgebra.Center
/-- A linear endomorphism of a free module of rank at least 2
that commutes with transvections consists of homotheties with central ratio.  -/
LinearMap.commute_transvections_iff_of_basis : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {ι : Type u_3}
  [Nontrivial ι] (b : Module.Basis ι R V) {f : V →ₗ[R] V},
  (∀ (i j : ι) (r : R), i ≠ j → Commute f ((b.coord i).transvection (r • b j))) → ∃ a, f = a • 1
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- Construct a context from a lean expression for a 2-morphism.  -/
Mathlib.Tactic.BicategoryLike.mkContext : {ρ : Type} → [Mathlib.Tactic.BicategoryLike.Context ρ] → Lean.Expr → Lean.MetaM ρ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.forIn_eq_forIn : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Std.TransCmp cmp] [inst_1 : Monad m] [inst_2 : LawfulMonad m] {f : α → β → δ → m (ForInStep δ)} {init : δ},
  Std.ExtTreeMap.forIn f init t = forIn t init fun a d => f a.1 a.2 d
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.instInsertOfBEqOfHashable : {α : Type u} → [BEq α] → [Hashable α] → Insert α (Std.HashSet.Raw α)
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.inv_smul_mem_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : Group α] [inst_2 : MulAction α β] {s : Finset β}
  {a : α} {b : β}, a⁻¹ • b ∈ s ↔ b ∈ a • s
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Functor.Monoidal.lift_μ_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) {X Y Z : C} [inst_4 : F.Monoidal] (f : X ⟶ Y) (g : X ⟶ Z) {Z_1 : D}
  (h : F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (F.map f) (F.map g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F Y Z) h) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CartesianMonoidalCategory.lift f g)) h
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.lift_lt_continuum : ∀ {c : Cardinal.{u}}, Cardinal.lift.{v, u} c < Cardinal.continuum ↔ c < Cardinal.continuum
-- Init.Data.Array.Lemmas
Array.mem_of_contains_eq_true : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {as : Array α}, as.contains a = true → a ∈ as
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
_private.Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis.0.Tactic.ComputeAsymptotics.BasisExtension.getBasis.match_1.splitter : (motive : (basis : Tactic.ComputeAsymptotics.Basis) → Tactic.ComputeAsymptotics.BasisExtension basis → Sort u_1) →
  (basis : Tactic.ComputeAsymptotics.Basis) →
    (ex : Tactic.ComputeAsymptotics.BasisExtension basis) →
      (Unit → motive [] Tactic.ComputeAsymptotics.BasisExtension.nil) →
        ((basis_hd : ℝ → ℝ) →
            (basis_tl : Tactic.ComputeAsymptotics.Basis) →
              (ex : Tactic.ComputeAsymptotics.BasisExtension basis_tl) →
                motive (basis_hd :: basis_tl) (Tactic.ComputeAsymptotics.BasisExtension.keep basis_hd ex)) →
          ((basis : Tactic.ComputeAsymptotics.Basis) →
              (f : ℝ → ℝ) →
                (ex : Tactic.ComputeAsymptotics.BasisExtension basis) →
                  motive basis (Tactic.ComputeAsymptotics.BasisExtension.insert f ex)) →
            motive basis ex
-- Mathlib.Algebra.Tropical.BigOperators
untrop_sum : ∀ {R : Type u_1} {S : Type u_2} [inst : ConditionallyCompleteLinearOrder R] [inst_1 : Fintype S]
  (f : S → Tropical (WithTop R)), Tropical.untrop (∑ i, f i) = ⨅ i, Tropical.untrop (f i)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {c : ℕ}, (Std.DHashMap.emptyWithCapacity c).size = 0
-- Mathlib.Logic.Relation
Relation.symmGen_comm : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α}, Relation.SymmGen r a b ↔ Relation.SymmGen r b a
-- Mathlib.Order.Monotone.Monovary
StrictMonoOn.trans_antivaryOn : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  {s : Set ι} [inst_2 : PartialOrder ι], StrictMonoOn f s → AntivaryOn g f s → AntitoneOn g s
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.Hom.ker_comp_of_isIso : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso f],
  AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.CategoryStruct.comp f g) = AlgebraicGeometry.Scheme.Hom.ker g
-- Mathlib.Dynamics.Ergodic.Conservative
/-- If `f` is a conservative self-map and `s` is a measurable set of nonzero measure,
then there exists a point `x ∈ s` that returns to `s` under a non-zero iteration of `f`.  -/
MeasureTheory.Conservative.exists_mem_iterate_mem' : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → α} {μ : MeasureTheory.Measure α},
  MeasureTheory.Conservative f μ → ∀ ⦃s : Set α⦄, MeasurableSet s → μ s ≠ 0 → ∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[m] x ∈ s
-- Std.Net.Addr
Std.Net.instDecidableEqMACAddr.decEq : (x x_1 : Std.Net.MACAddr) → Decidable (x = x_1)
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
RightDerivMeasurableAux.differentiable_set_eq_D : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {f : ℝ → F} (K : Set F),
  IsComplete K →
    {x | DifferentiableWithinAt ℝ f (Set.Ici x) x ∧ derivWithin f (Set.Ici x) x ∈ K} = RightDerivMeasurableAux.D f K
-- Mathlib.LinearAlgebra.Matrix.Integer
Matrix.num_map_intCast : ∀ {m : Type u_1} {n : Type u_2} [inst : Fintype m] [inst_1 : Fintype n] (A : Matrix m n ℤ), (A.map Int.cast).num = A
-- Mathlib.Topology.Algebra.ConstMulAction
tendsto_const_smul_iff : ∀ {α : Type u_2} {β : Type u_3} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [ContinuousConstSMul G α] {f : β → α} {l : Filter β} {a : α} (c : G),
  Filter.Tendsto (fun x => c • f x) l (nhds (c • a)) ↔ Filter.Tendsto f l (nhds a)
-- Init.Data.Nat.ToString
Nat.digitChar_eq_c : ∀ {n : ℕ}, n.digitChar = 'c' ↔ n = 12
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPullback.isIso_fst_of_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z},
  CategoryTheory.IsPullback fst snd f g →
    autoParam (CategoryTheory.IsIso g) CategoryTheory.IsPullback.isIso_fst_of_isIso._auto_1 → CategoryTheory.IsIso fst
-- Mathlib.Algebra.Notation.Pi.Basic
/-- Abbreviation for `mulSingle_eq_of_ne h.symm`, for ease of use by `simp`.  -/
Pi.mulSingle_eq_of_ne' : ∀ {ι : Type u_1} {M : ι → Type u_6} [inst : (i : ι) → One (M i)] [inst_1 : DecidableEq ι] {i i' : ι},
  i ≠ i' → ∀ (x : M i), Pi.mulSingle i x i' = 1
-- Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Nat.Partition.powerSeriesMk_card_countRestricted_eq_tprod : ∀ (R : Type u_1) [inst : TopologicalSpace R] [T2Space R] [inst_2 : CommSemiring R] {m : ℕ},
  0 < m →
    (PowerSeries.mk fun n => ↑(Nat.Partition.countRestricted n m).card) =
      ∏' (i : ℕ), ∑ j ∈ Finset.range m, PowerSeries.X ^ ((i + 1) * j)
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.mk.inj : ∀ {M : Type u_3} {inst : Mul M} {carrier : Set M} {mul_mem' : ∀ {a b : M}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier}
  {carrier_1 : Set M} {mul_mem'_1 : ∀ {a b : M}, a ∈ carrier_1 → b ∈ carrier_1 → a * b ∈ carrier_1},
  { carrier := carrier, mul_mem' := mul_mem' } = { carrier := carrier_1, mul_mem' := mul_mem'_1 } → carrier = carrier_1
-- Lean.Data.Json.Basic
Lean.Json.getObj? : Lean.Json → Except String (Std.TreeMap.Raw String Lean.Json compare)
-- Mathlib.Topology.Homeomorph.Lemmas
/-- `Equiv.piCongr` as a homeomorphism: this is the natural homeomorphism
`Π i₁, Y₁ i ≃ₜ Π i₂, Y₂ i₂` obtained from a bijection `ι₁ ≃ ι₂` and homeomorphisms
`Y₁ i₁ ≃ₜ Y₂ (e i₁)` for each `i₁ : ι₁`.  -/
Homeomorph.piCongr : {ι₁ : Type u_7} →
  {ι₂ : Type u_8} →
    {Y₁ : ι₁ → Type u_9} →
      {Y₂ : ι₂ → Type u_10} →
        [inst : (i₁ : ι₁) → TopologicalSpace (Y₁ i₁)] →
          [inst_1 : (i₂ : ι₂) → TopologicalSpace (Y₂ i₂)] →
            (e : ι₁ ≃ ι₂) → ((i₁ : ι₁) → Y₁ i₁ ≃ₜ Y₂ (e i₁)) → ((i₁ : ι₁) → Y₁ i₁) ≃ₜ ((i₂ : ι₂) → Y₂ i₂)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.MonObj.instIsMonHomToUnit : ∀ {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D] [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory D]
  (M : D) [inst_2 : CategoryTheory.MonObj M],
  CategoryTheory.IsMonHom (CategoryTheory.SemiCartesianMonoidalCategory.toUnit M)
-- Mathlib.Topology.Homotopy.Path
/-- Given a `Homotopy p₀ p₁`, we can define a `Homotopy p₁ p₀` by reversing the homotopy.
 -/
Path.Homotopy.symm : {X : Type u} → [inst : TopologicalSpace X] → {x₀ x₁ : X} → {p₀ p₁ : Path x₀ x₁} → p₀.Homotopy p₁ → p₁.Homotopy p₀
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.instToJsonModuleHierarchy.toJson : Lean.Lsp.Ipc.ModuleHierarchy → Lean.Json
-- Mathlib.Data.Int.Bitwise
/-- `bit b` appends the digit `b` to the binary representation of
its integer input.  -/
Int.bit : Bool → ℤ → ℤ
-- Mathlib.CategoryTheory.Functor.TwoSquare
/-- Notation for the horizontal composition of 2-squares.  -/
CategoryTheory.TwoSquare.«term_≫ₕ_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Sheaves.Flasque
TopCat.Sheaf.IsFlasque.structured_arrows_elements_sheaf_chains_bounded : ∀ {X : TopCat} {U : TopologicalSpace.Opens ↑X} {F G : TopCat.Sheaf AddCommGrpCat X} (g : F ⟶ G)
  (s : ↑(G.obj.obj (Opposite.op U))) (c : Set (TopCat.Sheaf.IsFlasque.Under g s)),
  IsChain (fun x y => Nonempty (y ⟶ x)) c → ∃ ub, ∀ a ∈ c, Nonempty (ub ⟶ a)
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
/-- The function `seminormFromConst` is a `RingSeminorm` on `R`.  -/
seminormFromConst : {R : Type u_1} → [inst : CommRing R] → {c : R} → {f : RingSeminorm R} → f 1 ≤ 1 → f c ≠ 0 → IsPowMul ⇑f → RingSeminorm R
-- Mathlib.Data.Finset.Prod
Finset.diag_singleton : ∀ {α : Type u_1} (a : α), {a}.diag = {(a, a)}
-- Std.Internal.Do.WP.Lemmas
_private.Std.Internal.Do.WP.Lemmas.0.Option.orElse.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → (Unit → Option α) → Sort u_2) (a : α) (x : Unit → Option α)
  (h_1 : (a : α) → (x : Unit → Option α) → motive (some a) x) (h_2 : (b : Unit → Option α) → motive none b),
  (match some a, x with
    | some a, x => h_1 a x
    | none, b => h_2 b) =
    h_1 a x
-- Mathlib.CategoryTheory.Limits.VanKampen
/-- Pullbacks distribute over universal coproducts on the right: This is the isomorphism
`∐ (Xᵢ ×[S] B) ≅ (∐ Xᵢ) ×[S] B`.  -/
CategoryTheory.IsUniversalColimit.isPullback_of_isColimit_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_3} {S B : C} {X : ι → C}
  {a : CategoryTheory.Limits.Cofan X},
  CategoryTheory.IsUniversalColimit a →
    ∀ (f : (i : ι) → X i ⟶ S) (u : a.pt ⟶ S) (v : B ⟶ S) {P : ι → C} (q₁ : (i : ι) → P i ⟶ X i)
      (q₂ : (i : ι) → P i ⟶ B),
      (∀ (i : ι), CategoryTheory.IsPullback (q₁ i) (q₂ i) (f i) v) →
        ∀ {d : CategoryTheory.Limits.Cofan P} (hd : CategoryTheory.Limits.IsColimit d),
          autoParam (∀ (i : ι), CategoryTheory.CategoryStruct.comp (a.inj i) u = f i)
              CategoryTheory.IsUniversalColimit.isPullback_of_isColimit_right._auto_1 →
            ∀ [CategoryTheory.Limits.HasPullback u v],
              CategoryTheory.IsPullback
                (CategoryTheory.Limits.Cofan.IsColimit.desc hd fun x =>
                  CategoryTheory.CategoryStruct.comp (q₁ x) (a.inj x))
                (CategoryTheory.Limits.Cofan.IsColimit.desc hd q₂) u v
-- Init.Data.Int.Linear
Int.Internal.Linear.instBEqPoly.beq.eq_2 : ∀ (a : ℤ) (a_1 : Int.Internal.Linear.Var) (a_2 : Int.Internal.Linear.Poly) (b : ℤ) (b_1 : Int.Internal.Linear.Var)
  (b_2 : Int.Internal.Linear.Poly),
  Int.Internal.Linear.instBEqPoly.beq (Int.Internal.Linear.Poly.add a a_1 a_2)
      (Int.Internal.Linear.Poly.add b b_1 b_2) =
    (a == b && (a_1 == b_1 && Int.Internal.Linear.instBEqPoly.beq a_2 b_2))
-- Batteries.Data.ByteSlice
/-- Test whether a byte slice is empty.  -/
ByteSlice.isEmpty : ByteSlice → Bool
-- Mathlib.GroupTheory.FreeAbelianGroup
instAddCommGroupFreeAbelianGroup : (α : Type u_1) → AddCommGroup (FreeAbelianGroup α)
-- Init.Data.List.TakeDrop
List.drop_tail : ∀ {α : Type u_1} {l : List α} {i : ℕ}, List.drop i l.tail = List.drop (i + 1) l
-- Std.Async.Signal
/-- Urgent condition on socket.
 -/
Std.Async.Signal.sigurg : Std.Async.Signal
-- Mathlib.Data.SetLike.Basic
SetLike.mem_coe : ∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} {x : B}, x ∈ ↑p ↔ x ∈ p
-- Lean.Compiler.IR.Basic
Lean.IR.LocalContextEntry.localVar : Lean.IR.IRType → Lean.IR.Expr → Lean.IR.LocalContextEntry
-- Std.Http.Protocol.H1.Writer
Std.Http.Protocol.H1.Writer.State.waitingHeaders.sizeOf_spec : sizeOf Std.Http.Protocol.H1.Writer.State.waitingHeaders = 1
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- Data stored for each "stained" location.  -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.StainData : Type
-- Init.Data.Int.Order
Int.natAbs_lt_natAbs_of_nonneg_of_lt : ∀ {a b : ℤ}, 0 ≤ a → a < b → a.natAbs < b.natAbs
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.inv_mk : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : DivisionRing β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {f : CauSeq β abv} (hf : ¬f.LimZero),
  (CauSeq.Completion.mk f)⁻¹ = CauSeq.Completion.mk (f.inv hf)
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.assemble₂_eq_some_iff_utf8EncodeChar_eq : ∀ {x y : UInt8} {c : Char},
  ByteArray.utf8DecodeChar?.parseFirstByte x = ByteArray.utf8DecodeChar?.FirstByte.oneMore ∧
      ByteArray.utf8DecodeChar?.assemble₂ x y = some c ↔
    String.utf8EncodeChar c = [x, y]
-- Mathlib.Order.Heyting.Basic
sdiff_idem : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, (a \ b) \ b = a \ b
-- Mathlib.Order.Interval.Multiset
/-- The multiset of elements `x` such that `x < b`. Basically `Set.Iio b` as a multiset.  -/
Multiset.Iio : {α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrderBot α] → α → Multiset α
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.openPartialHomeomorphCoe_source : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [hp : Fact (0 < p)] (a : 𝕜) [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜] [inst_5 : OrderTopology 𝕜]
  [inst_6 : DiscreteTopology ↥(AddSubgroup.zmultiples p)],
  (AddCircle.openPartialHomeomorphCoe p a).source = Set.Ioo a (a + p)
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.coe_expand : ∀ (R : Type u) [inst : CommSemiring R] (p : ℕ),
  ⇑(Polynomial.expand R p) = Polynomial.eval₂ Polynomial.C (Polynomial.X ^ p)
-- Mathlib.RingTheory.IsAdjoinRoot
/-- Adjoining a root gives a unique algebra up to isomorphism.

This is the converse of `IsAdjoinRoot.ofAlgEquiv`: this turns an `IsAdjoinRoot` into an
`AlgEquiv`, and `IsAdjoinRoot.ofAlgEquiv` turns an `AlgEquiv` into an `IsAdjoinRoot`.
 -/
IsAdjoinRoot.algEquiv : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : Ring S] →
        {f : Polynomial R} →
          [inst_2 : Algebra R S] →
            IsAdjoinRoot S f →
              {T : Type u_1} → [inst_3 : Ring T] → [inst_4 : Algebra R T] → IsAdjoinRoot T f → S ≃ₐ[R] T
-- Lean.DocString.Parser
Lean.Doc.Parser.OrderedListType.parenAfter.sizeOf_spec : sizeOf Lean.Doc.Parser.OrderedListType.parenAfter = 1
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.SpaceResult.foundFlattenedHardLine : Std.Format.SpaceResult✝ → Bool
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.Hom.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.AddMon C} [inst_2 : SizeOf C] (hom : M.X ⟶ N.X)
  [isAddMonHom_hom : CategoryTheory.IsAddMonHom hom],
  sizeOf { hom := hom, isAddMonHom_hom := isAddMonHom_hom } = 1 + sizeOf hom + sizeOf isAddMonHom_hom
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.funInvIdAssoc_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) (F : CategoryTheory.Functor C E) (X : C),
  (e.funInvIdAssoc F).hom.app X = F.map (e.unitInv.app X)
-- Mathlib.Dynamics.Ergodic.Action.OfMinimal
/-- Let `f : G →+ G` be an additive group endomorphism
of a topological additive group with second countable topology.
If the preimages of `0` under the iterations of `f` are dense,
then it is pre-ergodic with respect to any finite inner regular left invariant measure.  -/
AddMonoidHom.preErgodic_of_dense_iUnion_preimage_zero : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] [SecondCountableTopology G]
  [inst_4 : MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [MeasureTheory.IsFiniteMeasure μ]
  [μ.InnerRegular] [μ.IsAddLeftInvariant] (f : G →+ G), Dense (⋃ n, (⇑f)^[n] ⁻¹' 0) → PreErgodic (⇑f) μ