awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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
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)
⊢ ∃ (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)

Premises used: WeierstrassCurve.valuation_Δ_aux, WeierstrassCurve.exists_isIntegral, exists_maximalFor_of_wellFoundedGT, HSMul.hSMul, WeierstrassCurve.IsIntegral
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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
⊢ (fun (C_1 : VariableChange K) ↦ IsIntegral R (C_1 • C • W)) 1

Tactic:
simp only [one_smul, hC.1]

Premises used: one_smul, And.left
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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
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)
⊢ ∃ (C : VariableChange K), IsMinimal R (C • W)

Tactic:
refine ⟨C, ⟨⟨by simp only [one_smul, hC.1], ?_⟩⟩⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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)
⊢ IsIntegral R ((j • C) • W)

Tactic:
rw [← smul_assoc] at hj

Premises used: smul_assoc
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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) :=
  ⋯
simp_all :
  valuation_Δ_aux R (C • W) ≤ valuation_Δ_aux R (j • C • W) → valuation_Δ_aux R (j • C • W) ≤ valuation_Δ_aux R (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)

Tactic:
simp_all only [one_smul]

Premises used: one_smul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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) :=
  ⋯
rw :
  valuation_Δ_aux R (C • W) ≤ valuation_Δ_aux R ((j • C) • W) →
    valuation_Δ_aux R ((j • C) • W) ≤ valuation_Δ_aux R (C • W)
⊢ valuation_Δ_aux R (C • W) ≤ valuation_Δ_aux R (j • C • W) → valuation_Δ_aux R (j • C • W) ≤ valuation_Δ_aux R (C • W)

Tactic:
rw [← smul_assoc]

Premises used: smul_assoc
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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) :=
  ⋯
⊢ valuation_Δ_aux R (C • W) ≤ valuation_Δ_aux R ((j • C) • W) →
    valuation_Δ_aux R ((j • C) • W) ≤ valuation_Δ_aux R (C • W)

Tactic:
h
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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) :=
  ⋯
⊢ valuation_Δ_aux R (C • W) ≤ valuation_Δ_aux R ((j • C) • W) →
    valuation_Δ_aux R ((j • C) • W) ≤ valuation_Δ_aux R (C • W)

Tactic:
exact h
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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
⊢ IsMinimal R (minimal R W)

Tactic:
(W.exists_isMinimal R).choose_spec

Premises used: Exists.choose_spec, WeierstrassCurve.exists_isMinimal, WeierstrassCurve.minimal
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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))

Tactic:
Iff.trans ?_ (W.reduction R).isElliptic_iff.symm

Premises used: Iff.trans, WeierstrassCurve.reduction, WeierstrassCurve.isElliptic_iff, Iff.symm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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
refine : HasGoodReduction R W ↔ IsUnit (M := ResidueField R) (Δ (reduction R W) : ResidueField R)
⊢ HasGoodReduction R W ↔
    WeierstrassCurve.IsElliptic (R := ResidueField R) (reduction R W : WeierstrassCurve (ResidueField R))

Tactic:
refine Iff.trans ?_ (W.reduction R).isElliptic_iff.symm

Premises used: Iff.trans, WeierstrassCurve.reduction, WeierstrassCurve.isElliptic_iff, Iff.symm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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
simp : HasGoodReduction R W ↔ (integralModel R W).Δ ∉ IsLocalRing.maximalIdeal R
⊢ HasGoodReduction R W ↔ IsUnit (M := ResidueField R) (Δ (reduction R W) : ResidueField R)

Tactic:
simp only [reduction, map_Δ, isUnit_iff_ne_zero, ne_eq, residue_eq_zero_iff]

Premises used: IsLocalRing.residue_eq_zero_iff, isUnit_iff_ne_zero, ne_eq, WeierstrassCurve.reduction, WeierstrassCurve.map_Δ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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
⊢ ¬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 _ _
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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
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 ℤ))
⊢ HasGoodReduction R W ↔ (integralModel R W).Δ ∉ IsLocalRing.maximalIdeal R

Tactic:
refine ((integralModel_Δ_eq R W ▸ hasGoodReduction_iff _ _).trans ?_).trans h
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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
⊢ 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:
simpa [hW] using (valuation_le_one (R := R) (K := K) _ _).ge_iff_eq.symm

