mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- When `S₁.g` and `S₂.g` are zero and we have chosen colimit cokernel coforks `c₁` and `c₂`
for `S₁.f` and `S₂.f` respectively, the action on homology of a morphism `φ : S₁ ⟶ S₂` of
short complexes is given by the unique morphism `f : c₁.pt ⟶ c₂.pt` such that
`φ.τ₂ ≫ c₂.π = c₁.π ≫ f`.  -/
CategoryTheory.ShortComplex.HomologyMapData.ofIsColimitCokernelCofork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ : S₁ ⟶ S₂) →
          (hg₁ : S₁.g = 0) →
            (c₁ : CategoryTheory.Limits.CokernelCofork S₁.f) →
              (hc₁ : CategoryTheory.Limits.IsColimit c₁) →
                (hg₂ : S₂.g = 0) →
                  (c₂ : CategoryTheory.Limits.CokernelCofork S₂.f) →
                    (hc₂ : CategoryTheory.Limits.IsColimit c₂) →
                      (f : c₁.pt ⟶ c₂.pt) →
                        CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.Limits.Cofork.π c₂) =
                            CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π c₁) f →
                          CategoryTheory.ShortComplex.HomologyMapData φ
                            (CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork S₁ hg₁ c₁ hc₁)
                            (CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork S₂ hg₂ c₂ hc₂)
-- Mathlib.Topology.Defs.Filter
/-- Notation for the filter of left neighborhoods of a point.  -/
Topology.nhdsLE : Lean.ParserDescr
-- Mathlib.Lean.Meta.Simp
/-- Given a simplifier `S : Expr → MetaM Simp.Result`,
and an expression `e : Expr`, run `S` on the type of `e`, and then
convert `e` into that simplified type,
using a combination of type hints as well as casting if the proof is not definitional `Eq.mp`.

The optional argument `type?`, if present, must be definitionally equal to the type of `e`.
When it is specified we simplify this type rather than the inferred type of `e`.
 -/
Lean.Meta.simpType : (Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result) → Lean.Expr → optParam (Option Lean.Expr) none → Lean.MetaM Lean.Expr
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.monotone_l_comp_u : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
  GaloisConnection l u → Monotone (l ∘ u)
-- Mathlib.Analysis.SpecificLimits.Basic
ENNReal.tendsto_pow_atTop_nhds_zero_iff : ∀ {r : ENNReal}, Filter.Tendsto (fun n => r ^ n) Filter.atTop (nhds 0) ↔ r < 1
-- Mathlib.Order.WellFoundedSet
Set.IsWF.insert : ∀ {α : Type u_2} [inst : Preorder α] {s : Set α}, s.IsWF → ∀ (a : α), (insert a s).IsWF
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_alter_eq_self_of_mem : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : Option (β k) → Option (β k)}, k ∈ m → (f (m.get? k)).isSome = true → (m.alter k f).size = m.size
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.coker.condition : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasCokernels C],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Arrow.leftToRight (CategoryTheory.Limits.coker.π C) = 0
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_filterMap : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w}
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] [inst_4 : Inhabited γ]
  {f : α → β → Option γ} {k : α} (h : (↑m).WF),
  Std.DHashMap.Internal.Raw₀.Const.get! (Std.DHashMap.Internal.Raw₀.filterMap f m) k =
    ((Std.DHashMap.Internal.Raw₀.Const.get? m k).pbind fun x h' => f (m.getKey k ⋯) x).get!
-- Init.Data.Slice.List.Lemmas
_private.Init.Data.Slice.List.Lemmas.0.ListSlice.internalIter_eq_toIteratorIter : ∀ {α : Type u} {s : ListSlice α}, Std.Slice.Internal.iter s = Std.ToIterator.iter s
-- Mathlib.Algebra.Regular.ULift
ULift.isAddLeftRegular_up : ∀ {R : Type v} [inst : Add R] {a : R}, IsAddLeftRegular { down := a } ↔ IsAddLeftRegular a
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.aeval_coe : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : UniformSpace R] {S : Type u_3} [inst_2 : CommRing S]
  [inst_3 : UniformSpace S] {a : σ → S} [inst_4 : IsTopologicalSemiring R] [inst_5 : IsUniformAddGroup R]
  [inst_6 : IsUniformAddGroup S] [inst_7 : CompleteSpace S] [inst_8 : T2Space S] [inst_9 : IsTopologicalRing S]
  [inst_10 : IsLinearTopology S S] [inst_11 : Algebra R S] [inst_12 : ContinuousSMul R S] (ha : MvPowerSeries.HasEval a)
  (p : MvPolynomial σ R), (MvPowerSeries.aeval ha) ↑p = (MvPolynomial.aeval a) p
