mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.Attach
List.map_attachWith : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {P : α → Prop} {H : ∀ a ∈ l, P a} {f : { x // P x } → β},
  List.map f (l.attachWith P H) =
    List.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => f ⟨x, ⋯⟩)
      l.attach
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- The composition of morphisms between algebras of endofunctor `F`  -/
CategoryTheory.Endofunctor.Algebra.Hom.comp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C C} →
      {A₀ A₁ A₂ : CategoryTheory.Endofunctor.Algebra F} → A₀.Hom A₁ → A₁.Hom A₂ → A₀.Hom A₂
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.IsSubDPIdeal.mk : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {hI : DividedPowers I} {J : Ideal A},
  J ≤ I → (∀ (n : ℕ), n ≠ 0 → ∀ {j : A}, j ∈ J → hI.dpow n j ∈ J) → hI.IsSubDPIdeal J
-- Mathlib.Algebra.Lie.CartanCriterion
/-- If the trace form of `M` is zero, then the `⁅L, L⁆`-module `M` is nilpotent.  -/
LieModule.isNilpotent_derivedSeries_of_traceForm_eq_zero : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [CharZero R] [IsDomain R] [inst_3 : LieRing L]
  [inst_4 : LieAlgebra R L] [inst_5 : AddCommGroup M] [inst_6 : LieRingModule L M] [inst_7 : Module R M]
  [inst_8 : LieModule R L M] [IsNoetherian R M] [Module.Free R M],
  LieModule.traceForm R L M = 0 → LieModule.IsNilpotent (↥(LieAlgebra.derivedSeries R L 1)) M
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.fermatLastTheoremThree_of_dvd_a_of_gcd_eq_one_of_case2 : ∀ {a b c : ℤ},
  a ≠ 0 →
    3 ∣ a →
      {a, b, c}.gcd id = 1 →
        (∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3) →
          a ^ 3 + b ^ 3 + c ^ 3 ≠ 0
-- Mathlib.Analysis.Normed.Group.Hom
/-- Given `φ : NormedAddGroupHom V₁ V₂` and `ψ : NormedAddGroupHom W₁ W₂` such that
`ψ.comp f₁ = f₂.comp φ` and `ψ.comp g₁ = g₂.comp φ`, the induced morphism
`NormedAddGroupHom (f₁.equalizer g₁) (f₂.equalizer g₂)`.  -/
NormedAddGroupHom.Equalizer.map : {V₁ : Type u_3} →
  {V₂ : Type u_4} →
    [inst : SeminormedAddCommGroup V₁] →
      [inst_1 : SeminormedAddCommGroup V₂] →
        {W₁ : Type u_6} →
          {W₂ : Type u_7} →
            [inst_2 : SeminormedAddCommGroup W₁] →
              [inst_3 : SeminormedAddCommGroup W₂] →
                {f₁ g₁ : NormedAddGroupHom V₁ W₁} →
                  {f₂ g₂ : NormedAddGroupHom V₂ W₂} →
                    (φ : NormedAddGroupHom V₁ V₂) →
                      (ψ : NormedAddGroupHom W₁ W₂) →
                        ψ.comp f₁ = f₂.comp φ →
                          ψ.comp g₁ = g₂.comp φ → NormedAddGroupHom ↥(f₁.equalizer g₁) ↥(f₂.equalizer g₂)
-- Mathlib.Analysis.Meromorphic.Divisor
/-- Divisors are invariant under translation.  -/
MeromorphicOn.divisor_comp_sub_const_eq_divisor : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {z : 𝕜} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {c : 𝕜} {f : 𝕜 → E},
  (MeromorphicOn.divisor (f ∘ fun x => x - c) U) (z + c) = (MeromorphicOn.divisor f (U - {c})) z
