[GOAL]
m n : ℕ
α : Fin 0 → Sort u
⊢ Unique ((i : Fin 0) → α i)
[PROOFSTEP]
infer_instance
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
⊢ tail (cons x p) = p
[PROOFSTEP]
simp [tail, cons]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
⊢ cons x p (succ i) = p i
[PROOFSTEP]
simp [cons]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
⊢ cons x p 0 = x
[PROOFSTEP]
simp [cons]
[GOAL]
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p✝ : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Fin (n + 2) → Type u_1
x : α 0
p : (i : Fin (Nat.succ n)) → α (succ i)
⊢ cons x p 1 = p 0
[PROOFSTEP]
rw [← cons_succ x p]
[GOAL]
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p✝ : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Fin (n + 2) → Type u_1
x : α 0
p : (i : Fin (Nat.succ n)) → α (succ i)
⊢ cons x p 1 = cons x p (succ 0)
[PROOFSTEP]
rfl
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
⊢ cons x (update p i y) = update (cons x p) (succ i) y
[PROOFSTEP]
ext j
[GOAL]
case h
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
⊢ cons x (update p i y) j = update (cons x p) (succ i) y j
[PROOFSTEP]
by_cases h : j = 0
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : j = 0
⊢ cons x (update p i y) j = update (cons x p) (succ i) y j
[PROOFSTEP]
rw [h]
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : j = 0
⊢ cons x (update p i y) 0 = update (cons x p) (succ i) y 0
[PROOFSTEP]
simp [Ne.symm (succ_ne_zero i)]
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : ¬j = 0
⊢ cons x (update p i y) j = update (cons x p) (succ i) y j
[PROOFSTEP]
let j' := pred j h
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := pred j h
⊢ cons x (update p i y) j = update (cons x p) (succ i) y j
[PROOFSTEP]
have : j'.succ = j := succ_pred j h
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := pred j h
this : succ j' = j
⊢ cons x (update p i y) j = update (cons x p) (succ i) y j
[PROOFSTEP]
rw [← this, cons_succ]
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := pred j h
this : succ j' = j
⊢ update p i y j' = update (cons x p) (succ i) y (succ j')
[PROOFSTEP]
by_cases h' : j' = i
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := pred j h
this : succ j' = j
h' : j' = i
⊢ update p i y j' = update (cons x p) (succ i) y (succ j')
[PROOFSTEP]
rw [h']
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := pred j h
this : succ j' = j
h' : j' = i
⊢ update p i y i = update (cons x p) (succ i) y (succ i)
[PROOFSTEP]
simp
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := pred j h
this : succ j' = j
h' : ¬j' = i
⊢ update p i y j' = update (cons x p) (succ i) y (succ j')
[PROOFSTEP]
have : j'.succ ≠ i.succ := by rwa [Ne.def, succ_inj]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := pred j h
this : succ j' = j
h' : ¬j' = i
⊢ succ j' ≠ succ i
[PROOFSTEP]
rwa [Ne.def, succ_inj]
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := pred j h
this✝ : succ j' = j
h' : ¬j' = i
this : succ j' ≠ succ i
⊢ update p i y j' = update (cons x p) (succ i) y (succ j')
[PROOFSTEP]
rw [update_noteq h', update_noteq this, cons_succ]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x✝ : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i✝ : Fin n
y✝ : α (succ i✝)
z x₀ y₀ : α 0
x y : (i : Fin n) → α (succ i)
h : cons x₀ x = cons y₀ y
i : Fin n
⊢ x i = y i
[PROOFSTEP]
simpa using congr_fun h (Fin.succ i)
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
⊢ update (cons x p) 0 z = cons z p
[PROOFSTEP]
ext j
[GOAL]
case h
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
⊢ update (cons x p) 0 z j = cons z p j
[PROOFSTEP]
by_cases h : j = 0
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : j = 0
⊢ update (cons x p) 0 z j = cons z p j
[PROOFSTEP]
rw [h]
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : j = 0
⊢ update (cons x p) 0 z 0 = cons z p 0
[PROOFSTEP]
simp
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : ¬j = 0
⊢ update (cons x p) 0 z j = cons z p j
[PROOFSTEP]
simp only [h, update_noteq, Ne.def, not_false_iff]
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : ¬j = 0
⊢ cons x p j = cons z p j
[PROOFSTEP]
let j' := pred j h
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := pred j h
⊢ cons x p j = cons z p j
[PROOFSTEP]
have : j'.succ = j := succ_pred j h
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := pred j h
this : succ j' = j
⊢ cons x p j = cons z p j
[PROOFSTEP]
rw [← this, cons_succ, cons_succ]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
⊢ cons (q 0) (tail q) = q
[PROOFSTEP]
ext j
[GOAL]
case h
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
⊢ cons (q 0) (tail q) j = q j
[PROOFSTEP]
by_cases h : j = 0
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : j = 0
⊢ cons (q 0) (tail q) j = q j
[PROOFSTEP]
rw [h]
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : j = 0
⊢ cons (q 0) (tail q) 0 = q 0
[PROOFSTEP]
simp
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : ¬j = 0
⊢ cons (q 0) (tail q) j = q j
[PROOFSTEP]
let j' := pred j h
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := pred j h
⊢ cons (q 0) (tail q) j = q j
[PROOFSTEP]
have : j'.succ = j := succ_pred j h
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := pred j h
this : succ j' = j
⊢ cons (q 0) (tail q) j = q j
[PROOFSTEP]
rw [← this]
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := pred j h
this : succ j' = j
⊢ cons (q 0) (tail q) (succ j') = q (succ j')
[PROOFSTEP]
unfold tail
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := pred j h
this : succ j' = j
⊢ cons (q 0) (fun i => q (succ i)) (succ j') = q (succ j')
[PROOFSTEP]
rw [cons_succ]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x✝ : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
P : ((i : Fin (Nat.succ n)) → α i) → Sort v
h : (x₀ : α 0) → (x : (i : Fin n) → α (succ i)) → P (cons x₀ x)
x : (i : Fin (Nat.succ n)) → α i
⊢ P (cons (x 0) (tail x)) = P x
[PROOFSTEP]
rw [cons_self_tail]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x✝ : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
P : ((i : Fin (Nat.succ n)) → α i) → Sort v
h : (x₀ : α 0) → (x : (i : Fin n) → α (succ i)) → P (cons x₀ x)
x₀ : α 0
x : (i : Fin n) → α (succ i)
⊢ consCases h (cons x₀ x) = h x₀ x
[PROOFSTEP]
rw [consCases, cast_eq]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x✝ : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
P : ((i : Fin (Nat.succ n)) → α i) → Sort v
h : (x₀ : α 0) → (x : (i : Fin n) → α (succ i)) → P (cons x₀ x)
x₀ : α 0
x : (i : Fin n) → α (succ i)
⊢ h (cons x₀ x 0) (tail (cons x₀ x)) = h x₀ x
[PROOFSTEP]
congr
[GOAL]
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
P : {n : ℕ} → (Fin n → α) → Sort v
h0 : P elim0
h : {n : ℕ} → (x₀ : α) → (x : Fin n → α) → P x → P (cons x₀ x)
x : Fin 0 → α
⊢ P x
[PROOFSTEP]
convert h0
[GOAL]
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
⊢ Injective (cons x₀ x)
[PROOFSTEP]
refine' Fin.cases _ _
[GOAL]
case refine'_1
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
⊢ ∀ ⦃a₂ : Fin (n + 1)⦄, cons x₀ x 0 = cons x₀ x a₂ → 0 = a₂
[PROOFSTEP]
refine' Fin.cases _ _
[GOAL]
case refine'_1.refine'_1
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
⊢ cons x₀ x 0 = cons x₀ x 0 → 0 = 0
[PROOFSTEP]
intro
[GOAL]
case refine'_1.refine'_1
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
a✝ : cons x₀ x 0 = cons x₀ x 0
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case refine'_1.refine'_2
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
⊢ ∀ (i : Fin n), cons x₀ x 0 = cons x₀ x (succ i) → 0 = succ i
[PROOFSTEP]
intro j h
[GOAL]
case refine'_1.refine'_2
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
j : Fin n
h : cons x₀ x 0 = cons x₀ x (succ j)
⊢ 0 = succ j
[PROOFSTEP]
rw [cons_zero, cons_succ] at h 
[GOAL]
case refine'_1.refine'_2
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
j : Fin n
h : x₀ = x j
⊢ 0 = succ j
[PROOFSTEP]
exact hx₀.elim ⟨_, h.symm⟩
[GOAL]
case refine'_2
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
⊢ ∀ (i : Fin n) ⦃a₂ : Fin (n + 1)⦄, cons x₀ x (succ i) = cons x₀ x a₂ → succ i = a₂
[PROOFSTEP]
intro i
[GOAL]
case refine'_2
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i✝ : Fin n
y : α✝ (succ i✝)
z : α✝ 0
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i : Fin n
⊢ ∀ ⦃a₂ : Fin (n + 1)⦄, cons x₀ x (succ i) = cons x₀ x a₂ → succ i = a₂
[PROOFSTEP]
refine' Fin.cases _ _
[GOAL]
case refine'_2.refine'_1
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i✝ : Fin n
y : α✝ (succ i✝)
z : α✝ 0
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i : Fin n
⊢ cons x₀ x (succ i) = cons x₀ x 0 → succ i = 0
[PROOFSTEP]
intro h
[GOAL]
case refine'_2.refine'_1
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i✝ : Fin n
y : α✝ (succ i✝)
z : α✝ 0
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i : Fin n
h : cons x₀ x (succ i) = cons x₀ x 0
⊢ succ i = 0
[PROOFSTEP]
rw [cons_zero, cons_succ] at h 
[GOAL]
case refine'_2.refine'_1
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i✝ : Fin n
y : α✝ (succ i✝)
z : α✝ 0
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i : Fin n
h : x i = x₀
⊢ succ i = 0
[PROOFSTEP]
exact hx₀.elim ⟨_, h⟩
[GOAL]
case refine'_2.refine'_2
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i✝ : Fin n
y : α✝ (succ i✝)
z : α✝ 0
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i : Fin n
⊢ ∀ (i_1 : Fin n), cons x₀ x (succ i) = cons x₀ x (succ i_1) → succ i = succ i_1
[PROOFSTEP]
intro j h
[GOAL]
case refine'_2.refine'_2
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i✝ : Fin n
y : α✝ (succ i✝)
z : α✝ 0
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i j : Fin n
h : cons x₀ x (succ i) = cons x₀ x (succ j)
⊢ succ i = succ j
[PROOFSTEP]
rw [cons_succ, cons_succ] at h 
[GOAL]
case refine'_2.refine'_2
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i✝ : Fin n
y : α✝ (succ i✝)
z : α✝ 0
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i j : Fin n
h : x i = x j
⊢ succ i = succ j
[PROOFSTEP]
exact congr_arg _ (hx h)
[GOAL]
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
x₀ : α
x : Fin n → α
⊢ Injective (cons x₀ x) ↔ ¬x₀ ∈ Set.range x ∧ Injective x
[PROOFSTEP]
refine' ⟨fun h ↦ ⟨_, _⟩, fun h ↦ cons_injective_of_injective h.1 h.2⟩
[GOAL]
case refine'_1
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
x₀ : α
x : Fin n → α
h : Injective (cons x₀ x)
⊢ ¬x₀ ∈ Set.range x
[PROOFSTEP]
rintro ⟨i, hi⟩
[GOAL]
case refine'_1.intro
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i✝ : Fin n
y : α✝ (succ i✝)
z : α✝ 0
α : Type u_1
x₀ : α
x : Fin n → α
h : Injective (cons x₀ x)
i : Fin n
hi : x i = x₀
⊢ False
[PROOFSTEP]
replace h := @h i.succ 0
[GOAL]
case refine'_1.intro
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i✝ : Fin n
y : α✝ (succ i✝)
z : α✝ 0
α : Type u_1
x₀ : α
x : Fin n → α
i : Fin n
hi : x i = x₀
h : cons x₀ x (succ i) = cons x₀ x 0 → succ i = 0
⊢ False
[PROOFSTEP]
simp [hi, succ_ne_zero] at h 
[GOAL]
case refine'_2
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
x₀ : α
x : Fin n → α
h : Injective (cons x₀ x)
⊢ Injective x
[PROOFSTEP]
simpa [Function.comp] using h.comp (Fin.succ_injective _)
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
⊢ tail (update q 0 z) = tail q
[PROOFSTEP]
ext j
[GOAL]
case h
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin n
⊢ tail (update q 0 z) j = tail q j
[PROOFSTEP]
simp [tail, Fin.succ_ne_zero]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
⊢ tail (update q (succ i) y) = update (tail q) i y
[PROOFSTEP]
ext j
[GOAL]
case h
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin n
⊢ tail (update q (succ i) y) j = update (tail q) i y j
[PROOFSTEP]
by_cases h : j = i
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin n
h : j = i
⊢ tail (update q (succ i) y) j = update (tail q) i y j
[PROOFSTEP]
rw [h]
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin n
h : j = i
⊢ tail (update q (succ i) y) i = update (tail q) i y i
[PROOFSTEP]
simp [tail]
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
j : Fin n
h : ¬j = i
⊢ tail (update q (succ i) y) j = update (tail q) i y j
[PROOFSTEP]
simp [tail, (Fin.succ_injective n).ne h, h]
[GOAL]
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q✝ : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y✝ : α✝ (succ i)
z : α✝ 0
α : Type u_1
β : Type u_2
g : α → β
y : α
q : Fin n → α
⊢ g ∘ cons y q = cons (g y) (g ∘ q)
[PROOFSTEP]
ext j
[GOAL]
case h
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q✝ : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y✝ : α✝ (succ i)
z : α✝ 0
α : Type u_1
β : Type u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
⊢ (g ∘ cons y q) j = cons (g y) (g ∘ q) j
[PROOFSTEP]
by_cases h : j = 0
[GOAL]
case pos
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q✝ : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y✝ : α✝ (succ i)
z : α✝ 0
α : Type u_1
β : Type u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : j = 0
⊢ (g ∘ cons y q) j = cons (g y) (g ∘ q) j
[PROOFSTEP]
rw [h]
[GOAL]
case pos
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q✝ : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y✝ : α✝ (succ i)
z : α✝ 0
α : Type u_1
β : Type u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : j = 0
⊢ (g ∘ cons y q) 0 = cons (g y) (g ∘ q) 0
[PROOFSTEP]
rfl
[GOAL]
case neg
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q✝ : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y✝ : α✝ (succ i)
z : α✝ 0
α : Type u_1
β : Type u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : ¬j = 0
⊢ (g ∘ cons y q) j = cons (g y) (g ∘ q) j
[PROOFSTEP]
let j' := pred j h
[GOAL]
case neg
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q✝ : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y✝ : α✝ (succ i)
z : α✝ 0
α : Type u_1
β : Type u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := pred j h
⊢ (g ∘ cons y q) j = cons (g y) (g ∘ q) j
[PROOFSTEP]
have : j'.succ = j := succ_pred j h
[GOAL]
case neg
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q✝ : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y✝ : α✝ (succ i)
z : α✝ 0
α : Type u_1
β : Type u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := pred j h
this : succ j' = j
⊢ (g ∘ cons y q) j = cons (g y) (g ∘ q) j
[PROOFSTEP]
rw [← this, cons_succ, comp, comp, cons_succ]
[GOAL]
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q✝ : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
β : Type u_2
g : α → β
q : Fin (Nat.succ n) → α
⊢ g ∘ tail q = tail (g ∘ q)
[PROOFSTEP]
ext j
[GOAL]
case h
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q✝ : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
β : Type u_2
g : α → β
q : Fin (Nat.succ n) → α
j : Fin n
⊢ (g ∘ tail q) j = tail (g ∘ q) j
[PROOFSTEP]
simp [tail]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x✝ : α 0
q✝ : (i : Fin (n + 1)) → α i
p✝ : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
j : Fin n
⊢ q (succ j) ≤ cons x p (succ j) ↔ tail q j ≤ p j
[PROOFSTEP]
simp [tail]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x✝ : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y✝ : α (succ i)
z : α 0
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
x₀ y₀ : α 0
x y : (i : Fin n) → α (succ i)
⊢ (∀ (i : Fin n), cons x₀ x (succ i) ≤ cons y₀ y (succ i)) ↔ x ≤ y
[PROOFSTEP]
simp only [cons_succ, Pi.le_def]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x✝ : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y✝ : α (succ i)
z x₀ y₀ : α 0
x y : (i : Fin n) → α (succ i)
s : {i : Fin (Nat.succ n)} → α i → α i → Prop
⊢ Pi.Lex (fun x x_1 => x < x_1) s (cons x₀ x) (cons y₀ y) ↔
    s x₀ y₀ ∨ x₀ = y₀ ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i => s) x y
