m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
⊢ (if h : ↑castSucc j < i then
      (_ : ↑(succAbove i) (castLT (↑(succAbove i) j) (_ : ↑(↑(succAbove i) j) < n)) = ↑(succAbove i) j) ▸
        p (castLT (↑(succAbove i) j) (_ : ↑(↑(succAbove i) j) < n))
    else
      (_ : ↑(succAbove i) (pred (↑(succAbove i) j) (_ : ↑(succAbove i) j ≠ 0)) = ↑(succAbove i) j) ▸
        p (pred (↑(succAbove i) j) (_ : ↑(succAbove i) j ≠ 0))) =
    p j
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
⊢ insertNth i x p (↑(succAbove i) j) = p j
simp only [insertNth, succAboveCases, dif_neg (succAbove_ne _ _), succAbove_lt_iff]
case inl
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
hlt : ↑castSucc j < i
⊢ (_ : ↑(succAbove i) (castLT (↑(succAbove i) j) (_ : ↑(↑(succAbove i) j) < n)) = ↑(succAbove i) j) ▸
      p (castLT (↑(succAbove i) j) (_ : ↑(↑(succAbove i) j) < n)) =
    p j

case inr
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
hlt : ¬↑castSucc j < i
⊢ (_ : ↑(succAbove i) (pred (↑(succAbove i) j) (_ : ↑(succAbove i) j ≠ 0)) = ↑(succAbove i) j) ▸
      p (pred (↑(succAbove i) j) (_ : ↑(succAbove i) j ≠ 0)) =
    p j
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
⊢ (if h : ↑castSucc j < i then
      (_ : ↑(succAbove i) (castLT (↑(succAbove i) j) (_ : ↑(↑(succAbove i) j) < n)) = ↑(succAbove i) j) ▸
        p (castLT (↑(succAbove i) j) (_ : ↑(↑(succAbove i) j) < n))
    else
      (_ : ↑(succAbove i) (pred (↑(succAbove i) j) (_ : ↑(succAbove i) j ≠ 0)) = ↑(succAbove i) j) ▸
        p (pred (↑(succAbove i) j) (_ : ↑(succAbove i) j ≠ 0))) =
    p j
split_ifs with hlt
case inl
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
hlt : ↑castSucc j < i
H₁ : ↑(↑(succAbove i) j) < n
H₂ : ↑(succAbove i) (castLT (↑(succAbove i) j) (_ : ↑(↑(succAbove i) j) < n)) = ↑(succAbove i) j
⊢ H₂ ▸ p (castLT (↑(succAbove i) j) H₁) = p j
case inl
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
hlt : ↑castSucc j < i
⊢ (_ : ↑(succAbove i) (castLT (↑(succAbove i) j) (_ : ↑(↑(succAbove i) j) < n)) = ↑(succAbove i) j) ▸
      p (castLT (↑(succAbove i) j) (_ : ↑(↑(succAbove i) j) < n)) =
    p j
generalize_proofs H₁ H₂
case inl
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
hlt : ↑castSucc j < i
H₁ : ↑(↑(succAbove i) j) < n
⊢ ∀ (H₂ : ↑(succAbove i) (castLT (↑(succAbove i) j) (_ : ↑(↑(succAbove i) j) < n)) = ↑(succAbove i) j),
    H₂ ▸ p (castLT (↑(succAbove i) j) H₁) = p j
case inl
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
hlt : ↑castSucc j < i
H₁ : ↑(↑(succAbove i) j) < n
H₂ : ↑(succAbove i) (castLT (↑(succAbove i) j) (_ : ↑(↑(succAbove i) j) < n)) = ↑(succAbove i) j
⊢ H₂ ▸ p (castLT (↑(succAbove i) j) H₁) = p j
revert H₂
case inl
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
hlt : ↑castSucc j < i
H₁ : ↑(↑(succAbove i) j) < n
k : Fin n
hk : castLT (↑(succAbove i) j) H₁ = k
⊢ ∀ (H₂ : ↑(succAbove i) k = ↑(succAbove i) j), H₂ ▸ p k = p j
case inl
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
hlt : ↑castSucc j < i
H₁ : ↑(↑(succAbove i) j) < n
⊢ ∀ (H₂ : ↑(succAbove i) (castLT (↑(succAbove i) j) (_ : ↑(↑(succAbove i) j) < n)) = ↑(succAbove i) j),
    H₂ ▸ p (castLT (↑(succAbove i) j) H₁) = p j