-- Mathlib.Data.Sum.Order
OrderIso.sumLexAssoc_symm_apply_inr_inr : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst_1 : LE β] [inst_2 : LE γ] (c : γ),
  (OrderIso.sumLexAssoc α β γ).symm (Sum.inr (Sum.inr c)) = Sum.inr c
-- Mathlib.SetTheory.Ordinal.Basic
/-- Initial segment version of the lift operation on ordinals, embedding `Ordinal.{u}` in
`Ordinal.{v}` as an initial segment when `u ≤ v`.  -/
Ordinal.liftInitialSeg : Ordinal.{v} ≤i Ordinal.{max u v}
-- Mathlib.Topology.Compactness.Compact
/-- The intersection of a closed set and a compact set is a compact set.  -/
IsCompact.inter_left : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsCompact t → IsClosed s → IsCompact (s ∩ t)
-- Mathlib.Analysis.RCLike.Basic
RCLike.zero_im : ∀ {K : Type u_1} [inst : RCLike K], RCLike.im 0 = 0
-- Mathlib.Topology.Constructions
Pi.continuous_postcomp' : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] {X : ι → Type u_9}
  [inst : (i : ι) → TopologicalSpace (X i)] {g : (i : ι) → A i → X i},
  (∀ (i : ι), Continuous (g i)) → Continuous fun f i => g i (f i)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.domRestrict_apply : ∀ {M : Type u_1} [inst : AddZeroClass M] {N : Type u_5} {S : Type u_6} [inst_1 : AddZeroClass N] [inst_2 : SetLike S M]
  [inst_3 : AddSubmonoidClass S M] (f : M →+ N) (s : S) (x : ↥s), (f.domRestrict s) x = f ↑x
-- Mathlib.RingTheory.TensorProduct.Basic
LinearMap.liftBaseChange.congr_simp : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} (A : Type u_4) [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N] [inst_5 : Module R M]
  [inst_6 : Module R N] [inst_7 : Module A N] [inst_8 : IsScalarTower R A N] (l l_1 : M →ₗ[R] N),
  l = l_1 → LinearMap.liftBaseChange A l = LinearMap.liftBaseChange A l_1
-- Std.Sat.AIG.LawfulOperator
_private.Std.Sat.AIG.LawfulOperator.0.Std.Sat.AIG.toGraphviz.go.match_1.splitter : {α : Type} →
  (motive : Std.Sat.AIG.Decl α → Sort u_1) →
    (x : Std.Sat.AIG.Decl α) →
      (x = Std.Sat.AIG.Decl.false → motive Std.Sat.AIG.Decl.false) →
        ((idx : α) → x = Std.Sat.AIG.Decl.atom idx → motive (Std.Sat.AIG.Decl.atom idx)) →
          ((lhs rhs : Std.Sat.AIG.Fanin) → x = Std.Sat.AIG.Decl.gate lhs rhs → motive (Std.Sat.AIG.Decl.gate lhs rhs)) →
            motive x
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.instUniqueFactorizationMonoid : ∀ {k : Type u_2} [inst : Field k], UniqueFactorizationMonoid (PowerSeries k)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_filter_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → β → Bool},
  t.WF → ((Std.TreeMap.Raw.filter f t).isEmpty = true ↔ ∀ (k : α) (h : k ∈ t), f (t.getKey k h) t[k] = false)
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Returns `ULift.up true` if the monadic predicate `p` returns `ULift.up true` for
any element emitted by the iterator `it`.

`O(|it|)`. Short-circuits upon encountering the first match. The outputs of `it` are
examined in order of iteration.

This function is deprecated. Instead of `it.allowNontermination.anyM`, use `it.anyM`.
 -/
Std.IterM.Partial.anyM : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α m β] →
        [Std.IteratorLoop α m m] → (β → m (ULift.{w, 0} Bool)) → Std.IterM.Partial m β → m (ULift.{w, 0} Bool)