[PROOFSTEP]
simp_rw [Pi.Lex, Fin.exists_fin_succ, Fin.cons_succ, Fin.cons_zero, Fin.forall_fin_succ]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x✝ : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y✝ : α (succ i)
z x₀ y₀ : α 0
x y : (i : Fin n) → α (succ i)
s : {i : Fin (Nat.succ n)} → α i → α i → Prop
⊢ (((0 < 0 → cons x₀ x 0 = cons y₀ y 0) ∧ ∀ (i : Fin n), succ i < 0 → cons x₀ x (succ i) = cons y₀ y (succ i)) ∧
        s x₀ y₀ ∨
      ∃ i,
        ((0 < succ i → cons x₀ x 0 = cons y₀ y 0) ∧
            ∀ (i_1 : Fin n), succ i_1 < succ i → cons x₀ x (succ i_1) = cons y₀ y (succ i_1)) ∧
          s (x i) (y i)) ↔
    s x₀ y₀ ∨ x₀ = y₀ ∧ ∃ i, (∀ (j : Fin n), j < i → x j = y j) ∧ s (x i) (y i)
[PROOFSTEP]
simp [and_assoc, exists_and_left]
[GOAL]
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (succ i)
i : Fin n✝
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
n : ℕ
x : α
b : Fin n → α
⊢ Set.range (cons x b) = insert x (Set.range b)
[PROOFSTEP]
rw [range_fin_succ, cons_zero, tail_cons]
[GOAL]
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
⊢ m + n = m
[PROOFSTEP]
rw [hv, add_zero]
[GOAL]
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
⊢ append u v = u ∘ ↑(castIso (_ : m + n = m))
[PROOFSTEP]
refine' funext (Fin.addCases (fun l => _) fun r => _)
[GOAL]
case refine'_1
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
l : Fin m
⊢ append u v (castAdd n l) = (u ∘ ↑(castIso (_ : m + n = m))) (castAdd n l)
[PROOFSTEP]
rw [append_left, Function.comp_apply]
[GOAL]
case refine'_1
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
l : Fin m
⊢ u l = u (↑(castIso (_ : m + n = m)) (castAdd n l))
[PROOFSTEP]
refine' congr_arg u (Fin.ext _)
[GOAL]
case refine'_1
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
l : Fin m
⊢ ↑l = ↑(↑(castIso (_ : m + n = m)) (castAdd n l))
[PROOFSTEP]
simp
[GOAL]
case refine'_2
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
r : Fin n
⊢ append u v (natAdd m r) = (u ∘ ↑(castIso (_ : m + n = m))) (natAdd m r)
[PROOFSTEP]
exact (Fin.castIso hv r).elim0'
[GOAL]
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
⊢ m + n = n
[PROOFSTEP]
rw [hu, zero_add]
[GOAL]
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
⊢ append u v = v ∘ ↑(castIso (_ : m + n = n))
[PROOFSTEP]
refine' funext (Fin.addCases (fun l => _) fun r => _)
[GOAL]
case refine'_1
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
l : Fin m
⊢ append u v (castAdd n l) = (v ∘ ↑(castIso (_ : m + n = n))) (castAdd n l)
[PROOFSTEP]
exact (Fin.castIso hu l).elim0'
[GOAL]
case refine'_2
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ append u v (natAdd m r) = (v ∘ ↑(castIso (_ : m + n = n))) (natAdd m r)
[PROOFSTEP]
rw [append_right, Function.comp_apply]
[GOAL]
case refine'_2
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ v r = v (↑(castIso (_ : m + n = n)) (natAdd m r))
[PROOFSTEP]
refine' congr_arg v (Fin.ext _)
[GOAL]
case refine'_2
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ ↑r = ↑(↑(castIso (_ : m + n = n)) (natAdd m r))
[PROOFSTEP]
simp [hu]
[GOAL]
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p✝ : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
p : ℕ
α : Type u_1
a : Fin m → α
b : Fin n → α
c : Fin p → α
⊢ append (append a b) c = append a (append b c) ∘ ↑(castIso (_ : m + n + p = m + (n + p)))
[PROOFSTEP]
ext i
[GOAL]
case h
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p✝ : (i : Fin n) → α✝ (succ i)
i✝ : Fin n
y : α✝ (succ i✝)
z : α✝ 0
p : ℕ
α : Type u_1
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
⊢ append (append a b) c i = (append a (append b c) ∘ ↑(castIso (_ : m + n + p = m + (n + p)))) i
[PROOFSTEP]
rw [Function.comp_apply]
[GOAL]
case h
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p✝ : (i : Fin n) → α✝ (succ i)
i✝ : Fin n
y : α✝ (succ i✝)
z : α✝ 0
p : ℕ
α : Type u_1
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
⊢ append (append a b) c i = append a (append b c) (↑(castIso (_ : m + n + p = m + (n + p))) i)
[PROOFSTEP]
refine' Fin.addCases (fun l => _) (fun r => _) i
[GOAL]
case h.refine'_1
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p✝ : (i : Fin n) → α✝ (succ i)
i✝ : Fin n
y : α✝ (succ i✝)
z : α✝ 0
p : ℕ
α : Type u_1
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
⊢ append (append a b) c (castAdd p l) = append a (append b c) (↑(castIso (_ : m + n + p = m + (n + p))) (castAdd p l))
[PROOFSTEP]
rw [append_left]
[GOAL]
case h.refine'_1
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p✝ : (i : Fin n) → α✝ (succ i)
i✝ : Fin n
y : α✝ (succ i✝)
z : α✝ 0
p : ℕ
α : Type u_1
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
⊢ append a b l = append a (append b c) (↑(castIso (_ : m + n + p = m + (n + p))) (castAdd p l))
[PROOFSTEP]
refine' Fin.addCases (fun ll => _) (fun lr => _) l
[GOAL]
case h.refine'_1.refine'_1
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p✝ : (i : Fin n) → α✝ (succ i)
i✝ : Fin n
y : α✝ (succ i✝)
z : α✝ 0
p : ℕ
α : Type u_1
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
ll : Fin m
⊢ append a b (castAdd n ll) =
    append a (append b c) (↑(castIso (_ : m + n + p = m + (n + p))) (castAdd p (castAdd n ll)))
[PROOFSTEP]
rw [append_left]
  -- TODO: we need to decide the simp normal form here
        -- and potentially add `@[simp]` to `castIso_eq_cast`.