generalize hk : castLT ((succAbove i) j) H₁ = k
case inl
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
hlt : ↑castSucc j < i
H₁ : ↑(↑(succAbove i) j) < n
k : Fin n
hk : j = k
⊢ ∀ (H₂ : ↑(succAbove i) k = ↑(succAbove i) j), H₂ ▸ p k = p j
case inl
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
hlt : ↑castSucc j < i
H₁ : ↑(↑(succAbove i) j) < n
k : Fin n
hk : castLT (↑(succAbove i) j) H₁ = k
⊢ ∀ (H₂ : ↑(succAbove i) k = ↑(succAbove i) j), H₂ ▸ p k = p j
rw [castLT_succAbove hlt] at hk
case inl.refl
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
hlt : ↑castSucc j < i
H₁ : ↑(↑(succAbove i) j) < n
⊢ ∀ (H₂ : ↑(succAbove i) j = ↑(succAbove i) j), H₂ ▸ p j = p j
case inl
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
hlt : ↑castSucc j < i
H₁ : ↑(↑(succAbove i) j) < n
k : Fin n
hk : j = k
⊢ ∀ (H₂ : ↑(succAbove i) k = ↑(succAbove i) j), H₂ ▸ p k = p j
cases hk
case inl.refl
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
hlt : ↑castSucc j < i
H₁ : ↑(↑(succAbove i) j) < n
H₂✝ : ↑(succAbove i) j = ↑(succAbove i) j
⊢ H₂✝ ▸ p j = p j
case inl.refl
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
hlt : ↑castSucc j < i
H₁ : ↑(↑(succAbove i) j) < n
⊢ ∀ (H₂ : ↑(succAbove i) j = ↑(succAbove i) j), H₂ ▸ p j = p j
intro
no goals
case inl.refl
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
hlt : ↑castSucc j < i
H₁ : ↑(↑(succAbove i) j) < n
H₂✝ : ↑(succAbove i) j = ↑(succAbove i) j
⊢ H₂✝ ▸ p j = p j
rfl
case inr
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
hlt : ¬↑castSucc j < i
H₁ : ↑(succAbove i) j ≠ 0
H₂ : ↑(succAbove i) (pred (↑(succAbove i) j) (_ : ↑(succAbove i) j ≠ 0)) = ↑(succAbove i) j
⊢ H₂ ▸ p (pred (↑(succAbove i) j) H₁) = p j
case inr
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
hlt : ¬↑castSucc j < i
⊢ (_ : ↑(succAbove i) (pred (↑(succAbove i) j) (_ : ↑(succAbove i) j ≠ 0)) = ↑(succAbove i) j) ▸
      p (pred (↑(succAbove i) j) (_ : ↑(succAbove i) j ≠ 0)) =
    p j
generalize_proofs H₁ H₂
case inr
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
hlt : ¬↑castSucc j < i
H₁ : ↑(succAbove i) j ≠ 0
⊢ ∀ (H₂ : ↑(succAbove i) (pred (↑(succAbove i) j) (_ : ↑(succAbove i) j ≠ 0)) = ↑(succAbove i) j),
    H₂ ▸ p (pred (↑(succAbove i) j) H₁) = p j
case inr
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
hlt : ¬↑castSucc j < i
H₁ : ↑(succAbove i) j ≠ 0
H₂ : ↑(succAbove i) (pred (↑(succAbove i) j) (_ : ↑(succAbove i) j ≠ 0)) = ↑(succAbove i) j
⊢ H₂ ▸ p (pred (↑(succAbove i) j) H₁) = p j
revert H₂
case inr
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
hlt : ¬↑castSucc j < i
H₁ : ↑(succAbove i) j ≠ 0
k : Fin n
hk : pred (↑(succAbove i).toEmbedding j) H₁ = k
⊢ ∀ (H₂ : ↑(succAbove i) k = ↑(succAbove i) j), H₂ ▸ p k = p j
case inr
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
hlt : ¬↑castSucc j < i
H₁ : ↑(succAbove i) j ≠ 0
⊢ ∀ (H₂ : ↑(succAbove i) (pred (↑(succAbove i) j) (_ : ↑(succAbove i) j ≠ 0)) = ↑(succAbove i) j),
    H₂ ▸ p (pred (↑(succAbove i) j) H₁) = p j
generalize hk : pred ((succAbove i).toEmbedding j) H₁ = k
case inr
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
hlt : ¬↑castSucc j < i
H₁ : ↑(succAbove i) j ≠ 0
k : Fin n
hk : j = k
⊢ ∀ (H₂ : ↑(succAbove i) k = ↑(succAbove i) j), H₂ ▸ p k = p j
case inr
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
hlt : ¬↑castSucc j < i
H₁ : ↑(succAbove i) j ≠ 0
k : Fin n
hk : pred (↑(succAbove i).toEmbedding j) H₁ = k
⊢ ∀ (H₂ : ↑(succAbove i) k = ↑(succAbove i) j), H₂ ▸ p k = p j
erw [pred_succAbove (le_of_not_lt hlt)] at hk
case inr.refl
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
hlt : ¬↑castSucc j < i
H₁ : ↑(succAbove i) j ≠ 0
⊢ ∀ (H₂ : ↑(succAbove i) j = ↑(succAbove i) j), H₂ ▸ p j = p j
case inr
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
hlt : ¬↑castSucc j < i
H₁ : ↑(succAbove i) j ≠ 0
k : Fin n
hk : j = k
⊢ ∀ (H₂ : ↑(succAbove i) k = ↑(succAbove i) j), H₂ ▸ p k = p j
cases hk
case inr.refl
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
hlt : ¬↑castSucc j < i
H₁ : ↑(succAbove i) j ≠ 0
H₂✝ : ↑(succAbove i) j = ↑(succAbove i) j
⊢ H₂✝ ▸ p j = p j
case inr.refl
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
hlt : ¬↑castSucc j < i
H₁ : ↑(succAbove i) j ≠ 0
⊢ ∀ (H₂ : ↑(succAbove i) j = ↑(succAbove i) j), H₂ ▸ p j = p j
intro
no goals
case inr.refl
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (↑(succAbove i) j)
j : Fin n
hlt : ¬↑castSucc j < i
H₁ : ↑(succAbove i) j ≠ 0
H₂✝ : ↑(succAbove i) j = ↑(succAbove i) j
⊢ H₂✝ ▸ p j = p j
rfl