α✝ : Type u_1
s₁ t₁ s₂ t₂ : List α✝
h : s₁ ++ t₁ = s₂ ++ t₂
hl : length t₁ = length t₂
hap : length (s₁ ++ t₁) = length (s₂ ++ t₂) := congrArg length h
⊢ length s₁ + length t₁ = length s₂ + length t₁
α✝ : Type u_1
s₁ t₁ s₂ t₂ : List α✝
h : s₁ ++ t₁ = s₂ ++ t₂
hl : length t₁ = length t₂
⊢ length s₁ + length t₁ = length s₂ + length t₁
let hap := congrArg length h
α✝ : Type u_1
s₁ t₁ s₂ t₂ : List α✝
h : s₁ ++ t₁ = s₂ ++ t₂
hl : length t₁ = length t₂
hap : length s₁ + length t₁ = length s₂ + length t₁
⊢ length s₁ + length t₁ = length s₂ + length t₁
α✝ : Type u_1
s₁ t₁ s₂ t₂ : List α✝
h : s₁ ++ t₁ = s₂ ++ t₂
hl : length t₁ = length t₂
hap : length (s₁ ++ t₁) = length (s₂ ++ t₂) := congrArg length h
⊢ length s₁ + length t₁ = length s₂ + length t₁
simp only [length_append, ← hl] at hap
no goals
α✝ : Type u_1
s₁ t₁ s₂ t₂ : List α✝
h : s₁ ++ t₁ = s₂ ++ t₂
hl : length t₁ = length t₂
hap : length s₁ + length t₁ = length s₂ + length t₁
⊢ length s₁ + length t₁ = length s₂ + length t₁
exact hap