-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Iterate.lean
theorem hIterateFrom_elim {P : Nat → Sort _}(Q : ∀(i : Nat), P i → Prop)
    {n  : Nat}
    (f : ∀(i : Fin n), P i.val → P (i.val+1))
    {i : Nat} (ubnd : i ≤ n)
    (s : P i)
    (init : Q i s)
    (step : ∀(k : Fin n) (s : P k.val), Q k.val s → Q (k.val+1) (f k s)) :
    Q n (hIterateFrom P f i ubnd s)

Proof state:
case zero
P : Nat → Sort u_1
Q : (i : Nat) → P i → Prop
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
step : ∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)
i : Nat
ubnd : i ≤ n
s : P i
init : Q i s
p : i + 0 = n
⊢ Q n
    (if g : i < n then hIterateFrom P f (i + 1) g (f ⟨i, g⟩ s)
    else
      let_fun p := ⋯;
      cast ⋯ s)

Tactic:
have g : ¬ (i < n) := by simp at p; simp [p]

Result:
case zero
P : Nat → Sort u_1
Q : (i : Nat) → P i → Prop
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
step : ∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)
i : Nat
ubnd : i ≤ n
s : P i
init : Q i s
p : i + 0 = n
g : ¬i < n
⊢ Q n
    (if g : i < n then hIterateFrom P f (i + 1) g (f ⟨i, g⟩ s)
    else
      let_fun p := ⋯;
      cast ⋯ s)

Proof state:
case zero
P : Nat → Sort u_1
Q : (i : Nat) → P i → Prop
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
step : ∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)
i : Nat
ubnd : i ≤ n
s : P i
init : Q i s
p : i + 0 = n
⊢ Q n (hIterateFrom P f i ubnd s)

Tactic:
unfold hIterateFrom

Result:
case zero
P : Nat → Sort u_1
Q : (i : Nat) → P i → Prop
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
step : ∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)
i : Nat
ubnd : i ≤ n
s : P i
init : Q i s
p : i + 0 = n
⊢ Q n
    (if g : i < n then hIterateFrom P f (i + 1) g (f ⟨i, g⟩ s)
    else
      let_fun p := ⋯;
      cast ⋯ s)

Proof state:
case succ
P : Nat → Sort u_1
Q : (i : Nat) → P i → Prop
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
step : ∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)
j : Nat
inv : ∀ {i : Nat} (ubnd : i ≤ n) (s : P i), Q i s → i + j = n → Q n (hIterateFrom P f i ubnd s)
i : Nat
ubnd : i ≤ n
s : P i
init : Q i s
p : i + (j + 1) = n
d : i.succ + j = n
g : i < n
⊢ Q n
    (if g : i < n then hIterateFrom P f (i + 1) g (f ⟨i, g⟩ s)
    else
      let_fun p := ⋯;
      cast ⋯ s)

Tactic:
simp only [g]

Result:
case succ
P : Nat → Sort u_1
Q : (i : Nat) → P i → Prop
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
step : ∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)
j : Nat
inv : ∀ {i : Nat} (ubnd : i ≤ n) (s : P i), Q i s → i + j = n → Q n (hIterateFrom P f i ubnd s)
i : Nat
ubnd : i ≤ n
s : P i
init : Q i s
p : i + (j + 1) = n
d : i.succ + j = n
g : i < n
⊢ Q n (if h : True then hIterateFrom P f (i + 1) ⋯ (f ⟨i, ⋯⟩ s) else cast ⋯ s)

Proof state:
case zero
P : Nat → Sort u_1
Q : (i : Nat) → P i → Prop
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
step : ∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)
i : Nat
ubnd : i ≤ n
s : P i
init : Q i s
p : i + 0 = n
g : ¬i < n
⊢ Q n
    (if g : i < n then hIterateFrom P f (i + 1) g (f ⟨i, g⟩ s)
    else
      let_fun p := ⋯;
      cast ⋯ s)

Tactic:
have r : Q n (_root_.cast (congrArg P p) s) :=
  @Eq.rec Nat i (fun k eq => Q k (_root_.cast (congrArg P eq) s)) init n p

Result:
case zero
P : Nat → Sort u_1
Q : (i : Nat) → P i → Prop
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
step : ∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)
i : Nat
ubnd : i ≤ n
s : P i
init : Q i s
p : i + 0 = n
g : ¬i < n
r : Q n (cast ⋯ s)
⊢ Q n
    (if g : i < n then hIterateFrom P f (i + 1) g (f ⟨i, g⟩ s)
    else
      let_fun p := ⋯;
      cast ⋯ s)

