mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Meromorphic.Basic
/-- If two functions agree on a punctured neighborhood, then one is meromorphic iff the other is so.
 -/
MeromorphicAt.meromorphicAt_congr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f g : 𝕜 → E}, f =ᶠ[nhdsWithin x {x}ᶜ] g → (MeromorphicAt f x ↔ MeromorphicAt g x)
-- Init.Data.BitVec.Lemmas
BitVec.toNat_toInt_of_sle : ∀ {w : ℕ} {x : BitVec w}, (0#w).sle x = true → x.toInt.toNat = x.toNat
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.quotientKerEquivOfSurjective.eq_1 : ∀ {G : Type u} [inst : AddGroup G] {H : Type v} [inst_1 : AddGroup H] (φ : G →+ H) (hφ : Function.Surjective ⇑φ),
  QuotientAddGroup.quotientKerEquivOfSurjective φ hφ =
    QuotientAddGroup.quotientKerEquivOfRightInverse φ (Exists.choose ⋯) ⋯
-- Mathlib.Data.Multiset.DershowitzManna
_private.Mathlib.Data.Multiset.DershowitzManna.0.Multiset.acc_oneStep_cons_of_acc_lt : ∀ {α : Type u_1} [inst : Preorder α] {a : α},
  Acc LT.lt a → ∀ {M : Multiset α}, Acc Multiset.OneStep✝ M → Acc Multiset.OneStep✝ (a ::ₘ M)
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- Given `f : L →ₐ[K] L'`, `S.comap f` is the intermediate field between `K` and `L`
such that `f x ∈ S ↔ x ∈ S.comap f`.  -/
IntermediateField.comap : {K : Type u_1} →
  {L : Type u_2} →
    {L' : Type u_3} →
      [inst : Field K] →
        [inst_1 : Field L] →
          [inst_2 : Field L'] →
            [inst_3 : Algebra K L] →
              [inst_4 : Algebra K L'] → (L →ₐ[K] L') → IntermediateField K L' → IntermediateField K L
-- Mathlib.Logic.Equiv.Basic
Equiv.swap_self : ∀ {α : Sort u_1} [inst : DecidableEq α] (a : α), Equiv.swap a a = Equiv.refl α
-- Init.Data.SInt.Lemmas
ISize.lt_iff_toInt_lt : ∀ {x y : ISize}, x < y ↔ x.toInt < y.toInt
-- Std.Tactic.BVDecide.LRAT.Internal.CompactLRATChecker
_private.Std.Tactic.BVDecide.LRAT.Internal.CompactLRATChecker.0.Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go.match_1.eq_1 : ∀ {n : ℕ} (motive : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n × Bool → Sort u_1)
  (fst : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (checkSuccess : Bool)
  (h_1 :
    (fst : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) → (checkSuccess : Bool) → motive (fst, checkSuccess)),
  (match (fst, checkSuccess) with
    | (fst, checkSuccess) => h_1 fst checkSuccess) =
    h_1 fst checkSuccess
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.reverseOp.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M},
  CliffordAlgebra.reverseOp = (CliffordAlgebra.lift Q) ⟨↑(MulOpposite.opLinearEquiv R) ∘ₗ CliffordAlgebra.ι Q, ⋯⟩
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.toBilin'Aux.eq_1 : ∀ {R₁ : Type u_1} [inst : CommSemiring R₁] {n : Type u_5} [inst_1 : Fintype n] (M : Matrix n n R₁),
  M.toBilin'Aux = Matrix.toLinearMap₂'Aux (RingHom.id R₁) (RingHom.id R₁) M
-- Mathlib.Logic.Equiv.Defs
/-- Any type is equivalent to itself.  -/
Equiv.refl : (α : Sort u_1) → α ≃ α
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RooSliceData.mk.sizeOf_spec : ∀ {α : Type u} [inst : Ord α] [inst_1 : SizeOf α] (treeMap : Std.DTreeMap.Internal.Impl α fun x => Unit)
  (range : Std.Roo α), sizeOf { treeMap := treeMap, range := range } = 1 + sizeOf treeMap + sizeOf range
-- Mathlib.Analysis.Calculus.Implicit
/-- Right function  -/
ImplicitFunctionData.rightFun : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          [inst_3 : CompleteSpace E] →
            {F : Type u_3} →
              [inst_4 : NormedAddCommGroup F] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [inst_6 : CompleteSpace F] →
                    {G : Type u_4} →
                      [inst_7 : NormedAddCommGroup G] →
                        [inst_8 : NormedSpace 𝕜 G] → [inst_9 : CompleteSpace G] → ImplicitFunctionData 𝕜 E F G → E → G
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reflect_reflect : ∀ {R : Type u_1} [inst : Semiring R] {N : ℕ} {p : Polynomial R}, Polynomial.reflect N (Polynomial.reflect N p) = p
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.cylinder_empty : ∀ {ι : Type u_1} {α : ι → Type u_2} (s : Finset ι), MeasureTheory.cylinder s ∅ = ∅
-- Mathlib.Order.Heyting.Hom
instCoeTCCoheytingHomOfCoheytingHomClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : CoheytingAlgebra α] →
          [inst_2 : CoheytingAlgebra β] → [CoheytingHomClass F α β] → CoeTC F (CoheytingHom α β)
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.span_singleton_sup_orthogonal_eq_top : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {B : LinearMap.BilinForm K V} {x : V}, (B x) x ≠ 0 → K ∙ x ⊔ B.orthogonal (K ∙ x) = ⊤
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.any_eq_not_all_not : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {p : (a : α) → β a → Bool},
  m.any p = !m.all fun a b => !p a b
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- The functor `M ↦ R[M]`, from the category of magmas to the category of
non-unital, non-associative algebras over `R` is adjoint to the forgetful functor in the other
direction.  -/
AddMonoidAlgebra.liftMagma : (R : Type u_1) →
  {A : Type u_4} →
    {M : Type u_7} →
      [inst : Semiring R] →
        [inst_1 : Add M] →
          [inst_2 : NonUnitalNonAssocSemiring A] →
            [inst_3 : Module R A] →
              [IsScalarTower R A A] → [SMulCommClass R A A] → (Multiplicative M →ₙ* A) ≃ (AddMonoidAlgebra R M →ₙₐ[R] A)
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- `A ⟶[C] B` denotes the internal hom from `A` to `B`  -/
CategoryTheory.ihom.«term_⟶[_]_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.Derivation.Basic
Derivation.map_zero : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M] (D : Derivation R A M),
  D 0 = 0
-- Mathlib.Topology.NhdsWithin
closure_pi_set : ∀ {ι : Type u_5} {α : ι → Type u_6} [inst : (i : ι) → TopologicalSpace (α i)] (I : Set ι) (s : (i : ι) → Set (α i)),
  closure (I.pi s) = I.pi fun i => closure (s i)
-- Std.Data.DTreeMap.Internal.Operations
/-- Slower version of `containsThenInsertIfNew` which can be used in the absence of balance
information but still assumes the preconditions of `containsThenInsertIfNew`, otherwise might panic.
 -/
Std.DTreeMap.Internal.Impl.containsThenInsertIfNew! : {α : Type u} →
  {β : α → Type v} → [Ord α] → (k : α) → β k → Std.DTreeMap.Internal.Impl α β → Bool × Std.DTreeMap.Internal.Impl α β
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.ιOrZero_mapBifunctorAssociatorX_hom_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Category.{v_6, u_4} C₂₃]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_8 : CategoryTheory.Limits.HasZeroMorphisms C₃] [inst_9 : CategoryTheory.Preadditive C₁₂]
  [inst_10 : CategoryTheory.Preadditive C₂₃] [inst_11 : CategoryTheory.Preadditive C₄]
  {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)}
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)}
  {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [inst_12 : F₁₂.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_14 : G.Additive]
  [inst_15 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] [inst_16 : G₂₃.PreservesZeroMorphisms]
  [inst_17 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_18 : F.PreservesZeroMorphisms]
  [inst_19 : ∀ (X₁ : C₁), (F.obj X₁).Additive]
  (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G ≅ CategoryTheory.bifunctorComp₂₃ F G₂₃) {ι₁ : Type u_7}
  {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_20 : DecidableEq ι₄]
  {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁)
  (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃)
  (c₄ : ComplexShape ι₄) [inst_21 : TotalComplexShape c₁ c₂ c₁₂] [inst_22 : TotalComplexShape c₁₂ c₃ c₄]
  [inst_23 : TotalComplexShape c₂ c₃ c₂₃] [inst_24 : TotalComplexShape c₁ c₂₃ c₄], ⋯
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.compare_maxKeyD_modify_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {f : β → β} {fallback : α},
      compare ((Std.DTreeMap.Internal.Impl.Const.modify k f t).maxKeyD fallback) (t.maxKeyD fallback) = Ordering.eq
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.instHasLeftCalculusOfFractionsOppositeOpOfHasRightCalculusOfFractions : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [h : W.HasRightCalculusOfFractions], W.op.HasLeftCalculusOfFractions
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
CategoryTheory.ConcreteCategory.hom_injective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C},
  Function.Injective CategoryTheory.ConcreteCategory.hom
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.wr : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} {c c' : C}
  (self : CategoryTheory.Span Wₗ Wᵣ c c'), Wᵣ self.r
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw.buckets_empty : ∀ {α : Type u} {β : α → Type v} {i : ℕ} {h : i < ∅.buckets.size}, ∅.buckets[i] = Std.DHashMap.Internal.AssocList.nil
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.of_natDegree_le_one_of_invertible : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f.natDegree ≤ 1 → ∀ (h : Invertible f.leadingCoeff), f.Splits
-- Lean.Meta.Tactic.Grind.Types
/-- Generated while instantiating a theorem using E-matching.  -/
Lean.Meta.Grind.SplitSource.ematch : Lean.Meta.Grind.Origin → Lean.Meta.Grind.SplitSource
-- Mathlib.Data.EReal.Operations
EReal.mul_ne_top : ∀ (a b : EReal), a * b ≠ ⊤ ↔ (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤)
-- Mathlib.Order.WithBot
WithBot.coe_injective : ∀ {α : Type u_1}, Function.Injective WithBot.some
-- Lean.Expr
Lean.Nat.mkInstHPow : Lean.Expr
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceRpcKeepAliveParams : Lean.Lsp.FileSource Lean.Lsp.RpcKeepAliveParams
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- `f` coequalizes the two maps  -/
CategoryTheory.RegularEpi.w : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (self : CategoryTheory.RegularEpi f),
  CategoryTheory.CategoryStruct.comp self.left f = CategoryTheory.CategoryStruct.comp self.right f
-- Mathlib.RingTheory.LaurentSeries
/-- `LaurentSeries R` is the type of formal Laurent series with coefficients in `R`, denoted `R⸨X⸩`.

It is implemented as a `HahnSeries` with value group `ℤ`.
 -/
LaurentSeries : (R : Type u) → [Zero R] → Type (max 0 u)
-- Lean.Meta.Basic
/-- `withExistingLocalDecls decls k`, adds the given local declarations to the local context,
and then executes `k`. This method assumes declarations in `decls` have valid `FVarId`s.
After executing `k`, the local context is restored.

Remark: this method is used, for example, to implement the `match`-compiler.
Each `match`-alternative comes with a local declarations (corresponding to pattern variables),
and we use `withExistingLocalDecls` to add them to the local context before we process
them.
 -/
Lean.Meta.withExistingLocalDecls : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → List Lean.LocalDecl → n α → n α
-- Mathlib.Order.Defs.PartialOrder
lt_of_lt_of_le' : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, b < a → c ≤ b → c < a
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
/-- A set is **3AP-free** if it does not contain any non-trivial arithmetic
progression of length three.

This is also sometimes called a **non-averaging set** or **Salem-Spencer set**.  -/
ThreeAPFree : {α : Type u_2} → [AddMonoid α] → Set α → Prop
-- Mathlib.Data.Multiset.FinsetOps
Multiset.mem_ndunion : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α} {a : α}, a ∈ s.ndunion t ↔ a ∈ s ∨ a ∈ t
-- Init.Data.List.Lemmas
List.getElem?_set_self : ∀ {α : Type u_1} {l : List α} {i : ℕ} {a : α}, i < l.length → (l.set i a)[i]? = some a
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Kernels
/-- The kernel inclusion is itself a kernel in the functor category.  -/
CategoryTheory.Limits.kerIsKernel : (C : Type u_1) →
  [inst : CategoryTheory.Category.{u, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasKernels C] →
        CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.ker.ι C) ⋯)
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.IsOrdinal.mem_trichotomous : ∀ {x y : ZFSet.{u}}, x.IsOrdinal → y.IsOrdinal → x ∈ y ∨ x = y ∨ y ∈ x
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.filter_equiv_self_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {f : α → β → Bool},
  (Std.TreeMap.filter f t).Equiv t ↔ ∀ (k : α) (h : k ∈ t), f (t.getKey k h) t[k] = true
