[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
⊢ zipWith f l [] = []
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l' : List β
⊢ zipWith f l l' = [] ↔ l = [] ∨ l' = []
[PROOFSTEP]
cases l
[GOAL]
case nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l' : List β
⊢ zipWith f [] l' = [] ↔ [] = [] ∨ l' = []
[PROOFSTEP]
cases l'
[GOAL]
case cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l' : List β
head✝ : α
tail✝ : List α
⊢ zipWith f (head✝ :: tail✝) l' = [] ↔ head✝ :: tail✝ = [] ∨ l' = []
[PROOFSTEP]
cases l'
[GOAL]
case nil.nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
⊢ zipWith f [] [] = [] ↔ [] = [] ∨ [] = []
[PROOFSTEP]
simp
[GOAL]
case nil.cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
head✝ : β
tail✝ : List β
⊢ zipWith f [] (head✝ :: tail✝) = [] ↔ [] = [] ∨ head✝ :: tail✝ = []
[PROOFSTEP]
simp
[GOAL]
case cons.nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
head✝ : α
tail✝ : List α
⊢ zipWith f (head✝ :: tail✝) [] = [] ↔ head✝ :: tail✝ = [] ∨ [] = []
[PROOFSTEP]
simp
[GOAL]
case cons.cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
head✝¹ : α
tail✝¹ : List α
head✝ : β
tail✝ : List β
⊢ zipWith f (head✝¹ :: tail✝¹) (head✝ :: tail✝) = [] ↔ head✝¹ :: tail✝¹ = [] ∨ head✝ :: tail✝ = []
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l₁ : List α
⊢ map Prod.swap (zip l₁ []) = zip [] l₁
[PROOFSTEP]
rw [zip_nil_right]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l₁ : List α
⊢ map Prod.swap [] = zip [] l₁
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
a : α
l₁ : List α
b : β
l₂ : List β
⊢ map Prod.swap (zip (a :: l₁) (b :: l₂)) = zip (b :: l₂) (a :: l₁)
[PROOFSTEP]
simp only [zip_cons_cons, map_cons, zip_swap l₁ l₂, Prod.swap_prod_mk]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
p : γ → Prop
x✝ : length [] = length []
⊢ All₂ p (zipWith f [] []) ↔ Forall₂ (fun x y => p (f x y)) [] []
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
p : γ → Prop
a : α
l₁ : List α
b : β
l₂ : List β
h : length (a :: l₁) = length (b :: l₂)
⊢ All₂ p (zipWith f (a :: l₁) (b :: l₂)) ↔ Forall₂ (fun x y => p (f x y)) (a :: l₁) (b :: l₂)
[PROOFSTEP]
simp only [length_cons, succ_inj'] at h
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
p : γ → Prop
a : α
l₁ : List α
b : β
l₂ : List β
h : length l₁ = length l₂
⊢ All₂ p (zipWith f (a :: l₁) (b :: l₂)) ↔ Forall₂ (fun x y => p (f x y)) (a :: l₁) (b :: l₂)
[PROOFSTEP]
simp [all₂_zipWith h]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
i : ℕ
l : List α
l' : List β
h : i < length (zipWith f l l')
⊢ i < length l
[PROOFSTEP]
rw [length_zipWith, lt_min_iff] at h
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
i : ℕ
l : List α
l' : List β
h : i < length l ∧ i < length l'
⊢ i < length l
[PROOFSTEP]
exact h.left
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
i : ℕ
l : List α
l' : List β
h : i < length (zipWith f l l')
⊢ i < length l'
[PROOFSTEP]
rw [length_zipWith, lt_min_iff] at h
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
i : ℕ
l : List α
l' : List β
h : i < length l ∧ i < length l'
⊢ i < length l'
[PROOFSTEP]
exact h.right
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
r₁ : List α
l₂ r₂ : List β
h : length [] = length l₂
⊢ zip ([] ++ r₁) (l₂ ++ r₂) = zip [] l₂ ++ zip r₁ r₂
[PROOFSTEP]
simp only [eq_nil_of_length_eq_zero h.symm]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
r₁ : List α
l₂ r₂ : List β
h : length [] = length l₂
⊢ zip ([] ++ r₁) ([] ++ r₂) = zip [] [] ++ zip r₁ r₂
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l₁ r₁ : List α
r₂ : List β
h : length l₁ = length []
⊢ zip (l₁ ++ r₁) ([] ++ r₂) = zip l₁ [] ++ zip r₁ r₂
[PROOFSTEP]
simp only [eq_nil_of_length_eq_zero h]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l₁ r₁ : List α
r₂ : List β
h : length l₁ = length []
⊢ zip ([] ++ r₁) ([] ++ r₂) = zip [] [] ++ zip r₁ r₂
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
a : α
l₁ r₁ : List α
b : β
l₂ r₂ : List β
h : length (a :: l₁) = length (b :: l₂)
⊢ zip (a :: l₁ ++ r₁) (b :: l₂ ++ r₂) = zip (a :: l₁) (b :: l₂) ++ zip r₁ r₂
[PROOFSTEP]
simp only [cons_append, zip_cons_cons, zip_append (succ.inj h)]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → γ
g : β → δ
l₁ : List α
⊢ zip (map f l₁) (map g []) = map (Prod.map f g) (zip l₁ [])
[PROOFSTEP]
simp only [map, zip_nil_right]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → γ
g : β → δ
a : α
l₁ : List α
b : β
l₂ : List β
⊢ zip (map f (a :: l₁)) (map g (b :: l₂)) = map (Prod.map f g) (zip (a :: l₁) (b :: l₂))
[PROOFSTEP]
simp only [map, zip_cons_cons, zip_map, Prod.map]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → γ
g : β → δ
a : α
l₁ : List α
b : β
l₂ : List β
⊢ (f a, g b) :: map (fun x => (f x.fst, g x.snd)) (zip l₁ l₂) =
    (f a, g b) :: map (fun x => (f x.fst, g x.snd)) (zipWith Prod.mk l₁ l₂)
[PROOFSTEP]
constructor
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → γ
l₁ : List α
l₂ : List β
⊢ zip (map f l₁) l₂ = map (Prod.map f id) (zip l₁ l₂)
[PROOFSTEP]
rw [← zip_map, map_id]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : β → γ
l₁ : List α
l₂ : List β
⊢ zip l₁ (map f l₂) = map (Prod.map id f) (zip l₁ l₂)
[PROOFSTEP]
rw [← zip_map, map_id]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
μ : Type u_5
f : γ → δ → μ
g : α → γ
h : β → δ
as : List α
bs : List β
⊢ zipWith f (map g as) (map h bs) = zipWith (fun a b => f (g a) (h b)) as bs
[PROOFSTEP]
induction as generalizing bs
[GOAL]
case nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
μ : Type u_5
f : γ → δ → μ
g : α → γ
h : β → δ
bs : List β
⊢ zipWith f (map g []) (map h bs) = zipWith (fun a b => f (g a) (h b)) [] bs
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
μ : Type u_5
f : γ → δ → μ
g : α → γ
h : β → δ
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (bs : List β), zipWith f (map g tail✝) (map h bs) = zipWith (fun a b => f (g a) (h b)) tail✝ bs
bs : List β
⊢ zipWith f (map g (head✝ :: tail✝)) (map h bs) = zipWith (fun a b => f (g a) (h b)) (head✝ :: tail✝) bs
[PROOFSTEP]
cases bs
[GOAL]
case cons.nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
μ : Type u_5
f : γ → δ → μ
g : α → γ
h : β → δ
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (bs : List β), zipWith f (map g tail✝) (map h bs) = zipWith (fun a b => f (g a) (h b)) tail✝ bs
⊢ zipWith f (map g (head✝ :: tail✝)) (map h []) = zipWith (fun a b => f (g a) (h b)) (head✝ :: tail✝) []
[PROOFSTEP]
simp [*]
[GOAL]
case cons.cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
μ : Type u_5
f : γ → δ → μ
g : α → γ
h : β → δ
head✝¹ : α
tail✝¹ : List α
tail_ih✝ : ∀ (bs : List β), zipWith f (map g tail✝¹) (map h bs) = zipWith (fun a b => f (g a) (h b)) tail✝¹ bs
head✝ : β
tail✝ : List β
⊢ zipWith f (map g (head✝¹ :: tail✝¹)) (map h (head✝ :: tail✝)) =
    zipWith (fun a b => f (g a) (h b)) (head✝¹ :: tail✝¹) (head✝ :: tail✝)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
g : δ → α
l : List δ
l' : List β
⊢ zipWith f (map g l) l' = zipWith (f ∘ g) l l'
[PROOFSTEP]
convert zipWith_map f g id l l'
[GOAL]
case h.e'_2.h.e'_6
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
g : δ → α
l : List δ
l' : List β
⊢ l' = map id l'
[PROOFSTEP]
exact Eq.symm (List.map_id _)
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
g : δ → β
l' : List δ
⊢ zipWith f l (map g l') = zipWith (fun x => f x ∘ g) l l'
[PROOFSTEP]
convert List.zipWith_map f id g l l'
[GOAL]
case h.e'_2.h.e'_5
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
g : δ → β
l' : List δ
⊢ l = map id l
[PROOFSTEP]
exact Eq.symm (List.map_id _)
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β
g : α → γ
a : α
l : List α
⊢ zip (map f (a :: l)) (map g (a :: l)) = map (fun a => (f a, g a)) (a :: l)
[PROOFSTEP]
simp only [map, zip_cons_cons, zip_map']
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ✝ : Type u_3
ε : Type u_4
δ : Type u_5
f : α → β
g : γ → δ → α
l : List γ
l' : List δ
⊢ map f (zipWith g l l') = zipWith (fun x y => f (g x y)) l l'
[PROOFSTEP]
induction' l with hd tl hl generalizing l'
[GOAL]
case nil
α : Type u
β : Type u_1
γ : Type u_2
δ✝ : Type u_3
ε : Type u_4
δ : Type u_5
f : α → β
g : γ → δ → α
l'✝ l' : List δ
⊢ map f (zipWith g [] l') = zipWith (fun x y => f (g x y)) [] l'
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
β : Type u_1
γ : Type u_2
δ✝ : Type u_3
ε : Type u_4
δ : Type u_5
f : α → β
g : γ → δ → α
l'✝ : List δ
hd : γ
tl : List γ
hl : ∀ (l' : List δ), map f (zipWith g tl l') = zipWith (fun x y => f (g x y)) tl l'
l' : List δ
⊢ map f (zipWith g (hd :: tl) l') = zipWith (fun x y => f (g x y)) (hd :: tl) l'
[PROOFSTEP]
cases l'
[GOAL]
case cons.nil
α : Type u
β : Type u_1
γ : Type u_2
δ✝ : Type u_3
ε : Type u_4
δ : Type u_5
f : α → β
g : γ → δ → α
l' : List δ
hd : γ
tl : List γ
hl : ∀ (l' : List δ), map f (zipWith g tl l') = zipWith (fun x y => f (g x y)) tl l'
⊢ map f (zipWith g (hd :: tl) []) = zipWith (fun x y => f (g x y)) (hd :: tl) []
[PROOFSTEP]
simp
[GOAL]
case cons.cons
α : Type u
β : Type u_1
γ : Type u_2
δ✝ : Type u_3
ε : Type u_4
δ : Type u_5
f : α → β
g : γ → δ → α
l' : List δ
hd : γ
tl : List γ
hl : ∀ (l' : List δ), map f (zipWith g tl l') = zipWith (fun x y => f (g x y)) tl l'
head✝ : δ
tail✝ : List δ
⊢ map f (zipWith g (hd :: tl) (head✝ :: tail✝)) = zipWith (fun x y => f (g x y)) (hd :: tl) (head✝ :: tail✝)
[PROOFSTEP]
simp [hl]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
a : α
b : β
head✝¹ : α
l₁ : List α
head✝ : β
l₂ : List β
h : (a, b) ∈ zip (head✝¹ :: l₁) (head✝ :: l₂)
⊢ a ∈ head✝¹ :: l₁ ∧ b ∈ head✝ :: l₂
[PROOFSTEP]
cases' h with _ _ _ h
[GOAL]
case head
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
a : α
b : β
l₁ : List α
l₂ : List β
⊢ a ∈ a :: l₁ ∧ b ∈ b :: l₂
[PROOFSTEP]
simp
[GOAL]
case tail
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
a : α
b : β
head✝¹ : α
l₁ : List α
head✝ : β
l₂ : List β
h : Mem (a, b) (zipWith Prod.mk l₁ l₂)
⊢ a ∈ head✝¹ :: l₁ ∧ b ∈ head✝ :: l₂
[PROOFSTEP]
have := mem_zip h
[GOAL]
case tail
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
a : α
b : β
head✝¹ : α
l₁ : List α
head✝ : β
l₂ : List β
h : Mem (a, b) (zipWith Prod.mk l₁ l₂)
this : a ∈ l₁ ∧ b ∈ l₂
⊢ a ∈ head✝¹ :: l₁ ∧ b ∈ head✝ :: l₂
[PROOFSTEP]
exact ⟨Mem.tail _ this.1, Mem.tail _ this.2⟩
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
head✝¹ : α
as : List α
head✝ : β
bs : List β
h : length (head✝¹ :: as) ≤ length (head✝ :: bs)
⊢ map Prod.fst (zip (head✝¹ :: as) (head✝ :: bs)) = head✝¹ :: as
[PROOFSTEP]
simp [succ_le_succ_iff] at h
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
head✝¹ : α
as : List α
head✝ : β
bs : List β
h : length as ≤ length bs
⊢ map Prod.fst (zip (head✝¹ :: as) (head✝ :: bs)) = head✝¹ :: as
[PROOFSTEP]
change _ :: map Prod.fst (zip as bs) = _ :: as
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
head✝¹ : α
as : List α
head✝ : β
bs : List β
h : length as ≤ length bs
⊢ (head✝¹, head✝).fst :: map Prod.fst (zip as bs) = head✝¹ :: as
[PROOFSTEP]
rw [map_fst_zip as bs h]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
a : α
as : List α
h : length (a :: as) ≤ length []
⊢ map Prod.fst (zip (a :: as) []) = a :: as
[PROOFSTEP]
simp at h
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
x✝¹ : List α
x✝ : length [] ≤ length x✝¹
⊢ map Prod.snd (zip x✝¹ []) = []
[PROOFSTEP]
rw [zip_nil_right]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
x✝¹ : List α
x✝ : length [] ≤ length x✝¹
⊢ map Prod.snd [] = []
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
b : β
bs : List β
h : length (b :: bs) ≤ length []
⊢ map Prod.snd (zip [] (b :: bs)) = b :: bs
[PROOFSTEP]
simp at h
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
a : α
as : List α
b : β
bs : List β
h : length (b :: bs) ≤ length (a :: as)
⊢ map Prod.snd (zip (a :: as) (b :: bs)) = b :: bs
[PROOFSTEP]
simp [succ_le_succ_iff] at h
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
a : α
as : List α
b : β
bs : List β
h : length bs ≤ length as
⊢ map Prod.snd (zip (a :: as) (b :: bs)) = b :: bs
[PROOFSTEP]
change _ :: map Prod.snd (zip as bs) = _ :: bs
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
a : α
as : List α
b : β
bs : List β
h : length bs ≤ length as
⊢ (a, b).snd :: map Prod.snd (zip as bs) = b :: bs
[PROOFSTEP]
rw [map_snd_zip as bs h]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
a : α
b : β
l : List (α × β)
⊢ unzip ((a, b) :: l) = (map Prod.fst ((a, b) :: l), map Prod.snd ((a, b) :: l))
[PROOFSTEP]
simp only [unzip_cons, map_cons, unzip_eq_map l]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l : List (α × β)
⊢ (unzip l).fst = map Prod.fst l
[PROOFSTEP]
simp only [unzip_eq_map]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l : List (α × β)
⊢ (unzip l).snd = map Prod.snd l
[PROOFSTEP]
simp only [unzip_eq_map]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l : List (α × β)
⊢ unzip (map Prod.swap l) = Prod.swap (unzip l)
[PROOFSTEP]
simp only [unzip_eq_map, map_map]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l : List (α × β)
⊢ (map (Prod.fst ∘ Prod.swap) l, map (Prod.snd ∘ Prod.swap) l) = Prod.swap (map Prod.fst l, map Prod.snd l)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
a : α
b : β
l : List (α × β)
⊢ zip (unzip ((a, b) :: l)).fst (unzip ((a, b) :: l)).snd = (a, b) :: l
[PROOFSTEP]
simp only [unzip_cons, zip_cons_cons, zip_unzip l]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l₁ : List α
h : length l₁ ≤ length []
⊢ (unzip (zip l₁ [])).fst = l₁
[PROOFSTEP]
rw [eq_nil_of_length_eq_zero (Nat.eq_zero_of_le_zero h)]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l₁ : List α
h : length l₁ ≤ length []
⊢ (unzip (zip [] [])).fst = []
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
a : α
l₁ : List α
b : β
l₂ : List β
h : length (a :: l₁) ≤ length (b :: l₂)
⊢ (unzip (zip (a :: l₁) (b :: l₂))).fst = a :: l₁
[PROOFSTEP]
simp only [zip_cons_cons, unzip_cons, unzip_zip_left (le_of_succ_le_succ h)]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l₁ : List α
l₂ : List β
h : length l₂ ≤ length l₁
⊢ (unzip (zip l₁ l₂)).snd = l₂
[PROOFSTEP]
rw [← zip_swap, unzip_swap]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l₁ : List α
l₂ : List β
h : length l₂ ≤ length l₁
⊢ (Prod.swap (unzip (zip l₂ l₁))).snd = l₂
[PROOFSTEP]
exact unzip_zip_left h
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l₁ : List α
l₂ : List β
h : length l₁ = length l₂
⊢ unzip (zip l₁ l₂) = (l₁, l₂)
[PROOFSTEP]
rw [← Prod.mk.eta (p := unzip (zip l₁ l₂)), unzip_zip_left (le_of_eq h), unzip_zip_right (ge_of_eq h)]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l : List α
l' : List β
lp : List (α × β)
hl : map Prod.fst lp = l
hr : map Prod.snd lp = l'
⊢ lp = zip l l'
[PROOFSTEP]
rw [← hl, ← hr, ← zip_unzip lp, ← unzip_left, ← unzip_right, zip_unzip, zip_unzip]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l : List α
f : α → β
⊢ map (fun x => (x, f x)) l = zip l (map f l)
[PROOFSTEP]
rw [← zip_map']
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l : List α
f : α → β
⊢ zip (map (fun x => x) l) (map (fun x => f x) l) = zip l (map f l)
[PROOFSTEP]
congr
[GOAL]
case e_a
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l : List α
f : α → β
⊢ map (fun x => x) l = l
[PROOFSTEP]
exact map_id _
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l : List α
f : α → β
⊢ map (fun x => (f x, x)) l = zip (map f l) l
[PROOFSTEP]
rw [← zip_map']
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l : List α
f : α → β
⊢ zip (map (fun x => f x) l) (map (fun x => x) l) = zip (map f l) l
[PROOFSTEP]
congr
[GOAL]
case e_a
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l : List α
f : α → β
⊢ map (fun x => x) l = l
[PROOFSTEP]
exact map_id _
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f g : α → β → γ
la : List α
lb : List β
h : Forall₂ (fun a b => f a b = g a b) la lb
⊢ zipWith f la lb = zipWith g la lb
[PROOFSTEP]
induction' h with a b as bs hfg _ ih
[GOAL]
case nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f g : α → β → γ
la : List α
lb : List β
⊢ zipWith f [] [] = zipWith g [] []
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f g : α → β → γ
la : List α
lb : List β
a : α
b : β
as : List α
bs : List β
hfg : f a b = g a b
a✝ : Forall₂ (fun a b => f a b = g a b) as bs
ih : zipWith f as bs = zipWith g as bs
⊢ zipWith f (a :: as) (b :: bs) = zipWith g (a :: as) (b :: bs)
[PROOFSTEP]
exact congr_arg₂ _ hfg ih
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → α → β
comm : ∀ (x y : α), f x y = f y x
l l' : List α
⊢ zipWith f l l' = zipWith f l' l
[PROOFSTEP]
rw [zipWith_comm]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → α → β
comm : ∀ (x y : α), f x y = f y x
l l' : List α
⊢ zipWith (fun b a => f a b) l' l = zipWith f l' l
[PROOFSTEP]
simp only [comm]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l : List α
⊢ length (revzip l) = length l
[PROOFSTEP]
simp only [revzip, length_zip, length_reverse, min_self]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l : List α
⊢ map Prod.fst (revzip l) = l
[PROOFSTEP]
rw [← unzip_left, unzip_revzip]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l : List α
⊢ map Prod.snd (revzip l) = reverse l
[PROOFSTEP]
rw [← unzip_right, unzip_revzip]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l : List α
⊢ reverse (revzip l) = revzip (reverse l)
[PROOFSTEP]
rw [← zip_unzip (revzip l).reverse]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l : List α
⊢ zip (unzip (reverse (revzip l))).fst (unzip (reverse (revzip l))).snd = revzip (reverse l)
[PROOFSTEP]
simp [unzip_eq_map, revzip, map_reverse, map_fst_zip, map_snd_zip]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l : List α
⊢ map Prod.swap (revzip l) = revzip (reverse l)
[PROOFSTEP]
simp [revzip]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l₁ : List α
l₂ : List β
i : ℕ
⊢ get? (zipWith f l₁ l₂) i = Option.bind (Option.map f (get? l₁ i)) fun g => Option.map g (get? l₂ i)
[PROOFSTEP]
induction' l₁ with head tail generalizing l₂ i
[GOAL]
case nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l₂✝ : List β
i✝ : ℕ
l₂ : List β
i : ℕ
⊢ get? (zipWith f [] l₂) i = Option.bind (Option.map f (get? [] i)) fun g => Option.map g (get? l₂ i)
[PROOFSTEP]
rw [zipWith]
[GOAL]
case nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l₂✝ : List β
i✝ : ℕ
l₂ : List β
i : ℕ
⊢ get? [] i = Option.bind (Option.map f (get? [] i)) fun g => Option.map g (get? l₂ i)
[PROOFSTEP]
simp
[GOAL]
case nil.x_4
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l₂✝ : List β
i✝ : ℕ
l₂ : List β
i : ℕ
⊢ ∀ (x : α) (xs : List α) (y : β) (ys : List β), [] = x :: xs → l₂ = y :: ys → False
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l₂✝ : List β
i✝ : ℕ
head : α
tail : List α
tail_ih✝ :
  ∀ (l₂ : List β) (i : ℕ),
    get? (zipWith f tail l₂) i = Option.bind (Option.map f (get? tail i)) fun g => Option.map g (get? l₂ i)
l₂ : List β
i : ℕ
⊢ get? (zipWith f (head :: tail) l₂) i =
    Option.bind (Option.map f (get? (head :: tail) i)) fun g => Option.map g (get? l₂ i)
[PROOFSTEP]
cases l₂
[GOAL]
case cons.nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l₂ : List β
i✝ : ℕ
head : α
tail : List α
tail_ih✝ :
  ∀ (l₂ : List β) (i : ℕ),
    get? (zipWith f tail l₂) i = Option.bind (Option.map f (get? tail i)) fun g => Option.map g (get? l₂ i)
i : ℕ
⊢ get? (zipWith f (head :: tail) []) i =
    Option.bind (Option.map f (get? (head :: tail) i)) fun g => Option.map g (get? [] i)
case cons.cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l₂ : List β
i✝ : ℕ
head : α
tail : List α
tail_ih✝ :
  ∀ (l₂ : List β) (i : ℕ),
    get? (zipWith f tail l₂) i = Option.bind (Option.map f (get? tail i)) fun g => Option.map g (get? l₂ i)
i : ℕ
head✝ : β
tail✝ : List β
⊢ get? (zipWith f (head :: tail) (head✝ :: tail✝)) i =
    Option.bind (Option.map f (get? (head :: tail) i)) fun g => Option.map g (get? (head✝ :: tail✝) i)
[PROOFSTEP]
simp only [zipWith, Seq.seq, Functor.map, get?, Option.map_none']
[GOAL]
case cons.nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l₂ : List β
i✝ : ℕ
head : α
tail : List α
tail_ih✝ :
  ∀ (l₂ : List β) (i : ℕ),
    get? (zipWith f tail l₂) i = Option.bind (Option.map f (get? tail i)) fun g => Option.map g (get? l₂ i)
i : ℕ
⊢ none = Option.bind (Option.map f (get? (head :: tail) i)) fun g => none
[PROOFSTEP]
cases (head :: tail).get? i
[GOAL]
case cons.nil.none
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l₂ : List β
i✝ : ℕ
head : α
tail : List α
tail_ih✝ :
  ∀ (l₂ : List β) (i : ℕ),
    get? (zipWith f tail l₂) i = Option.bind (Option.map f (get? tail i)) fun g => Option.map g (get? l₂ i)
i : ℕ
⊢ none = Option.bind (Option.map f none) fun g => none
[PROOFSTEP]
rfl
[GOAL]
case cons.nil.some
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l₂ : List β
i✝ : ℕ
head : α
tail : List α
tail_ih✝ :
  ∀ (l₂ : List β) (i : ℕ),
    get? (zipWith f tail l₂) i = Option.bind (Option.map f (get? tail i)) fun g => Option.map g (get? l₂ i)
i : ℕ
val✝ : α
⊢ none = Option.bind (Option.map f (some val✝)) fun g => none
[PROOFSTEP]
rfl
[GOAL]
case cons.cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l₂ : List β
i✝ : ℕ
head : α
tail : List α
tail_ih✝ :
  ∀ (l₂ : List β) (i : ℕ),
    get? (zipWith f tail l₂) i = Option.bind (Option.map f (get? tail i)) fun g => Option.map g (get? l₂ i)
i : ℕ
head✝ : β
tail✝ : List β
⊢ get? (zipWith f (head :: tail) (head✝ :: tail✝)) i =
    Option.bind (Option.map f (get? (head :: tail) i)) fun g => Option.map g (get? (head✝ :: tail✝) i)
[PROOFSTEP]
cases i
[GOAL]
case cons.cons.zero
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l₂ : List β
i : ℕ
head : α
tail : List α
tail_ih✝ :
  ∀ (l₂ : List β) (i : ℕ),
    get? (zipWith f tail l₂) i = Option.bind (Option.map f (get? tail i)) fun g => Option.map g (get? l₂ i)
head✝ : β
tail✝ : List β
⊢ get? (zipWith f (head :: tail) (head✝ :: tail✝)) zero =
    Option.bind (Option.map f (get? (head :: tail) zero)) fun g => Option.map g (get? (head✝ :: tail✝) zero)
[PROOFSTEP]
simp only [Option.map_some', get?, Option.some_bind', *]
[GOAL]
case cons.cons.succ
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l₂ : List β
i : ℕ
head : α
tail : List α
tail_ih✝ :
  ∀ (l₂ : List β) (i : ℕ),
    get? (zipWith f tail l₂) i = Option.bind (Option.map f (get? tail i)) fun g => Option.map g (get? l₂ i)
head✝ : β
tail✝ : List β
n✝ : ℕ
⊢ get? (zipWith f (head :: tail) (head✝ :: tail✝)) (succ n✝) =
    Option.bind (Option.map f (get? (head :: tail) (succ n✝))) fun g => Option.map g (get? (head✝ :: tail✝) (succ n✝))
[PROOFSTEP]
simp only [Option.map_some', get?, Option.some_bind', *]
[GOAL]
α✝ : Type u
β✝ : Type u_1
γ✝ : Type u_2
δ : Type u_3
ε : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
f : α → β → γ
l₁ : List α
l₂ : List β
z : γ
i : ℕ
⊢ get? (zipWith f l₁ l₂) i = some z ↔ ∃ x y, get? l₁ i = some x ∧ get? l₂ i = some y ∧ f x y = z
[PROOFSTEP]
induction l₁ generalizing l₂ i
[GOAL]
case nil
α✝ : Type u
β✝ : Type u_1
γ✝ : Type u_2
δ : Type u_3
ε : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
f : α → β → γ
z : γ
l₂ : List β
i : ℕ
⊢ get? (zipWith f [] l₂) i = some z ↔ ∃ x y, get? [] i = some x ∧ get? l₂ i = some y ∧ f x y = z
[PROOFSTEP]
simp [zipWith]
[GOAL]
case cons
α✝ : Type u
β✝ : Type u_1
γ✝ : Type u_2
δ : Type u_3
ε : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
f : α → β → γ
z : γ
head✝ : α
tail✝ : List α
tail_ih✝ :
  ∀ (l₂ : List β) (i : ℕ),
    get? (zipWith f tail✝ l₂) i = some z ↔ ∃ x y, get? tail✝ i = some x ∧ get? l₂ i = some y ∧ f x y = z
l₂ : List β
i : ℕ
⊢ get? (zipWith f (head✝ :: tail✝) l₂) i = some z ↔
    ∃ x y, get? (head✝ :: tail✝) i = some x ∧ get? l₂ i = some y ∧ f x y = z
[PROOFSTEP]
cases l₂
[GOAL]
case cons.nil
α✝ : Type u
β✝ : Type u_1
γ✝ : Type u_2
δ : Type u_3
ε : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
f : α → β → γ
z : γ
head✝ : α
tail✝ : List α
tail_ih✝ :
  ∀ (l₂ : List β) (i : ℕ),
    get? (zipWith f tail✝ l₂) i = some z ↔ ∃ x y, get? tail✝ i = some x ∧ get? l₂ i = some y ∧ f x y = z
i : ℕ
⊢ get? (zipWith f (head✝ :: tail✝) []) i = some z ↔
    ∃ x y, get? (head✝ :: tail✝) i = some x ∧ get? [] i = some y ∧ f x y = z
[PROOFSTEP]
simp only [zipWith, get?, exists_false, and_false_iff, false_and_iff]
[GOAL]
case cons.cons
α✝ : Type u
β✝ : Type u_1
γ✝ : Type u_2
δ : Type u_3
ε : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
f : α → β → γ
z : γ
head✝¹ : α
tail✝¹ : List α
tail_ih✝ :
  ∀ (l₂ : List β) (i : ℕ),
    get? (zipWith f tail✝¹ l₂) i = some z ↔ ∃ x y, get? tail✝¹ i = some x ∧ get? l₂ i = some y ∧ f x y = z
i : ℕ
head✝ : β
tail✝ : List β
⊢ get? (zipWith f (head✝¹ :: tail✝¹) (head✝ :: tail✝)) i = some z ↔
    ∃ x y, get? (head✝¹ :: tail✝¹) i = some x ∧ get? (head✝ :: tail✝) i = some y ∧ f x y = z
[PROOFSTEP]
simp only [zipWith, get?, exists_false, and_false_iff, false_and_iff]
[GOAL]
case cons.cons
α✝ : Type u
β✝ : Type u_1
γ✝ : Type u_2
δ : Type u_3
ε : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
f : α → β → γ
z : γ
head✝¹ : α
tail✝¹ : List α
tail_ih✝ :
  ∀ (l₂ : List β) (i : ℕ),
    get? (zipWith f tail✝¹ l₂) i = some z ↔ ∃ x y, get? tail✝¹ i = some x ∧ get? l₂ i = some y ∧ f x y = z
i : ℕ
head✝ : β
tail✝ : List β
⊢ get? (f head✝¹ head✝ :: zipWith f tail✝¹ tail✝) i = some z ↔
    ∃ x y, get? (head✝¹ :: tail✝¹) i = some x ∧ get? (head✝ :: tail✝) i = some y ∧ f x y = z
[PROOFSTEP]
cases i
[GOAL]
case cons.cons.zero
α✝ : Type u
β✝ : Type u_1
γ✝ : Type u_2
δ : Type u_3
ε : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
f : α → β → γ
z : γ
head✝¹ : α
tail✝¹ : List α
tail_ih✝ :
  ∀ (l₂ : List β) (i : ℕ),
    get? (zipWith f tail✝¹ l₂) i = some z ↔ ∃ x y, get? tail✝¹ i = some x ∧ get? l₂ i = some y ∧ f x y = z
head✝ : β
tail✝ : List β
⊢ get? (f head✝¹ head✝ :: zipWith f tail✝¹ tail✝) zero = some z ↔
    ∃ x y, get? (head✝¹ :: tail✝¹) zero = some x ∧ get? (head✝ :: tail✝) zero = some y ∧ f x y = z
[PROOFSTEP]
simp [*]
[GOAL]
case cons.cons.succ
α✝ : Type u
β✝ : Type u_1
γ✝ : Type u_2
δ : Type u_3
ε : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
f : α → β → γ
z : γ
head✝¹ : α
tail✝¹ : List α
tail_ih✝ :
  ∀ (l₂ : List β) (i : ℕ),
    get? (zipWith f tail✝¹ l₂) i = some z ↔ ∃ x y, get? tail✝¹ i = some x ∧ get? l₂ i = some y ∧ f x y = z
head✝ : β
tail✝ : List β
n✝ : ℕ
⊢ get? (f head✝¹ head✝ :: zipWith f tail✝¹ tail✝) (succ n✝) = some z ↔
    ∃ x y, get? (head✝¹ :: tail✝¹) (succ n✝) = some x ∧ get? (head✝ :: tail✝) (succ n✝) = some y ∧ f x y = z
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l₁ : List α
l₂ : List β
z : α × β
i : ℕ
⊢ get? (zip l₁ l₂) i = some z ↔ get? l₁ i = some z.fst ∧ get? l₂ i = some z.snd
[PROOFSTEP]
cases z
[GOAL]
case mk
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l₁ : List α
l₂ : List β
i : ℕ
fst✝ : α
snd✝ : β
⊢ get? (zip l₁ l₂) i = some (fst✝, snd✝) ↔ get? l₁ i = some (fst✝, snd✝).fst ∧ get? l₂ i = some (fst✝, snd✝).snd
[PROOFSTEP]
rw [zip, get?_zip_with_eq_some]
[GOAL]
case mk
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l₁ : List α
l₂ : List β
i : ℕ
fst✝ : α
snd✝ : β
⊢ (∃ x y, get? l₁ i = some x ∧ get? l₂ i = some y ∧ (x, y) = (fst✝, snd✝)) ↔
    get? l₁ i = some (fst✝, snd✝).fst ∧ get? l₂ i = some (fst✝, snd✝).snd
[PROOFSTEP]
constructor
[GOAL]
case mk.mp
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l₁ : List α
l₂ : List β
i : ℕ
fst✝ : α
snd✝ : β
⊢ (∃ x y, get? l₁ i = some x ∧ get? l₂ i = some y ∧ (x, y) = (fst✝, snd✝)) →
    get? l₁ i = some (fst✝, snd✝).fst ∧ get? l₂ i = some (fst✝, snd✝).snd
[PROOFSTEP]
rintro ⟨x, y, h₀, h₁, h₂⟩
[GOAL]
case mk.mp.intro.intro.intro.intro
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l₁ : List α
l₂ : List β
i : ℕ
fst✝ : α
snd✝ : β
x : α
y : β
h₀ : get? l₁ i = some x
h₁ : get? l₂ i = some y
h₂ : (x, y) = (fst✝, snd✝)
⊢ get? l₁ i = some (fst✝, snd✝).fst ∧ get? l₂ i = some (fst✝, snd✝).snd
[PROOFSTEP]
simpa [h₀, h₁] using h₂
[GOAL]
case mk.mpr
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l₁ : List α
l₂ : List β
i : ℕ
fst✝ : α
snd✝ : β
⊢ get? l₁ i = some (fst✝, snd✝).fst ∧ get? l₂ i = some (fst✝, snd✝).snd →
    ∃ x y, get? l₁ i = some x ∧ get? l₂ i = some y ∧ (x, y) = (fst✝, snd✝)
[PROOFSTEP]
rintro ⟨h₀, h₁⟩
[GOAL]
case mk.mpr.intro
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l₁ : List α
l₂ : List β
i : ℕ
fst✝ : α
snd✝ : β
h₀ : get? l₁ i = some (fst✝, snd✝).fst
h₁ : get? l₂ i = some (fst✝, snd✝).snd
⊢ ∃ x y, get? l₁ i = some x ∧ get? l₂ i = some y ∧ (x, y) = (fst✝, snd✝)
[PROOFSTEP]
exact ⟨_, _, h₀, h₁, rfl⟩
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l' : List β
i : Fin (length (zipWith f l l'))
⊢ get (zipWith f l l') i =
    f (get l { val := ↑i, isLt := (_ : ↑i < length l) }) (get l' { val := ↑i, isLt := (_ : ↑i < length l') })
[PROOFSTEP]
rw [← Option.some_inj, ← get?_eq_get, get?_zip_with_eq_some]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l' : List β
i : Fin (length (zipWith f l l'))
⊢ ∃ x y,
    get? l ↑i = some x ∧
      get? l' ↑i = some y ∧
        f x y =
          f (get l { val := ↑i, isLt := (_ : ↑i < length l) }) (get l' { val := ↑i, isLt := (_ : ↑i < length l') })
[PROOFSTEP]
exact
  ⟨l.get ⟨i, lt_length_left_of_zipWith i.isLt⟩, l'.get ⟨i, lt_length_right_of_zipWith i.isLt⟩, by rw [get?_eq_get], by
    rw [get?_eq_get]; exact ⟨rfl, rfl⟩⟩
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l' : List β
i : Fin (length (zipWith f l l'))
⊢ get? l ↑i = some (get l { val := ↑i, isLt := (_ : ↑i < length l) })
[PROOFSTEP]
rw [get?_eq_get]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l' : List β
i : Fin (length (zipWith f l l'))
⊢ get? l' ↑i = some (get l' { val := ↑i, isLt := (_ : ↑i < length l') }) ∧
    f (get l { val := ↑i, isLt := (_ : ↑i < length l) }) (get l' { val := ↑i, isLt := (_ : ↑i < length l') }) =
      f (get l { val := ↑i, isLt := (_ : ↑i < length l) }) (get l' { val := ↑i, isLt := (_ : ↑i < length l') })
[PROOFSTEP]
rw [get?_eq_get]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l' : List β
i : Fin (length (zipWith f l l'))
⊢ some (get l' { val := ↑i, isLt := ?m.129801 }) = some (get l' { val := ↑i, isLt := (_ : ↑i < length l') }) ∧
    f (get l { val := ↑i, isLt := (_ : ↑i < length l) }) (get l' { val := ↑i, isLt := (_ : ↑i < length l') }) =
      f (get l { val := ↑i, isLt := (_ : ↑i < length l) }) (get l' { val := ↑i, isLt := (_ : ↑i < length l') })
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l' : List β
i : Fin (length (zipWith f l l'))
⊢ ↑i < length l'
[PROOFSTEP]
exact ⟨rfl, rfl⟩
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
l init tail : List α
⊢ (init, tail) ∈ zip (inits l) (tails l) ↔ init ++ tail = l
[PROOFSTEP]
induction' l with hd tl ih generalizing init tail
[GOAL]
case nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
init✝ tail✝ init tail : List α
⊢ (init, tail) ∈ zip (inits []) (tails []) ↔ init ++ tail = []
[PROOFSTEP]
simp_rw [tails, inits, zip_cons_cons]
[GOAL]
case cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
init✝ tail✝ : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
init tail : List α
⊢ (init, tail) ∈ zip (inits (hd :: tl)) (tails (hd :: tl)) ↔ init ++ tail = hd :: tl
[PROOFSTEP]
simp_rw [tails, inits, zip_cons_cons]
[GOAL]
case nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
init✝ tail✝ init tail : List α
⊢ (init, tail) ∈ ([], []) :: zip [] [] ↔ init ++ tail = []
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
init✝ tail✝ : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
init tail : List α
⊢ (init, tail) ∈ ([], hd :: tl) :: zip (map (fun t => hd :: t) (inits tl)) (tails tl) ↔ init ++ tail = hd :: tl
[PROOFSTEP]
constructor
[GOAL]
case cons.mp
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
init✝ tail✝ : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
init tail : List α
⊢ (init, tail) ∈ ([], hd :: tl) :: zip (map (fun t => hd :: t) (inits tl)) (tails tl) → init ++ tail = hd :: tl
[PROOFSTEP]
rw [mem_cons, zip_map_left, mem_map, Prod.exists]
[GOAL]
case cons.mpr
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
init✝ tail✝ : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
init tail : List α
⊢ init ++ tail = hd :: tl → (init, tail) ∈ ([], hd :: tl) :: zip (map (fun t => hd :: t) (inits tl)) (tails tl)
[PROOFSTEP]
rw [mem_cons, zip_map_left, mem_map, Prod.exists]
[GOAL]
case cons.mp
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
init✝ tail✝ : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
init tail : List α
⊢ ((init, tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ zip (inits tl) (tails tl) ∧ Prod.map (fun t => hd :: t) id (a, b) = (init, tail)) →
    init ++ tail = hd :: tl
[PROOFSTEP]
rintro (⟨rfl, rfl⟩ | ⟨_, _, h, rfl, rfl⟩)
[GOAL]
case cons.mp.inl.refl
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
init tail : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
⊢ [] ++ hd :: tl = hd :: tl
[PROOFSTEP]
simp
[GOAL]
case cons.mp.inr.intro.intro.intro.refl
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
init tail : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
w✝¹ w✝ : List α
h : (w✝¹, w✝) ∈ zip (inits tl) (tails tl)
⊢ (fun t => hd :: t) w✝¹ ++ id w✝ = hd :: tl
[PROOFSTEP]
simp [ih.mp h]
[GOAL]
case cons.mpr
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
init✝ tail✝ : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
init tail : List α
⊢ init ++ tail = hd :: tl →
    (init, tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ zip (inits tl) (tails tl) ∧ Prod.map (fun t => hd :: t) id (a, b) = (init, tail)
[PROOFSTEP]
cases' init with hd' tl'
[GOAL]
case cons.mpr.nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
init tail✝ : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
tail : List α
⊢ [] ++ tail = hd :: tl →
    ([], tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ zip (inits tl) (tails tl) ∧ Prod.map (fun t => hd :: t) id (a, b) = ([], tail)
[PROOFSTEP]
rintro rfl
[GOAL]
case cons.mpr.nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
init tail : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
⊢ ([], hd :: tl) = ([], hd :: tl) ∨
    ∃ a b, (a, b) ∈ zip (inits tl) (tails tl) ∧ Prod.map (fun t => hd :: t) id (a, b) = ([], hd :: tl)
[PROOFSTEP]
simp
[GOAL]
case cons.mpr.cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
init tail✝ : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
tail : List α
hd' : α
tl' : List α
⊢ hd' :: tl' ++ tail = hd :: tl →
    (hd' :: tl', tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ zip (inits tl) (tails tl) ∧ Prod.map (fun t => hd :: t) id (a, b) = (hd' :: tl', tail)
[PROOFSTEP]
intro h
[GOAL]
case cons.mpr.cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
init tail✝ : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
tail : List α
hd' : α
tl' : List α
h : hd' :: tl' ++ tail = hd :: tl
⊢ (hd' :: tl', tail) = ([], hd :: tl) ∨
    ∃ a b, (a, b) ∈ zip (inits tl) (tails tl) ∧ Prod.map (fun t => hd :: t) id (a, b) = (hd' :: tl', tail)
[PROOFSTEP]
right
[GOAL]
case cons.mpr.cons.h
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
init tail✝ : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
tail : List α
hd' : α
tl' : List α
h : hd' :: tl' ++ tail = hd :: tl
⊢ ∃ a b, (a, b) ∈ zip (inits tl) (tails tl) ∧ Prod.map (fun t => hd :: t) id (a, b) = (hd' :: tl', tail)
[PROOFSTEP]
use tl', tail
[GOAL]
case h
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
init tail✝ : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
tail : List α
hd' : α
tl' : List α
h : hd' :: tl' ++ tail = hd :: tl
⊢ (tl', tail) ∈ zip (inits tl) (tails tl) ∧ Prod.map (fun t => hd :: t) id (tl', tail) = (hd' :: tl', tail)
[PROOFSTEP]
simp_all
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l' : List β
⊢ map (Function.uncurry f) (zip l l') = zipWith f l l'
[PROOFSTEP]
rw [zip]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l' : List β
⊢ map (Function.uncurry f) (zipWith Prod.mk l l') = zipWith f l l'
[PROOFSTEP]
induction' l with hd tl hl generalizing l'
[GOAL]
case nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l'✝ l' : List β
⊢ map (Function.uncurry f) (zipWith Prod.mk [] l') = zipWith f [] l'
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l'✝ : List β
hd : α
tl : List α
hl : ∀ (l' : List β), map (Function.uncurry f) (zipWith Prod.mk tl l') = zipWith f tl l'
l' : List β
⊢ map (Function.uncurry f) (zipWith Prod.mk (hd :: tl) l') = zipWith f (hd :: tl) l'
[PROOFSTEP]
cases' l' with hd' tl'
[GOAL]
case cons.nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l' : List β
hd : α
tl : List α
hl : ∀ (l' : List β), map (Function.uncurry f) (zipWith Prod.mk tl l') = zipWith f tl l'
⊢ map (Function.uncurry f) (zipWith Prod.mk (hd :: tl) []) = zipWith f (hd :: tl) []
[PROOFSTEP]
simp
[GOAL]
case cons.cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l' : List β
hd : α
tl : List α
hl : ∀ (l' : List β), map (Function.uncurry f) (zipWith Prod.mk tl l') = zipWith f tl l'
hd' : β
tl' : List β
⊢ map (Function.uncurry f) (zipWith Prod.mk (hd :: tl) (hd' :: tl')) = zipWith f (hd :: tl) (hd' :: tl')
[PROOFSTEP]
simp [hl]
[GOAL]
α : Type u
β : Type u_1
γ✝ : Type u_2
δ : Type u_3
ε : Type u_4
γ : Type u_5
inst✝ : Semiring γ
f : α → β → γ
n : γ
l : List α
l' : List β
⊢ sum (zipWith (fun x y => n * f x y) l l') = n * sum (zipWith f l l')
[PROOFSTEP]
induction' l with hd tl hl generalizing f n l'
[GOAL]
case nil
α : Type u
β : Type u_1
γ✝ : Type u_2
δ : Type u_3
ε : Type u_4
γ : Type u_5
inst✝ : Semiring γ
f✝ : α → β → γ
n✝ : γ
l'✝ : List β
f : α → β → γ
n : γ
l' : List β
⊢ sum (zipWith (fun x y => n * f x y) [] l') = n * sum (zipWith f [] l')
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
β : Type u_1
γ✝ : Type u_2
δ : Type u_3
ε : Type u_4
γ : Type u_5
inst✝ : Semiring γ
f✝ : α → β → γ
n✝ : γ
l'✝ : List β
hd : α
tl : List α
hl : ∀ (f : α → β → γ) (n : γ) (l' : List β), sum (zipWith (fun x y => n * f x y) tl l') = n * sum (zipWith f tl l')
f : α → β → γ
n : γ
l' : List β
⊢ sum (zipWith (fun x y => n * f x y) (hd :: tl) l') = n * sum (zipWith f (hd :: tl) l')
[PROOFSTEP]
cases' l' with hd' tl'
[GOAL]
case cons.nil
α : Type u
β : Type u_1
γ✝ : Type u_2
δ : Type u_3
ε : Type u_4
γ : Type u_5
inst✝ : Semiring γ
f✝ : α → β → γ
n✝ : γ
l' : List β
hd : α
tl : List α
hl : ∀ (f : α → β → γ) (n : γ) (l' : List β), sum (zipWith (fun x y => n * f x y) tl l') = n * sum (zipWith f tl l')
f : α → β → γ
n : γ
⊢ sum (zipWith (fun x y => n * f x y) (hd :: tl) []) = n * sum (zipWith f (hd :: tl) [])
[PROOFSTEP]
simp
[GOAL]
case cons.cons
α : Type u
β : Type u_1
γ✝ : Type u_2
δ : Type u_3
ε : Type u_4
γ : Type u_5
inst✝ : Semiring γ
f✝ : α → β → γ
n✝ : γ
l' : List β
hd : α
tl : List α
hl : ∀ (f : α → β → γ) (n : γ) (l' : List β), sum (zipWith (fun x y => n * f x y) tl l') = n * sum (zipWith f tl l')
f : α → β → γ
n : γ
hd' : β
tl' : List β
⊢ sum (zipWith (fun x y => n * f x y) (hd :: tl) (hd' :: tl')) = n * sum (zipWith f (hd :: tl) (hd' :: tl'))
[PROOFSTEP]
simp [hl, mul_add]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l' : List β
n : ℕ
⊢ take n (zipWith f l l') = zipWith f (take n l) (take n l')
[PROOFSTEP]
induction' l with hd tl hl generalizing l' n
[GOAL]
case nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l'✝ : List β
n✝ : ℕ
l' : List β
n : ℕ
⊢ take n (zipWith f [] l') = zipWith f (take n []) (take n l')
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l'✝ : List β
n✝ : ℕ
hd : α
tl : List α
hl : ∀ (l' : List β) (n : ℕ), take n (zipWith f tl l') = zipWith f (take n tl) (take n l')
l' : List β
n : ℕ
⊢ take n (zipWith f (hd :: tl) l') = zipWith f (take n (hd :: tl)) (take n l')
[PROOFSTEP]
cases l'
[GOAL]
case cons.nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l' : List β
n✝ : ℕ
hd : α
tl : List α
hl : ∀ (l' : List β) (n : ℕ), take n (zipWith f tl l') = zipWith f (take n tl) (take n l')
n : ℕ
⊢ take n (zipWith f (hd :: tl) []) = zipWith f (take n (hd :: tl)) (take n [])
[PROOFSTEP]
simp
[GOAL]
case cons.cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l' : List β
n✝ : ℕ
hd : α
tl : List α
hl : ∀ (l' : List β) (n : ℕ), take n (zipWith f tl l') = zipWith f (take n tl) (take n l')
n : ℕ
head✝ : β
tail✝ : List β
⊢ take n (zipWith f (hd :: tl) (head✝ :: tail✝)) = zipWith f (take n (hd :: tl)) (take n (head✝ :: tail✝))
[PROOFSTEP]
cases n
[GOAL]
case cons.cons.zero
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l' : List β
n : ℕ
hd : α
tl : List α
hl : ∀ (l' : List β) (n : ℕ), take n (zipWith f tl l') = zipWith f (take n tl) (take n l')
head✝ : β
tail✝ : List β
⊢ take zero (zipWith f (hd :: tl) (head✝ :: tail✝)) = zipWith f (take zero (hd :: tl)) (take zero (head✝ :: tail✝))
[PROOFSTEP]
simp
[GOAL]
case cons.cons.succ
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l' : List β
n : ℕ
hd : α
tl : List α
hl : ∀ (l' : List β) (n : ℕ), take n (zipWith f tl l') = zipWith f (take n tl) (take n l')
head✝ : β
tail✝ : List β
n✝ : ℕ
⊢ take (succ n✝) (zipWith f (hd :: tl) (head✝ :: tail✝)) =
    zipWith f (take (succ n✝) (hd :: tl)) (take (succ n✝) (head✝ :: tail✝))
[PROOFSTEP]
simp [hl]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l' : List β
n : ℕ
⊢ drop n (zipWith f l l') = zipWith f (drop n l) (drop n l')
[PROOFSTEP]
induction' l with hd tl hl generalizing l' n
[GOAL]
case nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l'✝ : List β
n✝ : ℕ
l' : List β
n : ℕ
⊢ drop n (zipWith f [] l') = zipWith f (drop n []) (drop n l')
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l'✝ : List β
n✝ : ℕ
hd : α
tl : List α
hl : ∀ (l' : List β) (n : ℕ), drop n (zipWith f tl l') = zipWith f (drop n tl) (drop n l')
l' : List β
n : ℕ
⊢ drop n (zipWith f (hd :: tl) l') = zipWith f (drop n (hd :: tl)) (drop n l')
[PROOFSTEP]
cases l'
[GOAL]
case cons.nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l' : List β
n✝ : ℕ
hd : α
tl : List α
hl : ∀ (l' : List β) (n : ℕ), drop n (zipWith f tl l') = zipWith f (drop n tl) (drop n l')
n : ℕ
⊢ drop n (zipWith f (hd :: tl) []) = zipWith f (drop n (hd :: tl)) (drop n [])
[PROOFSTEP]
simp
[GOAL]
case cons.cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l' : List β
n✝ : ℕ
hd : α
tl : List α
hl : ∀ (l' : List β) (n : ℕ), drop n (zipWith f tl l') = zipWith f (drop n tl) (drop n l')
n : ℕ
head✝ : β
tail✝ : List β
⊢ drop n (zipWith f (hd :: tl) (head✝ :: tail✝)) = zipWith f (drop n (hd :: tl)) (drop n (head✝ :: tail✝))
[PROOFSTEP]
cases n
[GOAL]
case cons.cons.zero
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l' : List β
n : ℕ
hd : α
tl : List α
hl : ∀ (l' : List β) (n : ℕ), drop n (zipWith f tl l') = zipWith f (drop n tl) (drop n l')
head✝ : β
tail✝ : List β
⊢ drop zero (zipWith f (hd :: tl) (head✝ :: tail✝)) = zipWith f (drop zero (hd :: tl)) (drop zero (head✝ :: tail✝))
[PROOFSTEP]
simp
[GOAL]
case cons.cons.succ
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l' : List β
n : ℕ
hd : α
tl : List α
hl : ∀ (l' : List β) (n : ℕ), drop n (zipWith f tl l') = zipWith f (drop n tl) (drop n l')
head✝ : β
tail✝ : List β
n✝ : ℕ
⊢ drop (succ n✝) (zipWith f (hd :: tl) (head✝ :: tail✝)) =
    zipWith f (drop (succ n✝) (hd :: tl)) (drop (succ n✝) (head✝ :: tail✝))
[PROOFSTEP]
simp [hl]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l' : List β
n : ℕ
⊢ tail (zipWith f l l') = zipWith f (tail l) (tail l')
[PROOFSTEP]
simp_rw [← drop_one, zipWith_distrib_drop]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f✝ : α → β → γ
l✝ : List α
l'✝ : List β
n : ℕ
f : α → β → γ
l la : List α
l' lb : List β
h : length l = length l'
⊢ zipWith f (l ++ la) (l' ++ lb) = zipWith f l l' ++ zipWith f la lb
[PROOFSTEP]
induction' l with hd tl hl generalizing l'
[GOAL]
case nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f✝ : α → β → γ
l✝ : List α
l'✝¹ : List β
n : ℕ
f : α → β → γ
l la : List α
l'✝ lb : List β
h✝ : length l = length l'✝
l' : List β
h : length [] = length l'
⊢ zipWith f ([] ++ la) (l' ++ lb) = zipWith f [] l' ++ zipWith f la lb
[PROOFSTEP]
have : l' = [] := eq_nil_of_length_eq_zero (by simpa using h.symm)
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f✝ : α → β → γ
l✝ : List α
l'✝¹ : List β
n : ℕ
f : α → β → γ
l la : List α
l'✝ lb : List β
h✝ : length l = length l'✝
l' : List β
h : length [] = length l'
⊢ length l' = 0
[PROOFSTEP]
simpa using h.symm
[GOAL]
case nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f✝ : α → β → γ
l✝ : List α
l'✝¹ : List β
n : ℕ
f : α → β → γ
l la : List α
l'✝ lb : List β
h✝ : length l = length l'✝
l' : List β
h : length [] = length l'
this : l' = []
⊢ zipWith f ([] ++ la) (l' ++ lb) = zipWith f [] l' ++ zipWith f la lb
[PROOFSTEP]
simp [this]
[GOAL]
case cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f✝ : α → β → γ
l✝ : List α
l'✝¹ : List β
n : ℕ
f : α → β → γ
l la : List α
l'✝ lb : List β
h✝ : length l = length l'✝
hd : α
tl : List α
hl : ∀ (l' : List β), length tl = length l' → zipWith f (tl ++ la) (l' ++ lb) = zipWith f tl l' ++ zipWith f la lb
l' : List β
h : length (hd :: tl) = length l'
⊢ zipWith f (hd :: tl ++ la) (l' ++ lb) = zipWith f (hd :: tl) l' ++ zipWith f la lb
[PROOFSTEP]
cases l'
[GOAL]
case cons.nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f✝ : α → β → γ
l✝ : List α
l'✝ : List β
n : ℕ
f : α → β → γ
l la : List α
l' lb : List β
h✝ : length l = length l'
hd : α
tl : List α
hl : ∀ (l' : List β), length tl = length l' → zipWith f (tl ++ la) (l' ++ lb) = zipWith f tl l' ++ zipWith f la lb
h : length (hd :: tl) = length []
⊢ zipWith f (hd :: tl ++ la) ([] ++ lb) = zipWith f (hd :: tl) [] ++ zipWith f la lb
[PROOFSTEP]
simp at h
[GOAL]
case cons.cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f✝ : α → β → γ
l✝ : List α
l'✝ : List β
n : ℕ
f : α → β → γ
l la : List α
l' lb : List β
h✝ : length l = length l'
hd : α
tl : List α
hl : ∀ (l' : List β), length tl = length l' → zipWith f (tl ++ la) (l' ++ lb) = zipWith f tl l' ++ zipWith f la lb
head✝ : β
tail✝ : List β
h : length (hd :: tl) = length (head✝ :: tail✝)
⊢ zipWith f (hd :: tl ++ la) (head✝ :: tail✝ ++ lb) = zipWith f (hd :: tl) (head✝ :: tail✝) ++ zipWith f la lb
[PROOFSTEP]
simp only [add_left_inj, length] at h
[GOAL]
case cons.cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f✝ : α → β → γ
l✝ : List α
l'✝ : List β
n : ℕ
f : α → β → γ
l la : List α
l' lb : List β
h✝ : length l = length l'
hd : α
tl : List α
hl : ∀ (l' : List β), length tl = length l' → zipWith f (tl ++ la) (l' ++ lb) = zipWith f tl l' ++ zipWith f la lb
head✝ : β
tail✝ : List β
h : length tl = length tail✝
⊢ zipWith f (hd :: tl ++ la) (head✝ :: tail✝ ++ lb) = zipWith f (hd :: tl) (head✝ :: tail✝) ++ zipWith f la lb
[PROOFSTEP]
simp [hl _ h]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : length l = length l'
⊢ reverse (zipWith f l l') = zipWith f (reverse l) (reverse l')
[PROOFSTEP]
induction' l with hd tl hl generalizing l'
[GOAL]
case nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l'✝ : List β
n : ℕ
h✝ : length l = length l'✝
l' : List β
h : length [] = length l'
⊢ reverse (zipWith f [] l') = zipWith f (reverse []) (reverse l')
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l'✝ : List β
n : ℕ
h✝ : length l = length l'✝
hd : α
tl : List α
hl : ∀ (l' : List β), length tl = length l' → reverse (zipWith f tl l') = zipWith f (reverse tl) (reverse l')
l' : List β
h : length (hd :: tl) = length l'
⊢ reverse (zipWith f (hd :: tl) l') = zipWith f (reverse (hd :: tl)) (reverse l')
[PROOFSTEP]
cases' l' with hd' tl'
[GOAL]
case cons.nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l' : List β
n : ℕ
h✝ : length l = length l'
hd : α
tl : List α
hl : ∀ (l' : List β), length tl = length l' → reverse (zipWith f tl l') = zipWith f (reverse tl) (reverse l')
h : length (hd :: tl) = length []
⊢ reverse (zipWith f (hd :: tl) []) = zipWith f (reverse (hd :: tl)) (reverse [])
[PROOFSTEP]
simp
[GOAL]
case cons.cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l' : List β
n : ℕ
h✝ : length l = length l'
hd : α
tl : List α
hl : ∀ (l' : List β), length tl = length l' → reverse (zipWith f tl l') = zipWith f (reverse tl) (reverse l')
hd' : β
tl' : List β
h : length (hd :: tl) = length (hd' :: tl')
⊢ reverse (zipWith f (hd :: tl) (hd' :: tl')) = zipWith f (reverse (hd :: tl)) (reverse (hd' :: tl'))
[PROOFSTEP]
simp only [add_left_inj, length] at h
[GOAL]
case cons.cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l' : List β
n : ℕ
h✝ : length l = length l'
hd : α
tl : List α
hl : ∀ (l' : List β), length tl = length l' → reverse (zipWith f tl l') = zipWith f (reverse tl) (reverse l')
hd' : β
tl' : List β
h : length tl = length tl'
⊢ reverse (zipWith f (hd :: tl) (hd' :: tl')) = zipWith f (reverse (hd :: tl)) (reverse (hd' :: tl'))
[PROOFSTEP]
have : tl.reverse.length = tl'.reverse.length := by simp [h]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l' : List β
n : ℕ
h✝ : length l = length l'
hd : α
tl : List α
hl : ∀ (l' : List β), length tl = length l' → reverse (zipWith f tl l') = zipWith f (reverse tl) (reverse l')
hd' : β
tl' : List β
h : length tl = length tl'
⊢ length (reverse tl) = length (reverse tl')
[PROOFSTEP]
simp [h]
[GOAL]
case cons.cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → β → γ
l : List α
l' : List β
n : ℕ
h✝ : length l = length l'
hd : α
tl : List α
hl : ∀ (l' : List β), length tl = length l' → reverse (zipWith f tl l') = zipWith f (reverse tl) (reverse l')
hd' : β
tl' : List β
h : length tl = length tl'
this : length (reverse tl) = length (reverse tl')
⊢ reverse (zipWith f (hd :: tl) (hd' :: tl')) = zipWith f (reverse (hd :: tl)) (reverse (hd' :: tl'))
[PROOFSTEP]
simp [hl _ h, zipWith_append _ _ _ _ _ this]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
inst✝ : CommMonoid α
ys : List α
⊢ prod [] * prod ys =
    prod (zipWith (fun x x_1 => x * x_1) [] ys) * prod (drop (length ys) []) * prod (drop (length []) ys)
[PROOFSTEP]
simp [Nat.zero_le]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
inst✝ : CommMonoid α
xs : List α
⊢ prod xs * prod [] =
    prod (zipWith (fun x x_1 => x * x_1) xs []) * prod (drop (length []) xs) * prod (drop (length xs) [])
[PROOFSTEP]
simp [Nat.zero_le]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
inst✝ : CommMonoid α
x : α
xs : List α
y : α
ys : List α
⊢ prod (x :: xs) * prod (y :: ys) =
    prod (zipWith (fun x x_1 => x * x_1) (x :: xs) (y :: ys)) * prod (drop (length (y :: ys)) (x :: xs)) *
      prod (drop (length (x :: xs)) (y :: ys))
[PROOFSTEP]
simp only [drop, length, zipWith_cons_cons, prod_cons]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
inst✝ : CommMonoid α
x : α
xs : List α
y : α
ys : List α
⊢ x * prod xs * (y * prod ys) =
    x * y * prod (zipWith (fun x x_1 => x * x_1) xs ys) * prod (drop (Nat.add (length ys) 0) xs) *
      prod (drop (Nat.add (length xs) 0) ys)
[PROOFSTEP]
conv =>
  lhs; rw [mul_assoc]; right; rw [mul_comm, mul_assoc]; right
  rw [mul_comm, prod_mul_prod_eq_prod_zipWith_mul_prod_drop xs ys]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
inst✝ : CommMonoid α
x : α
xs : List α
y : α
ys : List α
| x * prod xs * (y * prod ys) =
    x * y * prod (zipWith (fun x x_1 => x * x_1) xs ys) * prod (drop (Nat.add (length ys) 0) xs) *
      prod (drop (Nat.add (length xs) 0) ys)
[PROOFSTEP]
  lhs; rw [mul_assoc]; right; rw [mul_comm, mul_assoc]; right
  rw [mul_comm, prod_mul_prod_eq_prod_zipWith_mul_prod_drop xs ys]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
inst✝ : CommMonoid α
x : α
xs : List α
y : α
ys : List α
| x * prod xs * (y * prod ys) =
    x * y * prod (zipWith (fun x x_1 => x * x_1) xs ys) * prod (drop (Nat.add (length ys) 0) xs) *
      prod (drop (Nat.add (length xs) 0) ys)
[PROOFSTEP]
  lhs; rw [mul_assoc]; right; rw [mul_comm, mul_assoc]; right
  rw [mul_comm, prod_mul_prod_eq_prod_zipWith_mul_prod_drop xs ys]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
inst✝ : CommMonoid α
x : α
xs : List α
y : α
ys : List α
| x * prod xs * (y * prod ys) =
    x * y * prod (zipWith (fun x x_1 => x * x_1) xs ys) * prod (drop (Nat.add (length ys) 0) xs) *
      prod (drop (Nat.add (length xs) 0) ys)
[PROOFSTEP]
lhs
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
inst✝ : CommMonoid α
x : α
xs : List α
y : α
ys : List α
| x * prod xs * (y * prod ys)
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
inst✝ : CommMonoid α
x : α
xs : List α
y : α
ys : List α
| x * (prod xs * (y * prod ys))
[PROOFSTEP]
right
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
inst✝ : CommMonoid α
x : α
xs : List α
y : α
ys : List α
| prod xs * (y * prod ys)
[PROOFSTEP]
rw [mul_comm, mul_assoc]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
inst✝ : CommMonoid α
x : α
xs : List α
y : α
ys : List α
| y * (prod ys * prod xs)
[PROOFSTEP]
right
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
inst✝ : CommMonoid α
x : α
xs : List α
y : α
ys : List α
| prod ys * prod xs
[PROOFSTEP]
rw [mul_comm, prod_mul_prod_eq_prod_zipWith_mul_prod_drop xs ys]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
inst✝ : CommMonoid α
x : α
xs : List α
y : α
ys : List α
⊢ x * (y * (prod (zipWith (fun x x_1 => x * x_1) xs ys) * prod (drop (length ys) xs) * prod (drop (length xs) ys))) =
    x * y * prod (zipWith (fun x x_1 => x * x_1) xs ys) * prod (drop (Nat.add (length ys) 0) xs) *
      prod (drop (Nat.add (length xs) 0) ys)
[PROOFSTEP]
simp only [add_eq, add_zero]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
inst✝ : CommMonoid α
x : α
xs : List α
y : α
ys : List α
⊢ x * (y * (prod (zipWith (fun x x_1 => x * x_1) xs ys) * prod (drop (length ys) xs) * prod (drop (length xs) ys))) =
    x * y * prod (zipWith (fun x x_1 => x * x_1) xs ys) * prod (drop (length ys) xs) * prod (drop (length xs) ys)
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
inst✝ : CommMonoid α
L L' : List α
h : length L = length L'
⊢ prod L * prod L' = prod (zipWith (fun x x_1 => x * x_1) L L')
[PROOFSTEP]
apply (prod_mul_prod_eq_prod_zipWith_mul_prod_drop L L').trans
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
inst✝ : CommMonoid α
L L' : List α
h : length L = length L'
⊢ prod (zipWith (fun x x_1 => x * x_1) L L') * prod (drop (length L') L) * prod (drop (length L) L') =
    prod (zipWith (fun x x_1 => x * x_1) L L')
[PROOFSTEP]
rw [← h, drop_length, h, drop_length, prod_nil, mul_one, mul_one]


[GOAL]
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
⊢ p ∣ prod L ↔ ∃ a, a ∈ L ∧ p ∣ a
[PROOFSTEP]
constructor
[GOAL]
case mp
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
⊢ p ∣ prod L → ∃ a, a ∈ L ∧ p ∣ a
[PROOFSTEP]
intro h
[GOAL]
case mp
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
h : p ∣ prod L
⊢ ∃ a, a ∈ L ∧ p ∣ a
[PROOFSTEP]
induction' L with L_hd L_tl L_ih
[GOAL]
case mp.nil
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
h✝ : p ∣ prod L
h : p ∣ prod []
⊢ ∃ a, a ∈ [] ∧ p ∣ a
[PROOFSTEP]
rw [prod_nil] at h
[GOAL]
case mp.nil
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
h✝ : p ∣ prod L
h : p ∣ 1
⊢ ∃ a, a ∈ [] ∧ p ∣ a
[PROOFSTEP]
exact absurd h pp.not_dvd_one
[GOAL]
case mp.cons
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
h✝ : p ∣ prod L
L_hd : M
L_tl : List M
L_ih : p ∣ prod L_tl → ∃ a, a ∈ L_tl ∧ p ∣ a
h : p ∣ prod (L_hd :: L_tl)
⊢ ∃ a, a ∈ L_hd :: L_tl ∧ p ∣ a
[PROOFSTEP]
rw [prod_cons] at h
[GOAL]
case mp.cons
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
h✝ : p ∣ prod L
L_hd : M
L_tl : List M
L_ih : p ∣ prod L_tl → ∃ a, a ∈ L_tl ∧ p ∣ a
h : p ∣ L_hd * prod L_tl
⊢ ∃ a, a ∈ L_hd :: L_tl ∧ p ∣ a
[PROOFSTEP]
cases' pp.dvd_or_dvd h with hd hd
[GOAL]
case mp.cons.inl
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
h✝ : p ∣ prod L
L_hd : M
L_tl : List M
L_ih : p ∣ prod L_tl → ∃ a, a ∈ L_tl ∧ p ∣ a
h : p ∣ L_hd * prod L_tl
hd : p ∣ L_hd
⊢ ∃ a, a ∈ L_hd :: L_tl ∧ p ∣ a
[PROOFSTEP]
exact ⟨L_hd, mem_cons_self L_hd L_tl, hd⟩
[GOAL]
case mp.cons.inr
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
h✝ : p ∣ prod L
L_hd : M
L_tl : List M
L_ih : p ∣ prod L_tl → ∃ a, a ∈ L_tl ∧ p ∣ a
h : p ∣ L_hd * prod L_tl
hd : p ∣ prod L_tl
⊢ ∃ a, a ∈ L_hd :: L_tl ∧ p ∣ a
[PROOFSTEP]
obtain ⟨x, hx1, hx2⟩ := L_ih hd
[GOAL]
case mp.cons.inr.intro.intro
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
h✝ : p ∣ prod L
L_hd : M
L_tl : List M
L_ih : p ∣ prod L_tl → ∃ a, a ∈ L_tl ∧ p ∣ a
h : p ∣ L_hd * prod L_tl
hd : p ∣ prod L_tl
x : M
hx1 : x ∈ L_tl
hx2 : p ∣ x
⊢ ∃ a, a ∈ L_hd :: L_tl ∧ p ∣ a
[PROOFSTEP]
exact ⟨x, mem_cons_of_mem L_hd hx1, hx2⟩
[GOAL]
case mpr
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
⊢ (∃ a, a ∈ L ∧ p ∣ a) → p ∣ prod L
[PROOFSTEP]
exact fun ⟨a, ha1, ha2⟩ => dvd_trans ha2 (dvd_prod ha1)
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
p : M
hp : Prime p
L : List M
hL : ∀ (q : M), q ∈ L → Prime q
hpL : p ∣ prod L
⊢ p ∈ L
[PROOFSTEP]
obtain ⟨x, hx1, hx2⟩ := hp.dvd_prod_iff.mp hpL
[GOAL]
case intro.intro
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
p : M
hp : Prime p
L : List M
hL : ∀ (q : M), q ∈ L → Prime q
hpL : p ∣ prod L
x : M
hx1 : x ∈ L
hx2 : p ∣ x
⊢ p ∈ L
[PROOFSTEP]
rwa [(prime_dvd_prime_iff_eq hp (hL x hx1)).mp hx2]
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
⊢ a :: l₁ ~ b :: l₂
[PROOFSTEP]
classical
have hl₁' : ∀ p ∈ l₁, Prime p := fun p hp => hl₁ p (mem_cons_of_mem _ hp)
have hl₂' : ∀ p ∈ (b :: l₂).erase a, Prime p := fun p hp => hl₂ p (mem_of_mem_erase hp)
have ha : a ∈ b :: l₂ :=
  mem_list_primes_of_dvd_prod (hl₁ a (mem_cons_self _ _)) hl₂ (h ▸ by rw [prod_cons]; exact dvd_mul_right _ _)
have hb : b :: l₂ ~ a :: (b :: l₂).erase a := perm_cons_erase ha
have hl : prod l₁ = prod ((b :: l₂).erase a) :=
  (mul_right_inj' (hl₁ a (mem_cons_self _ _)).ne_zero).1 <| by rwa [← prod_cons, ← prod_cons, ← hb.prod_eq]
exact Perm.trans ((perm_of_prod_eq_prod hl hl₁' hl₂').cons _) hb.symm
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
⊢ a :: l₁ ~ b :: l₂
[PROOFSTEP]
have hl₁' : ∀ p ∈ l₁, Prime p := fun p hp => hl₁ p (mem_cons_of_mem _ hp)
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
⊢ a :: l₁ ~ b :: l₂
[PROOFSTEP]
have hl₂' : ∀ p ∈ (b :: l₂).erase a, Prime p := fun p hp => hl₂ p (mem_of_mem_erase hp)
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ List.erase (b :: l₂) a → Prime p
⊢ a :: l₁ ~ b :: l₂
[PROOFSTEP]
have ha : a ∈ b :: l₂ :=
  mem_list_primes_of_dvd_prod (hl₁ a (mem_cons_self _ _)) hl₂ (h ▸ by rw [prod_cons]; exact dvd_mul_right _ _)
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ List.erase (b :: l₂) a → Prime p
⊢ a ∣ prod (a :: l₁)
[PROOFSTEP]
rw [prod_cons]
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ List.erase (b :: l₂) a → Prime p
⊢ a ∣ a * prod l₁
[PROOFSTEP]
exact dvd_mul_right _ _
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ List.erase (b :: l₂) a → Prime p
ha : a ∈ b :: l₂
⊢ a :: l₁ ~ b :: l₂
[PROOFSTEP]
have hb : b :: l₂ ~ a :: (b :: l₂).erase a := perm_cons_erase ha
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ List.erase (b :: l₂) a → Prime p
ha : a ∈ b :: l₂
hb : b :: l₂ ~ a :: List.erase (b :: l₂) a
⊢ a :: l₁ ~ b :: l₂
[PROOFSTEP]
have hl : prod l₁ = prod ((b :: l₂).erase a) :=
  (mul_right_inj' (hl₁ a (mem_cons_self _ _)).ne_zero).1 <| by rwa [← prod_cons, ← prod_cons, ← hb.prod_eq]
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ List.erase (b :: l₂) a → Prime p
ha : a ∈ b :: l₂
hb : b :: l₂ ~ a :: List.erase (b :: l₂) a
⊢ a * prod l₁ = a * prod (List.erase (b :: l₂) a)
[PROOFSTEP]
rwa [← prod_cons, ← prod_cons, ← hb.prod_eq]
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ List.erase (b :: l₂) a → Prime p
ha : a ∈ b :: l₂
hb : b :: l₂ ~ a :: List.erase (b :: l₂) a
hl : prod l₁ = prod (List.erase (b :: l₂) a)
⊢ a :: l₁ ~ b :: l₂
[PROOFSTEP]
exact Perm.trans ((perm_of_prod_eq_prod hl hl₁' hl₂').cons _) hb.symm