mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
ContinuousLinearMap.hasFDerivAt_uncurry_of_multilinear : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {ι : Type u_2}
  {G : ι → Type u_3} [inst_5 : (i : ι) → NormedAddCommGroup (G i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (G i)]
  [inst_7 : Fintype ι] [inst_8 : DecidableEq ι] (f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F) (v : E × ((i : ι) → G i)),
  HasFDerivAt (fun p => (f p.1) p.2)
    (f.flipMultilinear v.2 ∘SL ContinuousLinearMap.fst 𝕜 E ((i : ι) → G i) +
      ∑ i,
        (f v.1).toContinuousLinearMap v.2 i ∘SL
          ContinuousLinearMap.proj i ∘SL ContinuousLinearMap.snd 𝕜 E ((i : ι) → G i))
    v
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_diff_le_size_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF), m₂.WF → (m₁.diff m₂ ⋯).size ≤ m₁.size
-- Mathlib.Order.RelClasses
Order.Preimage.instIsStrictWeakOrder : ∀ {α : Type u} {β : Type v} {r : α → α → Prop} [IsStrictWeakOrder α r] {f : β → α}, IsStrictWeakOrder β (f ⁻¹'o r)
-- Mathlib.Dynamics.Ergodic.Ergodic
PreErgodic.of_iterate : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α} {μ : MeasureTheory.Measure α} (n : ℕ),
  PreErgodic f^[n] μ → PreErgodic f μ
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- The `vectorSpan` is the span of the pairwise subtractions with a given point on the left,
excluding the subtraction of that point from itself.  -/
vectorSpan_eq_span_vsub_set_left_ne : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P} {p : P},
  p ∈ s → vectorSpan k s = Submodule.span k ((fun x => p -ᵥ x) '' (s \ {p}))
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.yang_baxter_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y Z : C) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Z (CategoryTheory.MonoidalCategoryStruct.tensorObj Y X) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Y).hom Z)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Z).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (β_ X Z).hom)
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y Z X).inv
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ Y Z).hom X)
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Z Y X).hom
                  h)))))) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (β_ Y Z).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Z Y).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Z).hom Y)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z (β_ X Y).hom) h))))
