no goals
α : Type u_1
l₁ l₂ : List α
hl : length l₁ = length l₂
h :
  ∀ (n : Nat) (h₁ : n < length l₁) (h₂ : n < length l₂),
    get l₁ { val := n, isLt := h₁ } = get l₂ { val := n, isLt := h₂ }
n : Nat
h₁ : n < length l₁
⊢ get? l₁ n = get? l₂ n
rw [get?_eq_get, get?_eq_get, h n h₁ (by rwa [← hl])]
no goals
α : Type u_1
l₁ l₂ : List α
hl : length l₁ = length l₂
h :
  ∀ (n : Nat) (h₁ : n < length l₁) (h₂ : n < length l₂),
    get l₁ { val := n, isLt := h₁ } = get l₂ { val := n, isLt := h₂ }
n : Nat
h₁ : n < length l₁
⊢ n < length l₂
rwa [← hl]
α : Type u_1
l₁ l₂ : List α
hl : length l₁ = length l₂
h :
  ∀ (n : Nat) (h₁ : n < length l₁) (h₂ : n < length l₂),
    get l₁ { val := n, isLt := h₁ } = get l₂ { val := n, isLt := h₂ }
n : Nat
h₁✝ : ¬n < length l₁
h₁ : length l₁ ≤ n
⊢ get? l₁ n = get? l₂ n
α : Type u_1
l₁ l₂ : List α
hl : length l₁ = length l₂
h :
  ∀ (n : Nat) (h₁ : n < length l₁) (h₂ : n < length l₂),
    get l₁ { val := n, isLt := h₁ } = get l₂ { val := n, isLt := h₂ }
n : Nat
h₁ : ¬n < length l₁
⊢ get? l₁ n = get? l₂ n
have h₁ := Nat.le_of_not_lt h₁
α : Type u_1
l₁ l₂ : List α
hl : length l₁ = length l₂
h :
  ∀ (n : Nat) (h₁ : n < length l₁) (h₂ : n < length l₂),
    get l₁ { val := n, isLt := h₁ } = get l₂ { val := n, isLt := h₂ }
n : Nat
h₁✝ : ¬n < length l₁
h₁ : length l₁ ≤ n
⊢ length l₂ ≤ n
α : Type u_1
l₁ l₂ : List α
hl : length l₁ = length l₂
h :
  ∀ (n : Nat) (h₁ : n < length l₁) (h₂ : n < length l₂),
    get l₁ { val := n, isLt := h₁ } = get l₂ { val := n, isLt := h₂ }
n : Nat
h₁✝ : ¬n < length l₁
h₁ : length l₁ ≤ n
⊢ get? l₁ n = get? l₂ n
rw [get?_len_le h₁, get?_len_le]
no goals
α : Type u_1
l₁ l₂ : List α
hl : length l₁ = length l₂
h :
  ∀ (n : Nat) (h₁ : n < length l₁) (h₂ : n < length l₂),
    get l₁ { val := n, isLt := h₁ } = get l₂ { val := n, isLt := h₂ }
n : Nat
h₁✝ : ¬n < length l₁
h₁ : length l₁ ≤ n
⊢ length l₂ ≤ n
rwa [← hl]