-- Mathlib.Control.Bitraversable.Instances
_private.Mathlib.Control.Bitraversable.Instances.0.Sum.bitraverse.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : α ⊕ β → Sort u_3) (x : α) (h_1 : (x : α) → motive (Sum.inl x))
  (h_2 : (x : β) → motive (Sum.inr x)),
  (match Sum.inl x with
    | Sum.inl x => h_1 x
    | Sum.inr x => h_2 x) =
    h_1 x
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.Origin.decl.sizeOf_spec : ∀ (name : Lean.Name), sizeOf (Mathlib.Meta.FunProp.Origin.decl name) = 1 + sizeOf name
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.instSliceableImplRioSlice : {α : Type u} →
  {β : Type v} →
    [inst : Ord α] →
      Std.Rio.Sliceable (Std.DTreeMap.Internal.Impl α fun x => β) α (Std.DTreeMap.Internal.Const.RioSlice α β)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.sqrt_map_prod : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A]
  [IsSemitopologicalRing A] [T2Space A] {B : Type u_2} [inst_12 : PartialOrder B] [inst_13 : NonUnitalRing B]
  [inst_14 : TopologicalSpace B] [inst_15 : StarRing B] [inst_16 : Module ℝ B] [inst_17 : SMulCommClass ℝ B B]
  [inst_18 : IsScalarTower ℝ B B] [inst_19 : StarOrderedRing B]
  [inst_20 : NonUnitalContinuousFunctionalCalculus ℝ B IsSelfAdjoint]
  [inst_21 : NonUnitalContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint] [IsSemitopologicalRing B] [T2Space B]
  [inst_24 : NonnegSpectrumClass ℝ B] [inst_25 : NonnegSpectrumClass ℝ (A × B)] {a : A} {b : B},
  autoParam (0 ≤ a) CFC.sqrt_map_prod._auto_1 →
    autoParam (0 ≤ b) CFC.sqrt_map_prod._auto_3 → CFC.sqrt (a, b) = (CFC.sqrt a, CFC.sqrt b)
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
Real.differentiable_fourierChar_neg_bilinear_right : ∀ {V : Type u_1} {W : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : NormedAddCommGroup W]
  [inst_3 : NormedSpace ℝ W] (L : V →L[ℝ] W →L[ℝ] ℝ) (v : V), Differentiable ℝ fun w => ↑(Real.fourierChar (-(L v) w))
-- Init.Grind.Order
Lean.Grind.Order.lt_eq_false : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] {a : α}, (a < a) = False
-- Mathlib.Topology.ClusterPt
clusterPt_iff_not_disjoint : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {F : Filter X}, ClusterPt x F ↔ ¬Disjoint (nhds x) F
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.negAddY_of_X_eq' : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} {P Q : Fin 3 → R},
  W'.Equation P →
    W'.Equation Q → P 0 * Q 2 = Q 0 * P 2 → W'.negAddY P Q * (P 2 * Q 2) ^ 2 = (P 1 * Q 2 - Q 1 * P 2) ^ 3 * (P 2 * Q 2)
-- Mathlib.Analysis.Normed.Ring.Basic
/-- Multiplication is commutative in a commutative multiplicative magma.  -/
NormedCommRing.mul_comm : ∀ {α : Type u_5} [self : NormedCommRing α] (a b : α), a * b = b * a
-- Mathlib.Topology.Algebra.Order.Floor
/-- A special case of `ContinuousOn.comp_fract`.  -/
ContinuousOn.comp_fract'' : ∀ {α : Type u_1} {β : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α]
  [inst_3 : TopologicalSpace α] [IsStrictOrderedRing α] [OrderTopology α] [inst_6 : TopologicalSpace β] {f : α → β},
  ContinuousOn f (Set.Icc 0 1) → f 0 = f 1 → Continuous (f ∘ Int.fract)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey?_ofList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (Std.ExtDHashMap.Const.ofList l).getKey? k = none
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
/-- Lift a monoid homomorphism `f : GL n R →* M` that vanishes on all scalar matrices
to a homomorphism from `PGL(n, R)`.  -/
Matrix.ProjGenLinGroup.lift : {n : Type u_1} →
  {R : Type u_2} →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] →
        [inst_2 : CommRing R] →
          {M : Type u_3} →
            [inst_3 : Monoid M] →
              (f : GL n R →* M) → f.comp (Matrix.GeneralLinearGroup.scalar n) = 1 → Matrix.ProjGenLinGroup n R →* M
