Theorem: List.finite_length_eq (LeanCamCombi/Mathlib/Data/Set/Finite.lean)

State before:
case zero
α : Type u_1
inst✝ : Finite α
n : ℕ
⊢ {l | l.length = 0}.Finite
Tactic:
simp [List.length_eq_zero]
State after:
no goals

State before:
case succ
α : Type u_1
inst✝ : Finite α
n✝ n : ℕ
ih : {l | l.length = n}.Finite
⊢ {l | l.length = n + 1} = image2 (fun x x_1 => x :: x_1) univ {l | l.length = n}
Tactic:
ext (_ | _) <;> simp [n.succ_ne_zero.symm]
State after:
no goals

State before:
α : Type u_1
inst✝ : Finite α
n✝ n : ℕ
ih : {l | l.length = n}.Finite
this : {l | l.length = n + 1} = image2 (fun x x_1 => x :: x_1) univ {l | l.length = n}
⊢ {l | l.length = n + 1}.Finite
Tactic:
rw [this]
State after:
α : Type u_1
inst✝ : Finite α
n✝ n : ℕ
ih : {l | l.length = n}.Finite
this : {l | l.length = n + 1} = image2 (fun x x_1 => x :: x_1) univ {l | l.length = n}
⊢ (image2 (fun x x_1 => x :: x_1) univ {l | l.length = n}).Finite

State before:
α : Type u_1
inst✝ : Finite α
n✝ n : ℕ
ih : {l | l.length = n}.Finite
this : {l | l.length = n + 1} = image2 (fun x x_1 => x :: x_1) univ {l | l.length = n}
⊢ (image2 (fun x x_1 => x :: x_1) univ {l | l.length = n}).Finite
Tactic:
exact Set.finite_univ.image2 _ ih
State after:
no goals