Theorem: Model.a3_zero_of_a1_zero_of_disc_zero_of_char_two (ECTate/Algebra/EllipticCurve/Model.lean)

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]
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

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]
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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]
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals