internlm/Lean-Github huggingface dataset:
Theorem: List.get_product_fin_pair
Proof 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
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 = (tl.get i, 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 α
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]
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 = (tl ×ˢ L2).get (Fin.cast ⋯ (i.pair 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 α
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
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)
⊢ LL.get p = (tl ×ˢ L2).get (Fin.cast ⋯ (i.pair 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 α
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⟩
Proof 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))
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 α
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
Proof 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))
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 α
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
Proof 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))
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 α
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 ⊢
Proof 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))
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 α
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]
Proof 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
Theorem: List.get_product_fin_pair
Proof 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]
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 α
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
Proof 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)
Theorem: List.get_product_fin_pair
Proof 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]
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 α
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
Proof 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)
Theorem: List.get_product_fin_pair
Proof 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
Proof 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)
Theorem: List.get_product_fin_pair
Proof 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]
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 α
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
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 α
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]
Proof state after:
no goals
Theorem: List.get_product_eq_get_pair
Proof 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
Proof state after:
no goals
Theorem: List.get_product_eq_get_pair
Proof 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
Proof state after:
no goals
Theorem: List.get_product_eq_get_pair
Proof 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
Proof 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)
Theorem: List.get_product_eq_get_pair
Proof 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
Proof 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)
Theorem: List.get_product_eq_get_pair
Proof 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]
Proof 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)
Theorem: List.get_product_eq_get_pair
Proof 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
Proof 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)
Theorem: List.get_product_eq_get_pair
Proof 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
Proof 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)
Theorem: List.get_product_eq_get_pair
Proof 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]
Proof 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)
Theorem: List.get_product_eq_get_pair
Proof 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
Proof state after:
no goals
Theorem: List.get_product_eq_get_pair
Proof 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
Proof state after:
no goals
Theorem: List.get_product_eq_get_pair
Proof 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]
Proof state after:
no goals
Theorem: List.foldl_product
Proof state before:
γ : Type u_1
α : Type u_2
β : Type u_3
L1 : List α
L2 : List β
f : γ → α × β → γ
init : γ
⊢ foldl f init (L1 ×ˢ L2) = foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) init L1
Tactic:
induction L1 generalizing init <;> simp
Proof state after:
case cons
γ : Type u_1
α : Type u_2
β : Type u_3
L2 : List β
f : γ → α × β → γ
head✝ : α
tail✝ : List α
tail_ih✝ :
  ∀ (init : γ), foldl f init (tail✝ ×ˢ L2) = foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) init tail✝
init : γ
⊢ foldl f (foldl f init (map (fun b => (head✝, b)) L2)) (tail✝ ×ˢ L2) =
    foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) (foldl (fun acc b => f acc (head✝, b)) init L2) tail✝
Theorem: List.foldl_product
Proof state before:
γ : Type u_1
α : Type u_2
β : Type u_3
L2 : List β
f : γ → α × β → γ
hd : α
tl : List α
ih : ∀ (init : γ), foldl f init (tl ×ˢ L2) = foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) init tl
init : γ
⊢ foldl f (foldl f init (map (fun b => (hd, b)) L2)) (tl ×ˢ L2) =
    foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) (foldl (fun acc b => f acc (hd, b)) init L2) tl
Tactic:
case cons hd tl ih =>
rw [ih]; simp [foldl_map]
Proof state after:
no goals
Theorem: List.foldl_product
Proof state before:
γ : Type u_1
α : Type u_2
β : Type u_3
L2 : List β
f : γ → α × β → γ
hd : α
tl : List α
ih : ∀ (init : γ), foldl f init (tl ×ˢ L2) = foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) init tl
init : γ
⊢ foldl f (foldl f init (map (fun b => (hd, b)) L2)) (tl ×ˢ L2) =
    foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) (foldl (fun acc b => f acc (hd, b)) init L2) tl
Tactic:
rw [ih]
Proof state after:
γ : Type u_1
α : Type u_2
β : Type u_3
L2 : List β
f : γ → α × β → γ
hd : α
tl : List α
ih : ∀ (init : γ), foldl f init (tl ×ˢ L2) = foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) init tl
init : γ
⊢ foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) (foldl f init (map (fun b => (hd, b)) L2)) tl =
    foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) (foldl (fun acc b => f acc (hd, b)) init L2) tl
Theorem: List.foldl_product
Proof state before:
γ : Type u_1
α : Type u_2
β : Type u_3
L2 : List β
f : γ → α × β → γ
hd : α
tl : List α
ih : ∀ (init : γ), foldl f init (tl ×ˢ L2) = foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) init tl
init : γ
⊢ foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) (foldl f init (map (fun b => (hd, b)) L2)) tl =
    foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) (foldl (fun acc b => f acc (hd, b)) init L2) tl