[GOAL]
case h.refine'_1.refine'_1
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p✝ : (i : Fin n) → α✝ (succ i)
i✝ : Fin n
y : α✝ (succ i✝)
z : α✝ 0
p : ℕ
α : Type u_1
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
ll : Fin m
⊢ a ll = append a (append b c) (↑(castIso (_ : m + n + p = m + (n + p))) (castAdd p (castAdd n ll)))
[PROOFSTEP]
simp [castAdd_castAdd, castIso_eq_cast]
[GOAL]
case h.refine'_1.refine'_2
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p✝ : (i : Fin n) → α✝ (succ i)
i✝ : Fin n
y : α✝ (succ i✝)
z : α✝ 0
p : ℕ
α : Type u_1
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
lr : Fin n
⊢ append a b (natAdd m lr) = append a (append b c) (↑(castIso (_ : m + n + p = m + (n + p))) (castAdd p (natAdd m lr)))
[PROOFSTEP]
rw [append_right]
[GOAL]
case h.refine'_1.refine'_2
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p✝ : (i : Fin n) → α✝ (succ i)
i✝ : Fin n
y : α✝ (succ i✝)
z : α✝ 0
p : ℕ
α : Type u_1
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
lr : Fin n
⊢ b lr = append a (append b c) (↑(castIso (_ : m + n + p = m + (n + p))) (castAdd p (natAdd m lr)))
[PROOFSTEP]
simp [castAdd_natAdd, castIso_eq_cast]
[GOAL]
case h.refine'_2
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p✝ : (i : Fin n) → α✝ (succ i)
i✝ : Fin n
y : α✝ (succ i✝)
z : α✝ 0
p : ℕ
α : Type u_1
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
r : Fin p
⊢ append (append a b) c (natAdd (m + n) r) =
    append a (append b c) (↑(castIso (_ : m + n + p = m + (n + p))) (natAdd (m + n) r))
[PROOFSTEP]
rw [append_right]
[GOAL]
case h.refine'_2
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p✝ : (i : Fin n) → α✝ (succ i)
i✝ : Fin n
y : α✝ (succ i✝)
z : α✝ 0
p : ℕ
α : Type u_1
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
r : Fin p
⊢ c r = append a (append b c) (↑(castIso (_ : m + n + p = m + (n + p))) (natAdd (m + n) r))
[PROOFSTEP]
simp [← natAdd_natAdd, castIso_eq_cast]
[GOAL]
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (succ i)
i : Fin n✝
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
⊢ append x₀ x = cons (x₀ 0) x ∘ ↑(castIso (_ : 1 + n = n + 1))
[PROOFSTEP]
ext i
[GOAL]
case h
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (succ i)
i✝ : Fin n✝
y : α✝ (succ i✝)
z : α✝ 0
α : Type u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin (1 + n)
⊢ append x₀ x i = (cons (x₀ 0) x ∘ ↑(castIso (_ : 1 + n = n + 1))) i
[PROOFSTEP]
refine' Fin.addCases _ _ i
[GOAL]
case h.refine'_1
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (succ i)
i✝ : Fin n✝
y : α✝ (succ i✝)
z : α✝ 0
α : Type u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin (1 + n)
⊢ ∀ (i : Fin 1), append x₀ x (castAdd n i) = (cons (x₀ 0) x ∘ ↑(castIso (_ : 1 + n = n + 1))) (castAdd n i)
[PROOFSTEP]
clear i
[GOAL]
case h.refine'_2
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (succ i)
i✝ : Fin n✝
y : α✝ (succ i✝)
z : α✝ 0
α : Type u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin (1 + n)
⊢ ∀ (i : Fin n), append x₀ x (natAdd 1 i) = (cons (x₀ 0) x ∘ ↑(castIso (_ : 1 + n = n + 1))) (natAdd 1 i)
[PROOFSTEP]
clear i
[GOAL]
case h.refine'_1
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (succ i)
i : Fin n✝
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
⊢ ∀ (i : Fin 1), append x₀ x (castAdd n i) = (cons (x₀ 0) x ∘ ↑(castIso (_ : 1 + n = n + 1))) (castAdd n i)
[PROOFSTEP]
intro i
[GOAL]
case h.refine'_1
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (succ i)
i✝ : Fin n✝
y : α✝ (succ i✝)
z : α✝ 0
α : Type u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin 1
⊢ append x₀ x (castAdd n i) = (cons (x₀ 0) x ∘ ↑(castIso (_ : 1 + n = n + 1))) (castAdd n i)
[PROOFSTEP]
rw [Subsingleton.elim i 0, Fin.append_left, Function.comp_apply, eq_comm]
[GOAL]
case h.refine'_1
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (succ i)
i✝ : Fin n✝
y : α✝ (succ i✝)
z : α✝ 0
α : Type u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin 1
⊢ cons (x₀ 0) x (↑(castIso (_ : 1 + n = n + 1)) (castAdd n 0)) = x₀ 0
[PROOFSTEP]
exact Fin.cons_zero _ _
[GOAL]
case h.refine'_2
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (succ i)
i : Fin n✝
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
⊢ ∀ (i : Fin n), append x₀ x (natAdd 1 i) = (cons (x₀ 0) x ∘ ↑(castIso (_ : 1 + n = n + 1))) (natAdd 1 i)
[PROOFSTEP]
intro i
[GOAL]
case h.refine'_2
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (succ i)
i✝ : Fin n✝
y : α✝ (succ i✝)
z : α✝ 0
α : Type u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin n
⊢ append x₀ x (natAdd 1 i) = (cons (x₀ 0) x ∘ ↑(castIso (_ : 1 + n = n + 1))) (natAdd 1 i)
[PROOFSTEP]
rw [Fin.append_right, Function.comp_apply, Fin.castIso_natAdd, eq_comm, Fin.addNat_one]
[GOAL]
case h.refine'_2
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (succ i)
i✝ : Fin n✝
y : α✝ (succ i✝)
z : α✝ 0
α : Type u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin n
⊢ cons (x₀ 0) x (succ i) = x i
[PROOFSTEP]
exact Fin.cons_succ _ _ _
[GOAL]
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
a : Fin n → α
⊢ repeat 1 a = a ∘ ↑(castIso (_ : 1 * n = n))
[PROOFSTEP]
generalize_proofs h
[GOAL]
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
a : Fin n → α
h : 1 * n = n
⊢ repeat 1 a = a ∘ ↑(castIso h)
[PROOFSTEP]
apply funext
[GOAL]
case h
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
a : Fin n → α
h : 1 * n = n
⊢ ∀ (x : Fin (1 * n)), repeat 1 a x = (a ∘ ↑(castIso h)) x
[PROOFSTEP]
rw [(Fin.castIso h.symm).surjective.forall]
[GOAL]
case h
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
a : Fin n → α
h : 1 * n = n
⊢ ∀ (x : Fin n), repeat 1 a (↑(castIso (_ : n = 1 * n)) x) = (a ∘ ↑(castIso h)) (↑(castIso (_ : n = 1 * n)) x)
[PROOFSTEP]
intro i
[GOAL]
case h
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i✝ : Fin n
y : α✝ (succ i✝)
z : α✝ 0
α : Type u_1
a : Fin n → α
h : 1 * n = n
i : Fin n
⊢ repeat 1 a (↑(castIso (_ : n = 1 * n)) i) = (a ∘ ↑(castIso h)) (↑(castIso (_ : n = 1 * n)) i)
[PROOFSTEP]
simp [modNat, Nat.mod_eq_of_lt i.is_lt]
[GOAL]
m✝ n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
a : Fin n → α
m : ℕ
⊢ repeat (Nat.succ m) a = append a (repeat m a) ∘ ↑(castIso (_ : Nat.succ m * n = n + m * n))
[PROOFSTEP]
generalize_proofs h
[GOAL]
m✝ n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
a : Fin n → α
m : ℕ
h : Nat.succ m * n = n + m * n
⊢ repeat (Nat.succ m) a = append a (repeat m a) ∘ ↑(castIso h)
[PROOFSTEP]
apply funext
[GOAL]
case h
m✝ n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
a : Fin n → α
m : ℕ
h : Nat.succ m * n = n + m * n
⊢ ∀ (x : Fin (Nat.succ m * n)), repeat (Nat.succ m) a x = (append a (repeat m a) ∘ ↑(castIso h)) x
[PROOFSTEP]
rw [(Fin.castIso h.symm).surjective.forall]
[GOAL]
case h
m✝ n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
a : Fin n → α
m : ℕ
h : Nat.succ m * n = n + m * n
⊢ ∀ (x : Fin (n + m * n)),
    repeat (Nat.succ m) a (↑(castIso (_ : n + m * n = Nat.succ m * n)) x) =
      (append a (repeat m a) ∘ ↑(castIso h)) (↑(castIso (_ : n + m * n = Nat.succ m * n)) x)
[PROOFSTEP]
refine' Fin.addCases (fun l => _) fun r => _
[GOAL]
case h.refine'_1
m✝ n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
a : Fin n → α
m : ℕ
h : Nat.succ m * n = n + m * n
l : Fin n
⊢ repeat (Nat.succ m) a (↑(castIso (_ : n + m * n = Nat.succ m * n)) (castAdd (m * n) l)) =
    (append a (repeat m a) ∘ ↑(castIso h)) (↑(castIso (_ : n + m * n = Nat.succ m * n)) (castAdd (m * n) l))
[PROOFSTEP]
simp [modNat, Nat.mod_eq_of_lt l.is_lt]
[GOAL]
case h.refine'_2
m✝ n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
a : Fin n → α
m : ℕ
h : Nat.succ m * n = n + m * n
r : Fin (m * n)
⊢ repeat (Nat.succ m) a (↑(castIso (_ : n + m * n = Nat.succ m * n)) (natAdd n r)) =
    (append a (repeat m a) ∘ ↑(castIso h)) (↑(castIso (_ : n + m * n = Nat.succ m * n)) (natAdd n r))
[PROOFSTEP]
simp [modNat]
[GOAL]
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
a : Fin n → α
m₁ m₂ : ℕ
⊢ repeat (m₁ + m₂) a = append (repeat m₁ a) (repeat m₂ a) ∘ ↑(castIso (_ : (m₁ + m₂) * n = m₁ * n + m₂ * n))
[PROOFSTEP]
generalize_proofs h
[GOAL]
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
a : Fin n → α
m₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
⊢ repeat (m₁ + m₂) a = append (repeat m₁ a) (repeat m₂ a) ∘ ↑(castIso h)
[PROOFSTEP]
apply funext
[GOAL]
case h
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
a : Fin n → α
m₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
⊢ ∀ (x : Fin ((m₁ + m₂) * n)), repeat (m₁ + m₂) a x = (append (repeat m₁ a) (repeat m₂ a) ∘ ↑(castIso h)) x
[PROOFSTEP]
rw [(Fin.castIso h.symm).surjective.forall]
[GOAL]
case h
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
a : Fin n → α
m₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
⊢ ∀ (x : Fin (m₁ * n + m₂ * n)),
    repeat (m₁ + m₂) a (↑(castIso (_ : m₁ * n + m₂ * n = (m₁ + m₂) * n)) x) =
      (append (repeat m₁ a) (repeat m₂ a) ∘ ↑(castIso h)) (↑(castIso (_ : m₁ * n + m₂ * n = (m₁ + m₂) * n)) x)
[PROOFSTEP]
refine' Fin.addCases (fun l => _) fun r => _
[GOAL]
case h.refine'_1
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
a : Fin n → α
m₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
l : Fin (m₁ * n)
⊢ repeat (m₁ + m₂) a (↑(castIso (_ : m₁ * n + m₂ * n = (m₁ + m₂) * n)) (castAdd (m₂ * n) l)) =
    (append (repeat m₁ a) (repeat m₂ a) ∘ ↑(castIso h))
      (↑(castIso (_ : m₁ * n + m₂ * n = (m₁ + m₂) * n)) (castAdd (m₂ * n) l))
[PROOFSTEP]
simp [modNat, Nat.mod_eq_of_lt l.is_lt]
[GOAL]
case h.refine'_2
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
a : Fin n → α
m₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
r : Fin (m₂ * n)
⊢ repeat (m₁ + m₂) a (↑(castIso (_ : m₁ * n + m₂ * n = (m₁ + m₂) * n)) (natAdd (m₁ * n) r)) =
    (append (repeat m₁ a) (repeat m₂ a) ∘ ↑(castIso h))
      (↑(castIso (_ : m₁ * n + m₂ * n = (m₁ + m₂) * n)) (natAdd (m₁ * n) r))
