[GOAL]
α : Type u_1
l : List α
x : α
h : x ∈+ l
⊢ x ∈ l
[PROOFSTEP]
induction' h with l' _ y l' _ hm
[GOAL]
case cons_mem
α : Type u_1
l : List α
x : α
l' : List α
a✝ : x ∈ l'
⊢ x ∈ x :: l'
[PROOFSTEP]
exact mem_cons_self _ _
[GOAL]
case cons_duplicate
α : Type u_1
l : List α
x y : α
l' : List α
a✝ : x ∈+ l'
hm : x ∈ l'
⊢ x ∈ y :: l'
[PROOFSTEP]
exact mem_cons_of_mem _ hm
[GOAL]
α : Type u_1
l : List α
x : α
h : x ∈+ x :: l
⊢ x ∈ l
[PROOFSTEP]
cases' h with _ h _ _ h
[GOAL]
case cons_mem
α : Type u_1
l : List α
x : α
h : x ∈ l
⊢ x ∈ l
[PROOFSTEP]
exact h
[GOAL]
case cons_duplicate
α : Type u_1
l : List α
x : α
h : x ∈+ l
⊢ x ∈ l
[PROOFSTEP]
exact h.mem
[GOAL]
α : Type u_1
l : List α
x : α
h : x ∈+ l
y : α
⊢ l ≠ [y]
[PROOFSTEP]
induction' h with l' h z l' h _
[GOAL]
case cons_mem
α : Type u_1
l : List α
x y : α
l' : List α
h : x ∈ l'
⊢ x :: l' ≠ [y]
[PROOFSTEP]
simp [ne_nil_of_mem h]
[GOAL]
case cons_duplicate
α : Type u_1
l : List α
x y z : α
l' : List α
h : x ∈+ l'
a_ih✝ : l' ≠ [y]
⊢ z :: l' ≠ [y]
[PROOFSTEP]
simp [ne_nil_of_mem h.mem]
[GOAL]
α : Type u_1
l : List α
x y : α
⊢ x ∈+ y :: l ↔ y = x ∧ x ∈ l ∨ x ∈+ l
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
α : Type u_1
l : List α
x y : α
h : x ∈+ y :: l
⊢ y = x ∧ x ∈ l ∨ x ∈+ l
[PROOFSTEP]
cases' h with _ hm _ _ hm
[GOAL]
case refine'_1.cons_mem
α : Type u_1
l : List α
x : α
hm : x ∈ l
⊢ x = x ∧ x ∈ l ∨ x ∈+ l
[PROOFSTEP]
exact Or.inl ⟨rfl, hm⟩
[GOAL]
case refine'_1.cons_duplicate
α : Type u_1
l : List α
x y : α
hm : x ∈+ l
⊢ y = x ∧ x ∈ l ∨ x ∈+ l
[PROOFSTEP]
exact Or.inr hm
[GOAL]
case refine'_2
α : Type u_1
l : List α
x y : α
h : y = x ∧ x ∈ l ∨ x ∈+ l
⊢ x ∈+ y :: l
[PROOFSTEP]
rcases h with (⟨rfl | h⟩ | h)
[GOAL]
case refine'_2.inl.intro.refl
α : Type u_1
l : List α
x : α
right✝ : x ∈ l
⊢ x ∈+ x :: l
[PROOFSTEP]
simpa
[GOAL]
case refine'_2.inr
α : Type u_1
l : List α
x y : α
h : x ∈+ l
⊢ x ∈+ y :: l
[PROOFSTEP]
exact h.cons_duplicate
[GOAL]
α : Type u_1
l : List α
x y : α
h : x ∈+ y :: l
hx : x ≠ y
⊢ x ∈+ l
[PROOFSTEP]
simpa [duplicate_cons_iff, hx.symm] using h
[GOAL]
α : Type u_1
l : List α
x y : α
hne : x ≠ y
⊢ x ∈+ y :: l ↔ x ∈+ l
[PROOFSTEP]
simp [duplicate_cons_iff, hne.symm]
[GOAL]
α : Type u_1
l : List α
x : α
l' : List α
hx : x ∈+ l
h : l <+ l'
⊢ x ∈+ l'
[PROOFSTEP]
induction' h with l₁ l₂ y _ IH l₁ l₂ y h IH
[GOAL]
case slnil
α : Type u_1
l : List α
x : α
l' : List α
hx✝ : x ∈+ l
hx : x ∈+ []
⊢ x ∈+ []
[PROOFSTEP]
exact hx
[GOAL]
case cons
α : Type u_1
l : List α
x : α
l' : List α
hx✝ : x ∈+ l
l₁ l₂ : List α
y : α
a✝ : l₁ <+ l₂
IH : x ∈+ l₁ → x ∈+ l₂
hx : x ∈+ l₁
⊢ x ∈+ y :: l₂
[PROOFSTEP]
exact (IH hx).duplicate_cons _
[GOAL]
case cons₂
α : Type u_1
l : List α
x : α
l' : List α
hx✝ : x ∈+ l
l₁ l₂ : List α
y : α
h : l₁ <+ l₂
IH : x ∈+ l₁ → x ∈+ l₂
hx : x ∈+ y :: l₁
⊢ x ∈+ y :: l₂
[PROOFSTEP]
rw [duplicate_cons_iff] at hx ⊢
[GOAL]
case cons₂
α : Type u_1
l : List α
x : α
l' : List α
hx✝ : x ∈+ l
l₁ l₂ : List α
y : α
h : l₁ <+ l₂
IH : x ∈+ l₁ → x ∈+ l₂
hx : y = x ∧ x ∈ l₁ ∨ x ∈+ l₁
⊢ y = x ∧ x ∈ l₂ ∨ x ∈+ l₂
[PROOFSTEP]
rcases hx with (⟨rfl, hx⟩ | hx)
[GOAL]
case cons₂.inl.intro
α : Type u_1
l l' l₁ l₂ : List α
y : α
h : l₁ <+ l₂
hx✝ : y ∈+ l
IH : y ∈+ l₁ → y ∈+ l₂
hx : y ∈ l₁
⊢ y = y ∧ y ∈ l₂ ∨ y ∈+ l₂
[PROOFSTEP]
simp [h.subset hx]
[GOAL]
case cons₂.inr
α : Type u_1
l : List α
x : α
l' : List α
hx✝ : x ∈+ l
l₁ l₂ : List α
y : α
h : l₁ <+ l₂
IH : x ∈+ l₁ → x ∈+ l₂
hx : x ∈+ l₁
⊢ y = x ∧ x ∈ l₂ ∨ x ∈+ l₂
[PROOFSTEP]
simp [IH hx]
[GOAL]
α : Type u_1
l : List α
x : α
⊢ x ∈+ l ↔ [x, x] <+ l
[PROOFSTEP]
induction' l with y l IH
[GOAL]
case nil
α : Type u_1
l : List α
x : α
⊢ x ∈+ [] ↔ [x, x] <+ []
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
⊢ x ∈+ y :: l ↔ [x, x] <+ y :: l
[PROOFSTEP]
by_cases hx : x = y
[GOAL]
case pos
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : x = y
⊢ x ∈+ y :: l ↔ [x, x] <+ y :: l
[PROOFSTEP]
simp [hx, cons_sublist_cons_iff, singleton_sublist]
[GOAL]
case neg
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
⊢ x ∈+ y :: l ↔ [x, x] <+ y :: l
[PROOFSTEP]
rw [duplicate_cons_iff_of_ne hx, IH]
[GOAL]
case neg
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
⊢ [x, x] <+ l ↔ [x, x] <+ y :: l
[PROOFSTEP]
refine' ⟨sublist_cons_of_sublist y, fun h => _⟩
[GOAL]
case neg
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
h : [x, x] <+ y :: l
⊢ [x, x] <+ l
[PROOFSTEP]
cases h
[GOAL]
case neg.cons
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
a✝ : [x, x] <+ l
⊢ [x, x] <+ l
[PROOFSTEP]
assumption
[GOAL]
case neg.cons₂
α : Type u_1
l✝ : List α
x : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = x
a✝ : [x] <+ l
⊢ [x, x] <+ l
[PROOFSTEP]
contradiction
[GOAL]
α : Type u_1
l : List α
x : α
⊢ Nodup l ↔ ∀ (x : α), ¬x ∈+ l
[PROOFSTEP]
simp_rw [nodup_iff_sublist, duplicate_iff_sublist]
[GOAL]
α : Type u_1
l : List α
x : α
⊢ (∃ x, x ∈+ l) ↔ ¬Nodup l
[PROOFSTEP]
simp [nodup_iff_forall_not_duplicate]
[GOAL]
α : Type u_1
l : List α
x : α
inst✝ : DecidableEq α
⊢ x ∈+ l ↔ 2 ≤ count x l
[PROOFSTEP]
simp [duplicate_iff_sublist, le_count_iff_replicate_sublist]
[GOAL]
α : Type u_1
l✝ : List α
x✝ : α
inst✝ : DecidableEq α
x y : α
l : List α
h : ¬x ∈+ l
hx : ¬(y = x ∧ x ∈ l)
⊢ ¬x ∈+ y :: l
[PROOFSTEP]
simpa [duplicate_cons_iff, h] using hx


