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

State before:
α : Type u_1
β : Type u_2
L1 : List α
L2 : List β
i : Fin L1.length
j : Fin L2.length
p : Fin (L1 ×ˢ L2).length
hp : ↑p = ↑(i.pair j)
⊢ (L1 ×ˢ L2).get p = (L1.get i, L2.get j)
Tactic:
generalize hLL : L1 ×ˢ L2 = LL at p
State after:
α : Type u_1
β : Type u_2
L1 : List α
L2 : List β
i : Fin L1.length
j : Fin L2.length
LL : List (α × β)
hLL : L1 ×ˢ L2 = LL
p : Fin LL.length
hp : ↑p = ↑(i.pair j)
⊢ LL.get p = (L1.get i, L2.get j)

State before:
case nil
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
i : Fin [].length
LL : List (α × β)
hLL : [] ×ˢ L2 = LL
p : Fin LL.length
hp : ↑p = ↑(i.pair j)
⊢ LL.get p = ([].get i, L2.get j)
Tactic:
exact i.elim0
State after:
no goals

State before:
case cons
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
ih :
  ∀ {i : Fin tl.length} (LL : List (α × β)),
    tl ×ˢ L2 = LL → ∀ {p : Fin LL.length}, ↑p = ↑(i.pair j) → LL.get p = (tl.get i, L2.get j)
i : Fin (hd :: tl).length
LL : List (α × β)
hLL : (hd :: tl) ×ˢ L2 = LL
p : Fin LL.length
hp : ↑p = ↑(i.pair j)
⊢ LL.get p = ((hd :: tl).get i, L2.get j)
Tactic:
dsimp at i
State after:
case cons
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
ih :
  ∀ {i : Fin tl.length} (LL : List (α × β)),
    tl ×ˢ L2 = LL → ∀ {p : Fin LL.length}, ↑p = ↑(i.pair j) → LL.get p = (tl.get i, L2.get j)
i : Fin (tl.length + 1)
LL : List (α × β)
hLL : (hd :: tl) ×ˢ L2 = LL
p : Fin LL.length
hp : ↑p = ↑(i.pair j)
⊢ LL.get p = ((hd :: tl).get i, L2.get j)

State before:
case cons
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
ih :
  ∀ {i : Fin tl.length} (LL : List (α × β)),
    tl ×ˢ L2 = LL → ∀ {p : Fin LL.length}, ↑p = ↑(i.pair j) → LL.get p = (tl.get i, L2.get j)
i : Fin (tl.length + 1)
LL : List (α × β)
hLL : (hd :: tl) ×ˢ L2 = LL
p : Fin LL.length
hp : ↑p = ↑(i.pair j)
⊢ LL.get p = ((hd :: tl).get i, L2.get j)
Tactic:
induction i using Fin.cases
State after:
case cons.zero
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
ih :
  ∀ {i : Fin tl.length} (LL : List (α × β)),
    tl ×ˢ L2 = LL → ∀ {p : Fin LL.length}, ↑p = ↑(i.pair j) → LL.get p = (tl.get i, L2.get j)
LL : List (α × β)
hLL : (hd :: tl) ×ˢ L2 = LL
p : Fin LL.length
hp : ↑p = ↑(Fin.pair 0 j)
⊢ LL.get p = ((hd :: tl).get 0, L2.get j)

case cons.succ
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
ih :
  ∀ {i : Fin tl.length} (LL : List (α × β)),
    tl ×ˢ L2 = LL → ∀ {p : Fin LL.length}, ↑p = ↑(i.pair j) → LL.get p = (tl.get i, L2.get j)
LL : List (α × β)
hLL : (hd :: tl) ×ˢ L2 = LL
p : Fin LL.length
i✝ : Fin tl.length
hp : ↑p = ↑(i✝.succ.pair j)
⊢ LL.get p = ((hd :: tl).get i✝.succ, L2.get j)

State before:
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
ih :
  ∀ {i : Fin tl.length} (LL : List (α × β)),
    tl ×ˢ L2 = LL → ∀ {p : Fin LL.length}, ↑p = ↑(i.pair j) → LL.get p = (tl.get i, L2.get j)
