-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem snoc_update : snoc (update p i y) x = update (snoc p x) i.castSucc y

Proof state:
case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin (n + 1)
h : ↑j < n
⊢ (if h : ↑j < n then cast ⋯ (update p i y (j.castLT h)) else cast ⋯ x) = update (snoc p x) i.castSucc y j

Tactic:
simp only [h]

Result:
case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin (n + 1)
h : ↑j < n
⊢ (if h_1 : True then cast ⋯ (update p i y (j.castLT ⋯)) else cast ⋯ x) = update (snoc p x) i.castSucc y j

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin (n + 1)
h : ↑j < n
h' : j = i.castSucc
C1 : α i.castSucc = α j
E1 : update (snoc p x) i.castSucc y j = cast C1 y
C2 : α i.castSucc = α (j.castLT h).castSucc
⊢ update p i y (j.castLT h) = cast C2 y

Tactic:
have : update p (castLT j h) (_root_.cast C2 y) (castLT j h) = _root_.cast C2 y := by simp

Result:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin (n + 1)
h : ↑j < n
h' : j = i.castSucc
C1 : α i.castSucc = α j
E1 : update (snoc p x) i.castSucc y j = cast C1 y
C2 : α i.castSucc = α (j.castLT h).castSucc
this : update p (j.castLT h) (cast C2 y) (j.castLT h) = cast C2 y
⊢ update p i y (j.castLT h) = cast C2 y

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin (n + 1)
h : ↑j < n
h' : j = i.castSucc
C1 : α i.castSucc = α j
⊢ update (snoc p x) j (cast C1 y) j = cast C1 y

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
⊢ snoc (update p i y) x = update (snoc p x) i.castSucc y

Tactic:
ext j

Result:
case h
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin (n + 1)
⊢ snoc (update p i y) x j = update (snoc p x) i.castSucc y j

Proof state:
case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin (n + 1)
h : ↑j < n
h' : ¬j = i.castSucc
this : ¬j.castLT h = i
⊢ cast ⋯ (update p i y (j.castLT ⋯)) = update (snoc p x) i.castSucc y j

Tactic:
simp [h', this, snoc, h]

Result:
no goals

Proof state:
case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin (n + 1)
h : ↑j < n
⊢ cast ⋯ (update p i y (j.castLT ⋯)) = update (snoc p x) i.castSucc y j

Tactic:
by_cases h' : j = castSucc i

Result:
case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin (n + 1)
h : ↑j < n
h' : j = i.castSucc
⊢ cast ⋯ (update p i y (j.castLT ⋯)) = update (snoc p x) i.castSucc y j

case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin (n + 1)
h : ↑j < n
h' : ¬j = i.castSucc
⊢ cast ⋯ (update p i y (j.castLT ⋯)) = update (snoc p x) i.castSucc y j

Proof state:
case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin (n + 1)
h : ↑j < n
h' : j = i.castSucc
C1 : α i.castSucc = α j
E1 : update (snoc p x) i.castSucc y j = cast C1 y
C2 : α i.castSucc = α (j.castLT h).castSucc
E2 : update p i y (j.castLT h) = cast C2 y
⊢ cast ⋯ (cast C2 y) = cast C1 y

Tactic:
rfl

Result:
no goals

Proof state:
case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin (n + 1)
h : ↑j < n
h' : j = i.castSucc
C1 : α i.castSucc = α j
E1 : update (snoc p x) i.castSucc y j = cast C1 y
C2 : α i.castSucc = α (j.castLT h).castSucc
E2 : update p i y (j.castLT h) = cast C2 y
⊢ cast ⋯ (update p i y (j.castLT ⋯)) = update (snoc p x) i.castSucc y j

Tactic:
rw [E1, E2]

Result:
case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin (n + 1)
h : ↑j < n
h' : j = i.castSucc
C1 : α i.castSucc = α j
E1 : update (snoc p x) i.castSucc y j = cast C1 y
C2 : α i.castSucc = α (j.castLT h).castSucc
E2 : update p i y (j.castLT h) = cast C2 y
⊢ cast ⋯ (cast C2 y) = cast C1 y

Proof state:
case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin (n + 1)
h : ↑j < n
⊢ (if h_1 : True then cast ⋯ (update p i y (j.castLT ⋯)) else cast ⋯ x) = update (snoc p x) i.castSucc y j

Tactic:
simp only [dif_pos]

Result:
case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin (n + 1)
h : ↑j < n
⊢ cast ⋯ (update p i y (j.castLT ⋯)) = update (snoc p x) i.castSucc y j

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin (n + 1)
h : ↑j < n
h' : ¬j = i.castSucc
⊢ ¬j.castLT h = i

Tactic:
intro E

Result:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin (n + 1)
h : ↑j < n
h' : ¬j = i.castSucc
E : j.castLT h = i
⊢ False

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin (n + 1)
h : ↑j < n
h' : j = i.castSucc
C1 : α i.castSucc = α j
this : update (snoc p x) j (cast C1 y) j = cast C1 y
⊢ update (snoc p x) i.castSucc y j = cast C1 y

Tactic:
convert this

Result:
case h.e'_2.h.e'_5
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin (n + 1)
h : ↑j < n
h' : j = i.castSucc
C1 : α i.castSucc = α j
this : update (snoc p x) j (cast C1 y) j = cast C1 y
⊢ i.castSucc = j

case h.e'_2.h.e'_6
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin (n + 1)
h : ↑j < n
h' : j = i.castSucc
C1 : α i.castSucc = α j
this : update (snoc p x) j (cast C1 y) j = cast C1 y
e_5✝ : i.castSucc = j
⊢ HEq y (cast C1 y)

Proof state:
case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin (n + 1)
h : ↑j < n
h' : ¬j = i.castSucc
⊢ cast ⋯ (update p i y (j.castLT ⋯)) = update (snoc p x) i.castSucc y j

Tactic:
have : ¬castLT j h = i := by
  intro E
  apply h'
  rw [← E, castSucc_castLT]

Result:
case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin (n + 1)
h : ↑j < n
h' : ¬j = i.castSucc
this : ¬j.castLT h = i
⊢ cast ⋯ (update p i y (j.castLT ⋯)) = update (snoc p x) i.castSucc y j

Proof state:
case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin (n + 1)
h : ¬↑j < n
⊢ snoc (update p i y) x (last n) = update (snoc p x) i.castSucc y (last n)

Tactic:
simp [Fin.ne_of_gt i.castSucc_lt_last]

Result:
no goals

Proof state:
case h.e'_2.h.e'_5
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin (n + 1)
h : ↑j < n
h' : j = i.castSucc
C1 : α i.castSucc = α j
E1 : update (snoc p x) i.castSucc y j = cast C1 y
C2 : α i.castSucc = α (j.castLT h).castSucc
this : update p (j.castLT h) (cast C2 y) (j.castLT h) = cast C2 y
⊢ i = j.castLT h

Tactic:
simp [h, h']

Result:
no goals

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin (n + 1)
h : ↑j < n
h' : j = i.castSucc
C1 : α i.castSucc = α j
E1 : update (snoc p x) i.castSucc y j = cast C1 y
C2 : α i.castSucc = α (j.castLT h).castSucc
⊢ update p (j.castLT h) (cast C2 y) (j.castLT h) = cast C2 y

Tactic:
simp

Result:
no goals