-- Mathlib.Algebra.BigOperators.Ring.Finset
Int.cast_multiset_prod : ∀ {R : Type u_6} [inst : CommRing R] (s : Multiset ℤ), ↑s.prod = (Multiset.map Int.cast s).prod
-- Mathlib.Analysis.Calculus.ContDiff.Bounds
/-- Bounding the norm of the iterated derivative of `B (f x) (g x)` within a set in terms of the
iterated derivatives of `f` and `g` when `B` is bilinear:
`‖D^n (x ↦ B (f x) (g x))‖ ≤ ‖B‖ ∑_{k ≤ n} n.choose k ‖D^k f‖ ‖D^{n-k} g‖`  -/
ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {D : Type uD} [inst_1 : NormedAddCommGroup D]
  [inst_2 : NormedSpace 𝕜 D] {E : Type uE} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {F : Type uF}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {G : Type uG} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G) {f : D → E} {g : D → F} {N : WithTop ℕ∞} {s : Set D} {x : D},
  ContDiffOn 𝕜 N f s →
    ContDiffOn 𝕜 N g s →
      UniqueDiffOn 𝕜 s →
        x ∈ s →
          ∀ {n : ℕ},
            ↑n ≤ N →
              ‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖ ≤
                ‖B‖ *
                  ∑ i ∈ Finset.range (n + 1),
                    ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
-- Init.Data.Vector.Monadic
Vector.idRun_forIn_yield_eq_foldl : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} (f : α → β → Id β) (init : β),
  (forIn xs init fun a b => ForInStep.yield <$> f a b).run = Vector.foldl (fun b a => (f a b).run) init xs
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.size_filter_le_size : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Bool}, (Std.DHashMap.filter f m).size ≤ m.size
-- Mathlib.Data.Set.Inclusion
Set.inclusion_eq_subtype_map : ∀ {α : Type u_1} {s t : Set α} (h : s ⊆ t), Set.inclusion h = Subtype.map id h
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.updateParams : Array Lean.Expr → List Lean.InductiveType → Lean.Elab.TermElabM (List Lean.InductiveType)
-- Lean.Meta.Tactic.Grind.Types
/-- Returns a proof that `a = b`.
It assumes `a` and `b` are in the same equivalence class, and have the same type.
 -/
Lean.Meta.Grind.mkEqProof : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.Data.Multiset.AddSub
Multiset.add_sub_assoc : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Multiset α}, u ≤ t → s + t - u = s + (t - u)
-- Std.Data.ExtTreeSet.Basic
/-- Internal implementation detail of the tree map.  -/
Std.ExtTreeSet.inner : {α : Type u} →
  {cmp : autoParam (α → α → Ordering) Std.ExtTreeSet._auto_1} → Std.ExtTreeSet α cmp → Std.ExtTreeMap α Unit cmp
-- Mathlib.FieldTheory.SplittingField.IsSplittingField
/-- Characterize `IsSplittingField` with `IntermediateField.adjoin` instead of `Algebra.adjoin`.  -/
isSplittingField_iff_intermediateField : ∀ {K : Type v} {L : Type w} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {p : Polynomial K},
  Polynomial.IsSplittingField K L p ↔
    (Polynomial.map (algebraMap K L) p).Splits ∧ IntermediateField.adjoin K (p.rootSet L) = ⊤
-- Mathlib.Analysis.Normed.MulAction
Metric.smul_image_closedBall : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedDivisionRing α] [inst_1 : SeminormedAddCommGroup β] [inst_2 : Module α β]
  [NormSMulClass α β] {s : α},
  s ≠ 0 → ∀ (x : β) (ε : ℝ), (fun x => s • x) '' Metric.closedBall x ε = Metric.closedBall (s • x) (‖s‖ * ε)
-- Mathlib.MeasureTheory.MeasurableSpace.Instances
Fin.instMeasurableSpace : (n : ℕ) → MeasurableSpace (Fin n)
-- Init.Internal.Order.While
Lean.Loop.forIn.eq_1 : ∀ {β : Type u} {m : Type u → Type v} [inst : Monad m] (x : Lean.Loop) (init : β) (f : Unit → β → m (ForInStep β)),
  x.forIn init f =
    repeatM
      (fun b => do
        let __do_lift ← f () b
        match __do_lift with
          | ForInStep.done b' => pure (Sum.inr b')
          | ForInStep.yield b' => pure (Sum.inl b'))
      init