LL : List (α × β)
hLL : (hd :: tl) ×ˢ L2 = LL
p : Fin LL.length
hp : ↑p = ↑(Fin.pair 0 j)
⊢ LL.get p = ((hd :: tl).get 0, L2.get j)
Tactic:
case zero =>
  rcases p with ⟨p,_⟩
  simp [Fin.pair] at hp
  have : p < L2.length := by rw [hp]; exact j.isLt
  simp [product_cons] at hLL
  subst LL
  rw [get_append_left]
  case h => simp [this]
  simp; congr
State after:
no goals

State before:
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
ih :
  ∀ {i : Fin tl.length} (LL : List (α × β)),
    tl ×ˢ L2 = LL → ∀ {p : Fin LL.length}, ↑p = ↑(i.pair j) → LL.get p = (tl.get i, L2.get j)
LL : List (α × β)
hLL : (hd :: tl) ×ˢ L2 = LL
p : Fin LL.length
hp : ↑p = ↑(Fin.pair 0 j)
⊢ LL.get p = ((hd :: tl).get 0, L2.get j)
Tactic:
rcases p with ⟨p,_⟩
State after:
case mk
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
ih :
  ∀ {i : Fin tl.length} (LL : List (α × β)),
    tl ×ˢ L2 = LL → ∀ {p : Fin LL.length}, ↑p = ↑(i.pair j) → LL.get p = (tl.get i, L2.get j)
LL : List (α × β)
hLL : (hd :: tl) ×ˢ L2 = LL
p : ℕ
isLt✝ : p < LL.length
hp : ↑⟨p, isLt✝⟩ = ↑(Fin.pair 0 j)
⊢ LL.get ⟨p, isLt✝⟩ = ((hd :: tl).get 0, L2.get j)

State before:
case mk
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
ih :
  ∀ {i : Fin tl.length} (LL : List (α × β)),
    tl ×ˢ L2 = LL → ∀ {p : Fin LL.length}, ↑p = ↑(i.pair j) → LL.get p = (tl.get i, L2.get j)
LL : List (α × β)
hLL : (hd :: tl) ×ˢ L2 = LL
p : ℕ
isLt✝ : p < LL.length
hp : ↑⟨p, isLt✝⟩ = ↑(Fin.pair 0 j)
⊢ LL.get ⟨p, isLt✝⟩ = ((hd :: tl).get 0, L2.get j)
Tactic:
simp [Fin.pair] at hp
State after:
case mk
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
ih :
  ∀ {i : Fin tl.length} (LL : List (α × β)),
    tl ×ˢ L2 = LL → ∀ {p : Fin LL.length}, ↑p = ↑(i.pair j) → LL.get p = (tl.get i, L2.get j)
LL : List (α × β)
hLL : (hd :: tl) ×ˢ L2 = LL
p : ℕ
isLt✝ : p < LL.length
hp : p = ↑j
⊢ LL.get ⟨p, isLt✝⟩ = ((hd :: tl).get 0, L2.get j)

State before:
case mk
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
ih :
  ∀ {i : Fin tl.length} (LL : List (α × β)),
    tl ×ˢ L2 = LL → ∀ {p : Fin LL.length}, ↑p = ↑(i.pair j) → LL.get p = (tl.get i, L2.get j)
LL : List (α × β)
hLL : (hd :: tl) ×ˢ L2 = LL
p : ℕ
isLt✝ : p < LL.length
hp : p = ↑j
⊢ LL.get ⟨p, isLt✝⟩ = ((hd :: tl).get 0, L2.get j)
Tactic:
have : p < L2.length := by rw [hp]; exact j.isLt
State after:
case mk
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
ih :
  ∀ {i : Fin tl.length} (LL : List (α × β)),
    tl ×ˢ L2 = LL → ∀ {p : Fin LL.length}, ↑p = ↑(i.pair j) → LL.get p = (tl.get i, L2.get j)
