mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.instNeg : {F : Type u} → [inst : Field F] → {W : WeierstrassCurve.Jacobian F} → Neg W.Point
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_toList_iff_get?_eq_some : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {k : α} {v : β k}, ⟨k, v⟩ ∈ m.toList ↔ m.get? k = some v
-- Mathlib.Algebra.Lie.LieTheorem
_private.Mathlib.Algebra.Lie.LieTheorem.0.LieModule.termπ : Lean.ParserDescr
-- Mathlib.Order.Shrink
instSuccOrderShrink : {α : Type u_1} → [inst : Small.{u, u_1} α] → [inst_1 : Preorder α] → [SuccOrder α] → SuccOrder (Shrink.{u, u_1} α)
-- Init.Grind.AC
Lean.Grind.AC.eq_simp_lhs_prefix : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op}
  (lhs₁ rhs₁ tail lhs₂ rhs₂ lhs₂' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.simp_prefix_cert lhs₁ rhs₁ tail lhs₂ lhs₂' = true →
    Lean.Grind.AC.Seq.denote ctx lhs₁ = Lean.Grind.AC.Seq.denote ctx rhs₁ →
      Lean.Grind.AC.Seq.denote ctx lhs₂ = Lean.Grind.AC.Seq.denote ctx rhs₂ →
        Lean.Grind.AC.Seq.denote ctx lhs₂' = Lean.Grind.AC.Seq.denote ctx rhs₂
-- Aesop.RuleTac.Basic
Aesop.Subgoal.mk.sizeOf_spec : ∀ (diff : Aesop.GoalDiff), sizeOf { diff := diff } = 1 + sizeOf diff
-- Lean.MetavarContext
/-- Never assigned by isDefEq  -/
Lean.MetavarKind.syntheticOpaque : Lean.MetavarKind
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.derivFamily_add_one : ∀ {ι : Type u_1} (f : ι → Ordinal.{u_2} → Ordinal.{u_2}) (o : Ordinal.{u_2}),
  Ordinal.derivFamily f (o + 1) = Ordinal.nfpFamily f (Ordinal.derivFamily f o + 1)
-- Mathlib.Algebra.Lie.Derivation.Killing
/-- A local notation for the set of (Lie) derivations on `L`.  -/
_private.Mathlib.Algebra.Lie.Derivation.Killing.0.LieDerivation.IsKilling.term𝔻 : Lean.ParserDescr
-- Mathlib.RingTheory.Spectrum.Prime.Topology
IsLocalRing.instBoundedOrderPrimeSpectrumOfIsDomain : (R : Type u) → [inst : CommSemiring R] → [IsLocalRing R] → [IsDomain R] → BoundedOrder (PrimeSpectrum R)
-- Mathlib.Topology.UniformSpace.Cauchy
SequentiallyComplete.setSeq_sub_aux : ∀ {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α}
  (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (n : ℕ),
  SequentiallyComplete.setSeq hf U_mem n ⊆ ↑(SequentiallyComplete.setSeqAux hf U_mem n)
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
LinearMap.isSymmetricProjection_iff_eq_coe_starProjection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {p : E →ₗ[𝕜] E}, p.IsSymmetricProjection ↔ ∃ K, ∃ (x : K.HasOrthogonalProjection), p = ↑K.starProjection
-- Mathlib.Data.Nat.Digits.Defs
_private.Mathlib.Data.Nat.Digits.Defs.0.Nat.digits.match_1.eq_3 : ∀ (motive : ℕ → Sort u_1) (b : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (b : ℕ) → motive b.succ.succ),
  (match b.succ.succ with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | b.succ.succ => h_3 b) =
    h_3 b
-- Init.Data.Nat.Div.Basic
Nat.mul_mod_right : ∀ (m n : ℕ), m * n % m = 0
-- Mathlib.Data.Finsupp.Basic
/-- Given `f : α ≃ β`, we can map `l : α →₀ M` to `equivMapDomain f l : β →₀ M` (computably)
by mapping the support forwards and the function backwards.  -/
Finsupp.equivMapDomain : {α : Type u_1} → {β : Type u_2} → {M : Type u_5} → [inst : Zero M] → α ≃ β → (α →₀ M) → β →₀ M
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
IsDecompositionField.toIsGaloisGroup : ∀ {K : Type u_2} {L : Type u_3} {B : Type u_4} {inst : Field K} {inst_1 : Field L} {inst_2 : Algebra K L}
  {inst_3 : CommRing B} {P : Ideal B} {D : Type u_5} {inst_4 : Field D} {inst_5 : Algebra D L}
  {inst_6 : MulSemiringAction Gal(L/K) B} [self : IsDecompositionField K L P D],
  IsGaloisGroup (↥(MulAction.stabilizer Gal(L/K) P)) D L
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.getOfNotLT? : Lean.Meta.Grind.Arith.Cutsat.ToIntM (Option Lean.Expr)
-- Mathlib.LinearAlgebra.Matrix.Bilinear
/-- A version of `LinearMap.mulRight_eq_zero_iff` for matrix multiplication.  -/
mulRightLinearMap_eq_zero_iff : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type u_5} {A : Type u_6} [inst : Fintype m] [inst_1 : Semiring R]
  [inst_2 : Semiring A] [inst_3 : Module R A] [inst_4 : IsScalarTower R A A] (a : Matrix m n A) [Nonempty l],
  mulRightLinearMap l R a = 0 ↔ a = 0
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.instInhabitedCode : Inhabited Turing.ToPartrec.Code
-- Lean.Parser.Extra
Lean.Parser.identWithPartialTrailingDot.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_fin_zero : ∀ {R : Type u_6} [inst : AddCommMonoid R] (A : Matrix (Fin 0) (Fin 0) R), A.trace = 0
-- Mathlib.Algebra.Category.Ring.Basic
_private.Mathlib.Algebra.Category.Ring.Basic.0.CommRingCat.Hom.mk.sizeOf_spec : ∀ {R S : CommRingCat} (hom' : ↑R →+* ↑S), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the
given key, returning `none` if no such pair exists.
 -/
Std.DTreeMap.getEntryGE? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → α → Option ((a : α) × β a)
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.isUniformEmbedding_coe : ∀ (α : Type u_1) [inst : UniformSpace α] [T0Space α], IsUniformEmbedding UniformSpace.Completion.coe'
-- Mathlib.Logic.Relation
Relation.EqvGen.eqvGen_le : ∀ {α : Type u_1} {r r' : α → α → Prop} [IsEquiv α r'], r ≤ r' → Relation.EqvGen r ≤ r'
-- Mathlib.Topology.Category.Sequential
/-- The underlying topological space is sequential.  -/
Sequential.is_sequential : ∀ (self : Sequential), SequentialSpace ↑self.toTop
-- Mathlib.Computability.TuringMachine.Config
_private.Mathlib.Computability.TuringMachine.Config.0.Turing.ToPartrec.Code.eval.match_1.splitter : (motive : Turing.ToPartrec.Code → Sort u_1) →
  (x : Turing.ToPartrec.Code) →
    (Unit → motive Turing.ToPartrec.Code.zero') →
      (Unit → motive Turing.ToPartrec.Code.succ) →
        (Unit → motive Turing.ToPartrec.Code.tail) →
          ((f fs : Turing.ToPartrec.Code) → motive (f.cons fs)) →
            ((f g : Turing.ToPartrec.Code) → motive (f.comp g)) →
              ((f g : Turing.ToPartrec.Code) → motive (f.case g)) →
                ((f : Turing.ToPartrec.Code) → motive f.fix) → motive x
-- Mathlib.Data.Fintype.Sum
Fintype.card_subtype_or : ∀ {α : Type u_1} (p q : α → Prop) [inst : Fintype { x // p x }] [inst_1 : Fintype { x // q x }]
  [inst_2 : Fintype { x // p x ∨ q x }],
  Fintype.card { x // p x ∨ q x } ≤ Fintype.card { x // p x } + Fintype.card { x // q x }
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.instOne : {M : Type u_1} → [inst : Monoid M] → One (Associates M)
-- Lean.Elab.Tactic.Omega.Frontend
/-- Allow elaboration of `OmegaConfig` arguments to tactics.
 -/
Lean.Elab.Tactic.Omega.elabOmegaConfig : Lean.Syntax →
  optParam Lean.Meta.Omega.OmegaConfig { } → optParam Bool true → Lean.Elab.Tactic.TacticM Lean.Meta.Omega.OmegaConfig
-- Mathlib.Data.EReal.Basic
EReal.coe_nsmul : ∀ (n : ℕ) (x : ℝ), ↑(n • x) = n • ↑x
-- Mathlib.Data.Finset.Empty
Finset.inhabitedFinset : {α : Type u_1} → Inhabited (Finset α)
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.Cofan.inj_apply_eq_iff_of_isColimit : ∀ {C : Type u} {F : C → Type v} {c : CategoryTheory.Limits.Cofan F} (hc : CategoryTheory.Limits.IsColimit c) {i j : C}
  (x : F i) (y : F j),
  (CategoryTheory.ConcreteCategory.hom (c.inj i)) x = (CategoryTheory.ConcreteCategory.hom (c.inj j)) y ↔
    ∃ (hij : i = j), y = cast ⋯ x
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.aeval_toMvPolynomial : ∀ {R : Type u_1} {S : Type u_2} {σ : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (f : σ → S) (i : σ) (p : Polynomial R),
  (MvPolynomial.aeval f) ((Polynomial.toMvPolynomial i) p) = (Polynomial.aeval (f i)) p
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalarsComp'App_hom_naturality_assoc : ∀ {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [inst : Ring R₁] [inst_1 : Ring R₂] [inst_2 : Ring R₃] (f : R₁ →+* R₂)
  (g : R₂ →+* R₃) (gf : R₁ →+* R₃) (hgf : gf = g.comp f) {M N : ModuleCat R₃} (φ : M ⟶ N) {Z : ModuleCat R₁}
  (h : (ModuleCat.restrictScalars f).obj ((ModuleCat.restrictScalars g).obj N) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars gf).map φ)
      (CategoryTheory.CategoryStruct.comp (ModuleCat.restrictScalarsComp'App f g gf hgf N).hom h) =
    CategoryTheory.CategoryStruct.comp (ModuleCat.restrictScalarsComp'App f g gf hgf M).hom
      (CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars f).map ((ModuleCat.restrictScalars g).map φ)) h)
-- Mathlib.Algebra.Module.ULift
ULift.smulZeroClass' : {R : Type u} → {M : Type v} → [inst : Zero M] → [SMulZeroClass R M] → SMulZeroClass R (ULift.{u_1, v} M)
-- Mathlib.Algebra.Group.Pi.Lemmas
ZeroHom.single.eq_1 : ∀ {I : Type u} (f : I → Type v) [inst : DecidableEq I] [inst_1 : (i : I) → Zero (f i)] (i : I),
  ZeroHom.single f i = { toFun := Pi.single i, map_zero' := ⋯ }
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.add_toOuterMeasure : ∀ {α : Type u_1} {_m : MeasurableSpace α} (μ₁ μ₂ : MeasureTheory.Measure α),
  (μ₁ + μ₂).toOuterMeasure = μ₁.toOuterMeasure + μ₂.toOuterMeasure
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.conj_trans : ∀ {R₁' : Type u_12} {R₂' : Type u_13} {R₃' : Type u_14} {M₁' : Type u_20} {M₂' : Type u_21} {M₃' : Type u_22}
  [inst : CommSemiring R₁'] [inst_1 : CommSemiring R₂'] [inst_2 : CommSemiring R₃'] [inst_3 : AddCommMonoid M₁']
  [inst_4 : AddCommMonoid M₂'] [inst_5 : AddCommMonoid M₃'] [inst_6 : Module R₁' M₁'] [inst_7 : Module R₂' M₂']
  [inst_8 : Module R₃' M₃'] {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} {σ₂'₃' : R₂' →+* R₃'} {σ₃'₂' : R₃' →+* R₂'}
  {σ₁'₃' : R₁' →+* R₃'} {σ₃'₁' : R₃' →+* R₁'} [inst_9 : RingHomInvPair σ₁'₂' σ₂'₁']
  [inst_10 : RingHomInvPair σ₂'₁' σ₁'₂'] [inst_11 : RingHomInvPair σ₂'₃' σ₃'₂'] [inst_12 : RingHomInvPair σ₃'₂' σ₂'₃']
  [inst_13 : RingHomInvPair σ₁'₃' σ₃'₁'] [inst_14 : RingHomInvPair σ₃'₁' σ₁'₃']
  [inst_15 : RingHomCompTriple σ₁'₂' σ₂'₃' σ₁'₃'] [inst_16 : RingHomCompTriple σ₃'₂' σ₂'₁' σ₃'₁']
  (e₁ : M₁' ≃ₛₗ[σ₁'₂'] M₂') (e₂ : M₂' ≃ₛₗ[σ₂'₃'] M₃'), e₁.conj.trans e₂.conj = (e₁.trans e₂).conj
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_sdiff_both : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, Set.Icc a b \ {a, b} = Set.Ioo a b
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly : Type
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
HasFDerivAt.continuousAlternatingMap_apply : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F [⋀^ι]→L[𝕜] G} {f' : E →L[𝕜] F [⋀^ι]→L[𝕜] G}
  {g : ι → E → F} {g' : ι → E →L[𝕜] F} {x : E} [inst_7 : Fintype ι] [inst_8 : DecidableEq ι],
  HasFDerivAt f f' x →
    (∀ (i : ι), HasFDerivAt (g i) (g' i) x) →
      HasFDerivAt (fun x => (f x) fun x_1 => g x_1 x)
        ((ContinuousAlternatingMap.apply 𝕜 F G fun x_1 => g x_1 x) ∘SL f' +
          ∑ i, (f x).toContinuousLinearMap (fun x_1 => g x_1 x) i ∘SL g' i)
        x
-- Init.Data.Vector.Attach
Vector.foldl_pmap : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {γ : Type u_3} {xs : Vector α n} {P : α → Prop} {f : (a : α) → P a → β}
  (H : ∀ a ∈ xs, P a) (g : γ → β → γ) (x : γ),
  Vector.foldl g x (Vector.pmap f xs H) = Vector.foldl (fun acc a => g acc (f ↑a ⋯)) x xs.attach
-- Mathlib.FieldTheory.Fixed
FixedPoints.smul_polynomial : ∀ (M : Type u) [inst : Monoid M] (F : Type v) [inst_1 : Field F] [inst_2 : MulSemiringAction M F] (m : M)
  (p : Polynomial ↥(FixedPoints.subfield M F)), m • p = p
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
RightDerivMeasurableAux.A_mem_nhdsGT : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {f : ℝ → F} {L : F} {r ε x : ℝ},
  x ∈ RightDerivMeasurableAux.A f L r ε → RightDerivMeasurableAux.A f L r ε ∈ nhdsWithin x (Set.Ioi x)
-- Mathlib.CategoryTheory.Adjunction.Reflective
CategoryTheory.unitCompPartialBijective.congr_simp : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {i : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Reflective i] (A : C) {B : C} (hB : i.essImage B),
  CategoryTheory.unitCompPartialBijective A hB = CategoryTheory.unitCompPartialBijective A hB
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instZSMul : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : AddGroup β] → [IsTopologicalAddGroup β] → SMul ℤ C(α, β)
-- Mathlib.CategoryTheory.Bicategory.Basic
/-- We state it as a simp lemma, which is regarded as an involved version of
`id_whiskerRight f g : 𝟙 f ▷ g = 𝟙 (f ≫ g)`.
 -/
CategoryTheory.Bicategory.leftUnitor_whiskerRight : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.leftUnitor f).hom g =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.id a) f g).hom
      (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.comp f g)).hom
-- Mathlib.Analysis.InnerProductSpace.Rayleigh
ContinuousLinearMap.rayleighQuotient_le_norm : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (T : E →L[𝕜] E) (x : E), |T.rayleighQuotient x| ≤ ‖T‖
-- Mathlib.GroupTheory.Subgroup.Saturated
/-- **Alias** of `AddSubmonoid.ker_saturated`. -/
AddSubgroup.ker_saturated : ∀ {A₁ : Type u_1} {A₂ : Type u_2} [inst : AddGroup A₁] [inst_1 : AddMonoid A₂] [IsAddTorsionFree A₂] (f : A₁ →+ A₂),
  f.ker.NSMulSaturated
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.coe_iInf : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {ι : Sort u_2} {S : ι → NonUnitalSubalgebra R A},
  ↑(⨅ i, S i) = ⋂ i, ↑(S i)
-- Mathlib.Algebra.Group.Equiv.Opposite
AddHom.fromOpposite_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N)
  (hf : ∀ (x y : M), AddCommute (f x) (f y)), ⇑(f.fromOpposite hf) = ⇑f ∘ AddOpposite.unop
-- Init.Core
/-- `EmptyCollection α` is the typeclass which supports the notation `∅`, also written as `{}`.  -/
EmptyCollection : Type u → Type u
-- Mathlib.Analysis.Normed.Group.Defs
NormedCommGroup.toNorm : {E : Type u_8} → [self : NormedCommGroup E] → Norm E
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.Gal.rootsEquivRoots.congr_simp : ∀ {F : Type u_1} [inst : Field F] (p : Polynomial F) (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E]
  [inst_3 : Fact (Polynomial.map (algebraMap F E) p).Splits],
  Polynomial.Gal.rootsEquivRoots p E = Polynomial.Gal.rootsEquivRoots p E
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.expSeries_sum_eq_div : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : Field 𝕂] [inst_1 : DivisionRing 𝔸] [inst_2 : Algebra 𝕂 𝔸]
  [inst_3 : TopologicalSpace 𝔸] [inst_4 : IsTopologicalRing 𝔸] (x : 𝔸),
  (NormedSpace.expSeries 𝕂 𝔸).sum x = ∑' (n : ℕ), x ^ n / ↑n.factorial
-- Mathlib.Algebra.Group.Action.Pretransitive
MulAction.IsPretransitive.of_smul_eq : ∀ {M : Type u_5} {N : Type u_6} {α : Type u_7} [inst : SMul M α] [inst_1 : SMul N α] [MulAction.IsPretransitive M α]
  (f : M → N), (∀ {c : M} {x : α}, f c • x = c • x) → MulAction.IsPretransitive N α
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.unop_w : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂ᵒᵖ}
  (L : Φ.op.LeftResolution X₂), L.unop.w = L.w.unop
-- Mathlib.RingTheory.Spectrum.Prime.Polynomial
Polynomial.mem_image_comap_C_basicOpen : ∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R) (x : PrimeSpectrum R),
  x ∈ PrimeSpectrum.comap Polynomial.C '' ↑(PrimeSpectrum.basicOpen f) ↔ ∃ i, f.coeff i ∉ x.asIdeal
-- Init.Data.String.Basic
String.Pos.extract : {s : String} → s.Pos → s.Pos → String
-- Mathlib.Analysis.Complex.SqrtDeriv
Complex.hasDerivWithinAt_sqrt : ∀ {z : ℂ} {s : Set ℂ}, z ∈ Complex.slitPlane → HasDerivWithinAt Complex.sqrt (z ^ (-1 / 2) / 2) s z
-- Mathlib.LinearAlgebra.Complex.Module
Complex.coe_basisOneI_repr : ∀ (z : ℂ), ⇑(Complex.basisOneI.repr z) = ![z.re, z.im]
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.foldr_le_nfpFamily : ∀ {ι : Type u_1} [Small.{u, u_1} ι] (f : ι → Ordinal.{u} → Ordinal.{u}) (a : Ordinal.{u}) (l : List ι),
  List.foldr f a l ≤ Ordinal.nfpFamily f a
-- Mathlib.MeasureTheory.OuterMeasure.Basic
MeasureTheory.measure_lt_top_mono : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F}
  {s t : Set α}, s ⊆ t → μ t < ⊤ → μ s < ⊤
-- Batteries.Data.ByteArray
ByteArray.get_push_lt : ∀ (a : ByteArray) (x : UInt8) (i : ℕ) (h : i < a.size), (a.push x)[i] = a[i]
-- Mathlib.Order.Hom.Lattice
SupHom.const_apply : ∀ (α : Type u_2) {β : Type u_3} [inst : Max α] [inst_1 : SemilatticeSup β] (b : β) (a : α), (SupHom.const α b) a = b
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.mulCayley_mono : ∀ {M : Type u_1} [inst : Mul M] {U V : Set M}, U ⊆ V → SimpleGraph.mulCayley U ≤ SimpleGraph.mulCayley V
-- Lean.Meta.Tactic.Grind.Action
_private.Lean.Meta.Tactic.Grind.Action.0.Lean.Meta.Grind.Action.loop.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.algEquivOfCompEqX.congr_simp : ∀ {R : Type u} [inst : CommSemiring R] (p p_1 : Polynomial R) (e_p : p = p_1) (q q_1 : Polynomial R) (e_q : q = q_1)
  (hpq : p.comp q = Polynomial.X) (hqp : q.comp p = Polynomial.X),
  p.algEquivOfCompEqX q hpq hqp = p_1.algEquivOfCompEqX q_1 ⋯ ⋯
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The opposite of the right homology functor is the left homology functor.  -/
CategoryTheory.ShortComplex.rightHomologyFunctorOpNatIso : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasKernels C] →
        [inst_3 : CategoryTheory.Limits.HasCokernels C] →
          [inst_4 : CategoryTheory.Limits.HasKernels Cᵒᵖ] →
            [inst_5 : CategoryTheory.Limits.HasCokernels Cᵒᵖ] →
              (CategoryTheory.ShortComplex.rightHomologyFunctor C).op ≅
                (CategoryTheory.ShortComplex.opFunctor C).comp (CategoryTheory.ShortComplex.leftHomologyFunctor Cᵒᵖ)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] [inst_2 : Inhabited α] {l : List ((_ : α) × Unit)} {toInsert : List α}
  {k : α},
  Std.Internal.List.containsKey k l = false →
    toInsert.contains k = false →
      Std.Internal.List.getKey! k (Std.Internal.List.insertListIfNewUnit l toInsert) = default
-- Mathlib.Order.Grade
GradeBoundedOrder.toGradeMinOrder : {𝕆 : Type u_5} →
  {α : Type u_6} → {inst : Preorder 𝕆} → {inst_1 : Preorder α} → [self : GradeBoundedOrder 𝕆 α] → GradeMinOrder 𝕆 α
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
/-- The difference of `log (1+z)` and its `(n+1)`st Taylor polynomial can be bounded in
terms of `‖z‖`.  -/
Complex.norm_log_sub_logTaylor_le : ∀ (n : ℕ) {z : ℂ},
  ‖z‖ < 1 → ‖Complex.log (1 + z) - Complex.logTaylor (n + 1) z‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
/-- The obvious map `Fork f g → Cofork f.op g.op`  -/
CategoryTheory.Limits.Fork.op : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → {f g : X ⟶ Y} → CategoryTheory.Limits.Fork f g → CategoryTheory.Limits.Cofork f.op g.op
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.IsRegular.toIsProper : ∀ {X : SSet} {A : X.Subcomplex} {h : A.PairingCore} [self : h.IsRegular], h.IsProper
-- Mathlib.CategoryTheory.Center.Localization
CategoryTheory.CatCenter.localization_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (r s : CategoryTheory.CatCenter C) (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [inst_2 : L.IsLocalization W], (r * s).localization L W = r.localization L W * s.localization L W
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.instModularFormClassOfCuspFormClass : ∀ {F : Type u_1} {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [inst : FunLike F UpperHalfPlane ℂ] [CuspFormClass F Γ k],
  ModularFormClass F Γ k
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inl_v_fst_v_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (p q : ℤ) (hpq : q + 1 = p)
  {Z : C} (h : F.X p ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v p q ⋯)
      (CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v q p hpq) h) =
    h
-- Mathlib.Data.EReal.Operations
EReal.mul_ne_bot : ∀ (a b : EReal), a * b ≠ ⊥ ↔ (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤)
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.isPartition_iff_iUnion_eq : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I}, π.IsPartition ↔ π.iUnion = ↑I
-- Mathlib.Data.Nat.Nth
Nat.nth_true : ∀ (n : ℕ), Nat.nth (fun x => True) n = n
-- Mathlib.Algebra.Group.Fin.Basic
/-- This is not a global instance, but can introduced locally using `open Fin.NatCast in ...`.

This is not an instance because the `binop%` elaborator assumes that
there are no non-trivial coercion loops,
but this instance would introduce a coercion from `Nat` to `Fin n` and back.
Non-trivial loops lead to undesirable and counterintuitive elaboration behavior.

For example, for `x : Fin k` and `n : Nat`,
it causes `x < n` to be elaborated as `x < ↑n` rather than `↑x < n`,
silently introducing wraparound arithmetic.
 -/
Fin.instAddMonoidWithOne : (n : ℕ) → [NeZero n] → AddMonoidWithOne (Fin n)
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.loogleTacticImpl : Lean.Elab.Tactic.Tactic
-- Mathlib.Data.List.Chain
List.isChain_cons_map_of_isChain_cons : ∀ {α : Type u_1} {β : Type u_2} {R : α → α → Prop} {a : α} {S : β → β → Prop} (f : α → β),
  (∀ (a b : α), R a b → S (f a) (f b)) → ∀ {l : List α}, List.IsChain R (a :: l) → List.IsChain S (f a :: List.map f l)
-- Mathlib.LinearAlgebra.Prod
LinearEquiv.skewProd_symm_apply : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : AddCommGroup M₄] {module_M : Module R M}
  {module_M₂ : Module R M₂} {module_M₃ : Module R M₃} {module_M₄ : Module R M₄} (e₁ : M ≃ₗ[R] M₂) (e₂ : M₃ ≃ₗ[R] M₄)
  (f : M →ₗ[R] M₄) (x : M₂ × M₄), (e₁.skewProd e₂ f).symm x = (e₁.symm x.1, e₂.symm (x.2 - f (e₁.symm x.1)))