-- Lean.Data.Lsp.Extra
Lean.Lsp.PlainGoal.mk : String → Array String → Lean.Lsp.PlainGoal
-- Mathlib.Analysis.Complex.Trigonometric
Real.abs_tanh_lt_one : ∀ (x : ℝ), |Real.tanh x| < 1
-- Mathlib.CategoryTheory.Types.Basic
_private.Mathlib.CategoryTheory.Types.Basic.0.TypeCat.Hom.mk.inj : ∀ {X Y : Type u} {hom' hom'_1 : TypeCat.Fun X Y}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- A sequence `ℕ → M` is an `I`-adic Cauchy sequence if for every `m ≤ n`,
`f m ≡ f n` modulo `I ^ m • ⊤`.  -/
AdicCompletion.IsAdicCauchy : {R : Type u_1} →
  [inst : CommRing R] → Ideal R → (M : Type u_4) → [inst_1 : AddCommGroup M] → [Module R M] → (ℕ → M) → Prop
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- **Alias** of the forward direction of `MulAction.isBlock_iff_pairwiseDisjoint_range_smul`. -/
MulAction.IsBlock.pairwiseDisjoint_range_smul : ∀ {G : Type u_1} {X : Type u_2} [inst : SMul G X] {B : Set X},
  MulAction.IsBlock G B → (Set.range fun g => g • B).PairwiseDisjoint id
-- Mathlib.FieldTheory.Normal.Defs
AlgHom.restrictNormal'.eq_1 : ∀ {F : Type u_1} [inst : Field F] {K₁ : Type u_3} {K₂ : Type u_4} [inst_1 : Field K₁] [inst_2 : Field K₂]
  [inst_3 : Algebra F K₁] [inst_4 : Algebra F K₂] (ϕ : K₁ →ₐ[F] K₂) (E : Type u_6) [inst_5 : Field E]
  [inst_6 : Algebra F E] [inst_7 : Algebra E K₁] [inst_8 : Algebra E K₂] [inst_9 : IsScalarTower F E K₁]
  [inst_10 : IsScalarTower F E K₂] [inst_11 : Normal F E],
  ϕ.restrictNormal' E = AlgEquiv.ofBijective (ϕ.restrictNormal E) ⋯
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_insertMany!_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α] [inst_2 : Std.LawfulEqOrd α],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k : α} [inst_3 : Inhabited (β k)],
      (List.map Sigma.fst l).contains k = false → (↑(t.insertMany! l)).get! k = t.get! k
-- Mathlib.Data.Sym.Basic
Sym.coe_mk : ∀ {α : Type u_1} {n : ℕ} (s : Multiset α) (h : s.card = n), ↑(Sym.mk s h) = s
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.inter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β},
  m₁.WF → m₂.WF → (m₁ ∩ m₂).WF
-- Mathlib.GroupTheory.Submonoid.Inverses
Submonoid.instCommGroupSubtypeMemSubmonoid.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M],
  Submonoid.instCommGroupSubtypeMemSubmonoid = { toGroup := inferInstance, mul_comm := ⋯ }
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.toNonUnitalCommSemiring : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalCommSemiring A] →
        [inst_2 : Module R A] → (S : NonUnitalSubalgebra R A) → NonUnitalCommSemiring ↥S