LL : List (α × β)
hLL : (hd :: tl) ×ˢ L2 = LL
p : ℕ
isLt✝ : p < LL.length
hp : p = ↑j
this : p < L2.length
⊢ LL.get ⟨p, isLt✝⟩ = ((hd :: tl).get 0, L2.get j)

State before:
case mk
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
ih :
  ∀ {i : Fin tl.length} (LL : List (α × β)),
    tl ×ˢ L2 = LL → ∀ {p : Fin LL.length}, ↑p = ↑(i.pair j) → LL.get p = (tl.get i, L2.get j)
LL : List (α × β)
hLL : (hd :: tl) ×ˢ L2 = LL
p : ℕ
isLt✝ : p < LL.length
hp : p = ↑j
this : p < L2.length
⊢ LL.get ⟨p, isLt✝⟩ = ((hd :: tl).get 0, L2.get j)
Tactic:
simp [product_cons] at hLL
State after:
case mk
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
ih :
  ∀ {i : Fin tl.length} (LL : List (α × β)),
    tl ×ˢ L2 = LL → ∀ {p : Fin LL.length}, ↑p = ↑(i.pair j) → LL.get p = (tl.get i, L2.get j)
LL : List (α × β)
hLL : map (fun b => (hd, b)) L2 ++ tl ×ˢ L2 = LL
p : ℕ
isLt✝ : p < LL.length
hp : p = ↑j
this : p < L2.length
⊢ LL.get ⟨p, isLt✝⟩ = ((hd :: tl).get 0, L2.get j)

State before:
case mk
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
ih :
  ∀ {i : Fin tl.length} (LL : List (α × β)),
    tl ×ˢ L2 = LL → ∀ {p : Fin LL.length}, ↑p = ↑(i.pair j) → LL.get p = (tl.get i, L2.get j)
LL : List (α × β)
hLL : map (fun b => (hd, b)) L2 ++ tl ×ˢ L2 = LL
p : ℕ
isLt✝ : p < LL.length
hp : p = ↑j
this : p < L2.length
⊢ LL.get ⟨p, isLt✝⟩ = ((hd :: tl).get 0, L2.get j)
Tactic:
subst LL
State after:
case mk
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
ih :
  ∀ {i : Fin tl.length} (LL : List (α × β)),
    tl ×ˢ L2 = LL → ∀ {p : Fin LL.length}, ↑p = ↑(i.pair j) → LL.get p = (tl.get i, L2.get j)
p : ℕ
hp : p = ↑j
this : p < L2.length
isLt✝ : p < (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).length
⊢ (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).get ⟨p, isLt✝⟩ = ((hd :: tl).get 0, L2.get j)

State before:
case mk
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
ih :
  ∀ {i : Fin tl.length} (LL : List (α × β)),
    tl ×ˢ L2 = LL → ∀ {p : Fin LL.length}, ↑p = ↑(i.pair j) → LL.get p = (tl.get i, L2.get j)
p : ℕ
hp : p = ↑j
this : p < L2.length
isLt✝ : p < (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).length
⊢ (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).get ⟨p, isLt✝⟩ = ((hd :: tl).get 0, L2.get j)
Tactic:
rw [get_append_left]
State after:
case mk
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
ih :
  ∀ {i : Fin tl.length} (LL : List (α × β)),
    tl ×ˢ L2 = LL → ∀ {p : Fin LL.length}, ↑p = ↑(i.pair j) → LL.get p = (tl.get i, L2.get j)
p : ℕ
hp : p = ↑j
this : p < L2.length
isLt✝ : p < (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).length
⊢ (map (fun b => (hd, b)) L2).get ⟨p, ?mk.h⟩ = ((hd :: tl).get 0, L2.get j)

case mk.h
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
ih :
  ∀ {i : Fin tl.length} (LL : List (α × β)),
    tl ×ˢ L2 = LL → ∀ {p : Fin LL.length}, ↑p = ↑(i.pair j) → LL.get p = (tl.get i, L2.get j)
