mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.IsCofiltered.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [toIsCofilteredOrEmpty : CategoryTheory.IsCofilteredOrEmpty C]
  [nonempty : Nonempty C], CategoryTheory.IsCofiltered C
-- Mathlib.MeasureTheory.Function.Holder
ContinuousLinearMap.lpPairing_eq_integral : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {p q : ENNReal} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G) [inst_7 : Fact (1 ≤ p)] [inst_8 : Fact (1 ≤ q)]
  [inst_9 : p.HolderConjugate q] [inst_10 : NormedSpace ℝ G] [inst_11 : SMulCommClass ℝ 𝕜 G] [inst_12 : CompleteSpace G]
  (f : ↥(MeasureTheory.Lp E p μ)) (g : ↥(MeasureTheory.Lp F q μ)),
  ((ContinuousLinearMap.lpPairing μ p q B) f) g = ∫ (x : α), (B (↑↑f x)) (↑↑g x) ∂μ
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurablePow.measurable_pow : ∀ {β : Type u_2} {γ : Type u_3} {inst : MeasurableSpace β} {inst_1 : MeasurableSpace γ} {inst_2 : Pow β γ}
  [self : MeasurablePow β γ], Measurable fun p => p.1 ^ p.2
-- Mathlib.NumberTheory.LucasLehmer
/-- We define `ωb = 2 - √3`, which is the inverse of `ω`.  -/
LucasLehmer.X.ωb : {q : ℕ} → LucasLehmer.X q
-- Mathlib.Order.Atoms
IsAtom.le_sSup : ∀ {α : Type u_2} [inst : Order.Frame α] {s : Set α} {a : α}, IsAtom a → (a ≤ sSup s ↔ ∃ b ∈ s, a ≤ b)
-- Mathlib.CategoryTheory.Localization.HomEquiv
CategoryTheory.LocalizerMorphism.homMap_map : ∀ {C₁ : Type u_2} {C₂ : Type u_3} {D₁ : Type u_5} {D₂ : Type u_6} [inst : CategoryTheory.Category.{v_2, u_2} C₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C₂] [inst_2 : CategoryTheory.Category.{v_5, u_5} D₁]
  [inst_3 : CategoryTheory.Category.{v_6, u_6} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  (L₁ : CategoryTheory.Functor C₁ D₁) [inst_4 : L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂)
  [inst_5 : L₂.IsLocalization W₂] {X Y : C₁} (f : X ⟶ Y), Φ.homMap L₁ L₂ (L₁.map f) = L₂.map (Φ.functor.map f)
-- Mathlib.Algebra.Notation.Pi.Basic
Pi.uncurry_single_single : ∀ {ι : Type u_1} {ι' : Type u_2} [inst : DecidableEq ι] {M : Type u_9} [inst_1 : Zero M] [inst_2 : DecidableEq ι']
  (i : ι) (i' : ι') (b : M), Function.uncurry (Pi.single i (Pi.single i' b)) = Pi.single (i, i') b
-- Mathlib.Order.DirSupClosed
DirSupClosed.iInter : ∀ {α : Type u_1} [inst : Preorder α] {ι : Sort u_2} {f : ι → Set α},
  (∀ (i : ι), DirSupClosed (f i)) → DirSupClosed (⋂ i, f i)
-- Mathlib.Data.Multiset.Filter
Multiset.filter_map : ∀ {α : Type u_1} {β : Type v} (p : α → Prop) [inst : DecidablePred p] (f : β → α) (s : Multiset β),
  Multiset.filter p (Multiset.map f s) = Multiset.map f (Multiset.filter (p ∘ f) s)
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
MvPolynomial.mapEquivMonic.eq_1 : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (n : ℕ),
  MvPolynomial.mapEquivMonic R S n =
    { toFun := fun f => (Polynomial.MonicDegreeEq.freeMonic R n).map f.toRingHom,
      invFun := fun p => MvPolynomial.aeval fun x => (↑p).coeff ↑x, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso_inv_τ₁ : ∀ {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.kernelSequenceOpcyclesEIso._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso._auto_3),
  (X.kernelSequenceOpcyclesEIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv.τ₁ =
    CategoryTheory.CategoryStruct.id (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).homology
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_union : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α},
  Std.DTreeMap.Internal.Impl.Const.get! (m₁.union m₂ ⋯ ⋯) k =
    Std.DTreeMap.Internal.Impl.Const.getD m₂ k (Std.DTreeMap.Internal.Impl.Const.get! m₁ k)
-- Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying
/-- The currying operation taking a morphism `(z ⊗ y) ⟶ x` to a morphism `y ⟶ C(z, x)`,
constructed as a morphism in `C` between internal homs.  -/
CategoryTheory.MonoidalClosed.ihomCurry : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (x y z : C) →
        [inst_2 : CategoryTheory.Closed x] →
          [inst_3 : CategoryTheory.Closed y] →
            [inst_4 : CategoryTheory.Closed (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)] →
              CategoryTheory.MonoidalCategoryStruct.tensorObj x y ⟹ z ⟶ y ⟹ x ⟹ z
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.ProjectivePresentation.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X p : C} {projective : CategoryTheory.Projective p}
  {f : p ⟶ X} {epi : CategoryTheory.Epi f} {p_1 : C} {projective_1 : CategoryTheory.Projective p_1} {f_1 : p_1 ⟶ X}
  {epi_1 : CategoryTheory.Epi f_1},
  { p := p, projective := projective, f := f, epi := epi } =
      { p := p_1, projective := projective_1, f := f_1, epi := epi_1 } →
    p = p_1 ∧ f ≍ f_1
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
Bundle.Trivialization.contMDiffWithinAt_iff : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6}
  [inst : NontriviallyNormedField 𝕜] {EB : Type u_7} [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB]
  {HB : Type u_8} [inst_3 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B]
  [inst_5 : ChartedSpace HB B] {EM : Type u_9} [inst_6 : NormedAddCommGroup EM] [inst_7 : NormedSpace 𝕜 EM]
  {HM : Type u_10} [inst_8 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace HM M] [inst_11 : (x : B) → AddCommMonoid (E x)] [inst_12 : (x : B) → Module 𝕜 (E x)]
  [inst_13 : NormedAddCommGroup F] [inst_14 : NormedSpace 𝕜 F] [inst_15 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_16 : (x : B) → TopologicalSpace (E x)] [inst_17 : FiberBundle F E] [inst_18 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle n F E IB] {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e]
  {f : M → Bundle.TotalSpace F E} {s : Set M} {x₀ : M},
  f x₀ ∈ e.source →
    (ContMDiffWithinAt IM (IB.prod (modelWithCornersSelf 𝕜 F)) n f s x₀ ↔
      ContMDiffWithinAt IM IB n (fun x => (f x).proj) s x₀ ∧
        ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 F) n (fun x => (↑e (f x)).2) s x₀)