-- Mathlib.Analysis.Calculus.ContDiff.Operations
contDiff_update : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {ι : Type u_3} [inst_1 : Fintype ι] {F' : ι → Type u_5}
  [inst_2 : (i : ι) → NormedAddCommGroup (F' i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (F' i)] [inst_4 : DecidableEq ι]
  (k : WithTop ℕ∞) (x : (i : ι) → F' i) (i : ι), ContDiff 𝕜 k (Function.update x i)
-- Mathlib.Analysis.Convex.Between
Sbtw.trans_right_left : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {w x y z : P},
  Sbtw R w x z → Sbtw R x y z → Sbtw R w x y
-- Mathlib.AlgebraicGeometry.Morphisms.FlatRank
AlgebraicGeometry.Scheme.Hom.finrank_pullback_fst : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.Flat f] [AlgebraicGeometry.IsFinite f]
  (y : ↥Y),
  AlgebraicGeometry.Scheme.Hom.finrank (CategoryTheory.Limits.pullback.fst g f) y =
    AlgebraicGeometry.Scheme.Hom.finrank f (g y)
-- Mathlib.CategoryTheory.Localization.SmallHom
/-- The action of a localizer morphism `Φ` on `SmallHom`. In this version, we allow
the replacement of objects `Φ.functor.obj` by isomorphic objects.  -/
CategoryTheory.LocalizerMorphism.smallHomMap' : {C₁ : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
    {W₁ : CategoryTheory.MorphismProperty C₁} →
      {C₂ : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) →
              {X Y : C₁} →
                [inst_2 : CategoryTheory.Localization.HasSmallLocalizedHom W₁ X Y] →
                  {X' Y' : C₂} →
                    [CategoryTheory.Localization.HasSmallLocalizedHom W₂ X' X'] →
                      [inst_4 : CategoryTheory.Localization.HasSmallLocalizedHom W₂ X' Y'] →
                        [CategoryTheory.Localization.HasSmallLocalizedHom W₂ Y' Y'] →
                          (Φ.functor.obj X ≅ X') →
                            (Φ.functor.obj Y ≅ Y') →
                              CategoryTheory.Localization.SmallHom W₁ X Y →
                                CategoryTheory.Localization.SmallHom W₂ X' Y'
-- Mathlib.Computability.Language
Language.reverse_injective : ∀ {α : Type u_1}, Function.Injective Language.reverse
-- Lean.Data.Name
Lean.Name.isStr : Lean.Name → Bool
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.subRight.eq_1 : ∀ {G : Type w} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G] (x : G),
  Homeomorph.subRight x = { toEquiv := Equiv.subRight x, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Lean.Server.Completion.CompletionItemCompression
/-- Fast path for `(toJson l).compress` that skips the intermediate `Json` object.
Used in place of `(toJson l).compress` in the language server.
 -/
Lean.Lsp.ResolvableCompletionList.compressFast : Lean.Lsp.ResolvableCompletionList → String
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey!_insertManyIfNewUnit_empty_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] [inst : Inhabited α] {l : List α} {k k' : α},
  compare k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬compare a b = Ordering.eq) l →
      k ∈ l →
        (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit Std.DTreeMap.Internal.Impl.empty l ⋯)).getKey! k' = k
-- Mathlib.Tactic.GCongr.Core
/-- In `∀ xs, a xs' ~ b xs'`, for each `x` in `xs`, the position it appears in `xs'`.
This information is used to infer suitable names when introducing these variables.  -/
Mathlib.Tactic.GCongr.GCongrHyp.hypsPos : Mathlib.Tactic.GCongr.GCongrHyp → List (Option ℕ)
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.grothendieckTypeToCatInverse_obj_fiber_as : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : G.Elements),
  ((CategoryTheory.Grothendieck.grothendieckTypeToCatInverse G).obj X).fiber.as = X.snd
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.alternatingWord.eq_2 : ∀ {B : Type u_1} (i i' : B) (m_2 : ℕ),
  CoxeterSystem.alternatingWord i i' m_2.succ = (CoxeterSystem.alternatingWord i' i m_2).concat i'
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∉ m₂ → (m₁ ∩ m₂).getKey? k = none
-- Aesop.Stats.Extension
Aesop.statsExtension : Aesop.StatsExtension
-- Mathlib.Order.RelIso.Set
Subrel.instIsPreorderSubtype : ∀ {α : Type u_1} (r : α → α → Prop) [IsPreorder α r] (p : α → Prop), IsPreorder (Subtype p) (Subrel r p)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
CategoryTheory.NatTrans.Equifibered.of_discrete : ∀ {C : Type u_3} {ι : Type u_5} [inst : CategoryTheory.Category.{v_2, u_3} C]
  {F G : CategoryTheory.Functor (CategoryTheory.Discrete ι) C} (α : F ⟶ G), CategoryTheory.NatTrans.Equifibered α
