mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.findImportMatches : {α : Type} →
  IO.Ref (Option (Lean.Meta.LazyDiscrTree α)) →
    (Lean.Name → Lean.AsyncConstantInfo → Lean.MetaM (Array (Lean.Meta.LazyDiscrTree.InitEntry α))) →
      optParam (List (List Lean.Meta.LazyDiscrTree.Key)) [] →
        optParam ℕ 1000 →
          optParam (Option (IO.Ref (Option (Array α)))) none →
            Lean.Expr → Lean.MetaM (Lean.Meta.LazyDiscrTree.MatchResult α)
-- Std.Time.Date.Unit.Day
Std.Time.Day.instInhabitedOffset : Inhabited Std.Time.Day.Offset
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rxc.Iterator.pairwise_toList_upwardEnumerableLt : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.Rxc.IsAlwaysFinite α]
  (it : Std.Iter α), List.Pairwise (fun a b => Std.PRange.UpwardEnumerable.LT a b) it.toList
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
ULift.instMeasurableSpace : {α : Type u_1} → [MeasurableSpace α] → MeasurableSpace (ULift.{u_6, u_1} α)
-- Mathlib.Algebra.GradedMonoid
/-- `(•) : A 0 → A i → A i` is the value provided in `GradedMonoid.GMul.mul`, composed with
an `Eq.rec` to turn `A (0 + i)` into `A i`.
 -/
GradedMonoid.GradeZero.smul : {ι : Type u_1} → (A : ι → Type u_2) → [inst : AddZeroClass ι] → [GradedMonoid.GMul A] → (i : ι) → SMul (A 0) (A i)
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.generates_reverse : ∀ {T : Type u_1} {g : ContextFreeGrammar T} {u : List (Symbol T g.NT)}, g.reverse.Generates u.reverse ↔ g.Generates u
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
/-- The zero function is majorized with any exponent.  -/
Tactic.ComputeAsymptotics.Majorized.zero : ∀ {b : ℝ → ℝ} {exp : ℝ}, Tactic.ComputeAsymptotics.Majorized 0 b exp
-- Init.Data.String.Iterate
String.Slice.RevPosIterator.mk : {s : String.Slice} → s.Pos → s.RevPosIterator
-- Mathlib.Algebra.Order.Ring.Basic
not_isSquare_of_neg : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : LinearOrder R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftMono R] {x : R},
  x < 0 → ¬IsSquare x
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- The set of pair-self-adjoint endomorphisms are a submodule of the type of all endomorphisms.  -/
LinearMap.isPairSelfAdjointSubmodule : {R : Type u_1} →
  {M : Type u_5} →
    {M₂ : Type u_7} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommGroup M₂] →
              [inst_4 : Module R M₂] → (M →ₗ[R] M →ₗ[R] M₂) → (M →ₗ[R] M →ₗ[R] M₂) → Submodule R (Module.End R M)
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackRestrictIsoRestrict f U).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f U.ι) h) =
    CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj U).ι h
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.isCardinalFiltered : ∀ (J : Type w) [inst : CategoryTheory.SmallCategory J] (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalFiltered J κ],
  (∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)) →
    CategoryTheory.IsCardinalFiltered
      (CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ) κ
-- Mathlib.CategoryTheory.MorphismProperty.Descent
CategoryTheory.MorphismProperty.pushout_inr_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.MorphismProperty C} {Z X Y : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} [P.IsStableUnderCobaseChange] [P.CodescendsAlong Q]
  [inst_3 : CategoryTheory.Limits.HasPushout f g], Q g → (P (CategoryTheory.Limits.pushout.inr f g) ↔ P f)
-- Mathlib.RingTheory.Bialgebra.Basic
/-- Every commutative (semi)ring is a bialgebra over itself  -/
CommSemiring.toBialgebra : (R : Type u) → [inst : CommSemiring R] → Bialgebra R R
-- Mathlib.Topology.Order.IntermediateValue
isConnected_Icc : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {a b : α}, a ≤ b → IsConnected (Set.Icc a b)
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- The inner product of a linear combination of a set of orthonormal vectors with one of those
vectors picks out the coefficient of that vector.  -/
Orthonormal.inner_left_finsupp : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {v : ι → E},
  Orthonormal 𝕜 v → ∀ (l : ι →₀ 𝕜) (i : ι), inner 𝕜 ((Finsupp.linearCombination 𝕜 v) l) (v i) = (starRingEnd 𝕜) (l i)
