no goals
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : SizeOf α
l₁ l₂ : List α
h : l₁ ~ l₂
⊢ sizeOf l₁ = sizeOf l₂
induction h with | nil => rfl
| cons _ _ h_sz₁₂ => simp [h_sz₁₂]
| swap => simp [add_left_comm]
| trans _ _ h_sz₁₂ h_sz₂₃ => simp [h_sz₁₂, h_sz₂₃]
no goals
case nil
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : SizeOf α
l₁ l₂ : List α
⊢ sizeOf [] = sizeOf []
rfl
no goals
case cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
inst✝ : SizeOf α
l₁ l₂ : List α
x✝ : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
h_sz₁₂ : sizeOf l₁✝ = sizeOf l₂✝
⊢ sizeOf (x✝ :: l₁✝) = sizeOf (x✝ :: l₂✝)
simp [h_sz₁₂]
no goals
case swap
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : SizeOf α
l₁ l₂ : List α
x✝ y✝ : α
l✝ : List α
⊢ sizeOf (y✝ :: x✝ :: l✝) = sizeOf (x✝ :: y✝ :: l✝)
simp [add_left_comm]
no goals
case trans
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
inst✝ : SizeOf α
l₁ l₂ l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
h_sz₁₂ : sizeOf l₁✝ = sizeOf l₂✝
h_sz₂₃ : sizeOf l₂✝ = sizeOf l₃✝
⊢ sizeOf l₁✝ = sizeOf l₃✝
simp [h_sz₁₂, h_sz₂₃]