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

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

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

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

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

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

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

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

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