ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>a₁ : P.mp.A<VAR>f₁ : P.mp.B a₁ ⟹ α<VAR>a' : P.A<VAR>f' : (P.B a').drop ⟹ α<VAR>f₁' : (P.B a').last → P.M α<VAR>e₁ : MvPFunctor.M.dest P ⟨a₁, f₁⟩ = ⟨a', TypeVec.splitFun f' f₁'⟩<GOAL>∃ g₁', ∃ (e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩), f' = MvPFunctor.M.pathDestLeft P e₁' f₁ ∧ f₁' = fun x => ⟨g₁' x, MvPFunctor.M.pathDestRight P e₁' f₁ x⟩
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>R : P.M α → P.M α → Prop<VAR>h : ∀ (x y : P.M α), R x y → ∃ a f f₁ f₂, MvPFunctor.M.dest P x = ⟨a, TypeVec.splitFun f f₁⟩ ∧ MvPFunctor.M.dest P y = ⟨a, TypeVec.splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)<VAR>x y : P.M α<VAR>r : R x y<GOAL>x = y
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>R : P.M α → P.M α → Prop<VAR>h₀ : Equivalence R<VAR>h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> MvPFunctor.M.dest P x = (TypeVec.id ::: Quot.mk R) <$$> MvPFunctor.M.dest P y<VAR>x y : P.M α<VAR>r : R x y<GOAL>x = y
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>R : P.M α → P.M α → Prop<VAR>h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> MvPFunctor.M.dest P x = (TypeVec.id ::: Quot.mk R) <$$> MvPFunctor.M.dest P y<VAR>x y : P.M α<VAR>r : R x y<GOAL>x = y
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α β : TypeVec.{u} n<VAR>g : α ⟹ β<VAR>x : P.M α<GOAL>MvPFunctor.M.dest P (g <$$> x) = (g ::: fun x => g <$$> x) <$$> MvPFunctor.M.dest P x
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α β : TypeVec.{u} n<VAR>g : α ::: P.M α ⟹ β ::: P.M β<VAR>x : P.M α<VAR>h : ∀ (x : P.M α), TypeVec.lastFun g x = TypeVec.dropFun g <$$> x<GOAL>g <$$> MvPFunctor.M.dest P x = MvPFunctor.M.dest P (TypeVec.dropFun g <$$> x)
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>E : B → Type u_3<VAR>x x' : B<VAR>h : x = x'<VAR>b : E x<GOAL>Bundle.TotalSpace.mk' F x' (cast ⋯ b) = { proj := x, snd := b }
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>E : B → Type u_3<VAR>b : B<VAR>y y' : E b<GOAL>Bundle.TotalSpace.mk' F b y = Bundle.TotalSpace.mk' F b y' ↔ y = y'
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>E : B → Type u_3<VAR>b : B<GOAL>Function.Injective (Bundle.TotalSpace.mk b)
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>E : B → Type u_3<VAR>z : Bundle.TotalSpace F E<GOAL>{ proj := z.proj, snd := z.snd } = z
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>E : B → Type u_3<VAR>p : Bundle.TotalSpace F E → Prop<GOAL>(∃ x, p x) ↔ ∃ b y, p { proj := b, snd := y }
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>E : B → Type u_3<VAR>b : B<GOAL>Set.range (Bundle.TotalSpace.mk b) = Bundle.TotalSpace.proj ⁻¹' {b}
<VAR>B : Type u_4<VAR>F : Type u_5<VAR>x : B × F<GOAL>((Bundle.TotalSpace.toProd B F).symm x).snd = x.2
<VAR>B : Type u_4<VAR>F : Type u_5<VAR>x : Bundle.TotalSpace F fun x => F<GOAL>(Bundle.TotalSpace.toProd B F) x = (x.proj, x.snd)
<VAR>B : Type u_4<VAR>F : Type u_5<VAR>x : B × F<GOAL>((Bundle.TotalSpace.toProd B F).symm x).proj = x.1
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>E : B → Type u_3<VAR>B' : Type u_4<VAR>f : B' → B<GOAL>∀ (a : Bundle.TotalSpace F (f *ᵖ E)), (Bundle.Pullback.lift f a).snd = a.snd
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>E : B → Type u_3<VAR>B' : Type u_4<VAR>f : B' → B<GOAL>∀ (a : Bundle.TotalSpace F (f *ᵖ E)), (Bundle.Pullback.lift f a).proj = f a.proj
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>E : B → Type u_3<VAR>B' : Type u_4<VAR>f : B' → B<VAR>x : B'<VAR>y : E (f x)<GOAL>Bundle.Pullback.lift f (Bundle.TotalSpace.mk' F x y) = { proj := f x, snd := y }
<VAR>F : Sort u_1<VAR>α : outParam (Sort u_2)<VAR>β : outParam (Sort u_3)<VAR>FunLike F α β<VAR>self : EmbeddingLike F α β<VAR>f : F<GOAL>Function.Injective ⇑f
<VAR>F : Sort u_1<VAR>α : Sort u_2<VAR>β : Sort u_3<VAR>FunLike F α β<VAR>i : EmbeddingLike F α β<VAR>f : F<GOAL>Function.Injective ⇑f
<VAR>F : Sort u_1<VAR>α : Sort u_2<VAR>β : Sort u_3<VAR>FunLike F α β<VAR>i : EmbeddingLike F α β<VAR>f : F<VAR>x y : α<GOAL>f x = f y ↔ x = y
<VAR>α : Sort u_2<VAR>β : Sort u_3<VAR>γ : Sort u_4<VAR>F : Sort u_5<VAR>FunLike F β γ<VAR>EmbeddingLike F β γ<VAR>f : α → β<VAR>e : F<GOAL>Function.Injective (⇑e ∘ f) ↔ Function.Injective f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>a₁ a₂ : α<GOAL>Sum.inlₗ (a₁ ⊔ a₂) = Sum.inlₗ a₁ ⊔ Sum.inlₗ a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>b₁ b₂ : β<GOAL>Sum.inrₗ (b₁ ⊔ b₂) = Sum.inrₗ b₁ ⊔ Sum.inrₗ b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>a₁ a₂ : α<GOAL>Sum.inlₗ (a₁ ⊓ a₂) = Sum.inlₗ a₁ ⊓ Sum.inlₗ a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>b₁ b₂ : β<GOAL>Sum.inrₗ (b₁ ⊓ b₂) = Sum.inrₗ b₁ ⊓ Sum.inrₗ b₂
<VAR>F : Sort u_1<VAR>α : Sort u_3<VAR>β : α → Sort u_5<VAR>DFunLike F α β<VAR>Finite α<VAR>∀ (i : α), Finite (β i)<GOAL>Finite F
<VAR>G : Sort u_2<VAR>α : Sort u_3<VAR>γ : Sort u_4<VAR>FunLike G α γ<VAR>Finite α<VAR>Finite γ<GOAL>Finite G
<VAR>E : Sort u_1<VAR>α : outParam (Sort u_2)<VAR>β : outParam (Sort u_3)<VAR>self : EquivLike E α β<VAR>e : E<GOAL>Function.LeftInverse (EquivLike.inv e) (EquivLike.coe e)
<VAR>E : Sort u_1<VAR>α : outParam (Sort u_2)<VAR>β : outParam (Sort u_3)<VAR>self : EquivLike E α β<VAR>e g : E<GOAL>EquivLike.coe e = EquivLike.coe g → EquivLike.inv e = EquivLike.inv g → e = g
<VAR>E : Sort u_1<VAR>α : outParam (Sort u_2)<VAR>β : outParam (Sort u_3)<VAR>self : EquivLike E α β<VAR>e : E<GOAL>Function.RightInverse (EquivLike.inv e) (EquivLike.coe e)
<VAR>E : Sort u_1<VAR>α : Sort u_3<VAR>β : Sort u_4<VAR>iE : EquivLike E α β<GOAL>Function.Injective EquivLike.inv
<VAR>E : Sort u_1<VAR>α : Sort u_3<VAR>β : Sort u_4<VAR>iE : EquivLike E α β<VAR>e : E<GOAL>Function.Injective ⇑e
<VAR>E : Sort u_1<VAR>α : Sort u_3<VAR>β : Sort u_4<VAR>iE : EquivLike E α β<VAR>e : E<GOAL>Function.Surjective ⇑e
<VAR>E : Sort u_1<VAR>α : Sort u_3<VAR>β : Sort u_4<VAR>iE : EquivLike E α β<VAR>e : E<GOAL>Function.Bijective ⇑e
<VAR>E : Sort u_1<VAR>α : Sort u_3<VAR>β : Sort u_4<VAR>iE : EquivLike E α β<VAR>f : E<VAR>x y : α<GOAL>f x = f y ↔ x = y
<VAR>E : Sort u_1<VAR>α : Sort u_3<VAR>β : Sort u_4<VAR>γ : Sort u_5<VAR>iE : EquivLike E α β<VAR>e : E<VAR>f : β → γ<GOAL>Function.Injective (f ∘ ⇑e) ↔ Function.Injective f
<VAR>E : Sort u_1<VAR>α : Sort u_3<VAR>β : Sort u_4<VAR>γ : Sort u_5<VAR>iE : EquivLike E α β<VAR>e : E<VAR>f : β → γ<GOAL>Function.Surjective (f ∘ ⇑e) ↔ Function.Surjective f
<VAR>E : Sort u_1<VAR>α : Sort u_3<VAR>β : Sort u_4<VAR>γ : Sort u_5<VAR>iE : EquivLike E α β<VAR>e : E<VAR>f : β → γ<GOAL>Function.Bijective (f ∘ ⇑e) ↔ Function.Bijective f
<VAR>E : Sort u_1<VAR>α : Sort u_3<VAR>β : Sort u_4<VAR>iE : EquivLike E α β<VAR>e : E<VAR>a : α<GOAL>EquivLike.inv e (e a) = a
<VAR>E : Sort u_1<VAR>α : Sort u_3<VAR>β : Sort u_4<VAR>iE : EquivLike E α β<VAR>e : E<VAR>b : β<GOAL>e (EquivLike.inv e b) = b
<VAR>F : Sort u_2<VAR>α : Sort u_3<VAR>β : Sort u_4<VAR>γ : Sort u_5<VAR>iF : EquivLike F β γ<VAR>f : α → β<VAR>e : F<GOAL>Function.Injective (⇑e ∘ f) ↔ Function.Injective f
<VAR>F : Sort u_2<VAR>α : Sort u_3<VAR>β : Sort u_4<VAR>γ : Sort u_5<VAR>iF : EquivLike F β γ<VAR>f : α → β<VAR>e : F<GOAL>Function.Surjective (⇑e ∘ f) ↔ Function.Surjective f
<VAR>F : Sort u_2<VAR>α : Sort u_3<VAR>β : Sort u_4<VAR>γ : Sort u_5<VAR>iF : EquivLike F β γ<VAR>f : α → β<VAR>e : F<GOAL>Function.Bijective (⇑e ∘ f) ↔ Function.Bijective f
<VAR>F : Sort u_2<VAR>β : Sort u_4<VAR>γ : Sort u_5<VAR>iF : EquivLike F β γ<VAR>Subsingleton β<GOAL>Subsingleton F
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>Polynomial.C W.Ψ₂Sq = W.ψ₂ ^ 2 - 4 * W.toAffine.polynomial
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.ψ₂ ^ 2 = Polynomial.C W.Ψ₂Sq + 4 * W.toAffine.polynomial
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>(WeierstrassCurve.Affine.CoordinateRing.mk W) W.ψ₂ ^ 2 = (WeierstrassCurve.Affine.CoordinateRing.mk W) (Polynomial.C W.Ψ₂Sq)
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.Ψ₂Sq = W.twoTorsionPolynomial.toPoly
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.preΨ' 0 = 0
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.preΨ' 1 = 1
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.preΨ' 2 = 1
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.preΨ' 3 = W.Ψ₃
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.preΨ' 4 = W.preΨ₄
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>m : ℕ<GOAL>W.preΨ' (2 * (m + 2) + 1) = (W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3 * if Even m then W.Ψ₂Sq ^ 2 else 1) - W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3 * if Even m then 1 else W.Ψ₂Sq ^ 2
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>m : ℕ<GOAL>W.preΨ' (2 * (m + 3)) = W.preΨ' (m + 2) ^ 2 * W.preΨ' (m + 3) * W.preΨ' (m + 5) - W.preΨ' (m + 1) * W.preΨ' (m + 3) * W.preΨ' (m + 4) ^ 2
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<GOAL>W.preΨ ↑n = W.preΨ' n
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.preΨ 0 = 0
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.preΨ 1 = 1
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.preΨ 2 = 1
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.preΨ 3 = W.Ψ₃
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.preΨ 4 = W.preΨ₄
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>m : ℕ<GOAL>W.preΨ (2 * (↑m + 2) + 1) = (W.preΨ (↑m + 4) * W.preΨ (↑m + 2) ^ 3 * if Even m then W.Ψ₂Sq ^ 2 else 1) - W.preΨ (↑m + 1) * W.preΨ (↑m + 3) ^ 3 * if Even m then 1 else W.Ψ₂Sq ^ 2
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>m : ℕ<GOAL>W.preΨ (2 * (↑m + 3)) = W.preΨ (↑m + 2) ^ 2 * W.preΨ (↑m + 3) * W.preΨ (↑m + 5) - W.preΨ (↑m + 1) * W.preΨ (↑m + 3) * W.preΨ (↑m + 4) ^ 2
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℤ<GOAL>W.preΨ (-n) = -W.preΨ n
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<GOAL>W.ΨSq ↑n = W.preΨ' n ^ 2 * if Even n then W.Ψ₂Sq else 1
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.ΨSq 0 = 0
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.ΨSq 1 = 1
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.ΨSq 2 = W.Ψ₂Sq
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.ΨSq 3 = W.Ψ₃ ^ 2
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.ΨSq 4 = W.preΨ₄ ^ 2 * W.Ψ₂Sq
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>m : ℕ<GOAL>W.ΨSq (2 * (↑m + 2) + 1) = ((W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3 * if Even m then W.Ψ₂Sq ^ 2 else 1) - W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3 * if Even m then 1 else W.Ψ₂Sq ^ 2) ^ 2
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>m : ℕ<GOAL>W.ΨSq (2 * (↑m + 3)) = (W.preΨ' (m + 2) ^ 2 * W.preΨ' (m + 3) * W.preΨ' (m + 5) - W.preΨ' (m + 1) * W.preΨ' (m + 3) * W.preΨ' (m + 4) ^ 2) ^ 2 * W.Ψ₂Sq
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℤ<GOAL>W.ΨSq (-n) = W.ΨSq n
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<GOAL>W.Ψ ↑n = Polynomial.C (W.preΨ' n) * if Even n then W.ψ₂ else 1
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.Ψ 0 = 0
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.Ψ 1 = 1
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.Ψ 2 = W.ψ₂
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.Ψ 3 = Polynomial.C W.Ψ₃
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.Ψ 4 = Polynomial.C W.preΨ₄ * W.ψ₂
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>m : ℕ<GOAL>W.Ψ (2 * (↑m + 2) + 1) = W.Ψ (↑m + 4) * W.Ψ (↑m + 2) ^ 3 - W.Ψ (↑m + 1) * W.Ψ (↑m + 3) ^ 3 + W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) * Polynomial.C (if Even m then W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3 else -W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3)
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>m : ℕ<GOAL>W.Ψ (2 * (↑m + 3)) * W.ψ₂ = W.Ψ (↑m + 2) ^ 2 * W.Ψ (↑m + 3) * W.Ψ (↑m + 5) - W.Ψ (↑m + 1) * W.Ψ (↑m + 3) * W.Ψ (↑m + 4) ^ 2
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℤ<GOAL>W.Ψ (-n) = -W.Ψ n
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℤ<GOAL>(WeierstrassCurve.Affine.CoordinateRing.mk W) (W.Ψ n) ^ 2 = (WeierstrassCurve.Affine.CoordinateRing.mk W) (Polynomial.C (W.ΨSq n))
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<GOAL>W.Φ (↑n + 1) = (Polynomial.X * W.preΨ' (n + 1) ^ 2 * if Even n then 1 else W.Ψ₂Sq) - W.preΨ' (n + 2) * W.preΨ' n * if Even n then W.Ψ₂Sq else 1
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.Φ 0 = 1
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.Φ 1 = Polynomial.X
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.Φ 2 = Polynomial.X ^ 4 - Polynomial.C W.b₄ * Polynomial.X ^ 2 - Polynomial.C (2 * W.b₆) * Polynomial.X - Polynomial.C W.b₈
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.Φ 3 = Polynomial.X * W.Ψ₃ ^ 2 - W.preΨ₄ * W.Ψ₂Sq
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.Φ 4 = Polynomial.X * W.preΨ₄ ^ 2 * W.Ψ₂Sq - W.Ψ₃ * (W.preΨ₄ * W.Ψ₂Sq ^ 2 - W.Ψ₃ ^ 3)
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℤ<GOAL>W.Φ (-n) = W.Φ n
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.ψ 0 = 0
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.ψ 1 = 1
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.ψ 2 = W.ψ₂
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.ψ 3 = Polynomial.C W.Ψ₃
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.ψ 4 = Polynomial.C W.preΨ₄ * W.ψ₂
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>m : ℕ<GOAL>W.ψ (2 * (↑m + 2) + 1) = W.ψ (↑m + 4) * W.ψ (↑m + 2) ^ 3 - W.ψ (↑m + 1) * W.ψ (↑m + 3) ^ 3
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>m : ℕ<GOAL>W.ψ (2 * (↑m + 3)) * W.ψ₂ = W.ψ (↑m + 2) ^ 2 * W.ψ (↑m + 3) * W.ψ (↑m + 5) - W.ψ (↑m + 1) * W.ψ (↑m + 3) * W.ψ (↑m + 4) ^ 2
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℤ<GOAL>W.ψ (-n) = -W.ψ n
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℤ<GOAL>(WeierstrassCurve.Affine.CoordinateRing.mk W) (W.ψ n) = (WeierstrassCurve.Affine.CoordinateRing.mk W) (W.Ψ n)
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.φ 0 = 1
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.φ 1 = Polynomial.C Polynomial.X
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.φ 2 = Polynomial.C Polynomial.X * W.ψ₂ ^ 2 - Polynomial.C W.Ψ₃
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.φ 3 = Polynomial.C Polynomial.X * Polynomial.C W.Ψ₃ ^ 2 - Polynomial.C W.preΨ₄ * W.ψ₂ ^ 2
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.φ 4 = Polynomial.C Polynomial.X * Polynomial.C W.preΨ₄ ^ 2 * W.ψ₂ ^ 2 - Polynomial.C W.preΨ₄ * W.ψ₂ ^ 4 * Polynomial.C W.Ψ₃ + Polynomial.C W.Ψ₃ ^ 4
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℤ<GOAL>W.φ (-n) = W.φ n
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℤ<GOAL>(WeierstrassCurve.Affine.CoordinateRing.mk W) (W.φ n) = (WeierstrassCurve.Affine.CoordinateRing.mk W) (Polynomial.C (W.Φ n))
<VAR>R : Type r<VAR>S : Type s<VAR>CommRing R<VAR>CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<GOAL>(W.map f).ψ₂ = Polynomial.map (Polynomial.mapRingHom f) W.ψ₂
<VAR>R : Type r<VAR>S : Type s<VAR>CommRing R<VAR>CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<GOAL>(W.map f).Ψ₂Sq = Polynomial.map f W.Ψ₂Sq
<VAR>R : Type r<VAR>S : Type s<VAR>CommRing R<VAR>CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<GOAL>(W.map f).Ψ₃ = Polynomial.map f W.Ψ₃
<VAR>R : Type r<VAR>S : Type s<VAR>CommRing R<VAR>CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<GOAL>(W.map f).preΨ₄ = Polynomial.map f W.preΨ₄
<VAR>R : Type r<VAR>S : Type s<VAR>CommRing R<VAR>CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<VAR>n : ℕ<GOAL>(W.map f).preΨ' n = Polynomial.map f (W.preΨ' n)
<VAR>R : Type r<VAR>S : Type s<VAR>CommRing R<VAR>CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<VAR>n : ℤ<GOAL>(W.map f).preΨ n = Polynomial.map f (W.preΨ n)
<VAR>R : Type r<VAR>S : Type s<VAR>CommRing R<VAR>CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<VAR>n : ℤ<GOAL>(W.map f).ΨSq n = Polynomial.map f (W.ΨSq n)
<VAR>R : Type r<VAR>S : Type s<VAR>CommRing R<VAR>CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<VAR>n : ℤ<GOAL>(W.map f).Ψ n = Polynomial.map (Polynomial.mapRingHom f) (W.Ψ n)
<VAR>R : Type r<VAR>S : Type s<VAR>CommRing R<VAR>CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<VAR>n : ℤ<GOAL>(W.map f).Φ n = Polynomial.map f (W.Φ n)
<VAR>R : Type r<VAR>S : Type s<VAR>CommRing R<VAR>CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<VAR>n : ℤ<GOAL>(W.map f).ψ n = Polynomial.map (Polynomial.mapRingHom f) (W.ψ n)
<VAR>R : Type r<VAR>S : Type s<VAR>CommRing R<VAR>CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<VAR>n : ℤ<GOAL>(W.map f).φ n = Polynomial.map (Polynomial.mapRingHom f) (W.φ n)
<VAR>R : Type r<VAR>S : Type s<VAR>CommRing R<VAR>CommRing S<VAR>W : WeierstrassCurve R<VAR>Algebra R S<VAR>A : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>B : Type v<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>f : A →ₐ[S] B<GOAL>(W.baseChange B).ψ₂ = Polynomial.map (Polynomial.mapRingHom ↑f) (W.baseChange A).ψ₂
<VAR>R : Type r<VAR>S : Type s<VAR>CommRing R<VAR>CommRing S<VAR>W : WeierstrassCurve R<VAR>Algebra R S<VAR>A : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>B : Type v<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>f : A →ₐ[S] B<GOAL>(W.baseChange B).Ψ₂Sq = Polynomial.map (↑f) (W.baseChange A).Ψ₂Sq
<VAR>R : Type r<VAR>S : Type s<VAR>CommRing R<VAR>CommRing S<VAR>W : WeierstrassCurve R<VAR>Algebra R S<VAR>A : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>B : Type v<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>f : A →ₐ[S] B<GOAL>(W.baseChange B).Ψ₃ = Polynomial.map (↑f) (W.baseChange A).Ψ₃
<VAR>R : Type r<VAR>S : Type s<VAR>CommRing R<VAR>CommRing S<VAR>W : WeierstrassCurve R<VAR>Algebra R S<VAR>A : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>B : Type v<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>f : A →ₐ[S] B<GOAL>(W.baseChange B).preΨ₄ = Polynomial.map (↑f) (W.baseChange A).preΨ₄
<VAR>R : Type r<VAR>S : Type s<VAR>CommRing R<VAR>CommRing S<VAR>W : WeierstrassCurve R<VAR>Algebra R S<VAR>A : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>B : Type v<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>n : ℕ<GOAL>(W.baseChange B).preΨ' n = Polynomial.map (↑f) ((W.baseChange A).preΨ' n)
<VAR>R : Type r<VAR>S : Type s<VAR>CommRing R<VAR>CommRing S<VAR>W : WeierstrassCurve R<VAR>Algebra R S<VAR>A : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>B : Type v<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>n : ℤ<GOAL>(W.baseChange B).preΨ n = Polynomial.map (↑f) ((W.baseChange A).preΨ n)
<VAR>R : Type r<VAR>S : Type s<VAR>CommRing R<VAR>CommRing S<VAR>W : WeierstrassCurve R<VAR>Algebra R S<VAR>A : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>B : Type v<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>n : ℤ<GOAL>(W.baseChange B).ΨSq n = Polynomial.map (↑f) ((W.baseChange A).ΨSq n)
<VAR>R : Type r<VAR>S : Type s<VAR>CommRing R<VAR>CommRing S<VAR>W : WeierstrassCurve R<VAR>Algebra R S<VAR>A : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>B : Type v<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>n : ℤ<GOAL>(W.baseChange B).Ψ n = Polynomial.map (Polynomial.mapRingHom ↑f) ((W.baseChange A).Ψ n)
<VAR>R : Type r<VAR>S : Type s<VAR>CommRing R<VAR>CommRing S<VAR>W : WeierstrassCurve R<VAR>Algebra R S<VAR>A : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>B : Type v<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>n : ℤ<GOAL>(W.baseChange B).Φ n = Polynomial.map (↑f) ((W.baseChange A).Φ n)
<VAR>R : Type r<VAR>S : Type s<VAR>CommRing R<VAR>CommRing S<VAR>W : WeierstrassCurve R<VAR>Algebra R S<VAR>A : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>B : Type v<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>n : ℤ<GOAL>(W.baseChange B).ψ n = Polynomial.map (Polynomial.mapRingHom ↑f) ((W.baseChange A).ψ n)
<VAR>R : Type r<VAR>S : Type s<VAR>CommRing R<VAR>CommRing S<VAR>W : WeierstrassCurve R<VAR>Algebra R S<VAR>A : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>B : Type v<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>n : ℤ<GOAL>(W.baseChange B).φ n = Polynomial.map (Polynomial.mapRingHom ↑f) ((W.baseChange A).φ n)
<VAR>m n : ℕ<GOAL>↑m - ↑n ≤ ↑(m - n)
<VAR>n : ℕ<GOAL>0 < ↑n + 1
<VAR>a b : ℤ<GOAL>a.natAbs = b.natAbs ↔ a ^ 2 = b ^ 2
<VAR>a b : ℤ<GOAL>a.natAbs < b.natAbs ↔ a ^ 2 < b ^ 2
<VAR>a b : ℤ<GOAL>a.natAbs ≤ b.natAbs ↔ a ^ 2 ≤ b ^ 2
<VAR>a b : ℤ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>a.natAbs = b.natAbs ↔ a = b
<VAR>a b : ℤ<VAR>ha : a ≤ 0<VAR>hb : b ≤ 0<GOAL>a.natAbs = b.natAbs ↔ a = b
<VAR>a b : ℤ<VAR>ha : 0 ≤ a<VAR>hb : b ≤ 0<GOAL>a.natAbs = b.natAbs ↔ a = -b
<VAR>a b : ℤ<VAR>ha : a ≤ 0<VAR>hb : 0 ≤ b<GOAL>a.natAbs = b.natAbs ↔ -a = b
<VAR>a b n : ℕ<VAR>a_le_n : a ≤ n<VAR>b_le_n : b ≤ n<GOAL>(↑a - ↑b).natAbs ≤ n
<VAR>a b n : ℕ<VAR>a_lt_n : a < n<VAR>b_lt_n : b < n<GOAL>(↑a - ↑b).natAbs < n
<GOAL>StrictMonoOn Int.natAbs (Set.Ici 0)
<GOAL>StrictAntiOn Int.natAbs (Set.Iic 0)
<GOAL>Set.InjOn Int.natAbs (Set.Ici 0)
<GOAL>Set.InjOn Int.natAbs (Set.Iic 0)
<VAR>z : ℤ<GOAL>z ≤ 0 → z.toNat = 0
<VAR>b : Bool<VAR>n : ℤ<GOAL>(Int.bit b n).div2 = n
<VAR>R : Type u<VAR>AddGroupWithOne R<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>↑(n - m) = ↑n - ↑m
<VAR>R : Type u<VAR>AddGroupWithOne R<VAR>n : ℕ<GOAL>0 < n → ↑(n - 1) = ↑n - 1
<VAR>R : Type u<VAR>AddGroupWithOne R<VAR>n : ℕ<GOAL>↑(Int.negSucc n) = -↑(n + 1)
<VAR>R : Type u<VAR>AddGroupWithOne R<GOAL>↑0 = 0
<VAR>R : Type u<VAR>AddGroupWithOne R<VAR>n : ℕ<GOAL>↑↑n = ↑n
<VAR>R : Type u<VAR>AddGroupWithOne R<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>↑(OfNat.ofNat n) = OfNat.ofNat n
<VAR>R : Type u<VAR>AddGroupWithOne R<GOAL>↑1 = 1
<VAR>R : Type u<VAR>AddGroupWithOne R<VAR>n : ℤ<GOAL>↑(-n) = -↑n
<VAR>R : Type u<VAR>AddGroupWithOne R<VAR>m n : ℕ<GOAL>↑(Int.subNatNat m n) = ↑m - ↑n
<VAR>R : Type u<VAR>AddGroupWithOne R<VAR>n : ℕ<GOAL>↑(Int.negOfNat n) = -↑n
<VAR>R : Type u<VAR>AddGroupWithOne R<VAR>m n : ℤ<GOAL>↑(m + n) = ↑m + ↑n
<VAR>R : Type u<VAR>AddGroupWithOne R<VAR>m n : ℤ<GOAL>↑(m - n) = ↑m - ↑n
<VAR>R : Type u<VAR>AddGroupWithOne R<GOAL>↑2 = 2
<VAR>R : Type u<VAR>AddGroupWithOne R<GOAL>↑3 = 3
<VAR>R : Type u<VAR>AddGroupWithOne R<GOAL>↑4 = 4
<VAR>R : Type u<VAR>self : AddGroupWithOne R<VAR>n : ℕ<GOAL>IntCast.intCast (Int.negSucc n) = -↑(n + 1)
<VAR>R : Type u<VAR>self : AddGroupWithOne R<VAR>n : ℕ<GOAL>IntCast.intCast ↑n = ↑n
<VAR>R : Type u_2<VAR>DivisionRing R<VAR>n : ℕ<GOAL>↑(-↑n) = -↑n
<VAR>α : Type u_1<VAR>DivisionRing α<VAR>m n : ℤ<VAR>n_dvd : n ∣ m<VAR>hn : ↑n ≠ 0<GOAL>↑(m / n) = ↑m / ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsRefl α r<VAR>IsRefl β s<VAR>x : α ⊕ β<GOAL>Sum.LiftRel r s x x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsTrans α r<VAR>IsTrans β s<VAR>a b c : α ⊕ β<GOAL>Sum.LiftRel r s a b → Sum.LiftRel r s b c → Sum.LiftRel r s a c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LE α<VAR>LE β<VAR>a b : α ⊕ β<GOAL>a ≤ b ↔ Sum.LiftRel (fun x x_1 => x ≤ x_1) (fun x x_1 => x ≤ x_1) a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LT α<VAR>LT β<VAR>a b : α ⊕ β<GOAL>a < b ↔ Sum.LiftRel (fun x x_1 => x < x_1) (fun x x_1 => x < x_1) a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LE α<VAR>LE β<VAR>a b : α<GOAL>Sum.inl a ≤ Sum.inl b ↔ a ≤ b