awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
⊢ (W'.map f).dblX ((⇑f : (a : R) → S) ∘ P) = (f : (a : R) → S) (W'.dblX P)
have simp : HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) (W'.dblU P) : S) 2 -
        HMul.hMul (β := S) (W'.map f).a₁ ((f : (a : R) → S) (W'.dblU P) : S) * ((⇑f : (a : R) → S) ∘ P) z *
          HSub.hSub (α := S) (β := S) (((⇑f : (a : R) → S) ∘ P) y : S) ((f : (a : R) → S) (W'.negY P) : S) -
      (W'.map f).a₂ * HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ P) z) 2 *
        HPow.hPow (β := ℕ)
          (HSub.hSub (α := S) (β := S) (((⇑f : (a : R) → S) ∘ P) y : S) ((f : (a : R) → S) (W'.negY P) : S)) 2 -
    HMul.hMul (α := S) 2 (((⇑f : (a : R) → S) ∘ P) x) *
      HPow.hPow (β := ℕ)
        (HSub.hSub (α := S) (β := S) (((⇑f : (a : R) → S) ∘ P) y : S) ((f : (a : R) → S) (W'.negY P) : S)) 2 =
  (f : (a : R) → S)
    (HPow.hPow (β := ℕ) (W'.dblU P) 2 - W'.a₁ * W'.dblU P * P z * (P y - W'.negY P) -
        W'.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P y - W'.negY P) 2 -
      2 * P x * HPow.hPow (β := ℕ) (P y - W'.negY P) 2)
Tactic: simp only [dblX, map_dblU, map_negY]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
⊢ (W'.map f).negDblY ((⇑f : (a : R) → S) ∘ P) = (f : (a : R) → S) (W'.negDblY P)
have simp : HMul.hMul (α := S) (-(f : (a : R) → S) (W'.dblU P) : S)
      (HSub.hSub (α := S) ((f : (a : R) → S) (W'.dblX P) : S)
        (((⇑f : (a : R) → S) ∘ P) x *
          HPow.hPow (β := ℕ)
            (HSub.hSub (α := S) (β := S) (((⇑f : (a : R) → S) ∘ P) y : S) ((f : (a : R) → S) (W'.negY P) : S)) 2)) +
    ((⇑f : (a : R) → S) ∘ P) y *
      HPow.hPow (β := ℕ)
        (HSub.hSub (α := S) (β := S) (((⇑f : (a : R) → S) ∘ P) y : S) ((f : (a : R) → S) (W'.negY P) : S)) 3 =
  (f : (a : R) → S)
    (-W'.dblU P * (W'.dblX P - P x * HPow.hPow (β := ℕ) (P y - W'.negY P) 2) +
      P y * HPow.hPow (β := ℕ) (P y - W'.negY P) 3)
Tactic: simp only [negDblY, map_dblU, map_dblX, map_negY]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
⊢ (W'.map f).dblY ((⇑f : (a : R) → S) ∘ P) = (f : (a : R) → S) (W'.dblY P)
have simp : HSub.hSub (α := S) (-(f : (a : R) → S) (W'.negDblY P) : S)
      (HMul.hMul (β := S) (HMul.hMul (β := S) (W'.map f).a₁ ((f : (a : R) → S) (W'.dblX P) : S))
        ((f : (a : R) → S) (W'.dblZ P) : S)) -
    (W'.map f).a₃ * HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) (W'.dblZ P) : S) 3 =
  (f : (a : R) → S) (-W'.negDblY P - W'.a₁ * W'.dblX P * W'.dblZ P - W'.a₃ * HPow.hPow (β := ℕ) (W'.dblZ P) 3)
Tactic: simp only [dblY, negY_eq, map_negDblY, map_dblX, map_dblZ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
⊢ Eq.{v + 1} (α := K) (addU ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) : K) ((f : (a : F) → K) (addU P Q) : K)
have simp : -((((⇑f : (a : F) → K) ∘ P) y * HPow.hPow (α := K) (β := ℕ) (((⇑f : (a : F) → K) ∘ Q) z) 3 -
        ((⇑f : (a : F) → K) ∘ Q) y * HPow.hPow (α := K) (β := ℕ) (((⇑f : (a : F) → K) ∘ P) z) 3) /
      HMul.hMul (α := K) (((⇑f : (a : F) → K) ∘ P) z) (((⇑f : (a : F) → K) ∘ Q) z)) =
  (f : (a : F) → K) (-((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z)))
Tactic: simp only [addU]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
P Q : Fin 3 → R
⊢ Eq.{s + 1} (α := S) (addZ ((⇑f : (a : R) → S) ∘ P) ((⇑f : (a : R) → S) ∘ Q) : S) ((f : (a : R) → S) (addZ P Q) : S)
have simp : ((⇑f : (a : R) → S) ∘ P) x * HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ Q) z) 2 -
    ((⇑f : (a : R) → S) ∘ Q) x * HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ P) z) 2 =
  (f : (a : R) → S) (P x * HPow.hPow (β := ℕ) (Q z) 2 - Q x * HPow.hPow (β := ℕ) (P z) 2)
Tactic: simp only [addZ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Jacobian R
f : R →+* S
P Q : Fin 3 → R
⊢ (W'.map f).addY ((⇑f : (a : R) → S) ∘ P) ((⇑f : (a : R) → S) ∘ Q) = (f : (a : R) → S) (W'.addY P Q)
have simp : HSub.hSub (α := S) (-(f : (a : R) → S) (W'.negAddY P Q) : S)
      (HMul.hMul (β := S) (HMul.hMul (β := S) (W'.map f).a₁ ((f : (a : R) → S) (W'.addX P Q) : S))
        ((f : (a : R) → S) (addZ P Q) : S)) -
    (W'.map f).a₃ * HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) (addZ P Q) : S) 3 =
  (f : (a : R) → S) (-W'.negAddY P Q - W'.a₁ * W'.addX P Q * addZ P Q - W'.a₃ * HPow.hPow (β := ℕ) (addZ P Q) 3)
Tactic: simp only [addY, negY_eq, map_negAddY, map_addX, map_addZ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (W'⁄B).negY ((⇑f : (a : A) → B) ∘ P) = (f : (a : A) → B) ((W'⁄A).negY P)
have rw : (W'⁄B).negY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).negY P)
Tactic: rw [← RingHom.coe_coe, ← map_negY, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
rw : (W'⁄B).negY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).negY P)
⊢ (W'⁄B).negY ((⇑f : (a : A) → B) ∘ P) = (f : (a : A) → B) ((W'⁄A).negY P)
have rw₁ : (W'⁄B).negY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) =
  ((W'⁄A).map (↑f : A →+* B)).negY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
Tactic: rw [← RingHom.coe_coe, ← map_negY, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
rw : (W'⁄B).negY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).negY P)
rw₁ :
  (W'⁄B).negY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) =
    ((W'⁄A).map (↑f : A →+* B)).negY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
⊢ (W'⁄B).negY ((⇑f : (a : A) → B) ∘ P) = (f : (a : A) → B) ((W'⁄A).negY P)
have rw₂ : (W'⁄B).negY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = (W'⁄B).negY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
Tactic: rw [← RingHom.coe_coe, ← map_negY, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (W'⁄B).dblU ((⇑f : (a : A) → B) ∘ P) = (f : (a : A) → B) ((W'⁄A).dblU P)
have rw : (W'⁄B).dblU ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).dblU P)
Tactic: rw [← RingHom.coe_coe, ← map_dblU, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
rw : (W'⁄B).dblU ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).dblU P)
⊢ (W'⁄B).dblU ((⇑f : (a : A) → B) ∘ P) = (f : (a : A) → B) ((W'⁄A).dblU P)
have rw₁ : (W'⁄B).dblU ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) =
  ((W'⁄A).map (↑f : A →+* B)).dblU ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
Tactic: rw [← RingHom.coe_coe, ← map_dblU, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
rw : (W'⁄B).dblU ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).dblU P)
rw₁ :
  (W'⁄B).dblU ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) =
    ((W'⁄A).map (↑f : A →+* B)).dblU ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
⊢ (W'⁄B).dblU ((⇑f : (a : A) → B) ∘ P) = (f : (a : A) → B) ((W'⁄A).dblU P)
have rw₂ : (W'⁄B).dblU ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = (W'⁄B).dblU ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
Tactic: rw [← RingHom.coe_coe, ← map_dblU, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (W'⁄B).dblZ ((⇑f : (a : A) → B) ∘ P) = (f : (a : A) → B) ((W'⁄A).dblZ P)
have rw : (W'⁄B).dblZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).dblZ P)
Tactic: rw [← RingHom.coe_coe, ← map_dblZ, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
rw : (W'⁄B).dblZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).dblZ P)
⊢ (W'⁄B).dblZ ((⇑f : (a : A) → B) ∘ P) = (f : (a : A) → B) ((W'⁄A).dblZ P)
have rw₁ : (W'⁄B).dblZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) =
  ((W'⁄A).map (↑f : A →+* B)).dblZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
Tactic: rw [← RingHom.coe_coe, ← map_dblZ, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
rw : (W'⁄B).dblZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).dblZ P)
rw₁ :
  (W'⁄B).dblZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) =
    ((W'⁄A).map (↑f : A →+* B)).dblZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
⊢ (W'⁄B).dblZ ((⇑f : (a : A) → B) ∘ P) = (f : (a : A) → B) ((W'⁄A).dblZ P)
have rw₂ : (W'⁄B).dblZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = (W'⁄B).dblZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
Tactic: rw [← RingHom.coe_coe, ← map_dblZ, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (W'⁄B).dblX ((⇑f : (a : A) → B) ∘ P) = (f : (a : A) → B) ((W'⁄A).dblX P)
have rw : (W'⁄B).dblX ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).dblX P)
Tactic: rw [← RingHom.coe_coe, ← map_dblX, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
rw : (W'⁄B).dblX ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).dblX P)
⊢ (W'⁄B).dblX ((⇑f : (a : A) → B) ∘ P) = (f : (a : A) → B) ((W'⁄A).dblX P)
have rw₁ : (W'⁄B).dblX ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) =
  ((W'⁄A).map (↑f : A →+* B)).dblX ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
Tactic: rw [← RingHom.coe_coe, ← map_dblX, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
rw : (W'⁄B).dblX ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).dblX P)
rw₁ :
  (W'⁄B).dblX ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) =
    ((W'⁄A).map (↑f : A →+* B)).dblX ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
⊢ (W'⁄B).dblX ((⇑f : (a : A) → B) ∘ P) = (f : (a : A) → B) ((W'⁄A).dblX P)
have rw₂ : (W'⁄B).dblX ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = (W'⁄B).dblX ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
Tactic: rw [← RingHom.coe_coe, ← map_dblX, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (W'⁄B).negDblY ((⇑f : (a : A) → B) ∘ P) = (f : (a : A) → B) ((W'⁄A).negDblY P)
have rw : (W'⁄B).negDblY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).negDblY P)
Tactic: rw [← RingHom.coe_coe, ← map_negDblY, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
rw : (W'⁄B).negDblY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).negDblY P)
⊢ (W'⁄B).negDblY ((⇑f : (a : A) → B) ∘ P) = (f : (a : A) → B) ((W'⁄A).negDblY P)
have rw₁ : (W'⁄B).negDblY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) =
  ((W'⁄A).map (↑f : A →+* B)).negDblY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
Tactic: rw [← RingHom.coe_coe, ← map_negDblY, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
rw : (W'⁄B).negDblY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).negDblY P)
rw₁ :
  (W'⁄B).negDblY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) =
    ((W'⁄A).map (↑f : A →+* B)).negDblY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
⊢ (W'⁄B).negDblY ((⇑f : (a : A) → B) ∘ P) = (f : (a : A) → B) ((W'⁄A).negDblY P)
have rw₂ : (W'⁄B).negDblY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = (W'⁄B).negDblY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
Tactic: rw [← RingHom.coe_coe, ← map_negDblY, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (W'⁄B).dblY ((⇑f : (a : A) → B) ∘ P) = (f : (a : A) → B) ((W'⁄A).dblY P)
have rw : (W'⁄B).dblY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).dblY P)
Tactic: rw [← RingHom.coe_coe, ← map_dblY, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
rw : (W'⁄B).dblY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).dblY P)
⊢ (W'⁄B).dblY ((⇑f : (a : A) → B) ∘ P) = (f : (a : A) → B) ((W'⁄A).dblY P)
have rw₁ : (W'⁄B).dblY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) =
  ((W'⁄A).map (↑f : A →+* B)).dblY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
Tactic: rw [← RingHom.coe_coe, ← map_dblY, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
rw : (W'⁄B).dblY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).dblY P)
rw₁ :
  (W'⁄B).dblY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) =
    ((W'⁄A).map (↑f : A →+* B)).dblY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
⊢ (W'⁄B).dblY ((⇑f : (a : A) → B) ∘ P) = (f : (a : A) → B) ((W'⁄A).dblY P)
have rw₂ : (W'⁄B).dblY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = (W'⁄B).dblY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
Tactic: rw [← RingHom.coe_coe, ← map_dblY, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (W'⁄B).dblXYZ ((⇑f : (a : A) → B) ∘ P) = (⇑f : (a : A) → B) ∘ (W'⁄A).dblXYZ P
have rw : (W'⁄B).dblXYZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = (⇑(↑f : A →+* B) : (a : A) → B) ∘ (W'⁄A).dblXYZ P
Tactic: rw [← RingHom.coe_coe, ← map_dblXYZ, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
rw : (W'⁄B).dblXYZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = (⇑(↑f : A →+* B) : (a : A) → B) ∘ (W'⁄A).dblXYZ P
⊢ (W'⁄B).dblXYZ ((⇑f : (a : A) → B) ∘ P) = (⇑f : (a : A) → B) ∘ (W'⁄A).dblXYZ P
have rw₁ : (W'⁄B).dblXYZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) =
  ((W'⁄A).map (↑f : A →+* B)).dblXYZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
Tactic: rw [← RingHom.coe_coe, ← map_dblXYZ, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
rw : (W'⁄B).dblXYZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = (⇑(↑f : A →+* B) : (a : A) → B) ∘ (W'⁄A).dblXYZ P
rw₁ :
  (W'⁄B).dblXYZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) =
    ((W'⁄A).map (↑f : A →+* B)).dblXYZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
⊢ (W'⁄B).dblXYZ ((⇑f : (a : A) → B) ∘ P) = (⇑f : (a : A) → B) ∘ (W'⁄A).dblXYZ P
have rw₂ : (W'⁄B).dblXYZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = (W'⁄B).dblXYZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
Tactic: rw [← RingHom.coe_coe, ← map_dblXYZ, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P Q : Fin 3 → A
⊢ (W'⁄B).addX ((⇑f : (a : A) → B) ∘ P) ((⇑f : (a : A) → B) ∘ Q) = (f : (a : A) → B) ((W'⁄A).addX P Q)
have rw : (W'⁄B).addX ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
  ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).addX P Q)
Tactic: rw [← RingHom.coe_coe, ← map_addX, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P Q : Fin 3 → A
rw :
  (W'⁄B).addX ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
    ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).addX P Q)
⊢ (W'⁄B).addX ((⇑f : (a : A) → B) ∘ P) ((⇑f : (a : A) → B) ∘ Q) = (f : (a : A) → B) ((W'⁄A).addX P Q)
have rw₁ : (W'⁄B).addX ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
  ((W'⁄A).map (↑f : A →+* B)).addX ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q)
Tactic: rw [← RingHom.coe_coe, ← map_addX, map_baseChange]