mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyWith.mk.inj : ∀ {X : Type u} {Y : Type v} {inst : TopologicalSpace X} {inst_1 : TopologicalSpace Y} {f₀ f₁ : C(X, Y)}
  {P : C(X, Y) → Prop} {toHomotopy : f₀.Homotopy f₁}
  {prop' : ∀ (t : ↑unitInterval), P { toFun := fun x => toHomotopy.toFun (t, x), continuous_toFun := ⋯ }}
  {toHomotopy_1 : f₀.Homotopy f₁}
  {prop'_1 : ∀ (t : ↑unitInterval), P { toFun := fun x => toHomotopy_1.toFun (t, x), continuous_toFun := ⋯ }},
  { toHomotopy := toHomotopy, prop' := prop' } = { toHomotopy := toHomotopy_1, prop' := prop'_1 } →
    toHomotopy = toHomotopy_1
-- Mathlib.Data.Matrix.Composition
Matrix.compAlgEquiv_apply : ∀ (I : Type u_1) (J : Type u_2) (R : Type u_5) (K : Type u_7) [inst : CommSemiring K] [inst_1 : Semiring R]
  [inst_2 : Fintype I] [inst_3 : Fintype J] [inst_4 : Algebra K R] [inst_5 : DecidableEq I] [inst_6 : DecidableEq J]
  (M : Matrix I I (Matrix J J R)), (Matrix.compAlgEquiv I J R K) M = (Matrix.comp I I J J R) M
-- Mathlib.Analysis.Convex.Strict
StrictConvex.inter : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace E]
  [inst_3 : AddCommMonoid E] [inst_4 : SMul 𝕜 E] {s t : Set E},
  StrictConvex 𝕜 s → StrictConvex 𝕜 t → StrictConvex 𝕜 (s ∩ t)
-- Lean.Environment
Lean.Kernel.Exception.invalidProj.sizeOf_spec : ∀ (env : Lean.Kernel.Environment) (lctx : Lean.LocalContext) (proj : Lean.Expr),
  sizeOf (Lean.Kernel.Exception.invalidProj env lctx proj) = 1 + sizeOf env + sizeOf lctx + sizeOf proj
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.LeftHomologyData.op_H : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData), h.op.H = Opposite.op h.H
-- Mathlib.Algebra.GroupWithZero.ProdHom
MonoidWithZeroHom.snd_surjective : ∀ {G₀ : Type u_1} {H₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : GroupWithZero H₀],
  Function.Surjective ⇑(MonoidWithZeroHom.snd G₀ H₀)
-- Std.Http.Data.Body.Empty
Std.Http.Body.instCoeResponseEmptyAny : Coe (Std.Http.Response Std.Http.Body.Empty) (Std.Http.Response Std.Http.Body.Any)
-- Aesop.Rule.Name
Aesop.instToJsonBuilderName.toJson : Aesop.BuilderName → Lean.Json
-- Mathlib.AlgebraicGeometry.Sites.Pretopology
AlgebraicGeometry.Scheme.mem_grothendieckTopology_iff : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative]
  {X : AlgebraicGeometry.Scheme} {S : CategoryTheory.Sieve X},
  S ∈ (AlgebraicGeometry.Scheme.grothendieckTopology P) X ↔ ∃ 𝒰, CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows
-- Mathlib.Data.Nat.Bits
Nat.bodd_add_div2 : ∀ (n : ℕ), n.bodd.toNat + 2 * n.div2 = n
-- Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
HasStrictFDerivAt.implicitFunctionOfProdDomain_def : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁]
  [inst_2 : NormedSpace 𝕜 E₁] [inst_3 : CompleteSpace E₁] {E₂ : Type u_3} [inst_4 : NormedAddCommGroup E₂]
  [inst_5 : NormedSpace 𝕜 E₂] [inst_6 : CompleteSpace E₂] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
  [inst_8 : NormedSpace 𝕜 F] [inst_9 : CompleteSpace F] {u : E₁ × E₂} {f : E₁ × E₂ → F} {f'u : E₁ × E₂ →L[𝕜] F}
  {dfu : HasStrictFDerivAt f f'u u} {if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible},
  dfu.implicitFunctionOfProdDomain if₂u = fun x =>
    ((dfu.implicitFunctionDataOfProdDomain if₂u).implicitFunction (f u) x).2
-- Mathlib.Logic.Equiv.Finset
Denumerable.isChain_raise' : ∀ (l : List ℕ) (n : ℕ), List.IsChain (fun x1 x2 => x1 < x2) (Denumerable.raise' l n)
-- Mathlib.Algebra.Group.Indicator
Set.indicator_sdiff' : ∀ {α : Type u_1} {G : Type u_6} [inst : AddGroup G] {s t : Set α},
  s ⊆ t → ∀ (f : α → G), (t \ s).indicator f = t.indicator f + -s.indicator f
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
/-- **Alias** of the reverse direction of `NumberField.InfinitePlace.isUnramified_mk_iff_isUnmixed`. -/
NumberField.ComplexEmbedding.IsUnmixed.mk_isUnramified : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K] {φ : K →+* ℂ},
  NumberField.ComplexEmbedding.IsUnmixed k φ → NumberField.InfinitePlace.IsUnramified k (NumberField.InfinitePlace.mk φ)
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Group.isNilpotent_of_product_of_sylow_group`.

---

If a finite group is the direct product of its Sylow groups, it is nilpotent  -/
isNilpotent_of_product_of_sylow_group : ∀ {G : Type u_1} [hG : Group G] [Finite G] (e : ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p) G) → ↥↑P) ≃* G),
  Group.IsNilpotent G
-- Mathlib.Algebra.Group.Subsemigroup.Basic
AddSubsemigroup.instCompleteLattice.eq_1 : ∀ {M : Type u_1} [inst : Add M],
  AddSubsemigroup.instCompleteLattice =
    { le := fun x1 x2 => x1 ≤ x2, lt := fun x1 x2 => x1 < x2, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
      le_antisymm := ⋯, sup := SemilatticeSup.sup, le_sup_left := ⋯, le_sup_right := ⋯, sup_le := ⋯,
      inf := fun x1 x2 => x1 ⊓ x2, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯,
      toSupSet := (completeLatticeOfInf (AddSubsemigroup M) ⋯).toSupSet, isLUB_sSup := ⋯,
      toInfSet := AddSubsemigroup.instInfSet, isGLB_sInf := ⋯, toTop := AddSubsemigroup.instTop, le_top := ⋯,
      toBot := AddSubsemigroup.instBot, bot_le := ⋯ }
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.monoidalCategoryStruct_whiskerRight : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {X₁ X₂ : (i : I) → C i} (f : X₁ ⟶ X₂) (Y : (i : I) → C i)
  (i : I),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y i =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight (f i) (Y i)
-- Init.Data.AC
Lean.Data.AC.Context.mk.injEq : ∀ {α : Sort u} (op : α → α → α) (assoc : Std.Associative op) (comm : Option (PLift (Std.Commutative op)))
  (idem : Option (PLift (Std.IdempotentOp op))) (vars : List (Lean.Data.AC.Variable op)) (arbitrary : α)
  (op_1 : α → α → α) (assoc_1 : Std.Associative op_1) (comm_1 : Option (PLift (Std.Commutative op_1)))
  (idem_1 : Option (PLift (Std.IdempotentOp op_1))) (vars_1 : List (Lean.Data.AC.Variable op_1)) (arbitrary_1 : α),
  ({ op := op, assoc := assoc, comm := comm, idem := idem, vars := vars, arbitrary := arbitrary } =
      { op := op_1, assoc := assoc_1, comm := comm_1, idem := idem_1, vars := vars_1, arbitrary := arbitrary_1 }) =
    (op = op_1 ∧ comm ≍ comm_1 ∧ idem ≍ idem_1 ∧ vars ≍ vars_1 ∧ arbitrary = arbitrary_1)
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.rTensor_id : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W},
  Representation.IntertwiningMap.rTensor ρ (Representation.IntertwiningMap.id σ) =
    Representation.IntertwiningMap.id (σ.tprod ρ)
-- Mathlib.Algebra.Group.Shrink
Shrink.instAddCommGroup : {α : Type u_2} → [inst : Small.{v, u_2} α] → [AddCommGroup α] → AddCommGroup (Shrink.{v, u_2} α)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_right_left_as : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D T) (Y : T) (X : D)
  (Y_1 : CategoryTheory.StructuredArrow Y ((CategoryTheory.Under.forget X).comp F)),
  ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse F Y X).obj Y_1).right.left.as = PUnit.unit
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isClique_map_finset_iff_of_nontrivial : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {f : α ↪ β} {t : Finset β},
  t.Nontrivial → ((SimpleGraph.map (⇑f) G).IsClique ↑t ↔ ∃ s, G.IsClique ↑s ∧ Finset.map f s = t)
-- Mathlib.RingTheory.NonUnitalSubring.Defs
/-- `NonUnitalSubring R` is the type of non-unital subrings of `R`. A non-unital subring of `R`
is a subset `s` that is a multiplicative subsemigroup and an additive subgroup. Note in particular
that it shares the same 0 as R.  -/
NonUnitalSubring : (R : Type u) → [NonUnitalNonAssocRing R] → Type u
-- Mathlib.RingTheory.Valuation.LocalSubring
/-- [Stacks Tag 090P](https://stacks.math.columbia.edu/tag/090P) (part (2)) -/
LocalSubring.exists_le_valuationSubring_of_isIntegrallyClosedIn : ∀ {K : Type u_3} [inst : Field K] {x : K} {R : LocalSubring K},
  x ∉ R.toSubring → ∀ [IsIntegrallyClosedIn (↥R.toSubring) K], ∃ V, R ≤ V.toLocalSubring ∧ x ∉ V
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.instHasColimits : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C],
  CategoryTheory.Limits.HasColimits (CategoryTheory.SimplicialObject C)
-- Mathlib.RingTheory.Nilpotent.Basic
Commute.add_pow_add_eq_zero_of_pow_eq_zero : ∀ {R : Type u_1} {x y : R} [inst : Semiring R],
  Commute x y → ∀ {m n : ℕ}, x ^ m = 0 → y ^ n = 0 → (x + y) ^ (m + n - 1) = 0
-- Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
SSet.π₀.lift.congr_simp : ∀ {X : SSet} {T : Type u_1} (f f_1 : X.obj (Opposite.op { len := 0 }) → T) (e_f : f = f_1)
  (hf : ∀ ⦃x₀ x₁ : X.obj (Opposite.op { len := 0 })⦄ (x : SSet.Edge x₀ x₁), f x₀ = f x₁) (a a_1 : X.π₀),
  a = a_1 → SSet.π₀.lift f hf a = SSet.π₀.lift f_1 ⋯ a_1
-- Mathlib.Analysis.Convex.Jensen
ConvexOn.le_sup_of_mem_convexHull : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : LinearOrder β] [IsOrderedAddMonoid β]
  [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β} {x : E}
  {t : Finset E}, ConvexOn 𝕜 s f → ↑t ⊆ s → ∀ (hx : x ∈ (convexHull 𝕜) ↑t), f x ≤ t.sup' ⋯ f
-- Lean.LibrarySuggestions.Basic
/-- Construct a `Selector` (which acts on an `MVarId`)
from a function which takes the pretty printed goal.
 -/
Lean.LibrarySuggestions.ppSelector : (String → Lean.LibrarySuggestions.Config → Lean.MetaM (Array Lean.LibrarySuggestions.Suggestion)) →
  Lean.MVarId → Lean.LibrarySuggestions.Config → Lean.MetaM (Array Lean.LibrarySuggestions.Suggestion)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.alter_eq_empty_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)},
  t.alter k f = ∅ ↔ (t = ∅ ∨ t.size = 1 ∧ k ∈ t) ∧ f (t.get? k) = none
-- Mathlib.Algebra.Group.End
AddAut.addConj.eq_1 : ∀ {G : Type u_3} [inst : AddGroup G],
  AddAut.addConj =
    {
      toFun := fun g =>
        { toFun := fun h => g + h + -g, invFun := fun h => -g + h + g, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ },
      map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.isGroupoid : ∀ {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] (L : CategoryTheory.Functor C D) [L.IsLocalization ⊤],
  CategoryTheory.IsGroupoid D
-- Mathlib.Data.Rat.Defs
Rat.natCast_eq_one_iff : ∀ {n : ℕ}, ↑n = 1 ↔ n = 1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.equation_add : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ x₂ y₁ y₂ : F},
  W.Equation x₁ y₁ →
    W.Equation x₂ y₂ →
      ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂) →
        W.Equation (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_cons : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
  {h : Std.Internal.List.containsKey a (⟨k, v⟩ :: l) = true},
  Std.Internal.List.getKey a (⟨k, v⟩ :: l) h = if h' : (k == a) = true then k else Std.Internal.List.getKey a l ⋯
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- The image of a bicone under a functor.  -/
CategoryTheory.Functor.mapBicone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (F : CategoryTheory.Functor C D) →
              [F.PreservesZeroMorphisms] →
                {J : Type w₁} → {f : J → C} → CategoryTheory.Limits.Bicone f → CategoryTheory.Limits.Bicone (F.obj ∘ f)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.mop_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z},
  (CategoryTheory.CategoryStruct.comp f g).mop = CategoryTheory.CategoryStruct.comp f.mop g.mop
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
/-- A closed subset of a completely metrizable space is also completely metrizable.  -/
IsClosed.isCompletelyMetrizableSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [TopologicalSpace.IsCompletelyMetrizableSpace X] {s : Set X},
  IsClosed s → TopologicalSpace.IsCompletelyMetrizableSpace ↑s
-- Mathlib.MeasureTheory.Function.LpSpace.Complete
MeasureTheory.Lp.eLpNorm'_lim_le_liminf_eLpNorm' : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : SeminormedAddGroup E]
  {f : ℕ → α → E} {p : ℝ},
  0 < p →
    (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) →
      ∀ {f_lim : α → E},
        (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (f_lim x))) →
          MeasureTheory.eLpNorm' f_lim p μ ≤ Filter.liminf (fun n => MeasureTheory.eLpNorm' (f n) p μ) Filter.atTop
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- This is basically just `yoneda : Over A ⥤ (Over A)ᵒᵖ ⥤ Type (max u v)` restricted in the second
argument along the forgetful functor `CostructuredArrow yoneda A ⥤ Over A`, but done in a way
that we land in a smaller universe.

This is one direction of the equivalence we're constructing.  -/
CategoryTheory.OverPresheafAux.restrictedYoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (A : CategoryTheory.Functor Cᵒᵖ (Type v)) →
      CategoryTheory.Functor (CategoryTheory.Over A)
        (CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v))
-- Mathlib.Topology.UniformSpace.UniformApproximation
/-- A uniform limit of uniformly continuous functions is uniformly continuous.  -/
TendstoUniformly.uniformContinuous : ∀ {α : Type u_4} {β : Type u_5} {ι : Type u_6} [inst : UniformSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {p : Filter ι}, TendstoUniformly F f p → (∃ᶠ (n : ι) in p, UniformContinuous (F n)) → UniformContinuous f
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LetRecToLift.lctx : Lean.Elab.Term.LetRecToLift → Lean.LocalContext
-- Mathlib.Analysis.Analytic.IteratedFDeriv
/-- If a function has a power series in a ball, then its `n`-th iterated derivative is given by
`(v₁, ..., vₙ) ↦ ∑ pₙ (v_{σ (1)}, ..., v_{σ (n)})` where the sum is over all
permutations of `{1, ..., n}`.  -/
HasFPowerSeriesOnBall.iteratedFDeriv_eq_sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal},
  HasFPowerSeriesOnBall f p x r →
    AnalyticOn 𝕜 f Set.univ → ∀ {n : ℕ} (v : Fin n → E), (iteratedFDeriv 𝕜 n f x) v = ∑ σ, (p n) fun i => v (σ i)
-- Mathlib.Tactic.ComputeDegree
/-- `twoHeadsArgs e` takes an `Expr`ession `e` as input and recurses into `e` to make sure
that `e` looks like `lhs ≤ rhs`, `lhs < rhs` or `lhs = rhs` and that `lhs` is one of
`natDegree f, degree f, coeff f d`.
It returns
* the function being applied on the LHS (`natDegree`, `degree`, or `coeff`),
  or else `.anonymous` if it's none of these;
* the name of the relation (`Eq`, `LE.le` or `LT.lt`), or else `.anonymous` if it's none of these;
* either
  * `.inl zero`, `.inl one`, or `.inl many` if the polynomial in a numeral;
  * or `.inr` of the head symbol of `f`;
  * or `.inl .anonymous` if inapplicable;
* if it exists, whether the `rhs` is a metavariable;
* if the LHS is `coeff f d`, whether `d` is a metavariable.

This is all the data needed to figure out whether `compute_degree` can make progress on `e`
and, if so, which lemma it should apply.

Sample outputs:
* `natDegree (f + g) ≤ d => (natDegree, LE.le, HAdd.hAdd, d.isMVar, none)` (similarly for `=`);
* `degree (f * g) = d => (degree, Eq, HMul.hMul, d.isMVar, none)` (similarly for `≤`);
* `coeff (1 : ℕ[X]) c = x => (coeff, Eq, one, x.isMVar, c.isMVar)` (no `≤` option!).
 -/
Mathlib.Tactic.ComputeDegree.twoHeadsArgs : Lean.Expr → Lean.Name × Lean.Name × (Lean.Name ⊕ Lean.Name) × List Bool
-- Init.Core
lt_of_lt_of_eq : ∀ {α : Type u_1} {a b c : α} [inst : LT α], a < b → b = c → a < c
-- Mathlib.Tactic.Linter.Header
/-- Extracts the module name and modifiers from an import syntax node.
Returns `(module_id, isPublic, isMeta, isAll)`.  -/
_private.Mathlib.Tactic.Linter.Header.0.Mathlib.Linter.Style.header.importInfo : Lean.Syntax → Option (Lean.Syntax × Bool × Bool × Bool)
-- Mathlib.Data.PNat.Factors
/-- The type of multisets of prime numbers.  Unique factorization
gives an equivalence between this set and ℕ+, as we will formalize
below.  -/
PrimeMultiset : Type
-- Mathlib.Algebra.Category.MonCat.Limits
AddCommMonCat.limitCone.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommMonCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommMonCat)).sections],
  AddCommMonCat.limitCone F =
    CategoryTheory.liftLimit
      (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ AddCommMonCat AddMonCat)))
-- Init.Data.SInt.Lemmas
Int32.div_one : ∀ {a : Int32}, a / 1 = a
-- Init.Data.SInt.Bitwise
Int8.not_and_self : ∀ {a : Int8}, ~~~a &&& a = 0
-- Mathlib.Algebra.Group.Defs
IsCyclic.exists_zpow_surjective : ∀ {G : Type u} {inst : Pow G ℤ} [self : IsCyclic G], ∃ g, Function.Surjective fun x => g ^ x
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
IsSimpleAddGroup.isAddCyclic : ∀ {α : Type u_1} [inst : AddCommGroup α] [IsSimpleAddGroup α], IsAddCyclic α
-- Lean.Environment
Lean.AsyncConstantInfo.toConstantVal : Lean.AsyncConstantInfo → Lean.ConstantVal
-- Mathlib.Algebra.Group.Basic
div_div_cancel_left : ∀ {G : Type u_3} [inst : CommGroup G] (a b : G), a / b / a = b⁻¹
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.cos_ne_zero_iff : ∀ {θ : ℂ}, Complex.cos θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ (2 * ↑k + 1) * ↑Real.pi / 2
-- Mathlib.Combinatorics.Matroid.IndepAxioms
/-- The independence predicate  -/
IndepMatroid.Indep : {α : Type u_2} → IndepMatroid α → Set α → Prop
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
/-- A type of additive group homomorphisms that map nonnegative elements to nonnegative elements
is also a type of order homomorphisms.  -/
OrderHomClass.of_addMonoidHom : ∀ {F' : Type u_5} {E₁' : Type u_6} {E₂' : Type u_7} [inst : FunLike F' E₁' E₂'] [inst_1 : AddGroup E₁']
  [inst_2 : LE E₁'] [AddRightMono E₁'] [inst_4 : AddGroup E₂'] [inst_5 : LE E₂'] [AddRightMono E₂']
  [AddMonoidHomClass F' E₁' E₂'], (∀ (f : F') (x : E₁'), 0 ≤ x → 0 ≤ f x) → OrderHomClass F' E₁' E₂'
-- Mathlib.Data.Finsupp.Defs
Finsupp.hasFiniteSupport : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] (f : α →₀ M), Function.HasFiniteSupport ⇑f
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.orderTop_ne_of_coeff_eq_zero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {x : HahnSeries Γ R} {i : Γ},
  x.coeff i = 0 → x.orderTop ≠ ↑i
-- Init.Data.BitVec.Lemmas
BitVec.flattenList.toNatAux.induct : ∀ {n : ℕ} (motive : List (BitVec n) → Prop),
  motive [] →
    (∀ (x : BitVec n), motive [x]) →
      (∀ (x y : BitVec n) (rest : List (BitVec n)),
          have xs := x :: y :: rest;
          have mid := xs.length / 2;
          motive (List.take mid xs) → motive (List.drop mid xs) → motive (x :: y :: rest)) →
        ∀ (a : List (BitVec n)), motive a
-- Mathlib.Data.Sign.Defs
SignType.trichotomy : ∀ (a : SignType), a = -1 ∨ a = 0 ∨ a = 1
-- Init.Data.BitVec.Lemmas
BitVec.getElem_reverse : ∀ {w i : ℕ} (x : BitVec w) (h : i < w), x.reverse[i] = x.getMsbD i
-- Mathlib.Topology.Sequences
SequentialSpace.sup : ∀ {X : Type u_3} {t₁ t₂ : TopologicalSpace X}, SequentialSpace X → SequentialSpace X → SequentialSpace X
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.tendsto_cobounded : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β},
  AntilipschitzWith K f → Filter.Tendsto f (Bornology.cobounded α) (Bornology.cobounded β)
-- Init.Data.Float.Float32
/-- Computes the base-2 exponential `2^x` of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`exp2f`.
 -/
Float32.exp2 : Float32 → Float32
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.mem_ordConnectedComponent_trans : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} {x y z : α},
  y ∈ s.ordConnectedComponent x → z ∈ s.ordConnectedComponent y → z ∈ s.ordConnectedComponent x
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- If `v` belongs to the interior of the interval `integrableExpSet X μ`,
then `X ^ p * exp (v * X)` is integrable for all nonnegative `p : ℝ`.  -/
ProbabilityTheory.integrable_rpow_mul_exp_of_mem_interior_integrableExpSet : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {v : ℝ},
  v ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    ∀ {p : ℝ}, 0 ≤ p → MeasureTheory.Integrable (fun ω => X ω ^ p * Real.exp (v * X ω)) μ
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.Internal.List.getValueCastD.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) (l : List ((a : α) × β a))
  (fallback : β a), Std.Internal.List.getValueCastD a l fallback = (Std.Internal.List.getValueCast? a l).getD fallback
-- Mathlib.RingTheory.Extension.Presentation.Submersive
/-- If `P` is a submersive presentation, the partial derivatives of `P.relation i` by
`P.map j` form a basis of `σ → S`.  -/
Algebra.SubmersivePresentation.basisDeriv : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              [inst_3 : Finite σ] → Algebra.SubmersivePresentation R S ι σ → Module.Basis σ S (σ → S)
-- Mathlib.Order.IsNormal
/-- This condition is the RHS of the `IsLUB (f '' Iio a) (f a)` predicate, which is sufficient
since the LHS is implied by monotonicity.  -/
Order.IsNormal.mem_lowerBounds_upperBounds_of_isSuccLimit : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β},
  Order.IsNormal f → ∀ {a : α}, Order.IsSuccLimit a → f a ∈ lowerBounds (upperBounds (f '' Set.Iio a))
-- Mathlib.Data.List.Perm.Lattice
List.Perm.drop_inter : ∀ {α : Type u_1} [inst : DecidableEq α] {xs ys : List α} (n : ℕ),
  xs.Perm ys → ys.Nodup → (List.drop n xs).Perm (ys ∩ List.drop n xs)
-- Lean.Meta.Sym.Arith.Poly
Lean.Grind.CommRing.SPolResult.mk.inj : ∀ {spol : Lean.Grind.CommRing.Poly} {k₁ : ℤ} {m₁ : Lean.Grind.CommRing.Mon} {k₂ : ℤ} {m₂ : Lean.Grind.CommRing.Mon}
  {spol_1 : Lean.Grind.CommRing.Poly} {k₁_1 : ℤ} {m₁_1 : Lean.Grind.CommRing.Mon} {k₂_1 : ℤ}
  {m₂_1 : Lean.Grind.CommRing.Mon},
  { spol := spol, k₁ := k₁, m₁ := m₁, k₂ := k₂, m₂ := m₂ } =
      { spol := spol_1, k₁ := k₁_1, m₁ := m₁_1, k₂ := k₂_1, m₂ := m₂_1 } →
    spol = spol_1 ∧ k₁ = k₁_1 ∧ m₁ = m₁_1 ∧ k₂ = k₂_1 ∧ m₂ = m₂_1