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
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)
ext j
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

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
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
by_cases h : j = 0
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
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
rw [h]
no goals
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
rfl
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
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
let j' := pred j h
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
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
have : j'.succ = j := succ_pred j h
no goals
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
rw [← this, cons_succ, comp, comp, cons_succ]