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

State before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hchar' : ↑(ringChar K) = 2
⊢ c4 e = 0 ↔ e.a1 = 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
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
⊢ c4 e = 0 ↔ e.a1 = 0

State before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
⊢ c4 e = 0 ↔ e.a1 = 0
Tactic:
rw [c4, b2, show (24 : K) = 2 * 12 by norm_num, show (4 : K) = 2 * 2 by norm_num, hchar'', ← pow_two]
State after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
⊢ (e.a1 ^ 2 + 0 * 0 * e.a2) ^ 2 - 0 * 12 * b4 e = 0 ↔ e.a1 = 0

State before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
⊢ (e.a1 ^ 2 + 0 * 0 * e.a2) ^ 2 - 0 * 12 * b4 e = 0 ↔ e.a1 = 0
Tactic:
simp only [mul_zero, zero_mul, add_zero, ← pow_mul, sub_zero]
State after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
⊢ e.a1 ^ (2 * 2) = 0 ↔ e.a1 = 0

State before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
⊢ e.a1 ^ (2 * 2) = 0 ↔ e.a1 = 0
Tactic:
rw [pow_eq_zero_iff]
State after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
⊢ 0 < 2 * 2

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