case mp
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
H : ↑x = ↑y
⊢ ↑x = ↑y

case mpr
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
H : ↑x = ↑y
⊢ ↑x = ↑y
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
⊢ ↑x = ↑y ↔ ↑x = ↑y
constructor <;> intro H
no goals
case mpr
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
H : ↑x = ↑y
⊢ ↑x = ↑y
rw [nat_cast K p 0, nat_cast K p 0, H]
case mp
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
H : ∃ z, (↑(frobenius K p)^[(0, ↑y).fst + z]) (0, ↑x).snd = (↑(frobenius K p)^[(0, ↑x).fst + z]) (0, ↑y).snd
⊢ ↑x = ↑y
case mp
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
H : ↑x = ↑y
⊢ ↑x = ↑y
rw [nat_cast K p 0, nat_cast K p 0, eq_iff'] at H
case mp.intro
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y z : ℕ
H : (↑(frobenius K p)^[(0, ↑y).fst + z]) (0, ↑x).snd = (↑(frobenius K p)^[(0, ↑x).fst + z]) (0, ↑y).snd
⊢ ↑x = ↑y
case mp
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
H : ∃ z, (↑(frobenius K p)^[(0, ↑y).fst + z]) (0, ↑x).snd = (↑(frobenius K p)^[(0, ↑x).fst + z]) (0, ↑y).snd
⊢ ↑x = ↑y
cases' H with z H
no goals
case mp.intro
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y z : ℕ
H : (↑(frobenius K p)^[(0, ↑y).fst + z]) (0, ↑x).snd = (↑(frobenius K p)^[(0, ↑x).fst + z]) (0, ↑y).snd
⊢ ↑x = ↑y
simpa only [zero_add, iterate_fixed (frobenius_nat_cast K p _)] using H