Tactic:
simp [foldl_map]
Proof state after:
no goals
Theorem: LeanColls.Insert.toList_empty
Proof state before:
C : Type u
τ : outParam (Type v)
inst✝⁴ : Insert C τ
inst✝³ : Membership τ C
inst✝² : Mem C τ
inst✝¹ : ToList C τ
inst✝ : Mem.ToList C τ
⊢ toList empty = []
Tactic:
rw [List.eq_nil_iff_forall_not_mem]
Proof state after:
C : Type u
τ : outParam (Type v)
inst✝⁴ : Insert C τ
inst✝³ : Membership τ C
inst✝² : Mem C τ
inst✝¹ : ToList C τ
inst✝ : Mem.ToList C τ
⊢ ∀ (a : τ), a ∉ toList empty
Theorem: LeanColls.Insert.toList_empty
Proof state before:
C : Type u
τ : outParam (Type v)
inst✝⁴ : Insert C τ
inst✝³ : Membership τ C
inst✝² : Mem C τ
inst✝¹ : ToList C τ
inst✝ : Mem.ToList C τ
⊢ ∀ (a : τ), a ∉ toList empty
Tactic:
intro x
Proof state after:
C : Type u
τ : outParam (Type v)
inst✝⁴ : Insert C τ
inst✝³ : Membership τ C
inst✝² : Mem C τ
inst✝¹ : ToList C τ
inst✝ : Mem.ToList C τ
x : τ
⊢ x ∉ toList empty
Theorem: LeanColls.Insert.toList_empty
Proof state before:
C : Type u
τ : outParam (Type v)
inst✝⁴ : Insert C τ
inst✝³ : Membership τ C
inst✝² : Mem C τ
inst✝¹ : ToList C τ
inst✝ : Mem.ToList C τ
x : τ
⊢ x ∉ toList empty
Tactic:
rw [← Mem.ToList.mem_iff_mem_toList]
Proof state after:
C : Type u
τ : outParam (Type v)
inst✝⁴ : Insert C τ
inst✝³ : Membership τ C
inst✝² : Mem C τ
inst✝¹ : ToList C τ
inst✝ : Mem.ToList C τ
x : τ
⊢ x ∉ empty
Theorem: LeanColls.Insert.toList_empty
Proof state before:
C : Type u
τ : outParam (Type v)
inst✝⁴ : Insert C τ
inst✝³ : Membership τ C
inst✝² : Mem C τ
inst✝¹ : ToList C τ
inst✝ : Mem.ToList C τ
x : τ
⊢ x ∉ empty
Tactic:
apply Mem.mem_empty
Proof state after:
no goals
Theorem: LeanColls.Insert.toList_singleton
Proof state before:
C : Type u
τ : outParam (Type v)
inst✝⁴ : Insert C τ
x : τ
inst✝³ : ToList C τ
inst✝² : LeanColls.ToMultiset C τ
inst✝¹ : LawfulToList C τ
inst✝ : ToMultiset C τ
⊢ toList (singleton x) = [x]
Tactic:
apply Multiset.coe_eq_singleton.mp
Proof state after:
C : Type u
τ : outParam (Type v)
inst✝⁴ : Insert C τ
x : τ
inst✝³ : ToList C τ
inst✝² : LeanColls.ToMultiset C τ
inst✝¹ : LawfulToList C τ
inst✝ : ToMultiset C τ
⊢ ↑(toList (singleton x)) = {x}
Theorem: LeanColls.Insert.toList_singleton
Proof state before:
C : Type u
τ : outParam (Type v)
inst✝⁴ : Insert C τ
x : τ
inst✝³ : ToList C τ
inst✝² : LeanColls.ToMultiset C τ
inst✝¹ : LawfulToList C τ
inst✝ : ToMultiset C τ
⊢ ↑(toList (singleton x)) = {x}
Tactic:
rw [LawfulToList.toMultiset_toList]
Proof state after:
C : Type u
τ : outParam (Type v)
inst✝⁴ : Insert C τ
x : τ
inst✝³ : ToList C τ
inst✝² : LeanColls.ToMultiset C τ
inst✝¹ : LawfulToList C τ
inst✝ : ToMultiset C τ
⊢ ToMultiset.toMultiset (singleton x) = {x}
Theorem: LeanColls.Insert.toList_singleton
Proof state before:
C : Type u
τ : outParam (Type v)
inst✝⁴ : Insert C τ
x : τ
inst✝³ : ToList C τ
inst✝² : LeanColls.ToMultiset C τ
inst✝¹ : LawfulToList C τ
inst✝ : ToMultiset C τ
⊢ ToMultiset.toMultiset (singleton x) = {x}
Tactic:
rw [ToMultiset.toMultiset_singleton]
Proof state after:
no goals
Theorem: Insert.mem_into_iff
Proof state before:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
⊢ x ∈ into C' c ↔ x ∈ c
Tactic:
unfold into
Proof state after:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
⊢ x ∈ fold c insert empty ↔ x ∈ c
Theorem: Insert.mem_into_iff
Proof state before:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
⊢ x ∈ fold c insert empty ↔ x ∈ c
Tactic:
have ⟨L, perm, h⟩ := Fold.ToList.fold_eq_fold_toList c
Proof state after:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ x ∈ fold c insert empty ↔ x ∈ c
Theorem: Insert.mem_into_iff
Proof state before:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ x ∈ fold c insert empty ↔ x ∈ c
Tactic:
conv at h => ext; ext; ext; rw [← List.foldr_reverse]
Proof state after:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldr (fun y x => f x y) init L.reverse
⊢ x ∈ fold c insert empty ↔ x ∈ c
Theorem: Insert.mem_into_iff
Proof state before:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldr (fun y x => f x y) init L.reverse
⊢ x ∈ fold c insert empty ↔ x ∈ c
Tactic:
replace perm := (List.reverse_perm ..).trans perm
Proof state after:
C' : Type u_1
τ : Type u_2
C : Type u_3
x : τ
inst✝⁷ : Insert C' τ
inst✝⁶ : Membership τ C'
inst✝⁵ : Mem C' τ
inst✝⁴ : Fold C τ
inst✝³ : Membership τ C
inst✝² : ToList C τ
inst✝¹ : Fold.ToList C τ
inst✝ : Mem.ToList C τ
c : C
L : List τ
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldr (fun y x => f x y) init L.reverse
perm : L.reverse.Perm (toList c)
⊢ x ∈ fold c insert empty ↔ x ∈ c