p : ℕ
hp : p = ↑j
this : p < L2.length
isLt✝ : p < (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).length
⊢ p < (map (fun b => (hd, b)) L2).length

State before:
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
ih :
  ∀ {i : Fin tl.length} (LL : List (α × β)),
    tl ×ˢ L2 = LL → ∀ {p : Fin LL.length}, ↑p = ↑(i.pair j) → LL.get p = (tl.get i, L2.get j)
p : ℕ
hp : p = ↑j
this : p < L2.length
isLt✝ : p < (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).length
⊢ p < (map (fun b => (hd, b)) L2).length
Tactic:
case h => simp [this]
State after:
no goals

State before:
case mk
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
ih :
  ∀ {i : Fin tl.length} (LL : List (α × β)),
    tl ×ˢ L2 = LL → ∀ {p : Fin LL.length}, ↑p = ↑(i.pair j) → LL.get p = (tl.get i, L2.get j)
p : ℕ
hp : p = ↑j
this : p < L2.length
isLt✝ : p < (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).length
⊢ (map (fun b => (hd, b)) L2).get ⟨p, ⋯⟩ = ((hd :: tl).get 0, L2.get j)
Tactic:
simp
State after:
case mk
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
ih :
  ∀ {i : Fin tl.length} (LL : List (α × β)),
    tl ×ˢ L2 = LL → ∀ {p : Fin LL.length}, ↑p = ↑(i.pair j) → LL.get p = (tl.get i, L2.get j)
p : ℕ
hp : p = ↑j
this : p < L2.length
isLt✝ : p < (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).length
⊢ L2.get ⟨p, ⋯⟩ = L2.get j

State before:
case mk
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
ih :
  ∀ {i : Fin tl.length} (LL : List (α × β)),
    tl ×ˢ L2 = LL → ∀ {p : Fin LL.length}, ↑p = ↑(i.pair j) → LL.get p = (tl.get i, L2.get j)
p : ℕ
hp : p = ↑j
this : p < L2.length
isLt✝ : p < (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).length
⊢ L2.get ⟨p, ⋯⟩ = L2.get j
Tactic:
congr
State after:
no goals

State before:
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
ih :
  ∀ {i : Fin tl.length} (LL : List (α × β)),
    tl ×ˢ L2 = LL → ∀ {p : Fin LL.length}, ↑p = ↑(i.pair j) → LL.get p = (tl.get i, L2.get j)
LL : List (α × β)
hLL : (hd :: tl) ×ˢ L2 = LL
p : ℕ
isLt✝ : p < LL.length
hp : p = ↑j
⊢ p < L2.length
Tactic:
rw [hp]
State after:
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
ih :
  ∀ {i : Fin tl.length} (LL : List (α × β)),
    tl ×ˢ L2 = LL → ∀ {p : Fin LL.length}, ↑p = ↑(i.pair j) → LL.get p = (tl.get i, L2.get j)
LL : List (α × β)
hLL : (hd :: tl) ×ˢ L2 = LL
p : ℕ
isLt✝ : p < LL.length
hp : p = ↑j
⊢ ↑j < L2.length

State before:
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
ih :
  ∀ {i : Fin tl.length} (LL : List (α × β)),
    tl ×ˢ L2 = LL → ∀ {p : Fin LL.length}, ↑p = ↑(i.pair j) → LL.get p = (tl.get i, L2.get j)
LL : List (α × β)
hLL : (hd :: tl) ×ˢ L2 = LL
p : ℕ
isLt✝ : p < LL.length
hp : p = ↑j
⊢ ↑j < L2.length
Tactic:
exact j.isLt
State after:
no goals

State before:
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
ih :
  ∀ {i : Fin tl.length} (LL : List (α × β)),
    tl ×ˢ L2 = LL → ∀ {p : Fin LL.length}, ↑p = ↑(i.pair j) → LL.get p = (tl.get i, L2.get j)
