mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Pattern.String
_private.Init.Data.String.Pattern.String.0.String.Slice.Pattern.ForwardSliceSearcher.instIteratorIdSearchStep.match_3.eq_3 : ∀ (s : String.Slice)
  (motive :
    Std.IterStep (Std.IterM Id (String.Slice.Pattern.SearchStep s)) (String.Slice.Pattern.SearchStep s) → Sort u_1)
  (h_1 :
    (it' : Std.IterM Id (String.Slice.Pattern.SearchStep s)) →
      (out : String.Slice.Pattern.SearchStep s) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM Id (String.Slice.Pattern.SearchStep s)) → motive (Std.IterStep.skip it'))
  (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_monomial : ∀ {R : Type u} [inst : Semiring R] {x : R} {n : ℕ} {a : R}, Polynomial.eval x ((Polynomial.monomial n) a) = a * x ^ n
-- Mathlib.Topology.Algebra.Group.Torsor
IsTopologicalTorsor.toContinuousSMul : ∀ {V : Type u_1} {inst : Group V} {inst_1 : TopologicalSpace V} {P : Type u_2} {inst_2 : Torsor V P}
  {inst_3 : TopologicalSpace P} [self : IsTopologicalTorsor P], ContinuousSMul V P
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_shrinkYoneda_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {S : C} {ι : Type u_2} [Small.{w, u_2} ι] {X : ι → C}
  (f : (i : ι) → X i ⟶ S) {c : CategoryTheory.Limits.Cofan fun i => CategoryTheory.shrinkYoneda.{w, v, u}.obj (X i)}
  (hc : CategoryTheory.Limits.IsColimit c),
  CategoryTheory.Sieve.ofArrows X f ∈ J S ↔
    CategoryTheory.Presheaf.IsLocallySurjective J
      (CategoryTheory.Limits.Cofan.IsColimit.desc hc fun i => CategoryTheory.shrinkYoneda.{w, v, u}.map (f i))
-- Mathlib.Analysis.SpecialFunctions.Bernstein
bernstein.z_last : ∀ {n : ℕ}, n ≠ 0 → bernstein.z (Fin.last n) = 1
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.atBot_neBot_iff : ∀ {α : Type u_6} [inst : Preorder α], Filter.atBot.NeBot ↔ Nonempty α ∧ IsCodirectedOrder α
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.congr_const : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c₁ c₂ : ℝ} {f : α → E} {g : α → F}
  {l : Filter α}, Asymptotics.IsBigOWith c₁ l f g → c₁ = c₂ → Asymptotics.IsBigOWith c₂ l f g
-- Lean.Meta.Basic
Lean.Meta.instBEqSynthInstanceCacheKey.beq : Lean.Meta.SynthInstanceCacheKey → Lean.Meta.SynthInstanceCacheKey → Bool
-- Mathlib.Order.Comparable
CompRel.of_rel : ∀ {α : Type u_1} {a b : α} {r : α → α → Prop}, r a b → CompRel r a b
-- Init.Data.UInt.Basic
instMaxUInt64 : Max UInt64
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.Functor.map_effectiveEpiFamily : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) [F.PreservesEffectiveEpiFamilies]
  {α : Type u} {B : C} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π],
  CategoryTheory.EffectiveEpiFamily (fun a => F.obj (X a)) fun a => F.map (π a)
-- Mathlib.Data.Finset.NAry
/-- Symmetric statement to `Finset.image_image₂_antidistrib_left`.  -/
Finset.image₂_image_left_anticomm : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq α']
  [inst_1 : DecidableEq γ] {s : Finset α} {t : Finset β} [inst_2 : DecidableEq δ] {f : α' → β → γ} {g : α → α'}
  {f' : β → α → δ} {g' : δ → γ},
  (∀ (a : α) (b : β), f (g a) b = g' (f' b a)) →
    Finset.image₂ f (Finset.image g s) t = Finset.image g' (Finset.image₂ f' t s)
-- Lean.Meta.Tactic.Grind.AC.Types
/-- Structures/operators detected.
We expect to find a small number of associative operators in a given goal. Thus, using `Array` is fine here.
 -/
