internlm/Lean-Github huggingface dataset:
Theorem: Fin.foldl_eq_foldl_ofFn
Proof state before:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
ih :
  ∀ (init : α) (i : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
init : α
i : ℕ
h : i + (j + 1) = n
this : i < n
init' : α
⊢ foldl.loop n f init' (i + 1) = List.foldl f init' (List.ofFn fun i_1 => ⟨i + (↑i_1 + 1), ⋯⟩)
Tactic:
have : (i+1) + j = n := by omega
Proof state after:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
ih :
  ∀ (init : α) (i : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
init : α
i : ℕ
h : i + (j + 1) = n
this✝ : i < n
init' : α
this : i + 1 + j = n
⊢ foldl.loop n f init' (i + 1) = List.foldl f init' (List.ofFn fun i_1 => ⟨i + (↑i_1 + 1), ⋯⟩)
Theorem: Fin.foldl_eq_foldl_ofFn
Proof state before:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
ih :
  ∀ (init : α) (i : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
init : α
i : ℕ
h : i + (j + 1) = n
this✝ : i < n
init' : α
this : i + 1 + j = n
⊢ foldl.loop n f init' (i + 1) = List.foldl f init' (List.ofFn fun i_1 => ⟨i + (↑i_1 + 1), ⋯⟩)
Tactic:
specialize ih init' (i+1) this
Proof state after:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
init : α
i : ℕ
h : i + (j + 1) = n
this✝ : i < n
init' : α
this : i + 1 + j = n
ih : foldl.loop n f init' (i + 1) = List.foldl f init' (List.ofFn fun x => cast this (natAdd (i + 1) x))
⊢ foldl.loop n f init' (i + 1) = List.foldl f init' (List.ofFn fun i_1 => ⟨i + (↑i_1 + 1), ⋯⟩)
Theorem: Fin.foldl_eq_foldl_ofFn
Proof state before:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
init : α
i : ℕ
h : i + (j + 1) = n
this✝ : i < n
init' : α
this : i + 1 + j = n
ih : foldl.loop n f init' (i + 1) = List.foldl f init' (List.ofFn fun x => cast this (natAdd (i + 1) x))
⊢ foldl.loop n f init' (i + 1) = List.foldl f init' (List.ofFn fun i_1 => ⟨i + (↑i_1 + 1), ⋯⟩)
Tactic:
rw [ih]
Proof state after:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
init : α
i : ℕ
h : i + (j + 1) = n
this✝ : i < n
init' : α
this : i + 1 + j = n
ih : foldl.loop n f init' (i + 1) = List.foldl f init' (List.ofFn fun x => cast this (natAdd (i + 1) x))
⊢ List.foldl f init' (List.ofFn fun x => cast this (natAdd (i + 1) x)) =
    List.foldl f init' (List.ofFn fun i_1 => ⟨i + (↑i_1 + 1), ⋯⟩)
Theorem: Fin.foldl_eq_foldl_ofFn
Proof state before:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
init : α
i : ℕ
h : i + (j + 1) = n
this✝ : i < n
init' : α
this : i + 1 + j = n
ih : foldl.loop n f init' (i + 1) = List.foldl f init' (List.ofFn fun x => cast this (natAdd (i + 1) x))
⊢ List.foldl f init' (List.ofFn fun x => cast this (natAdd (i + 1) x)) =
    List.foldl f init' (List.ofFn fun i_1 => ⟨i + (↑i_1 + 1), ⋯⟩)
Tactic:
clear ih
Proof state after:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
init : α
i : ℕ
h : i + (j + 1) = n
this✝ : i < n
init' : α
this : i + 1 + j = n
⊢ List.foldl f init' (List.ofFn fun x => cast this (natAdd (i + 1) x)) =
    List.foldl f init' (List.ofFn fun i_1 => ⟨i + (↑i_1 + 1), ⋯⟩)
Theorem: Fin.foldl_eq_foldl_ofFn
Proof state before:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
init : α
i : ℕ
h : i + (j + 1) = n
this✝ : i < n
init' : α
this : i + 1 + j = n
⊢ List.foldl f init' (List.ofFn fun x => cast this (natAdd (i + 1) x)) =
    List.foldl f init' (List.ofFn fun i_1 => ⟨i + (↑i_1 + 1), ⋯⟩)
Tactic:
congr
Proof state after:
case succ.e_a.e_f
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
init : α
i : ℕ
h : i + (j + 1) = n
this✝ : i < n
init' : α
this : i + 1 + j = n
⊢ (fun x => cast this (natAdd (i + 1) x)) = fun i_1 => ⟨i + (↑i_1 + 1), ⋯⟩
Theorem: Fin.foldl_eq_foldl_ofFn
Proof state before:
case succ.e_a.e_f
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
init : α
i : ℕ
h : i + (j + 1) = n
this✝ : i < n
init' : α
this : i + 1 + j = n
⊢ (fun x => cast this (natAdd (i + 1) x)) = fun i_1 => ⟨i + (↑i_1 + 1), ⋯⟩
Tactic:
funext ⟨x,hx⟩
Proof state after:
case succ.e_a.e_f.h
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
init : α
i : ℕ
h : i + (j + 1) = n
this✝ : i < n
init' : α
this : i + 1 + j = n
x : ℕ
hx : x < j
⊢ cast this (natAdd (i + 1) ⟨x, hx⟩) = ⟨i + (↑⟨x, hx⟩ + 1), ⋯⟩
Theorem: Fin.foldl_eq_foldl_ofFn
Proof state before:
case succ.e_a.e_f.h
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
init : α
i : ℕ
h : i + (j + 1) = n
this✝ : i < n
init' : α
this : i + 1 + j = n
x : ℕ
hx : x < j
⊢ cast this (natAdd (i + 1) ⟨x, hx⟩) = ⟨i + (↑⟨x, hx⟩ + 1), ⋯⟩
Tactic:
simp
Proof state after:
case succ.e_a.e_f.h
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
init : α
i : ℕ
h : i + (j + 1) = n
this✝ : i < n
init' : α
this : i + 1 + j = n
x : ℕ
hx : x < j
⊢ i + 1 + x = i + (x + 1)
Theorem: Fin.foldl_eq_foldl_ofFn
Proof state before:
case succ.e_a.e_f.h
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
init : α
i : ℕ
h : i + (j + 1) = n
this✝ : i < n
init' : α
this : i + 1 + j = n
x : ℕ
hx : x < j
⊢ i + 1 + x = i + (x + 1)
Tactic:
omega
Proof state after:
no goals
Theorem: Fin.foldl_eq_foldl_ofFn
Proof state before:
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
ih :
  ∀ (init : α) (i : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
init : α
i : ℕ
h : i + (j + 1) = n
⊢ i < n
Tactic:
omega
Proof state after:
no goals
Theorem: Fin.foldl_eq_foldl_ofFn
Proof state before:
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
ih :
  ∀ (init : α) (i : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
init : α
i : ℕ
h : i + (j + 1) = n
this : i < n
init' : α
⊢ i + 1 + j = n
Tactic:
omega
Proof state after:
no goals
Theorem: Fin.pair_left_pair
Proof state before:
m n : ℕ
x : Fin m
y : Fin n
⊢ (x.pair y).pair_left = x
Tactic:
rcases x with ⟨x,hx⟩
Proof state after:
case mk
m n : ℕ
y : Fin n
x : ℕ
hx : x < m
⊢ (⟨x, hx⟩.pair y).pair_left = ⟨x, hx⟩
Theorem: Fin.pair_left_pair
Proof state before:
case mk
m n : ℕ
y : Fin n
x : ℕ
hx : x < m
⊢ (⟨x, hx⟩.pair y).pair_left = ⟨x, hx⟩
Tactic:
rcases y with ⟨y,hy⟩
Proof state after:
case mk.mk
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
⊢ (⟨x, hx⟩.pair ⟨y, hy⟩).pair_left = ⟨x, hx⟩
Theorem: Fin.pair_left_pair
Proof state before:
case mk.mk
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
⊢ (⟨x, hx⟩.pair ⟨y, hy⟩).pair_left = ⟨x, hx⟩
Tactic:
simp [pair_left, pair]
Proof state after:
case mk.mk
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
⊢ (x * n + y) / n = x
Theorem: Fin.pair_left_pair
Proof state before:
case mk.mk
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
⊢ (x * n + y) / n = x
Tactic:
have : n > 0 := by by_contra; simp_all
Proof state after:
case mk.mk
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
this : n > 0
⊢ (x * n + y) / n = x
Theorem: Fin.pair_left_pair
Proof state before:
case mk.mk
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
this : n > 0
⊢ (x * n + y) / n = x
Tactic:
rw [Nat.mul_comm, Nat.mul_add_div this, (Nat.div_eq_zero_iff this).mpr hy]
Proof state after:
case mk.mk
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
this : n > 0
⊢ x + 0 = x
Theorem: Fin.pair_left_pair
Proof state before:
case mk.mk
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
this : n > 0
⊢ x + 0 = x
Tactic:
simp
Proof state after:
no goals
Theorem: Fin.pair_left_pair
Proof state before:
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
⊢ n > 0
Tactic:
by_contra
Proof state after:
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
x✝ : ¬n > 0
⊢ False
Theorem: Fin.pair_left_pair
Proof state before:
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
x✝ : ¬n > 0
⊢ False
Tactic:
simp_all
Proof state after:
no goals
Theorem: Fin.pair_right_pair
Proof state before:
m n : ℕ
x : Fin m
y : Fin n
⊢ (x.pair y).pair_right = y
Tactic:
rcases x with ⟨x,hx⟩
Proof state after:
case mk
m n : ℕ
y : Fin n
x : ℕ
hx : x < m
⊢ (⟨x, hx⟩.pair y).pair_right = y
Theorem: Fin.pair_right_pair
Proof state before:
case mk
m n : ℕ
y : Fin n
x : ℕ
hx : x < m
⊢ (⟨x, hx⟩.pair y).pair_right = y
Tactic:
rcases y with ⟨y,hy⟩
Proof state after:
case mk.mk
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
⊢ (⟨x, hx⟩.pair ⟨y, hy⟩).pair_right = ⟨y, hy⟩
Theorem: Fin.pair_right_pair
Proof state before:
case mk.mk
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
⊢ (⟨x, hx⟩.pair ⟨y, hy⟩).pair_right = ⟨y, hy⟩
Tactic:
simp [pair_right, pair]
Proof state after:
case mk.mk
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
⊢ (x * n + y) % n = y
Theorem: Fin.pair_right_pair
Proof state before:
case mk.mk
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
⊢ (x * n + y) % n = y
Tactic:
have : n > 0 := by by_contra; simp_all
Proof state after:
case mk.mk
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
this : n > 0
⊢ (x * n + y) % n = y
Theorem: Fin.pair_right_pair
Proof state before:
case mk.mk
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
this : n > 0
⊢ (x * n + y) % n = y
Tactic:
rw [Nat.mul_comm, Nat.mul_add_mod _ _ _]
Proof state after:
case mk.mk
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
this : n > 0
⊢ y % n = y
Theorem: Fin.pair_right_pair
Proof state before:
case mk.mk
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
this : n > 0
⊢ y % n = y
Tactic:
apply Nat.mod_eq_of_lt hy
Proof state after:
no goals
Theorem: Fin.pair_right_pair
Proof state before:
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
⊢ n > 0
Tactic:
by_contra
Proof state after:
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
x✝ : ¬n > 0
⊢ False
Theorem: Fin.pair_right_pair
Proof state before:
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
x✝ : ¬n > 0
⊢ False
Tactic:
simp_all
Proof state after:
no goals
Theorem: Fin.pair_left_right
Proof state before:
m n : ℕ
p : Fin (m * n)
⊢ p.pair_left.pair p.pair_right = p
Tactic:
rcases p with ⟨p,hp⟩
Proof state after:
case mk
m n p : ℕ
hp : p < m * n
⊢ ⟨p, hp⟩.pair_left.pair ⟨p, hp⟩.pair_right = ⟨p, hp⟩
Theorem: Fin.pair_left_right
Proof state before:
case mk
m n p : ℕ
hp : p < m * n
⊢ ⟨p, hp⟩.pair_left.pair ⟨p, hp⟩.pair_right = ⟨p, hp⟩
Tactic:
simp [pair, pair_left, pair_right]
Proof state after:
case mk
m n p : ℕ
hp : p < m * n
⊢ p / n * n + p % n = p
Theorem: Fin.pair_left_right
Proof state before:
case mk
m n p : ℕ
hp : p < m * n
⊢ p / n * n + p % n = p
Tactic:
exact Nat.div_add_mod' p n
Proof state after:
no goals
Theorem: Fin.pair_succ_left
Proof state before:
m n : ℕ
x : Fin m
y : Fin n
⊢ ↑(x.succ.pair y) = ↑(x.pair y) + n
Tactic:
simp [pair, Nat.add_mul]
Proof state after:
m n : ℕ
x : Fin m
y : Fin n
⊢ ↑x * n + n + ↑y = ↑x * n + ↑y + n
Theorem: Fin.pair_succ_left
Proof state before:
m n : ℕ
x : Fin m
y : Fin n
⊢ ↑x * n + n + ↑y = ↑x * n + ↑y + n
Tactic:
ring
Proof state after:
no goals
Theorem: Fin.pair_ge_left
Proof state before:
m n : ℕ
x : Fin m
y : Fin n
⊢ ↑(x.pair y) ≥ ↑x * n
Tactic:
simp [pair]
Proof state after:
no goals
Theorem: List.get_product_fin_pair
Proof 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
Proof 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)
Theorem: List.get_product_fin_pair
Proof 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
Proof state after:
no goals
Theorem: List.get_product_fin_pair
Proof 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
Proof 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)
Theorem: List.get_product_fin_pair
Proof 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
Proof 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)
Theorem: List.get_product_fin_pair
Proof 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
Proof state after:
no goals
Theorem: List.get_product_fin_pair
Proof 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,_⟩
Proof 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)
Theorem: List.get_product_fin_pair
Proof 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
Proof 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)
Theorem: List.get_product_fin_pair
Proof 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
Proof 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)
Theorem: List.get_product_fin_pair
Proof 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
Proof 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)
Theorem: List.get_product_fin_pair
Proof 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
Proof 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)
Theorem: List.get_product_fin_pair
Proof 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]
Proof 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
Theorem: List.get_product_fin_pair
Proof 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]
Proof state after:
no goals
Theorem: List.get_product_fin_pair
Proof 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
Proof 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
Theorem: List.get_product_fin_pair
Proof 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
Proof state after:
no goals
Theorem: List.get_product_fin_pair
Proof 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]
Proof 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
Theorem: List.get_product_fin_pair
Proof 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
Proof state after:
no goals
Theorem: List.get_product_fin_pair
Proof 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]
Proof state after:
no goals
Theorem: List.get_product_fin_pair
Proof 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
Proof 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)