Theorem: Model.c4_zero_iff_b2_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
⊢ c4 e = 0 ↔ b2 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
hchar' : ↑(ringChar K) = 3
⊢ c4 e = 0 ↔ b2 e = 0

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

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

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

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

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

State before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 3
⊢ ↑(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
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
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
⊢ 24 = 3 * 8
Tactic:
norm_num
State after:
no goals