-- Aesop.RuleSet
Aesop.GlobalRuleSet.modifyBaseM : {m : Type → Type u_1} →
  [Monad m] → (Aesop.BaseRuleSet → m Aesop.BaseRuleSet) → Aesop.GlobalRuleSet → m Aesop.GlobalRuleSet
-- Mathlib.Analysis.InnerProductSpace.Projection.Submodule
/-- **Alias** of `Submodule.orthogonalProjectionOnto_apply_eq_projectionOnto`. -/
Submodule.orthogonalProjection_apply_eq_linearProjOfIsCompl : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] (x : E),
  K.orthogonalProjectionOnto x = (K.projectionOnto Kᗮ ⋯) x
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
/-- `log` is operator monotone.  -/
CFC.log_monotoneOn : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A],
  MonotoneOn CFC.log {a | IsStrictlyPositive a}
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.aeval_S : ∀ {R : Type u_1} {R' : Type u_2} [inst : CommRing R] [inst_1 : CommRing R'] [inst_2 : Algebra R R'] (x : R') (n : ℤ),
  (Polynomial.aeval x) (Polynomial.Chebyshev.S R n) = Polynomial.eval x (Polynomial.Chebyshev.S R' n)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
/-- A `PresheafedSpace C` is a topological space equipped with a presheaf of `C`s.  -/
AlgebraicGeometry.PresheafedSpace : (C : Type u_1) → [CategoryTheory.Category.{v_1, u_1} C] → Type (max (max (u + 1) u_1) v_1)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.getD_inter_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k fallback : α}, k ∉ m₂ → (m₁ ∩ m₂).getD k fallback = fallback
-- Mathlib.CategoryTheory.Simple
CategoryTheory.instNontrivialEndOfSimple : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C)
  [CategoryTheory.Simple X], Nontrivial (CategoryTheory.End X)
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
toWeakSpaceCLM_bijective : ∀ {𝕜 : Type u_2} {E : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : Module 𝕜 E] [inst_6 : TopologicalSpace E],
  Function.Bijective ⇑(toWeakSpaceCLM 𝕜 E)
-- Mathlib.Data.Int.Cast.Pi
Sum.elim_intCast_intCast : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : IntCast γ] (n : ℤ), Sum.elim ↑n ↑n = ↑n
-- Mathlib.Logic.UnivLE
/-- This is redundant as an instance given the below.  -/
UnivLE.succ : ∀ [UnivLE.{u, v}], UnivLE.{u, v + 1}
-- Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
CategoryTheory.Triangulated.TStructure.triangleω₁δ_map_hom₃ : ∀ {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]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b c : EInt) (hab : a ≤ b)
  (hbc : b ≤ c) {X Y : C} (φ : X ⟶ Y),
  ((t.triangleω₁δ a b c hab hbc).map φ).hom₃ = (t.eTruncGE.obj b).map ((t.eTruncLT.obj c).map φ)
-- Mathlib.ModelTheory.Basic
/-- Interpretation of the function symbols  -/
FirstOrder.Language.Structure.funMap : {L : FirstOrder.Language} → {M : Type w} → [self : L.Structure M] → {n : ℕ} → L.Functions n → (Fin n → M) → M
-- Init.Data.String.Lemmas.Intercalate
String.intercalate_singleton : ∀ {s t : String}, s.intercalate [t] = t
-- Mathlib.Algebra.HierarchyDesign
/-- Some definitions that define objects of a class cannot be instances, because they have an
explicit argument that does not occur in the conclusion. An example is `Preorder.lift` that has a
function `f : α → β` as an explicit argument to lift a preorder on `β` to a preorder on `α`.

If these definitions are used to define instances of this class *and* this class is an argument to
some other type-class so that type-class inference will have to unfold these instances to check
for definitional equality, then these definitions should be marked `@[reducible]`.

For example, `Preorder.lift` is used to define `Units.Preorder` and `PartialOrder.lift` is used
to define `Units.PartialOrder`. In some cases it is important that type-class inference can
recognize that `Units.Preorder` and `Units.PartialOrder` give rise to the same `LE` instance.
For example, you might have another class that takes `[LE α]` as an argument, and this argument
sometimes comes from `Units.Preorder` and sometimes from `Units.PartialOrder`.
Therefore, `Preorder.lift` and `PartialOrder.lift` are marked `@[reducible]`.
 -/