-- Init.Data.Slice.Array.Lemmas
_private.Init.Data.Slice.Array.Lemmas.0.Std.IterStep.successor.match_1.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (motive : Std.IterStep α β → Sort u_3)
  (h_1 : (it : α) → (out : β) → motive (Std.IterStep.yield it out)) (h_2 : (it : α) → motive (Std.IterStep.skip it))
  (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it out => h_1 it out
    | Std.IterStep.skip it => h_2 it
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.Order.Filter.Basic
Filter.frequently_principal : ∀ {α : Type u} {a : Set α} {p : α → Prop}, (∃ᶠ (x : α) in Filter.principal a, p x) ↔ ∃ x ∈ a, p x
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
/-- The identity lax transformation.  -/
CategoryTheory.Oplax.LaxTrans.id : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] → (F : CategoryTheory.OplaxFunctor B C) → CategoryTheory.Oplax.LaxTrans F F
-- Lean.Util.PPExt
Lean.FormatWithInfos.mk.inj : ∀ {fmt : Std.Format} {infos : Lean.PrettyPrinter.InfoPerPos} {fmt_1 : Std.Format}
  {infos_1 : Lean.PrettyPrinter.InfoPerPos},
  { fmt := fmt, infos := infos } = { fmt := fmt_1, infos := infos_1 } → fmt = fmt_1 ∧ infos = infos_1
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
OpenPartialHomeomorph.trans_refl : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), e.trans (OpenPartialHomeomorph.refl Y) = e
-- Mathlib.LinearAlgebra.Dimension.Constructions
/-- If `m` and `n` are `Fintype`, the `finrank` of `m × n` matrices over a module `M` is
`(Fintype.card m) * (Fintype.card n) * finrank R M`.  -/
Module.finrank_matrix : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Free R M] (m : Type u_2) (n : Type u_3) [inst_5 : Fintype m] [inst_6 : Fintype n],
  Module.finrank R (Matrix m n M) = Fintype.card m * Fintype.card n * Module.finrank R M
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
SSet.Nonsingular.mk : ∀ {X : SSet}, (∀ {n : ℕ} (x : ↑(X.nonDegenerate n)), CategoryTheory.Mono (SSet.yonedaEquiv.symm ↑x)) → X.Nonsingular
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
PresheafOfModules.instHasColimitModuleCatCarrierObjOppositeRingCatCompEvaluationRestrictScalarsHomMap : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R))
  [∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
      CategoryTheory.Limits.PreservesColimit (F.comp (PresheafOfModules.evaluation R Y))
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))]
  [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))] {X Y : Cᵒᵖ} (f : X ⟶ Y),
  CategoryTheory.Limits.HasColimit
    (F.comp ((PresheafOfModules.evaluation R Y).comp (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))))
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_zero : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  ArchimedeanClass.mk 0 = ⊤
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.Iteration.mapObj.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J]
  [inst_4 : CategoryTheory.Limits.HasIterationOfShape J C] [inst_5 : WellFoundedLT J] {j₁ j₂ : J}
  (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) {k₁ k₂ : J} (h₁₂ : k₁ ≤ k₂) (h₁ : k₁ ≤ j₁) (h₂ : k₂ ≤ j₂)
  (hj : j₁ ≤ j₂), iter₁.mapObj iter₂ h₁₂ h₁ h₂ hj = iter₁.mapObj iter₂ h₁₂ h₁ h₂ hj
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.hom_inv_apply : ∀ (R : Type u) [inst : CommRing R] {A B : AlgCat R} (e : A ≅ B) (x : ↑B),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) x) = x
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.coe_inter : ∀ (x y : ZFSet.{u}), ↑(x ∩ y) = ↑x ∩ ↑y
-- Mathlib.Order.OrderDual
OrderDual.instMaxOfMin.eq_1 : ∀ (α : Type u_2) [h : Min α], OrderDual.instMaxOfMin α = { max := fun a b => a ⊓ b }
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.star_eq_two_re_sub : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [inst : CommRing R],
  star a = ↑(2 * a.re + c₂ * a.imI) - a
-- Mathlib.CategoryTheory.Bicategory.Basic
/-- The category structure on the collection of 1-morphisms  -/
CategoryTheory.Bicategory.homCategory : {B : Type u} → [self : CategoryTheory.Bicategory B] → (a b : B) → CategoryTheory.Category.{w, v} (a ⟶ b)
-- Mathlib.Analysis.Normed.Group.Constructions
Prod.normedAddGroup.eq_1 : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddGroup E] [inst_1 : NormedAddGroup F],
  Prod.normedAddGroup =
    { toNorm := Prod.seminormedAddGroup.toNorm, toAddGroup := Prod.seminormedAddGroup.toAddGroup,
      toPseudoMetricSpace := Prod.seminormedAddGroup.toPseudoMetricSpace, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.b₆_of_isShortNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsShortNF], W.b₆ = 4 * W.a₆
-- Mathlib.Data.DFinsupp.Lex
Pi.lex_eq_dfinsupp_lex : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop}
  (a b : Π₀ (i : ι), α i), Pi.Lex r (fun {i} => s i) ⇑a ⇑b = DFinsupp.Lex r s a b
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.whiskerLeft_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y : CategoryTheory.Mon C} (f : X ⟶ Y) (Z : CategoryTheory.Mon C),
  (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z).hom =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom Z.X