[PROOFSTEP]
simp [modNat, Nat.add_mod]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x✝ : α (last n)
q : (i : Fin (n + 1)) → α i
p✝ : (i : Fin n) → α (castSucc i)
i✝ : Fin n
y : α (castSucc i✝)
z : α (last n)
p : (i : Fin n) → α (castSucc i)
x : α (last n)
i : Fin (n + 1)
h : ↑i < n
⊢ α (castSucc (castLT i h)) = α i
[PROOFSTEP]
rw [Fin.castSucc_castLT i h]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x✝ : α (last n)
q : (i : Fin (n + 1)) → α i
p✝ : (i : Fin n) → α (castSucc i)
i✝ : Fin n
y : α (castSucc i✝)
z : α (last n)
p : (i : Fin n) → α (castSucc i)
x : α (last n)
i : Fin (n + 1)
h : ¬↑i < n
⊢ α (last n) = α i
[PROOFSTEP]
rw [eq_last_of_not_lt h]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
⊢ init (snoc p x) = p
[PROOFSTEP]
ext i
[GOAL]
case h
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i✝ : Fin n
y : α (castSucc i✝)
z : α (last n)
i : Fin n
⊢ init (snoc p x) i = p i
[PROOFSTEP]
simp only [init, snoc, coe_castSucc, is_lt, cast_eq, dite_true]
[GOAL]
case h
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i✝ : Fin n
y : α (castSucc i✝)
z : α (last n)
i : Fin n
⊢ p (castLT (castSucc i) (_ : ↑i < n)) = p i
[PROOFSTEP]
convert cast_eq rfl (p i)
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
⊢ snoc p x (castSucc i) = p i
[PROOFSTEP]
simp only [snoc, coe_castSucc, is_lt, cast_eq, dite_true]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
⊢ p (castLT (castSucc i) (_ : ↑i < n)) = p i
[PROOFSTEP]
convert cast_eq rfl (p i)
[GOAL]
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (castSucc i)
i✝ : Fin n✝
y : α✝ (castSucc i✝)
z : α✝ (last n✝)
n : ℕ
α : Type u_1
a : α
f : Fin n → α
i : Fin n
⊢ (snoc f a ∘ castSucc) i = f i
[PROOFSTEP]
rw [Function.comp_apply, snoc_castSucc]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
⊢ snoc p x (last n) = x
[PROOFSTEP]
simp [snoc]
[GOAL]
m✝ n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (castSucc i)
i : Fin n✝
y : α✝ (castSucc i)
z : α✝ (last n✝)
n m : ℕ
α : Type u_1
f : Fin (m + n) → α
a : α
⊢ snoc f a ∘ natAdd m = snoc (f ∘ natAdd m) a
[PROOFSTEP]
ext i
[GOAL]
case h
m✝ n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (castSucc i)
i✝ : Fin n✝
y : α✝ (castSucc i✝)
z : α✝ (last n✝)
n m : ℕ
α : Type u_1
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
⊢ (snoc f a ∘ natAdd m) i = snoc (f ∘ natAdd m) a i
[PROOFSTEP]
refine' Fin.lastCases _ (fun i ↦ _) i
[GOAL]
case h.refine'_1
m✝ n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (castSucc i)
i✝ : Fin n✝
y : α✝ (castSucc i✝)
z : α✝ (last n✝)
n m : ℕ
α : Type u_1
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
⊢ (snoc f a ∘ natAdd m) (last n) = snoc (f ∘ natAdd m) a (last n)
[PROOFSTEP]
simp only [Function.comp_apply]
[GOAL]
case h.refine'_1
m✝ n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (castSucc i)
i✝ : Fin n✝
y : α✝ (castSucc i✝)
z : α✝ (last n✝)
n m : ℕ
α : Type u_1
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
⊢ snoc f a (natAdd m (last n)) = snoc (f ∘ natAdd m) a (last n)
[PROOFSTEP]
rw [snoc_last, natAdd_last, snoc_last]
[GOAL]
case h.refine'_2
m✝ n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (castSucc i)
i✝¹ : Fin n✝
y : α✝ (castSucc i✝¹)
z : α✝ (last n✝)
n m : ℕ
α : Type u_1
f : Fin (m + n) → α
a : α
i✝ : Fin (n + 1)
i : Fin n
⊢ (snoc f a ∘ natAdd m) (castSucc i) = snoc (f ∘ natAdd m) a (castSucc i)
[PROOFSTEP]
simp only [comp_apply, snoc_castSucc]
[GOAL]
case h.refine'_2
m✝ n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (castSucc i)
i✝¹ : Fin n✝
y : α✝ (castSucc i✝¹)
z : α✝ (last n✝)
n m : ℕ
α : Type u_1
f : Fin (m + n) → α
a : α
i✝ : Fin (n + 1)
i : Fin n
⊢ snoc f a (natAdd m (castSucc i)) = f (natAdd m i)
[PROOFSTEP]
rw [natAdd_castSucc, snoc_castSucc]
[GOAL]
m✝ n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (castSucc i)
i : Fin n✝
y : α✝ (castSucc i)
z : α✝ (last n✝)
n m : ℕ
α : Type u_1
f : Fin (n + m) → α
a : α
⊢ ∀ (x : Fin n), (snoc f a ∘ castAdd (m + 1)) x = (f ∘ castAdd m) x
[PROOFSTEP]
unfold comp
[GOAL]
m✝ n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (castSucc i)
i : Fin n✝
y : α✝ (castSucc i)
z : α✝ (last n✝)
n m : ℕ
α : Type u_1
f : Fin (n + m) → α
a : α
⊢ ∀ (x : Fin n), snoc f a (castAdd (m + 1) x) = f (castAdd m x)
[PROOFSTEP]
exact snoc_cast_add _ _
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
⊢ snoc (update p i y) x = update (snoc p x) (castSucc i) y
[PROOFSTEP]
ext j
[GOAL]
case h
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
⊢ snoc (update p i y) x j = update (snoc p x) (castSucc i) y j
[PROOFSTEP]
by_cases h : j.val < n
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
⊢ snoc (update p i y) x j = update (snoc p x) (castSucc i) y j
[PROOFSTEP]
rw [snoc]
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
⊢ (if h : ↑j < n then _root_.cast (_ : α (castSucc (castLT j h)) = α j) (update p i y (castLT j h))
    else _root_.cast (_ : α (last n) = α j) x) =
    update (snoc p x) (castSucc i) y j
[PROOFSTEP]
simp only [h]
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
⊢ (if h_1 : True then
      _root_.cast (_ : α (castSucc (castLT j (_ : ↑j < n))) = α j) (update p i y (castLT j (_ : ↑j < n)))
    else _root_.cast (_ : α (last n) = α j) x) =
    update (snoc p x) (castSucc i) y j
[PROOFSTEP]
simp only [dif_pos]
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
⊢ _root_.cast (_ : α (castSucc (castLT j (_ : ↑j < n))) = α j) (update p i y (castLT j (_ : ↑j < n))) =
    update (snoc p x) (castSucc i) y j
[PROOFSTEP]
by_cases h' : j = castSucc i
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
h' : j = castSucc i
⊢ _root_.cast (_ : α (castSucc (castLT j (_ : ↑j < n))) = α j) (update p i y (castLT j (_ : ↑j < n))) =
    update (snoc p x) (castSucc i) y j