-- Lean.Meta.LazyDiscrTree
/-- Push lazy entry to trie.  -/
Lean.Meta.LazyDiscrTree.Trie.pushPending : {α : Type} → Lean.Meta.LazyDiscrTree.Trie α → Lean.Meta.LazyDiscrTree.LazyEntry α → Lean.Meta.LazyDiscrTree.Trie α
-- Std.Time.Notation
_private.Std.Time.Notation.0.Std.Time.syntaxBounded : ℤ → Lean.MacroM (Lean.TSyntax `term)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.IsAddMonHom.addMonoidHom_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N O X : C} [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.AddMonObj N]
  [inst_4 : CategoryTheory.AddMonObj O] (f : M ⟶ N) (g : N ⟶ O) [inst_5 : CategoryTheory.IsAddMonHom f]
  [inst_6 : CategoryTheory.IsAddMonHom g],
  CategoryTheory.IsAddMonHom.addMonoidHom (CategoryTheory.CategoryStruct.comp f g) X =
    (CategoryTheory.IsAddMonHom.addMonoidHom g X).comp (CategoryTheory.IsAddMonHom.addMonoidHom f X)
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- The trailing coefficient of a product is the product of the trailing coefficients.
 -/
MeromorphicAt.meromorphicTrailingCoeffAt_fun_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {f₁ f₂ : 𝕜 → 𝕜},
  MeromorphicAt f₁ x →
    MeromorphicAt f₂ x →
      meromorphicTrailingCoeffAt (fun z => f₁ z * f₂ z) x =
        meromorphicTrailingCoeffAt f₁ x * meromorphicTrailingCoeffAt f₂ x
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_sUnion_le : ∀ {α : Type u} (A : Set (Set α)), Cardinal.mk ↑(⋃₀ A) ≤ Cardinal.mk ↑A * ⨆ s, Cardinal.mk ↑↑s
-- Aesop.Forward.State
/-- Metavariables for the premises of the rule for which a hyp or match is
being added. When adding hyps, they are unified with these metavariables.  -/
Aesop.ClusterState.AddM.Context.premiseMVars : Aesop.ClusterState.AddM.Context → Array Lean.MVarId
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.norm_fst : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : StarRing A]
  [CStarRing A] (a : DoubleCentralizer 𝕜 A), ‖a.toProd.1‖ = ‖a‖
-- Mathlib.RingTheory.TensorProduct.Quotient
/-- The tensor product over `R` of the quotient of an `S`-algebra `A` by an ideal `I` with `T`
is isomorphic (as an `S`-algebra) to the quotient of `A ⊗[R] T` by the extended ideal.  -/
Algebra.TensorProduct.quotientTensorEquiv : {R : Type u_1} →
  (S : Type u_2) →
    (T : Type u_3) →
      (A : Type u_4) →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              [inst_3 : CommRing T] →
                [inst_4 : Algebra R T] →
                  [inst_5 : CommRing A] →
                    [inst_6 : Algebra R A] →
                      [inst_7 : Algebra S A] →
                        [inst_8 : IsScalarTower R S A] →
                          (I : Ideal A) →
                            TensorProduct R (A ⧸ I) T ≃ₐ[S]
                              TensorProduct R A T ⧸ Ideal.map (algebraMap A (TensorProduct R A T)) I
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.IrreducibleCloseds.instCanLiftSetCoeAndIsIrreducibleIsClosed : ∀ {α : Type u_2} [inst : TopologicalSpace α],
  CanLift (Set α) (TopologicalSpace.IrreducibleCloseds α) SetLike.coe fun s => IsIrreducible s ∧ IsClosed s
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- If `g` is a linear map `M → M''` such that all scalar multiplication by `s : S` is invertible, then
there is a linear map `LocalizedModule S M → M''`.
 -/
LocalizedModule.lift' : {R : Type u_1} →
  [inst : CommSemiring R] →
    (S : Submonoid R) →
      {M : Type u_2} →
        {M'' : Type u_4} →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid M''] →
              [inst_3 : Module R M] →
                [inst_4 : Module R M''] →
                  (M →ₗ[R] M'') →
                    (∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) → LocalizedModule S M → M''
-- Init.Data.UInt.BasicAux
/-- Converts 8-bit unsigned integers to 64-bit unsigned integers.

This function is overridden at runtime with an efficient implementation.
 -/
UInt8.toUInt64 : UInt8 → UInt64
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mathlib.Tactic.MonTauto.associator_hom_comp_tensorHom_tensorHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) (h : Z₁ ⟶ Z₂),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ Y₁ Z₁).hom
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.MonoidalCategoryStruct.tensorHom g h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) h)
      (CategoryTheory.MonoidalCategoryStruct.associator X₂ Y₂ Z₂).hom
-- Mathlib.GroupTheory.Perm.Centralizer
/-- The number of cycles of given length  -/
Equiv.Perm.card_of_cycleType_singleton : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {n : ℕ},
  2 ≤ n → n ≤ Fintype.card α → {g | g.cycleType = {n}}.card = (n - 1).factorial * (Fintype.card α).choose n
-- Mathlib.Geometry.Convex.Cone.Pointed
/-- The preimage of a pointed cone under an `R`-linear map is a pointed cone.  -/
PointedCone.comap : {R : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : PartialOrder R] →
          [inst_2 : IsOrderedRing R] →
            [inst_3 : AddCommMonoid E] →
              [inst_4 : Module R E] →
                [inst_5 : AddCommMonoid F] → [inst_6 : Module R F] → (E →ₗ[R] F) → PointedCone R F → PointedCone R E
-- Mathlib.CategoryTheory.Limits.Types.Yoneda
/-- Sections of `F ⋙ coyoneda.obj (op X)` identify to natural
transformations `(const J).obj X ⟶ F`.  -/
CategoryTheory.Limits.compCoyonedaSectionsEquiv : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        (F : CategoryTheory.Functor J C) →
          (X : C) →
            ↑(F.comp (CategoryTheory.coyoneda.obj (Opposite.op X))).sections ≃
              ((CategoryTheory.Functor.const J).obj X ⟶ F)
-- Mathlib.Algebra.Opposites
MulOpposite.opEquiv_apply : ∀ {α : Type u_1}, ⇑MulOpposite.opEquiv = MulOpposite.op
-- Mathlib.RingTheory.Bialgebra.Equiv
/-- Reinterpret an element of a type of bialgebra equivalences as a bialgebra equivalence.  -/
BialgEquivClass.instCoeToBialgEquiv : {F : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Semiring B] →
              [inst_3 : Algebra R A] →
                [inst_4 : Algebra R B] →
                  [inst_5 : CoalgebraStruct R A] →
                    [inst_6 : CoalgebraStruct R B] →
                      [inst_7 : EquivLike F A B] → [BialgEquivClass F R A B] → CoeHead F (A ≃ₐc[R] B)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
CategoryTheory.MorphismProperty.LeftFraction₂.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y Y' : C}
  (f f' : X ⟶ Y') (s : Y ⟶ Y') (hs : W s) (Y'_1 : C) (f_1 f'_1 : X ⟶ Y'_1) (s_1 : Y ⟶ Y'_1) (hs_1 : W s_1),
  ({ Y' := Y', f := f, f' := f', s := s, hs := hs } = { Y' := Y'_1, f := f_1, f' := f'_1, s := s_1, hs := hs_1 }) =
    (Y' = Y'_1 ∧ f ≍ f_1 ∧ f' ≍ f'_1 ∧ s ≍ s_1)
-- Mathlib.RingTheory.Polynomial.DegreeLT
Polynomial.degreeLT.addLinearEquiv_symm_apply : ∀ {R : Type u_1} [inst : Semiring R] {m n : ℕ} (PQ : ↥(Polynomial.degreeLT R m) × ↥(Polynomial.degreeLT R n)),
  ↑((Polynomial.degreeLT.addLinearEquiv R m n).symm PQ) = ↑PQ.1 + ↑PQ.2 * Polynomial.X ^ m
-- Mathlib.Analysis.Normed.Operator.Extend
ContinuousLinearMap.extend_unique : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} [inst : AddCommGroup E]
  [inst_1 : UniformSpace E] [inst_2 : IsUniformAddGroup E] [inst_3 : AddCommGroup F] [inst_4 : UniformSpace F]
  [inst_5 : IsUniformAddGroup F] [inst_6 : T0Space F] [inst_7 : AddCommMonoid Eₗ] [inst_8 : UniformSpace Eₗ]
  [inst_9 : ContinuousAdd Eₗ] [inst_10 : Semiring 𝕜] [inst_11 : Semiring 𝕜₂] [inst_12 : Module 𝕜 E]
  [inst_13 : Module 𝕜₂ F] [inst_14 : Module 𝕜 Eₗ] [inst_15 : ContinuousConstSMul 𝕜 Eₗ]
  [inst_16 : ContinuousConstSMul 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) [inst_17 : CompleteSpace F] {e : E →L[𝕜] Eₗ},
  DenseRange ⇑e → IsUniformInducing ⇑e → ∀ (g : Eₗ →SL[σ₁₂] F), g ∘SL e = f → f.extend e = g
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.lift.congr_simp : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {α : Type u_2}
  (f f_1 : M → α) (e_f : f = f_1) (h : ∀ (a b : M), MulArchimedeanClass.mk a = MulArchimedeanClass.mk b → f a = f b)
  (a a_1 : MulArchimedeanClass M), a = a_1 → MulArchimedeanClass.lift f h a = MulArchimedeanClass.lift f_1 ⋯ a_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.filter_key_equiv_self_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] {f : α → Bool}
  (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter (fun k x => f k) t ⋯).impl.Equiv t ↔
    ∀ (a : α) (h : Std.DTreeMap.Internal.Impl.contains a t = true), f (t.getKey a h) = true
-- Mathlib.Tactic.Simproc.ExistsAndEq
/-- Traverses `P` and `goal` simultaneously, proving `goal`.  -/
_private.Mathlib.Tactic.Simproc.ExistsAndEq.0.ExistsAndEq.mkAfterToBefore.go : {goal P : Q(Prop)} → Q(«$P») → List ExistsAndEq.VarQ → ExistsAndEq.Path → Lean.MetaM Q(«$goal»)
-- Mathlib.Algebra.Group.Units.Hom
AddUnits.coeHom_apply : ∀ {M : Type u} [inst : AddMonoid M] (x : AddUnits M), (AddUnits.coeHom M) x = ↑x
-- Mathlib.Combinatorics.HalesJewett
/-- A line in `ι → α` and a point in `ι' → α` determine a line in `ι ⊕ ι' → α`.  -/
Combinatorics.Line.horizontal : {α : Type u_5} → {ι : Type u_6} → {ι' : Type u_7} → Combinatorics.Line α ι → (ι' → α) → Combinatorics.Line α (ι ⊕ ι')
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.neg_v : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} {n : ℤ} (z : CochainComplex.HomComplex.Cochain F G n) (p q : ℤ) (hpq : p + n = q),
  (-z).v p q hpq = -z.v p q hpq
-- Mathlib.Algebra.Algebra.Tower
AlgEquiv.restrictScalars_injective : ∀ (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B],
  Function.Injective (AlgEquiv.restrictScalars R)
-- Mathlib.Data.Multiset.Replicate
Multiset.replicate_le_coe : ∀ {α : Type u_1} {a : α} {n : ℕ} {l : List α}, Multiset.replicate n a ≤ ↑l ↔ (List.replicate n a).Sublist l
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.instSetLike.eq_1 : ∀ {G : Type u_1} [inst : Group G],
  FiniteIndexNormalSubgroup.instSetLike = { coe := fun U => ↑U.toSubgroup, coe_injective := ⋯ }
-- Mathlib.Topology.Compactness.SigmaCompact
/-- If `f : X → Y` is an embedding, the image `f '' s` of a set `s` is σ-compact
if and only `s` is σ-compact.  -/
Topology.IsEmbedding.isSigmaCompact_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X},
  Topology.IsEmbedding f → (IsSigmaCompact s ↔ IsSigmaCompact (f '' s))
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Power.x : Lean.Grind.CommRing.Power → Lean.Grind.CommRing.Var
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedSubgroup.mk.inj : ∀ {G : Type u} {inst : Group G} {inst_1 : TopologicalSpace G} {toSubgroup : Subgroup G}
  {isClosed' : IsClosed toSubgroup.carrier} {toSubgroup_1 : Subgroup G} {isClosed'_1 : IsClosed toSubgroup_1.carrier},
  { toSubgroup := toSubgroup, isClosed' := isClosed' } = { toSubgroup := toSubgroup_1, isClosed' := isClosed'_1 } →
    toSubgroup = toSubgroup_1
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.lift_of_eq_id : ∀ (α : Type u_1), FreeGroup.lift FreeGroup.of = MonoidHom.id (FreeGroup α)
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
Finset.measurableSet : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α] (s : Finset α), MeasurableSet ↑s
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.ext_contains_unit : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {t₁ t₂ : Std.ExtDTreeMap α (fun x => Unit) cmp}, (∀ (k : α), t₁.contains k = t₂.contains k) → t₁ = t₂
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.size_alter_le_size : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {f : Option β → Option β}, (Std.DHashMap.Const.alter m k f).size ≤ m.size + 1
-- Std.Do.WP.Sound
Std.Do.instWPSoundEStateMExceptArgPure : ∀ {ε σ : Type u_1},
  Std.Do.WPSound (EStateM ε σ) (Std.Do.PostShape.except ε (Std.Do.PostShape.arg σ Std.Do.PostShape.pure))
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.IsInduced.induce_top_verts : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph}, G'.IsInduced → ⊤.induce G'.verts = G'
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.prime_idealOfLE : ∀ {K : Type u} [inst : Field K] (R S : ValuationSubring K) (h : R ≤ S), (R.idealOfLE S h).IsPrime
-- Mathlib.Topology.Continuous
/-- If a continuous map with dense range maps a dense set to a subset of `t`, then `t` is a dense
set.  -/
DenseRange.dense_of_mapsTo : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {f : X → Y},
  DenseRange f → Continuous f → Dense s → ∀ {t : Set Y}, Set.MapsTo f s t → Dense t
-- Mathlib.RingTheory.Polynomial.Quotient
/-- For a commutative ring $R$, evaluating a polynomial at elements $y(X) \in R[X]$ and $x \in R$
induces an isomorphism of $R$-algebras $R[X, Y] / \langle X - x, Y - y(X) \rangle \cong R$.  -/
Polynomial.quotientSpanCXSubCXSubCAlgEquiv : {R : Type u_1} →
  [inst : CommRing R] →
    {x : R} →
      {y : Polynomial R} →
        (Polynomial (Polynomial R) ⧸
            Ideal.span {Polynomial.C (Polynomial.X - Polynomial.C x), Polynomial.X - Polynomial.C y}) ≃ₐ[R]
          R
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
/-- The difference with `Finset.prod_ite_eq_of_mem` is that the arguments to `Eq` are swapped.  -/
Finset.prod_ite_eq_of_mem' : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : DecidableEq ι] (s : Finset ι) (a : ι) (b : ι → M),
  a ∈ s → (∏ x ∈ s, if x = a then b x else 1) = b a
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Functor.homMonoidHom.eq_1 : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v, u_1} C]
  [inst_1 : CategoryTheory.CartesianMonoidalCategory C] [inst_2 : CategoryTheory.Category.{w, u_2} D]
  [inst_3 : CategoryTheory.CartesianMonoidalCategory D] {M X : C} [inst_4 : CategoryTheory.MonObj M]
  (F : CategoryTheory.Functor C D) [inst_5 : F.Monoidal],
  F.homMonoidHom = { toFun := F.map, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.ofTwoCocycle.mk.sizeOf_spec : ∀ {R : Type u_5} {L : Type u_6} {M : Type u_7} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  {c : ↥(LieModule.Cohomology.twoCocycle R L M)} [inst_7 : SizeOf R] [inst_8 : SizeOf L] [inst_9 : SizeOf M]
  (carrier : L × M), sizeOf { carrier := carrier } = 1 + sizeOf carrier
-- Mathlib.Analysis.Analytic.Basic
AnalyticOnNhd.eq_1 : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F) (s : Set E),
  AnalyticOnNhd 𝕜 f s = ∀ x ∈ s, AnalyticAt 𝕜 f x
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
/-- The functor `J ⥤ MonoOver X` which sends `j : J` to the inverse image by `z : X ⟶ c.pt`
of the subobject `Y.obj j` of `c.pt`; it is defined here as the object in `MonoOver X`
corresponding to the monomorphism
`(pullback.snd c.ι ((Functor.const _).map z)).app j`.  -/
CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.F : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Abelian C] →
      {X : C} →
        {J : Type w} →
          [inst_2 : CategoryTheory.SmallCategory J] →
            {Y : CategoryTheory.Functor J C} →
              {c : CategoryTheory.Limits.Cocone Y} →
                (X ⟶ c.pt) → [CategoryTheory.Mono c.ι] → CategoryTheory.Functor J (CategoryTheory.MonoOver X)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.ofList_nil : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α],
  Std.ExtDHashMap.Const.ofList [] = ∅