-- Lean.Server.References
/-- Finds the first definition or usage in `self` where the `RefInfo.Location.range`
contains the given `pos`. The `includeStop` parameter can be used to toggle between closed-interval
and half-open-interval behavior for the range. Closed-interval behavior matches the expectation of
VSCode when selecting an identifier at a cursor position (see #767).
 -/
Lean.Lsp.RefInfo.findReferenceLocation? : Lean.Lsp.RefInfo → Lean.Lsp.Position → optParam Bool false → Option Lean.Lsp.RefInfo.Location
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.logMap_eq_logEmbedding : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (u : (NumberField.RingOfIntegers K)ˣ),
  NumberField.mixedEmbedding.logMap
      ((NumberField.mixedEmbedding K) ((algebraMap (NumberField.RingOfIntegers K) K) ↑u)) =
    (NumberField.Units.logEmbedding K) (Additive.ofMul u)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.Monomial.toFun_tendsto_top_of_firstNonzeroIsPos : ∀ {coef : ℝ} {exps : Tactic.ComputeAsymptotics.UnitMonomial} {basis : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.WellFormedBasis basis →
    List.length exps = List.length basis →
      0 < coef →
        exps.FirstNonzeroIsPos →
          have t := { coef := coef, unit := exps };
          Filter.Tendsto (t.toFun basis) Filter.atTop Filter.atTop
-- Mathlib.MeasureTheory.Function.LpSeminorm.SMul
MeasureTheory.MemLp.const_mul : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {𝕜 : Type u_3}
  [inst : NormedRing 𝕜] {f : α → 𝕜}, MeasureTheory.MemLp f p μ → ∀ (c : 𝕜), MeasureTheory.MemLp (fun x => c * f x) p μ
-- Mathlib.RingTheory.Filtration
/-- If the components of a filtration are finitely generated, then the filtration is stable iff
its associated submodule of is finitely generated.  -/
Ideal.Filtration.submodule_fg_iff_stable : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  (F : I.Filtration M), (∀ (i : ℕ), (F.N i).FG) → (F.submodule.FG ↔ F.Stable)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.combine.sizeOf_spec : ∀ (c₁ c₂ : Lean.Meta.Grind.Arith.Linear.IneqCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.combine c₁ c₂) = 1 + sizeOf c₁ + sizeOf c₂
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.WhiskerLeft.of.inj : ∀ {η η_1 : Mathlib.Tactic.BicategoryLike.HorizontalComp},
  Mathlib.Tactic.BicategoryLike.WhiskerLeft.of η = Mathlib.Tactic.BicategoryLike.WhiskerLeft.of η_1 → η = η_1
-- Mathlib.Order.Filter.Interval
Filter.tendsto_Ico_pure_bot : ∀ {α : Type u_1} [inst : PartialOrder α] {a : α}, Filter.TendstoIxxClass Set.Ico (pure a) ⊥
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
CategoryTheory.MorphismProperty.isStableUnderColimitsOfShape_monomorphisms : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (J : Type u') [inst_1 : CategoryTheory.Category.{v', u'} J]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.Limits.colim.PreservesMonomorphisms],
  (CategoryTheory.MorphismProperty.monomorphisms C).IsStableUnderColimitsOfShape J
-- Mathlib.Order.SymmDiff
Pi.bihimp_apply : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : (i : ι) → GeneralizedHeytingAlgebra (π i)] (a b : (i : ι) → π i) (i : ι),
  bihimp a b i = bihimp (a i) (b i)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.instInhabited.eq_1 : ∀ (M : Type u_1) [inst : TopologicalSpace M] [inst_1 : Mul M],
  ContinuousMulEquiv.instInhabited M = { default := ContinuousMulEquiv.refl M }
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- Any change of coordinates with empty source belongs to `contDiffGroupoid`.  -/
ContDiffGroupoid.mem_of_source_eq_empty : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
  (f : OpenPartialHomeomorph H H), f.source = ∅ → f ∈ contDiffGroupoid n I
-- Mathlib.Topology.PartialHomeomorph.Basic
/-- If a `PartialEquiv` is a homeomorphism when restricted to source and target, then it is a
`PartialHomeomorph`.  -/
PartialHomeomorph.ofIsHomeomorphToEquiv : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → (f : PartialEquiv X Y) → IsHomeomorph ⇑f.toEquiv → PartialHomeomorph X Y
-- Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
isClosedMap_nndist : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [ProperSpace α] (x : α), IsClosedMap (nndist x)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.DistribMulActionHom.single_toFun : ∀ {R : Type u_3} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : DistribMulAction R M]
  {α : Type u_6} (a : α) (a_1 : M),
  (SkewMonoidAlgebra.DistribMulActionHom.single a) a_1 = (↑(SkewMonoidAlgebra.singleAddHom a)).toFun a_1
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.map_inf : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (H K : Subgroup G) (f : G →* N),
  Function.Injective ⇑f → Subgroup.map f (H ⊓ K) = Subgroup.map f H ⊓ Subgroup.map f K
-- Mathlib.Algebra.Group.Equiv.TypeTags
MulEquiv.Monoid.End_apply : ∀ {M : Type u_4} [inst : Monoid M] (f : M →* M),
  MulEquiv.Monoid.End f = { toFun := fun a => Additive.ofMul (f (Additive.toMul a)), map_zero' := ⋯, map_add' := ⋯ }
-- Lean.Meta.Tactic.Grind.MatchCond
_private.Lean.Meta.Tactic.Grind.MatchCond.0.Lean.Meta.Grind.collectMatchCondLhssAndAbstract.go.match_1.splitter : (motive : Option Lean.Expr → Sort u_1) →
  (α? : Option Lean.Expr) →
    ((α : Lean.Expr) → motive (some α)) →
      ((x : Option Lean.Expr) → (∀ (α : Lean.Expr), x = some α → False) → motive x) → motive α?
-- Init.Data.String.PosRaw
String.instHAddRawChar : HAdd String.Pos.Raw Char String.Pos.Raw
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arccos_le_pi_div_four : ∀ {x : ℝ}, Real.arccos x ≤ Real.pi / 4 ↔ √2 / 2 ≤ x
-- Mathlib.Analysis.Normed.Module.Basic
norm_natCast : ∀ {α : Type u_6} [inst : SeminormedRing α] [NormOneClass α] [NormSMulClass ℤ α] (a : ℕ), ‖↑a‖ = ↑a
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegralFun_restrictScalars : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F}
  {γ : Path a b} {𝕝 : Type u_4} [inst_5 : RCLike 𝕝] [inst_6 : NormedSpace 𝕝 F] [inst_7 : NormedSpace 𝕝 E]
  [inst_8 : LinearMap.CompatibleSMul E F 𝕝 𝕜],
  curveIntegralFun (fun t => ContinuousLinearMap.restrictScalars 𝕝 (ω t)) γ = curveIntegralFun ω γ
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
OrdinalApprox.lfpApprox_mono_right : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α}, Monotone (OrdinalApprox.lfpApprox f x)
-- Lean.Meta.Tactic.Grind.Arith.Simproc
/-- Generic instance normalizer  -/
Lean.Meta.Grind.Arith.normInst : ℕ → Lean.Expr → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.DStep
-- Mathlib.Order.DirectedInverseSystem
/-- Glue partial families of bijections at a limit ordinal,
obtaining a partial family over a right-open interval.  -/
InverseSystem.pEquivOnGlue : {ι : Type u_6} →
  {F : ι → Type u_7} →
    {X : ι → Type u_8} →
      {i : ι} →
        [inst : LinearOrder ι] →
          {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} →
            [inst_1 : SuccOrder ι] →
              {equivSucc : ⦃i : ι⦄ → ¬IsMax i → F (Order.succ i) ≃ F i × X i} →
                [WellFoundedLT ι] →
                  Order.IsSuccPrelimit i →
                    ((j : ↑(Set.Iio i)) → InverseSystem.PEquivOn f equivSucc (Set.Iic ↑j)) →
                      InverseSystem.PEquivOn f equivSucc (Set.Iio i)
