ι : Type ?u.104743
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
h : length l = 1
n : ℕ
h₁ : n < length l
h₂ : n < length [nthLe l 0 (_ : 0 < length l)]
⊢ get l { val := n, isLt := h₁ } = get [nthLe l 0 (_ : 0 < length l)] { val := n, isLt := h₂ }
ι : Type ?u.104743
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
h : length l = 1
⊢ l = [nthLe l 0 (_ : 0 < length l)]
refine' ext_get (by convert h) fun n h₁ h₂ => _
ι : Type ?u.104743
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
h : length l = 1
n : ℕ
h₁ : n < length l
h₂ : n < length [nthLe l 0 (_ : 0 < length l)]
⊢ get l { val := n, isLt := h₁ } = nthLe l 0 (_ : 0 < length l)
ι : Type ?u.104743
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
h : length l = 1
n : ℕ
h₁ : n < length l
h₂ : n < length [nthLe l 0 (_ : 0 < length l)]
⊢ get l { val := n, isLt := h₁ } = get [nthLe l 0 (_ : 0 < length l)] { val := n, isLt := h₂ }
simp only [get_singleton]
case e_a.e_val
ι : Type ?u.104743
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
h : length l = 1
n : ℕ
h₁ : n < length l
h₂ : n < length [nthLe l 0 (_ : 0 < length l)]
⊢ n = 0
ι : Type ?u.104743
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
h : length l = 1
n : ℕ
h₁ : n < length l
h₂ : n < length [nthLe l 0 (_ : 0 < length l)]
⊢ get l { val := n, isLt := h₁ } = nthLe l 0 (_ : 0 < length l)
congr
no goals
case e_a.e_val
ι : Type ?u.104743
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
h : length l = 1
n : ℕ
h₁ : n < length l
h₂ : n < length [nthLe l 0 (_ : 0 < length l)]
⊢ n = 0
exact eq_bot_iff.mpr (Nat.lt_succ_iff.mp h₂)
no goals
ι : Type ?u.104743
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
h : length l = 1
⊢ length l = length [nthLe l 0 (_ : 0 < length l)]
convert h