Theorem: Quotient.liftVec_mk (Logic/Vorspiel/Vorspiel.lean)

State before:
α : Type u
s : Setoid α
β : Sort v
n : ℕ
f : (Fin n → α) → β
h : ∀ (v₁ v₂ : Fin n → α), (∀ (n : Fin n), v₁ n ≈ v₂ n) → f v₁ = f v₂
v : Fin n → α
⊢ liftVec f h (Quotient.mk s ∘ v) = f v
Tactic:
induction' n with n ih <;> simp[liftVec, empty_eq, Quotient.liftOn_mk]
State after:
case succ
α : Type u
s : Setoid α
β : Sort v
n : ℕ
ih :
  ∀ (f : (Fin n → α) → β) (h : ∀ (v₁ v₂ : Fin n → α), (∀ (n : Fin n), v₁ n ≈ v₂ n) → f v₁ = f v₂) (v : Fin n → α),
    liftVec f h (Quotient.mk s ∘ v) = f v
f : (Fin (n + 1) → α) → β
h : ∀ (v₁ v₂ : Fin (n + 1) → α), (∀ (n : Fin (n + 1)), v₁ n ≈ v₂ n) → f v₁ = f v₂
v : Fin (n + 1) → α
⊢ liftVec (fun v_1 => f (vecHead v :> v_1)) ⋯ (Quotient.mk s ∘ vecTail v) = f v

State before:
case succ
α : Type u
s : Setoid α
β : Sort v
n : ℕ
ih :
  ∀ (f : (Fin n → α) → β) (h : ∀ (v₁ v₂ : Fin n → α), (∀ (n : Fin n), v₁ n ≈ v₂ n) → f v₁ = f v₂) (v : Fin n → α),
    liftVec f h (Quotient.mk s ∘ v) = f v
f : (Fin (n + 1) → α) → β
h : ∀ (v₁ v₂ : Fin (n + 1) → α), (∀ (n : Fin (n + 1)), v₁ n ≈ v₂ n) → f v₁ = f v₂
v : Fin (n + 1) → α
⊢ liftVec (fun v_1 => f (vecHead v :> v_1)) ⋯ (Quotient.mk s ∘ vecTail v) = f v
Tactic:
simpa using ih (fun v' => f (vecHead v :> v'))
  (fun v₁ v₂ hv => h (vecHead v :> v₁) (vecHead v :> v₂) (Fin.cases (refl _) hv)) (vecTail v)
State after:
no goals