mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.Rayleigh
/-- For a self-adjoint operator `T`, a maximum of the Rayleigh quotient of `T` on a sphere centred
at the origin is an eigenvector of `T`, with eigenvalue the global supremum of the Rayleigh
quotient.  -/
IsSelfAdjoint.hasEigenvector_of_isMaxOn : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {T : E →L[𝕜] E},
  IsSelfAdjoint T →
    ∀ {x₀ : E},
      x₀ ≠ 0 →
        IsMaxOn T.reApplyInnerSelf (Metric.sphere 0 ‖x₀‖) x₀ →
          Module.End.HasEigenvector (↑T) (↑(⨆ x, T.rayleighQuotient ↑x)) x₀
-- Init.Data.Nat.Basic
Nat.sub_le_sub_left : ∀ {n m : ℕ}, n ≤ m → ∀ (k : ℕ), k - m ≤ k - n
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Module.mem_freeLocus_of_isLocalization : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : PrimeSpectrum R)
  (Rₚ : Type u_1) (Mₚ : Type u_2) [inst_3 : CommRing Rₚ] [inst_4 : Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p.asIdeal]
  [inst_6 : AddCommGroup Mₚ] [inst_7 : Module R Mₚ] (f : M →ₗ[R] Mₚ) [IsLocalizedModule p.asIdeal.primeCompl f]
  [inst_9 : Module Rₚ Mₚ] [IsScalarTower R Rₚ Mₚ], p ∈ Module.freeLocus R M ↔ Module.Free Rₚ Mₚ
-- Mathlib.Algebra.Group.TypeTags.Basic
isAddLeftRegular_toAdd : ∀ {α : Type u} [inst : AddMonoid α] {a : Multiplicative α}, IsAddLeftRegular (Multiplicative.toAdd a) ↔ IsLeftRegular a
-- Init.PropLemmas
ite_else_not_self : ∀ {p : Prop} [inst : Decidable p] {q : Prop}, (if p then q else ¬p) ↔ p → q
-- Mathlib.Algebra.Group.Action.Defs
IsScalarTower.of_commMonoid : ∀ (R₁ : Type u_9) (R : Type u_10) [inst : Monoid R₁] [inst_1 : CommMonoid R] [inst_2 : MulAction R₁ R]
  [SMulCommClass R₁ R R], IsScalarTower R₁ R R
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.«builder_option(Transparency!:=_)» : Lean.ParserDescr
-- Lean.Elab.PreDefinition.FixedParams
_private.Lean.Elab.PreDefinition.FixedParams.0.Lean.Elab.FixedParamPerm.instantiateForall.go : Array Lean.Expr → List (Option ℕ) → Lean.Expr → Lean.MetaM Lean.Expr
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.isUnit.match_1.congr_eq_1 : ∀ {n : ℕ} (motive : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Sort u_1)
  (x : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
  (h_1 : (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) → motive [l])
  (h_2 : (x : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) → motive x)
  (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  x = [l] →
    (match x with
      | [l] => h_1 l
      | x => h_2 x) ≍
      h_1 l
-- Mathlib.Order.Filter.Extr
/-- **Alias** of the reverse direction of `isExtrOn_dual_iff`. -/
IsExtrOn.dual : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsExtrOn f s a → IsExtrOn (⇑OrderDual.toDual ∘ f) s a
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
SimpleGraph.IsEdgeConnected.eq_1 : ∀ {V : Type u_1} (G : SimpleGraph V) (k : ℕ), G.IsEdgeConnected k = ∀ (u v : V), G.IsEdgeReachable k u v
-- Lean.Server.InfoUtils
_private.Lean.Server.InfoUtils.0.Lean.Elab.InfoTree.foldInfoM.go : {m : Type u_1 → Type u_2} →
  {α : Type u_1} →
    [Monad m] →
      (Lean.Elab.ContextInfo → Lean.Elab.Info → α → m α) → Option Lean.Elab.ContextInfo → α → Lean.Elab.InfoTree → m α
-- Mathlib.LinearAlgebra.Determinant
LinearMap.det_comp : ∀ {M : Type u_2} [inst : AddCommGroup M] {A : Type u_5} [inst_1 : CommRing A] [inst_2 : Module A M] (f g : M →ₗ[A] M),
  LinearMap.det (f ∘ₗ g) = LinearMap.det f * LinearMap.det g
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.rightKanExtensionCompIsoOfPreserves_inv_fac_app : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesRightKanExtension F L] [inst_5 : L.HasRightKanExtension F]
  (a : A),
  CategoryTheory.CategoryStruct.comp ((G.rightKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a))
      (G.map ((L.rightKanExtensionCounit F).app a)) =
    (L.rightKanExtensionCounit (F.comp G)).app a
-- Mathlib.GroupTheory.Submonoid.Centralizer
Submonoid.center_le_centralizer : ∀ {M : Type u_1} [inst : Monoid M] (s : Set M), Submonoid.center M ≤ Submonoid.centralizer s
-- Mathlib.Topology.List
List.Vector.continuous_insertIdx : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {n : ℕ} {i : Fin (n + 1)}
  {f : β → α} {g : β → List.Vector α n},
  Continuous f → Continuous g → Continuous fun b => List.Vector.insertIdx (f b) i (g b)
-- Init.Data.Int.DivMod.Lemmas
Int.mul_fdiv_assoc' : ∀ (b : ℤ) {a c : ℤ}, c ∣ a → (a * b).fdiv c = a.fdiv c * b
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max_le : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α} {he : t.isEmpty = false},
  (cmp (t.max he) k).isLE = true ↔ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.NumberTheory.ModularForms.LevelOne.Basic
