mathlib-initiative/mathlib-types huggingface dataset:
-- ImportGraph.Imports.RequiredModules
_private.ImportGraph.Imports.RequiredModules.0.Lean.Environment.transitivelyRequiredModules'.toNameSet : Lean.Environment → {N : ℕ} → BitVec N → Lean.NameSet
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.Answer.mk.sizeOf_spec : ∀ (result : Lean.Meta.AbstractMVarsResult) (resultType : Lean.Expr) (size : ℕ),
  sizeOf { result := result, resultType := resultType, size := size } =
    1 + sizeOf result + sizeOf resultType + sizeOf size
-- Init.Data.Range.Polymorphic.SInt
Int32.instRxiHasSize.eq_1 : Int32.instRxiHasSize = { size := fun lo => (2 ^ 31 - lo.toInt).toNat }
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.map : ∀ {R : Type u} [inst : CommSemiring R] {x y : R},
  IsCoprime x y → ∀ {S : Type v} [inst_1 : CommSemiring S] (f : R →+* S), IsCoprime (f x) (f y)
-- Mathlib.Algebra.GroupWithZero.Action.Units
Equiv.smulRight_apply : ∀ {α : Type u_4} {β : Type u_5} [inst : GroupWithZero α] [inst_1 : MulAction α β] {a : α} (ha : a ≠ 0) (b : β),
  (Equiv.smulRight ha) b = a • b
-- Lean.Structure
/-- Gets the `StructureInfo` for `structName`, which is assumed to have been declared as a structure to the elaborator.
Panics on failure.
 -/
Lean.getStructureInfo : Lean.Environment → Lean.Name → Lean.StructureInfo
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
ISize.reduceToNatClampNeg : Lean.Meta.Simp.Simproc
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeff_update : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ) (a : R),
  (p.update n a).coeff = Function.update p.coeff n a
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.coe_range_mem_nhds : ∀ {r : NNReal}, Set.range ENNReal.ofNNReal ∈ nhds ↑r
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- `e` is `p`  -/
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defn : Lean.Expr → Int.Internal.Linear.Poly → Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof
-- Mathlib.CategoryTheory.Adjunction.Opposites
/-- If `G` is adjoint to `F` then `F.unop` is adjoint to `G.unop`.  -/
CategoryTheory.Adjunction.unop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} → {G : CategoryTheory.Functor Dᵒᵖ Cᵒᵖ} → (G ⊣ F) → (F.unop ⊣ G.unop)
-- Mathlib.Data.Nat.SuccPred
Nat.pred_iterate : ∀ (a n : ℕ), Nat.pred^[n] a = a - n
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.isUnit_weierstrassUnit : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] [inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A]
  {g : PowerSeries A} (hg : (PowerSeries.map (IsLocalRing.residue A)) g ≠ 0), IsUnit (g.weierstrassUnit hg)
-- Mathlib.Topology.Algebra.GroupWithZero
nhds_inv₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀] [ContinuousInv₀ G₀] {x : G₀},
  x ≠ 0 → nhds x⁻¹ = (nhds x)⁻¹
-- Mathlib.Analysis.Normed.Group.Pointwise
ball_div_one : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (s : Set E), Metric.ball 1 δ / s = Metric.thickening δ s⁻¹
-- Mathlib.Topology.TietzeExtension
/-- **Tietze extension theorem** for nonnegative real-valued continuous maps.
`ℝ≥0` is a `TietzeExtension` space.  -/
NNReal.instTietzeExtension : TietzeExtension NNReal
-- Mathlib.Analysis.Convex.Quasiconvex
Convex.quasiconcaveOn_of_convex_ge : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LE β] [inst_4 : SMul 𝕜 E] {s : Set E} {f : E → β},
  Convex 𝕜 s → (∀ (r : β), Convex 𝕜 {x | r ≤ f x}) → QuasiconcaveOn 𝕜 s f
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_lt_top_iff : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.eRk X < ⊤ ↔ M.IsRkFinite X
-- Mathlib.Topology.Category.FinTopCat
FinTopCat.mk.inj : ∀ {toTop : TopCat} {fintype : Fintype ↑toTop} {toTop_1 : TopCat} {fintype_1 : Fintype ↑toTop_1},
  { toTop := toTop, fintype := fintype } = { toTop := toTop_1, fintype := fintype_1 } →
    toTop = toTop_1 ∧ fintype ≍ fintype_1
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map_assoc : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n}
  (self : f.MulStruct g fg i) {Z : SSet} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc.castSucc)
      (CategoryTheory.CategoryStruct.comp self.map h) =
    CategoryTheory.CategoryStruct.comp g.map h