[PROOFSTEP]
have C1 : α (castSucc i) = α j := by rw [h']
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
h' : j = castSucc i
⊢ α (castSucc i) = α j
[PROOFSTEP]
rw [h']
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
h' : j = castSucc i
C1 : α (castSucc i) = α j
⊢ _root_.cast (_ : α (castSucc (castLT j (_ : ↑j < n))) = α j) (update p i y (castLT j (_ : ↑j < n))) =
    update (snoc p x) (castSucc i) y j
[PROOFSTEP]
have E1 : update (snoc p x) (castSucc i) y j = _root_.cast C1 y :=
  by
  have : update (snoc p x) j (_root_.cast C1 y) j = _root_.cast C1 y := by simp
  convert this
  · exact h'.symm
  · exact heq_of_cast_eq (congr_arg α (Eq.symm h')) rfl
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
h' : j = castSucc i
C1 : α (castSucc i) = α j
⊢ update (snoc p x) (castSucc i) y j = _root_.cast C1 y
[PROOFSTEP]
have : update (snoc p x) j (_root_.cast C1 y) j = _root_.cast C1 y := by simp
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
h' : j = castSucc i
C1 : α (castSucc i) = α j
⊢ update (snoc p x) j (_root_.cast C1 y) j = _root_.cast C1 y
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
h' : j = castSucc i
C1 : α (castSucc i) = α j
this : update (snoc p x) j (_root_.cast C1 y) j = _root_.cast C1 y
⊢ update (snoc p x) (castSucc i) y j = _root_.cast C1 y
[PROOFSTEP]
convert this
[GOAL]
case h.e'_2.h.e'_5
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
h' : j = castSucc i
C1 : α (castSucc i) = α j
this : update (snoc p x) j (_root_.cast C1 y) j = _root_.cast C1 y
⊢ castSucc i = j
[PROOFSTEP]
exact h'.symm
[GOAL]
case h.e'_2.h.e'_6
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
h' : j = castSucc i
C1 : α (castSucc i) = α j
this : update (snoc p x) j (_root_.cast C1 y) j = _root_.cast C1 y
e_5✝ : castSucc i = j
⊢ HEq y (_root_.cast C1 y)
[PROOFSTEP]
exact heq_of_cast_eq (congr_arg α (Eq.symm h')) rfl
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
h' : j = castSucc i
C1 : α (castSucc i) = α j
E1 : update (snoc p x) (castSucc i) y j = _root_.cast C1 y
⊢ _root_.cast (_ : α (castSucc (castLT j (_ : ↑j < n))) = α j) (update p i y (castLT j (_ : ↑j < n))) =
    update (snoc p x) (castSucc i) y j
[PROOFSTEP]
have C2 : α (castSucc i) = α (castSucc (castLT j h)) := by rw [castSucc_castLT, h']
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
h' : j = castSucc i
C1 : α (castSucc i) = α j
E1 : update (snoc p x) (castSucc i) y j = _root_.cast C1 y
⊢ α (castSucc i) = α (castSucc (castLT j h))
[PROOFSTEP]
rw [castSucc_castLT, h']
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
h' : j = castSucc i
C1 : α (castSucc i) = α j
E1 : update (snoc p x) (castSucc i) y j = _root_.cast C1 y
C2 : α (castSucc i) = α (castSucc (castLT j h))
⊢ _root_.cast (_ : α (castSucc (castLT j (_ : ↑j < n))) = α j) (update p i y (castLT j (_ : ↑j < n))) =
    update (snoc p x) (castSucc i) y j
[PROOFSTEP]
have E2 : update p i y (castLT j h) = _root_.cast C2 y :=
  by
  have : update p (castLT j h) (_root_.cast C2 y) (castLT j h) = _root_.cast C2 y := by simp
  convert this
  · simp [h, h']
  · exact heq_of_cast_eq C2 rfl
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
h' : j = castSucc i
C1 : α (castSucc i) = α j
E1 : update (snoc p x) (castSucc i) y j = _root_.cast C1 y
C2 : α (castSucc i) = α (castSucc (castLT j h))
⊢ update p i y (castLT j h) = _root_.cast C2 y
[PROOFSTEP]
have : update p (castLT j h) (_root_.cast C2 y) (castLT j h) = _root_.cast C2 y := by simp
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
h' : j = castSucc i
C1 : α (castSucc i) = α j
E1 : update (snoc p x) (castSucc i) y j = _root_.cast C1 y
C2 : α (castSucc i) = α (castSucc (castLT j h))
⊢ update p (castLT j h) (_root_.cast C2 y) (castLT j h) = _root_.cast C2 y
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
h' : j = castSucc i
C1 : α (castSucc i) = α j
E1 : update (snoc p x) (castSucc i) y j = _root_.cast C1 y
C2 : α (castSucc i) = α (castSucc (castLT j h))
this : update p (castLT j h) (_root_.cast C2 y) (castLT j h) = _root_.cast C2 y
⊢ update p i y (castLT j h) = _root_.cast C2 y
[PROOFSTEP]
convert this
[GOAL]
case h.e'_2.h.e'_5
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
h' : j = castSucc i
C1 : α (castSucc i) = α j
E1 : update (snoc p x) (castSucc i) y j = _root_.cast C1 y
C2 : α (castSucc i) = α (castSucc (castLT j h))
this : update p (castLT j h) (_root_.cast C2 y) (castLT j h) = _root_.cast C2 y
⊢ i = castLT j h
[PROOFSTEP]
simp [h, h']
[GOAL]
case h.e'_2.h.e'_6
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
h' : j = castSucc i
C1 : α (castSucc i) = α j
E1 : update (snoc p x) (castSucc i) y j = _root_.cast C1 y
C2 : α (castSucc i) = α (castSucc (castLT j h))
this : update p (castLT j h) (_root_.cast C2 y) (castLT j h) = _root_.cast C2 y
e_5✝ : i = castLT j h
⊢ HEq y (_root_.cast C2 y)
[PROOFSTEP]
exact heq_of_cast_eq C2 rfl
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
h' : j = castSucc i
C1 : α (castSucc i) = α j
E1 : update (snoc p x) (castSucc i) y j = _root_.cast C1 y
C2 : α (castSucc i) = α (castSucc (castLT j h))
E2 : update p i y (castLT j h) = _root_.cast C2 y
⊢ _root_.cast (_ : α (castSucc (castLT j (_ : ↑j < n))) = α j) (update p i y (castLT j (_ : ↑j < n))) =
    update (snoc p x) (castSucc i) y j
[PROOFSTEP]
rw [E1, E2]
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
h' : j = castSucc i
C1 : α (castSucc i) = α j
E1 : update (snoc p x) (castSucc i) y j = _root_.cast C1 y
C2 : α (castSucc i) = α (castSucc (castLT j h))
E2 : update p i y (castLT j h) = _root_.cast C2 y
⊢ _root_.cast (_ : α (castSucc (castLT j (_ : ↑j < n))) = α j) (_root_.cast C2 y) = _root_.cast C1 y
[PROOFSTEP]
exact eq_rec_compose (Eq.trans C2.symm C1) C2 y
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
h' : ¬j = castSucc i
⊢ _root_.cast (_ : α (castSucc (castLT j (_ : ↑j < n))) = α j) (update p i y (castLT j (_ : ↑j < n))) =
    update (snoc p x) (castSucc i) y j
[PROOFSTEP]
have : ¬castLT j h = i := by
  intro E
  apply h'
  rw [← E, castSucc_castLT]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
h' : ¬j = castSucc i
⊢ ¬castLT j h = i
[PROOFSTEP]
intro E
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
h' : ¬j = castSucc i
E : castLT j h = i
⊢ False
[PROOFSTEP]
apply h'
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
h' : ¬j = castSucc i
E : castLT j h = i
⊢ j = castSucc i
[PROOFSTEP]
rw [← E, castSucc_castLT]
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
h' : ¬j = castSucc i
this : ¬castLT j h = i
⊢ _root_.cast (_ : α (castSucc (castLT j (_ : ↑j < n))) = α j) (update p i y (castLT j (_ : ↑j < n))) =
    update (snoc p x) (castSucc i) y j
[PROOFSTEP]
simp [h', this, snoc, h]
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ¬↑j < n
⊢ snoc (update p i y) x j = update (snoc p x) (castSucc i) y j
[PROOFSTEP]
rw [eq_last_of_not_lt h]
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ¬↑j < n
⊢ snoc (update p i y) x (last n) = update (snoc p x) (castSucc i) y (last n)
[PROOFSTEP]
simp [Ne.symm (ne_of_lt (castSucc_lt_last i))]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
⊢ update (snoc p x) (last n) z = snoc p z
[PROOFSTEP]
ext j
[GOAL]
case h
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
⊢ update (snoc p x) (last n) z j = snoc p z j
[PROOFSTEP]
by_cases h : j.val < n
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
⊢ update (snoc p x) (last n) z j = snoc p z j
[PROOFSTEP]
have : j ≠ last n := ne_of_lt h
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
this : j ≠ last n
⊢ update (snoc p x) (last n) z j = snoc p z j
[PROOFSTEP]
simp [h, update_noteq, this, snoc]
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ¬↑j < n
⊢ update (snoc p x) (last n) z j = snoc p z j
[PROOFSTEP]
rw [eq_last_of_not_lt h]
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ¬↑j < n
⊢ update (snoc p x) (last n) z (last n) = snoc p z (last n)
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
⊢ snoc (init q) (q (last n)) = q
[PROOFSTEP]
ext j
[GOAL]
case h
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
⊢ snoc (init q) (q (last n)) j = q j
[PROOFSTEP]
by_cases h : j.val < n
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
⊢ snoc (init q) (q (last n)) j = q j
[PROOFSTEP]
simp only [init, snoc, h, cast_eq, dite_true]
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
⊢ q (castSucc (castLT j (_ : ↑j < n))) = q j
[PROOFSTEP]
have _ : castSucc (castLT j h) = j := castSucc_castLT _ _
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
x✝ : castSucc (castLT j h) = j
⊢ q (castSucc (castLT j (_ : ↑j < n))) = q j
[PROOFSTEP]
rw [← cast_eq rfl (q j)]
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
x✝ : castSucc (castLT j h) = j
⊢ q (castSucc (castLT j (_ : ↑j < n))) = _root_.cast (_ : α j = α j) (q j)
[PROOFSTEP]
congr
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ¬↑j < n
⊢ snoc (init q) (q (last n)) j = q j
[PROOFSTEP]
rw [eq_last_of_not_lt h]
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin (n + 1)
h : ¬↑j < n
⊢ snoc (init q) (q (last n)) (last n) = q (last n)
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
⊢ init (update q (last n) z) = init q
[PROOFSTEP]
ext j
[GOAL]
case h
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin n
⊢ init (update q (last n) z) j = init q j
[PROOFSTEP]
simp [init, ne_of_lt, castSucc_lt_last]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
⊢ init (update q (castSucc i) y) = update (init q) i y
[PROOFSTEP]
ext j
[GOAL]
case h
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin n
⊢ init (update q (castSucc i) y) j = update (init q) i y j
[PROOFSTEP]
by_cases h : j = i
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin n
h : j = i
⊢ init (update q (castSucc i) y) j = update (init q) i y j
[PROOFSTEP]
rw [h]
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin n
h : j = i
⊢ init (update q (castSucc i) y) i = update (init q) i y i
[PROOFSTEP]
simp [init]
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
j : Fin n
h : ¬j = i
⊢ init (update q (castSucc i) y) j = update (init q) i y j
[PROOFSTEP]
simp [init, h, castSucc_inj]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
β : Type u_1
q : Fin (n + 2) → β
⊢ tail (init q) = init (tail q)
[PROOFSTEP]
ext i
[GOAL]
case h
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i✝ : Fin n
y : α (castSucc i✝)
z : α (last n)
β : Type u_1
q : Fin (n + 2) → β
i : Fin n
⊢ tail (init q) i = init (tail q) i
[PROOFSTEP]
simp [tail, init, castSucc_fin_succ]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i : Fin n
y : α (castSucc i)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
⊢ cons a (snoc q b) = snoc (cons a q) b
[PROOFSTEP]
ext i
[GOAL]
case h
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i✝ : Fin n
y : α (castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
⊢ cons a (snoc q b) i = snoc (cons a q) b i
[PROOFSTEP]
by_cases h : i = 0
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i✝ : Fin n
y : α (castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : i = 0
⊢ cons a (snoc q b) i = snoc (cons a q) b i
[PROOFSTEP]
rw [h]
  -- Porting note: `refl` finished it here in Lean 3, but I had to add more.
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i✝ : Fin n
y : α (castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : i = 0
⊢ cons a (snoc q b) 0 = snoc (cons a q) b 0
[PROOFSTEP]
simp [snoc, castLT]
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i✝ : Fin n
y : α (castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
⊢ cons a (snoc q b) i = snoc (cons a q) b i
[PROOFSTEP]
set j := pred i h with ji
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i✝ : Fin n
y : α (castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
⊢ cons a (snoc q b) i = snoc (cons a q) b i
[PROOFSTEP]
have : i = j.succ := by rw [ji, succ_pred]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i✝ : Fin n
y : α (castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
⊢ i = succ j
[PROOFSTEP]
rw [ji, succ_pred]
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i✝ : Fin n
y : α (castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
this : i = succ j
⊢ cons a (snoc q b) i = snoc (cons a q) b i
[PROOFSTEP]
rw [this, cons_succ]
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i✝ : Fin n
y : α (castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
this : i = succ j
⊢ snoc q b j = snoc (cons a q) b (succ j)
[PROOFSTEP]
by_cases h' : j.val < n
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i✝ : Fin n
y : α (castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
this : i = succ j
h' : ↑j < n
⊢ snoc q b j = snoc (cons a q) b (succ j)
[PROOFSTEP]
set k := castLT j h' with jk
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i✝ : Fin n
y : α (castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
this : i = succ j
h' : ↑j < n
k : Fin n := castLT j h'
jk : k = castLT j h'
⊢ snoc q b j = snoc (cons a q) b (succ j)
[PROOFSTEP]
have : j = castSucc k := by rw [jk, castSucc_castLT]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i✝ : Fin n
y : α (castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
this : i = succ j
h' : ↑j < n
k : Fin n := castLT j h'
jk : k = castLT j h'
⊢ j = castSucc k
[PROOFSTEP]
rw [jk, castSucc_castLT]
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i✝ : Fin n
y : α (castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
this✝ : i = succ j
h' : ↑j < n
k : Fin n := castLT j h'
jk : k = castLT j h'
this : j = castSucc k
⊢ snoc q b j = snoc (cons a q) b (succ j)
[PROOFSTEP]
rw [this, ← castSucc_fin_succ, snoc]
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i✝ : Fin n
y : α (castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
this✝ : i = succ j
h' : ↑j < n
k : Fin n := castLT j h'
jk : k = castLT j h'
this : j = castSucc k
⊢ (if h : ↑(castSucc k) < n then
      _root_.cast (_ : (fun x => β) (succ (castSucc (castLT (castSucc k) h))) = (fun x => β) (succ (castSucc k)))
        (q (castLT (castSucc k) h))
    else _root_.cast (_ : (fun x => β) (succ (last n)) = (fun x => β) (succ (castSucc k))) b) =
    snoc (cons a q) b (castSucc (succ k))
[PROOFSTEP]
simp [pred, snoc, cons]
[GOAL]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i✝ : Fin n
y : α (castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
this✝ : i = succ j
h' : ↑j < n
k : Fin n := castLT j h'
jk : k = castLT j h'
this : j = castSucc k
⊢ (if h_1 : ↑i - 1 < n then q (castLT (subNat 1 i (_ : 0 < ↑i)) (_ : ↑(subNat 1 i (_ : 0 < ↑i)) < n)) else b) =
    if ↑i - 1 < n then q (castLT (subNat 1 i (_ : 0 < ↑i)) (_ : ↑(subNat 1 i (_ : 0 < ↑i)) < n)) else b
[PROOFSTEP]
rfl
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i✝ : Fin n
y : α (castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
this : i = succ j
h' : ¬↑j < n
⊢ snoc q b j = snoc (cons a q) b (succ j)
[PROOFSTEP]
rw [eq_last_of_not_lt h', succ_last]
[GOAL]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (castSucc i)
i✝ : Fin n
y : α (castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
this : i = succ j
h' : ¬↑j < n
⊢ snoc q b (last n) = snoc (cons a q) b (last (Nat.succ n))
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ (last n)
q✝ : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (castSucc i)
i : Fin n
y✝ : α✝ (castSucc i)
z : α✝ (last n)
α : Type u_1
β : Type u_2
g : α → β
q : Fin n → α
y : α
⊢ g ∘ snoc q y = snoc (g ∘ q) (g y)
[PROOFSTEP]
ext j
[GOAL]
case h
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ (last n)
q✝ : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (castSucc i)
i : Fin n
y✝ : α✝ (castSucc i)
z : α✝ (last n)
α : Type u_1
β : Type u_2
g : α → β
q : Fin n → α
y : α
j : Fin (n + 1)
⊢ (g ∘ snoc q y) j = snoc (g ∘ q) (g y) j
[PROOFSTEP]
by_cases h : j.val < n
[GOAL]
case pos
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ (last n)
q✝ : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (castSucc i)
i : Fin n
y✝ : α✝ (castSucc i)
z : α✝ (last n)
α : Type u_1
β : Type u_2
g : α → β
q : Fin n → α
y : α
j : Fin (n + 1)
h : ↑j < n
⊢ (g ∘ snoc q y) j = snoc (g ∘ q) (g y) j
[PROOFSTEP]
simp [h, snoc, castSucc_castLT]
[GOAL]
case neg
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ (last n)
q✝ : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (castSucc i)
i : Fin n
y✝ : α✝ (castSucc i)
z : α✝ (last n)
α : Type u_1
β : Type u_2
g : α → β
q : Fin n → α
y : α
j : Fin (n + 1)
h : ¬↑j < n
⊢ (g ∘ snoc q y) j = snoc (g ∘ q) (g y) j
[PROOFSTEP]
rw [eq_last_of_not_lt h]
[GOAL]
case neg
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ (last n)
q✝ : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (castSucc i)
i : Fin n
y✝ : α✝ (castSucc i)
z : α✝ (last n)
α : Type u_1
β : Type u_2
g : α → β
q : Fin n → α
y : α
j : Fin (n + 1)
h : ¬↑j < n
⊢ (g ∘ snoc q y) (last n) = snoc (g ∘ q) (g y) (last n)
[PROOFSTEP]
simp
[GOAL]
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (castSucc i)
i : Fin n✝
y : α✝ (castSucc i)
z : α✝ (last n✝)
α : Type u_1
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
⊢ append x x₀ = snoc x (x₀ 0)
[PROOFSTEP]
ext i
[GOAL]
case h
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (castSucc i)
i✝ : Fin n✝
y : α✝ (castSucc i✝)
z : α✝ (last n✝)
α : Type u_1
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin (n + 1)
⊢ append x x₀ i = snoc x (x₀ 0) i
[PROOFSTEP]
refine' Fin.addCases _ _ i
[GOAL]
case h.refine'_1
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (castSucc i)
i✝ : Fin n✝
y : α✝ (castSucc i✝)
z : α✝ (last n✝)
α : Type u_1
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin (n + 1)
⊢ ∀ (i : Fin n), append x x₀ (castAdd 1 i) = snoc x (x₀ 0) (castAdd 1 i)
[PROOFSTEP]
clear i
[GOAL]
case h.refine'_2
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (castSucc i)
i✝ : Fin n✝
y : α✝ (castSucc i✝)
z : α✝ (last n✝)
α : Type u_1
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin (n + 1)
⊢ ∀ (i : Fin 1), append x x₀ (natAdd n i) = snoc x (x₀ 0) (natAdd n i)
[PROOFSTEP]
clear i
[GOAL]
case h.refine'_1
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (castSucc i)
i : Fin n✝
y : α✝ (castSucc i)
z : α✝ (last n✝)
α : Type u_1
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
⊢ ∀ (i : Fin n), append x x₀ (castAdd 1 i) = snoc x (x₀ 0) (castAdd 1 i)
[PROOFSTEP]
intro i
[GOAL]
case h.refine'_1
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (castSucc i)
i✝ : Fin n✝
y : α✝ (castSucc i✝)
z : α✝ (last n✝)
α : Type u_1
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin n
⊢ append x x₀ (castAdd 1 i) = snoc x (x₀ 0) (castAdd 1 i)
[PROOFSTEP]
rw [Fin.append_left]
[GOAL]
case h.refine'_1
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (castSucc i)
i✝ : Fin n✝
y : α✝ (castSucc i✝)
z : α✝ (last n✝)
α : Type u_1
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin n
⊢ x i = snoc x (x₀ 0) (castAdd 1 i)
[PROOFSTEP]
exact (@snoc_castSucc _ (fun _ => α) _ _ i).symm
[GOAL]
case h.refine'_2
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (castSucc i)
i : Fin n✝
y : α✝ (castSucc i)
z : α✝ (last n✝)
α : Type u_1
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
⊢ ∀ (i : Fin 1), append x x₀ (natAdd n i) = snoc x (x₀ 0) (natAdd n i)
[PROOFSTEP]
intro i
[GOAL]
case h.refine'_2
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (castSucc i)
i✝ : Fin n✝
y : α✝ (castSucc i✝)
z : α✝ (last n✝)
α : Type u_1
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin 1
⊢ append x x₀ (natAdd n i) = snoc x (x₀ 0) (natAdd n i)
[PROOFSTEP]
rw [Subsingleton.elim i 0, Fin.append_right]
[GOAL]
case h.refine'_2
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ (last n✝)
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (castSucc i)
i✝ : Fin n✝
y : α✝ (castSucc i✝)
z : α✝ (last n✝)
α : Type u_1
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin 1
⊢ x₀ 0 = snoc x (x₀ 0) (natAdd n 0)
[PROOFSTEP]
exact (@snoc_last _ (fun _ => α) _ _).symm
[GOAL]
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ (last n)
q✝ : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (castSucc i)
i : Fin n
y : α✝ (castSucc i)
z : α✝ (last n)
α : Type u_1
β : Type u_2
g : α → β
q : Fin (Nat.succ n) → α
⊢ g ∘ init q = init (g ∘ q)
[PROOFSTEP]
ext j
[GOAL]
case h
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ (last n)
q✝ : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (castSucc i)
i : Fin n
y : α✝ (castSucc i)
z : α✝ (last n)
α : Type u_1
β : Type u_2
g : α → β
q : Fin (Nat.succ n) → α
j : Fin n
⊢ (g ∘ init q) j = init (g ∘ q) j
[PROOFSTEP]
simp [init]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (succAbove i j)
⊢ insertNth i x p i = x
[PROOFSTEP]
simp [insertNth, succAboveCases]
[GOAL]
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
[PROOFSTEP]
simp only [insertNth, succAboveCases, dif_neg (succAbove_ne _ _), succAbove_lt_iff]
[GOAL]
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
[PROOFSTEP]
split_ifs with hlt
[GOAL]
case pos
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
[PROOFSTEP]
generalize_proofs H₁ H₂
[GOAL]
case pos
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
[PROOFSTEP]
revert H₂
[GOAL]
case pos
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
[PROOFSTEP]
generalize hk : castLT ((succAbove i) j) H₁ = k
[GOAL]
case pos
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
[PROOFSTEP]
rw [castLT_succAbove hlt] at hk 
[GOAL]
case pos
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
[PROOFSTEP]
cases hk
[GOAL]
case pos.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
[PROOFSTEP]
intro
[GOAL]
case pos.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
[PROOFSTEP]
rfl
[GOAL]
case neg
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
[PROOFSTEP]
generalize_proofs H₁ H₂
[GOAL]
case neg
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
[PROOFSTEP]
revert H₂
[GOAL]
case neg
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
[PROOFSTEP]
generalize hk : pred ((succAboveEmb i).toEmbedding j) H₁ = k
[GOAL]
case neg
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 (↑(succAboveEmb i).toEmbedding j) H₁ = k
⊢ ∀ (H₂ : succAbove i k = succAbove i j), H₂ ▸ p k = p j
[PROOFSTEP]
erw [pred_succAbove (le_of_not_lt hlt)] at hk 
[GOAL]
case neg
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
[PROOFSTEP]
cases hk
[GOAL]
case neg.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
[PROOFSTEP]
intro
[GOAL]
case neg.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
[PROOFSTEP]
rfl
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : β
p : Fin n → β
⊢ ∀ (x_1 : Fin n), (insertNth i x p ∘ succAbove i) x_1 = p x_1
[PROOFSTEP]
unfold comp
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : β
p : Fin n → β
⊢ ∀ (x_1 : Fin n), insertNth i x p (succAbove i x_1) = p x_1
[PROOFSTEP]
exact insertNth_apply_succAbove i _ _
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (succAbove i j)
q : (j : Fin (n + 1)) → α j
⊢ insertNth i x p = q ↔ q i = x ∧ p = fun j => q (succAbove i j)
[PROOFSTEP]
simp [funext_iff, forall_iff_succAbove i, eq_comm]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i j : Fin (n + 1)
h : j < i
x : α i
p : (k : Fin n) → α (succAbove i k)
⊢ insertNth i x p j = Eq.recOn (_ : succAbove i (castLT j (_ : ↑j < n)) = j) (p (castLT j (_ : ↑j < n)))
[PROOFSTEP]
rw [insertNth, succAboveCases, dif_neg h.ne, dif_pos h]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
i j : Fin (n + 1)
h : i < j
x : α i
p : (k : Fin n) → α (succAbove i k)
⊢ insertNth i x p j = Eq.recOn (_ : succAbove i (pred j (_ : j ≠ 0)) = j) (p (pred j (_ : j ≠ 0)))
[PROOFSTEP]
rw [insertNth, succAboveCases, dif_neg h.ne', dif_neg h.not_lt]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α 0
p : (j : Fin n) → α (succAbove 0 j)
⊢ insertNth 0 x p = cons x fun j => _root_.cast (_ : α (succAbove 0 j) = α (succ j)) (p j)
[PROOFSTEP]
refine' insertNth_eq_iff.2 ⟨by simp, _⟩
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α 0
p : (j : Fin n) → α (succAbove 0 j)
⊢ cons x (fun j => _root_.cast (_ : α (succAbove 0 j) = α (succ j)) (p j)) 0 = x
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α 0
p : (j : Fin n) → α (succAbove 0 j)
⊢ p = fun j => cons x (fun j => _root_.cast (_ : α (succAbove 0 j) = α (succ j)) (p j)) (succAbove 0 j)
[PROOFSTEP]
ext j
[GOAL]
case h
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α 0
p : (j : Fin n) → α (succAbove 0 j)
j : Fin n
⊢ p j = cons x (fun j => _root_.cast (_ : α (succAbove 0 j) = α (succ j)) (p j)) (succAbove 0 j)
[PROOFSTEP]
convert (cons_succ x p j).symm
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : β
p : Fin n → β
⊢ insertNth 0 x p = cons x p
[PROOFSTEP]
simp [insertNth_zero]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α (last n)
p : (j : Fin n) → α (succAbove (last n) j)
⊢ insertNth (last n) x p = snoc (fun j => _root_.cast (_ : α (succAbove (last n) j) = α (castSucc j)) (p j)) x
[PROOFSTEP]
refine' insertNth_eq_iff.2 ⟨by simp, _⟩
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α (last n)
p : (j : Fin n) → α (succAbove (last n) j)
⊢ snoc (fun j => _root_.cast (_ : α (succAbove (last n) j) = α (castSucc j)) (p j)) x (last n) = x
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α (last n)
p : (j : Fin n) → α (succAbove (last n) j)
⊢ p = fun j =>
    snoc (fun j => _root_.cast (_ : α (succAbove (last n) j) = α (castSucc j)) (p j)) x (succAbove (last n) j)
[PROOFSTEP]
ext j
[GOAL]
case h
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α (last n)
p : (j : Fin n) → α (succAbove (last n) j)
j : Fin n
⊢ p j = snoc (fun j => _root_.cast (_ : α (succAbove (last n) j) = α (castSucc j)) (p j)) x (succAbove (last n) j)
[PROOFSTEP]
apply eq_of_heq
[GOAL]
case h.h
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α (last n)
p : (j : Fin n) → α (succAbove (last n) j)
j : Fin n
⊢ HEq (p j) (snoc (fun j => _root_.cast (_ : α (succAbove (last n) j) = α (castSucc j)) (p j)) x (succAbove (last n) j))
[PROOFSTEP]
trans snoc (fun j ↦ _root_.cast (congr_arg α (succAbove_last_apply j)) (p j)) x (castSucc j)
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α (last n)
p : (j : Fin n) → α (succAbove (last n) j)
j : Fin n
⊢ HEq (p j) (snoc (fun j => _root_.cast (_ : α (succAbove (last n) j) = α (castSucc j)) (p j)) x (castSucc j))
[PROOFSTEP]
rw [snoc_castSucc]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α (last n)
p : (j : Fin n) → α (succAbove (last n) j)
j : Fin n
⊢ HEq (p j) (_root_.cast (_ : α (succAbove (last n) j) = α (castSucc j)) (p j))
[PROOFSTEP]
exact (cast_heq _ _).symm
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α (last n)
p : (j : Fin n) → α (succAbove (last n) j)
j : Fin n
⊢ HEq (snoc (fun j => _root_.cast (_ : α (succAbove (last n) j) = α (castSucc j)) (p j)) x (castSucc j))
    (snoc (fun j => _root_.cast (_ : α (succAbove (last n) j) = α (castSucc j)) (p j)) x (succAbove (last n) j))
[PROOFSTEP]
apply congr_arg_heq
[GOAL]
case a
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : α (last n)
p : (j : Fin n) → α (succAbove (last n) j)
j : Fin n
⊢ castSucc j = succAbove (last n) j
[PROOFSTEP]
rw [succAbove_last]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
x : β
p : Fin n → β
⊢ insertNth (last n) x p = snoc p x
[PROOFSTEP]
simp [insertNth_last]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
inst✝ : (j : Fin (n + 1)) → Zero (α j)
i : Fin (n + 1)
x : α i
⊢ Pi.single i x i = x ∧ 0 = fun j => Pi.single i x (succAbove i j)
[PROOFSTEP]
simp [succAbove_ne, Pi.zero_def]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
op : (j : Fin (n + 1)) → α j → α j → α j
i : Fin (n + 1)
x y : α i
p q : (j : Fin n) → α (succAbove i j)
⊢ op i (insertNth i x p i) (insertNth i y q i) = op i x y ∧
    (fun j => op (succAbove i j) (p j) (q j)) = fun j =>
      op (succAbove i j) (insertNth i x p (succAbove i j)) (insertNth i y q (succAbove i j))
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
inst✝ : (j : Fin (n + 1)) → AddGroup (α j)
i : Fin (n + 1)
x y : α i
p : (j : Fin n) → α (succAbove i j)
⊢ insertNth i x p - insertNth i y p = Pi.single i (x - y)
[PROOFSTEP]
simp_rw [← insertNth_sub, ← insertNth_zero_right, Pi.sub_def, sub_self, Pi.zero_def]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (succAbove i j)
q : (j : Fin (n + 1)) → α j
⊢ insertNth i x p ≤ q ↔ x ≤ q i ∧ p ≤ fun j => q (succAbove i j)
[PROOFSTEP]
simp [Pi.le_def, forall_iff_succAbove i]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (succAbove i j)
q : (j : Fin (n + 1)) → α j
⊢ q ≤ insertNth i x p ↔ q i ≤ x ∧ (fun j => q (succAbove i j)) ≤ p
[PROOFSTEP]
simp [Pi.le_def, forall_iff_succAbove i]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (succAbove i j)
q₁ q₂ : (j : Fin (n + 1)) → α j
⊢ insertNth i x p ∈ Icc q₁ q₂ ↔
    x ∈ Icc (q₁ i) (q₂ i) ∧ p ∈ Icc (fun j => q₁ (succAbove i j)) fun j => q₂ (succAbove i j)
[PROOFSTEP]
simp only [mem_Icc, insertNth_le_iff, le_insertNth_iff, and_assoc, @and_left_comm (x ≤ q₂ i)]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
i : Fin (n + 1)
x : α i
q₁ q₂ : (j : Fin (n + 1)) → α j
hx : x ∈ Icc (q₁ i) (q₂ i)
p : (j : Fin n) → α (succAbove i j)
⊢ p ∈ insertNth i x ⁻¹' Icc q₁ q₂ ↔ p ∈ Icc (fun j => q₁ (succAbove i j)) fun j => q₂ (succAbove i j)
[PROOFSTEP]
simp only [mem_preimage, insertNth_mem_Icc, hx, true_and_iff]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
i : Fin (n + 1)
x : α i
q₁ q₂ : (j : Fin (n + 1)) → α j
hx : ¬x ∈ Icc (q₁ i) (q₂ i)
p : (j : Fin n) → α (succAbove i j)
⊢ p ∈ insertNth i x ⁻¹' Icc q₁ q₂ ↔ p ∈ ∅
[PROOFSTEP]
simp only [mem_preimage, insertNth_mem_Icc, hx, false_and_iff, mem_empty_iff_false]
[GOAL]
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
⊢ Option (Fin (n + 1))
[PROOFSTEP]
exact
  Option.casesOn (@find n (fun i ↦ p (i.castLT (Nat.lt_succ_of_lt i.2))) _)
    (if _ : p (Fin.last n) then some (Fin.last n) else none) fun i ↦ some (i.castLT (Nat.lt_succ_of_lt i.2))
[GOAL]
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
hi : i ∈ find p
⊢ p i
[PROOFSTEP]
rw [find] at hi 
[GOAL]
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
hi :
  i ∈
    Option.casesOn (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) (if x : p (last n) then some (last n) else none)
      fun i => some (castLT i (_ : ↑i < Nat.succ n))
⊢ p i
[PROOFSTEP]
cases' h : find fun i : Fin n ↦ p (i.castLT (Nat.lt_succ_of_lt i.2)) with j
[GOAL]
case none
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
hi :
  i ∈
    Option.casesOn (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) (if x : p (last n) then some (last n) else none)
      fun i => some (castLT i (_ : ↑i < Nat.succ n))
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
⊢ p i
[PROOFSTEP]
rw [h] at hi 
[GOAL]
case none
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
hi :
  i ∈
    Option.casesOn none (if x : p (last n) then some (last n) else none) fun i => some (castLT i (_ : ↑i < Nat.succ n))
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
⊢ p i
[PROOFSTEP]
dsimp at hi 
[GOAL]
case none
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
hi : i ∈ if p (last n) then some (last n) else none
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
⊢ p i
[PROOFSTEP]
split_ifs at hi  with hl
[GOAL]
case pos
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : p (last n)
hi : i ∈ some (last n)
⊢ p i
[PROOFSTEP]
simp only [Option.mem_def, Option.some.injEq] at hi 
[GOAL]
case pos
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : p (last n)
hi : last n = i
⊢ p i
[PROOFSTEP]
exact hi ▸ hl
[GOAL]
case neg
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : ¬p (last n)
hi : i ∈ none
⊢ p i
[PROOFSTEP]
exact (Option.not_mem_none _ hi).elim
[GOAL]
case some
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
hi :
  i ∈
    Option.casesOn (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) (if x : p (last n) then some (last n) else none)
      fun i => some (castLT i (_ : ↑i < Nat.succ n))
j : Fin n
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = some j
⊢ p i
[PROOFSTEP]
rw [h] at hi 
[GOAL]
case some
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
j : Fin n
hi :
  i ∈
    Option.casesOn (some j) (if x : p (last n) then some (last n) else none) fun i =>
      some (castLT i (_ : ↑i < Nat.succ n))
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = some j
⊢ p i
[PROOFSTEP]
dsimp at hi 
[GOAL]
case some
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
j : Fin n
hi : i ∈ some (castLT j (_ : ↑j < Nat.succ n))
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = some j
⊢ p i
[PROOFSTEP]
rw [← Option.some_inj.1 hi]
[GOAL]
case some
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
j : Fin n
hi : i ∈ some (castLT j (_ : ↑j < Nat.succ n))
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = some j
⊢ p (castLT j (_ : ↑j < Nat.succ n))
[PROOFSTEP]
refine @find_spec n (fun i ↦ p (i.castLT (Nat.lt_succ_of_lt i.2))) _ _ h
[GOAL]
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
h : Option.isSome (find p) = true
⊢ ∃ i, p i
[PROOFSTEP]
rw [Option.isSome_iff_exists] at h 
[GOAL]
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
h : ∃ a, find p = some a
⊢ ∃ i, p i
[PROOFSTEP]
cases' h with i hi
[GOAL]
case intro
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
hi : find p = some i
⊢ ∃ i, p i
[PROOFSTEP]
exact ⟨i, find_spec _ hi⟩
[GOAL]
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p { val := i, isLt := hin }
⊢ Option.isSome (find p) = true
[PROOFSTEP]
dsimp [find]
[GOAL]
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p { val := i, isLt := hin }
⊢ Option.isSome
      (Option.rec (if p (last n) then some (last n) else none) (fun val => some (castLT val (_ : ↑val < Nat.succ n)))
        (find fun i => p (castLT i (_ : ↑i < Nat.succ n)))) =
    true
[PROOFSTEP]
cases' h : find fun i : Fin n ↦ p (i.castLT (Nat.lt_succ_of_lt i.2)) with j
[GOAL]
case none
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p { val := i, isLt := hin }
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
⊢ Option.isSome
      (Option.rec (if p (last n) then some (last n) else none) (fun val => some (castLT val (_ : ↑val < Nat.succ n)))
        none) =
    true
[PROOFSTEP]
split_ifs with hl
[GOAL]
case pos
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p { val := i, isLt := hin }
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : p (last n)
⊢ Option.isSome (Option.rec (some (last n)) (fun val => some (castLT val (_ : ↑val < Nat.succ n))) none) = true
[PROOFSTEP]
exact Option.isSome_some
[GOAL]
case neg
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p { val := i, isLt := hin }
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : ¬p (last n)
⊢ Option.isSome (Option.rec none (fun val => some (castLT val (_ : ↑val < Nat.succ n))) none) = true
[PROOFSTEP]
have :=
  (@isSome_find_iff n (fun x ↦ p (x.castLT (Nat.lt_succ_of_lt x.2))) _).2
    ⟨⟨i, lt_of_le_of_ne (Nat.le_of_lt_succ hin) fun h ↦ by cases h; exact hl hi⟩, hi⟩
[GOAL]
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p { val := i, isLt := hin }
h✝ : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : ¬p (last n)
h : i = n
⊢ False
[PROOFSTEP]
cases h
[GOAL]
case refl
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : ¬p (last n)
hin : n < n + 1
hi : p { val := n, isLt := hin }
⊢ False
[PROOFSTEP]
exact hl hi
[GOAL]
case neg
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p { val := i, isLt := hin }
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : ¬p (last n)
this : Option.isSome (find fun x => p (castLT x (_ : ↑x < Nat.succ n))) = true
⊢ Option.isSome (Option.rec none (fun val => some (castLT val (_ : ↑val < Nat.succ n))) none) = true
[PROOFSTEP]
rw [h] at this 
[GOAL]
case neg
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p { val := i, isLt := hin }
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : ¬p (last n)
this : Option.isSome none = true
⊢ Option.isSome (Option.rec none (fun val => some (castLT val (_ : ↑val < Nat.succ n))) none) = true
[PROOFSTEP]
exact this
[GOAL]
case some
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p { val := i, isLt := hin }
j : Fin n
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = some j
⊢ Option.isSome
      (Option.rec (if p (last n) then some (last n) else none) (fun val => some (castLT val (_ : ↑val < Nat.succ n)))
        (some j)) =
    true
[PROOFSTEP]
simp
[GOAL]
m n✝ n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
⊢ find p = none ↔ ∀ (i : Fin n), ¬p i
[PROOFSTEP]
rw [← not_exists, ← isSome_find_iff]
[GOAL]
m n✝ n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
⊢ find p = none ↔ ¬Option.isSome (find fun x => p x) = true
[PROOFSTEP]
cases find p
[GOAL]
case none
m n✝ n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
⊢ none = none ↔ ¬Option.isSome none = true
[PROOFSTEP]
simp
[GOAL]
case some
m n✝ n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
val✝ : Fin n
⊢ some val✝ = none ↔ ¬Option.isSome (some val✝) = true
[PROOFSTEP]
simp
[GOAL]
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
hi : i ∈ find p
j : ℕ
hjn : j < n + 1
hj : { val := j, isLt := hjn } < i
hpj : p { val := j, isLt := hjn }
⊢ False
[PROOFSTEP]
rw [find] at hi 
[GOAL]
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
hi :
  i ∈
    Option.casesOn (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) (if x : p (last n) then some (last n) else none)
      fun i => some (castLT i (_ : ↑i < Nat.succ n))
j : ℕ
hjn : j < n + 1
hj : { val := j, isLt := hjn } < i
hpj : p { val := j, isLt := hjn }
⊢ False
[PROOFSTEP]
cases' h : find fun i : Fin n ↦ p (i.castLT (Nat.lt_succ_of_lt i.2)) with k
[GOAL]
case none
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
hi :
  i ∈
    Option.casesOn (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) (if x : p (last n) then some (last n) else none)
      fun i => some (castLT i (_ : ↑i < Nat.succ n))
j : ℕ
hjn : j < n + 1
hj : { val := j, isLt := hjn } < i
hpj : p { val := j, isLt := hjn }
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
⊢ False
[PROOFSTEP]
simp only [h] at hi 
[GOAL]
case none
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
j : ℕ
hjn : j < n + 1
hj : { val := j, isLt := hjn } < i
hpj : p { val := j, isLt := hjn }
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hi : i ∈ if x : p (last n) then some (last n) else none
⊢ False
[PROOFSTEP]
split_ifs at hi  with hl
[GOAL]
case pos
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
j : ℕ
hjn : j < n + 1
hj : { val := j, isLt := hjn } < i
hpj : p { val := j, isLt := hjn }
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : p (last n)
hi : i ∈ some (last n)
⊢ False
[PROOFSTEP]
cases hi
[GOAL]
case pos.refl
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
j : ℕ
hjn : j < n + 1
hpj : p { val := j, isLt := hjn }
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : p (last n)
hj : { val := j, isLt := hjn } < last n
⊢ False
[PROOFSTEP]
rw [find_eq_none_iff] at h 
[GOAL]
case pos.refl
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
j : ℕ
hjn : j < n + 1
hpj : p { val := j, isLt := hjn }
h : ∀ (i : Fin n), ¬p (castLT i (_ : ↑i < Nat.succ n))
hl : p (last n)
hj : { val := j, isLt := hjn } < last n
⊢ False
[PROOFSTEP]
refine h ⟨j, hj⟩ hpj
[GOAL]
case neg
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
j : ℕ
hjn : j < n + 1
hj : { val := j, isLt := hjn } < i
hpj : p { val := j, isLt := hjn }
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : ¬p (last n)
hi : i ∈ none
⊢ False
[PROOFSTEP]
exact Option.not_mem_none _ hi
[GOAL]
case some
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
hi :
  i ∈
    Option.casesOn (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) (if x : p (last n) then some (last n) else none)
      fun i => some (castLT i (_ : ↑i < Nat.succ n))
j : ℕ
hjn : j < n + 1
hj : { val := j, isLt := hjn } < i
hpj : p { val := j, isLt := hjn }
k : Fin n
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = some k
⊢ False
[PROOFSTEP]
rw [h] at hi 
[GOAL]
case some
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
j : ℕ
hjn : j < n + 1
hj : { val := j, isLt := hjn } < i
hpj : p { val := j, isLt := hjn }
k : Fin n
hi :
  i ∈
    Option.casesOn (some k) (if x : p (last n) then some (last n) else none) fun i =>
      some (castLT i (_ : ↑i < Nat.succ n))
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = some k
⊢ False
[PROOFSTEP]
dsimp at hi 
[GOAL]
case some
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
j : ℕ
hjn : j < n + 1
hj : { val := j, isLt := hjn } < i
hpj : p { val := j, isLt := hjn }
k : Fin n
hi : i ∈ some (castLT k (_ : ↑k < Nat.succ n))
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = some k
⊢ False
[PROOFSTEP]
obtain rfl := Option.some_inj.1 hi
[GOAL]
case some
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
j : ℕ
hjn : j < n + 1
hpj : p { val := j, isLt := hjn }
k : Fin n
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = some k
hj : { val := j, isLt := hjn } < castLT k (_ : ↑k < Nat.succ n)
hi : castLT k (_ : ↑k < Nat.succ n) ∈ some (castLT k (_ : ↑k < Nat.succ n))
⊢ False
[PROOFSTEP]
exact find_min h (show (⟨j, lt_trans hj k.2⟩ : Fin n) < k from hj) hpj
[GOAL]
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i hin, p { val := i, isLt := hin }
⊢ { val := Nat.find h, isLt := (_ : Nat.find h < n) } ∈ find p
[PROOFSTEP]
let ⟨i, hin, hi⟩ := h
[GOAL]
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i hin, p { val := i, isLt := hin }
i : ℕ
hin : i < n
hi : p { val := i, isLt := hin }
⊢ { val := Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }),
      isLt := (_ : Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }) < n) } ∈
    find p
[PROOFSTEP]
cases' hf : find p with f
[GOAL]
case none
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i hin, p { val := i, isLt := hin }
i : ℕ
hin : i < n
hi : p { val := i, isLt := hin }
hf : find p = none
⊢ { val := Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }),
      isLt := (_ : Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }) < n) } ∈
    none
[PROOFSTEP]
rw [find_eq_none_iff] at hf 
[GOAL]
case none
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i hin, p { val := i, isLt := hin }
i : ℕ
hin : i < n
hi : p { val := i, isLt := hin }
hf : ∀ (i : Fin n), ¬p i
⊢ { val := Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }),
      isLt := (_ : Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }) < n) } ∈
    none
[PROOFSTEP]
exact (hf ⟨i, hin⟩ hi).elim
[GOAL]
case some
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i hin, p { val := i, isLt := hin }
i : ℕ
hin : i < n
hi : p { val := i, isLt := hin }
f : Fin n
hf : find p = some f
⊢ { val := Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }),
      isLt := (_ : Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }) < n) } ∈
    some f
[PROOFSTEP]
refine' Option.some_inj.2 (le_antisymm _ _)
[GOAL]
case some.refine'_1
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i hin, p { val := i, isLt := hin }
i : ℕ
hin : i < n
hi : p { val := i, isLt := hin }
f : Fin n
hf : find p = some f
⊢ f ≤
    { val := Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }),
      isLt := (_ : Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }) < n) }
[PROOFSTEP]
exact find_min' hf (Nat.find_spec h).snd
[GOAL]
case some.refine'_2
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i hin, p { val := i, isLt := hin }
i : ℕ
hin : i < n
hi : p { val := i, isLt := hin }
f : Fin n
hf : find p = some f
⊢ { val := Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }),
      isLt := (_ : Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }) < n) } ≤
    f
[PROOFSTEP]
exact Nat.find_min' _ ⟨f.2, by convert find_spec p hf⟩
[GOAL]
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i hin, p { val := i, isLt := hin }
i : ℕ
hin : i < n
hi : p { val := i, isLt := hin }
f : Fin n
hf : find p = some f
⊢ p { val := ↑f, isLt := (_ : ↑f < n) }
[PROOFSTEP]
convert find_spec p hf
[GOAL]
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
⊢ (p i ∧ ∀ (j : Fin n), p j → i ≤ j) → i ∈ find p
[PROOFSTEP]
rintro ⟨hpi, hj⟩
[GOAL]
case intro
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
hpi : p i
hj : ∀ (j : Fin n), p j → i ≤ j
⊢ i ∈ find p
[PROOFSTEP]
cases hfp : Fin.find p
[GOAL]
case intro.none
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
hpi : p i
hj : ∀ (j : Fin n), p j → i ≤ j
hfp : find p = none
⊢ i ∈ none
[PROOFSTEP]
rw [find_eq_none_iff] at hfp 
[GOAL]
case intro.none
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
hpi : p i
hj : ∀ (j : Fin n), p j → i ≤ j
hfp : ∀ (i : Fin n), ¬p i
⊢ i ∈ none
[PROOFSTEP]
exact (hfp _ hpi).elim
[GOAL]
case intro.some
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
hpi : p i
hj : ∀ (j : Fin n), p j → i ≤ j
val✝ : Fin n
hfp : find p = some val✝
⊢ i ∈ some val✝
[PROOFSTEP]
exact Option.some_inj.2 (le_antisymm (find_min' hfp hpi) (hj _ (find_spec _ hfp)))
[GOAL]
m n : ℕ
α : Type u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
h : ↑k = ↑j
⊢ contractNth j op g k = op (g (castSucc k)) (g (succ k))
[PROOFSTEP]
have : ¬(k : ℕ) < j := not_lt.2 (le_of_eq h.symm)
[GOAL]
m n : ℕ
α : Type u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
h : ↑k = ↑j
this : ¬↑k < ↑j
⊢ contractNth j op g k = op (g (castSucc k)) (g (succ k))
[PROOFSTEP]
rw [contractNth, if_neg this, if_pos h]
[GOAL]
m n : ℕ
α : Type u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
h : ↑j < ↑k
⊢ contractNth j op g k = g (succ k)
[PROOFSTEP]
rw [contractNth, if_neg (not_lt_of_gt h), if_neg (Ne.symm <| ne_of_lt h)]
[GOAL]
m n : ℕ
α : Type u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
⊢ contractNth j op g k = g (succAbove j k)
[PROOFSTEP]
rcases lt_trichotomy (k : ℕ) j with (h | h | h)
[GOAL]
case inl
m n : ℕ
α : Type u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑k < ↑j
⊢ contractNth j op g k = g (succAbove j k)
[PROOFSTEP]
rwa [j.succAbove_below, contractNth_apply_of_lt]
[GOAL]
case inl.h
m n : ℕ
α : Type u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑k < ↑j
⊢ castSucc k < j
[PROOFSTEP]
rwa [Fin.lt_iff_val_lt_val]
[GOAL]
case inr.inl
m n : ℕ
α : Type u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑k = ↑j
⊢ contractNth j op g k = g (succAbove j k)
[PROOFSTEP]
exact False.elim (hjk h.symm)
[GOAL]
case inr.inr
m n : ℕ
α : Type u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑j < ↑k
⊢ contractNth j op g k = g (succAbove j k)
[PROOFSTEP]
rwa [j.succAbove_above, contractNth_apply_of_gt]
[GOAL]
case inr.inr.h
m n : ℕ
α : Type u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑j < ↑k
⊢ j ≤ castSucc k
[PROOFSTEP]
exact Fin.le_iff_val_le_val.2 (le_of_lt h)
[GOAL]
m n : ℕ
α : Type u_1
ai : ℕ
a : Fin ai → α
bi : ℕ
b : Fin bi → α
hi : { fst := ai, snd := a }.fst = { fst := bi, snd := b }.fst
h : { fst := ai, snd := a }.snd = { fst := bi, snd := b }.snd ∘ ↑(castIso hi)
⊢ { fst := ai, snd := a } = { fst := bi, snd := b }
[PROOFSTEP]
dsimp only at hi 
[GOAL]
m n : ℕ
α : Type u_1
ai : ℕ
a : Fin ai → α
bi : ℕ
b : Fin bi → α
hi : ai = bi
h : { fst := ai, snd := a }.snd = { fst := bi, snd := b }.snd ∘ ↑(castIso hi)
⊢ { fst := ai, snd := a } = { fst := bi, snd := b }
[PROOFSTEP]
subst hi
[GOAL]
m n : ℕ
α : Type u_1
ai : ℕ
a b : Fin ai → α
h : { fst := ai, snd := a }.snd = { fst := ai, snd := b }.snd ∘ ↑(castIso (_ : ai = ai))
⊢ { fst := ai, snd := a } = { fst := ai, snd := b }
[PROOFSTEP]
simpa using h