-- Mathlib.FieldTheory.IntermediateField.Algebraic
IntermediateField.finrank_dvd_of_le_right : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  {F E : IntermediateField K L}, F ≤ E → Module.finrank K ↥F ∣ Module.finrank K ↥E
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.SymExtension.getState : {σ : Type} → Lean.Meta.Sym.SymExtension σ → Lean.Meta.Sym.SymM σ
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
IsBaseChange.endHom.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {P : Type u_5} [inst_5 : AddCommMonoid P] [inst_6 : Module R P]
  [inst_7 : Module S P] [inst_8 : IsScalarTower R S P] {α α_1 : M →ₗ[R] P} (e_α : α = α_1) (j : IsBaseChange S α),
  j.endHom = ⋯.endHom
-- Std.Time.Zoned.ZoneRules
/-- Recurring rule from the TZif footer, used to extrapolate transitions beyond the last stored entry.
 -/
Std.Time.TimeZone.ZoneRules.transitionRule : Std.Time.TimeZone.ZoneRules → Option Std.Time.TimeZone.RecurringRule
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.condExp_nonpos : ∀ {α : Type u_1} {E : Type u_3} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → E}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] [inst_3 : PartialOrder E]
  [ClosedIciTopology E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E], f ≤ᵐ[μ] 0 → μ[f | m] ≤ᵐ[μ] 0
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
FirstOrder.Language.instIsAlgebraicPresburger : FirstOrder.Language.presburger.IsAlgebraic
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.coeFnₗ_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] (R : Type u_6) [inst_1 : Semiring R]
  [inst_2 : AddCommMonoid Y] [inst_3 : Module R Y] (a : LocallyConstant X Y) (a_1 : X),
  (LocallyConstant.coeFnₗ R) a a_1 = a a_1
-- Mathlib.Analysis.Normed.Group.Constructions
Prod.toNorm : {E : Type u_2} → {F : Type u_3} → [Norm E] → [Norm F] → Norm (E × F)
-- Mathlib.Tactic.ClickSuggestions.GRewrite
/-- Whether the two suggestions are duplicates of each other.  -/
Mathlib.Tactic.ClickSuggestions.GrwKey.isDuplicate : Mathlib.Tactic.ClickSuggestions.GrwKey → Mathlib.Tactic.ClickSuggestions.GrwKey → Lean.MetaM Bool
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.Context.inPattern : Lean.PrettyPrinter.Delaborator.Context → Bool
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
/-- For any `x` and any positive `n`, `smoothingFun μ x ≤ μ (x ^ (n : ℕ))^(1 / n : ℝ)`.  -/
smoothingFun_le : ∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R) (x : R) (n : ℕ+), smoothingFun μ x ≤ μ (x ^ ↑n) ^ (1 / ↑↑n)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.instCategory : {C : Type u} → [CategoryTheory.Category.{v, u} C] → CategoryTheory.Category.{v, u} (CategoryTheory.WithTerminal C)
-- Mathlib.Data.Multiset.Fintype
Multiset.sum_toEnumFinset : ∀ {α : Type u_1} [inst : DecidableEq α] {β : Type u_3} [inst_1 : AddCommMonoid β] (m : Multiset α) (f : α → ℕ → β),
  ∑ x ∈ m.toEnumFinset, f x.1 x.2 = ∑ x, f x.fst ↑x.snd
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- The finite set of all prime factors of the pushforward of `p`.  -/
IsDedekindDomain.primesOverFinset : {A : Type u_4} →
  [inst : CommRing A] →
    Ideal A → (B : Type u_5) → [inst_1 : CommRing B] → [IsDedekindDomain B] → [Algebra A B] → Finset (Ideal B)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_of_lt_add_of_nonpos_left : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftMono α] {a b c : α}, a < b + c → c ≤ 0 → a < b
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- The Ore localization of an additive monoid and a submonoid
fulfilling the Ore condition.  -/
AddOreLocalization : {R : Type u_1} →
  [inst : AddMonoid R] →
    (S : AddSubmonoid R) → [AddOreLocalization.AddOreSet S] → (X : Type u_2) → [AddAction R X] → Type (max u_1 u_2)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- A unary operation on two `BVExpr`.
 -/