p : ℕ
hp : p = ↑j
this : p < L2.length
isLt✝ : p < (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).length
⊢ p < (map (fun b => (hd, b)) L2).length
Tactic:
simp [this]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
ih :
  ∀ {i : Fin tl.length} (LL : List (α × β)),
    tl ×ˢ L2 = LL → ∀ {p : Fin LL.length}, ↑p = ↑(i.pair j) → LL.get p = (tl.get i, L2.get j)
LL : List (α × β)
hLL : (hd :: tl) ×ˢ L2 = LL
p : Fin LL.length
i : Fin tl.length
hp : ↑p = ↑(i.succ.pair j)
⊢ LL.get p = ((hd :: tl).get i.succ, L2.get j)
Tactic:
specialize @ih i (tl ×ˢ L2) rfl (Fin.pair i j |>.cast (List.length_product ..).symm) rfl
State after:
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
LL : List (α × β)
hLL : (hd :: tl) ×ˢ L2 = LL
p : Fin LL.length
i : Fin tl.length
hp : ↑p = ↑(i.succ.pair j)
ih : (tl ×ˢ L2).get (Fin.cast ⋯ (i.pair j)) = (tl.get i, L2.get j)
⊢ LL.get p = ((hd :: tl).get i.succ, L2.get j)

State before:
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
LL : List (α × β)
hLL : (hd :: tl) ×ˢ L2 = LL
p : Fin LL.length
i : Fin tl.length
hp : ↑p = ↑(i.succ.pair j)
ih : (tl ×ˢ L2).get (Fin.cast ⋯ (i.pair j)) = (tl.get i, L2.get j)
⊢ LL.get p = ((hd :: tl).get i.succ, L2.get j)
Tactic:
simp
State after:
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
LL : List (α × β)
hLL : (hd :: tl) ×ˢ L2 = LL
p : Fin LL.length
i : Fin tl.length
hp : ↑p = ↑(i.succ.pair j)
ih : (tl ×ˢ L2).get (Fin.cast ⋯ (i.pair j)) = (tl.get i, L2.get j)
⊢ LL.get p = (tl.get i, L2.get j)

State before:
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
LL : List (α × β)
hLL : (hd :: tl) ×ˢ L2 = LL
p : Fin LL.length
i : Fin tl.length
hp : ↑p = ↑(i.succ.pair j)
ih : (tl ×ˢ L2).get (Fin.cast ⋯ (i.pair j)) = (tl.get i, L2.get j)
⊢ LL.get p = (tl.get i, L2.get j)
Tactic:
rw [← ih]
State after:
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
LL : List (α × β)
hLL : (hd :: tl) ×ˢ L2 = LL
p : Fin LL.length
i : Fin tl.length
hp : ↑p = ↑(i.succ.pair j)
ih : (tl ×ˢ L2).get (Fin.cast ⋯ (i.pair j)) = (tl.get i, L2.get j)
⊢ LL.get p = (tl ×ˢ L2).get (Fin.cast ⋯ (i.pair j))

State before:
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
LL : List (α × β)
hLL : (hd :: tl) ×ˢ L2 = LL
p : Fin LL.length
i : Fin tl.length
hp : ↑p = ↑(i.succ.pair j)
ih : (tl ×ˢ L2).get (Fin.cast ⋯ (i.pair j)) = (tl.get i, L2.get j)
⊢ LL.get p = (tl ×ˢ L2).get (Fin.cast ⋯ (i.pair j))
Tactic:
clear ih
State after:
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
LL : List (α × β)
hLL : (hd :: tl) ×ˢ L2 = LL
p : Fin LL.length
i : Fin tl.length
hp : ↑p = ↑(i.succ.pair j)
⊢ LL.get p = (tl ×ˢ L2).get (Fin.cast ⋯ (i.pair j))

State before:
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
LL : List (α × β)
hLL : (hd :: tl) ×ˢ L2 = LL
p : Fin LL.length
i : Fin tl.length
hp : ↑p = ↑(i.succ.pair j)
⊢ LL.get p = (tl ×ˢ L2).get (Fin.cast ⋯ (i.pair j))
Tactic:
rcases p with ⟨p,h⟩
State after:
case mk
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
LL : List (α × β)
hLL : (hd :: tl) ×ˢ L2 = LL
i : Fin tl.length
p : ℕ
h : p < LL.length
hp : ↑⟨p, h⟩ = ↑(i.succ.pair j)
⊢ LL.get ⟨p, h⟩ = (tl ×ˢ L2).get (Fin.cast ⋯ (i.pair j))

