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