mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Enumerative.Catalan.Basic
_private.Mathlib.Combinatorics.Enumerative.Catalan.Basic.0.gosperCatalan.eq_1 : ∀ (n j : ℕ), gosperCatalan✝ n j = ↑j.centralBinom * ↑(n - j).centralBinom * (2 * ↑j - ↑n) / (2 * ↑n * (↑n + 1))
-- Aesop.Rule.Name
Aesop.BuilderName.constructors.sizeOf_spec : sizeOf Aesop.BuilderName.constructors = 1
-- Mathlib.Data.Nat.Factorial.Basic
Nat.pow_lt_ascFactorial : ∀ (n : ℕ) {k : ℕ}, 2 ≤ k → (n + 1) ^ k < (n + 1).ascFactorial k
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.isUnit_Y_of_Z_eq_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F},
  W.Nonsingular P → P 2 = 0 → IsUnit (P 1)
-- Mathlib.Tactic.Order.Graph.Tarjan
/-- Implementation of `findSCCs` in the `StateM TarjanState` monad.  -/
Mathlib.Tactic.Order.Graph.findSCCsImp : Mathlib.Tactic.Order.Graph → StateM Mathlib.Tactic.Order.Graph.TarjanState Unit
-- Init.Data.Nat.Bitwise.Lemmas
Nat.testBit_two_pow_sub_one : ∀ (n i : ℕ), (2 ^ n - 1).testBit i = decide (i < n)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_congr : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF → ∀ {a b : α}, (a == b) = true → Std.DHashMap.Raw.Const.get? m a = Std.DHashMap.Raw.Const.get? m b
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.MorphismProperty.regularMono.respectsIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C], (CategoryTheory.MorphismProperty.regularMono C).RespectsIso
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.map_comp_map : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g h : α → C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct f] [inst_2 : CategoryTheory.Limits.HasCoproduct g]
  [inst_3 : CategoryTheory.Limits.HasCoproduct h] (q : (a : α) → f a ⟶ g a) (q' : (a : α) → g a ⟶ h a),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.map q) (CategoryTheory.Limits.Sigma.map q') =
    CategoryTheory.Limits.Sigma.map fun a => CategoryTheory.CategoryStruct.comp (q a) (q' a)
-- Mathlib.Topology.Category.TopCat.Sphere
/-- `∂𝔻 n` denotes the boundary of the `n`-disk.  -/
TopCat.«term∂𝔻_» : Lean.ParserDescr
-- Mathlib.Algebra.Order.Antidiag.Nat
Nat.lcm.eq_1 : ∀ (m n : ℕ), m.lcm n = m * n / m.gcd n
-- Mathlib.Order.Heyting.Hom
/-- The proposition that a bi-Heyting homomorphism preserves the difference operation.  -/
BiheytingHomClass.map_sdiff : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} {inst : BiheytingAlgebra α} {inst_1 : BiheytingAlgebra β}
  {inst_2 : FunLike F α β} [self : BiheytingHomClass F α β] (f : F) (a b : α), f (a \ b) = f a \ f b
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.exp_add : ∀ {M : Type u_4} [inst : AddMonoid M] (a b : M), WithZero.exp (a + b) = WithZero.exp a * WithZero.exp b
-- Mathlib.Data.Subtype
Subtype.map_eq : ∀ {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} {f g : α → β} (h₁ : ∀ (a : α), p a → q (f a))
  (h₂ : ∀ (a : α), p a → q (g a)) {x y : Subtype p}, Subtype.map f h₁ x = Subtype.map g h₂ y ↔ f ↑x = g ↑y
-- Mathlib.MeasureTheory.Group.Arithmetic
measurableSMul₂_of_add : ∀ (M : Type u_2) [inst : Add M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M], MeasurableVAdd₂ M M
-- Mathlib.Condensed.Functors
/-- Dot notation for the value of `compHausToCondensed`.  -/
CompHaus.toCondensed : CompHaus → CondensedSet
-- Init.Data.Vector.Lemmas
Vector.forall_getElem : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {p : α → Prop}, (∀ (i : ℕ) (h : i < n), p xs[i]) ↔ ∀ a ∈ xs, p a
-- Mathlib.RingTheory.FractionalIdeal.Operations
/-- If the numerator ideal of a fractional ideal is principal, then so is the fractional ideal.  -/
FractionalIdeal.isPrincipal_of_isPrincipal_num : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] (I : FractionalIdeal (nonZeroDivisors R) (FractionRing R)),
  Submodule.IsPrincipal I.num → (↑I).IsPrincipal
-- Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
CategoryTheory.StructuredArrow.commaMapEquivalenceInverse_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T}
  {R : CategoryTheory.Functor D T} {C' : Type u₄} [inst_3 : CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅}
  [inst_4 : CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T']
  {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'}
  {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F)
  (β : R.comp F ⟶ F₂.comp R') [inst_6 : CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R')
  (Y :
    CategoryTheory.Comma (CategoryTheory.StructuredArrow.map₂ (CategoryTheory.CategoryStruct.id (L'.obj X.left)) α)
      (CategoryTheory.StructuredArrow.map₂ X.hom (CategoryTheory.inv β))),
  (CategoryTheory.StructuredArrow.commaMapEquivalenceInverse α β X).obj Y =
    CategoryTheory.StructuredArrow.mk { left := Y.left.hom, right := Y.right.hom, w := ⋯ }
-- Mathlib.Algebra.Order.CauSeq.Basic
IsCauSeq.cauchy₃ : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [IsAbsoluteValue abv] {f : ℕ → β},
  IsCauSeq abv f → ∀ {ε : α}, 0 < ε → ∃ i, ∀ j ≥ i, ∀ k ≥ j, abv (f k - f j) < ε
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k fallback : α}, k ∉ m₂ → (m₁ ∪ m₂).getKeyD k fallback = m₁.getKeyD k fallback
-- Lean.Parser.Term
Lean.Parser.Term.macroArg : Lean.Parser.Parser
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_eq_some_get : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α} (h' : a ∈ t), t.get? a = some (t.get a h')
-- Mathlib.Data.ENNReal.Basic
ENNReal.instAddCommMonoidWithOne : AddCommMonoidWithOne ENNReal
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.mkInjectiveTheoremValue : Lean.Name → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.iterated_mateEquiv_conjugateEquiv_symm : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} {f₁ : a ⟶ c} {u₁ : c ⟶ a} {f₂ : b ⟶ d} {u₂ : d ⟶ b}
  {l₁ : a ⟶ b} {r₁ : b ⟶ a} {l₂ : c ⟶ d} {r₂ : d ⟶ c} (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁)
  (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂) (adj₃ : CategoryTheory.Bicategory.Adjunction f₁ u₁)
  (adj₄ : CategoryTheory.Bicategory.Adjunction f₂ u₂)
  (α : CategoryTheory.CategoryStruct.comp u₂ r₁ ⟶ CategoryTheory.CategoryStruct.comp r₂ u₁),
  (CategoryTheory.Bicategory.mateEquiv adj₁ adj₂).symm ((CategoryTheory.Bicategory.mateEquiv adj₄ adj₃).symm α) =
    (CategoryTheory.Bicategory.conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)).symm α
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpParams.context? : Lean.Lsp.SignatureHelpParams → Option Lean.Lsp.SignatureHelpContext
-- Mathlib.CategoryTheory.Shift.Twist
CategoryTheory.TwistShiftData.z_zero_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type w} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (t : CategoryTheory.TwistShiftData C A) (b : A), t.z 0 b = 1
-- Init.Data.UInt.Bitwise
USize.not_inj : ∀ {a b : USize}, ~~~a = ~~~b ↔ a = b
-- Mathlib.GroupTheory.ArchimedeanDensely
/-- Any nontrivial (has other than 0 and 1) linearly ordered mul-archimedean group with zero is
either isomorphic (and order-isomorphic) to `ℤᵐ⁰`, or is densely ordered, exclusively  -/
LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered : ∀ (G : Type u_2) [inst : LinearOrderedCommGroupWithZero G] [Nontrivial Gˣ] [MulArchimedean G],
  Nonempty (G ≃*o WithZero (Multiplicative ℤ)) ↔ ¬DenselyOrdered G
-- Mathlib.Analysis.Complex.Exponential
Real.exp_approx_end' : ∀ {n : ℕ} {x a b : ℝ} (m : ℕ),
  n + 1 = m →
    ∀ (rm : ℝ),
      ↑m = rm →
        |x| ≤ 1 →
          |1 - a| ≤ b - |x| / rm * ((rm + 1) / rm) → |Real.exp x - Real.expNear n x a| ≤ |x| ^ n / ↑n.factorial * b
-- Mathlib.Data.Seq.Computation
_private.Mathlib.Data.Seq.Computation.0.Computation.LiftRelAux.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : α ⊕ Computation α → β ⊕ Computation β → Sort u_3) →
      (x : α ⊕ Computation α) →
        (x_1 : β ⊕ Computation β) →
          ((a : α) → (b : β) → motive (Sum.inl a) (Sum.inl b)) →
            ((a : α) → (cb : Computation β) → motive (Sum.inl a) (Sum.inr cb)) →
              ((ca : Computation α) → (b : β) → motive (Sum.inr ca) (Sum.inl b)) →
                ((ca : Computation α) → (cb : Computation β) → motive (Sum.inr ca) (Sum.inr cb)) → motive x x_1