-- Mathlib.Condensed.Discrete.LocallyConstant
CompHausLike.LocallyConstant.counitAppApp.congr_simp : ∀ {P : TopCat → Prop} [inst : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)]
  [inst_1 : CompHausLike.HasProp P PUnit.{u + 1}] (S : CompHausLike P)
  (Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w)))
  [inst_2 : CategoryTheory.Limits.PreservesFiniteProducts Y] [inst_3 : CompHausLike.HasExplicitFiniteCoproducts P],
  CompHausLike.LocallyConstant.counitAppApp S Y = CompHausLike.LocallyConstant.counitAppApp S Y
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Subgroup.zpowers.eq_1 : ∀ {G : Type u_1} [inst : Group G] (g : G),
  Subgroup.zpowers g = { carrier := Set.range fun x => g ^ x, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
-- Mathlib.Probability.Kernel.Irreducible
ProbabilityTheory.Kernel.instIsIrreducibleHSMulENNRealMeasure : ∀ {α : Type u_1} {mα : MeasurableSpace α} {c : ENNReal} {φ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α α}
  [hκ : ProbabilityTheory.Kernel.IsIrreducible φ κ], ProbabilityTheory.Kernel.IsIrreducible (c • φ) κ
-- Mathlib.Topology.SeparatedMap
IsSeparatedMap.eqOn_of_comp_eqOn : ∀ {X : Type u_1} {E : Type u_2} {A : Type u_3} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace A] {p : E → X}
  {s : Set A} {g₁ g₂ : A → E},
  IsSeparatedMap p →
    IsLocallyInjective p →
      IsPreconnected s →
        ContinuousOn g₁ s →
          ContinuousOn g₂ s → Set.EqOn (p ∘ g₁) (p ∘ g₂) s → ∀ {a : A}, a ∈ s → g₁ a = g₂ a → Set.EqOn g₁ g₂ s
