case zero
ι : Type ?u.128977
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a x : α
⊢ Injective (insertNth zero x)

case succ
ι : Type ?u.128977
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a x : α
n : ℕ
IH : Injective (insertNth n x)
⊢ Injective (insertNth (succ n) x)
ι : Type ?u.128977
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
n : ℕ
x : α
⊢ Injective (insertNth n x)
induction' n with n IH
case zero
ι : Type ?u.128977
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a x : α
this : insertNth 0 x = cons x
⊢ Injective (insertNth zero x)
case zero
ι : Type ?u.128977
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a x : α
⊢ Injective (insertNth zero x)
have : insertNth 0 x = cons x := funext fun _ => rfl
no goals
case zero
ι : Type ?u.128977
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a x : α
this : insertNth 0 x = cons x
⊢ Injective (insertNth zero x)
simp [this]
no goals
case succ
ι : Type ?u.128977
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a x : α
n : ℕ
IH : Injective (insertNth n x)
⊢ Injective (insertNth (succ n) x)
rintro (_ | ⟨a, as⟩) (_ | ⟨b, bs⟩) h <;> simpa [IH.eq_iff] using h