-- Mathlib.Analysis.Normed.Group.Constructions
/-- The seminorm of an element in a product space is `≤ r` if
and only if the norm of each component is.  -/
pi_norm_le_iff_of_nonneg : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddGroup (G i)] {x : (i : ι) → G i}
  {r : ℝ}, 0 ≤ r → (‖x‖ ≤ r ↔ ∀ (i : ι), ‖x i‖ ≤ r)
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
differentiable_riemannZeta₁ : Differentiable ℂ riemannZeta₁
-- Init.Omega.Coeffs
/-- Identity, turning `List Int` into `Coeffs`.  -/
Lean.Omega.Coeffs.ofList : List ℤ → Lean.Omega.Coeffs
-- Mathlib.RepresentationTheory.Coinvariants
Rep.coinvariantsShortComplex_X₁ : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{w, u, v} k G) (S : Subgroup G)
  [inst_2 : S.Normal], (A.coinvariantsShortComplex S).X₁ = A.toCoinvariantsKer S
-- Lean.LocalContext
/-- Return `true` if `lctx` contains a local declaration satisfying `p`.  -/
Lean.LocalContext.any : Lean.LocalContext → (Lean.LocalDecl → Bool) → Bool
-- Mathlib.Data.QPF.Univariate.Basic
/-- inductive type defined as initial algebra of a Quotient of Polynomial Functor  -/
QPF.Fix : (F : Type u → Type u) → [q : QPF F] → Type u
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.WF.brecOn : ∀ {α : Type u} [inst : Ord α] {motive : {β : α → Type v} → (a : Std.DTreeMap.Internal.Impl α β) → a.WF → Prop}
  {β : α → Type v} {a : Std.DTreeMap.Internal.Impl α β} (t : a.WF),
  (∀ {β : α → Type v} (a : Std.DTreeMap.Internal.Impl α β) (t : a.WF),
      Std.DTreeMap.Internal.Impl.WF.below t → motive a t) →
    motive a t
-- Mathlib.Topology.Clopen
IsClopen.union : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsClopen s → IsClopen t → IsClopen (s ∪ t)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
/-- The Yoneda embedding `Mon C ⥤ Cᵒᵖ ⥤ MonCat.{w}` for a locally `w`-small category `C`.  -/
CategoryTheory.shrinkYonedaMon : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.LocallySmall.{w, v, u} C] →
      [inst_2 : CategoryTheory.CartesianMonoidalCategory C] →
        CategoryTheory.Functor (CategoryTheory.Mon C) (CategoryTheory.Functor Cᵒᵖ MonCat)
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.emphLike.tok : Char → ℕ → String
-- Mathlib.Algebra.Star.SelfAdjoint
skewAdjoint.instIsStarNormalValMemAddSubgroup : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : StarRing R] (x : ↥(skewAdjoint R)), IsStarNormal ↑x
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instAddCommMonoid : {R : Type u_1} → {a b : R} → [AddCommMonoid R] → AddCommMonoid (QuadraticAlgebra R a b)
-- Mathlib.Order.Filter.Curry
Filter.prod_mem_curry : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {m : Filter β} {s : Set α} {t : Set β},
  s ∈ l → t ∈ m → s ×ˢ t ∈ l.curry m
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
/-- **Alias** of the reverse direction of `MeasureTheory.Measure.ae_le_iff_absolutelyContinuous`. -/
MeasureTheory.Measure.AbsolutelyContinuous.ae_le : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  μ.AbsolutelyContinuous ν → MeasureTheory.ae μ ≤ MeasureTheory.ae ν
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.leadingCoeff_scaleRoots : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) (r : R), (p.scaleRoots r).leadingCoeff = p.leadingCoeff
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.ext : ∀ {X Y : MonCat} {f g : X ⟶ Y},
  (∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) → f = g
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.surjective : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B), Function.Surjective ⇑e
-- Mathlib.MeasureTheory.VectorMeasure.WithDensity
/-- Having the same density implies the underlying functions are equal almost everywhere.  -/
MeasureTheory.Integrable.ae_eq_of_withDensityᵥ_eq : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f g : α → E},
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable g μ → μ.withDensityᵥ f = μ.withDensityᵥ g → f =ᵐ[μ] g
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.mk : {R : Type r} →
  [inst : CommRing R] →
    {W' : WeierstrassCurve.Projective R} →
      {point : WeierstrassCurve.Projective.PointClass R} → W'.NonsingularLift point → W'.Point
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.mk : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      {ι : Type u_4} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R N] →
                    [inst_6 : TopologicalSpace N] →
                      (toContinuousMultilinearMap : ContinuousMultilinearMap R (fun x => M) N) →
                        (∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → toContinuousMultilinearMap.toFun v = 0) →
                          M [⋀^ι]→L[R] N