Lean.Meta.Grind.AC.State.structs : Lean.Meta.Grind.AC.State → Array Lean.Meta.Grind.AC.Struct
-- Init.Data.Option.Lemmas
Option.map_eq_bind : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → α_1} {x : Option α}, Option.map f x = x.bind (some ∘ f)
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron'.comm₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : Z₁₂ ⟶ X₁}
  {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (self : CategoryTheory.Triangulated.Octahedron' comm h₁₂ h₂₃ h₁₃),
  CategoryTheory.CategoryStruct.comp w₁₂ ((CategoryTheory.shiftFunctor C 1).map self.m₁) =
    CategoryTheory.CategoryStruct.comp u₂₃ w₁₃
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
/-- The map `Cocycle K L n → Cocycle K (L⟦a⟧) n'` when `n' + a = n`.  -/
CochainComplex.HomComplex.Cocycle.rightShift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        {n : ℤ} →
          CochainComplex.HomComplex.Cocycle K L n →
            (a n' : ℤ) →
              n' + a = n →
                CochainComplex.HomComplex.Cocycle K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- A point in `K` with the orthogonality property (here characterized in terms of `Kᗮ`) must be the
orthogonal projection.  -/
Submodule.eq_starProjection_of_mem_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] {u v : E}, v ∈ K → u - v ∈ Kᗮ → K.starProjection u = v
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbolAux.mk.sizeOf_spec : ∀ {Self : Type} [inst : SizeOf Self] (name : String) (detail? : Option String) (kind : Lean.Lsp.SymbolKind)
  (range selectionRange : Lean.Lsp.Range) (children? : Option (Array Self)),
  sizeOf
      { name := name, detail? := detail?, kind := kind, range := range, selectionRange := selectionRange,
        children? := children? } =
    1 + sizeOf name + sizeOf detail? + sizeOf kind + sizeOf range + sizeOf selectionRange + sizeOf children?
-- Mathlib.GroupTheory.Divisible
Pi.divisibleBy : {ι : Type u_3} →
  {β : Type u_4} →
    (B : ι → Type u_5) →
      [inst : (i : ι) → SMul β (B i)] →
        [inst_1 : Zero β] →
          [inst_2 : (i : ι) → AddMonoid (B i)] → [(i : ι) → DivisibleBy (B i) β] → DivisibleBy ((i : ι) → B i) β
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.braiding_neg_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.SymmetricCategory C] (M N : CategoryTheory.AddMon C), (β_ M N).inv.hom = (β_ M.X N.X).inv
-- Mathlib.Order.Filter.AtTopBot.Basic
/-- The image of the filter `atBot` on `Iic a` under the coercion equals `atBot`.  -/
Filter.map_val_Iic_atBot : ∀ {α : Type u_3} [inst : Preorder α] [IsCodirectedOrder α] (a : α), Filter.map Subtype.val Filter.atBot = Filter.atBot
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go.match_1.splitter : (motive : ℕ → Sort u_1) → (curr : ℕ) → (Unit → motive 0) → ((curr : ℕ) → motive curr.succ) → motive curr
-- Mathlib.CategoryTheory.ComposableArrows.Four
/-- Variant of `fourδ₁Toδ₀` for preorders.  -/
CategoryTheory.ComposableArrows.fourδ₁Toδ₀' : {ι : Type u_1} →
  [inst : Preorder ι] →
    (i₀ i₁ i₂ i₃ i₄ : ι) →
      (hi₀₁ : i₀ ≤ i₁) →
        (hi₁₂ : i₁ ≤ i₂) →
          (hi₂₃ : i₂ ≤ i₃) →
            (hi₃₄ : i₃ ≤ i₄) →
              CategoryTheory.ComposableArrows.mk₃ (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE hi₂₃)
                  (CategoryTheory.homOfLE hi₃₄) ⟶
                CategoryTheory.ComposableArrows.mk₃ (CategoryTheory.homOfLE hi₁₂) (CategoryTheory.homOfLE hi₂₃)
                  (CategoryTheory.homOfLE hi₃₄)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- The explicit limit cone in `ProfiniteGrp`.  -/
ProfiniteGrp.limitCone : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J ProfiniteGrp.{max v u}) → CategoryTheory.Limits.Cone F
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cochain.toSingleMk_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f g : K.X p ⟶ X) {n : ℤ}
  (h : p + n = q),
  CochainComplex.HomComplex.Cochain.toSingleMk (f + g) h =
    CochainComplex.HomComplex.Cochain.toSingleMk f h + CochainComplex.HomComplex.Cochain.toSingleMk g h