Proof state:
case succ
P : Nat → Sort u_1
Q : (i : Nat) → P i → Prop
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
step : ∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)
j : Nat
inv : ∀ {i : Nat} (ubnd : i ≤ n) (s : P i), Q i s → i + j = n → Q n (hIterateFrom P f i ubnd s)
i : Nat
ubnd : i ≤ n
s : P i
init : Q i s
p : i + (j + 1) = n
d : i.succ + j = n
⊢ Q n
    (if g : i < n then hIterateFrom P f (i + 1) g (f ⟨i, g⟩ s)
    else
      let_fun p := ⋯;
      cast ⋯ s)

Tactic:
have g : i < n := Nat.le.intro d

Result:
case succ
P : Nat → Sort u_1
Q : (i : Nat) → P i → Prop
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
step : ∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)
j : Nat
inv : ∀ {i : Nat} (ubnd : i ≤ n) (s : P i), Q i s → i + j = n → Q n (hIterateFrom P f i ubnd s)
i : Nat
ubnd : i ≤ n
s : P i
init : Q i s
p : i + (j + 1) = n
d : i.succ + j = n
g : i < n
⊢ Q n
    (if g : i < n then hIterateFrom P f (i + 1) g (f ⟨i, g⟩ s)
    else
      let_fun p := ⋯;
      cast ⋯ s)

Proof state:
case succ
P : Nat → Sort u_1
Q : (i : Nat) → P i → Prop
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
step : ∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)
j : Nat
inv : ∀ {i : Nat} (ubnd : i ≤ n) (s : P i), Q i s → i + j = n → Q n (hIterateFrom P f i ubnd s)
i : Nat
ubnd : i ≤ n
s : P i
init : Q i s
p : i + (j + 1) = n
⊢ Q n (hIterateFrom P f i ubnd s)

Tactic:
unfold hIterateFrom

Result:
case succ
P : Nat → Sort u_1
Q : (i : Nat) → P i → Prop
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
step : ∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)
j : Nat
inv : ∀ {i : Nat} (ubnd : i ≤ n) (s : P i), Q i s → i + j = n → Q n (hIterateFrom P f i ubnd s)
i : Nat
ubnd : i ≤ n
s : P i
init : Q i s
p : i + (j + 1) = n
⊢ Q n
    (if g : i < n then hIterateFrom P f (i + 1) g (f ⟨i, g⟩ s)
    else
      let_fun p := ⋯;
      cast ⋯ s)

Proof state:
P : Nat → Sort u_1
Q : (i : Nat) → P i → Prop
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
step : ∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)
j : Nat
inv : ∀ {i : Nat} (ubnd : i ≤ n) (s : P i), Q i s → i + j = n → Q n (hIterateFrom P f i ubnd s)
i : Nat
ubnd : i ≤ n
s : P i
init : Q i s
p : i + (j + 1) = n
⊢ i.succ + j = n

Tactic:
simp [Nat.succ_add]

Result:
P : Nat → Sort u_1
Q : (i : Nat) → P i → Prop
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
step : ∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)
j : Nat
inv : ∀ {i : Nat} (ubnd : i ≤ n) (s : P i), Q i s → i + j = n → Q n (hIterateFrom P f i ubnd s)
i : Nat
ubnd : i ≤ n
s : P i
init : Q i s
p : i + (j + 1) = n
⊢ i + j + 1 = n

Proof state:
P : Nat → Sort u_1
Q : (i : Nat) → P i → Prop
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
step : ∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)
i : Nat
ubnd : i ≤ n
s : P i
init : Q i s
p : i + 0 = n
⊢ ¬i < n

Tactic:
simp at p

Result:
P : Nat → Sort u_1
Q : (i : Nat) → P i → Prop
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
step : ∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)
i : Nat
ubnd : i ≤ n
s : P i
init : Q i s
p : i = n
⊢ ¬i < n

Proof state:
P : Nat → Sort u_1
Q : (i : Nat) → P i → Prop
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
step : ∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)
j : Nat
inv : ∀ {i : Nat} (ubnd : i ≤ n) (s : P i), Q i s → i + j = n → Q n (hIterateFrom P f i ubnd s)
i : Nat
ubnd : i ≤ n
s : P i
init : Q i s
p : i + (j + 1) = n
⊢ i + j + 1 = n

Tactic:
exact p

Result:
no goals

Proof state:
P : Nat → Sort u_1
Q : (i : Nat) → P i → Prop
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
step : ∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)
i : Nat
ubnd : i ≤ n
s : P i
init : Q i s
p : i = n
⊢ ¬i < n

Tactic:
simp [p]

Result:
no goals