ModularForm.const.congr_simp : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} (x x_1 : ℂ),
  x = x_1 → ∀ [inst : Γ.HasDetOne], ModularForm.const x = ModularForm.const x_1
-- Mathlib.Computability.Reduce
ComputablePred.computable_of_oneOneReducible : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {p : α → Prop} {q : β → Prop},
  p ≤₁ q → ComputablePred q → ComputablePred p
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
CategoryTheory.Abelian.isIso_of_epi_of_isIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {R₁ R₂ : CategoryTheory.ComposableArrows C 2} (φ : R₁ ⟶ R₂),
  R₁.Exact →
    R₂.Exact →
      CategoryTheory.Epi
          (R₁.map' 1 2 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_6
            CategoryTheory.Abelian.mono_of_epi_of_epi_mono'._proof_1) →
        CategoryTheory.Epi
            (R₂.map' 1 2 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_6
              CategoryTheory.Abelian.mono_of_epi_of_epi_mono'._proof_1) →
          CategoryTheory.Epi
              (CategoryTheory.ComposableArrows.app' φ 0 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_2) →
            CategoryTheory.IsIso
                (CategoryTheory.ComposableArrows.app' φ 1
                  CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_6) →
              CategoryTheory.IsIso
                (CategoryTheory.ComposableArrows.app' φ 2 CategoryTheory.Abelian.mono_of_epi_of_epi_mono'._proof_1)
-- Mathlib.Algebra.Module.Rat
SMulCommClass.nnrat' : ∀ {α : Type u} {M : Type v} [inst : AddCommMonoid M] [inst_1 : DistribSMul α M] [inst_2 : Module ℚ≥0 M],
  SMulCommClass α ℚ≥0 M
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- Reformulation of equicontinuity at `x₀` within a set `S`, comparing two variables near `x₀`
instead of comparing only one with `x₀`.  -/
equicontinuousWithinAt_iff_pair : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α}
  {S : Set X} {x₀ : X},
  x₀ ∈ S →
    (EquicontinuousWithinAt F S x₀ ↔
      ∀ U ∈ uniformity α, ∃ V ∈ nhdsWithin x₀ S, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U)
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.instNNNormHom : {V W : SemiNormedGrp} → NNNorm (V ⟶ W)
-- Mathlib.Data.Finsupp.Notation
Finsupp.fun₀.matchAlts.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Field.Periodic
Function.Antiperiodic.const_inv_mul : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : DivisionSemiring α] [inst_1 : Neg β],
  Function.Antiperiodic f c → ∀ {a : α}, a ≠ 0 → Function.Antiperiodic (fun x => f (a⁻¹ * x)) (a * c)
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.smul_mk : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] (f : Polynomial R) [inst_1 : DistribSMul S R]
  [inst_2 : IsScalarTower S R R] (a : S) (x : Polynomial R), a • (AdjoinRoot.mk f) x = (AdjoinRoot.mk f) (a • x)
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.instSub : {A : Type u_1} →
  {G : Type u_2} →
    [inst : Semiring A] →
      [inst_1 : Monoid G] →
        {V : Type u_6} →
          {W : Type u_7} →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommGroup W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] →
                    (ρ : Representation A G V) → (σ : Representation A G W) → Sub (ρ.IntertwiningMap σ)