LibraryNote.«reducible_non-instances» : Batteries.Util.LibraryNote
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] [inst : Inhabited α]
  {l : List (α × β)} {k : α}, (List.map Prod.fst l).contains k = false → (Std.HashMap.ofList l).getKey! k = default
-- Mathlib.CategoryTheory.IsomorphismClasses
CategoryTheory.Groupoid.isIsomorphic_iff_nonempty_hom : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {X Y : C}, CategoryTheory.IsIsomorphic X Y ↔ Nonempty (X ⟶ Y)
-- Mathlib.Data.Multiset.AddSub
Multiset.rel_add_left : ∀ {α : Type u_1} {β : Type v} {r : α → β → Prop} {as₀ as₁ : Multiset α} {bs : Multiset β},
  Multiset.Rel r (as₀ + as₁) bs ↔ ∃ bs₀ bs₁, Multiset.Rel r as₀ bs₀ ∧ Multiset.Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
-- Mathlib.Control.ULiftable
instULiftableId : ULiftable Id Id
-- Init.Data.BitVec.Lemmas
BitVec.toNat_cpop_append : ∀ {w u : ℕ} {x : BitVec w} {y : BitVec u}, (x ++ y).cpop.toNat = x.cpop.toNat + y.cpop.toNat
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.norm_measure_zero : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} [inst : NormedAddCommGroup E]
  (f : ↥(MeasureTheory.Lp E p 0)), ‖f‖ = 0
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
/-- The integral representation of the function `x ↦ x^p` (where `p ∈ (1, 2)`) .  -/
Real.rpow_eq_const_mul_integral_rpowIntegrand₁₂ : ∀ {p x : ℝ},
  p ∈ Set.Ioo 1 2 →
    0 ≤ x →
      x ^ p = (∫ (t : ℝ) in Set.Ioi 0, (p - 1).rpowIntegrand₀₁ t 1)⁻¹ * ∫ (t : ℝ) in Set.Ioi 0, p.rpowIntegrand₁₂ t x
-- Init.Data.String.Decode
String.utf8EncodeChar_eq_utf8EncodeCharFast : String.utf8EncodeChar = String.utf8EncodeCharFast
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.ordered_insert : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {k : α} {v : β k} {l : Std.DTreeMap.Internal.Impl α β}
  (hlb : l.Balanced), l.Ordered → (Std.DTreeMap.Internal.Impl.insert k v l hlb).impl.Ordered
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.size_eq_match_roc : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxc.HasSize α] [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [Std.Rxc.IsAlwaysFinite α] [Std.Rxc.LawfulHasSize α],
  r.size =
    match Std.PRange.succ? r.lower with
    | none => 0
    | some next => if next ≤ r.upper then (next<...=r.upper).size + 1 else 0
-- Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.RingNF.nat_rawCast_0 : ∀ {R : Type u_1} [inst : CommSemiring R], Nat.rawCast 0 = 0
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.skipPrefix?_slice_eq_some_iff : ∀ {pat : String.Slice} {s : String} {pos : s.Pos}, s.skipPrefix? pat = some pos ↔ ∃ t, pos.Splits pat.copy t
-- Mathlib.Tactic.Ring.Common
/-- A precomputed `Cache` for `ℕ`.  -/
Mathlib.Tactic.Ring.Common.Cache.nat : Mathlib.Tactic.Ring.Common.Cache Mathlib.Tactic.Ring.Common.sℕ
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- **Alias** of `fderiv_finsetProd`. -/
fderiv_finset_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_5} {𝔸' : Type u_7} [inst_3 : NormedCommRing 𝔸'] [inst_4 : NormedAlgebra 𝕜 𝔸']
  {u : Finset ι} {g : ι → E → 𝔸'} [inst_5 : DecidableEq ι] {x : E},
  (∀ i ∈ u, DifferentiableAt 𝕜 (g i) x) →
    fderiv 𝕜 (fun x => ∏ i ∈ u, g i x) x = ∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • fderiv 𝕜 (g i) x
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.addVal.eq_1 : ∀ (R : Type u) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R],
  IsDiscreteValuationRing.addVal R = multiplicity_addValuation ⋯
-- Std.Data.DTreeMap.Basic
/-- Returns the key-value pair with the `n`-th smallest key.  -/
Std.DTreeMap.Const.entryAtIdx : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → (t : Std.DTreeMap α (fun x => β) cmp) → (n : ℕ) → n < t.size → α × β
-- Mathlib.LinearAlgebra.Finsupp.LSum
Finsupp.sum_smul_index_semilinearMap' : ∀ {α : Type u_1} {R : Type u_3} {R₂ : Type u_4} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid M₂]
  [inst_5 : Module R₂ M₂] {σ : R →+* R₂} {v : α →₀ M} {c : R} {h : α → M →ₛₗ[σ] M₂},
  ((c • v).sum fun a => ⇑(h a)) = σ c • v.sum fun a => ⇑(h a)
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.comp_preservesColimitsOfShape : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesColimitsOfShape J F]
  [CategoryTheory.Limits.PreservesColimitsOfShape J G], CategoryTheory.Limits.PreservesColimitsOfShape J (F.comp G)
