case inl
R : Type u_1
ι : Type ?u.24466
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ringChar R = 2
⊢ orderOf (-1) = 1

case inr
R : Type u_1
ι : Type ?u.24466
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ¬ringChar R = 2
⊢ orderOf (-1) = 2
R : Type u_1
ι : Type ?u.24466
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ orderOf (-1) = if ringChar R = 2 then 1 else 2
split_ifs with h
case inr.hg
R : Type u_1
ι : Type ?u.24466
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ¬ringChar R = 2
⊢ (-1) ^ 2 = 1

case inr.hg1
R : Type u_1
ι : Type ?u.24466
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ¬ringChar R = 2
⊢ -1 ≠ 1
case inr
R : Type u_1
ι : Type ?u.24466
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ¬ringChar R = 2
⊢ orderOf (-1) = 2
apply orderOf_eq_prime
no goals
case inr.hg1
R : Type u_1
ι : Type ?u.24466
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ¬ringChar R = 2
⊢ -1 ≠ 1
simpa [neg_one_eq_one_iff] using h
no goals
case inl
R : Type u_1
ι : Type ?u.24466
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ringChar R = 2
⊢ orderOf (-1) = 1
rw [neg_one_eq_one_iff.2 h, orderOf_one]
no goals
case inr.hg
R : Type u_1
ι : Type ?u.24466
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ¬ringChar R = 2
⊢ (-1) ^ 2 = 1
simp