-- Mathlib.Analysis.Convex.Approximation
/-- The countable version of `univ_sSup_affine_eq`.  -/
ConvexOn.univ_sSup_of_countable_affine_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} {φ : E → ℝ} [inst : RCLike 𝕜] [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℝ E] [inst_4 : Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  [LocallyConvexSpace ℝ E] [HereditarilyLindelofSpace E],
  LowerSemicontinuous φ →
    ConvexOn ℝ Set.univ φ →
      ∃ 𝓕', 𝓕'.Countable ∧ sSup 𝓕' = φ ∧ ∀ f ∈ 𝓕', f ≤ φ ∧ ∃ l c, f = ⇑RCLike.re ∘ ⇑l + Function.const E c
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- If we have particular colimit cocones available for `E ⋙ F` and for `F`,
we obtain a formula for `colimit.pre F E`.
 -/
CategoryTheory.Limits.colimit.pre_eq : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C}
  [inst_3 : CategoryTheory.Limits.HasColimit F] {E : CategoryTheory.Functor K J}
  [inst_4 : CategoryTheory.Limits.HasColimit (E.comp F)] (s : CategoryTheory.Limits.ColimitCocone (E.comp F))
  (t : CategoryTheory.Limits.ColimitCocone F),
  CategoryTheory.Limits.colimit.pre F E =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.isoColimitCocone s).hom
      (CategoryTheory.CategoryStruct.comp (s.isColimit.desc (CategoryTheory.Limits.Cocone.whisker E t.cocone))
        (CategoryTheory.Limits.colimit.isoColimitCocone t).inv)
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balance!.match_1.congr_eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (r : Std.DTreeMap.Internal.Impl α β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          motive
            (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf))
  (h_3 :
    (size : ℕ) →
      (rk : α) →
        (rv : β rk) →
          (rr : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k : α) →
                (v : β k) →
                  (l r : Std.DTreeMap.Internal.Impl α β) →
                    rr = Std.DTreeMap.Internal.Impl.inner size_1 k v l r →
                      motive
                        (Std.DTreeMap.Internal.Impl.inner size rk rv Std.DTreeMap.Internal.Impl.leaf
                          (Std.DTreeMap.Internal.Impl.inner size_1 k v l r)))
  (h_4 :
    (size : ℕ) →
      (rk : α) →
        (rv : β rk) →
          (size_1 : ℕ) →
            (rlk : α) →
              (rlv : β rlk) →
                (l r : Std.DTreeMap.Internal.Impl α β) →
                  motive
                    (Std.DTreeMap.Internal.Impl.inner size rk rv (Std.DTreeMap.Internal.Impl.inner size_1 rlk rlv l r)
                      Std.DTreeMap.Internal.Impl.leaf))
  (h_5 :
    (rs : ℕ) →
      (rk : α) →
        (rv : β rk) →
          (rls : ℕ) →
            (rlk : α) →
              (rlv : β rlk) →
                (rll rlr rr : Std.DTreeMap.Internal.Impl α β) →
                  (size : ℕ) →
                    (k : α) →
                      (v : β k) →
                        (l r : Std.DTreeMap.Internal.Impl α β) →
                          rr = Std.DTreeMap.Internal.Impl.inner size k v l r →
                            motive
                              (Std.DTreeMap.Internal.Impl.inner rs rk rv
                                (Std.DTreeMap.Internal.Impl.inner rls rlk rlv rll rlr)
                                (Std.DTreeMap.Internal.Impl.inner size k v l r)))
  (size : ℕ) (k : α) (v : β k),
  r = Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf →
    (match r with
      | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
      | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf =>
        h_2 size k v
      |
      Std.DTreeMap.Internal.Impl.inner size rk rv Std.DTreeMap.Internal.Impl.leaf
          rr@h:(Std.DTreeMap.Internal.Impl.inner size_1 k v l r) =>
        h_3 size rk rv rr size_1 k v l r h
      |
      Std.DTreeMap.Internal.Impl.inner size rk rv (Std.DTreeMap.Internal.Impl.inner size_1 rlk rlv l r)
          Std.DTreeMap.Internal.Impl.leaf =>
        h_4 size rk rv size_1 rlk rlv l r
      |
      Std.DTreeMap.Internal.Impl.inner rs rk rv (Std.DTreeMap.Internal.Impl.inner rls rlk rlv rll rlr)
          rr@h:(Std.DTreeMap.Internal.Impl.inner size k v l r) =>
        h_5 rs rk rv rls rlk rlv rll rlr rr size k v l r h) ≍
      h_2 size k v
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.HomologyData.map_right : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : S.HomologyData)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : h.left.IsPreservedBy F]
  [inst_6 : h.right.IsPreservedBy F], (h.map F).right = h.right.map F
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.natDegree_map : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] [Nontrivial S] {P : Polynomial R},
  P.Monic → ∀ (f : R →+* S), (Polynomial.map f P).natDegree = P.natDegree
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.Arrow.augmentedCechConerve_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C)
  [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom]
  (x : SimplexCategory), f.augmentedCechConerve.hom.app x = CategoryTheory.Limits.WidePushout.head fun x => f.hom
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.endofunctorMonoidalCategory_tensorUnit_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : C),
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor C C)).obj X = X
-- Init.Data.SInt.Lemmas
ISize.ofBitVec_int16ToBitVec : ∀ (x : Int16), ISize.ofBitVec (BitVec.signExtend System.Platform.numBits x.toBitVec) = x.toISize
-- Lean.Elab.Tactic.RCases
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.processConstructor.match_1.eq_1 : ∀ (motive : List Lean.Name × List Lean.Elab.Tactic.RCases.RCasesPatt → Sort u_1) (ns : List Lean.Name)
  (tl : List Lean.Elab.Tactic.RCases.RCasesPatt)
  (h_1 : (ns : List Lean.Name) → (tl : List Lean.Elab.Tactic.RCases.RCasesPatt) → motive (ns, tl)),
  (match (ns, tl) with
    | (ns, tl) => h_1 ns tl) =
    h_1 ns tl
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basis
Module.Basis.symmetricAlgebra_repr_apply : ∀ {κ : Type uκ} {R : Type uR} {M : Type uM} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis κ R M) (x : SymmetricAlgebra R M),
  b.symmetricAlgebra.repr x = (MvPolynomial.basisMonomials κ R).repr ((SymmetricAlgebra.equivMvPolynomial b) x)
