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 : 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
⊢ (C • W).j = W.j
have rw₈ : HPow.hPow (β := ℕ) ((↑C.u : R) * (↑C.u⁻¹ : R)) 12 * (↑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]
-- 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
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
⊢ (C • W).j = W.j
have rw₉ : HPow.hPow (α := R) (β := ℕ) 1 12 * (↑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]
-- 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
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
⊢ (C • W).j = W.j
have rw₁₀ : 1 * (↑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]
-- 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
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
⊢ (C • W).j = W.j
have rw₁₁ : (↑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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (hypothesis)
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)
⊢ x = x_1
have 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ˣ)
Tactic: rcases mk.inj h with ⟨h, _, _, _⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (hypothesis)
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ˣ)
⊢ x = x_1
have left : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.r : A) ((φ : (a : R) → A) x_1.r : A)
Tactic: rcases mk.inj h with ⟨h, _, _, _⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (hypothesis)
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)
⊢ x = x_1
have left₁ : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.s : A) ((φ : (a : R) → A) x_1.s : A)
Tactic: rcases mk.inj h with ⟨h, _, _, _⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (hypothesis)
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)
⊢ x = x_1
have right : Eq.{v + 1} (α := A) ((φ : (a : R) → A) x.t : A) ((φ : (a : R) → A) x_1.t : A)
Tactic: rcases mk.inj h with ⟨h, _, _, _⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (hypothesis)
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)
⊢ x = x_1
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
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)
⊢ x = x_1
have u : (↑x.u : R) = (↑x_1.u : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
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)
⊢ x = x_1
have r : x.r = x_1.r
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
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
⊢ x = x_1
have s : x.s = x_1.s
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
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
⊢ x = x_1
have t : x.t = x_1.t
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
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)
⊢ (↑x.u : R) = (↑x_1.u : R)
have u : Eq.{v + 1} (α := A) ((φ : (a : R) → A) (↑x.u : R) : A) ((φ : (a : R) → A) (↑x_1.u : R) : A)
Tactic: apply_fun _ using hφ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst_1 : CommRing A
φ : R →+* A
⊢ map 1 φ = 1
have simp : Eq (α := VariableChange A)
  ({ u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) 1, r := (φ : (a : R) → A) 0,
      s := (φ : (a : R) → A) 0, t := (φ : (a : R) → A) 0 } :
    VariableChange A)
  ({ u := 1, r := 0, s := 0, t := 0 } : VariableChange A)
Tactic: simp only [one_def, map]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst_1 : CommRing A
φ : R →+* A
⊢ Eq (α := VariableChange A)
    ({ u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) 1, r := (φ : (a : R) → A) 0,
        s := (φ : (a : R) → A) 0, t := (φ : (a : R) → A) 0 } :
      VariableChange A)
    ({ u := 1, r := 0, s := 0, t := 0 } : VariableChange A)
have u : Eq (α := A)
  ((↑(u
          { u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) 1, r := (φ : (a : R) → A) 0,
            s := (φ : (a : R) → A) 0, t := (φ : (a : R) → A) 0 }) :
      A) :
    A)
  ((↑(u { u := 1, r := 0, s := 0, t := 0 }) : A) : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst_1 : CommRing A
φ : R →+* A
u :
  Eq (α := A)
    ((↑(VariableChange.u
            { u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) 1, r := (φ : (a : R) → A) 0,
              s := (φ : (a : R) → A) 0, t := (φ : (a : R) → A) 0 }) :
        A) :
      A)
    ((↑(VariableChange.u { u := 1, r := 0, s := 0, t := 0 }) : A) : A)
⊢ Eq (α := VariableChange A)
    ({ u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) 1, r := (φ : (a : R) → A) 0,
        s := (φ : (a : R) → A) 0, t := (φ : (a : R) → A) 0 } :
      VariableChange A)
    ({ u := 1, r := 0, s := 0, t := 0 } : VariableChange A)
have r : Eq (α := A)
  (r
      { u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) 1, r := (φ : (a : R) → A) 0,
        s := (φ : (a : R) → A) 0, t := (φ : (a : R) → A) 0 } :
    A)
  (r { u := 1, r := 0, s := 0, t := 0 } : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst_1 : CommRing A
φ : R →+* A
u :
  Eq (α := A)
    ((↑(VariableChange.u
            { u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) 1, r := (φ : (a : R) → A) 0,
              s := (φ : (a : R) → A) 0, t := (φ : (a : R) → A) 0 }) :
        A) :
      A)
    ((↑(VariableChange.u { u := 1, r := 0, s := 0, t := 0 }) : A) : A)