-- Std.Http.Data.Request
/-- Optional dynamic metadata attached to the request.
 -/
Std.Http.Request.extensions : {t : Type} → Std.Http.Request t → Std.Http.Extensions
-- Mathlib.RingTheory.AdicCompletion.Algebra
/-- When `S` is `I`-adic complete, the canonical map from `S` to
its `I`-adic completion is an `S`-algebra isomorphism.
 -/
AdicCompletion.ofAlgEquiv : {S : Type u_5} → [inst : CommRing S] → (I : Ideal S) → [IsAdicComplete I S] → S ≃ₐ[S] AdicCompletion I S
-- Init.Data.Int.DivMod.Lemmas
Int.neg_mul_bmod_left : ∀ (a : ℤ) (b : ℕ), (-(a * ↑b)).bmod b = 0
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.unitOfArray : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {a : Array α}, (Std.DTreeMap.Raw.Const.unitOfArray a cmp).WF
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.Y_eq_of_Y_ne : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} {x₁ x₂ y₁ y₂ : F},
  W.Equation x₁ y₁ → W.Equation x₂ y₂ → x₁ = x₂ → y₁ ≠ W.negY x₂ y₂ → y₁ = y₂
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.isCharNeTwoNF_of_isCharThreeNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeNF], W.IsCharNeTwoNF
-- Mathlib.RingTheory.ReesAlgebra
/-- The Rees algebra of an ideal `I`, defined as the subalgebra of `R[X]` whose `i`-th coefficient
falls in `I ^ i`.  -/
reesAlgebra : {R : Type u} → [inst : CommRing R] → Ideal R → Subalgebra R (Polynomial R)
-- Lean.Compiler.CSimpAttr
Lean.Compiler.CSimp.instInhabitedState.default : Lean.Compiler.CSimp.State
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
isUnit_le_nonZeroDivisors : ∀ (M₀ : Type u_2) [inst : MonoidWithZero M₀], IsUnit.submonoid M₀ ≤ nonZeroDivisors M₀
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.PushoutCocone.inr_colimit_cocone : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : Z ⟶ X) (g : Z ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.span f g)],
  CategoryTheory.Limits.PushoutCocone.inr (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Limits.span f g)) =
    CategoryTheory.Limits.pushout.inr f g
-- Init.Data.List.Find
List.findIdx?_isNone : ∀ {α : Type u_1} {xs : List α} {p : α → Bool}, (List.findIdx? p xs).isNone = xs.all fun x => decide ¬p x = true
-- Init.System.IO
/-- Converts a task state to a string.
 -/
IO.TaskState.toString : IO.TaskState → String
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintParams.range : Lean.Lsp.InlayHintParams → Lean.Lsp.Range
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Martingale.integrable : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0} [CompleteSpace E],
  MeasureTheory.Martingale f ℱ μ → ∀ (i : ι), MeasureTheory.Integrable (f i) μ
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.enorm_setIntegral_le_lintegral_enorm_transpose : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  {s : Set X} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G},
  ‖∫ᵛ (x : X) in s, f x ∂[B; μ]‖ₑ ≤ ∫⁻ (x : X) in s, ‖f x‖ₑ ∂(μ.transpose B).variation
