awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
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)
⊢ (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)

Tactic:
simp only [b₂, b₄, b₆, variableChange_a₃, variableChange_a₆]

Premises used: WeierstrassCurve.b₂, WeierstrassCurve.b₄, WeierstrassCurve.variableChange_a₃, WeierstrassCurve.variableChange_a₆, WeierstrassCurve.b₆
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ 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:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
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)
⊢ (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)

Tactic:
simp only [b₂, b₄, b₆, b₈, variableChange_a₁, variableChange_a₂, variableChange_a₃,
    variableChange_a₄, variableChange_a₆]

Premises used: WeierstrassCurve.variableChange_a₁, WeierstrassCurve.b₂, WeierstrassCurve.b₄, WeierstrassCurve.variableChange_a₂, WeierstrassCurve.variableChange_a₃, WeierstrassCurve.b₈, WeierstrassCurve.variableChange_a₄, WeierstrassCurve.variableChange_a₆, WeierstrassCurve.b₆
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ 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:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
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₄)
⊢ (C • W).c₄ = HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4 * W.c₄

Tactic:
simp only [c₄, variableChange_b₂, variableChange_b₄]

Premises used: WeierstrassCurve.variableChange_b₂, WeierstrassCurve.c₄, WeierstrassCurve.variableChange_b₄
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ 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:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
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₆)
⊢ (C • W).c₆ = HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 6 * W.c₆

Tactic:
simp only [c₆, variableChange_b₂, variableChange_b₄, variableChange_b₆]

Premises used: WeierstrassCurve.variableChange_b₂, WeierstrassCurve.variableChange_b₆, WeierstrassCurve.c₆, WeierstrassCurve.variableChange_b₄
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ -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:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst_1 : W.IsElliptic
rw : IsUnit (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 12 * W.Δ)
⊢ (C • W).IsElliptic

Tactic:
rw [isElliptic_iff, variableChange_Δ]

Premises used: WeierstrassCurve.variableChange_Δ, WeierstrassCurve.isElliptic_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst_1 : W.IsElliptic
⊢ IsUnit (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 12 * W.Δ)

Tactic:
(C.u⁻¹.isUnit.pow 12).mul W.isUnit_Δ

Premises used: WeierstrassCurve.VariableChange.u, IsUnit.mul, IsUnit.pow, Inv.inv, WeierstrassCurve.isUnit_Δ, Units.isUnit, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst_1 : W.IsElliptic
⊢ IsUnit (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 12 * W.Δ)

Tactic:
exact (C.u⁻¹.isUnit.pow 12).mul W.isUnit_Δ

Premises used: WeierstrassCurve.VariableChange.u, IsUnit.mul, IsUnit.pow, Inv.inv, WeierstrassCurve.isUnit_Δ, Units.isUnit, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
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.Δ
simp_rw₃ : HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 12 * W.Δ = (↑(HPow.hPow (β := ℕ) C.u⁻¹ 12) : R) * W.Δ
⊢ (C • W).Δ' = HPow.hPow (β := ℕ) C.u⁻¹ 12 * W.Δ'

Tactic:
simp_rw [Units.ext_iff, Units.val_mul, coe_Δ', variableChange_Δ, Units.val_pow_eq_pow_val]

Premises used: Units.ext_iff, WeierstrassCurve.variableChange_Δ, WeierstrassCurve.coe_Δ', Units.val_pow_eq_pow_val, Units.val_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst_1 : W.IsElliptic
simp_rw : (C • W).Δ = HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 12 * W.Δ
⊢ (↑(C • W).Δ' : R) = HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 12 * (↑W.Δ' : R)

Tactic:
simp_rw [coe_Δ', variableChange_Δ]

Premises used: WeierstrassCurve.variableChange_Δ, WeierstrassCurve.coe_Δ'
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
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.Δ'⁻¹
rw₃ rw₄ : HPow.hPow (β := ℕ) C.u 12 * W.Δ'⁻¹ = HPow.hPow (β := ℕ) C.u 12 * W.Δ'⁻¹
⊢ (C • W).Δ'⁻¹ = HPow.hPow (β := ℕ) C.u 12 * W.Δ'⁻¹

Tactic:
rw [variableChange_Δ', mul_inv, inv_pow, inv_inv]

Premises used: WeierstrassCurve.variableChange_Δ', mul_inv, inv_pow, inv_inv
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
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)
rw₂ rw₃ : HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R) = HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R)
⊢ (↑(C • W).Δ'⁻¹ : R) = HPow.hPow (β := ℕ) (↑C.u : R) 12 * (↑W.Δ'⁻¹ : R)