[GOAL]
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
h : R b a
⊢ destutter' R b (a :: l) = b :: destutter' R a l
[PROOFSTEP]
rw [destutter', if_pos h]
[GOAL]
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
h : ¬R b a
⊢ destutter' R b (a :: l) = destutter' R b l
[PROOFSTEP]
rw [destutter', if_neg h]
[GOAL]
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
⊢ destutter' R a [b] = if R a b then [a, b] else [a]
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
h : R a b
⊢ destutter' R a [b] = [a, b]
[PROOFSTEP]
simp! [h]
[GOAL]
case neg
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
h : ¬R a b
⊢ destutter' R a [b] = [a]
[PROOFSTEP]
simp! [h]
[GOAL]
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b a : α
⊢ destutter' R a l <+ a :: l
[PROOFSTEP]
induction' l with b l hl generalizing a
[GOAL]
case nil
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝¹ b a✝ a : α
⊢ destutter' R a [] <+ [a]
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝¹ b✝ a✝ b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
⊢ destutter' R a (b :: l) <+ a :: b :: l
[PROOFSTEP]
rw [destutter']
[GOAL]
case cons
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝¹ b✝ a✝ b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
⊢ (if R a b then a :: destutter' R b l else destutter' R a l) <+ a :: b :: l
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝¹ b✝ a✝ b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
h✝ : R a b
⊢ a :: destutter' R b l <+ a :: b :: l
[PROOFSTEP]
exact Sublist.cons₂ a (hl b)
[GOAL]
case neg
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝¹ b✝ a✝ b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
h✝ : ¬R a b
⊢ destutter' R a l <+ a :: b :: l
[PROOFSTEP]
exact (hl a).trans ((l.sublist_cons b).cons_cons a)
[GOAL]
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b a : α
⊢ a ∈ destutter' R a l
[PROOFSTEP]
induction' l with b l hl
[GOAL]
case nil
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b a : α
⊢ a ∈ destutter' R a []
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b✝ a b : α
l : List α
hl : a ∈ destutter' R a l
⊢ a ∈ destutter' R a (b :: l)
[PROOFSTEP]
rw [destutter']
[GOAL]
case cons
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b✝ a b : α
l : List α
hl : a ∈ destutter' R a l
⊢ a ∈ if R a b then a :: destutter' R b l else destutter' R a l
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b✝ a b : α
l : List α
hl : a ∈ destutter' R a l
h✝ : R a b
⊢ a ∈ a :: destutter' R b l
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b✝ a b : α
l : List α
hl : a ∈ destutter' R a l
h✝ : ¬R a b
⊢ a ∈ destutter' R a l
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b✝ c : α
l : List α
a b : α
h : R a b
⊢ Chain R a (destutter' R b (c :: l))
[PROOFSTEP]
rw [destutter']
[GOAL]
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b✝ c : α
l : List α
a b : α
h : R a b
⊢ Chain R a (if R b c then b :: destutter' R c l else destutter' R b l)
[PROOFSTEP]
split_ifs with hbc
[GOAL]
case pos
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b✝ c : α
l : List α
a b : α
h : R a b
hbc : R b c
⊢ Chain R a (b :: destutter' R c l)
[PROOFSTEP]
rw [chain_cons]
[GOAL]
case pos
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b✝ c : α
l : List α
a b : α
h : R a b
hbc : R b c
⊢ R a b ∧ Chain R b (destutter' R c l)
[PROOFSTEP]
exact ⟨h, destutter'_is_chain l hbc⟩
[GOAL]
case neg
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b✝ c : α
l : List α
a b : α
h : R a b
hbc : ¬R b c
⊢ Chain R a (destutter' R b l)
[PROOFSTEP]
exact destutter'_is_chain l h
[GOAL]
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b a : α
⊢ Chain' R (destutter' R a l)
[PROOFSTEP]
induction' l with b l hl generalizing a
[GOAL]
case nil
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝¹ b a✝ a : α
⊢ Chain' R (destutter' R a [])
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝¹ b✝ a✝ b : α
l : List α
hl : ∀ (a : α), Chain' R (destutter' R a l)
a : α
⊢ Chain' R (destutter' R a (b :: l))
[PROOFSTEP]
rw [destutter']
[GOAL]
case cons
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝¹ b✝ a✝ b : α
l : List α
hl : ∀ (a : α), Chain' R (destutter' R a l)
a : α
⊢ Chain' R (if R a b then a :: destutter' R b l else destutter' R a l)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝¹ b✝ a✝ b : α
l : List α
hl : ∀ (a : α), Chain' R (destutter' R a l)
a : α
h : R a b
⊢ Chain' R (a :: destutter' R b l)
[PROOFSTEP]
exact destutter'_is_chain R l h
[GOAL]
case neg
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝¹ b✝ a✝ b : α
l : List α
hl : ∀ (a : α), Chain' R (destutter' R a l)
a : α
h : ¬R a b
⊢ Chain' R (destutter' R a l)
[PROOFSTEP]
exact hl a
[GOAL]
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
h : Chain R a l
⊢ destutter' R a l = a :: l
[PROOFSTEP]
induction' l with b l hb generalizing a
[GOAL]
case nil
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b : α
h✝ : Chain R a✝ l
a : α
h : Chain R a []
⊢ destutter' R a [] = [a]
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b✝ : α
h✝ : Chain R a✝ l✝
b : α
l : List α
hb : ∀ {a : α}, Chain R a l → destutter' R a l = a :: l
a : α
h : Chain R a (b :: l)
⊢ destutter' R a (b :: l) = a :: b :: l
[PROOFSTEP]
obtain ⟨h, hc⟩ := chain_cons.mp h
[GOAL]
case cons.intro
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b✝ : α
h✝¹ : Chain R a✝ l✝
b : α
l : List α
hb : ∀ {a : α}, Chain R a l → destutter' R a l = a :: l
a : α
h✝ : Chain R a (b :: l)
h : R a b
hc : Chain R b l
⊢ destutter' R a (b :: l) = a :: b :: l
[PROOFSTEP]
rw [l.destutter'_cons_pos h, hb hc]
[GOAL]
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b a : α
h : destutter' R a l = a :: l
⊢ Chain R a l
[PROOFSTEP]
suffices Chain' R (a :: l) by assumption
[GOAL]
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b a : α
h : destutter' R a l = a :: l
this : Chain' R (a :: l)
⊢ Chain R a l
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b a : α
h : destutter' R a l = a :: l
⊢ Chain' R (a :: l)
[PROOFSTEP]
rw [← h]
[GOAL]
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b a : α
h : destutter' R a l = a :: l
⊢ Chain' R (destutter' R a l)
[PROOFSTEP]
exact l.destutter'_is_chain' R a
[GOAL]
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
⊢ destutter R [] = [] ↔ Chain' R []
[PROOFSTEP]
simp


[GOAL]
α : Type u_1
β : Type u_2
l✝ l : List α
p : Palindrome l
⊢ reverse l = l
[PROOFSTEP]
induction p
[GOAL]
case nil
α : Type u_1
β : Type u_2
l✝ l : List α
⊢ reverse [] = []
[PROOFSTEP]
try (exact rfl)
[GOAL]
case nil
α : Type u_1
β : Type u_2
l✝ l : List α
⊢ reverse [] = []
[PROOFSTEP]
exact rfl
[GOAL]
case singleton
α : Type u_1
β : Type u_2
l✝ l : List α
x✝ : α
⊢ reverse [x✝] = [x✝]
[PROOFSTEP]
try (exact rfl)
[GOAL]
case singleton
α : Type u_1
β : Type u_2
l✝ l : List α
x✝ : α
⊢ reverse [x✝] = [x✝]
[PROOFSTEP]
exact rfl
[GOAL]
case cons_concat
α : Type u_1
β : Type u_2
l✝¹ l : List α
x✝ : α
l✝ : List α
a✝ : Palindrome l✝
a_ih✝ : reverse l✝ = l✝
⊢ reverse (x✝ :: (l✝ ++ [x✝])) = x✝ :: (l✝ ++ [x✝])
[PROOFSTEP]
try (exact rfl)
[GOAL]
case cons_concat
α : Type u_1
β : Type u_2
l✝¹ l : List α
x✝ : α
l✝ : List α
a✝ : Palindrome l✝
a_ih✝ : reverse l✝ = l✝
⊢ reverse (x✝ :: (l✝ ++ [x✝])) = x✝ :: (l✝ ++ [x✝])
[PROOFSTEP]
exact rfl
[GOAL]
case cons_concat
α : Type u_1
β : Type u_2
l✝¹ l : List α
x✝ : α
l✝ : List α
a✝ : Palindrome l✝
a_ih✝ : reverse l✝ = l✝
⊢ reverse (x✝ :: (l✝ ++ [x✝])) = x✝ :: (l✝ ++ [x✝])
[PROOFSTEP]
simp
[GOAL]
case cons_concat
α : Type u_1
β : Type u_2
l✝¹ l : List α
x✝ : α
l✝ : List α
a✝ : Palindrome l✝
a_ih✝ : reverse l✝ = l✝
⊢ reverse l✝ = l✝
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
l✝ l : List α
⊢ reverse l = l → Palindrome l
[PROOFSTEP]
refine' bidirectionalRecOn l (fun _ => Palindrome.nil) (fun a _ => Palindrome.singleton a) _
[GOAL]
α : Type u_1
β : Type u_2
l✝ l : List α
⊢ ∀ (a : α) (l : List α) (b : α),
    (reverse l = l → Palindrome l) → reverse (a :: (l ++ [b])) = a :: (l ++ [b]) → Palindrome (a :: (l ++ [b]))
[PROOFSTEP]
intro x l y hp hr
[GOAL]
α : Type u_1
β : Type u_2
l✝¹ l✝ : List α
x : α
l : List α
y : α
hp : reverse l = l → Palindrome l
hr : reverse (x :: (l ++ [y])) = x :: (l ++ [y])
⊢ Palindrome (x :: (l ++ [y]))
[PROOFSTEP]
rw [reverse_cons, reverse_append] at hr
[GOAL]
α : Type u_1
β : Type u_2
l✝¹ l✝ : List α
x : α
l : List α
y : α
hp : reverse l = l → Palindrome l
hr : reverse [y] ++ reverse l ++ [x] = x :: (l ++ [y])
⊢ Palindrome (x :: (l ++ [y]))
[PROOFSTEP]
rw [head_eq_of_cons_eq hr]
[GOAL]
α : Type u_1
β : Type u_2
l✝¹ l✝ : List α
x : α
l : List α
y : α
hp : reverse l = l → Palindrome l
hr : reverse [y] ++ reverse l ++ [x] = x :: (l ++ [y])
⊢ Palindrome (x :: (l ++ [x]))
[PROOFSTEP]
have : Palindrome l := hp (append_inj_left' (tail_eq_of_cons_eq hr) rfl)
[GOAL]
α : Type u_1
β : Type u_2
l✝¹ l✝ : List α
x : α
l : List α
y : α
hp : reverse l = l → Palindrome l
hr : reverse [y] ++ reverse l ++ [x] = x :: (l ++ [y])
this : Palindrome l
⊢ Palindrome (x :: (l ++ [x]))
[PROOFSTEP]
exact Palindrome.cons_concat x this
[GOAL]
α : Type u_1
β : Type u_2
l✝ l : List α
⊢ Palindrome (l ++ reverse l)
[PROOFSTEP]
apply of_reverse_eq
[GOAL]
case a
α : Type u_1
β : Type u_2
l✝ l : List α
⊢ reverse (l ++ reverse l) = l ++ reverse l
[PROOFSTEP]
rw [reverse_append, reverse_reverse]
[GOAL]
α : Type u_1
β : Type u_2
l : List α
f : α → β
p : Palindrome l
⊢ reverse (map f l) = map f l
[PROOFSTEP]
rw [← map_reverse, p.reverse_eq]


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx : ¬x ∈ l
⊢ Set.InjOn (fun k => insertNth k x l) {n | n ≤ length l}
[PROOFSTEP]
induction' l with hd tl IH
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hx : ¬x ∈ []
⊢ Set.InjOn (fun k => insertNth k x []) {n | n ≤ length []}
[PROOFSTEP]
intro n hn m hm _
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hx : ¬x ∈ []
n : ℕ
hn : n ∈ {n | n ≤ length []}
m : ℕ
hm : m ∈ {n | n ≤ length []}
a✝ : (fun k => insertNth k x []) n = (fun k => insertNth k x []) m
⊢ n = m
[PROOFSTEP]
simp only [Set.mem_singleton_iff, Set.setOf_eq_eq_singleton, length, nonpos_iff_eq_zero] at hn hm
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hx : ¬x ∈ []
n m : ℕ
a✝ : (fun k => insertNth k x []) n = (fun k => insertNth k x []) m
hn : n = 0
hm : m = 0
⊢ n = m
[PROOFSTEP]
simp [hn, hm]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hd : α
tl : List α
IH : ¬x ∈ tl → Set.InjOn (fun k => insertNth k x tl) {n | n ≤ length tl}
hx : ¬x ∈ hd :: tl
⊢ Set.InjOn (fun k => insertNth k x (hd :: tl)) {n | n ≤ length (hd :: tl)}
[PROOFSTEP]
intro n hn m hm h
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hd : α
tl : List α
IH : ¬x ∈ tl → Set.InjOn (fun k => insertNth k x tl) {n | n ≤ length tl}
hx : ¬x ∈ hd :: tl
n : ℕ
hn : n ∈ {n | n ≤ length (hd :: tl)}
m : ℕ
hm : m ∈ {n | n ≤ length (hd :: tl)}
h : (fun k => insertNth k x (hd :: tl)) n = (fun k => insertNth k x (hd :: tl)) m
⊢ n = m
[PROOFSTEP]
simp only [length, Set.mem_setOf_eq] at hn hm
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hd : α
tl : List α
IH : ¬x ∈ tl → Set.InjOn (fun k => insertNth k x tl) {n | n ≤ length tl}
hx : ¬x ∈ hd :: tl
n : ℕ
hn : n ≤ length tl + 1
m : ℕ
hm : m ≤ length tl + 1
h : (fun k => insertNth k x (hd :: tl)) n = (fun k => insertNth k x (hd :: tl)) m
⊢ n = m
[PROOFSTEP]
simp only [mem_cons, not_or] at hx
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hd : α
tl : List α
IH : ¬x ∈ tl → Set.InjOn (fun k => insertNth k x tl) {n | n ≤ length tl}
n : ℕ
hn : n ≤ length tl + 1
m : ℕ
hm : m ≤ length tl + 1
h : (fun k => insertNth k x (hd :: tl)) n = (fun k => insertNth k x (hd :: tl)) m
hx : ¬x = hd ∧ ¬x ∈ tl
⊢ n = m
[PROOFSTEP]
cases n
[GOAL]
case cons.zero
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hd : α
tl : List α
IH : ¬x ∈ tl → Set.InjOn (fun k => insertNth k x tl) {n | n ≤ length tl}
m : ℕ
hm : m ≤ length tl + 1
hx : ¬x = hd ∧ ¬x ∈ tl
hn : Nat.zero ≤ length tl + 1
h : (fun k => insertNth k x (hd :: tl)) Nat.zero = (fun k => insertNth k x (hd :: tl)) m
⊢ Nat.zero = m
[PROOFSTEP]
cases m
[GOAL]
case cons.succ
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hd : α
tl : List α
IH : ¬x ∈ tl → Set.InjOn (fun k => insertNth k x tl) {n | n ≤ length tl}
m : ℕ
hm : m ≤ length tl + 1
hx : ¬x = hd ∧ ¬x ∈ tl
n✝ : ℕ
hn : Nat.succ n✝ ≤ length tl + 1
h : (fun k => insertNth k x (hd :: tl)) (Nat.succ n✝) = (fun k => insertNth k x (hd :: tl)) m
⊢ Nat.succ n✝ = m
[PROOFSTEP]
cases m
[GOAL]
case cons.zero.zero
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hd : α
tl : List α
IH : ¬x ∈ tl → Set.InjOn (fun k => insertNth k x tl) {n | n ≤ length tl}
hx : ¬x = hd ∧ ¬x ∈ tl
hn hm : Nat.zero ≤ length tl + 1
h : (fun k => insertNth k x (hd :: tl)) Nat.zero = (fun k => insertNth k x (hd :: tl)) Nat.zero
⊢ Nat.zero = Nat.zero
[PROOFSTEP]
rfl
[GOAL]
case cons.zero.succ
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hd : α
tl : List α
IH : ¬x ∈ tl → Set.InjOn (fun k => insertNth k x tl) {n | n ≤ length tl}
hx : ¬x = hd ∧ ¬x ∈ tl
hn : Nat.zero ≤ length tl + 1
n✝ : ℕ
hm : Nat.succ n✝ ≤ length tl + 1
h : (fun k => insertNth k x (hd :: tl)) Nat.zero = (fun k => insertNth k x (hd :: tl)) (Nat.succ n✝)
⊢ Nat.zero = Nat.succ n✝
[PROOFSTEP]
simp [hx.left] at h
[GOAL]
case cons.succ.zero
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hd : α
tl : List α
IH : ¬x ∈ tl → Set.InjOn (fun k => insertNth k x tl) {n | n ≤ length tl}
hx : ¬x = hd ∧ ¬x ∈ tl
n✝ : ℕ
hn : Nat.succ n✝ ≤ length tl + 1
hm : Nat.zero ≤ length tl + 1
h : (fun k => insertNth k x (hd :: tl)) (Nat.succ n✝) = (fun k => insertNth k x (hd :: tl)) Nat.zero
⊢ Nat.succ n✝ = Nat.zero
[PROOFSTEP]
simp [Ne.symm hx.left] at h
[GOAL]
case cons.succ.succ
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hd : α
tl : List α
IH : ¬x ∈ tl → Set.InjOn (fun k => insertNth k x tl) {n | n ≤ length tl}
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : Nat.succ n✝¹ ≤ length tl + 1
n✝ : ℕ
hm : Nat.succ n✝ ≤ length tl + 1
h : (fun k => insertNth k x (hd :: tl)) (Nat.succ n✝¹) = (fun k => insertNth k x (hd :: tl)) (Nat.succ n✝)
⊢ Nat.succ n✝¹ = Nat.succ n✝
[PROOFSTEP]
simp only [true_and_iff, eq_self_iff_true, insertNth_succ_cons] at h
[GOAL]
case cons.succ.succ
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hd : α
tl : List α
IH : ¬x ∈ tl → Set.InjOn (fun k => insertNth k x tl) {n | n ≤ length tl}
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : Nat.succ n✝¹ ≤ length tl + 1
n✝ : ℕ
hm : Nat.succ n✝ ≤ length tl + 1
h : hd :: insertNth n✝¹ x tl = hd :: insertNth n✝ x tl
⊢ Nat.succ n✝¹ = Nat.succ n✝
[PROOFSTEP]
rw [Nat.succ_inj']
[GOAL]
case cons.succ.succ
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hd : α
tl : List α
IH : ¬x ∈ tl → Set.InjOn (fun k => insertNth k x tl) {n | n ≤ length tl}
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : Nat.succ n✝¹ ≤ length tl + 1
n✝ : ℕ
hm : Nat.succ n✝ ≤ length tl + 1
h : hd :: insertNth n✝¹ x tl = hd :: insertNth n✝ x tl
⊢ n✝¹ = n✝
[PROOFSTEP]
refine' IH hx.right _ _ (by injection h)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hd : α
tl : List α
IH : ¬x ∈ tl → Set.InjOn (fun k => insertNth k x tl) {n | n ≤ length tl}
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : Nat.succ n✝¹ ≤ length tl + 1
n✝ : ℕ
hm : Nat.succ n✝ ≤ length tl + 1
h : hd :: insertNth n✝¹ x tl = hd :: insertNth n✝ x tl
⊢ (fun k => insertNth k x tl) n✝¹ = (fun k => insertNth k x tl) n✝
[PROOFSTEP]
injection h
[GOAL]
case cons.succ.succ.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hd : α
tl : List α
IH : ¬x ∈ tl → Set.InjOn (fun k => insertNth k x tl) {n | n ≤ length tl}
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : Nat.succ n✝¹ ≤ length tl + 1
n✝ : ℕ
hm : Nat.succ n✝ ≤ length tl + 1
h : hd :: insertNth n✝¹ x tl = hd :: insertNth n✝ x tl
⊢ n✝¹ ∈ {n | n ≤ length tl}
[PROOFSTEP]
simpa [Nat.succ_le_succ_iff] using hn
[GOAL]
case cons.succ.succ.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
x : α
hx✝ : ¬x ∈ l
hd : α
tl : List α
IH : ¬x ∈ tl → Set.InjOn (fun k => insertNth k x tl) {n | n ≤ length tl}
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : Nat.succ n✝¹ ≤ length tl + 1
n✝ : ℕ
hm : Nat.succ n✝ ≤ length tl + 1
h : hd :: insertNth n✝¹ x tl = hd :: insertNth n✝ x tl
⊢ n✝ ∈ {n | n ≤ length tl}
[PROOFSTEP]
simpa [Nat.succ_le_succ_iff] using hm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
⊢ Set.range (foldr f a) ⊆ Set.range (foldr g a)
[PROOFSTEP]
rintro _ ⟨l, rfl⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
l : List β
⊢ foldr f a l ∈ Set.range (foldr g a)
[PROOFSTEP]
induction' l with b l H
[GOAL]
case intro.nil
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
⊢ foldr f a [] ∈ Set.range (foldr g a)
[PROOFSTEP]
exact ⟨[], rfl⟩
[GOAL]
case intro.cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
H : foldr f a l ∈ Set.range (foldr g a)
⊢ foldr f a (b :: l) ∈ Set.range (foldr g a)
[PROOFSTEP]
cases' hfg (Set.mem_range_self b) with c hgf
[GOAL]
case intro.cons.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
H : foldr f a l ∈ Set.range (foldr g a)
c : γ
hgf : g c = f b
⊢ foldr f a (b :: l) ∈ Set.range (foldr g a)
[PROOFSTEP]
cases' H with m hgf'
[GOAL]
case intro.cons.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
c : γ
hgf : g c = f b
m : List γ
hgf' : foldr g a m = foldr f a l
⊢ foldr f a (b :: l) ∈ Set.range (foldr g a)
[PROOFSTEP]
rw [foldr_cons, ← hgf, ← hgf']
[GOAL]
case intro.cons.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
c : γ
hgf : g c = f b
m : List γ
hgf' : foldr g a m = foldr f a l
⊢ g c (foldr g a m) ∈ Set.range (foldr g a)
[PROOFSTEP]
exact ⟨c :: m, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b
a : α
⊢ Set.range (foldl f a) ⊆ Set.range (foldl g a)
[PROOFSTEP]
change
  (Set.range fun l => _) ⊆
    Set.range fun l =>
      _
        -- Porting note: This was simply `simp_rw [← foldr_reverse]`
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b
a : α
⊢ (Set.range fun l => foldl f a l) ⊆ Set.range fun l => foldl g a l
[PROOFSTEP]
simp_rw [← foldr_reverse _ (fun z w => g w z), ← foldr_reverse _ (fun z w => f w z)]
  -- Porting note: This `change` was not necessary in mathlib3
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b
a : α
⊢ (Set.range fun l => foldr (fun z w => f w z) a (reverse l)) ⊆
    Set.range fun l => foldr (fun z w => g w z) a (reverse l)
[PROOFSTEP]
change (Set.range (foldr (fun z w => f w z) a ∘ reverse)) ⊆ Set.range (foldr (fun z w => g w z) a ∘ reverse)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b
a : α
⊢ Set.range (foldr (fun z w => f w z) a ∘ reverse) ⊆ Set.range (foldr (fun z w => g w z) a ∘ reverse)
[PROOFSTEP]
simp_rw [Set.range_comp _ reverse, reverse_involutive.bijective.surjective.range_eq, Set.image_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b
a : α
⊢ Set.range (foldr (fun z w => f w z) a) ⊆ Set.range (foldr (fun z w => g w z) a)
[PROOFSTEP]
exact foldr_range_subset_of_range_subset hfg a
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
f : α → σ → σ × β
a : α
as : List α
s : σ
⊢ mapAccumr f (a :: as) s =
    foldr
      (fun a s =>
        let r := f a s.fst;
        (r.fst, r.snd :: s.snd))
      (s, []) (a :: as)
[PROOFSTEP]
simp only [mapAccumr, foldr, mapAccumr_eq_foldr f as]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
f : α → β → σ → σ × φ
a : α
as : List α
b : β
bs : List β
s : σ
⊢ mapAccumr₂ f (a :: as) (b :: bs) s =
    foldr
      (fun ab s =>
        let r := f ab.fst ab.snd s.fst;
        (r.fst, r.snd :: s.snd))
      (s, []) (zip (a :: as) (b :: bs))
[PROOFSTEP]
simp only [mapAccumr₂, foldr, mapAccumr₂_eq_foldr f as]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
f : α → β → σ → σ × φ
a : α
as : List α
b : β
bs : List β
s : σ
⊢ ((f a b
          (foldr (fun ab s => ((f ab.fst ab.snd s.fst).fst, (f ab.fst ab.snd s.fst).snd :: s.snd)) (s, [])
              (zip as bs)).fst).fst,
      (f a b
            (foldr (fun ab s => ((f ab.fst ab.snd s.fst).fst, (f ab.fst ab.snd s.fst).snd :: s.snd)) (s, [])
                (zip as bs)).fst).snd ::
        (foldr (fun ab s => ((f ab.fst ab.snd s.fst).fst, (f ab.fst ab.snd s.fst).snd :: s.snd)) (s, [])
            (zip as bs)).snd) =
    ((f a b
          (foldr (fun ab s => ((f ab.fst ab.snd s.fst).fst, (f ab.fst ab.snd s.fst).snd :: s.snd)) (s, [])
              (zipWith Prod.mk as bs)).fst).fst,
      (f a b
            (foldr (fun ab s => ((f ab.fst ab.snd s.fst).fst, (f ab.fst ab.snd s.fst).snd :: s.snd)) (s, [])
                (zipWith Prod.mk as bs)).fst).snd ::
        (foldr (fun ab s => ((f ab.fst ab.snd s.fst).fst, (f ab.fst ab.snd s.fst).snd :: s.snd)) (s, [])
            (zipWith Prod.mk as bs)).snd)
[PROOFSTEP]
rfl


[GOAL]
α : Type u
n : ℕ
f : Fin n → α
⊢ length (ofFn f) = n
[PROOFSTEP]
simp [ofFn]
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
i : Fin (length (ofFn f))
⊢ length (ofFn f) = n
[PROOFSTEP]
simp
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
i : Fin (length (ofFn f))
⊢ get (ofFn f) i = f (↑(Fin.castIso (_ : length (ofFn f) = n)) i)
[PROOFSTEP]
have := Array.getElem_ofFn f i (by simpa using i.2)
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
i : Fin (length (ofFn f))
⊢ ↑i < Array.size (Array.ofFn f)
[PROOFSTEP]
simpa using i.2
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
i : Fin (length (ofFn f))
this : (Array.ofFn f)[↑i] = f { val := ↑i, isLt := (_ : ↑i < n) }
⊢ get (ofFn f) i = f (↑(Fin.castIso (_ : length (ofFn f) = n)) i)
[PROOFSTEP]
cases' i with i hi
[GOAL]
case mk
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
hi : i < length (ofFn f)
this :
  (Array.ofFn f)[↑{ val := i, isLt := hi }] =
    f { val := ↑{ val := i, isLt := hi }, isLt := (_ : ↑{ val := i, isLt := hi } < n) }
⊢ get (ofFn f) { val := i, isLt := hi } = f (↑(Fin.castIso (_ : length (ofFn f) = n)) { val := i, isLt := hi })
[PROOFSTEP]
simp only [getElem, Array.get] at this
[GOAL]
case mk
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
hi : i < length (ofFn f)
this :
  get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =
    f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }
⊢ get (ofFn f) { val := i, isLt := hi } = f (↑(Fin.castIso (_ : length (ofFn f) = n)) { val := i, isLt := hi })
[PROOFSTEP]
simp only [Fin.castIso_mk]
[GOAL]
case mk
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
hi : i < length (ofFn f)
this :
  get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =
    f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }
⊢ get (ofFn f) { val := i, isLt := hi } = f { val := i, isLt := (_ : i < n) }
[PROOFSTEP]
rw [← this]
[GOAL]
case mk
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
hi : i < length (ofFn f)
this :
  get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =
    f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }
⊢ get (ofFn f) { val := i, isLt := hi } =
    get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) }
