internlm/Lean-Github huggingface dataset:
Theorem: Model.c4_zero_iff_b2_zero_of_char_three
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 3
hchar' : ↑(ringChar K) = 3
⊢ c4 e = 0 ↔ b2 e = 0
Tactic:
have hchar'' : (3 : K) = 0 := by simp [← hchar', ringChar.Nat.cast_ringChar]
Proof state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 3
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
⊢ c4 e = 0 ↔ b2 e = 0
Theorem: Model.c4_zero_iff_b2_zero_of_char_three
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 3
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
⊢ c4 e = 0 ↔ b2 e = 0
Tactic:
rw [c4, show (24 : K) = 3 * 8 by norm_num, hchar'']
Proof state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 3
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
⊢ b2 e ^ 2 - 0 * 8 * b4 e = 0 ↔ b2 e = 0
Theorem: Model.c4_zero_iff_b2_zero_of_char_three
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 3
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
⊢ b2 e ^ 2 - 0 * 8 * b4 e = 0 ↔ b2 e = 0
Tactic:
simp only [mul_zero, zero_mul, add_zero, sub_zero]
Proof state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 3
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
⊢ b2 e ^ 2 = 0 ↔ b2 e = 0
Theorem: Model.c4_zero_iff_b2_zero_of_char_three
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 3
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
⊢ b2 e ^ 2 = 0 ↔ b2 e = 0
Tactic:
rw [pow_eq_zero_iff]
Proof state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 3
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
⊢ 0 < 2
Theorem: Model.c4_zero_iff_b2_zero_of_char_three
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 3
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Model.c4_zero_iff_b2_zero_of_char_three
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 3
⊢ ↑(ringChar K) = 3
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Model.c4_zero_iff_b2_zero_of_char_three
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 3
hchar' : ↑(ringChar K) = 3
⊢ 3 = 0
Tactic:
simp [← hchar', ringChar.Nat.cast_ringChar]
Proof state after:
no goals
Theorem: Model.c4_zero_iff_b2_zero_of_char_three
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 3
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
⊢ 24 = 3 * 8
Tactic:
norm_num
Proof state after:
no goals
Theorem: Model.a3_zero_of_a1_zero_of_disc_zero_of_char_two
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hdisc : discr e = 0
ha1 : e.a1 = 0
⊢ e.a3 = 0
Tactic:
have hchar' : (ringChar K : K) = 2 := by simp [h]
Proof state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hdisc : discr e = 0
ha1 : e.a1 = 0
hchar' : ↑(ringChar K) = 2
⊢ e.a3 = 0
Theorem: Model.a3_zero_of_a1_zero_of_disc_zero_of_char_two
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hdisc : discr e = 0
ha1 : e.a1 = 0
hchar' : ↑(ringChar K) = 2
⊢ e.a3 = 0
Tactic:
have hchar'' : (2 : K) = 0 := by simp [← hchar', ringChar.Nat.cast_ringChar]
Proof state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hdisc : discr e = 0
ha1 : e.a1 = 0
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
⊢ e.a3 = 0
Theorem: Model.a3_zero_of_a1_zero_of_disc_zero_of_char_two
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hdisc : discr e = 0
ha1 : e.a1 = 0
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
⊢ e.a3 = 0
Tactic:
rw [discr, b2, b4, b6, b8, ha1,
  show (8 : K) = 2 * 4 by norm_num, show (4 : K) = 2 * 2 by norm_num, show (27 : K) = 2 * 13 + 1 by norm_num, hchar''] at hdisc
Proof state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hdisc :
  -(0 * 0 + 0 * 0 * e.a2) * (0 * 0 + 0 * 0 * e.a2) *
            (0 * 0 * e.a6 - 0 * e.a3 * e.a4 + 0 * 0 * e.a2 * e.a6 + e.a2 * e.a3 * e.a3 - e.a4 * e.a4) -
          0 * (0 * 0) * (0 * e.a3 + 0 * e.a4) ^ 3 -
        (0 * 13 + 1) * (e.a3 * e.a3 + 0 * 0 * e.a6) * (e.a3 * e.a3 + 0 * 0 * e.a6) +
      9 * (0 * 0 + 0 * 0 * e.a2) * (0 * e.a3 + 0 * e.a4) * (e.a3 * e.a3 + 0 * 0 * e.a6) =
    0
ha1 : e.a1 = 0
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
⊢ e.a3 = 0
Theorem: Model.a3_zero_of_a1_zero_of_disc_zero_of_char_two
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hdisc :
  -(0 * 0 + 0 * 0 * e.a2) * (0 * 0 + 0 * 0 * e.a2) *
            (0 * 0 * e.a6 - 0 * e.a3 * e.a4 + 0 * 0 * e.a2 * e.a6 + e.a2 * e.a3 * e.a3 - e.a4 * e.a4) -
          0 * (0 * 0) * (0 * e.a3 + 0 * e.a4) ^ 3 -
        (0 * 13 + 1) * (e.a3 * e.a3 + 0 * 0 * e.a6) * (e.a3 * e.a3 + 0 * 0 * e.a6) +
      9 * (0 * 0 + 0 * 0 * e.a2) * (0 * e.a3 + 0 * e.a4) * (e.a3 * e.a3 + 0 * 0 * e.a6) =
    0
ha1 : e.a1 = 0
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
⊢ e.a3 = 0
Tactic:
simp only [mul_zero, zero_mul, add_zero, neg_zero, sub_self, zero_add, one_mul, zero_sub, neg_eq_zero]
  at hdisc
Proof state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
ha1 : e.a1 = 0
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hdisc : e.a3 * e.a3 * (e.a3 * e.a3) = 0
⊢ e.a3 = 0
Theorem: Model.a3_zero_of_a1_zero_of_disc_zero_of_char_two
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
ha1 : e.a1 = 0
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hdisc : e.a3 * e.a3 * (e.a3 * e.a3) = 0
⊢ e.a3 = 0
Tactic:
rw [← pow_two, ← pow_two, ← pow_mul] at hdisc
Proof state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
ha1 : e.a1 = 0
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hdisc : e.a3 ^ (2 * 2) = 0
⊢ e.a3 = 0
Theorem: Model.a3_zero_of_a1_zero_of_disc_zero_of_char_two
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
ha1 : e.a1 = 0
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hdisc : e.a3 ^ (2 * 2) = 0
⊢ e.a3 = 0
Tactic:
rwa [pow_eq_zero_iff] at hdisc
Proof state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
ha1 : e.a1 = 0
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hdisc : e.a3 ^ (2 * 2) = 0
⊢ 0 < 2 * 2
Theorem: Model.a3_zero_of_a1_zero_of_disc_zero_of_char_two
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
ha1 : e.a1 = 0
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hdisc : e.a3 ^ (2 * 2) = 0
⊢ 0 < 2 * 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Model.a3_zero_of_a1_zero_of_disc_zero_of_char_two
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hdisc : discr e = 0
ha1 : e.a1 = 0
⊢ ↑(ringChar K) = 2
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Model.a3_zero_of_a1_zero_of_disc_zero_of_char_two
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hdisc : discr e = 0
ha1 : e.a1 = 0
hchar' : ↑(ringChar K) = 2
⊢ 2 = 0
Tactic:
simp [← hchar', ringChar.Nat.cast_ringChar]
Proof state after:
no goals
Theorem: Model.a3_zero_of_a1_zero_of_disc_zero_of_char_two
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hdisc :
  -(0 * 0 + 4 * e.a2) * (0 * 0 + 4 * e.a2) *
            (0 * 0 * e.a6 - 0 * e.a3 * e.a4 + 4 * e.a2 * e.a6 + e.a2 * e.a3 * e.a3 - e.a4 * e.a4) -
          8 * (0 * e.a3 + 2 * e.a4) ^ 3 -
        27 * (e.a3 * e.a3 + 4 * e.a6) * (e.a3 * e.a3 + 4 * e.a6) +
      9 * (0 * 0 + 4 * e.a2) * (0 * e.a3 + 2 * e.a4) * (e.a3 * e.a3 + 4 * e.a6) =
    0
ha1 : e.a1 = 0
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
⊢ 8 = 2 * 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: Model.a3_zero_of_a1_zero_of_disc_zero_of_char_two
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hdisc :
  -(0 * 0 + 4 * e.a2) * (0 * 0 + 4 * e.a2) *
            (0 * 0 * e.a6 - 0 * e.a3 * e.a4 + 4 * e.a2 * e.a6 + e.a2 * e.a3 * e.a3 - e.a4 * e.a4) -
          2 * 4 * (0 * e.a3 + 2 * e.a4) ^ 3 -
        27 * (e.a3 * e.a3 + 4 * e.a6) * (e.a3 * e.a3 + 4 * e.a6) +
      9 * (0 * 0 + 4 * e.a2) * (0 * e.a3 + 2 * e.a4) * (e.a3 * e.a3 + 4 * e.a6) =
    0
ha1 : e.a1 = 0
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
⊢ 4 = 2 * 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Model.a3_zero_of_a1_zero_of_disc_zero_of_char_two
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hdisc :
  -(0 * 0 + 2 * 2 * e.a2) * (0 * 0 + 2 * 2 * e.a2) *
            (0 * 0 * e.a6 - 0 * e.a3 * e.a4 + 2 * 2 * e.a2 * e.a6 + e.a2 * e.a3 * e.a3 - e.a4 * e.a4) -
          2 * (2 * 2) * (0 * e.a3 + 2 * e.a4) ^ 3 -
        27 * (e.a3 * e.a3 + 2 * 2 * e.a6) * (e.a3 * e.a3 + 2 * 2 * e.a6) +
      9 * (0 * 0 + 2 * 2 * e.a2) * (0 * e.a3 + 2 * e.a4) * (e.a3 * e.a3 + 2 * 2 * e.a6) =
    0
ha1 : e.a1 = 0
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
⊢ 27 = 2 * 13 + 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: Model.b4_zero_of_b2_zero_of_disc_zero_of_char_three
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 3
hdisc : discr e = 0
hb2 : b2 e = 0
⊢ b4 e = 0
Tactic:
have hchar' : (ringChar K : K) = 3 := by simp [h]
Proof state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 3
hdisc : discr e = 0
hb2 : b2 e = 0
hchar' : ↑(ringChar K) = 3
⊢ b4 e = 0
Theorem: Model.b4_zero_of_b2_zero_of_disc_zero_of_char_three
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 3
hdisc : discr e = 0
hb2 : b2 e = 0
hchar' : ↑(ringChar K) = 3
⊢ b4 e = 0
Tactic:
have hchar'' : (3 : K) = 0 := by simp [← hchar', ringChar.Nat.cast_ringChar]
Proof state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 3
hdisc : discr e = 0
hb2 : b2 e = 0
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
⊢ b4 e = 0
Theorem: Model.b4_zero_of_b2_zero_of_disc_zero_of_char_three
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 3
hdisc : discr e = 0
hb2 : b2 e = 0
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
⊢ b4 e = 0
Tactic:
rw [discr, hb2,
  show (27 : K) = 3 * 9 by norm_num,
  show (8 : K) = 3 * 3 - 1 by norm_num,
  hchar''] at hdisc
Proof state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 3
hdisc : -0 * 0 * b8 e - (0 * 0 - 1) * b4 e ^ 3 - 0 * 9 * b6 e * b6 e + 9 * 0 * b4 e * b6 e = 0
hb2 : b2 e = 0
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
⊢ b4 e = 0
Theorem: Model.b4_zero_of_b2_zero_of_disc_zero_of_char_three
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 3
hdisc : -0 * 0 * b8 e - (0 * 0 - 1) * b4 e ^ 3 - 0 * 9 * b6 e * b6 e + 9 * 0 * b4 e * b6 e = 0
hb2 : b2 e = 0
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
⊢ b4 e = 0
Tactic:
simpa using hdisc
Proof state after:
no goals
Theorem: Model.b4_zero_of_b2_zero_of_disc_zero_of_char_three
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 3
hdisc : discr e = 0
hb2 : b2 e = 0
⊢ ↑(ringChar K) = 3
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Model.b4_zero_of_b2_zero_of_disc_zero_of_char_three
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 3
hdisc : discr e = 0
hb2 : b2 e = 0
hchar' : ↑(ringChar K) = 3
⊢ 3 = 0
Tactic:
simp [← hchar', ringChar.Nat.cast_ringChar]
Proof state after:
no goals
Theorem: Model.b4_zero_of_b2_zero_of_disc_zero_of_char_three
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 3
hdisc : -0 * 0 * b8 e - 8 * b4 e ^ 3 - 27 * b6 e * b6 e + 9 * 0 * b4 e * b6 e = 0
hb2 : b2 e = 0
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
⊢ 27 = 3 * 9
Tactic:
norm_num
Proof state after:
no goals
Theorem: Model.b4_zero_of_b2_zero_of_disc_zero_of_char_three
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 3
hdisc : -0 * 0 * b8 e - 8 * b4 e ^ 3 - 3 * 9 * b6 e * b6 e + 9 * 0 * b4 e * b6 e = 0
hb2 : b2 e = 0
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
⊢ 8 = 3 * 3 - 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: Model.Field.ringChar_eq_of_Prime
Proof state before:
K : Type u
inst✝¹ : Field K
n : ℕ
inst✝ : Nat.AtLeastTwo n
hn : OfNat.ofNat n = 0
hnp : Nat.Prime n
⊢ ringChar K = n
Tactic:
rw [← Nat.cast_eq_ofNat, ringChar.spec] at hn
Proof state after:
K : Type u
inst✝¹ : Field K
n : ℕ
inst✝ : Nat.AtLeastTwo n
hn : ringChar K ∣ n
hnp : Nat.Prime n
⊢ ringChar K = n
Theorem: Model.Field.ringChar_eq_of_Prime
Proof state before:
K : Type u
inst✝¹ : Field K
n : ℕ
inst✝ : Nat.AtLeastTwo n
hn : ringChar K ∣ n
hnp : Nat.Prime n
⊢ ringChar K = n
Tactic:
cases (Nat.dvd_prime hnp).mp hn with
| inl h =>
  simpa [h] using CharP.char_is_prime_or_zero K (ringChar K)
| inr h =>
  assumption
Proof state after:
no goals
Theorem: Model.Field.ringChar_eq_of_Prime
Proof state before:
case inl
K : Type u
inst✝¹ : Field K
n : ℕ
inst✝ : Nat.AtLeastTwo n
hn : ringChar K ∣ n
hnp : Nat.Prime n
h : ringChar K = 1
⊢ ringChar K = n
Tactic:
simpa [h] using CharP.char_is_prime_or_zero K (ringChar K)
Proof state after:
no goals
Theorem: Model.Field.ringChar_eq_of_Prime
Proof state before:
case inr
K : Type u
inst✝¹ : Field K
n : ℕ
inst✝ : Nat.AtLeastTwo n
hn : ringChar K ∣ n
hnp : Nat.Prime n
h : ringChar K = n
⊢ ringChar K = n
Tactic:
assumption
Proof state after:
no goals
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
⊢ is_singular_point e (singular_point e)
Tactic:
rw [singular_point]
Proof state after:
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
⊢ is_singular_point e
    (if c4 e = 0 then
      match ringChar K with
      | 2 => (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6))
      | 3 => (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3)
      | x => (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2)
    else ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e))
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
⊢ is_singular_point e
    (if c4 e = 0 then
      match ringChar K with
      | 2 => (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6))
      | 3 => (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3)
      | x => (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2)
    else ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e))
Tactic:
split_ifs with hc4
Proof state after:
case pos
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : c4 e = 0
⊢ is_singular_point e
    (match ringChar K with
    | 2 => (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6))
    | 3 => (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3)
    | x => (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2))

case neg
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ is_singular_point e ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e)
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case neg
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ is_singular_point e ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e)
Tactic:
. rw [is_singular_point]
  refine ⟨?_, ?_, ?_⟩
  . rw [weierstrass]
    apply nzero_mul_left_cancel (e.c4 ^ 3) _ _ (pow_ne_zero _ hc4)
    rw [mul_zero]
    simp only [div_eq_mul_inv]
    rw [show c4 e ^ 3 * (((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹) ^ 2 +
          e.a1 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) * ((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹) +
        e.a3 * ((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹) -
        (((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) ^ 3 + e.a2 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) ^ 2 +
        e.a4 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) + e.a6)) =
      (c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * ((b2 e * b5 e + 3 * b7 e)) ^ 2 +
        c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * e.a1 * ((18 * b6 e - b2 e * b4 e)) * ((b2 e * b5 e + 3 * b7 e)) +
      c4 e * (c4 e)⁻¹ * c4 e * c4 e * e.a3 * ((b2 e * b5 e + 3 * b7 e)) -
      (c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * ((18 * b6 e - b2 e * b4 e)) ^ 3 +
      c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * e.a2 * ((18 * b6 e - b2 e * b4 e)) ^ 2 +
        c4 e * (c4 e)⁻¹ * c4 e * c4 e * e.a4 * ((18 * b6 e - b2 e * b4 e)) +
      c4 e * c4 e * c4 e * e.a6)) by ring]
    simp only [mul_inv_cancel hc4, one_mul]
    rw [b5, b7, c4, b2, b4, b6]
    rw [← mul_zero (e.a1^6 + 12*e.a1^4*e.a2 + 48*e.a1^2*e.a2^2 - 36*e.a1^3*e.a3 + 64*e.a2^3
      - 144*e.a1*e.a2*e.a3 - 72*e.a1^2*e.a4 + 216*e.a3^2 - 288*e.a2*e.a4 + 864*e.a6),
      ← h, discr_eq_neg_singular]
    ring
  . rw [dweierstrass_dx]
    apply nzero_mul_left_cancel (e.c4 ^ 2) _ _ (pow_ne_zero _ hc4)
    rw [mul_zero, pow_two]
    simp only [div_eq_mul_inv]
    rw [show c4 e * c4 e *
      (e.a1 * ((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹) -
        (3 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) ^ 2
        + 2 * e.a2 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) + e.a4)) =
        c4 e * (c4 e)⁻¹ * c4 e * (e.a1 * (b2 e * b5 e + 3 * b7 e)
        - 2 * e.a2 * ((18 * b6 e - b2 e * b4 e)))
        - c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ *
        3 * (18 * b6 e - b2 e * b4 e) ^ 2 - e.a4 * c4 e * c4 e
      by ring]
    simp only [mul_inv_cancel hc4, one_mul]
    rw [b5, b7, c4, b2, b4, b6]
    rw [← mul_zero (36 : K), ← h, discr_eq_neg_singular]
    ring
  . rw [dweierstrass_dy]
    apply nzero_mul_left_cancel e.c4 _ _ hc4
    simp only [div_eq_mul_inv, mul_zero]
    rw [show c4 e * (2 * ((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹)
        + e.a1 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) + e.a3) =
      c4 e * (c4 e)⁻¹ * (2 * (b2 e * b5 e + 3 * b7 e)
      + e.a1 * ((18 * b6 e - b2 e * b4 e))) + c4 e * e.a3 by ring]
    simp only [mul_inv_cancel hc4, one_mul]
    rw [b5, b7, c4, b2, b4, b6]
    ring