-- Lean.DocString.Add
Lean.VersoDocResult.toVersoDocString : Lean.VersoDocResult → Lean.VersoDocString
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_add_of_distinct_val : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  {x y : R}, v x ≠ v y → v (x + y) = max (v x) (v y)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.toAddMon_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : CategoryTheory.AddGrp C), A.toAddMon.X = A.X
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Equivalence.rightOp_unitIso_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : Cᵒᵖ ≌ D) (X : C), e.rightOp.unitIso.inv.app X = (e.unitIso.hom.app (Opposite.op X)).unop
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.rTensor_add : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f g : N →ₗ[R] P), LinearMap.rTensor M (f + g) = LinearMap.rTensor M f + LinearMap.rTensor M g
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.Decl.isCasesOnParam?.go : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Decl pu → {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Code pu → Option ℕ
-- Mathlib.Analysis.InnerProductSpace.MulOpposite
/-- The multiplicative opposite of an orthonormal basis `b`, i.e., `b i ↦ op (b i)`.  -/
OrthonormalBasis.mulOpposite : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {ι : Type u_3} →
      {H : Type u_4} →
        [inst_1 : NormedAddCommGroup H] →
          [inst_2 : InnerProductSpace 𝕜 H] → [inst_3 : Fintype ι] → OrthonormalBasis ι 𝕜 H → OrthonormalBasis ι 𝕜 Hᵐᵒᵖ
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If the second of three points is strictly between the other two, the angle at the third point
is zero.  -/
Sbtw.angle₂₃₁_eq_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P}, Sbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.angle p₂ p₃ p₁ = 0
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.degree_gcd_le_right : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] (p : Polynomial R) {q : Polynomial R},
  q ≠ 0 → (gcd p q).degree ≤ q.degree
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_closure_union_closure_eq_closure_union : ∀ {α : Type u_2} (M : Matroid α) (X Y : Set α), M.closure (M.closure X ∪ M.closure Y) = M.closure (X ∪ Y)
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.instBialgebra : (R : Type u_1) →
  (A : Type u_3) →
    (M : Type u_8) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] → [Bialgebra R A] → [inst_3 : AddMonoid M] → Bialgebra R (AddMonoidAlgebra A M)
-- Mathlib.Data.List.Infix
List.length_inits : ∀ {α : Type u_1} (l : List α), l.inits.length = l.length + 1
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.range_snd : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S],
  NonUnitalRingHom.srange (NonUnitalRingHom.snd R S) = ⊤
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE_X₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE._auto_3),
  (X.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₃ = (X.H n₂).obj (CategoryTheory.ComposableArrows.mk₁ f₁)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
/-- **Alias** of the reverse direction of `measurableSet_setOfPred`. -/
Measurable.setOf : ∀ {α : Type u_1} [inst : MeasurableSpace α] {p : α → Prop}, Measurable p → MeasurableSet {a | p a}
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonTextDocumentPositionParams.fromJson : Lean.Json → Except String Lean.Lsp.TextDocumentPositionParams
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.Odd.not_even : ∀ {S : Type u_2} [inst : CommRing S] {m : ℕ} (ψ : DirichletCharacter S m) [NeZero 2], ψ.Odd → ¬ψ.Even
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k k' : α}, (k == k') = true → ∀ {v : β k}, ⟨k, v⟩ ∈ l → Std.Internal.List.getEntry? k' l = some ⟨k, v⟩
-- Mathlib.NumberTheory.JacobiSum.Basic
/-- The *Jacobi sum* of two multiplicative characters on a finite commutative ring.  -/
jacobiSum : {R : Type u_1} →
  {R' : Type u_2} → [inst : CommRing R] → [Fintype R] → [inst_2 : CommRing R'] → MulChar R R' → MulChar R R' → R'