-- Mathlib.Data.ZMod.Basic
ZMod.castHom_apply : ∀ {n : ℕ} {R : Type u_1} [inst : Ring R] {m : ℕ} [inst_1 : CharP R m] {h : m ∣ n} (i : ZMod n),
  (ZMod.castHom h R) i = i.cast
-- Mathlib.Topology.Bornology.Constructions
instBoundedSpaceForall : ∀ {ι : Type u_3} {X : ι → Type u_4} [inst : (i : ι) → Bornology (X i)] [∀ (i : ι), BoundedSpace (X i)],
  BoundedSpace ((i : ι) → X i)
-- Mathlib.Data.Seq.Defs
Stream'.Seq.instMembership : {α : Type u} → Membership α (Stream'.Seq α)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.δ_comp_ofHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G K : CochainComplex C ℤ} {n : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n) (f : G ⟶ K) (m : ℤ),
  CochainComplex.HomComplex.δ n m (z₁.comp (CochainComplex.HomComplex.Cochain.ofHom f) ⋯) =
    (CochainComplex.HomComplex.δ n m z₁).comp (CochainComplex.HomComplex.Cochain.ofHom f) ⋯
-- Mathlib.Algebra.Order.Antidiag.Prod
/-- In a canonically ordered additive monoid, the antidiagonal can be construct by filtering.

Note that this is not an instance, as for some times a more efficient algorithm is available.  -/
Finset.HasAntidiagonal.antidiagonalOfLocallyFinite : {A : Type u_2} →
  [inst : AddCommMonoid A] →
    [inst_1 : PartialOrder A] →
      [CanonicallyOrderedAdd A] → [LocallyFiniteOrderBot A] → [DecidableEq A] → Finset.HasAntidiagonal A
-- Std.Http.Protocol.H1.Event
Std.Http.Protocol.H1.Event.next.sizeOf_spec : ∀ {dir : Std.Http.Protocol.H1.Direction}, sizeOf Std.Http.Protocol.H1.Event.next = 1
-- Init.Data.Range.Polymorphic.UInt
UInt16.upwardEnumerableLT_ofBitVec : ∀ {x y : BitVec 16},
  Std.PRange.UpwardEnumerable.LT { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LT x y
-- Mathlib.Analysis.Complex.Norm
Complex.ne_zero_of_one_lt_re : ∀ {s : ℂ}, 1 < s.re → s ≠ 0
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
SheafOfModules.instIsLeftAdjointOverOverRingCatOverMapOfHasPullbacks : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.Limits.HasPullbacks C] {X Y : C} (f : X ⟶ Y),
  (SheafOfModules.overMap R f).IsLeftAdjoint
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- Typeclass for reverse monotonicity of addition on the left,
namely `a + b₁ ≤ a + b₂ → b₁ ≤ b₂`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsOrderedCancelAddMonoid`.  -/
AddLeftReflectLE : (M : Type u_1) → [Add M] → [LE M] → Prop
-- Mathlib.RingTheory.Algebraic.Basic
Algebra.IsAlgebraic.injective_tower_top : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] {A : Type u_3} [inst_1 : CommRing S] [NoZeroDivisors S]
  [inst_3 : Algebra R S] [alg : Algebra.IsAlgebraic R S] [inst_4 : Ring A] [inst_5 : Algebra R A] [inst_6 : Algebra S A]
  [IsScalarTower R S A], Function.Injective ⇑(algebraMap R A) → Function.Injective ⇑(algebraMap S A)
-- Lean.Message
Lean.MessageData.ofWidget.inj : ∀ {a : Lean.Widget.WidgetInstance} {a_1 : Lean.MessageData} {a_2 : Lean.Widget.WidgetInstance} {a_3 : Lean.MessageData},
  Lean.MessageData.ofWidget a a_1 = Lean.MessageData.ofWidget a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Init.Data.List.ToArray
List.isPrefixOf_toArray : ∀ {α : Type u_1} [inst : BEq α] (l₁ l₂ : List α), l₁.toArray.isPrefixOf l₂.toArray = l₁.isPrefixOf l₂
-- Lean.ExtraModUses
/-- Checks whether this module should be preserved as an import by `shake`.  -/
Lean.isExtraRevModUse : Lean.Environment → Lean.ModuleIdx → Bool
-- Mathlib.Topology.Order.OrderClosed
Icc_mem_nhdsGE_of_mem : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {a b c : α},
  b ∈ Set.Ico c a → Set.Icc c a ∈ nhdsWithin b (Set.Ici b)
-- Init.Data.Rat.Basic
/-- Constructs a rational number from components.
We rename the constructor to `mk'` to avoid a clash with the smart constructor.  -/
Rat.mk' : (num : ℤ) →
  (den : ℕ) → autoParam (den ≠ 0) Rat.den_nz._autoParam → autoParam (num.natAbs.Coprime den) Rat.reduced._autoParam → ℚ
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.coeff_one : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f) [Nontrivial S], h.coeff 1 = Pi.single 0 1
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'_mul_mk'_eq_one' : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (x : R) (y : ↥M) (h : x ∈ M),
  IsLocalization.mk' S x y * IsLocalization.mk' S ↑y ⟨x, h⟩ = 1