State before:
case mk
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
LL : List (α × β)
hLL : (hd :: tl) ×ˢ L2 = LL
i : Fin tl.length
p : ℕ
h : p < LL.length
hp : ↑⟨p, h⟩ = ↑(i.succ.pair j)
⊢ LL.get ⟨p, h⟩ = (tl ×ˢ L2).get (Fin.cast ⋯ (i.pair j))
Tactic:
simp at hp hLL
State after:
case mk
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
LL : List (α × β)
hLL : map (fun b => (hd, b)) L2 ++ tl ×ˢ L2 = LL
i : Fin tl.length
p : ℕ
h : p < LL.length
hp : p = ↑(i.succ.pair j)
⊢ LL.get ⟨p, h⟩ = (tl ×ˢ L2).get (Fin.cast ⋯ (i.pair j))

State before:
case mk
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
LL : List (α × β)
hLL : map (fun b => (hd, b)) L2 ++ tl ×ˢ L2 = LL
i : Fin tl.length
p : ℕ
h : p < LL.length
hp : p = ↑(i.succ.pair j)
⊢ LL.get ⟨p, h⟩ = (tl ×ˢ L2).get (Fin.cast ⋯ (i.pair j))
Tactic:
subst p LL
State after:
case mk
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
i : Fin tl.length
h : ↑(i.succ.pair j) < (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).length
⊢ (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).get ⟨↑(i.succ.pair j), h⟩ = (tl ×ˢ L2).get (Fin.cast ⋯ (i.pair j))

State before:
case mk
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
i : Fin tl.length
h : ↑(i.succ.pair j) < (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).length
⊢ (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).get ⟨↑(i.succ.pair j), h⟩ = (tl ×ˢ L2).get (Fin.cast ⋯ (i.pair j))
Tactic:
simp [Nat.add_mul, length_product] at h ⊢
State after:
case mk
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
i : Fin tl.length
h✝ : ↑(i.succ.pair j) < (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).length
h : ↑(i.succ.pair j) < L2.length + tl.length * L2.length
⊢ (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).get ⟨↑(i.succ.pair j), h✝⟩ = (tl ×ˢ L2).get (Fin.cast ⋯ (i.pair j))

State before:
case mk
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
i : Fin tl.length
h✝ : ↑(i.succ.pair j) < (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).length
h : ↑(i.succ.pair j) < L2.length + tl.length * L2.length
⊢ (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).get ⟨↑(i.succ.pair j), h✝⟩ = (tl ×ˢ L2).get (Fin.cast ⋯ (i.pair j))
Tactic:
rw [get_append_right]
State after:
case mk
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
i : Fin tl.length
h✝ : ↑(i.succ.pair j) < (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).length
h : ↑(i.succ.pair j) < L2.length + tl.length * L2.length
⊢ (tl ×ˢ L2).get ⟨↑(i.succ.pair j) - (map (fun b => (hd, b)) L2).length, ?mk.h''⟩ =
    (tl ×ˢ L2).get (Fin.cast ⋯ (i.pair j))

case mk.h
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
i : Fin tl.length
h✝ : ↑(i.succ.pair j) < (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).length
h : ↑(i.succ.pair j) < L2.length + tl.length * L2.length
⊢ ¬↑(i.succ.pair j) < (map (fun b => (hd, b)) L2).length

case mk.h''
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
i : Fin tl.length
h✝ : ↑(i.succ.pair j) < (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).length
h : ↑(i.succ.pair j) < L2.length + tl.length * L2.length
⊢ ↑(i.succ.pair j) - (map (fun b => (hd, b)) L2).length < (tl ×ˢ L2).length