-- Mathlib.RingTheory.Derivation.ToSquareZero
liftOfDerivationToSquareZero_mk_apply' : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (I : Ideal B) [inst_5 : Algebra A B] (d : Derivation R A ↥I) (x : A),
  (Ideal.Quotient.mk I) ↑(d x) + (algebraMap A (B ⧸ I)) x = (algebraMap A (B ⧸ I)) x
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- A nonzero continuous linear functional is open.  -/
ContinuousLinearMap.isOpenMap_of_ne_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : TopologicalSpace R] [inst_1 : DivisionRing R] [ContinuousSub R]
  [inst_3 : AddCommGroup M] [inst_4 : TopologicalSpace M] [ContinuousAdd M] [inst_6 : Module R M] [ContinuousSMul R M]
  (f : StrongDual R M), f ≠ 0 → IsOpenMap ⇑f
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.mk_mapInvariants_apply : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {π : ContRepresentation R G V} {π' : ContRepresentation R G W} (f : ContIntertwiningMap π π') (v : V)
  (hv : v ∈ π.invariants), ↑(f.mapInvariants ⟨v, hv⟩) = f v
-- Init.GrindInstances.Ring.Int
Lean.Grind.instCommRingInt : Lean.Grind.CommRing ℤ
-- Init.Data.Array.Subarray
/-- Runs a monadic action on each element of a subarray.