-- Mathlib.Topology.Algebra.Constructions
/-- `AddOpposite.op` as a homeomorphism.  -/
AddOpposite.opHomeomorph : {M : Type u_1} → [inst : TopologicalSpace M] → M ≃ₜ Mᵃᵒᵖ
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight.go_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {n w : ℕ} (aig : Std.Sat.AIG α) (distance : aig.RefVec n)
  (curr : ℕ) (acc : aig.RefVec w),
  aig.decls.size ≤ (Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight.go aig distance curr acc).aig.decls.size
-- Mathlib.RingTheory.Etale.Kaehler
Algebra.tensorH1CotangentOfIsLocalization.eq_1 : ∀ (R : Type u_1) {S : Type u_2} (T : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] (M : Submonoid S)
  [inst_7 : IsLocalization M T],
  Algebra.tensorH1CotangentOfIsLocalization R T M =
    (Algebra.Extension.tensorH1CotangentOfFormallyEtale
          {
            toRingHom :=
              algebraMap (Algebra.Generators.self R S).toExtension.Ring
                (Localization (Submonoid.comap (algebraMap (Algebra.Generators.self R S).toExtension.Ring S) M)),
            toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
          ⋯ ⋯ ⋯).trans
      (Algebra.Extension.ofSurjective (IsLocalization.liftAlgHom ⋯) ⋯).equivH1CotangentOfFormallySmooth
-- Mathlib.Order.Filter.Map
Filter.comap_iInf : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {m : α → β} {f : ι → Filter β},
  Filter.comap m (⨅ i, f i) = ⨅ i, Filter.comap m (f i)
-- Mathlib.Topology.Order.Compact
IsCompact.exists_sInf_image_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [inst_2 : TopologicalSpace β] [ClosedIicTopology α] {s : Set β},
  IsCompact s → s.Nonempty → ∀ {f : β → α}, ContinuousOn f s → ∃ x ∈ s, sInf (f '' s) = f x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_erase! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k a fallback : α},
      (Std.DTreeMap.Internal.Impl.erase! k t).getKeyD a fallback =
        if compare k a = Ordering.eq then fallback else t.getKeyD a fallback
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
/-- Predicate saying that a given set is measurable. Use `MeasurableSet` in the root namespace
instead.  -/
MeasurableSpace.MeasurableSet' : {α : Type u_7} → MeasurableSpace α → Set α → Prop
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.ofSliceTo_next : ∀ {s : String.Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {h : p ≠ (s.sliceTo p₀).endPos},
  String.Slice.Pos.ofSliceTo (p.next h) = (String.Slice.Pos.ofSliceTo p).next ⋯
-- Mathlib.Analysis.InnerProductSpace.TwoDim
/-- Continuous linear map version of `Orientation.areaForm`, useful for calculus.  -/
Orientation.areaForm' : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] → [Fact (Module.finrank ℝ E = 2)] → Orientation ℝ E (Fin 2) → E →L[ℝ] E →L[ℝ] ℝ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_modify : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k : α} {f : β k → β k}, m.WF → (m.modify k f).size = m.size
-- Mathlib.RingTheory.ZariskisMainTheorem
Algebra.ZariskisMainProperty.trans : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] (p : Ideal T) [p.IsPrime],
  Algebra.ZariskisMainProperty R (Ideal.under S p) →
    (∃ r ∉ Ideal.under S p, ⊥.saturation (Submonoid.powers ((algebraMap S T) r)) ⋯ = ⊤) →
      Algebra.ZariskisMainProperty R p
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.dfold.loop.eq_1 : ∀ (n : ℕ) {α : (i : ℕ) → autoParam (i ≤ n) Nat.dfold._auto_1 → Type u} (f : (i : ℕ) → (h : i < n) → α i ⋯ → α (i + 1) ⋯)
  (h : 0 ≤ n) (a : α (n - 0) ⋯), Nat.dfold.loop✝ n f 0 h a = a
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_true_clz_of_ne_zero : ∀ {w : ℕ} {x : BitVec w}, 0 < w → x ≠ 0#w → x.getLsbD (w - 1 - x.clz.toNat) = true
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.ReflQuiv.adj.unit.map_app_eq : ∀ (V : Type u) [inst : CategoryTheory.ReflQuiver V],
  (CategoryTheory.ReflQuiv.adj.unit.app (CategoryTheory.ReflQuiv.of V)).toPrefunctor =
    CategoryTheory.Quiv.adj.unit.app (CategoryTheory.Quiv.of V) ⋙q
      (CategoryTheory.Cat.FreeRefl.quotientFunctor V).toPrefunctor
