awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun (a : K) ↦ (valuation R K : (a : K) → ValueGroup R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos (l := l) ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax
ha₀ : a ≠ 0
⊢ lmax ≤ HPow.hPow (β := ℕ) lmax 6
have h : Ne (α := ℕ) 6 0
Tactic: apply le_self_pow hlmax_ge_1.le
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun (a : K) ↦ (valuation R K : (a : K) → ValueGroup R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos (l := l) ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax
ha₀ : a ≠ 0
⊢ Ne (α := ℕ) 6 0
have linarith : Eq (α := ℕ) 6 0 → HMul.hMul (α := ℤ) 6 (-1) + HSub.hSub (α := ℤ) 6 0 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun (a : K) ↦ (valuation R K : (a : K) → ValueGroup R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos (l := l) ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax
ha₀ : a ≠ 0
linarith : Eq (α := ℕ) 6 0 → HMul.hMul (α := ℤ) 6 (-1) + HSub.hSub (α := ℤ) 6 0 = 0
⊢ Ne (α := ℕ) 6 0
have linarith₁ : Eq (α := ℕ) 6 0 → GT.gt (α := ℤ) 6 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
h : IsIntegral R W
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        W.Δ :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
have choose : ∀ (r : R) (hr : (algebraMap R K : (a : R) → K) r = W.Δ),
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        W.Δ :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
Tactic: choose r hr using Δ_integral_of_isIntegral R W
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
h : IsIntegral R W
r : R
hr : (algebraMap R K : (a : R) → K) r = W.Δ
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        W.Δ :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
have rw : LE.le (α := WithZero (Multiplicative ℤ))
  (((valuation K (maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
      ((algebraMap R K : (a : R) → K) r) :
    WithZero (Multiplicative ℤ))
  (1 : WithZero (Multiplicative ℤ))
Tactic: rw [← hr]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
⊢ ∃ (C : VariableChange K), IsMinimal R (C • W)
have obtain : ∀ (C : VariableChange K)
  (hC :
    MaximalFor (α := { v : WithZero (Multiplicative ℤ) // v ≤ 1 }) (fun (C : VariableChange K) ↦ IsIntegral R (C • W))
      (fun (C : VariableChange K) ↦ valuation_Δ_aux R (C • W)) C),
  ∃ (C : VariableChange K), IsMinimal R (C • W)
Tactic: obtain ⟨C, hC⟩ := exists_maximalFor_of_wellFoundedGT
    (fun (C : VariableChange K) ↦ IsIntegral R (C • W))
    (fun (C : VariableChange K) ↦ valuation_Δ_aux R (C • W))
    (exists_isIntegral R W)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
C : VariableChange K
hC :
  MaximalFor (α := { v : WithZero (Multiplicative ℤ) // v ≤ 1 }) (fun (C : VariableChange K) ↦ IsIntegral R (C • W))
    (fun (C : VariableChange K) ↦ valuation_Δ_aux R (C • W)) C
⊢ ∃ (C : VariableChange K), IsMinimal R (C • W)
have refine : ∀ ⦃j : VariableChange K⦄,
  (fun (C_1 : VariableChange K) ↦ IsIntegral R (C_1 • C • W)) j →
    LE.le (α := { v : WithZero (Multiplicative ℤ) // v ≤ 1 })
        ((fun (C_1 : VariableChange K) ↦ valuation_Δ_aux R (C_1 • C • W)) 1)
        ((fun (C_1 : VariableChange K) ↦ valuation_Δ_aux R (C_1 • C • W)) j) →
      LE.le (α := { v : WithZero (Multiplicative ℤ) // v ≤ 1 })
        ((fun (C_1 : VariableChange K) ↦ valuation_Δ_aux R (C_1 • C • W)) j)
        ((fun (C_1 : VariableChange K) ↦ valuation_Δ_aux R (C_1 • C • W)) 1)
Tactic: refine ⟨C, ⟨⟨by simp only [one_smul, hC.1], ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
C : VariableChange K
hC :
  MaximalFor (α := { v : WithZero (Multiplicative ℤ) // v ≤ 1 }) (fun (C : VariableChange K) ↦ IsIntegral R (C • W))
    (fun (C : VariableChange K) ↦ valuation_Δ_aux R (C • W)) C
j : VariableChange K
hj : IsIntegral R (j • C • W)
⊢ LE.le (α := { v : WithZero (Multiplicative ℤ) // v ≤ 1 })
      ((fun (C_1 : VariableChange K) ↦ valuation_Δ_aux R (C_1 • C • W)) 1)
      ((fun (C_1 : VariableChange K) ↦ valuation_Δ_aux R (C_1 • C • W)) j) →
    LE.le (α := { v : WithZero (Multiplicative ℤ) // v ≤ 1 })
      ((fun (C_1 : VariableChange K) ↦ valuation_Δ_aux R (C_1 • C • W)) j)
      ((fun (C_1 : VariableChange K) ↦ valuation_Δ_aux R (C_1 • C • W)) 1)
have hj₁ : IsIntegral R ((j • C) • W)
Tactic: rw [← smul_assoc] at hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
C : VariableChange K
hC :
  MaximalFor (α := { v : WithZero (Multiplicative ℤ) // v ≤ 1 }) (fun (C : VariableChange K) ↦ IsIntegral R (C • W))
    (fun (C : VariableChange K) ↦ valuation_Δ_aux R (C • W)) C
j : VariableChange K
hj : IsIntegral R ((j • C) • W)
h : LE.le (α := { v : WithZero (Multiplicative ℤ) // v ≤ 1 })
    ((fun (C : VariableChange K) ↦ valuation_Δ_aux R (C • W)) C)
    ((fun (C : VariableChange K) ↦ valuation_Δ_aux R (C • W)) (j • C)) →
  LE.le (α := { v : WithZero (Multiplicative ℤ) // v ≤ 1 })
    ((fun (C : VariableChange K) ↦ valuation_Δ_aux R (C • W)) (j • C))
    ((fun (C : VariableChange K) ↦ valuation_Δ_aux R (C • W)) C) :=
  ⋯
⊢ LE.le (α := { v : WithZero (Multiplicative ℤ) // v ≤ 1 })
      ((fun (C_1 : VariableChange K) ↦ valuation_Δ_aux R (C_1 • C • W)) 1)
      ((fun (C_1 : VariableChange K) ↦ valuation_Δ_aux R (C_1 • C • W)) j) →
    LE.le (α := { v : WithZero (Multiplicative ℤ) // v ≤ 1 })
      ((fun (C_1 : VariableChange K) ↦ valuation_Δ_aux R (C_1 • C • W)) j)
      ((fun (C_1 : VariableChange K) ↦ valuation_Δ_aux R (C_1 • C • W)) 1)
have simp_all : valuation_Δ_aux R (C • W) ≤ valuation_Δ_aux R (j • C • W) → valuation_Δ_aux R (j • C • W) ≤ valuation_Δ_aux R (C • W)
Tactic: simp_all only [one_smul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
hW : IsMinimal R W
⊢ HasGoodReduction R W ↔
    WeierstrassCurve.IsElliptic (R := ResidueField R) (reduction R W : WeierstrassCurve (ResidueField R))
have refine : HasGoodReduction R W ↔ IsUnit (M := ResidueField R) (Δ (reduction R W) : ResidueField R)
Tactic: refine Iff.trans ?_ (W.reduction R).isElliptic_iff.symm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
hW : IsMinimal R W
⊢ HasGoodReduction R W ↔ IsUnit (M := ResidueField R) (Δ (reduction R W) : ResidueField R)
have simp : HasGoodReduction R W ↔ (integralModel R W).Δ ∉ IsLocalRing.maximalIdeal R
Tactic: simp only [reduction, map_Δ, isUnit_iff_ne_zero, ne_eq, residue_eq_zero_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
hW : IsMinimal R W
⊢ HasGoodReduction R W ↔ (integralModel R W).Δ ∉ IsLocalRing.maximalIdeal R
have h : ¬LT.lt (α := WithZero (Multiplicative ℤ))
      (((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
            (a : K) → WithZero (Multiplicative ℤ))
          ((algebraMap R K : (a : R) → K) (integralModel R W).Δ) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)) ↔
  (integralModel R W).Δ ∉ IsLocalRing.maximalIdeal R
Tactic: have h :
      ¬(valuation K (maximalIdeal R) (algebraMap R K (integralModel R W).Δ) < 1)
      ↔ (integralModel R W).Δ ∉ IsLocalRing.maximalIdeal R :=
    not_iff_not.mpr <| valuation_lt_one_iff_mem _ _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
hW : IsMinimal R W
h :
  ¬LT.lt (α := WithZero (Multiplicative ℤ))
        (((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
              (a : K) → WithZero (Multiplicative ℤ))
            ((algebraMap R K : (a : R) → K) (integralModel R W).Δ) :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ)) ↔
    (integralModel R W).Δ ∉ IsLocalRing.maximalIdeal R
⊢ HasGoodReduction R W ↔ (integralModel R W).Δ ∉ IsLocalRing.maximalIdeal R
have refine : IsMinimal R W ∧
    Eq (α := WithZero (Multiplicative ℤ))
      (((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
            (a : K) → WithZero (Multiplicative ℤ))
          ((algebraMap R K : (a : R) → K) (integralModel R W).Δ) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)) ↔
  ¬LT.lt (α := WithZero (Multiplicative ℤ))
      (((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
            (a : K) → WithZero (Multiplicative ℤ))
          ((algebraMap R K : (a : R) → K) (integralModel R W).Δ) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
Tactic: refine ((integralModel_Δ_eq R W ▸ hasGoodReduction_iff _ _).trans ?_).trans h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
inst_6 : IsMinimal R W
⊢ HasGoodReduction R W ∨ HasMultiplicativeReduction R W ∨ HasAdditiveReduction R W
have rw : IsMinimal R W ∧
    Eq (α := WithZero (Multiplicative ℤ))
      (((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
            (a : K) → WithZero (Multiplicative ℤ))
          ((algebraMap R K : (a : R) → K) (integralModel R W).Δ) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)) ∨
  IsMinimal R W ∧
      LT.lt (α := WithZero (Multiplicative ℤ))
          (((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
                (a : K) → WithZero (Multiplicative ℤ))
              ((algebraMap R K : (a : R) → K) (integralModel R W).Δ) :
            WithZero (Multiplicative ℤ))
          (1 : WithZero (Multiplicative ℤ)) ∧
        Eq (α := WithZero (Multiplicative ℤ))
          (((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
                (a : K) → WithZero (Multiplicative ℤ))
              ((algebraMap R K : (a : R) → K) (integralModel R W).c₄) :
            WithZero (Multiplicative ℤ))
          (1 : WithZero (Multiplicative ℤ)) ∨
    IsMinimal R W ∧
      LT.lt (α := WithZero (Multiplicative ℤ))
          (((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
                (a : K) → WithZero (Multiplicative ℤ))
              ((algebraMap R K : (a : R) → K) (integralModel R W).Δ) :
            WithZero (Multiplicative ℤ))
          (1 : WithZero (Multiplicative ℤ)) ∧
        LT.lt (α := WithZero (Multiplicative ℤ))
          (((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
                (a : K) → WithZero (Multiplicative ℤ))
              ((algebraMap R K : (a : R) → K) (integralModel R W).c₄) :
            WithZero (Multiplicative ℤ))
          (1 : WithZero (Multiplicative ℤ))
Tactic: rw [hasGoodReduction_iff, hasMultiplicativeReduction_iff, hasAdditiveReduction_iff,
    ← integralModel_Δ_eq R W, ← integralModel_c₄_eq R W]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C C' x x_1 x_2 : VariableChange R
⊢ x * x_1 * x_2 = x * (x_1 * x_2)
have u : (↑(x * x_1 * x_2).u : R) = (↑(x * (x_1 * x_2)).u : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C C' x x_1 x_2 : VariableChange R
u : (↑(x * x_1 * x_2).u : R) = (↑(x * (x_1 * x_2)).u : R)
⊢ x * x_1 * x_2 = x * (x_1 * x_2)
have r : (x * x_1 * x_2).r = (x * (x_1 * x_2)).r
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C C' x x_1 x_2 : VariableChange R
u : (↑(x * x_1 * x_2).u : R) = (↑(x * (x_1 * x_2)).u : R)
r : (x * x_1 * x_2).r = (x * (x_1 * x_2)).r
⊢ x * x_1 * x_2 = x * (x_1 * x_2)
have s : (x * x_1 * x_2).s = (x * (x_1 * x_2)).s
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C C' x x_1 x_2 : VariableChange R
u : (↑(x * x_1 * x_2).u : R) = (↑(x * (x_1 * x_2)).u : R)
r : (x * x_1 * x_2).r = (x * (x_1 * x_2)).r
s : (x * x_1 * x_2).s = (x * (x_1 * x_2)).s
⊢ x * x_1 * x_2 = x * (x_1 * x_2)
have t : (x * x_1 * x_2).t = (x * (x_1 * x_2)).t
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C C' x x_1 x_2 : VariableChange R
⊢ (↑(x * x_1 * x_2).u : R) = (↑(x * (x_1 * x_2)).u : R)
have u : (↑x.u : R) * (↑x_1.u : R) * (↑x_2.u : R) = (↑x.u : R) * ((↑x_1.u : R) * (↑x_2.u : R))
Tactic: simp only [mul_def, Units.val_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C C' x x_1 x_2 : VariableChange R
⊢ (x * x_1 * x_2).r = (x * (x_1 * x_2)).r
have r : (x.r * HPow.hPow (β := ℕ) (↑x_1.u : R) 2 + x_1.r) * HPow.hPow (β := ℕ) (↑x_2.u : R) 2 + x_2.r =
  x.r * HPow.hPow (β := ℕ) ((↑x_1.u : R) * (↑x_2.u : R)) 2 + (x_1.r * HPow.hPow (β := ℕ) (↑x_2.u : R) 2 + x_2.r)
Tactic: simp only [mul_def, Units.val_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C C' x x_1 x_2 : VariableChange R
⊢ (x * x_1 * x_2).s = (x * (x_1 * x_2)).s
have s : (↑x_2.u : R) * ((↑x_1.u : R) * x.s + x_1.s) + x_2.s = (↑x_1.u : R) * (↑x_2.u : R) * x.s + ((↑x_2.u : R) * x_1.s + x_2.s)
Tactic: simp only [mul_def, Units.val_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C C' x x_1 x_2 : VariableChange R
⊢ (x * x_1 * x_2).t = (x * (x_1 * x_2)).t
have t : (x.t * HPow.hPow (β := ℕ) (↑x_1.u : R) 3 + x.r * x_1.s * HPow.hPow (β := ℕ) (↑x_1.u : R) 2 + x_1.t) *
        HPow.hPow (β := ℕ) (↑x_2.u : R) 3 +
      (x.r * HPow.hPow (β := ℕ) (↑x_1.u : R) 2 + x_1.r) * x_2.s * HPow.hPow (β := ℕ) (↑x_2.u : R) 2 +
    x_2.t =
  x.t * HPow.hPow (β := ℕ) ((↑x_1.u : R) * (↑x_2.u : R)) 3 +
      x.r * ((↑x_2.u : R) * x_1.s + x_2.s) * HPow.hPow (β := ℕ) ((↑x_1.u : R) * (↑x_2.u : R)) 2 +
    (x_1.t * HPow.hPow (β := ℕ) (↑x_2.u : R) 3 + x_1.r * x_2.s * HPow.hPow (β := ℕ) (↑x_2.u : R) 2 + x_2.t)
Tactic: simp only [mul_def, Units.val_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C_1 C' C : VariableChange R
⊢ C⁻¹ * C = 1
have rw : {
    u :=
      { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
            t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.u *
        C.u,
    r :=
      { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
              t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.r *
          HPow.hPow (β := ℕ) (↑C.u : R) 2 +
        C.r,
    s :=
      (↑C.u : R) *
          { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
              t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.s +
        C.s,
    t :=
      { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.t *
            HPow.hPow (β := ℕ) (↑C.u : R) 3 +
          { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                  t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.r *
              C.s *
            HPow.hPow (β := ℕ) (↑C.u : R) 2 +
        C.t :
    VariableChange R } =
  { u := 1, r := 0, s := 0, t := 0 }
Tactic: rw [mul_def, one_def, inv_def]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C_1 C' C : VariableChange R
⊢ {
      u :=
        { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
              t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.u *
          C.u,
      r :=
        { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.r *
            HPow.hPow (β := ℕ) (↑C.u : R) 2 +
          C.r,
      s :=
        (↑C.u : R) *
            { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.s +
          C.s,
      t :=
        { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                  t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.t *
              HPow.hPow (β := ℕ) (↑C.u : R) 3 +
            { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                    t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.r *
                C.s *
              HPow.hPow (β := ℕ) (↑C.u : R) 2 +
          C.t :
      VariableChange R } =
    { u := 1, r := 0, s := 0, t := 0 }
have u : (↑{
          u :=
            { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                  t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.u *
              C.u,
          r :=
            { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                    t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.r *
                HPow.hPow (β := ℕ) (↑C.u : R) 2 +
              C.r,
          s :=
            (↑C.u : R) *
                { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                    t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.s +
              C.s,
          t :=
            { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                      t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.t *
                  HPow.hPow (β := ℕ) (↑C.u : R) 3 +
                { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                        t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.r *
                    C.s *
                  HPow.hPow (β := ℕ) (↑C.u : R) 2 +
              C.t :
          VariableChange R }.u :
    R) =
  (↑(u { u := 1, r := 0, s := 0, t := 0 }) : R)
Tactic: ext