-- Mathlib/FieldTheory/PerfectClosure.lean
theorem natCast (n x : ℕ) : (x : PerfectClosure K p) = mk K p (n, x)

Proof state:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x n : ℕ
ih : ↑x = mk K p (n, ↑x)
this : R K p (n, ↑x) (n.succ, (frobenius K p) ↑x)
⊢ R K p (n, ↑x) (n + 1, ↑x)

Tactic:
rwa [frobenius_natCast K p x] at this

Result:
no goals

Proof state:
case zero.zero
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
⊢ ↑0 = mk K p (0, ↑0)

Tactic:
simp

Result:
no goals

Proof state:
case zero.succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ
ih : ↑x = mk K p (0, ↑x)
⊢ ↑(x + 1) = mk K p (0, ↑(x + 1))

Tactic:
rw [Nat.cast_succ, Nat.cast_succ, ih]

Result:
case zero.succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ
ih : ↑x = mk K p (0, ↑x)
⊢ mk K p (0, ↑x) + 1 = mk K p (0, ↑x + 1)

Proof state:
case succ.a
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x n : ℕ
ih : ↑x = mk K p (n, ↑x)
⊢ R K p (n, ↑x) (n.succ, (frobenius K p) ↑x)

Tactic:
apply R.intro

Result:
no goals

Proof state:
case zero
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ
⊢ ↑x = mk K p (0, ↑x)

Tactic:
induction' x with x ih

Result:
case zero.zero
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
⊢ ↑0 = mk K p (0, ↑0)

case zero.succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ
ih : ↑x = mk K p (0, ↑x)
⊢ ↑(x + 1) = mk K p (0, ↑(x + 1))

Proof state:
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x n : ℕ
ih : ↑x = mk K p (n, ↑x)
⊢ ↑x = mk K p (n + 1, ↑x)

Tactic:
rw [ih]

Result:
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x n : ℕ
ih : ↑x = mk K p (n, ↑x)
⊢ mk K p (n, ↑x) = mk K p (n + 1, ↑x)

Proof state:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n x : ℕ
⊢ ↑x = mk K p (n, ↑x)

Tactic:
induction' n with n ih

Result:
case zero
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ
⊢ ↑x = mk K p (0, ↑x)

case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x n : ℕ
ih : ↑x = mk K p (n, ↑x)
⊢ ↑x = mk K p (n + 1, ↑x)

Proof state:
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x n : ℕ
ih : ↑x = mk K p (n, ↑x)
⊢ mk K p (n, ↑x) = mk K p (n + 1, ↑x)

Tactic:
apply Quot.sound

Result:
case succ.a
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x n : ℕ
ih : ↑x = mk K p (n, ↑x)
⊢ R K p (n, ↑x) (n + 1, ↑x)

Proof state:
case zero.succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ
ih : ↑x = mk K p (0, ↑x)
⊢ mk K p (0, ↑x) + 1 = mk K p (0, ↑x + 1)

Tactic:
rfl

Result:
no goals

Proof state:
case succ.a
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x n : ℕ
ih : ↑x = mk K p (n, ↑x)
⊢ R K p (n, ↑x) (n + 1, ↑x)

Tactic:
suffices R K p (n, (x : K)) (Nat.succ n, frobenius K p (x : K)) by
  rwa [frobenius_natCast K p x] at this

Result:
case succ.a
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x n : ℕ
ih : ↑x = mk K p (n, ↑x)
⊢ R K p (n, ↑x) (n.succ, (frobenius K p) ↑x)