-- Mathlib.Algebra.Notation.Lemmas
ite_nonpos : ∀ {α : Type u_1} [inst : Zero α] {p : Prop} [inst_1 : Decidable p] {a b : α} [inst_2 : LE α],
  a ≤ 0 → b ≤ 0 → (if p then a else b) ≤ 0
-- Mathlib.Data.Part
Part.get_eq_of_mem : ∀ {α : Type u_1} {o : Part α} {a : α}, a ∈ o → ∀ (h' : o.Dom), o.get h' = a
-- Mathlib.Order.DirectedInverseSystem
DirectLimit.lift_injective : ∀ {ι : Type u_1} [inst : Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
  (f : (i j : ι) → (h : i ≤ j) → T h) [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
  [inst_2 : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] {C : Sort u_9}
  (ih : (i : ι) → F i → C) (compat : ∀ (i j : ι) (h : i ≤ j) (x : F i), ih i x = ih j ((f i j h) x)),
  (∀ (i : ι), Function.Injective (ih i)) → Function.Injective (DirectLimit.lift f ih compat)
-- Std.Sat.AIG.Relabel
Std.Sat.AIG.relabel.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Type} [inst_2 : Hashable β] [inst_3 : DecidableEq β]
  (r : α → β) (aig : Std.Sat.AIG α),
  Std.Sat.AIG.relabel r aig =
    { decls := Array.map (Std.Sat.AIG.Decl.relabel r) aig.decls, cache := Std.Sat.AIG.Cache.empty, hdag := ⋯,
      hzero := ⋯, hconst := ⋯ }
-- Mathlib.Algebra.Star.Free
FreeAlgebra.star_ι : ∀ {R : Type u_1} [inst : CommSemiring R] {X : Type u_2} (x : X), star (FreeAlgebra.ι R x) = FreeAlgebra.ι R x
-- Mathlib.Topology.UniformSpace.Defs
/-- The ball around `(x : β)` with respect to `(V : Set (β × β))`. Intended to be
used for `V ∈ 𝓤 β`, but this is not needed for the definition. Recovers the
notions of metric space ball when `V = {p | dist p.1 p.2 < r }`.  -/
UniformSpace.ball : {β : Type ub} → β → Set (β × β) → Set β
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.Precoverage.Saturate.below.pullback : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {J : CategoryTheory.Precoverage C}
  {motive : (X : C) → (a : CategoryTheory.Sieve X) → J.Saturate X a → Prop} (X : C) (S : CategoryTheory.Sieve X)
  (a : J.Saturate X S) (Y : C) (f : Y ⟶ X),
  CategoryTheory.Precoverage.Saturate.below a → motive X S a → CategoryTheory.Precoverage.Saturate.below ⋯
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.containsThenInsertIfNew_snd : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β k}, (t.containsThenInsertIfNew k v).2 = t.insertIfNew k v
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {R₁ R₂ : CategoryTheory.ComposableArrows C 3} (φ : R₁ ⟶ R₂),
  R₁.Exact →
    R₂.Exact →
      CategoryTheory.Epi
          (CategoryTheory.ComposableArrows.app' φ 0 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_13) →
        CategoryTheory.Mono
            (CategoryTheory.ComposableArrows.app' φ 1 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_11) →
          CategoryTheory.Mono
              (CategoryTheory.ComposableArrows.app' φ 3 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_7) →
            CategoryTheory.Mono
              (CategoryTheory.ComposableArrows.app' φ 2 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_4)
-- Init.Data.UInt.Bitwise
UInt16.ne_not_self : ∀ {a : UInt16}, a ≠ ~~~a
-- Aesop.Search.Main
Aesop.handleNonfatalError : {Q : Type} → [inst : Aesop.Queue Q] → Lean.MessageData → Aesop.SearchM Q (Array Lean.MVarId)
-- Init.Data.Range.Polymorphic.PRange
Std.Rxo.IsAlwaysFinite.mk : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α],
  (∀ (init hi : α), ∃ n, (Std.PRange.succMany? n init).elim True fun x => ¬x < hi) → Std.Rxo.IsAlwaysFinite α
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.find?_toList_eq_some_iff_get?_eq_some : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF → ∀ {k : α} {v : β k}, List.find? (fun x => x.fst == k) (↑m).toList = some ⟨k, v⟩ ↔ m.get? k = some v
-- Mathlib.AlgebraicTopology.ModelCategory.Homotopy
HomotopicalAlgebra.RightHomotopyClass.precomp_bijective_of_weakEquivalence : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C} (Z : C)
  [HomotopicalAlgebra.IsFibrant Z] (f : X ⟶ Y) [HomotopicalAlgebra.IsCofibrant X] [HomotopicalAlgebra.IsCofibrant Y]
  [HomotopicalAlgebra.WeakEquivalence f], Function.Bijective fun g => g.precomp f
-- Mathlib.Topology.PartitionOfUnity
PartitionOfUnity.exists_finset_nhds : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] (ρ : PartitionOfUnity ι X) (x₀ : X),
  ∃ I, ∀ᶠ (x : X) in nhds x₀, ∑ i ∈ I, (ρ i) x = 1 ∧ (Function.support fun x_1 => (ρ x_1) x) ⊆ ↑I
-- Init.Data.UInt.Bitwise
UInt64.toFin_not : ∀ (a : UInt64), (~~~a).toFin = a.toFin.rev
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
/-- Given a braiding `β : curriedTensor C ≅ (curriedTensor C).flip` as a natural isomorphism between
bifunctors, and the two equalities `hexagon_forward` and `hexagon_reverse` of natural
transformations between trifunctors, we obtain a braided category structure.
 -/
CategoryTheory.BraidedCategory.ofBifunctor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (β : CategoryTheory.MonoidalCategory.curriedTensor C ≅ (CategoryTheory.MonoidalCategory.curriedTensor C).flip) →
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.curriedAssociatorNatIso C).hom
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.BraidedCategory.ofBifunctor.Forward.firstMap₂ β)
                (CategoryTheory.BraidedCategory.ofBifunctor.Forward.firstMap₃ C)) =
            CategoryTheory.CategoryStruct.comp (CategoryTheory.BraidedCategory.ofBifunctor.Forward.secondMap₁ β)
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.BraidedCategory.ofBifunctor.Forward.secondMap₂ C)
                (CategoryTheory.BraidedCategory.ofBifunctor.Forward.secondMap₃ β)) →
          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.curriedAssociatorNatIso C).inv
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.BraidedCategory.ofBifunctor.Reverse.firstMap₂ β)
                  (CategoryTheory.BraidedCategory.ofBifunctor.Reverse.firstMap₃ C)) =
              CategoryTheory.CategoryStruct.comp (CategoryTheory.BraidedCategory.ofBifunctor.Reverse.secondMap₁ β)
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.BraidedCategory.ofBifunctor.Reverse.secondMap₂ C)
                  (CategoryTheory.BraidedCategory.ofBifunctor.Reverse.secondMap₃ β)) →
            CategoryTheory.BraidedCategory C
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk.eq_1 : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] (a : M),
  ArchimedeanClass.mk a = toAntisymmetrization (fun x1 x2 => x1 ≤ x2) (ArchimedeanOrder.of a)