Proof state after:
no goals
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case pos
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : c4 e = 0
⊢ is_singular_point e
    (match ringChar K with
    | 2 => (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6))
    | 3 => (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3)
    | x => (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2))
Tactic:
have hc6 : c6 e = 0 := by
  simpa [h, hc4, pow_succ, mul_eq_zero] using discr_identity e
Proof state after:
case pos
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : c4 e = 0
hc6 : c6 e = 0
⊢ is_singular_point e
    (match ringChar K with
    | 2 => (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6))
    | 3 => (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3)
    | x => (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2))
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case pos
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : c4 e = 0
hc6 : c6 e = 0
⊢ is_singular_point e
    (match ringChar K with
    | 2 => (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6))
    | 3 => (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3)
    | x => (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2))
Tactic:
split
Proof state after:
case pos.h_1
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : c4 e = 0
hc6 : c6 e = 0
x✝ : ℕ
heq✝ : ringChar K = 2
⊢ is_singular_point e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6))

case pos.h_2
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : c4 e = 0
hc6 : c6 e = 0
x✝ : ℕ
heq✝ : ringChar K = 3
⊢ is_singular_point e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3)

case pos.h_3
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : c4 e = 0
hc6 : c6 e = 0
x✝² : ℕ
x✝¹ : ringChar K = 2 → False
x✝ : ringChar K = 3 → False
⊢ is_singular_point e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2)
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case pos.h_1
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : c4 e = 0
hc6 : c6 e = 0
x✝ : ℕ
heq✝ : ringChar K = 2
⊢ is_singular_point e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6))