-- Init.Data.BitVec.Bitblast
/-- This is used when proving the correctness of the division algorithm,
where we know that `r < d`.
We then want to show that `((r.shiftConcat b) - d) < d` as the loop invariant.
In arithmetic, this is the same as showing that
`r * 2 + 1 - d < d`, which this theorem establishes.
 -/
_private.Init.Data.BitVec.Bitblast.0.BitVec.two_mul_add_sub_lt_of_lt_of_lt_two : ∀ {a x y : ℕ}, a < x → y < 2 → 2 * a + y - x < x
-- Lean.Parser.Command
/-- `set_option opt val in tacs` (the tactic) acts like `set_option opt val` at the command level,
but it sets the option only within the tactics `tacs`.  -/
Lean.Parser.Tactic.set_option : Lean.Parser.Parser
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
Ideal.toTwoSided.eq_1 : ∀ {R : Type u_1} [inst : Ring R] (I : Ideal R) [inst_1 : I.IsTwoSided], I.toTwoSided = TwoSidedIdeal.mk' ↑I ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.ofNat_kronecker : ∀ {α : Type u_3} {l : Type u_9} {m : Type u_10} {n : Type u_11} [inst : NonAssocSemiring α] [inst_1 : DecidableEq l]
  (a : ℕ) [inst_2 : a.AtLeastTwo] (B : Matrix m n α),
  Matrix.kroneckerMap (fun x1 x2 => x1 * x2) (OfNat.ofNat a) B =
    (Matrix.reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (Matrix.blockDiagonal fun x => OfNat.ofNat a • B)
-- Mathlib.Analysis.SpecificLimits.Normed
/-- If `‖r‖ < 1`, then `∑' n : ℕ, n * r ^ n = r / (1 - r) ^ 2`.  -/
tsum_coe_mul_geometric_of_norm_lt_one : ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] {r : 𝕜}, ‖r‖ < 1 → ∑' (n : ℕ), ↑n * r ^ n = r / (1 - r) ^ 2
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.ae_ae_eq_of_ae_eq_uncurry : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {γ : Type u_4} {f g : α → β → γ},
  Function.uncurry f =ᵐ[μ.prod ν] Function.uncurry g → ∀ᵐ (x : α) ∂μ, f x =ᵐ[ν] g x
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- Coface maps for a cosimplicial object.  -/
CategoryTheory.CosimplicialObject.δ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : CategoryTheory.CosimplicialObject C) → {n : ℕ} → Fin (n + 2) → (X.obj { len := n } ⟶ X.obj { len := n + 1 })
-- Mathlib.Tactic.Linter.OverlappingInstances
_private.Mathlib.Tactic.Linter.OverlappingInstances.0.Mathlib.Linter.OverlappingInstances.getAbstractProjections.go : Lean.Name →
  Lean.Expr →
    Array Lean.Expr → Array Lean.Expr → Bool → StateRefT' IO.RealWorld Lean.NameSet Lean.MetaM (Array Lean.Expr)
-- Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
Mathlib.Tactic.BicategoryLike.Normalize.Result.mk.sizeOf_spec : ∀ (normalizedHom : Mathlib.Tactic.BicategoryLike.NormalizedHom) (toNormalize : Mathlib.Tactic.BicategoryLike.Mor₂Iso),
  sizeOf { normalizedHom := normalizedHom, toNormalize := toNormalize } = 1 + sizeOf normalizedHom + sizeOf toNormalize
-- Mathlib.Algebra.Category.MonCat.Limits
AddCommMonCat.forget₂Mon_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ AddCommMonCat AddMonCat)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Cont'.fix.injEq : ∀ (a : Turing.ToPartrec.Code) (a_1 : Turing.PartrecToTM2.Cont') (a_2 : Turing.ToPartrec.Code)
  (a_3 : Turing.PartrecToTM2.Cont'),
  (Turing.PartrecToTM2.Cont'.fix a a_1 = Turing.PartrecToTM2.Cont'.fix a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Analysis.Convex.Strong
uniformConvexOn_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E} {f : E → ℝ},
  UniformConvexOn s 0 f ↔ ConvexOn ℝ s f
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.dblXYZ_of_Z_eq_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P : Fin 3 → R},
  W'.Equation P → P 2 = 0 → W'.dblXYZ P = P 0 ^ 2 • ![1, 1, 0]