-- Mathlib.Order.Filter.Pointwise
Filter.principal_one : ∀ {α : Type u_2} [inst : One α], Filter.principal 1 = 1
-- Mathlib.Analysis.Fourier.Notation
/-- The inverse Fourier transform is continuous.  -/
ContinuousFourierInv : (E : Type u_5) →
  (F : outParam (Type u_6)) → [TopologicalSpace E] → [TopologicalSpace F] → [FourierTransformInv E F] → Prop
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf_map' : ∀ (R : Type u) [inst : CommRing R]
  {U V :
    (TopologicalSpace.Opens ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of R)).toPresheafedSpace)ᵒᵖ}
  (i : U ⟶ V),
  (AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of R)).presheaf.map i =
    (AlgebraicGeometry.Spec.structureSheaf R).obj.map i
-- Mathlib.Order.Circular
/-- **Alias** of `sbtw_of_btw_not_btw`. -/
Btw.btw.sbtw_of_not_btw : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, btw a b c → ¬btw c b a → sbtw a b c
-- Lean.Environment
_private.Lean.Environment.0.Lean.finalizeImport.unsafe_impl_12 : Lean.Environment → NonScalar
-- Lean.Parser.Command
Lean.Parser.Command.eraseAttr : Lean.Parser.Parser
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
Ordinal.CNF.coeff_one_left : ∀ (o : Ordinal.{u_1}), Ordinal.CNF.coeff 1 o = fun₀ | 0 => o
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {h_mem : k ∈ m₁ ∩ m₂},
  Std.ExtDHashMap.Const.get (m₁ ∩ m₂) k h_mem = Std.ExtDHashMap.Const.get m₁ k ⋯
-- Mathlib.Data.Stream.Init
Stream'.get_zero_cons : ∀ {α : Type u} (a : α) (s : Stream' α), (Stream'.cons a s).get 0 = a
-- Mathlib.Topology.Algebra.Algebra
/-- If `R` is a discrete topological ring, then any topological ring `S` which is an `R`-algebra
is also a topological `R`-algebra.

NB: This could be an instance but the signature makes it very expensive in search.
See https://github.com/leanprover-community/mathlib4/pull/15339
for the regressions caused by making this an instance.  -/
DiscreteTopology.instContinuousSMul : ∀ (R : Type u_1) (A : Type u) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : TopologicalSpace R] [inst_4 : TopologicalSpace A] [IsTopologicalSemiring A] [DiscreteTopology R],
  ContinuousSMul R A
-- Lean.Parser.Command
Lean.Parser.Command.optionValue.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Http.Protocol.H1.Reader
/-- Transitions to the state for reading headers.
 -/