-- Mathlib.Topology.LocallyFinsupp
LocallyFiniteSupport.locallyFinite_support : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_2} [inst_1 : Zero Y] (f : X → Y),
  LocallyFiniteSupport f → LocallyFinite fun s => {↑s}
-- Mathlib.Topology.Algebra.UniformConvergence
UniformOnFun.hasBasis_nhds_zero_of_basis : ∀ {α : Type u_1} {G : Type u_2} {ι : Type u_3} [inst : AddGroup G] [inst_1 : UniformSpace G] [IsUniformAddGroup G]
  (𝔖 : Set (Set α)),
  𝔖.Nonempty →
    DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖 →
      ∀ {p : ι → Prop} {b : ι → Set G},
        (nhds 0).HasBasis p b →
          (nhds 0).HasBasis (fun Si => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si =>
            {f | ∀ x ∈ Si.1, (UniformOnFun.toFun 𝔖) f x ∈ b Si.2}
-- Init.Data.UInt.Lemmas
USize.toNat.eq_1 : ∀ (n : USize), n.toNat = n.toBitVec.toNat
-- Mathlib.Algebra.BigOperators.Ring.Finset
Nat.cast_list_sum : ∀ {R : Type u_4} [inst : AddMonoidWithOne R] (s : List ℕ), ↑s.sum = (List.map Nat.cast s).sum
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α} {k k' fallback : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (Std.TreeSet.Raw.ofList l cmp).getD k' fallback = k
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.forIn.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w₂} [inst : Monad m]
  [inst_1 : LawfulMonad m] [inst_2 : Std.TransCmp cmp] (f f_1 : (a : α) → β a → δ → m (ForInStep δ)),
  f = f_1 →
    ∀ (init init_1 : δ),
      init = init_1 →
        ∀ (t t_1 : Std.ExtDTreeMap α β cmp),
          t = t_1 → Std.ExtDTreeMap.forIn f init t = Std.ExtDTreeMap.forIn f_1 init_1 t_1
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- If `y` is a conjugate root of `x` in some division ring and `f` is an `R`-algebra homomorphism, then
`f y` is a conjugate root of `f x`.
 -/