-- Mathlib.GroupTheory.Perm.Sign
/-- `signBijAux f ⟨a, b⟩` returns the pair consisting of `f a` and `f b` in decreasing order.  -/
Equiv.Perm.signBijAux : {n : ℕ} → Equiv.Perm (Fin n) → (_ : Fin n) × Fin n → (_ : Fin n) × Fin n
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- This definition provides a convenient way to show that a multifork is a limit.  -/
CategoryTheory.Limits.Multifork.IsLimit.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MulticospanShape} →
      {I : CategoryTheory.Limits.MulticospanIndex J C} →
        (K : CategoryTheory.Limits.Multifork I) →
          (lift : (E : CategoryTheory.Limits.Multifork I) → E.pt ⟶ K.pt) →
            (∀ (E : CategoryTheory.Limits.Multifork I) (i : J.L),
                CategoryTheory.CategoryStruct.comp (lift E) (K.ι i) = E.ι i) →
              (∀ (E : CategoryTheory.Limits.Multifork I) (m : E.pt ⟶ K.pt),
                  (∀ (i : J.L), CategoryTheory.CategoryStruct.comp m (K.ι i) = E.ι i) → m = lift E) →
                CategoryTheory.Limits.IsLimit K
-- Mathlib.CategoryTheory.Subobject.Comma
/-- A quotient of the underlying object of a costructured arrow can be lifted to a quotient of
the costructured arrow, provided that there is a morphism making the quotient into a
costructured arrow.  -/
CategoryTheory.CostructuredArrow.liftQuotient : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : CategoryTheory.Functor C D} →
          {T : D} →
            {A : CategoryTheory.CostructuredArrow S T} →
              (P : CategoryTheory.Subobject (Opposite.op A.left)) →
                {q : S.obj (Opposite.unop (CategoryTheory.Subobject.underlying.obj P)) ⟶ T} →
                  CategoryTheory.CategoryStruct.comp (S.map P.arrow.unop) q = A.hom →
                    CategoryTheory.Subobject (Opposite.op A)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
instFiniteAlgHomOfFinite : ∀ (R : Type u_1) [inst : CommSemiring R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K] (S : Type u_3)
  [inst_3 : Semiring S] [inst_4 : Algebra R S] [Module.Finite R S], Finite (S →ₐ[R] K)
-- Lean.Elab.Match
/-- Pattern variables that were explicitly provided by the user.
Recall that implicit parameters and `_` are elaborated as metavariables, and then converted into pattern variables
by the `normalize` procedure.
 -/
Lean.Elab.Term.ToDepElimPattern.Context.explicitPatternVars : Lean.Elab.Term.ToDepElimPattern.Context → Array Lean.FVarId
-- Mathlib.Order.Filter.AtTopBot.Defs
/-- `atTop` is the filter representing the limit `→ ∞` on an ordered set.
It is generated by the collection of up-sets `{b | a ≤ b}`.
(The preorder need not have a top element for this to be well defined,
and indeed is trivial when a top element `x` exists, i.e., it coincides with `pure x`.)  -/
Filter.atTop : {α : Type u_3} → [Preorder α] → Filter α
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.lift_map_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  [inst_3 : CategoryTheory.Limits.HasBiproduct g] {P : C} (k : (j : J) → P ⟶ f j) (p : (j : J) → f j ⟶ g j) {Z : C}
  (h : ⨁ g ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift k)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.map p) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.biproduct.lift fun j => CategoryTheory.CategoryStruct.comp (k j) (p j)) h
-- Mathlib.Topology.Algebra.GroupWithZero
ContinuousInv₀.mk : ∀ {G₀ : Type u_4} [inst : Zero G₀] [inst_1 : Inv G₀] [inst_2 : TopologicalSpace G₀],
  (∀ ⦃x : G₀⦄, x ≠ 0 → ContinuousAt Inv.inv x) → ContinuousInv₀ G₀
-- Mathlib.Analysis.SpecialFunctions.Exponential
/-- The exponential map in a complete normed field `𝕂` of characteristic zero has derivative
`NormedSpace.exp x` at any point `x` in the disk of convergence.  -/
hasDerivAt_exp_of_mem_ball : ∀ {𝕂 : Type u_1} [inst : NontriviallyNormedField 𝕂] [CompleteSpace 𝕂] [CharZero 𝕂] {x : 𝕂},
  x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝕂).radius → HasDerivAt NormedSpace.exp (NormedSpace.exp x) x