Std.Http.Protocol.H1.Reader.startHeaders : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Reader dir → Std.Http.Protocol.H1.Reader dir
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The braiding isomorphism which swaps a binary coproduct.  -/
CategoryTheory.Limits.coprod.braiding : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C] → (P Q : C) → P ⨿ Q ≅ Q ⨿ P
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal'_sub : ∀ {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [inst : DecidableEq o] [inst_1 : AddGroup α]
  (M N : (i : o) → Matrix (m' i) (n' i) α),
  Matrix.blockDiagonal' (M - N) = Matrix.blockDiagonal' M - Matrix.blockDiagonal' N
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂Hom_congr : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] {f₁ f₂ : R →+* S₁}
  {g₁ g₂ : σ → S₁} {p₁ p₂ : MvPolynomial σ R},
  f₁ = f₂ → g₁ = g₂ → p₁ = p₂ → (MvPolynomial.eval₂Hom f₁ g₁) p₁ = (MvPolynomial.eval₂Hom f₂ g₂) p₂
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsType₂.φ_succ_snd : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) {d : ℕ}
  (hd : x.dim = d),
  (SSet.prodStdSimplex.pairingCore.IsType₂.φ x hd (SSet.prodStdSimplex.pairingCore.min x hd).succ).2 =
    (SSet.prodStdSimplex.pairingCore.IsType₂.φ x hd (SSet.prodStdSimplex.pairingCore.min x hd).castSucc).2
-- Mathlib.Algebra.Lie.Nilpotent
/-- The max nilpotent submodule is the `sSup` of all nilpotent submodules.  -/
LieModule.maxNilpotentSubmodule : (R : Type u) →
  (L : Type v) →
    (M : Type w) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → [inst_4 : LieRingModule L M] → LieSubmodule R L M
-- Mathlib.Algebra.Field.Subfield.Defs
/-- A subfield is closed under addition.  -/
Subfield.add_mem : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) {x y : K}, x ∈ s → y ∈ s → x + y ∈ s
-- Mathlib.Algebra.Category.Grp.Limits
AddGrpCat.addGroupObj.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrpCat) (j : J),
  AddGrpCat.addGroupObj F j =
    { toAdd := AddGrpCat.addGroupObj._aux_1 F j, add_assoc := ⋯, toZero := AddGrpCat.addGroupObj._aux_4 F j,
      zero_add := ⋯, add_zero := ⋯, toNSMul := AddGrpCat.addGroupObj._aux_8 F j, nsmul_zero := ⋯, nsmul_succ := ⋯,
      toNeg := AddGrpCat.addGroupObj._aux_12 F j, toSub := AddGrpCat.addGroupObj._aux_14 F j,
      toZSMul := AddGrpCat.addGroupObj._aux_16 F j, sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯,
      zsmul_neg' := ⋯, neg_add_cancel := ⋯ }
-- Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
/-- An `𝒮ℒ` modular form with vanishing q-expansion constant term vanishes at every cusp.  -/
ModularForm.isZeroAt_of_coeffZero_eq_zero : ∀ {k : ℤ} (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k),
  (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 ⇑f) = 0 →
    ∀ {c : OnePoint ℝ}, IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range → c.IsZeroAt (⇑f) k
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- Coercion to function as an `AddMonoidHom`.  -/
lp.coeFnAddMonoidHom : {α : Type u_3} →
  (E : α → Type u_4) → (p : ENNReal) → [inst : (i : α) → NormedAddCommGroup (E i)] → ↥(lp E p) →+ (i : α) → E i
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.SearchStep.cast_matched : ∀ {s t : String.Slice} {hst : s.copy = t.copy} {startPos endPos : s.Pos},
  String.Slice.Pattern.SearchStep.cast hst (String.Slice.Pattern.SearchStep.matched startPos endPos) =
    String.Slice.Pattern.SearchStep.matched (startPos.cast hst) (endPos.cast hst)
-- Lean.Meta.Sym.Arith.Types
/-- Run `k` with a temporary exponent threshold.  -/
Lean.Meta.Sym.Arith.withExpThreshold : {α : Type} → ℕ → Lean.Meta.Sym.SymM α → Lean.Meta.Sym.SymM α
-- Init.ShareCommon
ShareCommon.StateFactoryBuilder.setInsert : (self : ShareCommon.StateFactoryBuilder) →
  {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → self.Set α → α → self.Set α
-- Init.Data.AC
Lean.Data.AC.mergeIdem.eq_2 : ∀ (a : ℕ) (as : List ℕ), Lean.Data.AC.mergeIdem (a :: as) = Lean.Data.AC.mergeIdem.loop a as
-- Lean.Declaration
/-- Whether the definition is flagged as unsafe.  -/
Lean.InductiveVal.isUnsafe : Lean.InductiveVal → Bool
-- Mathlib.Order.Hom.CompleteLattice
sInfHomClass.mk : ∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} [inst : InfSet α] [inst_1 : InfSet β] [inst_2 : FunLike F α β],
  (∀ (f : F) (s : Set α), f (sInf s) = sInf (⇑f '' s)) → sInfHomClass F α β
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
Lean.Meta.RefinedDiscrTree.instInhabitedMatchResult : {a : Type} → Inhabited (Lean.Meta.RefinedDiscrTree.MatchResult a)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Iso.connectedComponentEquiv_refl : ∀ {V : Type u} {G : SimpleGraph V}, SimpleGraph.Iso.refl.connectedComponentEquiv = Equiv.refl G.ConnectedComponent
-- Mathlib.Data.Int.Cast.Field
/-- Auxiliary lemma for `norm_cast` to move the cast `-↑n` upwards to `↑-↑n`.

(The restriction to `DivisionRing` is necessary, otherwise this would also apply in the case where
`R = ℤ` and cause nontermination.)
 -/
Int.cast_neg_natCast : ∀ {R : Type u_2} [inst : DivisionRing R] (n : ℕ), ↑(-↑n) = -↑n
-- Mathlib.Data.Nat.Totient
/-- `Nat.totient m` and `Nat.totient n` are coprime iff one of them is 1.  -/
Nat.totient_coprime_totient_iff : ∀ (m n : ℕ), m.totient.Coprime n.totient ↔ (m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2
-- Mathlib.Topology.Connected.TotallyDisconnected
/-- The universal set `Set.univ` in a totally disconnected space is totally disconnected.  -/
TotallyDisconnectedSpace.isTotallyDisconnected_univ : ∀ {α : Type u} {inst : TopologicalSpace α} [self : TotallyDisconnectedSpace α], IsTotallyDisconnected Set.univ
-- Mathlib.MeasureTheory.Measure.WithDensity
/-- If `μ ≪ ν` and `ν` is s-finite, then `μ` is s-finite.  -/
MeasureTheory.sFinite_of_absolutelyContinuous : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.SFinite ν],
  μ.AbsolutelyContinuous ν → MeasureTheory.SFinite μ
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a fallback : α}, (m.erase k).getKeyD a fallback = if (k == a) = true then fallback else m.getKeyD a fallback
-- Mathlib.Order.Filter.Pi
Filter.tendsto_eval_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} (f : (i : ι) → Filter (α i)) (i : ι),
  Filter.Tendsto (Function.eval i) (Filter.pi f) (f i)