-- Lean.Meta.Tactic.Grind.AC.Seq
Lean.Grind.AC.Seq.contains : Lean.Grind.AC.Seq → Lean.Grind.AC.Var → Bool
-- Lean.Expr
/-- Replace occurrences of the free variable `fvarId` in `e` with `v`  -/
Lean.Expr.replaceFVarId : Lean.Expr → Lean.FVarId → Lean.Expr → Lean.Expr
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S : J.Cover X} {I₁ I₂ : S.Arrow} {Z : C} {g₁ : Z ⟶ I₁.Y} {g₂ : Z ⟶ I₂.Y}
  {w :
    autoParam (CategoryTheory.CategoryStruct.comp g₁ I₁.f = CategoryTheory.CategoryStruct.comp g₂ I₂.f)
      CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.w._autoParam}
  {Z_1 : C} {g₁_1 : Z_1 ⟶ I₁.Y} {g₂_1 : Z_1 ⟶ I₂.Y}
  {w_1 :
    autoParam (CategoryTheory.CategoryStruct.comp g₁_1 I₁.f = CategoryTheory.CategoryStruct.comp g₂_1 I₂.f)
      CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.w._autoParam},
  { Z := Z, g₁ := g₁, g₂ := g₂, w := w } = { Z := Z_1, g₁ := g₁_1, g₂ := g₂_1, w := w_1 } →
    Z = Z_1 ∧ g₁ ≍ g₁_1 ∧ g₂ ≍ g₂_1
-- Mathlib.Algebra.Star.Basic
MulOpposite.instStarAddMonoid : {R : Type u} → [inst : AddMonoid R] → [StarAddMonoid R] → StarAddMonoid Rᵐᵒᵖ
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.sproj.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {n offset : ℕ} {var : Lean.FVarId}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_11} {n_1 offset_1 : ℕ}
  {var_1 : Lean.FVarId} {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_11},
  Lean.Compiler.LCNF.LetValue.sproj n offset var h = Lean.Compiler.LCNF.LetValue.sproj n_1 offset_1 var_1 h_1 →
    n = n_1 ∧ offset = offset_1 ∧ var = var_1
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.of_injective : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : MulOneClass M] [Nontrivial R],
  Function.Injective ⇑(MonoidAlgebra.of R M)
-- Lean.Elab.DocString
/-- An expander for roles in docstrings.
 -/
Lean.Doc.DocRoleExpander : Type
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The norm of the sum of two non-zero vectors equals the sum of their norms
if and only the angle between the two vectors is 0.  -/
InnerProductGeometry.norm_add_eq_add_norm_iff_angle_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  x ≠ 0 → y ≠ 0 → (‖x + y‖ = ‖x‖ + ‖y‖ ↔ InnerProductGeometry.angle x y = 0)
-- Mathlib.Probability.Kernel.Composition.Lemmas
MeasureTheory.Measure.prod_comp_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν] {κ : ProbabilityTheory.Kernel α γ} [ProbabilityTheory.IsSFiniteKernel κ],
  (μ.bind ⇑κ).prod ν = (μ.prod ν).bind ⇑(κ.parallelComp ProbabilityTheory.Kernel.id)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_inter_eq_false_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₁.contains k = false → (m₁.inter m₂).contains k = false
