Theorem: List.get_eq_get (LeanColls/Data/List.lean)

State before:
α : Type u_1
L1 L2 : List α
i : Fin L1.length
j : Fin L2.length
⊢ L1 = L2 → ↑i = ↑j → L1.get i = L2.get j
Tactic:
cases i
State after:
case mk
α : Type u_1
L1 L2 : List α
j : Fin L2.length
val✝ : ℕ
isLt✝ : val✝ < L1.length
⊢ L1 = L2 → ↑⟨val✝, isLt✝⟩ = ↑j → L1.get ⟨val✝, isLt✝⟩ = L2.get j

State before:
case mk
α : Type u_1
L1 L2 : List α
j : Fin L2.length
val✝ : ℕ
isLt✝ : val✝ < L1.length
⊢ L1 = L2 → ↑⟨val✝, isLt✝⟩ = ↑j → L1.get ⟨val✝, isLt✝⟩ = L2.get j
Tactic:
cases j
State after:
case mk.mk
α : Type u_1
L1 L2 : List α
val✝¹ : ℕ
isLt✝¹ : val✝¹ < L1.length
val✝ : ℕ
isLt✝ : val✝ < L2.length
⊢ L1 = L2 → ↑⟨val✝¹, isLt✝¹⟩ = ↑⟨val✝, isLt✝⟩ → L1.get ⟨val✝¹, isLt✝¹⟩ = L2.get ⟨val✝, isLt✝⟩

State before:
case mk.mk
α : Type u_1
L1 L2 : List α
val✝¹ : ℕ
isLt✝¹ : val✝¹ < L1.length
val✝ : ℕ
isLt✝ : val✝ < L2.length
⊢ L1 = L2 → ↑⟨val✝¹, isLt✝¹⟩ = ↑⟨val✝, isLt✝⟩ → L1.get ⟨val✝¹, isLt✝¹⟩ = L2.get ⟨val✝, isLt✝⟩
Tactic:
rintro rfl h
State after:
case mk.mk
α : Type u_1
L1 : List α
val✝¹ : ℕ
isLt✝¹ : val✝¹ < L1.length
val✝ : ℕ
isLt✝ : val✝ < L1.length
h : ↑⟨val✝¹, isLt✝¹⟩ = ↑⟨val✝, isLt✝⟩
⊢ L1.get ⟨val✝¹, isLt✝¹⟩ = L1.get ⟨val✝, isLt✝⟩

State before:
case mk.mk
α : Type u_1
L1 : List α
val✝¹ : ℕ
isLt✝¹ : val✝¹ < L1.length
val✝ : ℕ
isLt✝ : val✝ < L1.length
h : ↑⟨val✝¹, isLt✝¹⟩ = ↑⟨val✝, isLt✝⟩
⊢ L1.get ⟨val✝¹, isLt✝¹⟩ = L1.get ⟨val✝, isLt✝⟩
Tactic:
simp at h
State after:
case mk.mk
α : Type u_1
L1 : List α
val✝¹ : ℕ
isLt✝¹ : val✝¹ < L1.length
val✝ : ℕ
isLt✝ : val✝ < L1.length
h : val✝¹ = val✝
⊢ L1.get ⟨val✝¹, isLt✝¹⟩ = L1.get ⟨val✝, isLt✝⟩

State before:
case mk.mk
α : Type u_1
L1 : List α
val✝¹ : ℕ
isLt✝¹ : val✝¹ < L1.length
val✝ : ℕ
isLt✝ : val✝ < L1.length
h : val✝¹ = val✝
⊢ L1.get ⟨val✝¹, isLt✝¹⟩ = L1.get ⟨val✝, isLt✝⟩
Tactic:
cases h
State after:
case mk.mk.refl
α : Type u_1
L1 : List α
val✝ : ℕ
isLt✝¹ isLt✝ : val✝ < L1.length
⊢ L1.get ⟨val✝, isLt✝¹⟩ = L1.get ⟨val✝, isLt✝⟩

State before:
case mk.mk.refl
α : Type u_1
L1 : List α
val✝ : ℕ
isLt✝¹ isLt✝ : val✝ < L1.length
⊢ L1.get ⟨val✝, isLt✝¹⟩ = L1.get ⟨val✝, isLt✝⟩
Tactic:
rfl
State after:
no goals