-- Lean.Setup
Lean.ImportArtifacts.olean? : Lean.ImportArtifacts → Option System.FilePath
-- Mathlib.Data.Set.Finite.Basic
/-- **Alias** of `Set.toFinset_sdiff`. -/
Set.Finite.toFinset_diff : ∀ {α : Type u_1} (s t : Set α) [inst : DecidableEq α] [inst_1 : Fintype ↑s] [inst_2 : Fintype ↑t]
  [inst_3 : Fintype ↑(s \ t)], (s \ t).toFinset = s.toFinset \ t.toFinset
-- Mathlib.RingTheory.Polynomial.Tower
Subalgebra.aeval_coe : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R A) (x : ↥S) (p : Polynomial R), (Polynomial.aeval ↑x) p = ↑((Polynomial.aeval x) p)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.inv_prodComparison_map_snd : ∀ {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) (A B : C)
  [inst_4 : CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B)],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.inv (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B))
      (F.map (CategoryTheory.SemiCartesianMonoidalCategory.snd A B)) =
    CategoryTheory.SemiCartesianMonoidalCategory.snd (F.obj A) (F.obj B)
-- Mathlib.Algebra.CharP.Lemmas
sub_pow_char_pow_of_commute : ∀ {R : Type u_1} [inst : Ring R] {x y : R} (p n : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p],
  Commute x y → (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
-- Mathlib.Order.OrderIsoNat
RelEmbedding.coe_natGT : ∀ {α : Type u_1} {r : α → α → Prop} [inst : IsStrictOrder α r] {f : ℕ → α} {H : ∀ (n : ℕ), r (f (n + 1)) (f n)},
  ⇑(RelEmbedding.natGT f H) = f
-- Mathlib.RingTheory.DividedPowers.Basic
DividedPowers.coe_injective : ∀ {A : Type u_1} [inst : CommSemiring A] (I : Ideal A), Function.Injective fun h => h.dpow
-- Mathlib.Algebra.Group.Units.Basic
Units.inv_unique : ∀ {α : Type u} [inst : Monoid α] {u₁ u₂ : αˣ}, ↑u₁ = ↑u₂ → ↑u₁⁻¹ = ↑u₂⁻¹
-- Lean.Data.Name
/-- The frontend does not allow user declarations to start with `_` in any of its parts.
We use name parts starting with `_` internally to create auxiliary names (e.g., `_private`).

This function checks if any component of the name starts with `_`, or is numeric.
 -/
Lean.Name.isInternalOrNum : Lean.Name → Bool
-- Mathlib.Algebra.Homology.Additive
ChainComplex.map_chain_complex_of : ∀ {W₁ : Type u_3} {W₂ : Type u_4} [inst : CategoryTheory.Category.{v_2, u_3} W₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_4} W₂] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms W₁]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms W₂] {α : Type u_5} [inst_4 : AddRightCancelSemigroup α]
  [inst_5 : One α] [inst_6 : DecidableEq α] (F : CategoryTheory.Functor W₁ W₂) [inst_7 : F.PreservesZeroMorphisms]
  (X : α → W₁) (d : (n : α) → X (n + 1) ⟶ X n)
  (sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d (n + 1)) (d n) = 0),
  (F.mapHomologicalComplex (ComplexShape.down α)).obj (ChainComplex.of X d sq) =
    ChainComplex.of (fun n => F.obj (X n)) (fun n => F.map (d n)) ⋯