Premises used: LE.le.ge_iff_eq, IsDedekindDomain.HeightOneSpectrum.valuation_le_one, Iff.symm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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
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 ℤ))
⊢ HasGoodReduction R W ∨ HasMultiplicativeReduction R W ∨ HasAdditiveReduction R W

Tactic:
rw [hasGoodReduction_iff, hasMultiplicativeReduction_iff, hasAdditiveReduction_iff,
    ← integralModel_Δ_eq R W, ← integralModel_c₄_eq R W]

Premises used: WeierstrassCurve.integralModel_Δ_eq, WeierstrassCurve.hasGoodReduction_iff, WeierstrassCurve.hasMultiplicativeReduction_iff, WeierstrassCurve.hasAdditiveReduction_iff, WeierstrassCurve.integralModel_c₄_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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
⊢ 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:
grind [valuation_le_one]

Premises used: IsDedekindDomain.HeightOneSpectrum.valuation_le_one
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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 : HasGoodReduction R W
⊢ ¬HasMultiplicativeReduction R W

Tactic:
fun h ↦ h.badReduction.ne hW.goodReduction

Premises used: WeierstrassCurve.HasGoodReduction.goodReduction, WeierstrassCurve.HasMultiplicativeReduction.badReduction, Not, LT.lt.ne
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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 : HasGoodReduction R W
⊢ ¬HasAdditiveReduction R W

Tactic:
fun h ↦ h.badReduction.ne hW.goodReduction

Premises used: WeierstrassCurve.HasAdditiveReduction.badReduction, WeierstrassCurve.HasGoodReduction.goodReduction, Not, LT.lt.ne
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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 : HasMultiplicativeReduction R W
⊢ ¬HasGoodReduction R W

Tactic:
fun h ↦ hW.badReduction.ne h.goodReduction

Premises used: WeierstrassCurve.HasGoodReduction.goodReduction, WeierstrassCurve.HasMultiplicativeReduction.badReduction, Not, LT.lt.ne
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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 : HasAdditiveReduction R W
⊢ ¬HasGoodReduction R W

Tactic:
fun h ↦ hW.badReduction.ne h.goodReduction

Premises used: WeierstrassCurve.HasAdditiveReduction.badReduction, WeierstrassCurve.HasGoodReduction.goodReduction, Not, LT.lt.ne
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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 : HasMultiplicativeReduction R W
⊢ ¬HasAdditiveReduction R W

Tactic:
fun h ↦ h.additiveReduction.ne hW.multiplicativeReduction

Premises used: WeierstrassCurve.HasAdditiveReduction.additiveReduction, Not, LT.lt.ne, WeierstrassCurve.HasMultiplicativeReduction.multiplicativeReduction
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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 : HasAdditiveReduction R W
⊢ ¬HasMultiplicativeReduction R W

Tactic:
fun h ↦ hW.additiveReduction.ne h.multiplicativeReduction

Premises used: WeierstrassCurve.HasAdditiveReduction.additiveReduction, Not, LT.lt.ne, WeierstrassCurve.HasMultiplicativeReduction.multiplicativeReduction
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
⊢ Eq.{u + 1} (α := VariableChange R) 1 { u := 1, r := 0, s := 0, t := 0 }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
C C' : VariableChange R
⊢ C * C' =
    { u := C.u * C'.u, r := C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r, s := (↑C'.u : R) * C.s + C'.s,
      t := C.t * HPow.hPow (β := ℕ) (↑C'.u : R) 3 + C.r * C'.s * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.t }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
C : VariableChange R
⊢ C⁻¹ =
    { 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 }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
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
t : (x * x_1 * x_2).t = (x * (x_1 * x_2)).t
⊢ x * x_1 * x_2 = x * (x_1 * x_2)

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C C' x x_1 x_2 : VariableChange R
u : (↑x.u : R) * (↑x_1.u : R) * (↑x_2.u : R) = (↑x.u : R) * ((↑x_1.u : R) * (↑x_2.u : R))
⊢ (↑(x * x_1 * x_2).u : R) = (↑(x * (x_1 * x_2)).u : R)

Tactic:
simp only [mul_def, Units.val_mul]

Premises used: WeierstrassCurve.VariableChange.mul_def, Units.val_mul