State before:
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
i : Fin tl.length
h✝ : ↑(i.succ.pair j) < (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).length
h : ↑(i.succ.pair j) < L2.length + tl.length * L2.length
⊢ ↑(i.succ.pair j) - (map (fun b => (hd, b)) L2).length < (tl ×ˢ L2).length
Tactic:
case h'' =>
  simp [length_product, Fin.pair_succ_left]
State after:
no goals

State before:
case mk
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
i : Fin tl.length
h✝ : ↑(i.succ.pair j) < (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).length
h : ↑(i.succ.pair j) < L2.length + tl.length * L2.length
⊢ (tl ×ˢ L2).get ⟨↑(i.succ.pair j) - (map (fun b => (hd, b)) L2).length, ⋯⟩ = (tl ×ˢ L2).get (Fin.cast ⋯ (i.pair j))
Tactic:
congr
State after:
case mk.e_a.e_val
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
i : Fin tl.length
h✝ : ↑(i.succ.pair j) < (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).length
h : ↑(i.succ.pair j) < L2.length + tl.length * L2.length
⊢ ↑(i.succ.pair j) - (map (fun b => (hd, b)) L2).length = ↑(i.pair j)

State before:
case mk.e_a.e_val
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
i : Fin tl.length
h✝ : ↑(i.succ.pair j) < (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).length
h : ↑(i.succ.pair j) < L2.length + tl.length * L2.length
⊢ ↑(i.succ.pair j) - (map (fun b => (hd, b)) L2).length = ↑(i.pair j)
Tactic:
simp [Fin.pair_succ_left]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
i : Fin tl.length
h✝ : ↑(i.succ.pair j) < (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).length
h : ↑(i.succ.pair j) < L2.length + tl.length * L2.length
⊢ ¬↑(i.succ.pair j) < (map (fun b => (hd, b)) L2).length
Tactic:
simp
State after:
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
i : Fin tl.length
h✝ : ↑(i.succ.pair j) < (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).length
h : ↑(i.succ.pair j) < L2.length + tl.length * L2.length
⊢ L2.length ≤ ↑(i.succ.pair j)

State before:
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
i : Fin tl.length
h✝ : ↑(i.succ.pair j) < (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).length
h : ↑(i.succ.pair j) < L2.length + tl.length * L2.length
⊢ L2.length ≤ ↑(i.succ.pair j)
Tactic:
trans i.succ * L2.length
State after:
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
i : Fin tl.length
h✝ : ↑(i.succ.pair j) < (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).length
h : ↑(i.succ.pair j) < L2.length + tl.length * L2.length
⊢ L2.length ≤ ↑i.succ * L2.length

α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
i : Fin tl.length
h✝ : ↑(i.succ.pair j) < (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).length
h : ↑(i.succ.pair j) < L2.length + tl.length * L2.length
⊢ ↑i.succ * L2.length ≤ ↑(i.succ.pair j)

State before:
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
i : Fin tl.length
h✝ : ↑(i.succ.pair j) < (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).length
h : ↑(i.succ.pair j) < L2.length + tl.length * L2.length
⊢ L2.length ≤ ↑i.succ * L2.length
Tactic:
simp [Nat.add_mul]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
i : Fin tl.length
h✝ : ↑(i.succ.pair j) < (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).length
h : ↑(i.succ.pair j) < L2.length + tl.length * L2.length
⊢ ↑i.succ * L2.length ≤ ↑(i.succ.pair j)
Tactic:
apply Fin.pair_ge_left
State after:
no goals

State before:
α : Type u_1
β : Type u_2
L2 : List β
j : Fin L2.length
hd : α
tl : List α
i : Fin tl.length
h✝ : ↑(i.succ.pair j) < (map (fun b => (hd, b)) L2 ++ tl ×ˢ L2).length
h : ↑(i.succ.pair j) < L2.length + tl.length * L2.length
⊢ ↑(i.succ.pair j) - (map (fun b => (hd, b)) L2).length < (tl ×ˢ L2).length
Tactic:
simp [length_product, Fin.pair_succ_left]
State after:
no goals