Theorem: List.zip_length_eq_of_length_eq (Table/BuiltinExtensions.lean)

State before:
α : Type u_1
β : Type u_2
x : α
xs : List α
y : β
ys : List β
h : length (x :: xs) = length (y :: ys)
⊢ length xs = length ys
Tactic:
simp only [List.length] at h
State after:
α : Type u_1
β : Type u_2
x : α
xs : List α
y : β
ys : List β
h : length xs + 1 = length ys + 1
⊢ length xs = length ys

State before:
α : Type u_1
β : Type u_2
x : α
xs : List α
y : β
ys : List β
h : length xs + 1 = length ys + 1
⊢ length xs = length ys
Tactic:
apply Nat.succ.inj
State after:
case x
α : Type u_1
β : Type u_2
x : α
xs : List α
y : β
ys : List β
h : length xs + 1 = length ys + 1
⊢ Nat.succ (length xs) = Nat.succ (length ys)

State before:
case x
α : Type u_1
β : Type u_2
x : α
xs : List α
y : β
ys : List β
h : length xs + 1 = length ys + 1
⊢ Nat.succ (length xs) = Nat.succ (length ys)
Tactic:
apply h
State after:
no goals