[PROOFSTEP]
congr
[GOAL]
case mk.h.e_2.h
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
hi : i < length (ofFn f)
this :
  get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =
    f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }
⊢ ofFn f = (Array.ofFn f).data
[PROOFSTEP]
simp [ofFn]
[GOAL]
case mk.h.e_3.e_1.e_a
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
hi : i < length (ofFn f)
this :
  get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =
    f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }
⊢ ofFn f = (Array.ofFn f).data
[PROOFSTEP]
simp [ofFn]
[GOAL]
case mk.h.e_3.e_3
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
hi : i < length (ofFn f)
this :
  get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =
    f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }
⊢ HEq hi (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f))
[PROOFSTEP]
simp [ofFn]
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
h : i < length (ofFn f)
⊢ get? (ofFn f) i = ofFnNthVal f i
[PROOFSTEP]
rw [get?_eq_get h, get_ofFn]
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
h : i < length (ofFn f)
⊢ some (f (↑(Fin.castIso (_ : length (ofFn f) = n)) { val := i, isLt := h })) = ofFnNthVal f i
[PROOFSTEP]
simp at h
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
h✝ : i < length (ofFn f)
h : i < n
⊢ some (f (↑(Fin.castIso (_ : length (ofFn f) = n)) { val := i, isLt := h✝ })) = ofFnNthVal f i
[PROOFSTEP]
simp [ofFnNthVal, h]
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
h : ¬i < length (ofFn f)
⊢ get? (ofFn f) i = ofFnNthVal f i
[PROOFSTEP]
rw [ofFnNthVal, dif_neg]
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
h : ¬i < length (ofFn f)
⊢ get? (ofFn f) i = none
[PROOFSTEP]
simpa using h
[GOAL]
case hnc
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
h : ¬i < length (ofFn f)
⊢ ¬i < n
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
i : Fin n
⊢ nthLe (ofFn f) ↑i (_ : ↑i < length (ofFn f)) = f i
[PROOFSTEP]
simp [nthLe]
[GOAL]
α : Type u
β : Type u_1
n : ℕ
f : Fin n → α
g : α → β
⊢ length (map g (ofFn f)) = length (ofFn (g ∘ f))
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type u_1
n : ℕ
f : Fin n → α
g : α → β
i : ℕ
h : i < length (map g (ofFn f))
h' : i < length (ofFn (g ∘ f))
⊢ get (map g (ofFn f)) { val := i, isLt := h } = get (ofFn (g ∘ f)) { val := i, isLt := h' }
[PROOFSTEP]
simp
[GOAL]
α : Type u
m n : ℕ
h : m = n
f : Fin m → α
⊢ ofFn f = ofFn fun i => f (↑(Fin.castIso (_ : n = m)) i)
[PROOFSTEP]
subst h
[GOAL]
α : Type u
m : ℕ
f : Fin m → α
⊢ ofFn f = ofFn fun i => f (↑(Fin.castIso (_ : m = m)) i)
[PROOFSTEP]
simp_rw [Fin.castIso_refl, OrderIso.refl_apply]
[GOAL]
α : Type u
n : ℕ
f : Fin (succ n) → α
⊢ length (ofFn f) = length (f 0 :: ofFn fun i => f (Fin.succ i))
[PROOFSTEP]
simp
[GOAL]
α : Type u
n : ℕ
f : Fin (succ n) → α
i : ℕ
hi₁ : i < length (ofFn f)
hi₂ : i < length (f 0 :: ofFn fun i => f (Fin.succ i))
⊢ get (ofFn f) { val := i, isLt := hi₁ } = get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := i, isLt := hi₂ }
[PROOFSTEP]
cases i
[GOAL]
case zero
α : Type u
n : ℕ
f : Fin (succ n) → α
hi₁ : zero < length (ofFn f)
hi₂ : zero < length (f 0 :: ofFn fun i => f (Fin.succ i))
⊢ get (ofFn f) { val := zero, isLt := hi₁ } = get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := zero, isLt := hi₂ }
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u
n : ℕ
f : Fin (succ n) → α
n✝ : ℕ
hi₁ : succ n✝ < length (ofFn f)
hi₂ : succ n✝ < length (f 0 :: ofFn fun i => f (Fin.succ i))
⊢ get (ofFn f) { val := succ n✝, isLt := hi₁ } =
    get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := succ n✝, isLt := hi₂ }
