awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W_1 : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
⊢ { a₁ := 1 * (W.a₁ + HMul.hMul (α := R) 2 (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R })),
        a₂ :=
          HPow.hPow (α := R) (β := ℕ) 1 2 *
            (W.a₂ - VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₁ +
                HMul.hMul (α := R) 3 (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) -
              HPow.hPow (α := R) (β := ℕ) (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2),
        a₃ :=
          HPow.hPow (α := R) (β := ℕ) 1 3 *
            (W.a₃ + VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₁ +
              HMul.hMul (α := R) 2 (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R })),
        a₄ :=
          HPow.hPow (α := R) (β := ℕ) 1 4 *
            (W.a₄ - VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₃ +
                    HMul.hMul (α := R) 2 (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
                      W.a₂ -
                  (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R } +
                      HMul.hMul (α := R) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                        (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R })) *
                    W.a₁ +
                3 *
                  HPow.hPow (α := R) (β := ℕ) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                    2 -
              HMul.hMul (α := R) 2 (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
                VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }),
        a₆ :=
          HPow.hPow (α := R) (β := ℕ) 1 6 *
            (W.a₆ + VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₄ +
                      HPow.hPow (α := R) (β := ℕ)
                          (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2 *
                        W.a₂ +
                    HPow.hPow (α := R) (β := ℕ) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                      3 -
                  VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₃ -
                HPow.hPow (α := R) (β := ℕ) (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2 -
              HMul.hMul (α := R) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                  (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
                W.a₁) :
        WeierstrassCurve R }.a₆ =
    W.a₆
have a₆ : HPow.hPow (α := R) (β := ℕ) 1 6 *
    (W.a₆ + 0 * W.a₄ + HPow.hPow (α := R) (β := ℕ) 0 2 * W.a₂ + HPow.hPow (α := R) (β := ℕ) 0 3 - 0 * W.a₃ -
        HPow.hPow (α := R) (β := ℕ) 0 2 -
      HMul.hMul (α := R) 0 0 * W.a₁) =
  W.a₆
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (C • W).b₂ = HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2 * (W.b₂ + 12 * C.r)
have simp : HPow.hPow (β := ℕ) ((↑C.u⁻¹ : R) * (W.a₁ + 2 * C.s)) 2 +
    4 * (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - HPow.hPow (β := ℕ) C.s 2)) =
  HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2 * (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂ + 12 * C.r)
Tactic: simp only [b₂, variableChange_a₁, variableChange_a₂]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (C • W).b₄ = HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4 * (W.b₄ + C.r * W.b₂ + 6 * HPow.hPow (β := ℕ) C.r 2)
have simp : 2 *
      (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4 *
        (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * HPow.hPow (β := ℕ) C.r 2 -
          2 * C.s * C.t)) +
    (↑C.u⁻¹ : R) * (W.a₁ + 2 * C.s) * (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) =
  HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4 *
    (2 * W.a₄ + W.a₁ * W.a₃ + C.r * (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂) + 6 * HPow.hPow (β := ℕ) C.r 2)
Tactic: simp only [b₂, b₄, variableChange_a₁, variableChange_a₃, variableChange_a₄]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (C • W).b₆ =
    HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 6 *
      (W.b₆ + 2 * C.r * W.b₄ + HPow.hPow (β := ℕ) C.r 2 * W.b₂ + 4 * HPow.hPow (β := ℕ) C.r 3)
have simp : HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) 2 +
    4 *
      (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 6 *
        (W.a₆ + C.r * W.a₄ + HPow.hPow (β := ℕ) C.r 2 * W.a₂ + HPow.hPow (β := ℕ) C.r 3 - C.t * W.a₃ -
            HPow.hPow (β := ℕ) C.t 2 -
          C.r * C.t * W.a₁)) =
  HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 6 *
    (HPow.hPow (β := ℕ) W.a₃ 2 + 4 * W.a₆ + 2 * C.r * (2 * W.a₄ + W.a₁ * W.a₃) +
        HPow.hPow (β := ℕ) C.r 2 * (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂) +
      4 * HPow.hPow (β := ℕ) C.r 3)
Tactic: simp only [b₂, b₄, b₆, variableChange_a₃, variableChange_a₆]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (C • W).b₈ =
    HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 8 *
      (W.b₈ + 3 * C.r * W.b₆ + 3 * HPow.hPow (β := ℕ) C.r 2 * W.b₄ + HPow.hPow (β := ℕ) C.r 3 * W.b₂ +
        3 * HPow.hPow (β := ℕ) C.r 4)
