-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem cons_update : cons x (update p i y) = update (cons x p) i.succ y

Proof state:
case pos
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
h' : j' = i
⊢ update p i y i = update (cons x p) i.succ y i.succ

Tactic:
simp

Result:
no goals

Proof state:
case pos
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
j : Fin (n + 1)
h : j = 0
⊢ cons x (update p i y) j = update (cons x p) i.succ y j

Tactic:
rw [h]

Result:
case pos
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
j : Fin (n + 1)
h : j = 0
⊢ cons x (update p i y) 0 = update (cons x p) i.succ y 0

Proof state:
case neg
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
j : Fin (n + 1)
h : ¬j = 0
⊢ cons x (update p i y) j = update (cons x p) i.succ y j

Tactic:
let j' := pred j h

Result:
case neg
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
⊢ cons x (update p i y) j = update (cons x p) i.succ y j

Proof state:
case pos
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
h' : j' = i
⊢ update p i y j' = update (cons x p) i.succ y j'.succ

Tactic:
rw [h']

Result:
case pos
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
h' : j' = i
⊢ update p i y i = update (cons x p) i.succ y i.succ

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
⊢ cons x (update p i y) = update (cons x p) i.succ y

Tactic:
ext j

Result:
case h
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
j : Fin (n + 1)
⊢ cons x (update p i y) j = update (cons x p) i.succ y j

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
h' : ¬j' = i
⊢ j'.succ ≠ i.succ

Tactic:
rwa [Ne, succ_inj]

Result:
no goals

Proof state:
case pos
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
j : Fin (n + 1)
h : j = 0
⊢ cons x (update p i y) 0 = update (cons x p) i.succ y 0

Tactic:
simp [Ne.symm (succ_ne_zero i)]

Result:
no goals

Proof state:
case neg
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
⊢ cons x (update p i y) j = update (cons x p) i.succ y j

Tactic:
have : j'.succ = j := succ_pred j h

Result:
case neg
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
⊢ cons x (update p i y) j = update (cons x p) i.succ y j

Proof state:
case neg
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
h' : ¬j' = i
⊢ update p i y j' = update (cons x p) i.succ y j'.succ

Tactic:
have : j'.succ ≠ i.succ := by rwa [Ne, succ_inj]

Result:
case neg
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this✝ : j'.succ = j
h' : ¬j' = i
this : j'.succ ≠ i.succ
⊢ update p i y j' = update (cons x p) i.succ y j'.succ

Proof state:
case neg
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
⊢ cons x (update p i y) j = update (cons x p) i.succ y j

Tactic:
rw [← this, cons_succ]

Result:
case neg
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
⊢ update p i y j' = update (cons x p) i.succ y j'.succ

Proof state:
case h
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
j : Fin (n + 1)
⊢ cons x (update p i y) j = update (cons x p) i.succ y j

Tactic:
by_cases h : j = 0

Result:
case pos
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
j : Fin (n + 1)
h : j = 0
⊢ cons x (update p i y) j = update (cons x p) i.succ y j

case neg
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
j : Fin (n + 1)
h : ¬j = 0
⊢ cons x (update p i y) j = update (cons x p) i.succ y j

Proof state:
case neg
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
⊢ update p i y j' = update (cons x p) i.succ y j'.succ

Tactic:
by_cases h' : j' = i

Result:
case pos
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
h' : j' = i
⊢ update p i y j' = update (cons x p) i.succ y j'.succ

case neg
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
h' : ¬j' = i
⊢ update p i y j' = update (cons x p) i.succ y j'.succ

Proof state:
case neg
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this✝ : j'.succ = j
h' : ¬j' = i
this : j'.succ ≠ i.succ
⊢ update p i y j' = update (cons x p) i.succ y j'.succ

Tactic:
rw [update_of_ne h', update_of_ne this, cons_succ]

Result:
no goals