-- Mathlib.CategoryTheory.Grothendieck
/-- Given an equivalence of categories `G`, `preInv _ G` is the (weak) inverse of the `pre _ G.functor`.
 -/
CategoryTheory.Grothendieck.preInv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} D] →
        (F : CategoryTheory.Functor C CategoryTheory.Cat) →
          (G : D ≌ C) →
            CategoryTheory.Functor (CategoryTheory.Grothendieck F) (CategoryTheory.Grothendieck (G.functor.comp F))
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_alter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k k' fallback : α} {f : Option β → Option β},
  (m.alter k f).getKeyD k' fallback =
    if (k == k') = true then if (f m[k]?).isSome = true then k else fallback else m.getKeyD k' fallback
-- Lean.Elab.Do.Basic
Lean.Elab.Do.DoElemCont.mk.inj : ∀ {resultName : Lean.Name} {resultType : Lean.Expr} {k : Lean.Elab.Do.DoElabM Lean.Expr}
  {kind : Lean.Elab.Do.DoElemContKind} {resultName_1 : Lean.Name} {resultType_1 : Lean.Expr}
  {k_1 : Lean.Elab.Do.DoElabM Lean.Expr} {kind_1 : Lean.Elab.Do.DoElemContKind},
  { resultName := resultName, resultType := resultType, k := k, kind := kind } =
      { resultName := resultName_1, resultType := resultType_1, k := k_1, kind := kind_1 } →
    resultName = resultName_1 ∧ resultType = resultType_1 ∧ k = k_1 ∧ kind = kind_1
-- Mathlib.Topology.Order.DenselyOrdered
interior_Ioc : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [NoMaxOrder α] {a b : α}, interior (Set.Ioc a b) = Set.Ioo a b