isConjRoot_algHom_iff : ∀ {R : Type u_1} {B : Type u_6} [inst : CommRing R] [inst_1 : Ring B] [inst_2 : Algebra R B] {A : Type u_7}
  [inst_3 : DivisionRing A] [inst_4 : Algebra R A] [Nontrivial B] {x y : A} (f : A →ₐ[R] B),
  IsConjRoot R (f x) (f y) ↔ IsConjRoot R x y
-- Mathlib.MeasureTheory.MeasurableSpace.Instances
Nat.instMeasurableSingletonClass : MeasurableSingletonClass ℕ
-- Mathlib.AlgebraicGeometry.Noetherian
AlgebraicGeometry.IsNoetherian.mk : ∀ {X : AlgebraicGeometry.Scheme} [toIsLocallyNoetherian : AlgebraicGeometry.IsLocallyNoetherian X]
  [toCompactSpace : CompactSpace ↥X], AlgebraicGeometry.IsNoetherian X
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.existsPairNE.sizeOf_spec : sizeOf FirstOrder.Field.FieldAxiom.existsPairNE = 1
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
CategoryTheory.Limits.PreservesPullback.iso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_2 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G]
  [inst_3 : CategoryTheory.Limits.HasPullback f g] [inst_4 : CategoryTheory.Limits.HasPullback (G.map f) (G.map g)],
  CategoryTheory.Limits.PreservesPullback.iso G f g =
    CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso
      (CategoryTheory.Limits.isLimitOfHasPullbackOfPreservesLimit G f g)
      (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Limits.cospan (G.map f) (G.map g)))
-- Mathlib.Topology.Sequences
SeqCompactSpace.tendsto_subseq : ∀ {X : Type u_1} [inst : TopologicalSpace X] [SeqCompactSpace X] (x : ℕ → X),
  ∃ a φ, StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (nhds a)
-- Lean.Meta.LazyDiscrTree
/-- Create a key path from an expression using the function used for patterns.

This differs from Lean.Meta.DiscrTree.mkPath and targetPath in that the expression
should uses free variables rather than meta-variables for holes.
 -/