The elements are processed starting at the lowest index and moving up.
 -/
Subarray.forM : {α : Type u} → {m : Type v → Type w} → [Monad m] → (α → m PUnit.{v + 1}) → Subarray α → m PUnit.{v + 1}
-- Mathlib.RingTheory.Localization.Finiteness
Submodule.localized_fg : ∀ {R : Type u} [inst : CommSemiring R] {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Submodule R M}
  (S : Submonoid R), N.FG → (Submodule.localized S N).FG
-- Mathlib.Geometry.Euclidean.Projection
EuclideanGeometry.orthogonalProjection_orthogonalProjection_of_le : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {s₁ s₂ : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s₁] [inst_6 : Nonempty ↥s₂] [inst_7 : s₁.direction.HasOrthogonalProjection]
  [inst_8 : s₂.direction.HasOrthogonalProjection],
  s₁ ≤ s₂ →
    ∀ (p : P),
      (EuclideanGeometry.orthogonalProjection s₁) ↑((EuclideanGeometry.orthogonalProjection s₂) p) =
        (EuclideanGeometry.orthogonalProjection s₁) p
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
/-- The action of `stabilizer M a` is one-less preprimitive.  -/
MulAction.isMultiplyPreprimitive_ofStabilizer : ∀ (M : Type u_1) (α : Type u_2) [inst : Group M] [inst_1 : MulAction M α] [MulAction.IsPretransitive M α] {n : ℕ}
  {a : α} [MulAction.IsMultiplyPreprimitive M α n.succ],
  MulAction.IsMultiplyPreprimitive (↥(MulAction.stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.lt_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  μ < ν ↔ μ ≤ ν ∧ ∃ s, MeasurableSet s ∧ μ s < ν s
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- If `G.IsBipartiteWith s t` and `w ∈ t`, then if `v` is adjacent to `w` in `G` then `v ∈ s`.  -/
SimpleGraph.IsBipartiteWith.mem_of_mem_adj' : ∀ {V : Type u_1} {v w : V} {G : SimpleGraph V} {s t : Set V}, G.IsBipartiteWith s t → w ∈ t → G.Adj v w → v ∈ s
-- Mathlib.Data.Finmap
Finmap.lookup_insert : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} (s : Finmap β),
  Finmap.lookup a (Finmap.insert a b s) = some b
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.takeUntilEscFn : (Char → Bool) → Lean.Parser.ParserFn
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.of_smul_def : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → DecidableEq (M i)] (i : ι) (w : Monoid.CoprodI.Word M) (m : M i),
  Monoid.CoprodI.of m • w =
    Monoid.CoprodI.Word.rcons
      (have __src := (Monoid.CoprodI.Word.equivPair i) w;
      { head := m * ((Monoid.CoprodI.Word.equivPair i) w).head, tail := __src.tail, fstIdx_ne := ⋯ })