-- Mathlib.RingTheory.Valuation.Discrete.Basic
/-- The structure `Uniformizer` bundles together the term in the ring and a proof that it is a
uniformizer.  -/
Valuation.Uniformizer : {Γ : Type u_1} →
  [inst : LinearOrderedCommGroupWithZero Γ] →
    {A : Type u_2} → [inst_1 : Ring A] → (v : Valuation A Γ) → [hv : v.IsRankOneDiscrete] → Type u_2
-- Mathlib.Topology.Algebra.Order.Floor
tendsto_fract_right : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] [inst_3 : TopologicalSpace α]
  [IsStrictOrderedRing α] [OrderClosedTopology α] [IsTopologicalAddGroup α] (n : ℤ),
  Filter.Tendsto Int.fract (nhdsWithin (↑n) (Set.Ici ↑n)) (nhdsWithin 0 (Set.Ici 0))
-- Mathlib.Geometry.Convex.ConvexSpace.AffineMap
Convexity.ConvexSpace.AffineMap.assoc : ∀ {R : Type u_1} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R] {X : Type u_2}
  {Y : Type u_3} {Z : Type u_4} {T : Type u_5} [inst_3 : Convexity.ConvexSpace R X] [inst_4 : Convexity.ConvexSpace R Y]
  [inst_5 : Convexity.ConvexSpace R Z] [inst_6 : Convexity.ConvexSpace R T] (f₁ : Convexity.ConvexSpace.AffineMap R Z T)
  (f₂ : Convexity.ConvexSpace.AffineMap R Y Z) (f₃ : Convexity.ConvexSpace.AffineMap R X Y),
  (f₁.comp f₂).comp f₃ = f₁.comp (f₂.comp f₃)
-- Std.Time.Zoned.Database.TZdb
/-- Parses the value of the `TZ` environment variable. Returns `none` for empty or
`:` (empty path after the colon) values.
 -/
Std.Time.Database.TZdb.parseTZValue : String → Option Std.Time.Database.TZdb.TZSpec
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.smul_mem_smul : ∀ {R : Type u_2} {A : Type u_3} [inst : AddMonoid R] [inst_1 : AddMonoid A] [inst_2 : DistribSMul R A]
  {M : AddSubmonoid R} {N : AddSubmonoid A} {m : R} {n : A}, m ∈ M → n ∈ N → m • n ∈ M • N
-- Mathlib.Algebra.Polynomial.Degree.SmallDegree
Polynomial.le_natDegree_of_coe_le_degree : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R}, ↑n ≤ p.degree → n ≤ p.natDegree
-- Mathlib.RingTheory.Perfectoid.FontaineTheta
WittVector.fontaineTheta.congr_simp : ∀ (R : Type u) [inst : CommRing R] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : Fact ¬IsUnit ↑p]
  [inst_3 : IsAdicComplete (Ideal.span {↑p}) R], WittVector.fontaineTheta R p = WittVector.fontaineTheta R p
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioo_map_sectR : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : DecidableLE (α × β)] (c : α) (a b : β),
  Finset.map (Function.Embedding.sectR c β) (Finset.Ioo a b) = Finset.Ioo (c, a) (c, b)