Theorem: List.get_product_eq_get_pair (LeanColls/MathlibUpstream.lean)

State before:
α : Type ?u.58035
β : Type ?u.58037
L1 : List α
L2 : List β
i : Fin (L1.product L2).length
⊢ (L1.product L2).length = L1.length * ?m.58072
Tactic:
apply List.length_product
State after:
no goals

State before:
α : Type ?u.58035
β : Type ?u.58037
L1 : List α
L2 : List β
i : Fin (L1.product L2).length
⊢ (L1.product L2).length = ?m.58083 * L2.length
Tactic:
apply List.length_product
State after:
no goals

State before:
α : Type u_1
β : Type u_2
L1 : List α
L2 : List β
i : Fin (L1.product L2).length
⊢ (L1 ×ˢ L2).get i = (L1.get (Fin.cast ⋯ i).pair_left, L2.get (Fin.cast ⋯ i).pair_right)
Tactic:
generalize hleft : Fin.pair_left _ = left
State after:
α : Type u_1
β : Type u_2
L1 : List α
L2 : List β
i : Fin (L1.product L2).length
left : Fin L1.length
hleft : (Fin.cast ⋯ i).pair_left = left
⊢ (L1 ×ˢ L2).get i = (L1.get left, L2.get (Fin.cast ⋯ i).pair_right)

State before:
α : Type u_1
β : Type u_2
L1 : List α
L2 : List β
i : Fin (L1.product L2).length
left : Fin L1.length
hleft : (Fin.cast ⋯ i).pair_left = left
⊢ (L1 ×ˢ L2).get i = (L1.get left, L2.get (Fin.cast ⋯ i).pair_right)
Tactic:
generalize hright : Fin.pair_right _ = right
State after:
α : Type u_1
β : Type u_2
L1 : List α
L2 : List β
i : Fin (L1.product L2).length
left : Fin L1.length
hleft : (Fin.cast ⋯ i).pair_left = left
right : Fin L2.length
hright : (Fin.cast ⋯ i).pair_right = right
⊢ (L1 ×ˢ L2).get i = (L1.get left, L2.get right)

State before:
α : Type u_1
β : Type u_2
L1 : List α
L2 : List β
i : Fin (L1.product L2).length
left : Fin L1.length
hleft : (Fin.cast ⋯ i).pair_left = left
right : Fin L2.length
hright : (Fin.cast ⋯ i).pair_right = right
⊢ (L1 ×ˢ L2).get i = (L1.get left, L2.get right)
Tactic:
have : i = (Fin.pair left right).cast (by apply (List.length_product ..).symm) := by
  simp [← hleft, ← hright]
State after:
α : Type u_1
β : Type u_2
L1 : List α
L2 : List β
i : Fin (L1.product L2).length
left : Fin L1.length
hleft : (Fin.cast ⋯ i).pair_left = left
right : Fin L2.length
hright : (Fin.cast ⋯ i).pair_right = right
this : i = Fin.cast ⋯ (left.pair right)
⊢ (L1 ×ˢ L2).get i = (L1.get left, L2.get right)

State before:
α : Type u_1
β : Type u_2
L1 : List α
L2 : List β
i : Fin (L1.product L2).length
left : Fin L1.length
hleft : (Fin.cast ⋯ i).pair_left = left
right : Fin L2.length
hright : (Fin.cast ⋯ i).pair_right = right
this : i = Fin.cast ⋯ (left.pair right)
⊢ (L1 ×ˢ L2).get i = (L1.get left, L2.get right)
Tactic:
clear hleft hright
State after:
α : Type u_1
β : Type u_2
L1 : List α
L2 : List β
i : Fin (L1.product L2).length
left : Fin L1.length
right : Fin L2.length
this : i = Fin.cast ⋯ (left.pair right)
⊢ (L1 ×ˢ L2).get i = (L1.get left, L2.get right)

State before:
α : Type u_1
β : Type u_2
L1 : List α
L2 : List β
i : Fin (L1.product L2).length
left : Fin L1.length
right : Fin L2.length
this : i = Fin.cast ⋯ (left.pair right)
⊢ (L1 ×ˢ L2).get i = (L1.get left, L2.get right)
Tactic:
subst i
State after:
α : Type u_1
β : Type u_2
L1 : List α
L2 : List β
left : Fin L1.length
right : Fin L2.length
⊢ (L1 ×ˢ L2).get (Fin.cast ⋯ (left.pair right)) = (L1.get left, L2.get right)

State before:
α : Type u_1
β : Type u_2
L1 : List α
L2 : List β
left : Fin L1.length
right : Fin L2.length
⊢ (L1 ×ˢ L2).get (Fin.cast ⋯ (left.pair right)) = (L1.get left, L2.get right)
Tactic:
rw [List.get_product_fin_pair]
State after:
case hp
α : Type u_1
β : Type u_2
L1 : List α
L2 : List β
left : Fin L1.length
right : Fin L2.length
⊢ ↑(Fin.cast ⋯ (left.pair right)) = ↑(left.pair right)

State before:
case hp
α : Type u_1
β : Type u_2
L1 : List α
L2 : List β
left : Fin L1.length
right : Fin L2.length
⊢ ↑(Fin.cast ⋯ (left.pair right)) = ↑(left.pair right)
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
β : Type u_2
L1 : List α
L2 : List β
i : Fin (L1.product L2).length
left : Fin L1.length
hleft : (Fin.cast ⋯ i).pair_left = left
right : Fin L2.length
hright : (Fin.cast ⋯ i).pair_right = right
⊢ L1.length * L2.length = (L1.product L2).length
Tactic:
apply (List.length_product ..).symm
State after:
no goals

State before:
α : Type u_1
β : Type u_2
L1 : List α
L2 : List β
i : Fin (L1.product L2).length
left : Fin L1.length
hleft : (Fin.cast ⋯ i).pair_left = left
right : Fin L2.length
hright : (Fin.cast ⋯ i).pair_right = right
⊢ i = Fin.cast ⋯ (left.pair right)
Tactic:
simp [← hleft, ← hright]
State after:
no goals