-- Mathlib.Topology.MetricSpace.Completion
/-- The extension of an isometry to the completion of the domain.  -/
Isometry.extensionHom : {α : Type u} →
  {β : Type v} →
    [inst : PseudoMetricSpace α] →
      [inst_1 : Ring α] →
        [inst_2 : IsTopologicalRing α] →
          [inst_3 : IsUniformAddGroup α] →
            [inst_4 : Ring β] →
              [inst_5 : PseudoMetricSpace β] →
                [IsUniformAddGroup β] →
                  [IsTopologicalRing β] →
                    [CompleteSpace β] → [T0Space β] → {f : α →+* β} → Isometry ⇑f → UniformSpace.Completion α →+* β
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.funCongrLeft_apply : ∀ (R : Type u_1) (M : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {m : Type u_9}
  {n : Type u_10} (e : m ≃ n) (x : n → M), (LinearEquiv.funCongrLeft R M e) x = (LinearMap.funLeft R M ⇑e) x
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_of_isEmpty : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, m.isEmpty = true → m.getKey? a = none
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.primeSpectrumProdOfSum.eq_2 : ∀ (R : Type u) (S : Type v) [inst : CommSemiring R] [inst_1 : CommSemiring S] (J : Ideal S) (isPrime : J.IsPrime),
  PrimeSpectrum.primeSpectrumProdOfSum R S (Sum.inr { asIdeal := J, isPrime := isPrime }) =
    { asIdeal := ⊤.prod J, isPrime := ⋯ }