have simp : HPow.hPow (β := ℕ) ((↑C.u⁻¹ : R) * (W.a₁ + 2 * C.s)) 2 *
            (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 6 *
              (W.a₆ + C.r * W.a₄ + HPow.hPow (β := ℕ) C.r 2 * W.a₂ + HPow.hPow (β := ℕ) C.r 3 - C.t * W.a₃ -
                  HPow.hPow (β := ℕ) C.t 2 -
                C.r * C.t * W.a₁)) +
          4 * (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - HPow.hPow (β := ℕ) C.s 2)) *
            (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 6 *
              (W.a₆ + C.r * W.a₄ + HPow.hPow (β := ℕ) C.r 2 * W.a₂ + HPow.hPow (β := ℕ) C.r 3 - C.t * W.a₃ -
                  HPow.hPow (β := ℕ) C.t 2 -
                C.r * C.t * W.a₁)) -
        (↑C.u⁻¹ : R) * (W.a₁ + 2 * C.s) * (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) *
          (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4 *
            (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * HPow.hPow (β := ℕ) C.r 2 -
              2 * C.s * C.t)) +
      HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - HPow.hPow (β := ℕ) C.s 2) *
        HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) 2 -
    HPow.hPow (β := ℕ)
      (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4 *
        (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * HPow.hPow (β := ℕ) C.r 2 - 2 * C.s * C.t))
      2 =
  HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 8 *
    (HPow.hPow (β := ℕ) W.a₁ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * HPow.hPow (β := ℕ) W.a₃ 2 -
              HPow.hPow (β := ℕ) W.a₄ 2 +
            3 * C.r * (HPow.hPow (β := ℕ) W.a₃ 2 + 4 * W.a₆) +
          3 * HPow.hPow (β := ℕ) C.r 2 * (2 * W.a₄ + W.a₁ * W.a₃) +
        HPow.hPow (β := ℕ) C.r 3 * (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂) +
      3 * HPow.hPow (β := ℕ) C.r 4)
Tactic: simp only [b₂, b₄, b₆, b₈, variableChange_a₁, variableChange_a₂, variableChange_a₃,
    variableChange_a₄, variableChange_a₆]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (C • W).c₄ = HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4 * W.c₄
have simp : HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2 * (W.b₂ + 12 * C.r)) 2 -
    24 * (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4 * (W.b₄ + C.r * W.b₂ + 6 * HPow.hPow (β := ℕ) C.r 2)) =
  HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4 * (HPow.hPow (β := ℕ) W.b₂ 2 - 24 * W.b₄)
Tactic: simp only [c₄, variableChange_b₂, variableChange_b₄]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (C • W).c₆ = HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 6 * W.c₆
have simp : -HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2 * (W.b₂ + 12 * C.r)) 3 +
      36 * (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2 * (W.b₂ + 12 * C.r)) *
        (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4 * (W.b₄ + C.r * W.b₂ + 6 * HPow.hPow (β := ℕ) C.r 2)) -
    216 *
      (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 6 *
        (W.b₆ + 2 * C.r * W.b₄ + HPow.hPow (β := ℕ) C.r 2 * W.b₂ + 4 * HPow.hPow (β := ℕ) C.r 3)) =
  HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 6 * (-HPow.hPow (β := ℕ) W.b₂ 3 + 36 * W.b₂ * W.b₄ - 216 * W.b₆)