Std.Tactic.BVDecide.BVExpr.un : {w : ℕ} → Std.Tactic.BVDecide.BVUnOp → Std.Tactic.BVDecide.BVExpr w → Std.Tactic.BVDecide.BVExpr w
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
neg_le_iff_add_nonneg : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddRightMono α] {a b : α}, -a ≤ b ↔ 0 ≤ b + a
-- Mathlib.CategoryTheory.Sites.Sieves
/-- The intersection of two sieves is a sieve.  -/
CategoryTheory.Sieve.inter : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → CategoryTheory.Sieve X → CategoryTheory.Sieve X → CategoryTheory.Sieve X
-- Init.Data.List.Erase
List.le_length_eraseIdx : ∀ {α : Type u_1} (l : List α) (i : ℕ), l.length - 1 ≤ (l.eraseIdx i).length
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
/-- Alternative characterisation of discrete valuation rings.  -/
IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization : (R : Type u_1) → [CommRing R] → Prop
-- Init.Data.SInt.Lemmas
Int8.toInt_bmod_4294967296 : ∀ (x : Int8), x.toInt.bmod 4294967296 = x.toInt
-- Mathlib.Order.Sublattice
Sublattice.prod_left_mono : ∀ {α : Type u_2} [inst : Lattice α] {M : Sublattice α}, Monotone fun L => L.prod M
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.map_lift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} {X Y : C} {p : X ⟶ Y} {f : F.obj ⊥ ⟶ X}
  {g : c.pt ⟶ Y} [inst_3 : F.IsWellOrderContinuous] {j : J} (hj : Order.IsSuccLimit j)
  (s : ↑(⋯.functor.op.comp (CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor c p f g)).sections)
  {i : J} (hij : i < j),
  CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.map
      (CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.lift hj s)
      (CategoryTheory.homOfLE ⋯) =
    ↑s (Opposite.op ⟨i, hij⟩)
-- Std.Data.Internal.List.Associative
Std.Internal.List.Option.exists_eq_some_and_iff : ∀ {α : Type u} (o : Option α) (p : α → Prop), (∃ x, o = some x ∧ p x) ↔ ∃ (h : o.isSome = true), p (o.get h)
-- Mathlib.Data.Finset.Sym
Finset.sym2_map : ∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α), (Finset.map f s).sym2 = Finset.map f.sym2Map s.sym2
-- Mathlib.Order.Irreducible
not_supIrred_bot : ∀ {α : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderBot α], ¬SupIrred ⊥
-- Std.Time.Internal.Bounded
/-- Convert a `Nat` to a `Bounded.LE` using the lower boundary too.
 -/