[PROOFSTEP]
simp
[GOAL]
α : Type u
n : ℕ
f : Fin (succ n) → α
⊢ ofFn f = concat (ofFn fun i => f (Fin.castSucc i)) (f (Fin.last n))
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
α : Type u
n : ℕ
f✝ : Fin (succ n) → α
f : Fin (succ zero) → α
⊢ ofFn f = concat (ofFn fun i => f (Fin.castSucc i)) (f (Fin.last zero))
[PROOFSTEP]
rw [ofFn_zero, concat_nil, ofFn_succ, ofFn_zero]
[GOAL]
case zero
α : Type u
n : ℕ
f✝ : Fin (succ n) → α
f : Fin (succ zero) → α
⊢ [f 0] = [f (Fin.last zero)]
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u
n✝ : ℕ
f✝ : Fin (succ n✝) → α
n : ℕ
IH : ∀ (f : Fin (succ n) → α), ofFn f = concat (ofFn fun i => f (Fin.castSucc i)) (f (Fin.last n))
f : Fin (succ (succ n)) → α
⊢ ofFn f = concat (ofFn fun i => f (Fin.castSucc i)) (f (Fin.last (succ n)))
[PROOFSTEP]
rw [ofFn_succ, IH, ofFn_succ, concat_cons, Fin.castSucc_zero]
[GOAL]
case succ
α : Type u
n✝ : ℕ
f✝ : Fin (succ n✝) → α
n : ℕ
IH : ∀ (f : Fin (succ n) → α), ofFn f = concat (ofFn fun i => f (Fin.castSucc i)) (f (Fin.last n))
f : Fin (succ (succ n)) → α
⊢ f 0 :: concat (ofFn fun i => f (Fin.succ (Fin.castSucc i))) (f (Fin.succ (Fin.last n))) =
    f 0 :: concat (ofFn fun i => f (Fin.castSucc (Fin.succ i))) (f (Fin.last (succ n)))
[PROOFSTEP]
congr
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
⊢ ofFn f = [] ↔ n = 0
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u
f : Fin zero → α
⊢ ofFn f = [] ↔ zero = 0
[PROOFSTEP]
simp only [ofFn_zero, ofFn_succ, eq_self_iff_true, Nat.succ_ne_zero]
[GOAL]
case succ
α : Type u
n✝ : ℕ
f : Fin (succ n✝) → α
⊢ ofFn f = [] ↔ succ n✝ = 0
[PROOFSTEP]
simp only [ofFn_zero, ofFn_succ, eq_self_iff_true, Nat.succ_ne_zero]
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
h : ofFn f ≠ []
hn : optParam (n - 1 < n) (_ : pred (Nat.sub n 0) < Nat.sub n 0)
⊢ getLast (ofFn f) h = f { val := n - 1, isLt := hn }
[PROOFSTEP]
simp [getLast_eq_get]
[GOAL]
α : Type u
m n : ℕ
f : Fin (m + n) → α
⊢ ofFn f = (ofFn fun i => f (Fin.castAdd n i)) ++ ofFn fun j => f (Fin.natAdd m j)
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
α : Type u
m n : ℕ
f✝ : Fin (m + n) → α
f : Fin (m + zero) → α
⊢ ofFn f = (ofFn fun i => f (Fin.castAdd zero i)) ++ ofFn fun j => f (Fin.natAdd m j)
[PROOFSTEP]
rw [ofFn_zero, append_nil, Fin.castAdd_zero]
[GOAL]
case zero
α : Type u
m n : ℕ
f✝ : Fin (m + n) → α
f : Fin (m + zero) → α
⊢ ofFn f = ofFn fun i => f (Fin.cast (_ : m = m) i)
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u
m n✝ : ℕ
f✝ : Fin (m + n✝) → α
n : ℕ
IH : ∀ (f : Fin (m + n) → α), ofFn f = (ofFn fun i => f (Fin.castAdd n i)) ++ ofFn fun j => f (Fin.natAdd m j)
f : Fin (m + succ n) → α
⊢ ofFn f = (ofFn fun i => f (Fin.castAdd (succ n) i)) ++ ofFn fun j => f (Fin.natAdd m j)
[PROOFSTEP]
rw [ofFn_succ', ofFn_succ', IH, append_concat]
[GOAL]
case succ
α : Type u
m n✝ : ℕ
f✝ : Fin (m + n✝) → α
n : ℕ
IH : ∀ (f : Fin (m + n) → α), ofFn f = (ofFn fun i => f (Fin.castAdd n i)) ++ ofFn fun j => f (Fin.natAdd m j)
f : Fin (m + succ n) → α
⊢ concat ((ofFn fun i => f (Fin.castSucc (Fin.castAdd n i))) ++ ofFn fun j => f (Fin.castSucc (Fin.natAdd m j)))
      (f (Fin.last (Nat.add m n))) =
    concat ((ofFn fun i => f (Fin.castAdd (succ n) i)) ++ ofFn fun i => f (Fin.natAdd m (Fin.castSucc i)))
      (f (Fin.natAdd m (Fin.last n)))
[PROOFSTEP]
rfl
[GOAL]
α : Type u
m n : ℕ
a : Fin m → α
b : Fin n → α
⊢ ofFn (Fin.append a b) = ofFn a ++ ofFn b
[PROOFSTEP]
simp_rw [ofFn_add, Fin.append_left, Fin.append_right]
[GOAL]
α : Type u
m n : ℕ
f : Fin (m * n) → α
⊢ ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })
[PROOFSTEP]
induction' m with m IH
[GOAL]
case zero
α : Type u
m n : ℕ
f✝ : Fin (m * n) → α
f : Fin (zero * n) → α
⊢ ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < zero * n) })
[PROOFSTEP]
simp [ofFn_zero, zero_mul, ofFn_zero, join]
[GOAL]
case succ
α : Type u
m✝ n : ℕ
f✝ : Fin (m✝ * n) → α
m : ℕ
IH :
  ∀ (f : Fin (m * n) → α),
    ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })
f : Fin (succ m * n) → α
⊢ ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < succ m * n) })
[PROOFSTEP]
simp_rw [ofFn_succ', succ_mul, join_concat, ofFn_add, IH]
[GOAL]
case succ
α : Type u
m✝ n : ℕ
f✝ : Fin (m✝ * n) → α
m : ℕ
IH :
  ∀ (f : Fin (m * n) → α),
    ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })
f : Fin (succ m * n) → α
⊢ (join
        (ofFn fun i =>
          ofFn fun j =>
            f
              (↑(Fin.castIso (_ : m * n + n = succ m * n))
                (Fin.castAdd n { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) }))) ++
      ofFn fun j => f (↑(Fin.castIso (_ : m * n + n = succ m * n)) (Fin.natAdd (m * n) j))) =
    join
        (ofFn fun i =>
          ofFn fun j =>
            f { val := ↑(Fin.castSucc i) * n + ↑j, isLt := (_ : ↑(Fin.castSucc i) * n + ↑j < succ m * n) }) ++
      ofFn fun j => f { val := ↑(Fin.last m) * n + ↑j, isLt := (_ : ↑(Fin.last m) * n + ↑j < succ m * n) }
[PROOFSTEP]
rfl
[GOAL]
α : Type u
m n : ℕ
f : Fin (m * n) → α
⊢ ofFn f = join (ofFn fun i => ofFn fun j => f { val := m * ↑i + ↑j, isLt := (_ : m * ↑i + ↑j < m * n) })
[PROOFSTEP]
simp_rw [mul_comm m n, mul_comm m, ofFn_mul, Fin.castIso_mk]
[GOAL]
α : Type u
a : α
l : List α
⊢ ofFn (get (a :: l)) = a :: l
[PROOFSTEP]
rw [ofFn_succ]
[GOAL]
α : Type u
a : α
l : List α
⊢ (get (a :: l) 0 :: ofFn fun i => get (a :: l) (Fin.succ i)) = a :: l
[PROOFSTEP]
congr
[GOAL]
case e_tail
α : Type u
a : α
l : List α
⊢ (ofFn fun i => get (a :: l) (Fin.succ i)) = l
[PROOFSTEP]
exact ofFn_get l
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
a : α
⊢ a ∈ ofFn f ↔ a ∈ Set.range f
[PROOFSTEP]
simp only [mem_iff_get, Set.mem_range, get_ofFn]
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
a : α
⊢ (∃ n_1, f (↑(Fin.castIso (_ : length (ofFn f) = n)) n_1) = a) ↔ ∃ y, f y = a
[PROOFSTEP]
exact ⟨fun ⟨i, hi⟩ => ⟨Fin.castIso (by simp) i, hi⟩, fun ⟨i, hi⟩ => ⟨Fin.castIso (by simp) i, hi⟩⟩
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
a : α
x✝ : ∃ n_1, f (↑(Fin.castIso (_ : length (ofFn f) = n)) n_1) = a
i : Fin (length (ofFn f))
hi : f (↑(Fin.castIso (_ : length (ofFn f) = n)) i) = a
⊢ length (ofFn f) = n
[PROOFSTEP]
simp
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
a : α
x✝ : ∃ y, f y = a
i : Fin n
hi : f i = a
⊢ n = length (ofFn f)
[PROOFSTEP]
simp
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
P : α → Prop
⊢ (∀ (i : α), i ∈ ofFn f → P i) ↔ ∀ (j : Fin n), P (f j)
[PROOFSTEP]
simp only [mem_ofFn, Set.forall_range_iff]
[GOAL]
α : Type u
n : ℕ
c : α
⊢ (ofFn fun x => c) = replicate (n + 1) c
[PROOFSTEP]
rw [replicate, ← ofFn_const n]
[GOAL]
α : Type u
n : ℕ
c : α
⊢ (ofFn fun x => c) = c :: ofFn fun x => c
[PROOFSTEP]
simp
[GOAL]
α : Type u
m : ℕ
a : Fin m → α
n : ℕ
⊢ ofFn (Fin.repeat n a) = join (replicate n (ofFn a))
[PROOFSTEP]
simp_rw [ofFn_mul, ← ofFn_const, Fin.repeat, Fin.modNat, add_comm, Nat.add_mul_mod_self_right,
  Nat.mod_eq_of_lt (Fin.is_lt _)]
[GOAL]
α : Type u
R : α → α → Prop
n : ℕ
f : Fin n → α
⊢ Pairwise R (ofFn f) ↔ ∀ ⦃i j : Fin n⦄, i < j → R (f i) (f j)
[PROOFSTEP]
simp only [pairwise_iff_get, (Fin.castIso (length_ofFn f)).surjective.forall, get_ofFn, OrderIso.lt_iff_lt]
[GOAL]
α : Type u
C : List α → Sort u_1
h : (n : ℕ) → (f : Fin n → α) → C (ofFn f)
n : ℕ
f : Fin n → α
⊢ ofFnRec h (ofFn f) = h n f
[PROOFSTEP]
have := (@equivSigmaTuple α).rightInverse_symm
[GOAL]
α : Type u
C : List α → Sort u_1
h : (n : ℕ) → (f : Fin n → α) → C (ofFn f)
n : ℕ
f : Fin n → α
this : Function.RightInverse ↑equivSigmaTuple.symm ↑equivSigmaTuple
⊢ ofFnRec h (ofFn f) = h n f
[PROOFSTEP]
dsimp [equivSigmaTuple] at this
[GOAL]
α : Type u
C : List α → Sort u_1
h : (n : ℕ) → (f : Fin n → α) → C (ofFn f)
n : ℕ
f : Fin n → α
this : Function.RightInverse (fun f => ofFn f.snd) fun l => { fst := length l, snd := get l }
⊢ ofFnRec h (ofFn f) = h n f
[PROOFSTEP]
have := this.cast_eq (fun s => h s.1 s.2) ⟨n, f⟩
[GOAL]
α : Type u
C : List α → Sort u_1
h : (n : ℕ) → (f : Fin n → α) → C (ofFn f)
n : ℕ
f : Fin n → α
this✝ : Function.RightInverse (fun f => ofFn f.snd) fun l => { fst := length l, snd := get l }
this :
  cast
      (_ :
        C (ofFn { fst := length (ofFn { fst := n, snd := f }.snd), snd := get (ofFn { fst := n, snd := f }.snd) }.snd) =
          C (ofFn { fst := n, snd := f }.snd))
      (h { fst := length (ofFn { fst := n, snd := f }.snd), snd := get (ofFn { fst := n, snd := f }.snd) }.fst
        { fst := length (ofFn { fst := n, snd := f }.snd), snd := get (ofFn { fst := n, snd := f }.snd) }.snd) =
    h { fst := n, snd := f }.fst { fst := n, snd := f }.snd
⊢ ofFnRec h (ofFn f) = h n f
[PROOFSTEP]
dsimp only at this
[GOAL]
α : Type u
C : List α → Sort u_1
h : (n : ℕ) → (f : Fin n → α) → C (ofFn f)
n : ℕ
f : Fin n → α
this✝ : Function.RightInverse (fun f => ofFn f.snd) fun l => { fst := length l, snd := get l }
this :
  cast (_ : C (ofFn { fst := length (ofFn f), snd := get (ofFn f) }.snd) = C (ofFn { fst := n, snd := f }.snd))
      (h (length (ofFn f)) (get (ofFn f))) =
    h n f