Tactic: simp only [c₆, variableChange_b₂, variableChange_b₄, variableChange_b₆]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst_1 : W.IsElliptic
⊢ (C • W).IsElliptic
have rw : IsUnit (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 12 * W.Δ)
Tactic: rw [isElliptic_iff, variableChange_Δ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst_1 : W.IsElliptic
⊢ (C • W).Δ' = HPow.hPow (β := ℕ) C.u⁻¹ 12 * W.Δ'
have simp_rw : (↑(C • W).Δ' : R) = (↑(HPow.hPow (β := ℕ) C.u⁻¹ 12 * W.Δ') : R)
Tactic: simp_rw [Units.ext_iff, Units.val_mul, coe_Δ', variableChange_Δ, Units.val_pow_eq_pow_val]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst_1 : W.IsElliptic
simp_rw : (↑(C • W).Δ' : R) = (↑(HPow.hPow (β := ℕ) C.u⁻¹ 12 * W.Δ') : R)
⊢ (C • W).Δ' = HPow.hPow (β := ℕ) C.u⁻¹ 12 * W.Δ'
have simp_rw₁ : (↑(C • W).Δ' : R) = (↑(HPow.hPow (β := ℕ) C.u⁻¹ 12) : R) * (↑W.Δ' : R)
Tactic: simp_rw [Units.ext_iff, Units.val_mul, coe_Δ', variableChange_Δ, Units.val_pow_eq_pow_val]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst_1 : W.IsElliptic
simp_rw : (↑(C • W).Δ' : R) = (↑(HPow.hPow (β := ℕ) C.u⁻¹ 12 * W.Δ') : R)
simp_rw₁ : (↑(C • W).Δ' : R) = (↑(HPow.hPow (β := ℕ) C.u⁻¹ 12) : R) * (↑W.Δ' : R)
⊢ (C • W).Δ' = HPow.hPow (β := ℕ) C.u⁻¹ 12 * W.Δ'
have simp_rw₂ : (C • W).Δ = (↑(HPow.hPow (β := ℕ) C.u⁻¹ 12) : R) * W.Δ
Tactic: simp_rw [Units.ext_iff, Units.val_mul, coe_Δ', variableChange_Δ, Units.val_pow_eq_pow_val]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst_1 : W.IsElliptic
simp_rw : (↑(C • W).Δ' : R) = (↑(HPow.hPow (β := ℕ) C.u⁻¹ 12 * W.Δ') : R)
simp_rw₁ : (↑(C • W).Δ' : R) = (↑(HPow.hPow (β := ℕ) C.u⁻¹ 12) : R) * (↑W.Δ' : R)
simp_rw₂ : (C • W).Δ = (↑(HPow.hPow (β := ℕ) C.u⁻¹ 12) : R) * W.Δ
⊢ (C • W).Δ' = HPow.hPow (β := ℕ) C.u⁻¹ 12 * W.Δ'
have simp_rw₃ : HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 12 * W.Δ = (↑(HPow.hPow (β := ℕ) C.u⁻¹ 12) : R) * W.Δ
Tactic: simp_rw [Units.ext_iff, Units.val_mul, coe_Δ', variableChange_Δ, Units.val_pow_eq_pow_val]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst_1 : W.IsElliptic
⊢ (↑(C • W).Δ' : R) = HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 12 * (↑W.Δ' : R)
have simp_rw : (C • W).Δ = HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 12 * W.Δ
Tactic: simp_rw [coe_Δ', variableChange_Δ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst_1 : W.IsElliptic
⊢ (C • W).Δ'⁻¹ = HPow.hPow (β := ℕ) C.u 12 * W.Δ'⁻¹
have rw : (HPow.hPow (β := ℕ) C.u⁻¹ 12 * W.Δ')⁻¹ = HPow.hPow (β := ℕ) C.u 12 * W.Δ'⁻¹
Tactic: rw [variableChange_Δ', mul_inv, inv_pow, inv_inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst_1 : W.IsElliptic
rw : (HPow.hPow (β := ℕ) C.u⁻¹ 12 * W.Δ')⁻¹ = HPow.hPow (β := ℕ) C.u 12 * W.Δ'⁻¹
⊢ (C • W).Δ'⁻¹ = HPow.hPow (β := ℕ) C.u 12 * W.Δ'⁻¹
have rw₁ : (HPow.hPow (β := ℕ) C.u⁻¹ 12)⁻¹ * W.Δ'⁻¹ = HPow.hPow (β := ℕ) C.u 12 * W.Δ'⁻¹
Tactic: rw [variableChange_Δ', mul_inv, inv_pow, inv_inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst_1 : W.IsElliptic
rw : (HPow.hPow (β := ℕ) C.u⁻¹ 12 * W.Δ')⁻¹ = HPow.hPow (β := ℕ) C.u 12 * W.Δ'⁻¹
rw₁ : (HPow.hPow (β := ℕ) C.u⁻¹ 12)⁻¹ * W.Δ'⁻¹ = HPow.hPow (β := ℕ) C.u 12 * W.Δ'⁻¹
⊢ (C • W).Δ'⁻¹ = HPow.hPow (β := ℕ) C.u 12 * W.Δ'⁻¹
have rw₂ : (HPow.hPow (β := ℕ) C.u 12)⁻¹⁻¹ * W.Δ'⁻¹ = HPow.hPow (β := ℕ) C.u 12 * W.Δ'⁻¹
Tactic: rw [variableChange_Δ', mul_inv, inv_pow, inv_inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst_1 : W.IsElliptic
rw : (HPow.hPow (β := ℕ) C.u⁻¹ 12 * W.Δ')⁻¹ = HPow.hPow (β := ℕ) C.u 12 * W.Δ'⁻¹
rw₁ : (HPow.hPow (β := ℕ) C.u⁻¹ 12)⁻¹ * W.Δ'⁻¹ = HPow.hPow (β := ℕ) C.u 12 * W.Δ'⁻¹
rw₂ : (HPow.hPow (β := ℕ) C.u 12)⁻¹⁻¹ * W.Δ'⁻¹ = HPow.hPow (β := ℕ) C.u 12 * W.Δ'⁻¹
⊢ (C • W).Δ'⁻¹ = HPow.hPow (β := ℕ) C.u 12 * W.Δ'⁻¹
have rw₃ : HPow.hPow (β := ℕ) C.u 12 * W.Δ'⁻¹ = HPow.hPow (β := ℕ) C.u 12 * W.Δ'⁻¹
Tactic: rw [variableChange_Δ', mul_inv, inv_pow, inv_inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst_1 : W.IsElliptic
⊢ (↑(C • W).Δ'⁻¹ : R) = HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R)
have rw : (↑(HPow.hPow (β := ℕ) C.u 12 * W.Δ'⁻¹) : R) = HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R)
Tactic: rw [inv_variableChange_Δ', Units.val_mul, Units.val_pow_eq_pow_val]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst_1 : W.IsElliptic
rw : (↑(HPow.hPow (β := ℕ) C.u 12 * W.Δ'⁻¹) : R) = HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R)
⊢ (↑(C • W).Δ'⁻¹ : R) = HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R)
have rw₁ : (↑(HPow.hPow (β := ℕ) C.u 12) : R) * (↑W.Δ'⁻¹ : R) = HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R)
Tactic: rw [inv_variableChange_Δ', Units.val_mul, Units.val_pow_eq_pow_val]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst_1 : W.IsElliptic
rw : (↑(HPow.hPow (β := ℕ) C.u 12 * W.Δ'⁻¹) : R) = HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R)
rw₁ : (↑(HPow.hPow (β := ℕ) C.u 12) : R) * (↑W.Δ'⁻¹ : R) = HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R)
⊢ (↑(C • W).Δ'⁻¹ : R) = HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R)
have rw₂ : HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R) = HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R)
Tactic: rw [inv_variableChange_Δ', Units.val_mul, Units.val_pow_eq_pow_val]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst_1 : W.IsElliptic
⊢ (C • W).j = W.j
have rw : (↑(C • W).Δ'⁻¹ : R) * HPow.hPow (β := ℕ) (C • W).c₄ 3 = W.j
Tactic: rw [j, coe_inv_variableChange_Δ', variableChange_c₄, j, mul_pow, ← pow_mul, ← mul_assoc,
    mul_right_comm (C.u.val ^ 12), ← mul_pow, C.u.mul_inv, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst_1 : W.IsElliptic
rw : (↑(C • W).Δ'⁻¹ : R) * HPow.hPow (β := ℕ) (C • W).c₄ 3 = W.j
⊢ (C • W).j = W.j
have rw₁ : HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) (C • W).c₄ 3 = W.j
Tactic: rw [j, coe_inv_variableChange_Δ', variableChange_c₄, j, mul_pow, ← pow_mul, ← mul_assoc,
    mul_right_comm (C.u.val ^ 12), ← mul_pow, C.u.mul_inv, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst_1 : W.IsElliptic
rw : (↑(C • W).Δ'⁻¹ : R) * HPow.hPow (β := ℕ) (C • W).c₄ 3 = W.j
rw₁ : HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) (C • W).c₄ 3 = W.j
⊢ (C • W).j = W.j
have rw₂ : HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4 * W.c₄) 3 = W.j
Tactic: rw [j, coe_inv_variableChange_Δ', variableChange_c₄, j, mul_pow, ← pow_mul, ← mul_assoc,
    mul_right_comm (C.u.val ^ 12), ← mul_pow, C.u.mul_inv, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst_1 : W.IsElliptic
rw : (↑(C • W).Δ'⁻¹ : R) * HPow.hPow (β := ℕ) (C • W).c₄ 3 = W.j
rw₁ : HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) (C • W).c₄ 3 = W.j
rw₂ :
  HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4 * W.c₄) 3 =
    W.j
⊢ (C • W).j = W.j
have rw₃ : HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4 * W.c₄) 3 =
  (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3
Tactic: rw [j, coe_inv_variableChange_Δ', variableChange_c₄, j, mul_pow, ← pow_mul, ← mul_assoc,
    mul_right_comm (C.u.val ^ 12), ← mul_pow, C.u.mul_inv, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst_1 : W.IsElliptic
rw : (↑(C • W).Δ'⁻¹ : R) * HPow.hPow (β := ℕ) (C • W).c₄ 3 = W.j
rw₁ : HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) (C • W).c₄ 3 = W.j
rw₂ :
  HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4 * W.c₄) 3 =
    W.j
rw₃ :
  HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4 * W.c₄) 3 =
    (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3
⊢ (C • W).j = W.j
have rw₄ : HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R) *
    (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4) 3 * HPow.hPow (β := ℕ) W.c₄ 3) =
  (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3
Tactic: rw [j, coe_inv_variableChange_Δ', variableChange_c₄, j, mul_pow, ← pow_mul, ← mul_assoc,
    mul_right_comm (C.u.val ^ 12), ← mul_pow, C.u.mul_inv, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst_1 : W.IsElliptic
rw : (↑(C • W).Δ'⁻¹ : R) * HPow.hPow (β := ℕ) (C • W).c₄ 3 = W.j
rw₁ : HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) (C • W).c₄ 3 = W.j
rw₂ :
  HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4 * W.c₄) 3 =
    W.j
rw₃ :
  HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4 * W.c₄) 3 =
    (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3
rw₄ :
  HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R) *
      (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4) 3 * HPow.hPow (β := ℕ) W.c₄ 3) =
    (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3
⊢ (C • W).j = W.j
have rw₅ : HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R) * ((↑C.u⁻¹ : R) ^ HMul.hMul (α := ℕ) 4 3 * HPow.hPow (β := ℕ) W.c₄ 3) =
  (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3
Tactic: rw [j, coe_inv_variableChange_Δ', variableChange_c₄, j, mul_pow, ← pow_mul, ← mul_assoc,
    mul_right_comm (C.u.val ^ 12), ← mul_pow, C.u.mul_inv, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst_1 : W.IsElliptic
rw : (↑(C • W).Δ'⁻¹ : R) * HPow.hPow (β := ℕ) (C • W).c₄ 3 = W.j
rw₁ : HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) (C • W).c₄ 3 = W.j
rw₂ :
  HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4 * W.c₄) 3 =
    W.j
rw₃ :
  HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4 * W.c₄) 3 =
    (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3
rw₄ :
  HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R) *
      (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4) 3 * HPow.hPow (β := ℕ) W.c₄ 3) =
    (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3
rw₅ :
  HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R) *
      ((↑C.u⁻¹ : R) ^ HMul.hMul (α := ℕ) 4 3 * HPow.hPow (β := ℕ) W.c₄ 3) =
    (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3
⊢ (C • W).j = W.j
have rw₆ : HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R) * (↑C.u⁻¹ : R) ^ HMul.hMul (α := ℕ) 4 3 * HPow.hPow (β := ℕ) W.c₄ 3 =
  (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3
Tactic: rw [j, coe_inv_variableChange_Δ', variableChange_c₄, j, mul_pow, ← pow_mul, ← mul_assoc,
    mul_right_comm (C.u.val ^ 12), ← mul_pow, C.u.mul_inv, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst_1 : W.IsElliptic
rw : (↑(C • W).Δ'⁻¹ : R) * HPow.hPow (β := ℕ) (C • W).c₄ 3 = W.j
rw₁ : HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) (C • W).c₄ 3 = W.j
rw₂ :
  HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4 * W.c₄) 3 =
    W.j
rw₃ :
  HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4 * W.c₄) 3 =
    (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3
rw₄ :
  HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R) *
      (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4) 3 * HPow.hPow (β := ℕ) W.c₄ 3) =
    (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3
rw₅ :
  HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R) *
      ((↑C.u⁻¹ : R) ^ HMul.hMul (α := ℕ) 4 3 * HPow.hPow (β := ℕ) W.c₄ 3) =
    (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3
rw₆ :
  HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R) * (↑C.u⁻¹ : R) ^ HMul.hMul (α := ℕ) 4 3 * HPow.hPow (β := ℕ) W.c₄ 3 =
    (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3
⊢ (C • W).j = W.j
have rw₇ : HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑C.u⁻¹ : R) ^ HMul.hMul (α := ℕ) 4 3 * (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3 =
  (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3
Tactic: rw [j, coe_inv_variableChange_Δ', variableChange_c₄, j, mul_pow, ← pow_mul, ← mul_assoc,
    mul_right_comm (C.u.val ^ 12), ← mul_pow, C.u.mul_inv, one_pow, one_mul]