Tactic:
rw [inv_variableChange_Δ', Units.val_mul, Units.val_pow_eq_pow_val]

Premises used: WeierstrassCurve.inv_variableChange_Δ', Units.val_pow_eq_pow_val, Units.val_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
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
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
rw₈ :
  HPow.hPow (β := ℕ) ((↑C.u : R) * (↑C.u⁻¹ : R)) 12 * (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3 =
    (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3
rw₉ :
  HPow.hPow (α := R) (β := ℕ) 1 12 * (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3 =
    (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3
rw₁₀ : 1 * (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3 = (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3
rw₁₁ rw₁₂ : (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3 = (↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3
⊢ (C • W).j = 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]

Premises used: one_pow, Units.val, WeierstrassCurve.j, mul_assoc, WeierstrassCurve.VariableChange.u, Units.mul_inv, pow_mul, WeierstrassCurve.coe_inv_variableChange_Δ', HPow.hPow, mul_right_comm, OfNat.ofNat, mul_pow, WeierstrassCurve.variableChange_c₄, one_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
C : VariableChange R
⊢ C.map (RingHom.id R) = C

Tactic:
rfl

Premises used: WeierstrassCurve.VariableChange.map, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
C : VariableChange R
A : Type v
inst_1 : CommRing A
φ : R →+* A
B : Type w
inst_2 : CommRing B
ψ : A →+* B
⊢ (C.map φ).map ψ = C.map (ψ.comp φ)

Tactic:
rfl

Premises used: WeierstrassCurve.VariableChange.map, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
C : VariableChange R
S : Type s
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type v
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type w
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
ψ : A →ₐ[S] B
⊢ Eq (α := VariableChange B) (map C⁄A (↑ψ : A →+* B)) C⁄B

Tactic:
congr_arg C.map <| ψ.comp_algebraMap_of_tower R

Premises used: AlgHom.comp_algebraMap_of_tower, congr_arg, WeierstrassCurve.VariableChange.map, WeierstrassCurve.VariableChange.baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
φ : R →+* A
hφ : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑φ : (a : R) → A)
x x_1 : VariableChange R
h :
  Eq.{v + 1} (α := VariableChange A) ((fun (C : VariableChange R) ↦ C.map φ) x)
    ((fun (C : VariableChange R) ↦ C.map φ) x_1)
⊢ Eq.{v + 1} (α := Aˣ) (((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) x.u : Aˣ)
    (((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) x_1.u : Aˣ)

Tactic:
rcases mk.inj h with ⟨h, _, _, _⟩

Premises used: WeierstrassCurve.VariableChange.mk.inj
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
φ : R →+* A
hφ : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑φ : (a : R) → A)
x x_1 : VariableChange R
h :
  Eq.{v + 1} (α := VariableChange A) ((fun (C : VariableChange R) ↦ C.map φ) x)
    ((fun (C : VariableChange R) ↦ C.map φ) x_1)
h₁ :
  Eq.{v + 1} (α := Aˣ) (((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) x.u : Aˣ)
    (((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) x_1.u : Aˣ)
⊢ Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.r : A) ((φ : (a : R) → A) x_1.r : A)

Tactic:
rcases mk.inj h with ⟨h, _, _, _⟩

Premises used: WeierstrassCurve.VariableChange.mk.inj
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
φ : R →+* A
hφ : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑φ : (a : R) → A)
x x_1 : VariableChange R
h :
  Eq.{v + 1} (α := VariableChange A) ((fun (C : VariableChange R) ↦ C.map φ) x)
    ((fun (C : VariableChange R) ↦ C.map φ) x_1)
h₁ :
  Eq.{v + 1} (α := Aˣ) (((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) x.u : Aˣ)
    (((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) x_1.u : Aˣ)
left : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.r : A) ((φ : (a : R) → A) x_1.r : A)
⊢ Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.s : A) ((φ : (a : R) → A) x_1.s : A)

Tactic:
rcases mk.inj h with ⟨h, _, _, _⟩

Premises used: WeierstrassCurve.VariableChange.mk.inj
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
φ : R →+* A
hφ : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑φ : (a : R) → A)
x x_1 : VariableChange R
h :
  Eq.{v + 1} (α := VariableChange A) ((fun (C : VariableChange R) ↦ C.map φ) x)
    ((fun (C : VariableChange R) ↦ C.map φ) x_1)
h₁ :
  Eq.{v + 1} (α := Aˣ) (((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) x.u : Aˣ)
    (((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) x_1.u : Aˣ)
left : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.r : A) ((φ : (a : R) → A) x_1.r : A)
left₁ : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.s : A) ((φ : (a : R) → A) x_1.s : A)
⊢ Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.t : A) ((φ : (a : R) → A) x_1.t : A)

Tactic:
rcases mk.inj h with ⟨h, _, _, _⟩

Premises used: WeierstrassCurve.VariableChange.mk.inj
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
φ : R →+* A
hφ : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑φ : (a : R) → A)
x x_1 : VariableChange R
h_1 :
  Eq.{v + 1} (α := VariableChange A) ((fun (C : VariableChange R) ↦ C.map φ) x)
    ((fun (C : VariableChange R) ↦ C.map φ) x_1)
h :
  Eq.{v + 1} (α := Aˣ) (((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) x.u : Aˣ)
    (((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) x_1.u : Aˣ)
left : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.r : A) ((φ : (a : R) → A) x_1.r : A)
left_1 : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.s : A) ((φ : (a : R) → A) x_1.s : A)
right : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.t : A) ((φ : (a : R) → A) x_1.t : A)
⊢ Eq.{v + 1} (α := A) (((↑φ : R →* A) : (a : R) → A) (↑x.u : R) : A) (((↑φ : R →* A) : (a : R) → A) (↑x_1.u : R) : A)

Tactic:
replace h := (Units.mk.inj h).left
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
φ : R →+* A
hφ : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑φ : (a : R) → A)
x x_1 : VariableChange R
h_1 :
  Eq.{v + 1} (α := VariableChange A) ((fun (C : VariableChange R) ↦ C.map φ) x)
    ((fun (C : VariableChange R) ↦ C.map φ) x_1)
left : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.r : A) ((φ : (a : R) → A) x_1.r : A)
left_1 : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.s : A) ((φ : (a : R) → A) x_1.s : A)
right : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.t : A) ((φ : (a : R) → A) x_1.t : A)
h : Eq.{v + 1} (α := A) (((↑φ : R →* A) : (a : R) → A) (↑x.u : R) : A) (((↑φ : R →* A) : (a : R) → A) (↑x_1.u : R) : A)
u : (↑x.u : R) = (↑x_1.u : R)
r : x.r = x_1.r
s : x.s = x_1.s
t : x.t = x_1.t
⊢ x = x_1

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
φ : R →+* A
hφ : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑φ : (a : R) → A)
x x_1 : VariableChange R
h_1 :
  Eq.{v + 1} (α := VariableChange A) ((fun (C : VariableChange R) ↦ C.map φ) x)
    ((fun (C : VariableChange R) ↦ C.map φ) x_1)
left : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.r : A) ((φ : (a : R) → A) x_1.r : A)
left_1 : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.s : A) ((φ : (a : R) → A) x_1.s : A)
right : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.t : A) ((φ : (a : R) → A) x_1.t : A)
h : Eq.{v + 1} (α := A) (((↑φ : R →* A) : (a : R) → A) (↑x.u : R) : A) (((↑φ : R →* A) : (a : R) → A) (↑x_1.u : R) : A)
⊢ Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑φ : (a : R) → A)

Tactic:
hφ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
φ : R →+* A
hφ : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑φ : (a : R) → A)
x x_1 : VariableChange R
h_1 :
  Eq.{v + 1} (α := VariableChange A) ((fun (C : VariableChange R) ↦ C.map φ) x)
    ((fun (C : VariableChange R) ↦ C.map φ) x_1)
left : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.r : A) ((φ : (a : R) → A) x_1.r : A)
left_1 : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.s : A) ((φ : (a : R) → A) x_1.s : A)
right : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.t : A) ((φ : (a : R) → A) x_1.t : A)
h : Eq.{v + 1} (α := A) (((↑φ : R →* A) : (a : R) → A) (↑x.u : R) : A) (((↑φ : R →* A) : (a : R) → A) (↑x_1.u : R) : A)
u : Eq.{v + 1} (α := A) ((φ : (a : R) → A) (↑x.u : R) : A) ((φ : (a : R) → A) (↑x_1.u : R) : A)
⊢ (↑x.u : R) = (↑x_1.u : R)

Tactic:
apply_fun _ using hφ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
φ : R →+* A
hφ : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑φ : (a : R) → A)
x x_1 : VariableChange R
h_1 :
  Eq.{v + 1} (α := VariableChange A) ((fun (C : VariableChange R) ↦ C.map φ) x)
    ((fun (C : VariableChange R) ↦ C.map φ) x_1)
left : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.r : A) ((φ : (a : R) → A) x_1.r : A)
left_1 : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.s : A) ((φ : (a : R) → A) x_1.s : A)
right : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.t : A) ((φ : (a : R) → A) x_1.t : A)
h : Eq.{v + 1} (α := A) (((↑φ : R →* A) : (a : R) → A) (↑x.u : R) : A) (((↑φ : R →* A) : (a : R) → A) (↑x_1.u : R) : A)
r : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.r : A) ((φ : (a : R) → A) x_1.r : A)
⊢ x.r = x_1.r

Tactic:
apply_fun _ using hφ