case mk
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
m : ℕ
x : K
⊢ mk K p (m, x) = (↑(pthRoot (PerfectClosure K p) p)^[(m, x).fst]) (↑(of K p) (m, x).snd)
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
⊢ mk K p x = (↑(pthRoot (PerfectClosure K p) p)^[x.fst]) (↑(of K p) x.snd)
rcases x with ⟨m, x⟩
case mk.zero
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
⊢ mk K p (Nat.zero, x) = (↑(pthRoot (PerfectClosure K p) p)^[(Nat.zero, x).fst]) (↑(of K p) (Nat.zero, x).snd)

case mk.succ
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
m : ℕ
ih : mk K p (m, x) = (↑(pthRoot (PerfectClosure K p) p)^[(m, x).fst]) (↑(of K p) (m, x).snd)
⊢ mk K p (Nat.succ m, x) = (↑(pthRoot (PerfectClosure K p) p)^[(Nat.succ m, x).fst]) (↑(of K p) (Nat.succ m, x).snd)
case mk
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
m : ℕ
x : K
⊢ mk K p (m, x) = (↑(pthRoot (PerfectClosure K p) p)^[(m, x).fst]) (↑(of K p) (m, x).snd)
induction' m with m ih
case mk.succ
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
m : ℕ
ih : mk K p (m, x) = (↑(pthRoot (PerfectClosure K p) p)^[(m, x).fst]) (↑(of K p) (m, x).snd)
⊢ mk K p (Nat.succ m, x) = ↑(pthRoot (PerfectClosure K p) p) (mk K p (m, x))
case mk.succ
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
m : ℕ
ih : mk K p (m, x) = (↑(pthRoot (PerfectClosure K p) p)^[(m, x).fst]) (↑(of K p) (m, x).snd)
⊢ mk K p (Nat.succ m, x) = (↑(pthRoot (PerfectClosure K p) p)^[(Nat.succ m, x).fst]) (↑(of K p) (Nat.succ m, x).snd)
rw [iterate_succ_apply', ← ih]
no goals
case mk.succ
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
m : ℕ
ih : mk K p (m, x) = (↑(pthRoot (PerfectClosure K p) p)^[(m, x).fst]) (↑(of K p) (m, x).snd)
⊢ mk K p (Nat.succ m, x) = ↑(pthRoot (PerfectClosure K p) p) (mk K p (m, x))
rfl
no goals
case mk.zero
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
⊢ mk K p (Nat.zero, x) = (↑(pthRoot (PerfectClosure K p) p)^[(Nat.zero, x).fst]) (↑(of K p) (Nat.zero, x).snd)
rfl