-- Mathlib.LinearAlgebra.Complex.Module
Complex.distribSMul : {R : Type u_1} → [DistribSMul R ℝ] → DistribSMul R ℂ
-- Mathlib.Topology.Maps.Basic
Topology.IsInducing.image_eq_isClosed_inter_range : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace X],
  Topology.IsInducing f → ∀ {s : Set X}, IsClosed s → ∃ c, IsClosed c ∧ f '' s = c ∩ Set.range f
-- Mathlib.Analysis.Normed.Ring.Basic
/-- Deduce `NormOneClass` from `NormMulClass` under a suitable nontriviality hypothesis. Not
an instance, in order to avoid loops with `NormOneClass.nontrivial`.  -/
NormMulClass.toNormOneClass : ∀ {α : Type u_2} [inst : NormedAddCommGroup α] [inst_1 : MulOneClass α] [NormMulClass α] [Nontrivial α], NormOneClass α
-- Mathlib.Order.Disjoint
isCompl_iff' : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α] {a b : α},
  IsCompl a b ↔ Codisjoint a b ∧ Disjoint a b
-- Mathlib.Computability.Ackermann
ack_succ_right_le_ack_succ_left : ∀ (m n : ℕ), ack m (n + 1) ≤ ack (m + 1) n
-- Init.Data.Range.Polymorphic.UInt
USize.instIsAlwaysFinite : Std.Rxc.IsAlwaysFinite USize
-- Mathlib.RepresentationTheory.Rep.Basic
/-- The category of representations of monoid `G` and their morphisms.  -/
Rep : (k : Type u) → (G : Type v) → [Semiring k] → [Monoid G] → Type (max (max u v) (w + 1))
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
ZetaAsymptotics.term_of_lt : ∀ {n : ℕ},
  0 < n →
    ∀ {s : ℝ},
      1 < s →
        ZetaAsymptotics.term n s =
          1 / (s - 1) * (1 / ↑n ^ (s - 1) - 1 / (↑n + 1) ^ (s - 1)) - ↑n / s * (1 / ↑n ^ s - 1 / (↑n + 1) ^ s)
-- Init.Data.String.Bootstrap
String.Internal.intercalate : String → List String → String
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.rightAdjointUniq_hom_app_counit_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G G' : CategoryTheory.Functor D C}
  (adj1 : F ⊣ G) (adj2 : F ⊣ G') (x : D) {Z : D} (h : x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map ((adj1.rightAdjointUniq adj2).hom.app x))
      (CategoryTheory.CategoryStruct.comp (adj2.counit.app x) h) =
    CategoryTheory.CategoryStruct.comp (adj1.counit.app x) h
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.truncatedInf_union_left : ∀ {α : Type u_1} [inst : SemilatticeInf α] {s t : Finset α} {a : α} [inst_1 : DecidableLE α] [inst_2 : BoundedOrder α]
  [inst_3 : DecidableEq α], a ∈ upperClosure ↑s → a ∉ upperClosure ↑t → (s ∪ t).truncatedInf a = s.truncatedInf a
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α}
  {v : β}, (t.insertIfNew k v).contains a = (cmp k a == Ordering.eq || t.contains a)
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- Compositional version of `Finset.measurable_sum` for use by `fun_prop`.  -/
Finset.measurable_sum_apply : ∀ {M : Type u_2} {ι : Type u_3} {α : Type u_4} {β : Type u_5} [inst : AddCommMonoid M] [inst_1 : MeasurableSpace M]
  [MeasurableAdd₂ M] {m : MeasurableSpace α} {mβ : MeasurableSpace β} {f : ι → α → β → M} {g : α → β} {s : Finset ι},
  (∀ i ∈ s, Measurable ↿(f i)) → Measurable g → Measurable fun a => (∑ i ∈ s, f i a) (g a)
-- Mathlib.Algebra.Group.Submonoid.Units
Submonoid.units_iInf₂ : ∀ {M : Type u_1} [inst : Monoid M] {ι : Sort u_2} {κ : ι → Sort u_3} (f : (i : ι) → κ i → Submonoid M),
  (⨅ i, ⨅ j, f i j).units = ⨅ i, ⨅ j, (f i j).units