-- Init.Data.ByteArray.Lemmas
ByteArray.extract_append_size_add : ∀ {a b : ByteArray} {i j : ℕ}, (a ++ b).extract (a.size + i) (a.size + j) = b.extract i j
-- Lean.Elab.InfoTree.Types
Lean.Elab.DocElabKind.noConfusionType : Sort v✝ → Lean.Elab.DocElabKind → Lean.Elab.DocElabKind → Sort v✝
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.max?_erase_eq_iff_not_compare_eq_max? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.erase k).max? = t.max? ↔ ∀ {km : α}, t.max? = some km → ¬cmp k km = Ordering.eq
-- Lean.Util.Trace
Lean.TraceState.mk.inj : ∀ {tid : UInt64} {traces : Lean.PersistentArray Lean.TraceElem} {tid_1 : UInt64}
  {traces_1 : Lean.PersistentArray Lean.TraceElem},
  { tid := tid, traces := traces } = { tid := tid_1, traces := traces_1 } → tid = tid_1 ∧ traces = traces_1
-- Mathlib.RingTheory.PicardGroup
ClassGroup.equivPic_apply : ∀ (R : Type u_5) [inst : CommRing R] [inst_1 : IsDomain R] (a : ClassGroup R),
  (ClassGroup.equivPic R) a =
    ↑((QuotientGroup.quotientKerEquivRange (Submodule.unitsToPic R (FractionRing R)))
        ((QuotientGroup.congr (Units.map ↑(Submodule.spanSingleton R)).range
            (Submodule.unitsToPic R (FractionRing R)).ker (MulEquiv.refl (Submodule R (FractionRing R))ˣ) ⋯)
          ((ClassGroup.mulEquivUnitsSubmoduleQuotRange R) a)))
-- Mathlib.RingTheory.AdicCompletion.Completeness
/-- `AdicCompletion I M` is adic complete when `I` is finitely generated.  -/
AdicCompletion.isAdicComplete : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  I.FG → IsAdicComplete I (AdicCompletion I M)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.fst_add : ∀ {R : Type u} {M : Type v} [inst : Add R] [inst_1 : Add M] (x₁ x₂ : TrivSqZeroExt R M), (x₁ + x₂).fst = x₁.fst + x₂.fst
-- Mathlib.Data.Sym.Sym2
/-- Note: `Sym2.map_id` will not simplify `Sym2.map id z` due to `Sym2.map_congr`.  -/
Sym2.map_id' : ∀ {α : Type u_1}, (Sym2.map fun x => x) = id
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- Convergence along filters for `WithSeminorms`.  -/
WithSeminorms.tendsto_nhds : ∀ {𝕜 : Type u_2} {E : Type u_6} {F : Type u_7} {ι : Type u_9} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] {p : SeminormFamily 𝕜 E ι},
  WithSeminorms p →
    ∀ (u : F → E) {f : Filter F} (y₀ : E),
      Filter.Tendsto u f (nhds y₀) ↔ ∀ (i : ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, (p i) (u x - y₀) < ε
-- Mathlib.Topology.UniformSpace.ProdApproximation
ContinuousMap.prodMul_apply : ∀ {X : Type u_5} {Y : Type u_6} {R : Type u_7} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : CommRing R] [inst_3 : TopologicalSpace R] [inst_4 : IsTopologicalRing R] (f : C(X, R)) (g : C(Y, R))
  (p : X × Y), ((ContinuousMap.prodMul f) g) p = f p.1 * g p.2
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toList_roo_eq_none : ∀ {m n i : ℕ}, n ≤ i + (m + 1) → (m<...n).toList[i]? = none
-- Mathlib.FieldTheory.Minpoly.Field
/-- The minimal polynomial of `1` is `X - 1`.  -/
minpoly.one : ∀ (A : Type u_1) (B : Type u_2) [inst : Field A] [inst_1 : Ring B] [inst_2 : Algebra A B] [Nontrivial B],
  minpoly A 1 = Polynomial.X - 1
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
/-- The limit of `x * log (1 + g x)` as `(x : ℝ) → ∞` is `t`,
where `t : ℂ` is the limit of `x * g x`.  -/
Complex.tendsto_mul_log_one_add_of_tendsto : ∀ {g : ℝ → ℂ} {t : ℂ},
  Filter.Tendsto (fun x => ↑x * g x) Filter.atTop (nhds t) →
    Filter.Tendsto (fun x => ↑x * Complex.log (1 + g x)) Filter.atTop (nhds t)