Std.Time.Internal.Bounded.LE.clip : {lo hi : ℤ} → ℤ → lo ≤ hi → Std.Time.Internal.Bounded.LE lo hi
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.zero_smul' : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [inst : PartialOrder Γ] [inst_1 : PartialOrder Γ']
  [inst_2 : VAdd Γ Γ'] [inst_3 : IsOrderedCancelVAdd Γ Γ'] [inst_4 : AddCommMonoid V] [inst_5 : Zero R]
  [inst_6 : SMulWithZero R V] {x : HahnModule Γ' R V}, 0 • x = 0
-- Mathlib.FieldTheory.Galois.Profinite
/-- `toAlgEquivAux` as an `AlgEquiv`.
It is done by using above lifting lemmas on bigger `FiniteGaloisIntermediateField`.  -/
InfiniteGalois.limitToAlgEquiv : {k : Type u_3} →
  {K : Type u_4} →
    [inst : Field k] →
      [inst_1 : Field K] →
        [inst_2 : Algebra k K] →
          [IsGalois k K] →
            ↑(ProfiniteGrp.limit (InfiniteGalois.asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop → Gal(K/k)
-- Mathlib.RingTheory.Etale.StandardEtale
IsLocalization.Away.liftAlgHom.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {P : Type u_3}
  [inst_3 : CommSemiring P] (x x_1 : R) (e_x : x = x_1) [inst_4 : IsLocalization.Away x S] {A : Type u_4}
  [inst_5 : CommSemiring A] [inst_6 : Algebra A R] [inst_7 : Algebra A S] [inst_8 : Algebra A P]
  [inst_9 : IsScalarTower A R S] {f f_1 : R →ₐ[A] P} (e_f : f = f_1) (hf : IsUnit (f x)),
  IsLocalization.Away.liftAlgHom x hf = IsLocalization.Away.liftAlgHom x_1 ⋯
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.mk.inj : ∀ {toOrderHom : ℝ →o ℝ} {map_add_one' : ∀ (x : ℝ), toOrderHom.toFun (x + 1) = toOrderHom.toFun x + 1}
  {toOrderHom_1 : ℝ →o ℝ} {map_add_one'_1 : ∀ (x : ℝ), toOrderHom_1.toFun (x + 1) = toOrderHom_1.toFun x + 1},
  { toOrderHom := toOrderHom, map_add_one' := map_add_one' } =
      { toOrderHom := toOrderHom_1, map_add_one' := map_add_one'_1 } →
    toOrderHom = toOrderHom_1
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
LieRinehartRing.leibniz_smul_right' : ∀ {A : Type u_1} {L : Type u_2} {inst : CommRing A} {inst_1 : LieRing L} {inst_2 : Module A L}
  {inst_3 : LieRingModule L A} [self : LieRinehartRing A L] (x y : L) (a : A), ⁅x, a • y⁆ = a • ⁅x, y⁆ + ⁅x, a⁆ • y
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey!_modify_self : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.WF →
    ∀ [inst : Inhabited α] {k : α} {f : β → β},
      (Std.DTreeMap.Internal.Impl.Const.modify k f t).getKey! k = if k ∈ t then k else default
-- Mathlib.Topology.Separation.Hausdorff
/-- Points of a finite set can be separated by open sets from each other.  -/
Set.Finite.t2_separation : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] {s : Set X},
  s.Finite → ∃ U, (∀ (x : X), x ∈ U x ∧ IsOpen (U x)) ∧ s.PairwiseDisjoint U
-- Mathlib.Computability.PartrecBasis
Nat.Partrec'.of_eq : ∀ {n : ℕ} {f g : List.Vector ℕ n →. ℕ}, Nat.Partrec' f → (∀ (i : List.Vector ℕ n), f i = g i) → Nat.Partrec' g
-- Mathlib.Analysis.Convex.Gauge
/-- **Alias** of `setOfPred_gauge_lt_one_eq_interior`. -/
setOf_gauge_lt_one_eq_interior : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} [inst_2 : TopologicalSpace E]
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E], Convex ℝ s → s ∈ nhds 0 → {x | gauge s x < 1} = interior s
-- Mathlib.Data.Set.Lattice
Set.biUnion_le_eq_iUnion : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] {s : α → Set β}, ⋃ n, ⋃ m, ⋃ (_ : m ≤ n), s m = ⋃ n, s n
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.Scheme.Hom.finite_preimage : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyQuasiFinite f]
  [AlgebraicGeometry.QuasiCompact f] {s : Set ↥Y}, s.Finite → (⇑f ⁻¹' s).Finite
-- Mathlib.Algebra.Order.Quantale
AddQuantale.leftAddResiduation_le_iff_add_le : ∀ {α : Type u_1} {x y z : α} [inst : AddSemigroup α] [inst_1 : CompleteLattice α] [IsAddQuantale α],
  x ≤ AddQuantale.leftAddResiduation y z ↔ x + y ≤ z
-- Mathlib.Order.Filter.Map
Function.Semiconj.filter_comap : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α} {gb : β → β},
  Function.Semiconj f ga gb → Function.Semiconj (Filter.comap f) (Filter.comap gb) (Filter.comap ga)
-- Mathlib.Order.BooleanAlgebra.Set
Set.compl_singleton_eq : ∀ {α : Type u_1} (a : α), {a}ᶜ = {x | x ≠ a}
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
TopologicalSpace.PositiveCompacts.Icc01.eq_1 : TopologicalSpace.PositiveCompacts.Icc01 =
  { carrier := Set.Icc 0 1, isCompact' := TopologicalSpace.PositiveCompacts.Icc01._proof_1,
    interior_nonempty' := TopologicalSpace.PositiveCompacts.Icc01._proof_3 }
-- Mathlib.Data.PFunctor.Multivariate.W
_private.Mathlib.Data.PFunctor.Multivariate.W.0.MvPFunctor.wMk'.match_1.eq_1 : ∀ {n : ℕ} (P : MvPFunctor.{u_1} (n + 1)) {α : TypeVec.{u_1} n} (motive : ↑P (α ::: P.W α) → Sort u_2) (a : P.A)
  (f : (P.B a).Arrow (α ::: P.W α)) (h_1 : (a : P.A) → (f : (P.B a).Arrow (α ::: P.W α)) → motive ⟨a, f⟩),
  (match ⟨a, f⟩ with
    | ⟨a, f⟩ => h_1 a f) =
    h_1 a f
-- Mathlib.Data.Finset.NAry
Finset.image_image₂ : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq γ] {s : Finset α} {t : Finset β}
  [inst_1 : DecidableEq δ] (f : α → β → γ) (g : γ → δ),
  Finset.image g (Finset.image₂ f s t) = Finset.image₂ (fun a b => g (f a b)) s t