Lean.Meta.LazyDiscrTree.patternPath : Lean.Expr → Lean.MetaM (Array Lean.Meta.LazyDiscrTree.Key)
-- Init.Grind.Ordered.Field
Lean.Grind.Field.IsOrdered.mul_lt_mul_iff_of_pos_left : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] {a b c : R}, 0 < c → (c * a < c * b ↔ a < b)
-- Batteries.Data.String.Lemmas
Substring.Raw.ValidFor.atEnd : ∀ {l m r : List Char} {p : ℕ} {s : Substring.Raw},
  Substring.Raw.ValidFor l m r s → (s.atEnd { byteIdx := p } = true ↔ p = String.utf8Len m)
-- Mathlib.Data.Vector.Basic
List.Vector.scanl.eq_1 : ∀ {α : Type u_1} {n : ℕ} {β : Type u_6} (f : β → α → β) (b : β) (v : List.Vector α n),
  List.Vector.scanl f b v = ⟨List.scanl f b v.toList, ⋯⟩
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
MeasureTheory.OuterMeasure.isCaratheodory_disjointed : ∀ {α : Type u} (m : MeasureTheory.OuterMeasure α) {ι : Type u_1} [inst : Preorder ι] [inst_1 : LocallyFiniteOrderBot ι]
  {s : ι → Set α}, (∀ (i : ι), m.IsCaratheodory (s i)) → ∀ (i : ι), m.IsCaratheodory (disjointed s i)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.size_alter_eq_add_one : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : Option β → Option β},
  k ∉ t → (f (Std.ExtDTreeMap.Const.get? t k)).isSome = true → (Std.ExtDTreeMap.Const.alter t k f).size = t.size + 1
-- Init.Data.Array.Subarray
instSelfSliceSubarrayDataSubarray : ∀ {α : Type u}, Std.Slice.Self (Std.Slice (Std.Slice.Internal.SubarrayData α)) (Subarray α)
-- Mathlib.Topology.Inseparable
inseparable_iff_forall_isOpen : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, Inseparable x y ↔ ∀ (s : Set X), IsOpen s → (x ∈ s ↔ y ∈ s)
-- Mathlib.RingTheory.PowerSeries.WellKnown
PowerSeries.invUnitsSub_mul_X : ∀ {R : Type u_1} [inst : Ring R] (u : Rˣ),
  PowerSeries.invUnitsSub u * PowerSeries.X = PowerSeries.invUnitsSub u * PowerSeries.C ↑u - 1
-- Mathlib.Analysis.Normed.Field.Basic
norm_div : ∀ {α : Type u_2} [inst : NormedDivisionRing α] (a b : α), ‖a / b‖ = ‖a‖ / ‖b‖
-- Mathlib.Topology.TietzeExtension
/-- Any homeomorphism from a `TietzeExtension` space is one itself.  -/
TietzeExtension.of_homeo : ∀ {Y : Type v} {Z : Type w} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace Z] [TietzeExtension Z] (e : Y ≃ₜ Z),
  TietzeExtension Y
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- If there is a primitive `n`-th root of unity in `K`, then `X ^ n - 1` splits.  -/
Polynomial.X_pow_sub_one_splits : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {n : ℕ}, IsPrimitiveRoot ζ n → (Polynomial.X ^ n - Polynomial.C 1).Splits
-- Mathlib.Analysis.Calculus.Deriv.Basic
derivWithin_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (s : Set 𝕜) (c : F), derivWithin (Function.const 𝕜 c) s = 0
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inr_fst_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  {d e f : ℤ} (γ : CochainComplex.HomComplex.Cochain F K d) (he : 1 + d = e) (hf : 0 + e = f),
  (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)).comp
      ((↑(CochainComplex.mappingCone.fst φ)).comp γ he) hf =
    0
-- Mathlib.CategoryTheory.Monad.Comonadicity
/-- The "main pair" for a coalgebra `(A, α)` is the pair of morphisms `(G α, η_GA)`. It is always a
coreflexive pair, and will be used to construct the left adjoint to the comparison functor and show
it is an equivalence.
 -/
CategoryTheory.Comonad.ComonadicityInternal.main_pair_coreflexive : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (A : adj.toComonad.Coalgebra),
  CategoryTheory.IsCoreflexivePair (G.map A.a) (adj.unit.app (G.obj A.A))
-- Mathlib.Algebra.BigOperators.Finprod
finsum_mem_def : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (s : Set α) (f : α → M),
  ∑ᶠ (a : α) (_ : a ∈ s), f a = ∑ᶠ (a : α), s.indicator f a