-- Mathlib.Data.Int.Bitwise
Nat.ldiff.eq_1 : Nat.ldiff = Nat.bitwise fun a b => a && !b
-- Mathlib.Topology.Separation.DisjointCover
/-- If `S` is any neighbourhood of the diagonal in a compact topological space `X`, then there
exists a finite cover of `X` by opens `U i` such that `U i ×ˢ U i ⊆ S` for all `i`.

That the indexing set is a finset of `X` is an artifact of the proof; it could be any finite type.
 -/
TopologicalSpace.exists_finite_open_cover_prod_subset_of_mem_nhds_diagonal_of_compact : ∀ {X : Type u_1} [inst : TopologicalSpace X] {S : Set (X × X)} [CompactSpace X],
  S ∈ nhdsSet (Set.diagonal X) → ∃ t U, TopologicalSpace.IsOpenCover U ∧ ∀ (i : ↥t), ↑(U i) ×ˢ ↑(U i) ⊆ S
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the forward direction of `lowerSemicontinuousOn_iff_frequently`. -/
LowerSemicontinuousOn.frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f : α → β} {s : Set α},
  LowerSemicontinuousOn f s → ∀ x ∈ s, ∀ (y : β), (∃ᶠ (x' : α) in nhdsWithin x s, f x' ≤ y) → f x ≤ y
-- Mathlib.GroupTheory.HNNExtension
/-- Given a `TransversalPair`, we can make a normal form for words in the `HNNExtension G A B φ`.
The normal form is a `head`, which is an element of `G`, followed by the product list of pairs,
`t ^ u * g`, where `u` is `1` or `-1` and `g` is the chosen element of its right coset of
`toSubgroup A B u`. There should also be no sequences of the form `t^u * g * t^-u`
where `g ∈ toSubgroup A B u`  -/
HNNExtension.NormalWord : {G : Type u_1} → [inst : Group G] → {A B : Subgroup G} → HNNExtension.NormalWord.TransversalPair G A B → Type u_1
-- Lean.MetavarContext
Lean.instantiateLocalDeclMVars : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → Lean.LocalDecl → m Lean.LocalDecl
-- Lean.ResolveName
/-- Given a name `n`, return a list of possible interpretations.
Each interpretation is a pair `(declName, fieldList)`, where `declName`
is the name of a declaration in the current environment, and `fieldList` are
(potential) field names.
The pair is needed because in Lean `.` may be part of a qualified name or
a field (aka dot-notation).
As an example, consider the following definitions
```
def Boo.x   := 1
def Foo.x   := 2
def Foo.x.y := 3
```
After `open Foo`, we have
- `resolveGlobalName x`     => `[(Foo.x, [])]`
- `resolveGlobalName x.y`   => `[(Foo.x.y, [])]`
- `resolveGlobalName x.z.w` => `[(Foo.x, [z, w])]`

After `open Foo open Boo`, we have
- `resolveGlobalName x`     => `[(Foo.x, []), (Boo.x, [])]`
- `resolveGlobalName x.y`   => `[(Foo.x.y, [])]`
- `resolveGlobalName x.z.w` => `[(Foo.x, [z, w]), (Boo.x, [z, w])]`

If `enableLog` is false, this function does not ever log warnings etc, which is useful if it may be
called incidentally or multiple times.
 -/
Lean.resolveGlobalName : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadResolveName m] →
      [Lean.MonadEnv m] →
        [Lean.MonadOptions m] →
          [Lean.MonadLog m] →
            [Lean.AddMessageContext m] → Lean.Name → optParam Bool true → m (List (Lean.Name × List String))
