-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
h : Function.Surjective (α := R) (β := R) (⇑(frobenius R p) : (a : R) → R)
n : ℕ
x : R
m : ℕ
refine_2 :
  ∀ (h1 : n ≤ m),
    HPow.hPow (α := R)
        ((fun (m : ℕ) ↦
            (if h_1 : n ≤ m then
                Nat.leRec (motive := fun (m : ℕ) (h : n ≤ m) ↦ R) x
                  (fun ⦃k : ℕ⦄ (hle : n ≤ k) (xk : R) ↦
                    (fun (x : R) (hx : (frobenius R p : (a : R) → R) x = xk) ↦ x)
                      (Classical.choose (p := fun (a : R) ↦ (frobenius R p : (a : R) → R) a = xk) ⋯) ⋯)
                  h_1
              else x ^ p ^ (n - m) :
              R))
          (m + 1))
        p =
      (fun (m : ℕ) ↦
          (if h_1 : n ≤ m then
              Nat.leRec (motive := fun (m : ℕ) (h : n ≤ m) ↦ R) x
                (fun ⦃k : ℕ⦄ (hle : n ≤ k) (xk : R) ↦
                  (fun (x : R) (hx : (frobenius R p : (a : R) → R) x = xk) ↦ x)
                    (Classical.choose (p := fun (a : R) ↦ (frobenius R p : (a : R) → R) a = xk) ⋯) ⋯)
                h_1
            else x ^ p ^ (n - m) :
            R))
        m
refine_2₁ :
  ∀ (h1 : n = m + 1),
    HPow.hPow (α := R)
        ((fun (m : ℕ) ↦
            (if h_1 : n ≤ m then
                Nat.leRec (motive := fun (m : ℕ) (h : n ≤ m) ↦ R) x
                  (fun ⦃k : ℕ⦄ (hle : n ≤ k) (xk : R) ↦
                    (fun (x : R) (hx : (frobenius R p : (a : R) → R) x = xk) ↦ x)
                      (Classical.choose (p := fun (a : R) ↦ (frobenius R p : (a : R) → R) a = xk) ⋯) ⋯)
                  h_1
              else x ^ p ^ (n - m) :
              R))
          (m + 1))
        p =
      (fun (m : ℕ) ↦
          (if h_1 : n ≤ m then
              Nat.leRec (motive := fun (m : ℕ) (h : n ≤ m) ↦ R) x
                (fun ⦃k : ℕ⦄ (hle : n ≤ k) (xk : R) ↦
                  (fun (x : R) (hx : (frobenius R p : (a : R) → R) x = xk) ↦ x)
                    (Classical.choose (p := fun (a : R) ↦ (frobenius R p : (a : R) → R) a = xk) ⋯) ⋯)
                h_1
            else x ^ p ^ (n - m) :
            R))
        m
⊢ HPow.hPow (α := R)
      ((fun (m : ℕ) ↦
          (if h_1 : n ≤ m then
              Nat.leRec (motive := fun (m : ℕ) (h : n ≤ m) ↦ R) x
                (fun ⦃k : ℕ⦄ (hle : n ≤ k) (xk : R) ↦
                  (fun (x : R) (hx : (frobenius R p : (a : R) → R) x = xk) ↦ x)
                    (Classical.choose (p := fun (a : R) ↦ (frobenius R p : (a : R) → R) a = xk) ⋯) ⋯)
                h_1
            else x ^ p ^ (n - m) :
            R))
        (m + 1))
      p =
    (fun (m : ℕ) ↦
        (if h_1 : n ≤ m then
            Nat.leRec (motive := fun (m : ℕ) (h : n ≤ m) ↦ R) x
              (fun ⦃k : ℕ⦄ (hle : n ≤ k) (xk : R) ↦
                (fun (x : R) (hx : (frobenius R p : (a : R) → R) x = xk) ↦ x)
                  (Classical.choose (p := fun (a : R) ↦ (frobenius R p : (a : R) → R) a = xk) ⋯) ⋯)
              h_1
          else x ^ p ^ (n - m) :
          R))
      m
have refine_2₂ : ∀ (h1 : ¬n ≤ m + 1),
  HPow.hPow (α := R)
      ((fun (m : ℕ) ↦
          (if h_1 : n ≤ m then
              Nat.leRec (motive := fun (m : ℕ) (h : n ≤ m) ↦ R) x
                (fun ⦃k : ℕ⦄ (hle : n ≤ k) (xk : R) ↦
                  (fun (x : R) (hx : (frobenius R p : (a : R) → R) x = xk) ↦ x)
                    (Classical.choose (p := fun (a : R) ↦ (frobenius R p : (a : R) → R) a = xk) sorry) sorry)
                h_1
            else x ^ p ^ (n - m) :
            R))
        (m + 1))
      p =
    (fun (m : ℕ) ↦
        (if h_1 : n ≤ m then
            Nat.leRec (motive := fun (m : ℕ) (h : n ≤ m) ↦ R) x
              (fun ⦃k : ℕ⦄ (hle : n ≤ k) (xk : R) ↦
                (fun (x : R) (hx : (frobenius R p : (a : R) → R) x = xk) ↦ x)
                  (Classical.choose (p := fun (a : R) ↦ (frobenius R p : (a : R) → R) a = xk) sorry) sorry)
              h_1
          else x ^ p ^ (n - m) :
          R))
      m
Tactic: obtain (h1 | h1 | h1) : n ≤ m ∨ n = m + 1 ∨ ¬ n ≤ m + 1 := by lia