r :
  Eq (α := A)
    (VariableChange.r
        { u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) 1, r := (φ : (a : R) → A) 0,
          s := (φ : (a : R) → A) 0, t := (φ : (a : R) → A) 0 } :
      A)
    (VariableChange.r { u := 1, r := 0, s := 0, t := 0 } : A)
⊢ Eq (α := VariableChange A)
    ({ u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) 1, r := (φ : (a : R) → A) 0,
        s := (φ : (a : R) → A) 0, t := (φ : (a : R) → A) 0 } :
      VariableChange A)
    ({ u := 1, r := 0, s := 0, t := 0 } : VariableChange A)
have s : Eq (α := A)
  (s
      { u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) 1, r := (φ : (a : R) → A) 0,
        s := (φ : (a : R) → A) 0, t := (φ : (a : R) → A) 0 } :
    A)
  (s { u := 1, r := 0, s := 0, t := 0 } : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst_1 : CommRing A
φ : R →+* A
u :
  Eq (α := A)
    ((↑(VariableChange.u
            { u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) 1, r := (φ : (a : R) → A) 0,
              s := (φ : (a : R) → A) 0, t := (φ : (a : R) → A) 0 }) :
        A) :
      A)
    ((↑(VariableChange.u { u := 1, r := 0, s := 0, t := 0 }) : A) : A)
r :
  Eq (α := A)
    (VariableChange.r
        { u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) 1, r := (φ : (a : R) → A) 0,
          s := (φ : (a : R) → A) 0, t := (φ : (a : R) → A) 0 } :
      A)
    (VariableChange.r { u := 1, r := 0, s := 0, t := 0 } : A)
s :
  Eq (α := A)
    (VariableChange.s
        { u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) 1, r := (φ : (a : R) → A) 0,
          s := (φ : (a : R) → A) 0, t := (φ : (a : R) → A) 0 } :
      A)
    (VariableChange.s { u := 1, r := 0, s := 0, t := 0 } : A)
⊢ Eq (α := VariableChange A)
    ({ u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) 1, r := (φ : (a : R) → A) 0,
        s := (φ : (a : R) → A) 0, t := (φ : (a : R) → A) 0 } :
      VariableChange A)
    ({ u := 1, r := 0, s := 0, t := 0 } : VariableChange A)
have t : Eq (α := A)
  (t
      { u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) 1, r := (φ : (a : R) → A) 0,
        s := (φ : (a : R) → A) 0, t := (φ : (a : R) → A) 0 } :
    A)
  (t { u := 1, r := 0, s := 0, t := 0 } : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C_1 : VariableChange R
A : Type v
inst_1 : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ (C * C').map φ = C.map φ * C'.map φ
have simp : { u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) (C.u * C'.u),
    r := (φ : (a : R) → A) (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r),
    s := (φ : (a : R) → A) ((↑C'.u : R) * C.s + C'.s),
    t :=
      (φ : (a : R) → A)
        (C.t * HPow.hPow (β := ℕ) (↑C'.u : R) 3 + C.r * C'.s * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.t) } =
  {
    u :=
      HMul.hMul (α := Aˣ) (β := Aˣ) (((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C.u : Aˣ)
        (((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u : Aˣ),
    r :=
      HAdd.hAdd (β := A)
        (HMul.hMul (α := A) ((φ : (a : R) → A) C.r : A)
          (HPow.hPow (α := A) (β := ℕ)
            (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) 2))
        ((φ : (a : R) → A) C'.r : A),
    s :=
      HAdd.hAdd (β := A)
        (HMul.hMul (α := A) (β := A)
          ((↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) : A)
          ((φ : (a : R) → A) C.s : A))
        ((φ : (a : R) → A) C'.s : A),
    t :=
      HAdd.hAdd (β := A)
        (HMul.hMul (α := A) ((φ : (a : R) → A) C.t : A)
            (HPow.hPow (α := A) (β := ℕ)
              (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) 3) +
          HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.r : A) ((φ : (a : R) → A) C'.s : A) *
            HPow.hPow (α := A) (β := ℕ)
              (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) 2)
        ((φ : (a : R) → A) C'.t : A) :
    VariableChange A }
Tactic: simp only [mul_def, map]