-- Mathlib.AlgebraicTopology.SimplicialSet.Op
SSet.opEquivalence_counitIso : SSet.opEquivalence.counitIso = SSet.opFunctorCompOpFunctorIso
-- Lean.Server.Rpc.Basic
_private.Lean.Server.Rpc.Basic.0.Lean.Server.WithRpcRef.id : {α : Type u} → Lean.Server.WithRpcRef α → USize
-- Mathlib.GroupTheory.Nilpotent
Subgroup.lowerCentralSeries_map_subtype_le : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) (n : ℕ),
  Subgroup.map H.subtype (⊤.lowerCentralSeries n) ≤ ⊤.lowerCentralSeries n
-- Mathlib.Algebra.Order.CompleteField
ConditionallyCompleteLinearOrderedField.inducedOrderRingIso_symm : ∀ (β : Type u_3) (γ : Type u_4) [inst : Field β] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : IsStrictOrderedRing β] [inst_3 : Field γ] [inst_4 : ConditionallyCompleteLinearOrder γ]
  [inst_5 : IsStrictOrderedRing γ],
  (ConditionallyCompleteLinearOrderedField.inducedOrderRingIso β γ).symm =
    ConditionallyCompleteLinearOrderedField.inducedOrderRingIso γ β
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- The left adjoint of a lax monoidal functor is oplax monoidal.  -/
CategoryTheory.Adjunction.leftAdjointOplaxMonoidal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              {G : CategoryTheory.Functor D C} → (F ⊣ G) → [G.LaxMonoidal] → F.OplaxMonoidal
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- Simple graphs contain a copy of a `completeBipartiteGraph α β` iff there exists a "left"
subset of `card α` vertices and a "right" subset of `card β` vertices such that every vertex
in the "left" subset is adjacent to every vertex in the "right" subset.  -/
SimpleGraph.completeBipartiteGraph_isContained_iff : ∀ {V : Type u_1} {G : SimpleGraph V} {α : Type u_2} {β : Type u_3} [inst : Fintype α] [inst_1 : Fintype β],
  (completeBipartiteGraph α β).IsContained G ↔
    ∃ left right, left.card = Fintype.card α ∧ right.card = Fintype.card β ∧ G.IsCompleteBetween ↑left ↑right
-- Mathlib.Topology.PartialHomeomorph.Basic
Topology.IsEmbedding.toPartialHomeomorph_target : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y)
  (h : Topology.IsEmbedding f) [inst_2 : Nonempty X],
  (Topology.IsEmbedding.toPartialHomeomorph f h).target = Set.range f
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
SSet.stdSimplex.σ_objMk₁_of_le : ∀ {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)),
  i ≤ j.castSucc →
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ (SSet.stdSimplex.obj { len := 1 }) j))
        (SSet.stdSimplex.objMk₁ i) =
      SSet.stdSimplex.objMk₁ i.castSucc
-- Lean.Util.FoldConsts
Lean.Expr.FoldConstsImpl.FoldM : Type → Type
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
ContinuousFunctionalCalculus.exists_cfc_of_predicate : ∀ {R : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} {inst : CommSemiring R} {inst_1 : StarRing R}
  {inst_2 : MetricSpace R} {inst_3 : IsTopologicalSemiring R} {inst_4 : ContinuousStar R} {inst_5 : Ring A}
  {inst_6 : StarRing A} {inst_7 : TopologicalSpace A} {inst_8 : Algebra R A} [self : ContinuousFunctionalCalculus R A p]
  (a : A),
  p a →
    ∃ φ,
      Continuous ⇑φ ∧
        Function.Injective ⇑φ ∧
          φ (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = a ∧
            (∀ (f : C(↑(spectrum R a), R)), spectrum R (φ f) = Set.range ⇑f) ∧ ∀ (f : C(↑(spectrum R a), R)), p (φ f)
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.generateFrom_iInter_of_generateFrom_eq_self : ∀ {X : Type u_1} {ι : Type u_2} (G : ι → Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X))),
  (∀ (i : ι), (DiffeologicalSpace.generateFrom (G i)).toPlots = G i) →
    DiffeologicalSpace.generateFrom (⋂ i, G i) = ⨅ i, DiffeologicalSpace.generateFrom (G i)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.commute_nat_add : ∀ (f : CircleDeg1Lift) (n : ℕ), Function.Commute ⇑f fun x => ↑n + x