-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem snoc_update : snoc (update p i y) x = update (snoc p x) i.castSucc 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
E : j.castLT h = i
⊢ False

Tactic:
apply h'

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
⊢ j = i.castSucc

Proof state:
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

Tactic:
by_cases h : j.val < n

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
⊢ snoc (update p i y) x j = 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
⊢ snoc (update p i y) x j = 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
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

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
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

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
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
e_5✝ : i = j.castLT h
⊢ HEq y (cast C2 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
h' : j = i.castSucc
⊢ cast ⋯ (update p i y (j.castLT ⋯)) = update (snoc p x) i.castSucc y j

Tactic:
have C1 : α i.castSucc = α j := by rw [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
h' : j = i.castSucc
C1 : α i.castSucc = α j
⊢ cast ⋯ (update p i y (j.castLT ⋯)) = update (snoc p x) i.castSucc y j

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
this : update (snoc p x) j (cast C1 y) j = cast C1 y
⊢ i.castSucc = j

Tactic:
exact h'.symm

Result:
no goals

Proof state:
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
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
e_5✝ : i = j.castLT h
⊢ HEq y (cast C2 y)

Tactic:
exact heq_of_cast_eq C2 rfl

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
⊢ update (snoc p x) i.castSucc y j = cast C1 y

Tactic:
have : update (snoc p x) j (_root_.cast C1 y) j = _root_.cast C1 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
this : update (snoc p x) j (cast C1 y) j = cast C1 y
⊢ update (snoc p x) i.castSucc y j = 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
⊢ snoc (update p i y) x j = update (snoc p x) i.castSucc y j

Tactic:
rw [eq_last_of_not_lt h]

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
⊢ snoc (update p i y) x (last n) = update (snoc p x) i.castSucc y (last n)

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
⊢ α i.castSucc = α (j.castLT h).castSucc

Tactic:
rw [castSucc_castLT, 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
h' : j = i.castSucc
C1 : α i.castSucc = α j
E1 : update (snoc p x) i.castSucc y j = cast C1 y
⊢ cast ⋯ (update p i y (j.castLT ⋯)) = update (snoc p x) i.castSucc y j

Tactic:
have C2 : α i.castSucc = α (castLT j h).castSucc := by rw [castSucc_castLT, 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
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
⊢ 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
⊢ α i.castSucc = α j

Tactic:
rw [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
E : j.castLT h = i
⊢ j = i.castSucc

Tactic:
rw [← E, castSucc_castLT]

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
⊢ snoc (update p i y) x j = update (snoc p x) i.castSucc y j

Tactic:
rw [snoc]

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 : ↑j < n then cast ⋯ (update p i y (j.castLT h)) else cast ⋯ x) = update (snoc p x) i.castSucc y j

Proof state:
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)

Tactic:
exact heq_of_cast_eq (congr_arg α (Eq.symm h')) rfl

Result:
no goals