case pos.h_2
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : c4 e = 0
hc6 : c6 e = 0
x✝ : ℕ
heq✝ : ringChar K = 3
⊢ is_singular_point e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3)

case pos.h_3
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : c4 e = 0
hc6 : c6 e = 0
x✝² : ℕ
x✝¹ : ringChar K = 2 → False
x✝ : ringChar K = 3 → False
⊢ is_singular_point e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2)
Tactic:
. rw [is_singular_point]
  have hchar : ringChar K = 2 := by assumption
  have hchar' : (ringChar K : K) = 2 := by simp [hchar]
  have hchar'' : (2 : K) = 0 := by simp [← hchar', ringChar.Nat.cast_ringChar]
  have hcharne : ringChar K ≠ 0 := by simp [hchar]
  have ha1 : e.a1 = 0 := by simpa [c4_zero_iff_a1_zero_of_char_two e hchar] using hc4
  have ha3 : e.a3 = 0 := a3_zero_of_a1_zero_of_disc_zero_of_char_two e hchar h ha1
  refine ⟨?_, ?_, ?_⟩
  . rw [weierstrass]
    simp only [ha1, ha3, mul_zero, zero_add, zero_mul, add_zero]
    rw [show 3 = 2 + 1 by norm_num]
    rw [pow_succ _ 2]
    rw [← hchar, pth_root_pow_char hcharne]
    rw [pth_root_pow_char hcharne]
    ring_nf
    simp [hchar'']
  . rw [dweierstrass_dx]
    simp only [ha1, zero_mul, hchar'', add_zero, zero_sub, neg_add_rev]
    rw [← hchar, pth_root_pow_char hcharne, ← sub_eq_add_neg]
    simp only [add_sub_add_right_eq_sub, sub_eq_iff_eq_add, zero_add]
    rw [show (3 : K) = 2 * 2 - 1 by norm_num]
    rw [hchar'']
    simp [← neg_mul_eq_neg_mul]
  . simp [dweierstrass_dy, ha1, ha3, hchar'']
Proof state after:
case pos.h_2
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : c4 e = 0
hc6 : c6 e = 0
x✝ : ℕ
heq✝ : ringChar K = 3
⊢ is_singular_point e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3)

case pos.h_3
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : c4 e = 0
hc6 : c6 e = 0
x✝² : ℕ
x✝¹ : ringChar K = 2 → False
x✝ : ringChar K = 3 → False
⊢ is_singular_point e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2)