-- Init.Control.Lawful.Instances
OptionT.fail.eq_1 : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type u}, OptionT.fail = OptionT.mk (pure none)
-- Mathlib.CategoryTheory.SingleObj
/-- One and `flip (*)` become `id` and `comp` for morphisms of the single object category.  -/
CategoryTheory.SingleObj.categoryStruct : (M : Type u) → [One M] → [Mul M] → CategoryTheory.CategoryStruct.{u, 0} (CategoryTheory.SingleObj M)
-- Mathlib.Logic.Equiv.Fin.Rotate
finCycle_symm_apply : ∀ {n : ℕ} (k i : Fin n), (Equiv.symm (finCycle k)) i = i - k
-- Mathlib.GroupTheory.GroupAction.Primitive
MulAction.isTrivialBlock_of_card_le_two : ∀ {X : Type u_2} [Finite X], Nat.card X ≤ 2 → ∀ (B : Set X), MulAction.IsTrivialBlock B
-- Mathlib.Data.Matrix.Mul
Matrix.vecMul_apply_eq_sum : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype m] (v : m → α)
  (M : Matrix m n α) (i : n), Matrix.vecMul v M i = ∑ j, v j * M j i
-- Mathlib.Data.List.Forall2
List.forall₂_iff_zip : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l₁ : List α} {l₂ : List β},
  List.Forall₂ R l₁ l₂ ↔ l₁.length = l₂.length ∧ ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b
-- Mathlib.Topology.Algebra.Algebra
/-- If two continuous algebra maps are equal on a set `s`, then they are equal on the closure
of the `Algebra.adjoin` of this set.  -/
ContinuousAlgHom.eqOn_closure_adjoin : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [T2Space B] {s : Set A} {f g : A →A[R] B}, Set.EqOn (⇑f) (⇑g) s → Set.EqOn (⇑f) (⇑g) (closure ↑(Algebra.adjoin R s))
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.preimage_closedEBall : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β) (x : β)
  (r : ENNReal), ⇑h ⁻¹' Metric.closedEBall x r = Metric.closedEBall (h.symm x) r
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.Q.liftOn₂ : {α : Type u} →
  [inst : Lean.Grind.NatModule α] →
    {β : Sort u_1} →
      Lean.Grind.IntModule.OfNatModule.Q α →
        Lean.Grind.IntModule.OfNatModule.Q α →
          (f : α × α → α × α → β) →
            (∀ {a₁ b₁ a₂ b₂ : α × α},
                Lean.Grind.IntModule.OfNatModule.r α a₁ a₂ →
                  Lean.Grind.IntModule.OfNatModule.r α b₁ b₂ → f a₁ b₁ = f a₂ b₂) →
              β
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.coe_vadd : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {K : Type u_5} [inst_1 : VAdd K β] (c : K)
  (f : MeasureTheory.SimpleFunc α β), ⇑(c +ᵥ f) = c +ᵥ ⇑f
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction
CochainComplex.HomComplex.Cochain.InductionUp.limitSequence_eqUpTo : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {d : ℤ} {X : ℕ → Set (CochainComplex.HomComplex.Cochain K L d)}
  (φ : (n : ℕ) → ↑(X n) → ↑(X (n + 1))) {p₀ : ℤ} (hφ : ∀ (n : ℕ) (x : ↑(X n)), (↑(φ n x)).EqUpTo (↑x) (p₀ + ↑n))
  (x₀ : ↑(X 0)) (n : ℕ),
  (CochainComplex.HomComplex.Cochain.InductionUp.limitSequence φ hφ x₀).EqUpTo
    (↑(CochainComplex.HomComplex.Cochain.InductionUp.sequence φ x₀ n)) (p₀ + ↑n)
-- Lean.Data.Position
Lean.Position.line : Lean.Position → ℕ
-- Lean.Meta.Tactic.Assert
Lean.Meta.Hypothesis.value : Lean.Meta.Hypothesis → Lean.Expr
-- Mathlib.Control.Monad.Writer
instMonadWriterReaderT : {M : Type u → Type v} → {ω ρ : Type u} → [MonadWriter ω M] → MonadWriter ω (ReaderT ρ M)
-- Mathlib.Data.EReal.Operations
EReal.right_distrib_of_nonneg_of_ne_top : ∀ {x : EReal}, 0 ≤ x → x ≠ ⊤ → ∀ (y z : EReal), (y + z) * x = y * x + z * x