ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a a' : α<VAR>b : β a<VAR>b' : β a'<VAR>s : AList β<VAR>h : a ≠ a'<GOAL>(AList.insert a' b' (AList.insert a b s)).entries ~ (AList.insert a b (AList.insert a' b' s)).entries
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b b' : β a<GOAL>AList.insert a b (AList.singleton a b') = AList.singleton a b
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>xs : List (Sigma β)<GOAL>xs.toAList.entries = xs.dedupKeys
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>xs : List (Sigma β)<GOAL>(⟨a, b⟩ :: xs).toAList = AList.insert a b xs.toAList
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>c : Sigma β<VAR>l : List (Sigma β)<VAR>h : (c :: l).NodupKeys<GOAL>{ entries := c :: l, nodupKeys := h } = AList.insert c.fst c.snd { entries := l, nodupKeys := ⋯ }
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>C : AList β → Sort u_1<VAR>H0 : C ∅<VAR>IH : (a : α) → (b : β a) → (l : AList β) → a ∉ l → C l → C (AList.insert a b l)<GOAL>AList.insertRec H0 IH ∅ = H0
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>C : AList β → Sort u_1<VAR>H0 : C ∅<VAR>IH : (a : α) → (b : β a) → (l : AList β) → a ∉ l → C l → C (AList.insert a b l)<VAR>c : Sigma β<VAR>l : AList β<VAR>h : c.fst ∉ l<GOAL>AList.insertRec H0 IH (AList.insert c.fst c.snd l) = IH c.fst c.snd l h (AList.insertRec H0 IH l)
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>C : AList β → Sort u_1<VAR>H0 : C ∅<VAR>IH : (a : α) → (b : β a) → (l : AList β) → a ∉ l → C l → C (AList.insert a b l)<VAR>a : α<VAR>b : β a<VAR>l : AList β<VAR>h : a ∉ l<GOAL>AList.insertRec H0 IH (AList.insert a b l) = IH a b l h (AList.insertRec H0 IH l)
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>s : AList β<GOAL>AList.extract a s = (AList.lookup a s, AList.erase a s)
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>s₁ s₂ : AList β<GOAL>(s₁ ∪ s₂).entries = s₁.entries.kunion s₂.entries
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>s : AList β<GOAL>∅ ∪ s = s
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>s : AList β<GOAL>s ∪ ∅ = s
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>s₁ s₂ : AList β<GOAL>a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ ∨ a ∈ s₂
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>s₁ s₂ s₃ s₄ : AList β<VAR>p₁₂ : s₁.entries ~ s₂.entries<VAR>p₃₄ : s₃.entries ~ s₄.entries<GOAL>(s₁ ∪ s₃).entries ~ (s₂ ∪ s₄).entries
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>s₁ s₂ : AList β<GOAL>AList.erase a (s₁ ∪ s₂) = AList.erase a s₁ ∪ AList.erase a s₂
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>s₁ s₂ : AList β<GOAL>a ∈ s₁ → AList.lookup a (s₁ ∪ s₂) = AList.lookup a s₁
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>s₁ s₂ : AList β<GOAL>a ∉ s₁ → AList.lookup a (s₁ ∪ s₂) = AList.lookup a s₂
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>s₁ s₂ : AList β<GOAL>b ∈ AList.lookup a (s₁ ∪ s₂) ↔ b ∈ AList.lookup a s₁ ∨ a ∉ s₁ ∧ b ∈ AList.lookup a s₂
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>s₁ s₂ : AList β<GOAL>AList.lookup a (s₁ ∪ s₂) = some b ↔ AList.lookup a s₁ = some b ∨ a ∉ s₁ ∧ AList.lookup a s₂ = some b
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>s₁ s₂ s₃ : AList β<GOAL>b ∈ AList.lookup a (s₁ ∪ s₃) → a ∉ s₂ → b ∈ AList.lookup a (s₁ ∪ s₂ ∪ s₃)
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>s₁ s₂ : AList β<GOAL>AList.insert a b (s₁ ∪ s₂) = AList.insert a b s₁ ∪ s₂
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>s₁ s₂ s₃ : AList β<GOAL>(s₁ ∪ s₂ ∪ s₃).entries ~ (s₁ ∪ (s₂ ∪ s₃)).entries
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>s₁ s₂ : AList β<VAR>h : s₁.Disjoint s₂<GOAL>(s₁ ∪ s₂).entries ~ (s₂ ∪ s₁).entries
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>4 * W.b₈ = W.b₂ * W.b₆ - W.b₄ ^ 2
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>1728 * W.Δ = W.c₄ ^ 3 - W.c₆ ^ 2
<VAR>R : Type u<VAR>CommRing R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>WeierstrassCurve.VariableChange.id.comp C = C
<VAR>R : Type u<VAR>CommRing R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>C.comp WeierstrassCurve.VariableChange.id = C
<VAR>R : Type u<VAR>CommRing R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>C.inv.comp C = WeierstrassCurve.VariableChange.id
<VAR>R : Type u<VAR>CommRing R<VAR>C C' C'' : WeierstrassCurve.VariableChange R<GOAL>(C.comp C').comp C'' = C.comp (C'.comp C'')
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>(W.variableChange C).a₂ = ↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>(W.variableChange C).a₃ = ↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>(W.variableChange C).a₁ = ↑C.u⁻¹ * (W.a₁ + 2 * C.s)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>(W.variableChange C).a₄ = ↑C.u⁻¹ ^ 4 * (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>(W.variableChange C).a₆ = ↑C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.variableChange WeierstrassCurve.VariableChange.id = W
<VAR>R : Type u<VAR>CommRing R<VAR>C C' : WeierstrassCurve.VariableChange R<VAR>W : WeierstrassCurve R<GOAL>W.variableChange (C.comp C') = (W.variableChange C').variableChange C
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>(W.variableChange C).b₂ = ↑C.u⁻¹ ^ 2 * (W.b₂ + 12 * C.r)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>(W.variableChange C).b₄ = ↑C.u⁻¹ ^ 4 * (W.b₄ + C.r * W.b₂ + 6 * C.r ^ 2)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>(W.variableChange C).b₆ = ↑C.u⁻¹ ^ 6 * (W.b₆ + 2 * C.r * W.b₄ + C.r ^ 2 * W.b₂ + 4 * C.r ^ 3)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>(W.variableChange C).b₈ = ↑C.u⁻¹ ^ 8 * (W.b₈ + 3 * C.r * W.b₆ + 3 * C.r ^ 2 * W.b₄ + C.r ^ 3 * W.b₂ + 3 * C.r ^ 4)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>(W.variableChange C).c₄ = ↑C.u⁻¹ ^ 4 * W.c₄
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>(W.variableChange C).c₆ = ↑C.u⁻¹ ^ 6 * W.c₆
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>(W.variableChange C).Δ = ↑C.u⁻¹ ^ 12 * W.Δ
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<GOAL>(W.map φ).a₃ = φ W.a₃
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<GOAL>(W.map φ).a₆ = φ W.a₆
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<GOAL>(W.map φ).a₄ = φ W.a₄
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<GOAL>(W.map φ).a₁ = φ W.a₁
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<GOAL>(W.map φ).a₂ = φ W.a₂
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<GOAL>(W.map φ).b₂ = φ W.b₂
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<GOAL>(W.map φ).b₄ = φ W.b₄
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<GOAL>(W.map φ).b₆ = φ W.b₆
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<GOAL>(W.map φ).b₈ = φ W.b₈
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<GOAL>(W.map φ).c₄ = φ W.c₄
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<GOAL>(W.map φ).c₆ = φ W.c₆
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<GOAL>(W.map φ).Δ = φ W.Δ
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.map (RingHom.id R) = W
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<VAR>B : Type w<VAR>CommRing B<VAR>ψ : A →+* B<GOAL>(W.map φ).map ψ = W.map (ψ.comp φ)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>S : Type s<VAR>CommRing S<VAR>Algebra R S<VAR>A : Type v<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>B : Type w<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>ψ : A →ₐ[S] B<GOAL>(W.baseChange A).map ↑ψ = W.baseChange B
<VAR>R : Type u<VAR>CommRing R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<VAR>hφ : Function.Injective ⇑φ<GOAL>Function.Injective fun W => W.map φ
<VAR>R : Type u<VAR>CommRing R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<VAR>C : WeierstrassCurve.VariableChange R<GOAL>(WeierstrassCurve.VariableChange.map φ C).t = φ C.t
<VAR>R : Type u<VAR>CommRing R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<VAR>C : WeierstrassCurve.VariableChange R<GOAL>(WeierstrassCurve.VariableChange.map φ C).r = φ C.r
<VAR>R : Type u<VAR>CommRing R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<VAR>C : WeierstrassCurve.VariableChange R<GOAL>(WeierstrassCurve.VariableChange.map φ C).s = φ C.s
<VAR>R : Type u<VAR>CommRing R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<VAR>C : WeierstrassCurve.VariableChange R<GOAL>(WeierstrassCurve.VariableChange.map φ C).u = (Units.map ↑φ) C.u
<VAR>R : Type u<VAR>CommRing R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>WeierstrassCurve.VariableChange.map (RingHom.id R) C = C
<VAR>R : Type u<VAR>CommRing R<VAR>C : WeierstrassCurve.VariableChange R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<VAR>B : Type w<VAR>CommRing B<VAR>ψ : A →+* B<GOAL>WeierstrassCurve.VariableChange.map ψ (WeierstrassCurve.VariableChange.map φ C) = WeierstrassCurve.VariableChange.map (ψ.comp φ) C
<VAR>R : Type u<VAR>CommRing R<VAR>C : WeierstrassCurve.VariableChange R<VAR>S : Type s<VAR>CommRing S<VAR>Algebra R S<VAR>A : Type v<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>B : Type w<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>ψ : A →ₐ[S] B<GOAL>WeierstrassCurve.VariableChange.map (↑ψ) (WeierstrassCurve.VariableChange.baseChange A C) = WeierstrassCurve.VariableChange.baseChange B C
<VAR>R : Type u<VAR>CommRing R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<VAR>hφ : Function.Injective ⇑φ<GOAL>Function.Injective (WeierstrassCurve.VariableChange.map φ)
<VAR>R : Type u<VAR>CommRing R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<GOAL>WeierstrassCurve.VariableChange.map φ WeierstrassCurve.VariableChange.id = WeierstrassCurve.VariableChange.id
<VAR>R : Type u<VAR>CommRing R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<VAR>C C' : WeierstrassCurve.VariableChange R<GOAL>WeierstrassCurve.VariableChange.map φ (C.comp C') = (WeierstrassCurve.VariableChange.map φ C).comp (WeierstrassCurve.VariableChange.map φ C')
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<VAR>C : WeierstrassCurve.VariableChange R<GOAL>(W.map φ).variableChange (WeierstrassCurve.VariableChange.map φ C) = (W.variableChange C).map φ
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<GOAL>W.twoTorsionPolynomial.disc = 16 * W.Δ
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>Invertible 2<GOAL>IsUnit W.twoTorsionPolynomial.disc ↔ IsUnit W.Δ
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve R<VAR>Nontrivial R<VAR>Invertible 2<VAR>hΔ : IsUnit W.Δ<GOAL>W.twoTorsionPolynomial.disc ≠ 0
<VAR>R : Type u<VAR>CommRing R<GOAL>(WeierstrassCurve.ofJ0 R).c₄ = 0
<VAR>R : Type u<VAR>CommRing R<GOAL>(WeierstrassCurve.ofJ0 R).Δ = -27
<VAR>R : Type u<VAR>CommRing R<GOAL>(WeierstrassCurve.ofJ1728 R).c₄ = -48
<VAR>R : Type u<VAR>CommRing R<GOAL>(WeierstrassCurve.ofJ1728 R).Δ = -64
<VAR>R : Type u<VAR>CommRing R<VAR>j : R<GOAL>(WeierstrassCurve.ofJ j).c₄ = j * (j - 1728) ^ 3
<VAR>R : Type u<VAR>CommRing R<VAR>j : R<GOAL>(WeierstrassCurve.ofJ j).Δ = j ^ 2 * (j - 1728) ^ 9
<VAR>R : Type u<VAR>CommRing R<VAR>self : EllipticCurve R<GOAL>↑self.Δ' = self.Δ
<VAR>R : Type u<VAR>CommRing R<VAR>E : EllipticCurve R<VAR>Nontrivial R<VAR>Invertible 2<GOAL>E.twoTorsionPolynomial.disc ≠ 0
<VAR>R : Type u<VAR>CommRing R<VAR>E : EllipticCurve R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>(E.variableChange C).a₄ = ↑C.u⁻¹ ^ 4 * (E.a₄ - C.s * E.a₃ + 2 * C.r * E.a₂ - (C.t + C.r * C.s) * E.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)
<VAR>R : Type u<VAR>CommRing R<VAR>E : EllipticCurve R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>(E.variableChange C).toWeierstrassCurve = E.variableChange C
<VAR>R : Type u<VAR>CommRing R<VAR>E : EllipticCurve R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>(E.variableChange C).Δ' = C.u⁻¹ ^ 12 * E.Δ'
<VAR>R : Type u<VAR>CommRing R<VAR>E : EllipticCurve R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>(E.variableChange C).a₃ = ↑C.u⁻¹ ^ 3 * (E.a₃ + C.r * E.a₁ + 2 * C.t)
<VAR>R : Type u<VAR>CommRing R<VAR>E : EllipticCurve R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>(E.variableChange C).a₁ = ↑C.u⁻¹ * (E.a₁ + 2 * C.s)
<VAR>R : Type u<VAR>CommRing R<VAR>E : EllipticCurve R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>(E.variableChange C).a₂ = ↑C.u⁻¹ ^ 2 * (E.a₂ - C.s * E.a₁ + 3 * C.r - C.s ^ 2)
<VAR>R : Type u<VAR>CommRing R<VAR>E : EllipticCurve R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>(E.variableChange C).a₆ = ↑C.u⁻¹ ^ 6 * (E.a₆ + C.r * E.a₄ + C.r ^ 2 * E.a₂ + C.r ^ 3 - C.t * E.a₃ - C.t ^ 2 - C.r * C.t * E.a₁)
<VAR>R : Type u<VAR>CommRing R<VAR>E : EllipticCurve R<GOAL>E.variableChange WeierstrassCurve.VariableChange.id = E
<VAR>R : Type u<VAR>CommRing R<VAR>C C' : WeierstrassCurve.VariableChange R<VAR>E : EllipticCurve R<GOAL>E.variableChange (C.comp C') = (E.variableChange C').variableChange C
<VAR>R : Type u<VAR>CommRing R<VAR>E : EllipticCurve R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>(E.variableChange C).Δ'⁻¹ = C.u ^ 12 * E.Δ'⁻¹
<VAR>R : Type u<VAR>CommRing R<VAR>E : EllipticCurve R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>(E.variableChange C).j = E.j
<VAR>R : Type u<VAR>CommRing R<VAR>E : EllipticCurve R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<GOAL>(E.map φ).a₆ = φ E.a₆
<VAR>R : Type u<VAR>CommRing R<VAR>E : EllipticCurve R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<GOAL>(E.map φ).a₄ = φ E.a₄
<VAR>R : Type u<VAR>CommRing R<VAR>E : EllipticCurve R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<GOAL>(E.map φ).a₂ = φ E.a₂
<VAR>R : Type u<VAR>CommRing R<VAR>E : EllipticCurve R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<GOAL>(E.map φ).toWeierstrassCurve = E.map φ
<VAR>R : Type u<VAR>CommRing R<VAR>E : EllipticCurve R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<GOAL>(E.map φ).Δ' = (Units.map ↑φ) E.Δ'
<VAR>R : Type u<VAR>CommRing R<VAR>E : EllipticCurve R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<GOAL>(E.map φ).a₁ = φ E.a₁
<VAR>R : Type u<VAR>CommRing R<VAR>E : EllipticCurve R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<GOAL>(E.map φ).a₃ = φ E.a₃
<VAR>R : Type u<VAR>CommRing R<VAR>E : EllipticCurve R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<GOAL>↑(E.map φ).Δ' = φ ↑E.Δ'
<VAR>R : Type u<VAR>CommRing R<VAR>E : EllipticCurve R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<GOAL>↑(E.map φ).Δ'⁻¹ = φ ↑E.Δ'⁻¹
<VAR>R : Type u<VAR>CommRing R<VAR>E : EllipticCurve R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<GOAL>(E.map φ).j = φ E.j
<VAR>R : Type u<VAR>CommRing R<VAR>A : Type v<VAR>CommRing A<VAR>φ : R →+* A<VAR>hφ : Function.Injective ⇑φ<GOAL>Function.Injective fun E => E.map φ
<VAR>R : Type u<VAR>CommRing R<VAR>Invertible 3<GOAL>(EllipticCurve.ofJ0 R).j = 0
<VAR>R : Type u<VAR>CommRing R<VAR>Invertible 2<GOAL>(EllipticCurve.ofJ1728 R).j = 1728
<VAR>R : Type u<VAR>CommRing R<VAR>j : R<VAR>Invertible j<VAR>Invertible (j - 1728)<GOAL>(EllipticCurve.ofJ' j).j = j
<VAR>F : Type u<VAR>Field F<GOAL>2 ≠ 0 ∨ 3 ≠ 0
<VAR>F : Type u<VAR>Field F<VAR>DecidableEq F<VAR>h3 : NeZero 3<GOAL>EllipticCurve.ofJ 0 = EllipticCurve.ofJ0 F
<VAR>F : Type u<VAR>Field F<VAR>DecidableEq F<VAR>h3 : 3 = 0<GOAL>EllipticCurve.ofJ 0 = EllipticCurve.ofJ1728 F
<VAR>F : Type u<VAR>Field F<VAR>DecidableEq F<VAR>h2 : 2 = 0<GOAL>EllipticCurve.ofJ 0 = EllipticCurve.ofJ0 F
<VAR>F : Type u<VAR>Field F<VAR>DecidableEq F<VAR>h3 : 3 = 0<GOAL>EllipticCurve.ofJ 1728 = EllipticCurve.ofJ1728 F
<VAR>F : Type u<VAR>Field F<VAR>DecidableEq F<VAR>h2 : NeZero 2<GOAL>EllipticCurve.ofJ 1728 = EllipticCurve.ofJ1728 F
<VAR>F : Type u<VAR>Field F<VAR>DecidableEq F<VAR>h2 : 2 = 0<GOAL>EllipticCurve.ofJ 1728 = EllipticCurve.ofJ0 F
<VAR>F : Type u<VAR>Field F<VAR>j : F<VAR>DecidableEq F<VAR>h0 : j ≠ 0<VAR>h1728 : j ≠ 1728<GOAL>EllipticCurve.ofJ j = EllipticCurve.ofJ' j
<VAR>F : Type u<VAR>Field F<VAR>j : F<VAR>DecidableEq F<GOAL>(EllipticCurve.ofJ j).j = j
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>r : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))<VAR>x : ↑X.toTopCat<GOAL>r ∉ (X.toΓSpecFun x).asIdeal ↔ IsUnit ((X.presheaf.Γgerm x) r)
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>r : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))<GOAL>X.toΓSpecFun ⁻¹' (PrimeSpectrum.basicOpen r).carrier = (X.toRingedSpace.basicOpen r).carrier
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<GOAL>Continuous X.toΓSpecFun
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<GOAL>∀ (a : ↑X.toTopCat), X.toΓSpecBase a = X.toΓSpecFun a
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>r : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))<GOAL>X.toΓSpecMapBasicOpen r = X.toRingedSpace.basicOpen r
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>r : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))<GOAL>IsUnit ((X.toToΓSpecMapBasicOpen r) r)
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>r : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))<VAR>f : (AlgebraicGeometry.Spec.structureSheaf ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))).val.obj (Opposite.op (PrimeSpectrum.basicOpen r)) ⟶ X.presheaf.obj (Opposite.op (X.toΓSpecMapBasicOpen r))<GOAL>CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toOpen (↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))) (PrimeSpectrum.basicOpen r)) f = X.toToΓSpecMapBasicOpen r ↔ f = X.toΓSpecCApp r
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>r : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))<GOAL>CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toOpen (↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))) (PrimeSpectrum.basicOpen r)) (X.toΓSpecCApp r) = X.toToΓSpecMapBasicOpen r
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>r : (CategoryTheory.InducedCategory (TopologicalSpace.Opens (PrimeSpectrum ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X)))) PrimeSpectrum.basicOpen)ᵒᵖ<GOAL>X.toΓSpecCBasicOpens.app r = X.toΓSpecCApp (Opposite.unop r)
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<GOAL>X.toΓSpecSheafedSpace.base = X.toΓSpecBase
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<GOAL>X.toΓSpecSheafedSpace.c = (TopCat.Sheaf.restrictHomEquivHom (AlgebraicGeometry.Spec.structureSheaf ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))).val ((TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase).obj X.𝒪) ⋯) X.toΓSpecCBasicOpens
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>r : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))<GOAL>X.toΓSpecSheafedSpace.c.app (Opposite.op (PrimeSpectrum.basicOpen r)) = X.toΓSpecCApp r
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>r : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))<GOAL>CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toOpen (↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))) (PrimeSpectrum.basicOpen r)) (X.toΓSpecSheafedSpace.c.app (Opposite.op (PrimeSpectrum.basicOpen r))) = X.toToΓSpecMapBasicOpen r
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>x : ↑X.toTopCat<GOAL>CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toStalk (↑(Opposite.unop (Opposite.op (AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))))) (X.toΓSpecSheafedSpace.base x)) (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace x) = X.presheaf.Γgerm x
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<GOAL>X.toΓSpec.val.base = X.toΓSpecBase
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>s : Set ↑(X.presheaf.obj (Opposite.op ⊤))<GOAL>⇑X.toΓSpec.val.base ⁻¹' PrimeSpectrum.zeroLocus s = X.toRingedSpace.zeroLocus s
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>R : CommRingCat<VAR>f : R ⟶ AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X)<VAR>β : X ⟶ AlgebraicGeometry.Spec.locallyRingedSpaceObj R<VAR>w : CategoryTheory.CategoryStruct.comp X.toΓSpec.val.base (AlgebraicGeometry.Spec.locallyRingedSpaceMap f).val.base = β.val.base<VAR>h : ∀ (r : ↑R), CategoryTheory.CategoryStruct.comp f (X.presheaf.map (CategoryTheory.homOfLE ⋯).op) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toOpen (↑R) (PrimeSpectrum.basicOpen r)) (β.val.c.app (Opposite.op (PrimeSpectrum.basicOpen r)))<GOAL>CategoryTheory.CategoryStruct.comp X.toΓSpec (AlgebraicGeometry.Spec.locallyRingedSpaceMap f) = β
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<GOAL>CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.toSpecΓ (AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))) (X.toΓSpec.val.c.app (Opposite.op ⊤)) = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<GOAL>CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity.inv.app (AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))) ((AlgebraicGeometry.identityToΓSpec.app X).val.c.app (Opposite.op ⊤)) = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id CommRingCat).obj (AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X)))
<VAR>R : CommRingCat<GOAL>CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.identityToΓSpec.app (AlgebraicGeometry.Spec.toLocallyRingedSpace.obj (Opposite.op R))) (AlgebraicGeometry.Spec.toLocallyRingedSpace.map (AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity.inv.app R).op) = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id AlgebraicGeometry.LocallyRingedSpace).obj (AlgebraicGeometry.Spec.toLocallyRingedSpace.obj (Opposite.op R)))
<GOAL>AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.unit = AlgebraicGeometry.identityToΓSpec
<GOAL>AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.counit = (CategoryTheory.NatIso.op AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity).inv
<VAR>R : CommRingCatᵒᵖ<GOAL>AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.counit.app R = (AlgebraicGeometry.StructureSheaf.toOpen ↑(Opposite.unop R) ⊤).op
<VAR>R : Type u<VAR>CommRing R<GOAL>AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.counit.app (Opposite.op (CommRingCat.of R)) = (AlgebraicGeometry.StructureSheaf.toOpen R ⊤).op
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>R : CommRingCatᵒᵖ<VAR>f : AlgebraicGeometry.LocallyRingedSpace.Γ.rightOp.obj X ⟶ R<GOAL>(AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.homEquiv X R) f = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.identityToΓSpec.app X) (AlgebraicGeometry.Spec.locallyRingedSpaceMap f.unop)