⊢ ofFnRec h (ofFn f) = h n f
[PROOFSTEP]
rw [ofFnRec, ← this]
[GOAL]
α : Type u
n : ℕ
f g : Fin n → α
h : ofFn f = ofFn g
⊢ HEq f g
[PROOFSTEP]
rw [ofFn_inj'] at h
[GOAL]
α : Type u
n : ℕ
f g : Fin n → α
h : { fst := n, snd := f } = { fst := n, snd := g }
⊢ HEq f g
[PROOFSTEP]
cases h
[GOAL]
case refl
α : Type u
n : ℕ
f : Fin n → α
⊢ HEq f f
[PROOFSTEP]
rfl


[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : NonUnitalNonAssocSemiring R
a : R
l : List R
h : ∀ (b : R), b ∈ l → Commute a b
⊢ Commute a (sum l)
[PROOFSTEP]
induction' l with x xs ih
[GOAL]
case nil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : NonUnitalNonAssocSemiring R
a : R
l : List R
h✝ : ∀ (b : R), b ∈ l → Commute a b
h : ∀ (b : R), b ∈ [] → Commute a b
⊢ Commute a (sum [])
[PROOFSTEP]
exact Commute.zero_right _
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : NonUnitalNonAssocSemiring R
a : R
l : List R
h✝ : ∀ (b : R), b ∈ l → Commute a b
x : R
xs : List R
ih : (∀ (b : R), b ∈ xs → Commute a b) → Commute a (sum xs)
h : ∀ (b : R), b ∈ x :: xs → Commute a b
⊢ Commute a (sum (x :: xs))
[PROOFSTEP]
rw [List.sum_cons]
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : NonUnitalNonAssocSemiring R
a : R
l : List R
h✝ : ∀ (b : R), b ∈ l → Commute a b
x : R
xs : List R
ih : (∀ (b : R), b ∈ xs → Commute a b) → Commute a (sum xs)
h : ∀ (b : R), b ∈ x :: xs → Commute a b
⊢ Commute a (x + sum xs)
[PROOFSTEP]
exact (h _ <| mem_cons_self _ _).add_right (ih fun j hj => h _ <| mem_cons_of_mem _ hj)
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedMonoid M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ prod l = 1
[PROOFSTEP]
rw [List.eq_replicate.2 ⟨_, h⟩, prod_replicate, one_pow]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedMonoid M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ ℕ
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedMonoid M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ length l = ?m.7726
[PROOFSTEP]
exact (length l)
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedMonoid M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ length l = length l
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
l : List ℤ
h : prod l = -1
⊢ -1 ∈ l
[PROOFSTEP]
obtain ⟨x, h₁, h₂⟩ := exists_mem_ne_one_of_prod_ne_one (ne_of_eq_of_ne h (by decide))
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
l : List ℤ
h : prod l = -1
⊢ -1 ≠ 1
[PROOFSTEP]
decide
[GOAL]
case intro.intro
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
l : List ℤ
h : prod l = -1
x : ℤ
h₁ : x ∈ l
h₂ : x ≠ 1
⊢ -1 ∈ l
[PROOFSTEP]
exact
  Or.resolve_left (Int.isUnit_iff.mp (prod_isUnit_iff.mp (h.symm ▸ IsUnit.neg isUnit_one : IsUnit l.prod) x h₁)) h₂ ▸ h₁
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
L : List ℕ
h : ∀ (i : ℕ), i ∈ L → 1 ≤ i
⊢ length L ≤ sum L
[PROOFSTEP]
induction' L with j L IH h
[GOAL]
case nil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
L : List ℕ
h✝ : ∀ (i : ℕ), i ∈ L → 1 ≤ i
h : ∀ (i : ℕ), i ∈ [] → 1 ≤ i
⊢ length [] ≤ sum []
[PROOFSTEP]
simp
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
L✝ : List ℕ
h✝ : ∀ (i : ℕ), i ∈ L✝ → 1 ≤ i
j : ℕ
L : List ℕ
IH : (∀ (i : ℕ), i ∈ L → 1 ≤ i) → length L ≤ sum L
h : ∀ (i : ℕ), i ∈ j :: L → 1 ≤ i
⊢ length (j :: L) ≤ sum (j :: L)
[PROOFSTEP]
rw [sum_cons, length, add_comm]
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
L✝ : List ℕ
h✝ : ∀ (i : ℕ), i ∈ L✝ → 1 ≤ i
j : ℕ
L : List ℕ
IH : (∀ (i : ℕ), i ∈ L → 1 ≤ i) → length L ≤ sum L
h : ∀ (i : ℕ), i ∈ j :: L → 1 ≤ i
⊢ 1 + length L ≤ j + sum L
[PROOFSTEP]
exact add_le_add (h _ (mem_cons_self _ _)) (IH fun i hi => h i (mem_cons.2 (Or.inr hi)))
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CommMonoid M
a : M
l : List M
ha : a ∈ l
⊢ a ∣ prod l
[PROOFSTEP]
let ⟨s, t, h⟩ := mem_split ha
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CommMonoid M
a : M
l : List M
ha : a ∈ l
s t : List M
h : l = s ++ a :: t
⊢ a ∣ prod l
[PROOFSTEP]
rw [h, prod_append, prod_cons, mul_left_comm]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CommMonoid M
a : M
l : List M
ha : a ∈ l
s t : List M
h : l = s ++ a :: t
⊢ a ∣ a * (prod s * prod t)
[PROOFSTEP]
exact dvd_mul_right _ _
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Semiring R
a : R
l : List R
h : ∀ (x : R), x ∈ l → a ∣ x
⊢ a ∣ sum l
[PROOFSTEP]
induction' l with x l ih
[GOAL]
case nil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Semiring R
a : R
l : List R
h✝ : ∀ (x : R), x ∈ l → a ∣ x
h : ∀ (x : R), x ∈ [] → a ∣ x
⊢ a ∣ sum []
[PROOFSTEP]
exact dvd_zero _
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Semiring R
a : R
l✝ : List R
h✝ : ∀ (x : R), x ∈ l✝ → a ∣ x
x : R
l : List R
ih : (∀ (x : R), x ∈ l → a ∣ x) → a ∣ sum l
h : ∀ (x_1 : R), x_1 ∈ x :: l → a ∣ x_1
⊢ a ∣ sum (x :: l)
[PROOFSTEP]
rw [List.sum_cons]
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Semiring R
a : R
l✝ : List R
h✝ : ∀ (x : R), x ∈ l✝ → a ∣ x
x : R
l : List R
ih : (∀ (x : R), x ∈ l → a ∣ x) → a ∣ sum l
h : ∀ (x_1 : R), x_1 ∈ x :: l → a ∣ x_1
⊢ a ∣ x + sum l
[PROOFSTEP]
exact dvd_add (h _ (mem_cons_self _ _)) (ih fun x hx => h x (mem_cons_of_mem _ hx))
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CommGroup α
l₂ : List α
⊢ alternatingProd ([] ++ l₂) = alternatingProd [] * alternatingProd l₂ ^ (-1) ^ length []
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CommGroup α
a : α
l₁ l₂ : List α
⊢ alternatingProd (a :: l₁ ++ l₂) = alternatingProd (a :: l₁) * alternatingProd l₂ ^ (-1) ^ length (a :: l₁)
[PROOFSTEP]
simp_rw [cons_append, alternatingProd_cons, alternatingProd_append, length_cons, pow_succ, neg_mul, one_mul, zpow_neg, ←
  div_eq_mul_inv, div_div]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CommGroup α
⊢ alternatingProd (reverse []) = alternatingProd [] ^ (-1) ^ (length [] + 1)
[PROOFSTEP]
simp only [alternatingProd_nil, one_zpow, reverse_nil]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CommGroup α
a : α
l : List α
⊢ alternatingProd (reverse (a :: l)) = alternatingProd (a :: l) ^ (-1) ^ (length (a :: l) + 1)
[PROOFSTEP]
simp_rw [reverse_cons, alternatingProd_append, alternatingProd_reverse, alternatingProd_singleton, alternatingProd_cons,
  length_reverse, length, pow_succ, neg_mul, one_mul, zpow_neg, inv_inv]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CommGroup α
a : α
l : List α
⊢ (alternatingProd l ^ (-1) ^ length l)⁻¹ * a ^ (-1) ^ length l = (a / alternatingProd l) ^ (-1) ^ length l
[PROOFSTEP]
rw [mul_comm, ← div_eq_mul_inv, div_zpow]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Monoid M
⊢ ∀ (l : List M), op (prod l) = prod (reverse (map op l))
[PROOFSTEP]
intro l
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Monoid M
l : List M
⊢ op (prod l) = prod (reverse (map op l))
[PROOFSTEP]
induction l with
| nil => rfl
| cons x xs ih => rw [List.prod_cons, List.map_cons, List.reverse_cons', List.prod_concat, op_mul, ih]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Monoid M
l : List M
⊢ op (prod l) = prod (reverse (map op l))
[PROOFSTEP]
induction l with
| nil => rfl
| cons x xs ih => rw [List.prod_cons, List.map_cons, List.reverse_cons', List.prod_concat, op_mul, ih]
[GOAL]
case nil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Monoid M
⊢ op (prod []) = prod (reverse (map op []))
[PROOFSTEP]

| nil => rfl
[GOAL]
case nil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Monoid M
⊢ op (prod []) = prod (reverse (map op []))
[PROOFSTEP]
rfl
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Monoid M
x : M
xs : List M
ih : op (prod xs) = prod (reverse (map op xs))
⊢ op (prod (x :: xs)) = prod (reverse (map op (x :: xs)))
[PROOFSTEP]

| cons x xs ih => rw [List.prod_cons, List.map_cons, List.reverse_cons', List.prod_concat, op_mul, ih]
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Monoid M
x : M
xs : List M
ih : op (prod xs) = prod (reverse (map op xs))
⊢ op (prod (x :: xs)) = prod (reverse (map op (x :: xs)))
[PROOFSTEP]
rw [List.prod_cons, List.map_cons, List.reverse_cons', List.prod_concat, op_mul, ih]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Monoid M
l : List Mᵐᵒᵖ
⊢ unop (prod l) = prod (reverse (map unop l))
[PROOFSTEP]
rw [← op_inj, op_unop, MulOpposite.op_list_prod, map_reverse, map_map, reverse_reverse, op_comp_unop, map_id]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
F : Type u_9
inst✝ : MonoidHomClass F M Nᵐᵒᵖ
f : F
l : List M
⊢ unop (↑f (prod l)) = prod (reverse (map (unop ∘ ↑f) l))
[PROOFSTEP]
rw [map_list_prod f l, MulOpposite.unop_list_prod, List.map_map]


[GOAL]
M : Type u_1
inst✝¹ : Zero M
l : List M
inst✝ : DecidablePred fun x => getD l x 0 ≠ 0
n✝ n : ℕ
⊢ n ∈ Finset.filter (fun i => getD l i 0 ≠ 0) (Finset.range (length l)) ↔ (fun i => getD l i 0) n ≠ 0
[PROOFSTEP]
simp only [Ne.def, Finset.mem_filter, Finset.mem_range, and_iff_right_iff_imp]
[GOAL]
M : Type u_1
inst✝¹ : Zero M
l : List M
inst✝ : DecidablePred fun x => getD l x 0 ≠ 0
n✝ n : ℕ
⊢ ¬getD l n 0 = 0 → n < length l
[PROOFSTEP]
contrapose!
[GOAL]
M : Type u_1
inst✝¹ : Zero M
l : List M
inst✝ : DecidablePred fun x => getD l x 0 ≠ 0
n✝ n : ℕ
⊢ length l ≤ n → getD l n 0 = 0
[PROOFSTEP]
exact getD_eq_default _ _
[GOAL]
M : Type u_1
inst✝² : Zero M
l : List M
inst✝¹ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
inst✝ : DecidablePred fun i => getD [] i 0 ≠ 0
⊢ toFinsupp [] = 0
[PROOFSTEP]
ext
[GOAL]
case h
M : Type u_1
inst✝² : Zero M
l : List M
inst✝¹ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
inst✝ : DecidablePred fun i => getD [] i 0 ≠ 0
a✝ : ℕ
⊢ ↑(toFinsupp []) a✝ = ↑0 a✝
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
inst✝² : Zero M
l : List M
inst✝¹ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
x : M
inst✝ : DecidablePred fun x_1 => getD [x] x_1 0 ≠ 0
⊢ toFinsupp [x] = Finsupp.single 0 x
[PROOFSTEP]
ext ⟨_ | i⟩
[GOAL]
case h.zero
M : Type u_1
inst✝² : Zero M
l : List M
inst✝¹ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
x : M
inst✝ : DecidablePred fun x_1 => getD [x] x_1 0 ≠ 0
⊢ ↑(toFinsupp [x]) Nat.zero = ↑(Finsupp.single 0 x) Nat.zero
[PROOFSTEP]
simp [Finsupp.single_apply, (Nat.zero_lt_succ _).ne]
[GOAL]
case h.succ
M : Type u_1
inst✝² : Zero M
l : List M
inst✝¹ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
x : M
inst✝ : DecidablePred fun x_1 => getD [x] x_1 0 ≠ 0
n✝ : ℕ
⊢ ↑(toFinsupp [x]) (Nat.succ n✝) = ↑(Finsupp.single 0 x) (Nat.succ n✝)
[PROOFSTEP]
simp [Finsupp.single_apply, (Nat.zero_lt_succ _).ne]
[GOAL]
M : Type u_1
inst✝⁵ : Zero M
l : List M
inst✝⁴ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x => getD (l₁ ++ l₂) x 0 ≠ 0
inst✝¹ : DecidablePred fun x => getD l₁ x 0 ≠ 0
inst✝ : DecidablePred fun x => getD l₂ x 0 ≠ 0
⊢ toFinsupp (l₁ ++ l₂) = toFinsupp l₁ + Finsupp.embDomain (addLeftEmbedding (length l₁)) (toFinsupp l₂)
[PROOFSTEP]
ext n
[GOAL]
case h
M : Type u_1
inst✝⁵ : Zero M
l : List M
inst✝⁴ : DecidablePred fun x => getD l x 0 ≠ 0
n✝ : ℕ
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x => getD (l₁ ++ l₂) x 0 ≠ 0
inst✝¹ : DecidablePred fun x => getD l₁ x 0 ≠ 0
inst✝ : DecidablePred fun x => getD l₂ x 0 ≠ 0
n : ℕ
⊢ ↑(toFinsupp (l₁ ++ l₂)) n = ↑(toFinsupp l₁ + Finsupp.embDomain (addLeftEmbedding (length l₁)) (toFinsupp l₂)) n
[PROOFSTEP]
simp only [toFinsupp_apply, Finsupp.add_apply]
[GOAL]
case h
M : Type u_1
inst✝⁵ : Zero M
l : List M
inst✝⁴ : DecidablePred fun x => getD l x 0 ≠ 0
n✝ : ℕ
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x => getD (l₁ ++ l₂) x 0 ≠ 0
inst✝¹ : DecidablePred fun x => getD l₁ x 0 ≠ 0
inst✝ : DecidablePred fun x => getD l₂ x 0 ≠ 0
n : ℕ
⊢ getD (l₁ ++ l₂) n 0 = getD l₁ n 0 + ↑(Finsupp.embDomain (addLeftEmbedding (length l₁)) (toFinsupp l₂)) n
[PROOFSTEP]
cases lt_or_le n l₁.length with
| inl h =>
  rw [getD_append _ _ _ _ h, Finsupp.embDomain_notin_range, add_zero]
  rintro ⟨k, rfl : length l₁ + k = n⟩
  exact h.not_le (self_le_add_right _ _)
| inr h =>
  rcases exists_add_of_le h with ⟨k, rfl⟩
  rw [getD_append_right _ _ _ _ h, add_tsub_cancel_left, getD_eq_default _ _ h, zero_add]
  exact Eq.symm (Finsupp.embDomain_apply _ _ _)
[GOAL]
case h
M : Type u_1
inst✝⁵ : Zero M
l : List M
inst✝⁴ : DecidablePred fun x => getD l x 0 ≠ 0
n✝ : ℕ
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x => getD (l₁ ++ l₂) x 0 ≠ 0
inst✝¹ : DecidablePred fun x => getD l₁ x 0 ≠ 0
inst✝ : DecidablePred fun x => getD l₂ x 0 ≠ 0
n : ℕ
x✝ : n < length l₁ ∨ length l₁ ≤ n
⊢ getD (l₁ ++ l₂) n 0 = getD l₁ n 0 + ↑(Finsupp.embDomain (addLeftEmbedding (length l₁)) (toFinsupp l₂)) n
[PROOFSTEP]
cases lt_or_le n l₁.length with
| inl h =>
  rw [getD_append _ _ _ _ h, Finsupp.embDomain_notin_range, add_zero]
  rintro ⟨k, rfl : length l₁ + k = n⟩
  exact h.not_le (self_le_add_right _ _)
| inr h =>
  rcases exists_add_of_le h with ⟨k, rfl⟩
  rw [getD_append_right _ _ _ _ h, add_tsub_cancel_left, getD_eq_default _ _ h, zero_add]
  exact Eq.symm (Finsupp.embDomain_apply _ _ _)
[GOAL]
case h.inl
M : Type u_1
inst✝⁵ : Zero M
l : List M
inst✝⁴ : DecidablePred fun x => getD l x 0 ≠ 0
n✝ : ℕ
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x => getD (l₁ ++ l₂) x 0 ≠ 0
inst✝¹ : DecidablePred fun x => getD l₁ x 0 ≠ 0
inst✝ : DecidablePred fun x => getD l₂ x 0 ≠ 0
n : ℕ
h : n < length l₁
⊢ getD (l₁ ++ l₂) n 0 = getD l₁ n 0 + ↑(Finsupp.embDomain (addLeftEmbedding (length l₁)) (toFinsupp l₂)) n
[PROOFSTEP]

| inl h =>
  rw [getD_append _ _ _ _ h, Finsupp.embDomain_notin_range, add_zero]
  rintro ⟨k, rfl : length l₁ + k = n⟩
  exact h.not_le (self_le_add_right _ _)
[GOAL]
case h.inl
M : Type u_1
inst✝⁵ : Zero M
l : List M
inst✝⁴ : DecidablePred fun x => getD l x 0 ≠ 0
n✝ : ℕ
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x => getD (l₁ ++ l₂) x 0 ≠ 0
inst✝¹ : DecidablePred fun x => getD l₁ x 0 ≠ 0
inst✝ : DecidablePred fun x => getD l₂ x 0 ≠ 0
n : ℕ
h : n < length l₁
⊢ getD (l₁ ++ l₂) n 0 = getD l₁ n 0 + ↑(Finsupp.embDomain (addLeftEmbedding (length l₁)) (toFinsupp l₂)) n
[PROOFSTEP]
rw [getD_append _ _ _ _ h, Finsupp.embDomain_notin_range, add_zero]
[GOAL]
case h.inl.h
M : Type u_1
inst✝⁵ : Zero M
l : List M
inst✝⁴ : DecidablePred fun x => getD l x 0 ≠ 0
n✝ : ℕ
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x => getD (l₁ ++ l₂) x 0 ≠ 0
inst✝¹ : DecidablePred fun x => getD l₁ x 0 ≠ 0
inst✝ : DecidablePred fun x => getD l₂ x 0 ≠ 0
n : ℕ
h : n < length l₁
⊢ ¬n ∈ Set.range ↑(addLeftEmbedding (length l₁))
[PROOFSTEP]
rintro ⟨k, rfl : length l₁ + k = n⟩
[GOAL]
case h.inl.h.intro
M : Type u_1
inst✝⁵ : Zero M
l : List M
inst✝⁴ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x => getD (l₁ ++ l₂) x 0 ≠ 0
inst✝¹ : DecidablePred fun x => getD l₁ x 0 ≠ 0
inst✝ : DecidablePred fun x => getD l₂ x 0 ≠ 0
k : ℕ
h : length l₁ + k < length l₁
⊢ False
[PROOFSTEP]
exact h.not_le (self_le_add_right _ _)
[GOAL]
case h.inr
M : Type u_1
inst✝⁵ : Zero M
l : List M
inst✝⁴ : DecidablePred fun x => getD l x 0 ≠ 0
n✝ : ℕ
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x => getD (l₁ ++ l₂) x 0 ≠ 0
inst✝¹ : DecidablePred fun x => getD l₁ x 0 ≠ 0
inst✝ : DecidablePred fun x => getD l₂ x 0 ≠ 0
n : ℕ
h : length l₁ ≤ n
⊢ getD (l₁ ++ l₂) n 0 = getD l₁ n 0 + ↑(Finsupp.embDomain (addLeftEmbedding (length l₁)) (toFinsupp l₂)) n
[PROOFSTEP]

| inr h =>
  rcases exists_add_of_le h with ⟨k, rfl⟩
  rw [getD_append_right _ _ _ _ h, add_tsub_cancel_left, getD_eq_default _ _ h, zero_add]
  exact Eq.symm (Finsupp.embDomain_apply _ _ _)
[GOAL]
case h.inr
M : Type u_1
inst✝⁵ : Zero M
l : List M
inst✝⁴ : DecidablePred fun x => getD l x 0 ≠ 0
n✝ : ℕ
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x => getD (l₁ ++ l₂) x 0 ≠ 0
inst✝¹ : DecidablePred fun x => getD l₁ x 0 ≠ 0
inst✝ : DecidablePred fun x => getD l₂ x 0 ≠ 0
n : ℕ
h : length l₁ ≤ n
⊢ getD (l₁ ++ l₂) n 0 = getD l₁ n 0 + ↑(Finsupp.embDomain (addLeftEmbedding (length l₁)) (toFinsupp l₂)) n
[PROOFSTEP]
rcases exists_add_of_le h with ⟨k, rfl⟩
[GOAL]
case h.inr.intro
M : Type u_1
inst✝⁵ : Zero M
l : List M
inst✝⁴ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x => getD (l₁ ++ l₂) x 0 ≠ 0
inst✝¹ : DecidablePred fun x => getD l₁ x 0 ≠ 0
inst✝ : DecidablePred fun x => getD l₂ x 0 ≠ 0
k : ℕ
h : length l₁ ≤ length l₁ + k
⊢ getD (l₁ ++ l₂) (length l₁ + k) 0 =
    getD l₁ (length l₁ + k) 0 + ↑(Finsupp.embDomain (addLeftEmbedding (length l₁)) (toFinsupp l₂)) (length l₁ + k)
[PROOFSTEP]
rw [getD_append_right _ _ _ _ h, add_tsub_cancel_left, getD_eq_default _ _ h, zero_add]
[GOAL]
case h.inr.intro
M : Type u_1
inst✝⁵ : Zero M
l : List M
inst✝⁴ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x => getD (l₁ ++ l₂) x 0 ≠ 0
inst✝¹ : DecidablePred fun x => getD l₁ x 0 ≠ 0
inst✝ : DecidablePred fun x => getD l₂ x 0 ≠ 0
k : ℕ
h : length l₁ ≤ length l₁ + k
⊢ getD l₂ k 0 = ↑(Finsupp.embDomain (addLeftEmbedding (length l₁)) (toFinsupp l₂)) (length l₁ + k)
[PROOFSTEP]
exact Eq.symm (Finsupp.embDomain_apply _ _ _)
[GOAL]
M : Type u_1
inst✝⁴ : Zero M
l : List M
inst✝³ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun x_1 => getD (x :: xs) x_1 0 ≠ 0
inst✝ : DecidablePred fun x => getD xs x 0 ≠ 0
⊢ toFinsupp (x :: xs) =
    Finsupp.single 0 x + Finsupp.embDomain { toFun := Nat.succ, inj' := Nat.succ_injective } (toFinsupp xs)
[PROOFSTEP]
classical
convert toFinsupp_append [x] xs using 3
· exact (toFinsupp_singleton x).symm
· ext n
  exact add_comm n 1
[GOAL]
M : Type u_1
inst✝⁴ : Zero M
l : List M
inst✝³ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun x_1 => getD (x :: xs) x_1 0 ≠ 0
inst✝ : DecidablePred fun x => getD xs x 0 ≠ 0
⊢ toFinsupp (x :: xs) =
    Finsupp.single 0 x + Finsupp.embDomain { toFun := Nat.succ, inj' := Nat.succ_injective } (toFinsupp xs)
[PROOFSTEP]
convert toFinsupp_append [x] xs using 3
[GOAL]
case h.e'_3.h.e'_5
M : Type u_1
inst✝⁴ : Zero M
l : List M
inst✝³ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun x_1 => getD (x :: xs) x_1 0 ≠ 0
inst✝ : DecidablePred fun x => getD xs x 0 ≠ 0
⊢ Finsupp.single 0 x = toFinsupp [x]
[PROOFSTEP]
exact (toFinsupp_singleton x).symm
[GOAL]
case h.e'_3.h.e'_6.h.e'_5
M : Type u_1
inst✝⁴ : Zero M
l : List M
inst✝³ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun x_1 => getD (x :: xs) x_1 0 ≠ 0
inst✝ : DecidablePred fun x => getD xs x 0 ≠ 0
⊢ { toFun := Nat.succ, inj' := Nat.succ_injective } = addLeftEmbedding (length [x])
[PROOFSTEP]
ext n
[GOAL]
case h.e'_3.h.e'_6.h.e'_5.h
M : Type u_1
inst✝⁴ : Zero M
l : List M
inst✝³ : DecidablePred fun x => getD l x 0 ≠ 0
n✝ : ℕ
R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun x_1 => getD (x :: xs) x_1 0 ≠ 0
inst✝ : DecidablePred fun x => getD xs x 0 ≠ 0
n : ℕ
⊢ ↑{ toFun := Nat.succ, inj' := Nat.succ_injective } n = ↑(addLeftEmbedding (length [x])) n
[PROOFSTEP]
exact add_comm n 1
[GOAL]
M : Type u_1
inst✝⁴ : Zero M
l : List M
inst✝³ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun i => getD (xs ++ [x]) i 0 ≠ 0
inst✝ : DecidablePred fun i => getD xs i 0 ≠ 0
⊢ toFinsupp (xs ++ [x]) = toFinsupp xs + Finsupp.single (length xs) x
[PROOFSTEP]
classical rw [toFinsupp_append, toFinsupp_singleton, Finsupp.embDomain_single, addLeftEmbedding_apply, add_zero]
[GOAL]
M : Type u_1
inst✝⁴ : Zero M
l : List M
inst✝³ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun i => getD (xs ++ [x]) i 0 ≠ 0
inst✝ : DecidablePred fun i => getD xs i 0 ≠ 0
⊢ toFinsupp (xs ++ [x]) = toFinsupp xs + Finsupp.single (length xs) x
[PROOFSTEP]
rw [toFinsupp_append, toFinsupp_singleton, Finsupp.embDomain_single, addLeftEmbedding_apply, add_zero]
[GOAL]
M : Type u_1
inst✝³ : Zero M
l✝ : List M
inst✝² : DecidablePred fun x => getD l✝ x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝¹ : AddMonoid R
l : List R
inst✝ : DecidablePred fun x => getD l x 0 ≠ 0
⊢ toFinsupp l = sum (map (fun nr => Finsupp.single nr.fst nr.snd) (enum l))
[PROOFSTEP]
revert l
[GOAL]
M : Type u_1
inst✝² : Zero M
l : List M
inst✝¹ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝ : AddMonoid R
⊢ ∀ (l : List R) [inst : DecidablePred fun x => getD l x 0 ≠ 0],
    toFinsupp l = sum (map (fun nr => Finsupp.single nr.fst nr.snd) (enum l))
[PROOFSTEP]
intro l
[GOAL]
M : Type u_1
inst✝² : Zero M
l✝ : List M
inst✝¹ : DecidablePred fun x => getD l✝ x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝ : AddMonoid R
l : List R
⊢ ∀ [inst : DecidablePred fun x => getD l x 0 ≠ 0],
    toFinsupp l = sum (map (fun nr => Finsupp.single nr.fst nr.snd) (enum l))
[PROOFSTEP]
induction l using List.reverseRecOn with
| H0 => exact toFinsupp_nil
| H1 x xs ih => classical simp [toFinsupp_concat_eq_toFinsupp_add_single, enum_append, ih]
[GOAL]
M : Type u_1
inst✝² : Zero M
l✝ : List M
inst✝¹ : DecidablePred fun x => getD l✝ x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝ : AddMonoid R
l : List R
⊢ ∀ [inst : DecidablePred fun x => getD l x 0 ≠ 0],
    toFinsupp l = sum (map (fun nr => Finsupp.single nr.fst nr.snd) (enum l))
[PROOFSTEP]
induction l using List.reverseRecOn with
| H0 => exact toFinsupp_nil
| H1 x xs ih => classical simp [toFinsupp_concat_eq_toFinsupp_add_single, enum_append, ih]
[GOAL]
case H0
M : Type u_1
inst✝² : Zero M
l : List M
inst✝¹ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝ : AddMonoid R
⊢ ∀ [inst : DecidablePred fun x => getD [] x 0 ≠ 0],
    toFinsupp [] = sum (map (fun nr => Finsupp.single nr.fst nr.snd) (enum []))
[PROOFSTEP]

| H0 => exact toFinsupp_nil
[GOAL]
case H0
M : Type u_1
inst✝² : Zero M
l : List M
inst✝¹ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝ : AddMonoid R
⊢ ∀ [inst : DecidablePred fun x => getD [] x 0 ≠ 0],
    toFinsupp [] = sum (map (fun nr => Finsupp.single nr.fst nr.snd) (enum []))
[PROOFSTEP]
exact toFinsupp_nil
[GOAL]
case H1
M : Type u_1
inst✝² : Zero M
l : List M
inst✝¹ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝ : AddMonoid R
x : List R
xs : R
ih :
  ∀ [inst : DecidablePred fun x_1 => getD x x_1 0 ≠ 0],
    toFinsupp x = sum (map (fun nr => Finsupp.single nr.fst nr.snd) (enum x))
⊢ ∀ [inst : DecidablePred fun x_1 => getD (x ++ [xs]) x_1 0 ≠ 0],
    toFinsupp (x ++ [xs]) = sum (map (fun nr => Finsupp.single nr.fst nr.snd) (enum (x ++ [xs])))
[PROOFSTEP]

| H1 x xs ih => classical simp [toFinsupp_concat_eq_toFinsupp_add_single, enum_append, ih]
[GOAL]
case H1
M : Type u_1
inst✝² : Zero M
l : List M
inst✝¹ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝ : AddMonoid R
x : List R
xs : R
ih :
  ∀ [inst : DecidablePred fun x_1 => getD x x_1 0 ≠ 0],
    toFinsupp x = sum (map (fun nr => Finsupp.single nr.fst nr.snd) (enum x))
⊢ ∀ [inst : DecidablePred fun x_1 => getD (x ++ [xs]) x_1 0 ≠ 0],
    toFinsupp (x ++ [xs]) = sum (map (fun nr => Finsupp.single nr.fst nr.snd) (enum (x ++ [xs])))
[PROOFSTEP]
classical simp [toFinsupp_concat_eq_toFinsupp_add_single, enum_append, ih]
[GOAL]
case H1
M : Type u_1
inst✝² : Zero M
l : List M
inst✝¹ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝ : AddMonoid R
x : List R
xs : R
ih :
  ∀ [inst : DecidablePred fun x_1 => getD x x_1 0 ≠ 0],
    toFinsupp x = sum (map (fun nr => Finsupp.single nr.fst nr.snd) (enum x))
⊢ ∀ [inst : DecidablePred fun x_1 => getD (x ++ [xs]) x_1 0 ≠ 0],
    toFinsupp (x ++ [xs]) = sum (map (fun nr => Finsupp.single nr.fst nr.snd) (enum (x ++ [xs])))
[PROOFSTEP]
simp [toFinsupp_concat_eq_toFinsupp_add_single, enum_append, ih]


[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
⊢ (a₁, b₁) < (a₂, b₂) ↔ (a₁, b₁) ≤ (a₂, b₂) ∧ ¬(a₂, b₂) ≤ (a₁, b₁)
[PROOFSTEP]
constructor
[GOAL]
case mp
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
⊢ (a₁, b₁) < (a₂, b₂) → (a₁, b₁) ≤ (a₂, b₂) ∧ ¬(a₂, b₂) ≤ (a₁, b₁)
[PROOFSTEP]
rintro (⟨_, _, hlt⟩ | ⟨_, hlt⟩)
[GOAL]
case mp.left
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
hlt : a₁ < a₂
⊢ (a₁, b₁) ≤ (a₂, b₂) ∧ ¬(a₂, b₂) ≤ (a₁, b₁)
[PROOFSTEP]
constructor
[GOAL]
case mp.left.left
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
hlt : a₁ < a₂
⊢ (a₁, b₁) ≤ (a₂, b₂)
[PROOFSTEP]
exact left _ _ hlt
[GOAL]
case mp.left.right
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
hlt : a₁ < a₂
⊢ ¬(a₂, b₂) ≤ (a₁, b₁)
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case mp.left.right.left
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
hlt : a₁ < a₂
h✝ : a₂ < a₁
⊢ False
[PROOFSTEP]
apply lt_asymm hlt
[GOAL]
case mp.left.right.left
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
hlt : a₁ < a₂
h✝ : a₂ < a₁
⊢ a₂ < a₁
[PROOFSTEP]
assumption
[GOAL]
case mp.left.right.right
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
hlt : a₁ < a₁
h✝ : b₂ ≤ b₁
⊢ False
[PROOFSTEP]
exact lt_irrefl _ hlt
[GOAL]
case mp.right
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
hlt : b₁ < b₂
⊢ (a₁, b₁) ≤ (a₁, b₂) ∧ ¬(a₁, b₂) ≤ (a₁, b₁)
[PROOFSTEP]
constructor
[GOAL]
case mp.right.left
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
hlt : b₁ < b₂
⊢ (a₁, b₁) ≤ (a₁, b₂)
[PROOFSTEP]
right
[GOAL]
case mp.right.left.h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
hlt : b₁ < b₂
⊢ b₁ ≤ b₂
[PROOFSTEP]
rw [lt_iff_le_not_le] at hlt
[GOAL]
case mp.right.left.h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
hlt : b₁ ≤ b₂ ∧ ¬b₂ ≤ b₁
⊢ b₁ ≤ b₂
[PROOFSTEP]
exact hlt.1
[GOAL]
case mp.right.right
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
hlt : b₁ < b₂
⊢ ¬(a₁, b₂) ≤ (a₁, b₁)
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case mp.right.right.left
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
hlt : b₁ < b₂
h✝ : a₁ < a₁
⊢ False
[PROOFSTEP]
apply lt_irrefl a₁
[GOAL]
case mp.right.right.left
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
hlt : b₁ < b₂
h✝ : a₁ < a₁
⊢ a₁ < a₁
[PROOFSTEP]
assumption
[GOAL]
case mp.right.right.right
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
hlt : b₁ < b₂
h✝ : b₂ ≤ b₁
⊢ False
[PROOFSTEP]
rw [lt_iff_le_not_le] at hlt
[GOAL]
case mp.right.right.right
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
hlt : b₁ ≤ b₂ ∧ ¬b₂ ≤ b₁
h✝ : b₂ ≤ b₁
⊢ False
[PROOFSTEP]
apply hlt.2
[GOAL]
case mp.right.right.right
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
hlt : b₁ ≤ b₂ ∧ ¬b₂ ≤ b₁
h✝ : b₂ ≤ b₁
⊢ b₂ ≤ b₁
[PROOFSTEP]
assumption
[GOAL]
case mpr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
⊢ (a₁, b₁) ≤ (a₂, b₂) ∧ ¬(a₂, b₂) ≤ (a₁, b₁) → (a₁, b₁) < (a₂, b₂)
[PROOFSTEP]
rintro ⟨⟨⟩, h₂r⟩
[GOAL]
case mpr.intro.left
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h₂r : ¬(a₂, b₂) ≤ (a₁, b₁)
h✝ : a₁ < a₂
⊢ (a₁, b₁) < (a₂, b₂)
[PROOFSTEP]
left
[GOAL]
case mpr.intro.left.h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h₂r : ¬(a₂, b₂) ≤ (a₁, b₁)
h✝ : a₁ < a₂
⊢ a₁ < a₂
[PROOFSTEP]
assumption
[GOAL]
case mpr.intro.right
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
h₂r : ¬(a₁, b₂) ≤ (a₁, b₁)
h✝ : b₁ ≤ b₂
⊢ (a₁, b₁) < (a₁, b₂)
[PROOFSTEP]
right
[GOAL]
case mpr.intro.right.h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
h₂r : ¬(a₁, b₂) ≤ (a₁, b₁)
h✝ : b₁ ≤ b₂
⊢ b₁ < b₂
[PROOFSTEP]
rw [lt_iff_le_not_le]
[GOAL]
case mpr.intro.right.h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
h₂r : ¬(a₁, b₂) ≤ (a₁, b₁)
h✝ : b₁ ≤ b₂
⊢ b₁ ≤ b₂ ∧ ¬b₂ ≤ b₁
[PROOFSTEP]
constructor
[GOAL]
case mpr.intro.right.h.left
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
h₂r : ¬(a₁, b₂) ≤ (a₁, b₁)
h✝ : b₁ ≤ b₂
⊢ b₁ ≤ b₂
[PROOFSTEP]
assumption
[GOAL]
case mpr.intro.right.h.right
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
h₂r : ¬(a₁, b₂) ≤ (a₁, b₁)
h✝ : b₁ ≤ b₂
⊢ ¬b₂ ≤ b₁
[PROOFSTEP]
intro h
[GOAL]
case mpr.intro.right.h.right
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
h₂r : ¬(a₁, b₂) ≤ (a₁, b₁)
h✝ : b₁ ≤ b₂
h : b₂ ≤ b₁
⊢ False
[PROOFSTEP]
apply h₂r
[GOAL]
case mpr.intro.right.h.right
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
h₂r : ¬(a₁, b₂) ≤ (a₁, b₁)
h✝ : b₁ ≤ b₂
h : b₂ ≤ b₁
⊢ (a₁, b₂) ≤ (a₁, b₁)
[PROOFSTEP]
right
[GOAL]
case mpr.intro.right.h.right.h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
h₂r : ¬(a₁, b₂) ≤ (a₁, b₁)
h✝ : b₁ ≤ b₂
h : b₂ ≤ b₁
⊢ b₂ ≤ b₁
[PROOFSTEP]
exact h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
⊢ Monotone ↑toLex
[PROOFSTEP]
rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ ⟨ha, hb⟩
[GOAL]
case mk.mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
ha : (a₁, b₁).fst ≤ (a₂, b₂).fst
hb : (a₁, b₁).snd ≤ (a₂, b₂).snd
⊢ ↑toLex (a₁, b₁) ≤ ↑toLex (a₂, b₂)
[PROOFSTEP]
obtain rfl | ha : a₁ = a₂ ∨ _ := ha.eq_or_lt
[GOAL]
case mk.mk.intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ b₂ : β
ha : (a₁, b₁).fst ≤ (a₁, b₂).fst
hb : (a₁, b₁).snd ≤ (a₁, b₂).snd
⊢ ↑toLex (a₁, b₁) ≤ ↑toLex (a₁, b₂)
[PROOFSTEP]
exact right _ hb
[GOAL]
case mk.mk.intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
ha✝ : (a₁, b₁).fst ≤ (a₂, b₂).fst
hb : (a₁, b₁).snd ≤ (a₂, b₂).snd
ha : (a₁, b₁).fst < (a₂, b₂).fst
⊢ ↑toLex (a₁, b₁) ≤ ↑toLex (a₂, b₂)
[PROOFSTEP]
exact left _ _ ha
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
⊢ StrictMono ↑toLex
[PROOFSTEP]
rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ h
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : (a₁, b₁) < (a₂, b₂)
⊢ ↑toLex (a₁, b₁) < ↑toLex (a₂, b₂)
[PROOFSTEP]
obtain rfl | ha : a₁ = a₂ ∨ _ := h.le.1.eq_or_lt
[GOAL]
case mk.mk.inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ b₂ : β
h : (a₁, b₁) < (a₁, b₂)
⊢ ↑toLex (a₁, b₁) < ↑toLex (a₁, b₂)
[PROOFSTEP]
exact right _ (Prod.mk_lt_mk_iff_right.1 h)
[GOAL]
case mk.mk.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : (a₁, b₁) < (a₂, b₂)
ha : (a₁, b₁).fst < (a₂, b₂).fst
⊢ ↑toLex (a₁, b₁) < ↑toLex (a₂, b₂)
[PROOFSTEP]
exact left _ _ ha
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
src✝ : Preorder (Lex (α × β)) := preorder α β
⊢ ∀ (a b : Lex (α × β)), a ≤ b → b ≤ a → a = b
[PROOFSTEP]
haveI : IsStrictOrder α (· < ·) := { irrefl := lt_irrefl, trans := fun _ _ _ => lt_trans }
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
src✝ : Preorder (Lex (α × β)) := preorder α β
this : IsStrictOrder α fun x x_1 => x < x_1
⊢ ∀ (a b : Lex (α × β)), a ≤ b → b ≤ a → a = b
[PROOFSTEP]
haveI : IsAntisymm β (· ≤ ·) := ⟨fun _ _ => le_antisymm⟩
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
src✝ : Preorder (Lex (α × β)) := preorder α β
this✝ : IsStrictOrder α fun x x_1 => x < x_1
this : IsAntisymm β fun x x_1 => x ≤ x_1
⊢ ∀ (a b : Lex (α × β)), a ≤ b → b ≤ a → a = b
[PROOFSTEP]
exact @antisymm _ (Prod.Lex _ _) _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
⊢ ∀ (a₁ a₂ : Lex (α × β)), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
[PROOFSTEP]
rintro _ _ (@⟨a₁, b₁, a₂, b₂, h⟩ | @⟨a, b₁, b₂, h⟩)
[GOAL]
case left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : a₁ < a₂
⊢ ∃ a, (a₁, b₁) < a ∧ a < (a₂, b₂)
[PROOFSTEP]
obtain ⟨c, h₁, h₂⟩ := exists_between h
[GOAL]
case left.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : a₁ < a₂
c : α
h₁ : a₁ < c
h₂ : c < a₂
⊢ ∃ a, (a₁, b₁) < a ∧ a < (a₂, b₂)
[PROOFSTEP]
exact ⟨(c, b₁), left _ _ h₁, left _ _ h₂⟩
[GOAL]
case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a : α
b₁ b₂ : β
h : b₁ < b₂
⊢ ∃ a_1, (a, b₁) < a_1 ∧ a_1 < (a, b₂)
[PROOFSTEP]
obtain ⟨c, h₁, h₂⟩ := exists_between h
[GOAL]
case right.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a : α
b₁ b₂ : β
h : b₁ < b₂
c : β
h₁ : b₁ < c
h₂ : c < b₂
⊢ ∃ a_1, (a, b₁) < a_1 ∧ a_1 < (a, b₂)
[PROOFSTEP]
exact ⟨(a, c), right _ h₁, right _ h₂⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder α
⊢ ∀ (a : Lex (α × β)), ∃ b, a < b
[PROOFSTEP]
rintro ⟨a, b⟩
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder α
a : α
b : β
⊢ ∃ b_1, (a, b) < b_1
[PROOFSTEP]
obtain ⟨c, h⟩ := exists_gt a
[GOAL]
case mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder α
a : α
b : β
c : α
h : a < c
⊢ ∃ b_1, (a, b) < b_1
[PROOFSTEP]
exact ⟨⟨c, b⟩, left _ _ h⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMinOrder α
⊢ ∀ (a : Lex (α × β)), ∃ b, b < a
[PROOFSTEP]
rintro ⟨a, b⟩
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMinOrder α
a : α
b : β
⊢ ∃ b_1, b_1 < (a, b)
[PROOFSTEP]
obtain ⟨c, h⟩ := exists_lt a
[GOAL]
case mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMinOrder α
a : α
b : β
c : α
h : c < a
⊢ ∃ b_1, b_1 < (a, b)
[PROOFSTEP]
exact ⟨⟨c, b⟩, left _ _ h⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
⊢ ∀ (a : Lex (α × β)), ∃ b, a < b
[PROOFSTEP]
rintro ⟨a, b⟩
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
a : α
b : β
⊢ ∃ b_1, (a, b) < b_1
[PROOFSTEP]
obtain ⟨c, h⟩ := exists_gt b
[GOAL]
case mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
a : α
b c : β
h : b < c
⊢ ∃ b_1, (a, b) < b_1
[PROOFSTEP]
exact ⟨⟨a, c⟩, right _ h⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMinOrder β
⊢ ∀ (a : Lex (α × β)), ∃ b, b < a
[PROOFSTEP]
rintro ⟨a, b⟩
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMinOrder β
a : α
b : β
⊢ ∃ b_1, b_1 < (a, b)
[PROOFSTEP]
obtain ⟨c, h⟩ := exists_lt b
[GOAL]
case mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMinOrder β
a : α
b c : β
h : c < b
⊢ ∃ b_1, b_1 < (a, b)
[PROOFSTEP]
exact ⟨⟨a, c⟩, right _ h⟩


[GOAL]
ι : Type u
α : ι → Type v
i✝ j✝ : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
is : List ι
v : TProd α (i :: is)
j : ι
hj : j ∈ i :: is
hji : j = i
⊢ α j
[PROOFSTEP]
subst hji
[GOAL]
ι : Type u
α : ι → Type v
i j✝ : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
is : List ι
j : ι
v : TProd α (j :: is)
hj : j ∈ j :: is
⊢ α j
[PROOFSTEP]
exact v.1
[GOAL]
ι : Type u
α : ι → Type v
i j : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
v : TProd α (i :: l)
⊢ TProd.elim v (_ : i ∈ i :: l) = v.fst
[PROOFSTEP]
simp [TProd.elim]
[GOAL]
ι : Type u
α : ι → Type v
i j : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
hj : j ∈ i :: l
hji : j ≠ i
v : TProd α (i :: l)
⊢ TProd.elim v hj = TProd.elim v.snd (_ : j ∈ l)
[PROOFSTEP]
simp [TProd.elim, hji]
[GOAL]
ι : Type u
α : ι → Type v
i j : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
hl : Nodup (i :: l)
hj : j ∈ l
v : TProd α (i :: l)
⊢ TProd.elim v (_ : j ∈ i :: l) = TProd.elim v.snd hj
[PROOFSTEP]
apply elim_of_ne
[GOAL]
case hji
ι : Type u
α : ι → Type v
i j : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
hl : Nodup (i :: l)
hj : j ∈ l
v : TProd α (i :: l)
⊢ j ≠ i
[PROOFSTEP]
rintro rfl
[GOAL]
case hji
ι : Type u
α : ι → Type v
j : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
hj : j ∈ l
hl : Nodup (j :: l)
v : TProd α (j :: l)
⊢ False
[PROOFSTEP]
exact hl.not_mem hj
[GOAL]
ι : Type u
α : ι → Type v
i✝ j✝ : ι
l : List ι
f✝ : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
⊢ TProd.elim (TProd.mk (i :: is) f) hj = f j
[PROOFSTEP]
by_cases hji : j = i
[GOAL]
case pos
ι : Type u
α : ι → Type v
i✝ j✝ : ι
l : List ι
f✝ : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
hji : j = i
⊢ TProd.elim (TProd.mk (i :: is) f) hj = f j
[PROOFSTEP]
subst hji
[GOAL]
case pos
ι : Type u
α : ι → Type v
i j✝ : ι
l : List ι
f✝ : (i : ι) → α i
inst✝ : DecidableEq ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ j :: is
⊢ TProd.elim (TProd.mk (j :: is) f) hj = f j
[PROOFSTEP]
simp
[GOAL]
case neg
ι : Type u
α : ι → Type v
i✝ j✝ : ι
l : List ι
f✝ : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
hji : ¬j = i
⊢ TProd.elim (TProd.mk (i :: is) f) hj = f j
[PROOFSTEP]
rw [TProd.elim_of_ne _ hji, snd_mk, elim_mk is]
[GOAL]
ι : Type u
α : ι → Type v
i✝ j : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : Nodup (i :: is)
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), TProd.elim v hi = TProd.elim w hi
⊢ v = w
[PROOFSTEP]
apply Prod.ext
[GOAL]
case h₁
ι : Type u
α : ι → Type v
i✝ j : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : Nodup (i :: is)
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), TProd.elim v hi = TProd.elim w hi
⊢ v.fst = w.fst
case h₂
ι : Type u
α : ι → Type v
i✝ j : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : Nodup (i :: is)
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), TProd.elim v hi = TProd.elim w hi
⊢ v.snd = w.snd
[PROOFSTEP]
rw [← elim_self v, hvw, elim_self]
[GOAL]
case h₂
ι : Type u
α : ι → Type v
i✝ j : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : Nodup (i :: is)
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), TProd.elim v hi = TProd.elim w hi
⊢ v.snd = w.snd
[PROOFSTEP]
refine' ext (nodup_cons.mp hl).2 fun j hj => _
[GOAL]
case h₂
ι : Type u
α : ι → Type v
i✝ j✝ : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : Nodup (i :: is)
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), TProd.elim v hi = TProd.elim w hi
j : ι
hj : j ∈ is
⊢ TProd.elim v.snd hj = TProd.elim w.snd hj
[PROOFSTEP]
rw [← elim_of_mem hl, hvw, elim_of_mem hl]
[GOAL]
ι : Type u
α : ι → Type v
i✝ j : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
hnd : Nodup l
h : ∀ (i : ι), i ∈ l
v : TProd α l
i : ι
hi : i ∈ l
⊢ TProd.elim (TProd.mk l (TProd.elim' h v)) hi = TProd.elim v hi
[PROOFSTEP]
simp [elim_mk]
[GOAL]
ι : Type u
α : ι → Type v
i j : ι
l : List ι
f : (i : ι) → α i
t : (i : ι) → Set (α i)
⊢ TProd.mk [] ⁻¹' Set.tprod [] t = pi {i | i ∈ []} t
[PROOFSTEP]
simp [Set.tprod]
[GOAL]
ι : Type u
α : ι → Type v
i✝ j : ι
l✝ : List ι
f : (i : ι) → α i
i : ι
l : List ι
t : (i : ι) → Set (α i)
⊢ TProd.mk (i :: l) ⁻¹' Set.tprod (i :: l) t = pi {i_1 | i_1 ∈ i :: l} t
[PROOFSTEP]
ext f
[GOAL]
case h
ι : Type u
α : ι → Type v
i✝ j : ι
l✝ : List ι
f✝ : (i : ι) → α i
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ f ∈ TProd.mk (i :: l) ⁻¹' Set.tprod (i :: l) t ↔ f ∈ pi {i_1 | i_1 ∈ i :: l} t
[PROOFSTEP]
have h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ i : ι, i ∈ l → f i ∈ t i :=
  by
  change f ∈ TProd.mk l ⁻¹' Set.tprod l t ↔ f ∈ {x | x ∈ l}.pi t
  rw [mk_preimage_tprod l t]
    -- `simp [Set.TProd, TProd.mk, this]` can close this goal but is slow.
[GOAL]
ι : Type u
α : ι → Type v
i✝ j : ι
l✝ : List ι
f✝ : (i : ι) → α i
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
[PROOFSTEP]
change f ∈ TProd.mk l ⁻¹' Set.tprod l t ↔ f ∈ {x | x ∈ l}.pi t
[GOAL]
ι : Type u
α : ι → Type v
i✝ j : ι
l✝ : List ι
f✝ : (i : ι) → α i
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ f ∈ TProd.mk l ⁻¹' Set.tprod l t ↔ f ∈ pi {x | x ∈ l} t
[PROOFSTEP]
rw [mk_preimage_tprod l t]
  -- `simp [Set.TProd, TProd.mk, this]` can close this goal but is slow.
[GOAL]
case h
ι : Type u
α : ι → Type v
i✝ j : ι
l✝ : List ι
f✝ : (i : ι) → α i
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
⊢ f ∈ TProd.mk (i :: l) ⁻¹' Set.tprod (i :: l) t ↔ f ∈ pi {i_1 | i_1 ∈ i :: l} t
[PROOFSTEP]
rw [Set.tprod, TProd.mk, mem_preimage, mem_pi, prod_mk_mem_set_prod_eq]
[GOAL]
case h
ι : Type u
α : ι → Type v
i✝ j : ι
l✝ : List ι
f✝ : (i : ι) → α i
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
⊢ f i ∈ t i ∧ TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i_1 : ι), i_1 ∈ {i_2 | i_2 ∈ i :: l} → f i_1 ∈ t i_1
[PROOFSTEP]
simp_rw [mem_setOf_eq, mem_cons]
[GOAL]
case h
ι : Type u
α : ι → Type v
i✝ j : ι
l✝ : List ι
f✝ : (i : ι) → α i
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
⊢ f i ∈ t i ∧ TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i_1 : ι), i_1 = i ∨ i_1 ∈ l → f i_1 ∈ t i_1
[PROOFSTEP]
rw [forall_eq_or_imp, and_congr_right_iff]
[GOAL]
case h
ι : Type u
α : ι → Type v
i✝ j : ι
l✝ : List ι
f✝ : (i : ι) → α i
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
⊢ f i ∈ t i → (TProd.mk l f ∈ Set.tprod l t ↔ ∀ (a : ι), a ∈ l → f a ∈ t a)
[PROOFSTEP]
exact fun _ => h
[GOAL]
ι : Type u
α : ι → Type v
i j : ι
l✝ : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
l : List ι
hnd : Nodup l
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
⊢ TProd.elim' h ⁻¹' pi univ t = Set.tprod l t
[PROOFSTEP]
have h2 : {i | i ∈ l} = univ := by
  ext i
  simp [h]
[GOAL]
ι : Type u
α : ι → Type v
i j : ι
l✝ : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
l : List ι
hnd : Nodup l
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
⊢ {i | i ∈ l} = univ
[PROOFSTEP]
ext i
[GOAL]
case h
ι : Type u
α : ι → Type v
i✝ j : ι
l✝ : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
l : List ι
hnd : Nodup l
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
i : ι
⊢ i ∈ {i | i ∈ l} ↔ i ∈ univ
[PROOFSTEP]
simp [h]
[GOAL]
ι : Type u
α : ι → Type v
i j : ι
l✝ : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
l : List ι
hnd : Nodup l
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
h2 : {i | i ∈ l} = univ
⊢ TProd.elim' h ⁻¹' pi univ t = Set.tprod l t
[PROOFSTEP]
rw [← h2, ← mk_preimage_tprod, preimage_preimage]
[GOAL]
ι : Type u
α : ι → Type v
i j : ι
l✝ : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
l : List ι
hnd : Nodup l
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
h2 : {i | i ∈ l} = univ
⊢ (fun x => TProd.mk l (TProd.elim' h x)) ⁻¹' Set.tprod l t = Set.tprod l t
[PROOFSTEP]
simp only [TProd.mk_elim hnd h]
[GOAL]
ι : Type u
α : ι → Type v
i j : ι
l✝ : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
l : List ι
hnd : Nodup l
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
h2 : {i | i ∈ l} = univ
⊢ (fun x => x) ⁻¹' Set.tprod l t = Set.tprod l t
[PROOFSTEP]
dsimp
[GOAL]
ι : Type u
α : ι → Type v
i j : ι
l✝ : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
l : List ι
hnd : Nodup l
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
h2 : {i | i ∈ l} = univ
⊢ Set.tprod l t = Set.tprod l t
[PROOFSTEP]
rfl