[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
h : ¬a ∈ s
⊢ fold op b f (cons a s h) = op (f a) (fold op b f s)
[PROOFSTEP]
dsimp only [fold]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
h : ¬a ∈ s
⊢ Multiset.fold op b (Multiset.map f (cons a s h).val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
[PROOFSTEP]
rw [cons_val, Multiset.map_cons, fold_cons_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)
[PROOFSTEP]
unfold fold
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ Multiset.fold op b (Multiset.map f (insert a s).val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
[PROOFSTEP]
rw [insert_val, ndinsert_of_not_mem h, Multiset.map_cons, fold_cons_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
g : γ ↪ α
s : Finset γ
⊢ fold op b f (map g s) = fold op b (f ∘ ↑g) s
[PROOFSTEP]
simp only [fold, map, Multiset.map_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
inst✝ : DecidableEq α
g : γ → α
s : Finset γ
H : ∀ (x : γ), x ∈ s → ∀ (y : γ), y ∈ s → g x = g y → x = y
⊢ fold op b f (image g s) = fold op b (f ∘ g) s
[PROOFSTEP]
simp only [fold, image_val_of_injOn H, Multiset.map_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
g : α → β
H : ∀ (x : α), x ∈ s → f x = g x
⊢ fold op b f s = fold op b g s
[PROOFSTEP]
rw [fold, fold, map_congr rfl H]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f✝ : α → β
b : β
s : Finset α
a : α
f g : α → β
b₁ b₂ : β
⊢ fold op (op b₁ b₂) (fun x => op (f x) (g x)) s = op (fold op b₁ f s) (fold op b₂ g s)
[PROOFSTEP]
simp only [fold, fold_distrib]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
hd : Decidable (s = ∅)
c : β
h : op c (op b c) = op b c
⊢ fold op b (fun x => c) s = if s = ∅ then b else op b c
[PROOFSTEP]
classical
induction' s using Finset.induction_on with x s hx IH generalizing hd
· simp
· simp only [Finset.fold_insert hx, IH, if_false, Finset.insert_ne_empty]
  split_ifs
  · rw [hc.comm]
  · exact h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
hd : Decidable (s = ∅)
c : β
h : op c (op b c) = op b c
⊢ fold op b (fun x => c) s = if s = ∅ then b else op b c
[PROOFSTEP]
induction' s using Finset.induction_on with x s hx IH generalizing hd
[GOAL]
case empty
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
hd✝ : Decidable (s = ∅)
c : β
h : op c (op b c) = op b c
hd : Decidable (∅ = ∅)
⊢ fold op b (fun x => c) ∅ = if ∅ = ∅ then b else op b c
[PROOFSTEP]
simp
[GOAL]
case insert
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
hd✝ : Decidable (s✝ = ∅)
c : β
h : op c (op b c) = op b c
x : α
s : Finset α
hx : ¬x ∈ s
IH : ∀ [hd : Decidable (s = ∅)], fold op b (fun x => c) s = if s = ∅ then b else op b c
hd : Decidable (insert x s = ∅)
⊢ fold op b (fun x => c) (insert x s) = if insert x s = ∅ then b else op b c
[PROOFSTEP]
simp only [Finset.fold_insert hx, IH, if_false, Finset.insert_ne_empty]
[GOAL]
case insert
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
hd✝ : Decidable (s✝ = ∅)
c : β
h : op c (op b c) = op b c
x : α
s : Finset α
hx : ¬x ∈ s
IH : ∀ [hd : Decidable (s = ∅)], fold op b (fun x => c) s = if s = ∅ then b else op b c
hd : Decidable (insert x s = ∅)
⊢ op c (if s = ∅ then b else op b c) = op b c
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
hd✝ : Decidable (s✝ = ∅)
c : β
h : op c (op b c) = op b c
x : α
s : Finset α
hx : ¬x ∈ s
IH : ∀ [hd : Decidable (s = ∅)], fold op b (fun x => c) s = if s = ∅ then b else op b c
hd : Decidable (insert x s = ∅)
h✝ : s = ∅
⊢ op c b = op b c
[PROOFSTEP]
rw [hc.comm]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
hd✝ : Decidable (s✝ = ∅)
c : β
h : op c (op b c) = op b c
x : α
s : Finset α
hx : ¬x ∈ s
IH : ∀ [hd : Decidable (s = ∅)], fold op b (fun x => c) s = if s = ∅ then b else op b c
hd : Decidable (insert x s = ∅)
h✝ : ¬s = ∅
⊢ op c (op b c) = op b c
[PROOFSTEP]
exact h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
op' : γ → γ → γ
inst✝¹ : IsCommutative γ op'
inst✝ : IsAssociative γ op'
m : β → γ
hm : ∀ (x y : β), m (op x y) = op' (m x) (m y)
⊢ fold op' (m b) (fun x => m (f x)) s = m (fold op b f s)
[PROOFSTEP]
rw [fold, fold, ← Multiset.fold_hom op hm, Multiset.map_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
op' : γ → γ → γ
inst✝¹ : IsCommutative γ op'
inst✝ : IsAssociative γ op'
m : β → γ
hm : ∀ (x y : β), m (op x y) = op' (m x) (m y)
⊢ Multiset.fold op' (m b) (Multiset.map (fun x => m (f x)) s.val) = Multiset.fold op' (m b) (Multiset.map (m ∘ f) s.val)
[PROOFSTEP]
simp only [Function.comp_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
s₁ s₂ : Finset α
b₁ b₂ : β
⊢ op (fold op b₁ f (s₁ ∪ s₂)) (fold op b₂ f (s₁ ∩ s₂)) = op (fold op b₂ f s₁) (fold op b₁ f s₂)
[PROOFSTEP]
unfold fold
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
s₁ s₂ : Finset α
b₁ b₂ : β
⊢ op (Multiset.fold op b₁ (Multiset.map f (s₁ ∪ s₂).val)) (Multiset.fold op b₂ (Multiset.map f (s₁ ∩ s₂).val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
[PROOFSTEP]
rw [← fold_add op, ← Multiset.map_add, union_val, inter_val, union_add_inter, Multiset.map_add, hc.comm, fold_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
hi : IsIdempotent β op
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)
[PROOFSTEP]
by_cases h : a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
hi : IsIdempotent β op
h : a ∈ s
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)
[PROOFSTEP]
rw [← insert_erase h]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
hi : IsIdempotent β op
h : a ∈ s
⊢ fold op b f (insert a (insert a (erase s a))) = op (f a) (fold op b f (insert a (erase s a)))
[PROOFSTEP]
simp [← ha.assoc, hi.idempotent]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
hi : IsIdempotent β op
h : ¬a ∈ s
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)
[PROOFSTEP]
apply fold_insert h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
inst✝ : DecidableEq α
g : γ → α
s : Finset γ
hi : IsIdempotent β op
⊢ fold op b f (image g s) = fold op b (f ∘ g) s
[PROOFSTEP]
induction' s using Finset.cons_induction with x xs hx ih
[GOAL]
case empty
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
g : γ → α
hi : IsIdempotent β op
⊢ fold op b f (image g ∅) = fold op b (f ∘ g) ∅
[PROOFSTEP]
rw [fold_empty, image_empty, fold_empty]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
g : γ → α
hi : IsIdempotent β op
x : γ
xs : Finset γ
hx : ¬x ∈ xs
ih : fold op b f (image g xs) = fold op b (f ∘ g) xs
⊢ fold op b f (image g (cons x xs hx)) = fold op b (f ∘ g) (cons x xs hx)
[PROOFSTEP]
haveI := Classical.decEq γ
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
g : γ → α
hi : IsIdempotent β op
x : γ
xs : Finset γ
hx : ¬x ∈ xs
ih : fold op b f (image g xs) = fold op b (f ∘ g) xs
this : DecidableEq γ
⊢ fold op b f (image g (cons x xs hx)) = fold op b (f ∘ g) (cons x xs hx)
[PROOFSTEP]
rw [fold_cons, cons_eq_insert, image_insert, fold_insert_idem, ih]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
g : γ → α
hi : IsIdempotent β op
x : γ
xs : Finset γ
hx : ¬x ∈ xs
ih : fold op b f (image g xs) = fold op b (f ∘ g) xs
this : DecidableEq γ
⊢ op (f (g x)) (fold op b (f ∘ g) xs) = op ((f ∘ g) x) (fold op b (f ∘ g) xs)
[PROOFSTEP]
simp only [Function.comp_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
⊢ fold op b (fun i => if p i then f i else g i) s =
    op (fold op b f (filter p s)) (fold op b g (filter (fun i => ¬p i) s))
[PROOFSTEP]
classical
induction' s using Finset.induction_on with x s hx IH
· simp [hb]
· simp only [Finset.fold_insert hx]
  split_ifs with h
  · have : x ∉ Finset.filter p s := by simp [hx]
    simp [Finset.filter_insert, h, Finset.fold_insert this, ha.assoc, IH]
  · have : x ∉ Finset.filter (fun i => ¬p i) s := by simp [hx]
    simp [Finset.filter_insert, h, Finset.fold_insert this, IH, ← ha.assoc, hc.comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
⊢ fold op b (fun i => if p i then f i else g i) s =
    op (fold op b f (filter p s)) (fold op b g (filter (fun i => ¬p i) s))
[PROOFSTEP]
induction' s using Finset.induction_on with x s hx IH
[GOAL]
case empty
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
⊢ fold op b (fun i => if p i then f i else g i) ∅ =
    op (fold op b f (filter p ∅)) (fold op b g (filter (fun i => ¬p i) ∅))
[PROOFSTEP]
simp [hb]
[GOAL]
case insert
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : ¬x ∈ s
IH :
  fold op b (fun i => if p i then f i else g i) s =
    op (fold op b f (filter p s)) (fold op b g (filter (fun i => ¬p i) s))
⊢ fold op b (fun i => if p i then f i else g i) (insert x s) =
    op (fold op b f (filter p (insert x s))) (fold op b g (filter (fun i => ¬p i) (insert x s)))
[PROOFSTEP]
simp only [Finset.fold_insert hx]
[GOAL]
case insert
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : ¬x ∈ s
IH :
  fold op b (fun i => if p i then f i else g i) s =
    op (fold op b f (filter p s)) (fold op b g (filter (fun i => ¬p i) s))
⊢ op (if p x then f x else g x) (fold op b (fun i => if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g (filter (fun i => ¬p i) (insert x s)))
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : ¬x ∈ s
IH :
  fold op b (fun i => if p i then f i else g i) s =
    op (fold op b f (filter p s)) (fold op b g (filter (fun i => ¬p i) s))
h : p x
⊢ op (f x) (fold op b (fun i => if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g (filter (fun i => ¬p i) (insert x s)))
[PROOFSTEP]
have : x ∉ Finset.filter p s := by simp [hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : ¬x ∈ s
IH :
  fold op b (fun i => if p i then f i else g i) s =
    op (fold op b f (filter p s)) (fold op b g (filter (fun i => ¬p i) s))
h : p x
⊢ ¬x ∈ filter p s
[PROOFSTEP]
simp [hx]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : ¬x ∈ s
IH :
  fold op b (fun i => if p i then f i else g i) s =
    op (fold op b f (filter p s)) (fold op b g (filter (fun i => ¬p i) s))
h : p x
this : ¬x ∈ filter p s
⊢ op (f x) (fold op b (fun i => if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g (filter (fun i => ¬p i) (insert x s)))
[PROOFSTEP]
simp [Finset.filter_insert, h, Finset.fold_insert this, ha.assoc, IH]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : ¬x ∈ s
IH :
  fold op b (fun i => if p i then f i else g i) s =
    op (fold op b f (filter p s)) (fold op b g (filter (fun i => ¬p i) s))
h : ¬p x
⊢ op (g x) (fold op b (fun i => if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g (filter (fun i => ¬p i) (insert x s)))
[PROOFSTEP]
have : x ∉ Finset.filter (fun i => ¬p i) s := by simp [hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : ¬x ∈ s
IH :
  fold op b (fun i => if p i then f i else g i) s =
    op (fold op b f (filter p s)) (fold op b g (filter (fun i => ¬p i) s))
h : ¬p x
⊢ ¬x ∈ filter (fun i => ¬p i) s
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : ¬x ∈ s
IH :
  fold op b (fun i => if p i then f i else g i) s =
    op (fold op b f (filter p s)) (fold op b g (filter (fun i => ¬p i) s))
h : ¬p x
this : ¬x ∈ filter (fun i => ¬p i) s
⊢ op (g x) (fold op b (fun i => if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g (filter (fun i => ¬p i) (insert x s)))
[PROOFSTEP]
simp [Finset.filter_insert, h, Finset.fold_insert this, IH, ← ha.assoc, hc.comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
⊢ r c (fold op b f s) ↔ r c b ∧ ∀ (x : α), x ∈ s → r c (f x)
[PROOFSTEP]
classical
induction' s using Finset.induction_on with a s ha IH
· simp
rw [Finset.fold_insert ha, hr, IH, ← and_assoc, @and_comm (r c (f a)), and_assoc]
apply and_congr Iff.rfl
constructor
· rintro ⟨h₁, h₂⟩
  intro b hb
  rw [Finset.mem_insert] at hb
  rcases hb with (rfl | hb) <;> solve_by_elim
· intro h
  constructor
  · exact h a (Finset.mem_insert_self _ _)
  · exact fun b hb => h b <| Finset.mem_insert_of_mem hb
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
⊢ r c (fold op b f s) ↔ r c b ∧ ∀ (x : α), x ∈ s → r c (f x)
[PROOFSTEP]
induction' s using Finset.induction_on with a s ha IH
[GOAL]
case empty
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
⊢ r c (fold op b f ∅) ↔ r c b ∧ ∀ (x : α), x ∈ ∅ → r c (f x)
[PROOFSTEP]
simp
[GOAL]
case insert
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ (x : α), x ∈ s → r c (f x)
⊢ r c (fold op b f (insert a s)) ↔ r c b ∧ ∀ (x : α), x ∈ insert a s → r c (f x)
[PROOFSTEP]
rw [Finset.fold_insert ha, hr, IH, ← and_assoc, @and_comm (r c (f a)), and_assoc]
[GOAL]
case insert
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ (x : α), x ∈ s → r c (f x)
⊢ (r c b ∧ r c (f a) ∧ ∀ (x : α), x ∈ s → r c (f x)) ↔ r c b ∧ ∀ (x : α), x ∈ insert a s → r c (f x)
[PROOFSTEP]
apply and_congr Iff.rfl
[GOAL]
case insert
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ (x : α), x ∈ s → r c (f x)
⊢ (r c (f a) ∧ ∀ (x : α), x ∈ s → r c (f x)) ↔ ∀ (x : α), x ∈ insert a s → r c (f x)
[PROOFSTEP]
constructor
[GOAL]
case insert.mp
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ (x : α), x ∈ s → r c (f x)
⊢ (r c (f a) ∧ ∀ (x : α), x ∈ s → r c (f x)) → ∀ (x : α), x ∈ insert a s → r c (f x)
[PROOFSTEP]
rintro ⟨h₁, h₂⟩
[GOAL]
case insert.mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ (x : α), x ∈ s → r c (f x)
h₁ : r c (f a)
h₂ : ∀ (x : α), x ∈ s → r c (f x)
⊢ ∀ (x : α), x ∈ insert a s → r c (f x)
[PROOFSTEP]
intro b hb
[GOAL]
case insert.mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b✝ : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b✝ f s) ↔ r c b✝ ∧ ∀ (x : α), x ∈ s → r c (f x)
h₁ : r c (f a)
h₂ : ∀ (x : α), x ∈ s → r c (f x)
b : α
hb : b ∈ insert a s
⊢ r c (f b)
[PROOFSTEP]
rw [Finset.mem_insert] at hb
[GOAL]
case insert.mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b✝ : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b✝ f s) ↔ r c b✝ ∧ ∀ (x : α), x ∈ s → r c (f x)
h₁ : r c (f a)
h₂ : ∀ (x : α), x ∈ s → r c (f x)
b : α
hb : b = a ∨ b ∈ s
⊢ r c (f b)
[PROOFSTEP]
rcases hb with (rfl | hb)
[GOAL]
case insert.mp.intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b✝ : β
s✝ : Finset α
a : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
s : Finset α
IH : r c (fold op b✝ f s) ↔ r c b✝ ∧ ∀ (x : α), x ∈ s → r c (f x)
h₂ : ∀ (x : α), x ∈ s → r c (f x)
b : α
ha : ¬b ∈ s
h₁ : r c (f b)
⊢ r c (f b)
[PROOFSTEP]
solve_by_elim
[GOAL]
case insert.mp.intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b✝ : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b✝ f s) ↔ r c b✝ ∧ ∀ (x : α), x ∈ s → r c (f x)
h₁ : r c (f a)
h₂ : ∀ (x : α), x ∈ s → r c (f x)
b : α
hb : b ∈ s
⊢ r c (f b)
[PROOFSTEP]
solve_by_elim
[GOAL]
case insert.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ (x : α), x ∈ s → r c (f x)
⊢ (∀ (x : α), x ∈ insert a s → r c (f x)) → r c (f a) ∧ ∀ (x : α), x ∈ s → r c (f x)
[PROOFSTEP]
intro h
[GOAL]
case insert.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ (x : α), x ∈ s → r c (f x)
h : ∀ (x : α), x ∈ insert a s → r c (f x)
⊢ r c (f a) ∧ ∀ (x : α), x ∈ s → r c (f x)
[PROOFSTEP]
constructor
[GOAL]
case insert.mpr.left
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ (x : α), x ∈ s → r c (f x)
h : ∀ (x : α), x ∈ insert a s → r c (f x)
⊢ r c (f a)
[PROOFSTEP]
exact h a (Finset.mem_insert_self _ _)
[GOAL]
case insert.mpr.right
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ (x : α), x ∈ s → r c (f x)
h : ∀ (x : α), x ∈ insert a s → r c (f x)
⊢ ∀ (x : α), x ∈ s → r c (f x)
[PROOFSTEP]
exact fun b hb => h b <| Finset.mem_insert_of_mem hb
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
⊢ r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
[PROOFSTEP]
classical
induction' s using Finset.induction_on with a s ha IH
· simp
rw [Finset.fold_insert ha, hr, IH, ← or_assoc, @or_comm (r c (f a)), or_assoc]
apply or_congr Iff.rfl
constructor
· rintro (h₁ | ⟨x, hx, h₂⟩)
  · use a
    simp [h₁]
  · refine' ⟨x, by simp [hx], h₂⟩
· rintro ⟨x, hx, h⟩
  exact (mem_insert.mp hx).imp (fun hx => by rwa [hx] at h ) (fun hx => ⟨x, hx, h⟩)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
⊢ r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
[PROOFSTEP]
induction' s using Finset.induction_on with a s ha IH
[GOAL]
case empty
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
⊢ r c (fold op b f ∅) ↔ r c b ∨ ∃ x, x ∈ ∅ ∧ r c (f x)
[PROOFSTEP]
simp
[GOAL]
case insert
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
⊢ r c (fold op b f (insert a s)) ↔ r c b ∨ ∃ x, x ∈ insert a s ∧ r c (f x)
[PROOFSTEP]
rw [Finset.fold_insert ha, hr, IH, ← or_assoc, @or_comm (r c (f a)), or_assoc]
[GOAL]
case insert
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
⊢ (r c b ∨ r c (f a) ∨ ∃ x, x ∈ s ∧ r c (f x)) ↔ r c b ∨ ∃ x, x ∈ insert a s ∧ r c (f x)
[PROOFSTEP]
apply or_congr Iff.rfl
[GOAL]
case insert
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
⊢ (r c (f a) ∨ ∃ x, x ∈ s ∧ r c (f x)) ↔ ∃ x, x ∈ insert a s ∧ r c (f x)
[PROOFSTEP]
constructor
[GOAL]
case insert.mp
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
⊢ (r c (f a) ∨ ∃ x, x ∈ s ∧ r c (f x)) → ∃ x, x ∈ insert a s ∧ r c (f x)
[PROOFSTEP]
rintro (h₁ | ⟨x, hx, h₂⟩)
[GOAL]
case insert.mp.inl
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
h₁ : r c (f a)
⊢ ∃ x, x ∈ insert a s ∧ r c (f x)
[PROOFSTEP]
use a
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
h₁ : r c (f a)
⊢ a ∈ insert a s ∧ r c (f a)
[PROOFSTEP]
simp [h₁]
[GOAL]
case insert.mp.inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
x : α
hx : x ∈ s
h₂ : r c (f x)
⊢ ∃ x, x ∈ insert a s ∧ r c (f x)
[PROOFSTEP]
refine' ⟨x, by simp [hx], h₂⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
x : α
hx : x ∈ s
h₂ : r c (f x)
⊢ x ∈ insert a s
[PROOFSTEP]
simp [hx]
[GOAL]
case insert.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
⊢ (∃ x, x ∈ insert a s ∧ r c (f x)) → r c (f a) ∨ ∃ x, x ∈ s ∧ r c (f x)
[PROOFSTEP]
rintro ⟨x, hx, h⟩
[GOAL]
case insert.mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
x : α
hx : x ∈ insert a s
h : r c (f x)
⊢ r c (f a) ∨ ∃ x, x ∈ s ∧ r c (f x)
[PROOFSTEP]
exact (mem_insert.mp hx).imp (fun hx => by rwa [hx] at h ) (fun hx => ⟨x, hx, h⟩)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
x : α
hx✝ : x ∈ insert a s
h : r c (f x)
hx : x = a
⊢ r c (f a)
[PROOFSTEP]
rwa [hx] at h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
inst✝ : DecidableEq α
s : Finset α
⊢ fold (fun x x_1 => x ∪ x_1) ∅ singleton s = s
[PROOFSTEP]
induction' s using Finset.induction_on with a s has ih
[GOAL]
case empty
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
⊢ fold (fun x x_1 => x ∪ x_1) ∅ singleton ∅ = ∅
[PROOFSTEP]
simp only [fold_empty]
[GOAL]
case insert
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
inst✝ : DecidableEq α
a : α
s : Finset α
has : ¬a ∈ s
ih : fold (fun x x_1 => x ∪ x_1) ∅ singleton s = s
⊢ fold (fun x x_1 => x ∪ x_1) ∅ singleton (insert a s) = insert a s
[PROOFSTEP]
rw [fold_insert has, ih, insert_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c : β
⊢ fold min b f s ≤ c ↔ b ≤ c ∨ ∃ x, x ∈ s ∧ f x ≤ c
[PROOFSTEP]
show _ ≥ _ ↔ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c : β
⊢ c ≥ fold min b f s ↔ b ≤ c ∨ ∃ x, x ∈ s ∧ f x ≤ c
[PROOFSTEP]
apply fold_op_rel_iff_or
[GOAL]
case hr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c : β
⊢ ∀ {x y z : β}, x ≥ min y z ↔ x ≥ y ∨ x ≥ z
[PROOFSTEP]
intro x y z
[GOAL]
case hr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c x y z : β
⊢ x ≥ min y z ↔ x ≥ y ∨ x ≥ z
[PROOFSTEP]
show _ ≤ _ ↔ _
[GOAL]
case hr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c x y z : β
⊢ min y z ≤ x ↔ x ≥ y ∨ x ≥ z
[PROOFSTEP]
exact min_le_iff
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c : β
⊢ fold min b f s < c ↔ b < c ∨ ∃ x, x ∈ s ∧ f x < c
[PROOFSTEP]
show _ > _ ↔ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c : β
⊢ c > fold min b f s ↔ b < c ∨ ∃ x, x ∈ s ∧ f x < c
[PROOFSTEP]
apply fold_op_rel_iff_or
[GOAL]
case hr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c : β
⊢ ∀ {x y z : β}, x > min y z ↔ x > y ∨ x > z
[PROOFSTEP]
intro x y z
[GOAL]
case hr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c x y z : β
⊢ x > min y z ↔ x > y ∨ x > z
[PROOFSTEP]
show _ < _ ↔ _
[GOAL]
case hr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c x y z : β
⊢ min y z < x ↔ x > y ∨ x > z
[PROOFSTEP]
exact min_lt_iff
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c : β
⊢ fold max b f s ≤ c ↔ b ≤ c ∧ ∀ (x : α), x ∈ s → f x ≤ c
[PROOFSTEP]
show _ ≥ _ ↔ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c : β
⊢ c ≥ fold max b f s ↔ b ≤ c ∧ ∀ (x : α), x ∈ s → f x ≤ c
[PROOFSTEP]
apply fold_op_rel_iff_and
[GOAL]
case hr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c : β
⊢ ∀ {x y z : β}, x ≥ max y z ↔ x ≥ y ∧ x ≥ z
[PROOFSTEP]
intro x y z
[GOAL]
case hr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c x y z : β
⊢ x ≥ max y z ↔ x ≥ y ∧ x ≥ z
[PROOFSTEP]
show _ ≤ _ ↔ _
[GOAL]
case hr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c x y z : β
⊢ max y z ≤ x ↔ x ≥ y ∧ x ≥ z
[PROOFSTEP]
exact max_le_iff
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c : β
⊢ fold max b f s < c ↔ b < c ∧ ∀ (x : α), x ∈ s → f x < c
[PROOFSTEP]
show _ > _ ↔ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c : β
⊢ c > fold max b f s ↔ b < c ∧ ∀ (x : α), x ∈ s → f x < c
[PROOFSTEP]
apply fold_op_rel_iff_and
[GOAL]
case hr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c : β
⊢ ∀ {x y z : β}, x > max y z ↔ x > y ∧ x > z
[PROOFSTEP]
intro x y z
[GOAL]
case hr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c x y z : β
⊢ x > max y z ↔ x > y ∧ x > z
[PROOFSTEP]
show _ < _ ↔ _
[GOAL]
case hr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c x y z : β
⊢ max y z < x ↔ x > y ∧ x > z
[PROOFSTEP]
exact max_lt_iff
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
inst✝² : LinearOrder β
c : β
inst✝¹ : Add β
inst✝ : CovariantClass β β (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
n : WithBot β
s : Finset α
⊢ fold max ⊥ (fun x => ↑(f x) + n) s = fold max ⊥ (WithBot.some ∘ f) s + n
[PROOFSTEP]
classical induction' s using Finset.induction_on with a s _ ih <;> simp [*, max_add_add_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
inst✝² : LinearOrder β
c : β
inst✝¹ : Add β
inst✝ : CovariantClass β β (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
n : WithBot β
s : Finset α
⊢ fold max ⊥ (fun x => ↑(f x) + n) s = fold max ⊥ (WithBot.some ∘ f) s + n
[PROOFSTEP]
induction' s using Finset.induction_on with a s _ ih
[GOAL]
case empty
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝² : LinearOrder β
c : β
inst✝¹ : Add β
inst✝ : CovariantClass β β (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
n : WithBot β
⊢ fold max ⊥ (fun x => ↑(f x) + n) ∅ = fold max ⊥ (WithBot.some ∘ f) ∅ + n
[PROOFSTEP]
simp [*, max_add_add_right]
[GOAL]
case insert
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝¹ : α
inst✝² : LinearOrder β
c : β
inst✝¹ : Add β
inst✝ : CovariantClass β β (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
n : WithBot β
a : α
s : Finset α
a✝ : ¬a ∈ s
ih : fold max ⊥ (fun x => ↑(f x) + n) s = fold max ⊥ (WithBot.some ∘ f) s + n
⊢ fold max ⊥ (fun x => ↑(f x) + n) (insert a s) = fold max ⊥ (WithBot.some ∘ f) (insert a s) + n
[PROOFSTEP]
simp [*, max_add_add_right]


[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
⊢ f ∈ Finset.finsupp s t ↔ f.support ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i
[PROOFSTEP]
refine' mem_map.trans ⟨_, _⟩
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
⊢ (∃ a, a ∈ pi s t ∧ ↑{ toFun := indicator s, inj' := (_ : Function.Injective fun f => indicator s f) } a = f) →
    f.support ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i
[PROOFSTEP]
rintro ⟨f, hf, rfl⟩
[GOAL]
case refine'_1.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
t : ι → Finset α
f : (i : ι) → i ∈ s → α
hf : f ∈ pi s t
⊢ (↑{ toFun := indicator s, inj' := (_ : Function.Injective fun f => indicator s f) } f).support ⊆ s ∧
    ∀ (i : ι), i ∈ s → ↑(↑{ toFun := indicator s, inj' := (_ : Function.Injective fun f => indicator s f) } f) i ∈ t i
[PROOFSTEP]
refine' ⟨support_indicator_subset _ _, fun i hi => _⟩
[GOAL]
case refine'_1.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
t : ι → Finset α
f : (i : ι) → i ∈ s → α
hf : f ∈ pi s t
i : ι
hi : i ∈ s
⊢ ↑(↑{ toFun := indicator s, inj' := (_ : Function.Injective fun f => indicator s f) } f) i ∈ t i
[PROOFSTEP]
convert mem_pi.1 hf i hi
[GOAL]
case h.e'_4
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
t : ι → Finset α
f : (i : ι) → i ∈ s → α
hf : f ∈ pi s t
i : ι
hi : i ∈ s
⊢ ↑(↑{ toFun := indicator s, inj' := (_ : Function.Injective fun f => indicator s f) } f) i = f i hi
[PROOFSTEP]
exact indicator_of_mem hi _
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
⊢ (f.support ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i) →
    ∃ a, a ∈ pi s t ∧ ↑{ toFun := indicator s, inj' := (_ : Function.Injective fun f => indicator s f) } a = f
[PROOFSTEP]
refine' fun h => ⟨fun i _ => f i, mem_pi.2 h.2, _⟩
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
h : f.support ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i
⊢ (↑{ toFun := indicator s, inj' := (_ : Function.Injective fun f => indicator s f) } fun i x => ↑f i) = f
[PROOFSTEP]
ext i
[GOAL]
case refine'_2.h
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
h : f.support ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i
i : ι
⊢ ↑(↑{ toFun := indicator s, inj' := (_ : Function.Injective fun f => indicator s f) } fun i x => ↑f i) i = ↑f i
[PROOFSTEP]
exact ite_eq_left_iff.2 fun hi => (not_mem_support_iff.1 fun H => hi <| h.1 H).symm
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
⊢ f ∈ Finset.finsupp s ↑t ↔ ∀ (i : ι), ↑f i ∈ ↑t i
[PROOFSTEP]
refine'
  mem_finsupp_iff.trans
    (forall_and.symm.trans <|
      forall_congr' fun i =>
        ⟨fun h => _, fun h => ⟨fun hi => ht <| mem_support_iff.2 fun H => mem_support_iff.1 hi _, fun _ => h⟩⟩)
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → ↑f i ∈ ↑t i)
⊢ ↑f i ∈ ↑t i
[PROOFSTEP]
by_cases hi : i ∈ s
[GOAL]
case pos
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → ↑f i ∈ ↑t i)
hi : i ∈ s
⊢ ↑f i ∈ ↑t i
[PROOFSTEP]
exact h.2 hi
[GOAL]
case neg
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → ↑f i ∈ ↑t i)
hi : ¬i ∈ s
⊢ ↑f i ∈ ↑t i
[PROOFSTEP]
rw [not_mem_support_iff.1 (mt h.1 hi), not_mem_support_iff.1 fun H => hi <| ht H]
[GOAL]
case neg
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → ↑f i ∈ ↑t i)
hi : ¬i ∈ s
⊢ 0 ∈ 0
[PROOFSTEP]
exact zero_mem_zero
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
i : ι
h : ↑f i ∈ ↑t i
hi : i ∈ f.support
H : ↑t i = 0
⊢ ↑f i = 0
[PROOFSTEP]
rwa [H, mem_zero] at h
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f✝ : ι →₀ α
f : ι →₀ Finset α
⊢ card (pi f) = prod f fun i => ↑(card (↑f i))
[PROOFSTEP]
rw [pi, card_finsupp]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f✝ : ι →₀ α
f : ι →₀ Finset α
⊢ ∏ i in f.support, card (↑f i) = prod f fun i => ↑(card (↑f i))
[PROOFSTEP]
exact Finset.prod_congr rfl fun i _ => by simp only [Pi.nat_apply, Nat.cast_id]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f✝ : ι →₀ α
f : ι →₀ Finset α
i : ι
x✝ : i ∈ f.support
⊢ card (↑f i) = (fun i => ↑(card (↑f i))) i (↑f i)
[PROOFSTEP]
simp only [Pi.nat_apply, Nat.cast_id]


[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
⊢ Monotone card
[PROOFSTEP]
apply card_le_of_subset
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
⊢ card ({a} ∩ s) ≤ 1
[PROOFSTEP]
cases' Finset.decidableMem a s with h h
[GOAL]
case isFalse
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ card ({a} ∩ s) ≤ 1
[PROOFSTEP]
simp [Finset.singleton_inter_of_not_mem h]
[GOAL]
case isTrue
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : a ∈ s
⊢ card ({a} ∩ s) ≤ 1
[PROOFSTEP]
simp [Finset.singleton_inter_of_mem h]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ card (insert a s) = card s + 1
[PROOFSTEP]
rw [← cons_eq_insert _ _ h, card_cons]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : a ∈ s
⊢ card (insert a s) = card s
[PROOFSTEP]
rw [insert_eq_of_mem h]
[GOAL]
α : Type u_1
β : Type u_2
s✝ t : Finset α
a✝ b : α
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ card (insert a s) ≤ card s + 1
[PROOFSTEP]
by_cases h : a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
s✝ t : Finset α
a✝ b : α
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ card (insert a s) ≤ card s + 1
[PROOFSTEP]
rw [insert_eq_of_mem h]
[GOAL]
case pos
α : Type u_1
β : Type u_2
s✝ t : Finset α
a✝ b : α
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ card s ≤ card s + 1
[PROOFSTEP]
exact Nat.le_succ _
[GOAL]
case neg
α : Type u_1
β : Type u_2
s✝ t : Finset α
a✝ b : α
inst✝ : DecidableEq α
a : α
s : Finset α
h : ¬a ∈ s
⊢ card (insert a s) ≤ card s + 1
[PROOFSTEP]
rw [card_insert_of_not_mem h]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
⊢ card (insert a s) = if a ∈ s then card s else card s + 1
[PROOFSTEP]
by_cases h : a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : a ∈ s
⊢ card (insert a s) = if a ∈ s then card s else card s + 1
[PROOFSTEP]
rw [card_insert_of_mem h, if_pos h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ card (insert a s) = if a ∈ s then card s else card s + 1
[PROOFSTEP]
rw [card_insert_of_not_mem h, if_neg h]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : a ≠ b
⊢ card {a, b} = 2
[PROOFSTEP]
rw [card_insert_of_not_mem (not_mem_singleton.2 h), card_singleton]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
⊢ card s - 1 ≤ card (erase s a)
[PROOFSTEP]
by_cases h : a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : a ∈ s
⊢ card s - 1 ≤ card (erase s a)
[PROOFSTEP]
exact (card_erase_of_mem h).ge
[GOAL]
case neg
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ card s - 1 ≤ card (erase s a)
[PROOFSTEP]
rw [erase_eq_of_not_mem h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ card s - 1 ≤ card s
[PROOFSTEP]
exact Nat.sub_le _ _
[GOAL]
α : Type u_1
β : Type u_2
s✝ t : Finset α
f : α → β
n : ℕ
s : Finset α
⊢ List.length (toList s) = card s
[PROOFSTEP]
rw [toList, ← Multiset.coe_card, Multiset.coe_toList, card_def]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq β
⊢ card (image f s) ≤ card s
[PROOFSTEP]
simpa only [card_map] using (s.1.map f).toFinset_card_le
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq β
H : Set.InjOn f ↑s
⊢ card (image f s) = card s
[PROOFSTEP]
simp only [card, image_val_of_injOn H, card_map]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq β
H : card (image f s) = card s
⊢ Set.InjOn f ↑s
[PROOFSTEP]
rw [card_def, card_def, image, toFinset] at H
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq β
H :
  ↑Multiset.card { val := dedup (Multiset.map f s.val), nodup := (_ : Nodup (dedup (Multiset.map f s.val))) }.val =
    ↑Multiset.card s.val
⊢ Set.InjOn f ↑s
[PROOFSTEP]
dsimp only at H
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq β
H : ↑Multiset.card (dedup (Multiset.map f s.val)) = ↑Multiset.card s.val
⊢ Set.InjOn f ↑s
[PROOFSTEP]
have : (s.1.map f).dedup = s.1.map f :=
  by
  refine Multiset.eq_of_le_of_card_le (Multiset.dedup_le _) ?_
  simp only [H, Multiset.card_map, le_rfl]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq β
H : ↑Multiset.card (dedup (Multiset.map f s.val)) = ↑Multiset.card s.val
⊢ dedup (Multiset.map f s.val) = Multiset.map f s.val
[PROOFSTEP]
refine Multiset.eq_of_le_of_card_le (Multiset.dedup_le _) ?_
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq β
H : ↑Multiset.card (dedup (Multiset.map f s.val)) = ↑Multiset.card s.val
⊢ ↑Multiset.card (Multiset.map f s.val) ≤ ↑Multiset.card (dedup (Multiset.map f s.val))
[PROOFSTEP]
simp only [H, Multiset.card_map, le_rfl]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq β
H : ↑Multiset.card (dedup (Multiset.map f s.val)) = ↑Multiset.card s.val
this : dedup (Multiset.map f s.val) = Multiset.map f s.val
⊢ Set.InjOn f ↑s
[PROOFSTEP]
rw [Multiset.dedup_eq_self] at this
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq β
H : ↑Multiset.card (dedup (Multiset.map f s.val)) = ↑Multiset.card s.val
this : Nodup (Multiset.map f s.val)
⊢ Set.InjOn f ↑s
[PROOFSTEP]
exact inj_on_of_nodup_map this
[GOAL]
α : Type u_1
β : Type u_2
s✝ t : Finset α
f✝ : α → β
n : ℕ
s : Finset α
f : α → β
inst✝ : DecidableEq β
y : β
⊢ card (filter (fun x => f x = y) s) ≠ 0 ↔ y ∈ image f s
[PROOFSTEP]
rw [← pos_iff_ne_zero, card_pos, fiber_nonempty_iff_mem_image]
[GOAL]
α : Type u_1
β : Type u_2
s✝ t : Finset α
f : α → β
n : ℕ
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
⊢ card (Finset.subtype p s) = card (filter p s)
[PROOFSTEP]
simp [Finset.subtype]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
p : α → Prop
inst✝ : DecidablePred p
h : card (filter p s) = card s
x : α
hx : x ∈ s
⊢ p x
[PROOFSTEP]
rw [← eq_of_subset_of_card_le (s.filter_subset p) h.ge, mem_filter] at hx
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
p : α → Prop
inst✝ : DecidablePred p
h : card (filter p s) = card s
x : α
hx : x ∈ s ∧ p x
⊢ p x
[PROOFSTEP]
exact hx.2
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f✝ : α → β
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ (a : α), a ∈ s → ∃ i h, f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
⊢ card s = n
[PROOFSTEP]
classical
have : ∀ a : α, a ∈ s ↔ ∃ (i : _) (hi : i ∈ range n), f i (mem_range.1 hi) = a := fun a =>
  ⟨fun ha =>
    let ⟨i, hi, eq⟩ := hf a ha
    ⟨i, mem_range.2 hi, eq⟩,
    fun ⟨i, hi, eq⟩ => eq ▸ hf' i (mem_range.1 hi)⟩
have : s = (range n).attach.image fun i => f i.1 (mem_range.1 i.2) := by
  simpa only [ext_iff, mem_image, exists_prop, Subtype.exists, mem_attach, true_and_iff]
calc
  s.card = card ((range n).attach.image fun i => f i.1 (mem_range.1 i.2)) := by rw [this]
  _ = card (range n).attach :=
    ((card_image_of_injective _) fun ⟨i, hi⟩ ⟨j, hj⟩ eq => Subtype.eq <| f_inj i j (mem_range.1 hi) (mem_range.1 hj) eq)
  _ = card (range n) := card_attach
  _ = n := card_range n
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f✝ : α → β
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ (a : α), a ∈ s → ∃ i h, f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
⊢ card s = n
[PROOFSTEP]
have : ∀ a : α, a ∈ s ↔ ∃ (i : _) (hi : i ∈ range n), f i (mem_range.1 hi) = a := fun a =>
  ⟨fun ha =>
    let ⟨i, hi, eq⟩ := hf a ha
    ⟨i, mem_range.2 hi, eq⟩,
    fun ⟨i, hi, eq⟩ => eq ▸ hf' i (mem_range.1 hi)⟩
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f✝ : α → β
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ (a : α), a ∈ s → ∃ i h, f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
this : ∀ (a : α), a ∈ s ↔ ∃ i hi, f i (_ : i < n) = a
⊢ card s = n
[PROOFSTEP]
have : s = (range n).attach.image fun i => f i.1 (mem_range.1 i.2) := by
  simpa only [ext_iff, mem_image, exists_prop, Subtype.exists, mem_attach, true_and_iff]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f✝ : α → β
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ (a : α), a ∈ s → ∃ i h, f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
this : ∀ (a : α), a ∈ s ↔ ∃ i hi, f i (_ : i < n) = a
⊢ s = image (fun i => f ↑i (_ : ↑i < n)) (attach (range n))
[PROOFSTEP]
simpa only [ext_iff, mem_image, exists_prop, Subtype.exists, mem_attach, true_and_iff]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f✝ : α → β
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ (a : α), a ∈ s → ∃ i h, f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
this✝ : ∀ (a : α), a ∈ s ↔ ∃ i hi, f i (_ : i < n) = a
this : s = image (fun i => f ↑i (_ : ↑i < n)) (attach (range n))
⊢ card s = n
[PROOFSTEP]
calc
  s.card = card ((range n).attach.image fun i => f i.1 (mem_range.1 i.2)) := by rw [this]
  _ = card (range n).attach :=
    ((card_image_of_injective _) fun ⟨i, hi⟩ ⟨j, hj⟩ eq => Subtype.eq <| f_inj i j (mem_range.1 hi) (mem_range.1 hj) eq)
  _ = card (range n) := card_attach
  _ = n := card_range n
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f✝ : α → β
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ (a : α), a ∈ s → ∃ i h, f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
this✝ : ∀ (a : α), a ∈ s ↔ ∃ i hi, f i (_ : i < n) = a
this : s = image (fun i => f ↑i (_ : ↑i < n)) (attach (range n))
⊢ card s = card (image (fun i => f ↑i (_ : ↑i < n)) (attach (range n)))
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
⊢ card s = card t
[PROOFSTEP]
classical calc
  s.card = s.attach.card := card_attach.symm
  _ = (s.attach.image fun a : { a // a ∈ s } => f a.1 a.2).card :=
    (Eq.symm ((card_image_of_injective _) fun a b h => Subtype.eq <| h₂ _ _ _ _ h))
  _ = t.card :=
    congr_arg card
      (Finset.ext fun b =>
        ⟨fun h =>
          let ⟨a, _, ha₂⟩ := mem_image.1 h
          ha₂ ▸ h₁ _ _,
          fun h =>
          let ⟨a, ha₁, ha₂⟩ := h₃ b h
          mem_image.2 ⟨⟨a, ha₁⟩, by simp [ha₂]⟩⟩)
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
⊢ card s = card t
[PROOFSTEP]
calc
  s.card = s.attach.card := card_attach.symm
  _ = (s.attach.image fun a : { a // a ∈ s } => f a.1 a.2).card :=
    (Eq.symm ((card_image_of_injective _) fun a b h => Subtype.eq <| h₂ _ _ _ _ h))
  _ = t.card :=
    congr_arg card
      (Finset.ext fun b =>
        ⟨fun h =>
          let ⟨a, _, ha₂⟩ := mem_image.1 h
          ha₂ ▸ h₁ _ _,
          fun h =>
          let ⟨a, ha₁, ha₂⟩ := h₃ b h
          mem_image.2 ⟨⟨a, ha₁⟩, by simp [ha₂]⟩⟩)
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
b : β
h : b ∈ t
a : α
ha₁ : a ∈ s
ha₂ : f a ha₁ = b
⊢ { val := a, property := ha₁ } ∈ attach s ∧
    f ↑{ val := a, property := ha₁ } (_ : ↑{ val := a, property := ha₁ } ∈ s) = b
[PROOFSTEP]
simp [ha₂]
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
f_inj : ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → f a₁ = f a₂ → a₁ = a₂
⊢ card s ≤ card t
[PROOFSTEP]
classical calc
  s.card = (s.image f).card := (card_image_of_injOn f_inj).symm
  _ ≤ t.card := card_le_of_subset <| image_subset_iff.2 hf
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
f_inj : ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → f a₁ = f a₂ → a₁ = a₂
⊢ card s ≤ card t
[PROOFSTEP]
calc
  s.card = (s.image f).card := (card_image_of_injOn f_inj).symm
  _ ≤ t.card := card_le_of_subset <| image_subset_iff.2 hf
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
hc : card t < card s
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
⊢ ∃ x, x ∈ s ∧ ∃ y, y ∈ s ∧ x ≠ y ∧ f x = f y
[PROOFSTEP]
classical
by_contra' hz
refine' hc.not_le (card_le_card_of_inj_on f hf _)
intro x hx y hy
contrapose
exact hz x hx y hy
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
hc : card t < card s
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
⊢ ∃ x, x ∈ s ∧ ∃ y, y ∈ s ∧ x ≠ y ∧ f x = f y
[PROOFSTEP]
by_contra' hz
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
hc : card t < card s
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
hz : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → f x ≠ f y
⊢ False
[PROOFSTEP]
refine' hc.not_le (card_le_card_of_inj_on f hf _)
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
hc : card t < card s
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
hz : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → f x ≠ f y
⊢ ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → f a₁ = f a₂ → a₁ = a₂
[PROOFSTEP]
intro x hx y hy
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
hc : card t < card s
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
hz : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → f x ≠ f y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ f x = f y → x = y
[PROOFSTEP]
contrapose
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
hc : card t < card s
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
hz : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → f x ≠ f y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ ¬x = y → ¬f x = f y
[PROOFSTEP]
exact hz x hx y hy
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f✝ : α → β
n : ℕ
f : ℕ → α
hf : ∀ (i : ℕ), i < n → f i ∈ s
f_inj : ∀ (i : ℕ), i < n → ∀ (j : ℕ), j < n → f i = f j → i = j
⊢ ∀ (a : ℕ), a ∈ range n → f a ∈ s
[PROOFSTEP]
simpa only [mem_range]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f✝ : α → β
n : ℕ
f : ℕ → α
hf : ∀ (i : ℕ), i < n → f i ∈ s
f_inj : ∀ (i : ℕ), i < n → ∀ (j : ℕ), j < n → f i = f j → i = j
⊢ ∀ (a₁ : ℕ), a₁ ∈ range n → ∀ (a₂ : ℕ), a₂ ∈ range n → f a₁ = f a₂ → a₁ = a₂
[PROOFSTEP]
simpa only [mem_range]
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : card t ≤ card s
⊢ ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
[PROOFSTEP]
classical
intro b hb
have h : (s.attach.image fun a : { a // a ∈ s } => f a a.prop).card = s.card :=
  @card_attach _ s ▸ card_image_of_injective _ fun ⟨a₁, ha₁⟩ ⟨a₂, ha₂⟩ h => Subtype.eq <| hinj _ _ _ _ h
have h' : image (fun a : { a // a ∈ s } => f a a.prop) s.attach = t :=
  eq_of_subset_of_card_le
    (fun b h =>
      let ⟨a, _, ha₂⟩ := mem_image.1 h
      ha₂ ▸ hf _ _)
    (by simp [hst, h])
rw [← h'] at hb
obtain ⟨a, _, ha₂⟩ := mem_image.1 hb
exact ⟨a, a.2, ha₂.symm⟩
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : card t ≤ card s
⊢ ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
[PROOFSTEP]
intro b hb
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : card t ≤ card s
b : β
hb : b ∈ t
⊢ ∃ a ha, b = f a ha
[PROOFSTEP]
have h : (s.attach.image fun a : { a // a ∈ s } => f a a.prop).card = s.card :=
  @card_attach _ s ▸ card_image_of_injective _ fun ⟨a₁, ha₁⟩ ⟨a₂, ha₂⟩ h => Subtype.eq <| hinj _ _ _ _ h
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : card t ≤ card s
b : β
hb : b ∈ t
h : card (image (fun a => f ↑a (_ : ↑a ∈ s)) (attach s)) = card s
⊢ ∃ a ha, b = f a ha
[PROOFSTEP]
have h' : image (fun a : { a // a ∈ s } => f a a.prop) s.attach = t :=
  eq_of_subset_of_card_le
    (fun b h =>
      let ⟨a, _, ha₂⟩ := mem_image.1 h
      ha₂ ▸ hf _ _)
    (by simp [hst, h])
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : card t ≤ card s
b : β
hb : b ∈ t
h : card (image (fun a => f ↑a (_ : ↑a ∈ s)) (attach s)) = card s
⊢ card t ≤ card (image (fun a => f ↑a (_ : ↑a ∈ s)) (attach s))
[PROOFSTEP]
simp [hst, h]
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : card t ≤ card s
b : β
hb : b ∈ t
h : card (image (fun a => f ↑a (_ : ↑a ∈ s)) (attach s)) = card s
h' : image (fun a => f ↑a (_ : ↑a ∈ s)) (attach s) = t
⊢ ∃ a ha, b = f a ha
[PROOFSTEP]
rw [← h'] at hb
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : card t ≤ card s
b : β
hb : b ∈ image (fun a => f ↑a (_ : ↑a ∈ s)) (attach s)
h : card (image (fun a => f ↑a (_ : ↑a ∈ s)) (attach s)) = card s
h' : image (fun a => f ↑a (_ : ↑a ∈ s)) (attach s) = t
⊢ ∃ a ha, b = f a ha
[PROOFSTEP]
obtain ⟨a, _, ha₂⟩ := mem_image.1 hb
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : card t ≤ card s
b : β
hb : b ∈ image (fun a => f ↑a (_ : ↑a ∈ s)) (attach s)
h : card (image (fun a => f ↑a (_ : ↑a ∈ s)) (attach s)) = card s
h' : image (fun a => f ↑a (_ : ↑a ∈ s)) (attach s) = t
a : { a // a ∈ s }
left✝ : a ∈ attach s
ha₂ : f ↑a (_ : ↑a ∈ s) = b
⊢ ∃ a ha, b = f a ha
[PROOFSTEP]
exact ⟨a, a.2, ha₂.symm⟩
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : card s ≤ card t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
this : Inhabited { x // x ∈ s }
f' : { x // x ∈ s } → { x // x ∈ t } := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
g : { x // x ∈ t } → { x // x ∈ s } := surjInv (_ : ∀ (x : { x // x ∈ t }), ∃ a, f' a = x)
hg : Injective g
x : { x // x ∈ s }
⊢ card (attach s) ≤ card (attach t)
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
⊢ card (s ∪ ∅) + card (s ∩ ∅) = card s + card ∅
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
a : α
r : Finset α
har : ¬a ∈ r
h : card (s ∪ r) + card (s ∩ r) = card s + card r
⊢ card (s ∪ insert a r) + card (s ∩ insert a r) = card s + card (insert a r)
[PROOFSTEP]
by_cases a ∈ s
[GOAL]
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
a : α
r : Finset α
har : ¬a ∈ r
h : card (s ∪ r) + card (s ∩ r) = card s + card r
⊢ card (s ∪ insert a r) + card (s ∩ insert a r) = card s + card (insert a r)
[PROOFSTEP]
by_cases a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
a : α
r : Finset α
har : ¬a ∈ r
h✝ : card (s ∪ r) + card (s ∩ r) = card s + card r
h : a ∈ s
⊢ card (s ∪ insert a r) + card (s ∩ insert a r) = card s + card (insert a r)
[PROOFSTEP]
simp [*, ← add_assoc, add_right_comm _ 1]
[GOAL]
case neg
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
a : α
r : Finset α
har : ¬a ∈ r
h✝ : card (s ∪ r) + card (s ∩ r) = card s + card r
h : ¬a ∈ s
⊢ card (s ∪ insert a r) + card (s ∩ insert a r) = card s + card (insert a r)
[PROOFSTEP]
simp [*, ← add_assoc, add_right_comm _ 1]
[GOAL]
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
⊢ card (s ∩ t) + card (s ∪ t) = card s + card t
[PROOFSTEP]
rw [add_comm, card_union_add_card_inter]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
h : _root_.Disjoint s t
⊢ card (s ∪ t) = card s + card t
[PROOFSTEP]
rw [← disjUnion_eq_union s t h, card_disjUnion _ _ _]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
h : s ⊆ t
⊢ card (t \ s) = card t - card s
[PROOFSTEP]
suffices card (t \ s) = card (t \ s ∪ s) - s.card by rwa [sdiff_union_of_subset h] at this
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
h : s ⊆ t
this : card (t \ s) = card (t \ s ∪ s) - card s
⊢ card (t \ s) = card t - card s
[PROOFSTEP]
rwa [sdiff_union_of_subset h] at this
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
h : s ⊆ t
⊢ card (t \ s) = card (t \ s ∪ s) - card s
[PROOFSTEP]
rw [card_disjoint_union sdiff_disjoint, add_tsub_cancel_right]
[GOAL]
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
⊢ card (t \ (s ∩ t)) ≤ card (t \ s)
[PROOFSTEP]
rw [sdiff_inter_self_right t s]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ card (s \ t) + card t = card (s ∪ t)
[PROOFSTEP]
rw [← card_disjoint_union sdiff_disjoint, sdiff_union_self_eq_union]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
⊢ card (filter p s) + card (filter (fun a => ¬p a) s) = card s
[PROOFSTEP]
classical rw [← card_union_eq (disjoint_filter_filter_neg _ _ _), filter_union_filter_neg_eq]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
⊢ card (filter p s) + card (filter (fun a => ¬p a) s) = card s
[PROOFSTEP]
rw [← card_union_eq (disjoint_filter_filter_neg _ _ _), filter_union_filter_neg_eq]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
A B : Finset α
i : ℕ
h₁ : i + card B ≤ card A
h₂ : B ⊆ A
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
[PROOFSTEP]
classical
rcases Nat.le.dest h₁ with ⟨k, h⟩
clear h₁
induction' k with k ih generalizing A
· exact ⟨A, h₂, Subset.refl _, h.symm⟩
obtain ⟨a, ha⟩ : (A \ B).Nonempty :=
  by
  rw [← card_pos, card_sdiff h₂, ← h, Nat.add_right_comm, add_tsub_cancel_right, Nat.add_succ]
  apply Nat.succ_pos
have z : i + card B + k = card (erase A a) := by
  rw [card_erase_of_mem (mem_sdiff.1 ha).1, ← h, Nat.add_sub_assoc (Nat.one_le_iff_ne_zero.mpr k.succ_ne_zero), ←
    pred_eq_sub_one, k.pred_succ]
have : B ⊆ A.erase a := by
  rintro t th
  apply mem_erase_of_ne_of_mem _ (h₂ th)
  rintro rfl
  exact not_mem_sdiff_of_mem_right th ha
rcases ih this z with ⟨B', hB', B'subA', cards⟩
exact ⟨B', hB', B'subA'.trans (erase_subset _ _), cards⟩
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
A B : Finset α
i : ℕ
h₁ : i + card B ≤ card A
h₂ : B ⊆ A
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
[PROOFSTEP]
rcases Nat.le.dest h₁ with ⟨k, h⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
A B : Finset α
i : ℕ
h₁ : i + card B ≤ card A
h₂ : B ⊆ A
k : ℕ
h : i + card B + k = card A
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
[PROOFSTEP]
clear h₁
[GOAL]
case intro
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
A B : Finset α
i : ℕ
h₂ : B ⊆ A
k : ℕ
h : i + card B + k = card A
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
[PROOFSTEP]
induction' k with k ih generalizing A
[GOAL]
case intro.zero
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k : ℕ
h✝ : i + card B + k = card A✝
A : Finset α
h₂ : B ⊆ A
h : i + card B + zero = card A
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
[PROOFSTEP]
exact ⟨A, h₂, Subset.refl _, h.symm⟩
[GOAL]
case intro.succ
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
[PROOFSTEP]
obtain ⟨a, ha⟩ : (A \ B).Nonempty :=
  by
  rw [← card_pos, card_sdiff h₂, ← h, Nat.add_right_comm, add_tsub_cancel_right, Nat.add_succ]
  apply Nat.succ_pos
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
⊢ Finset.Nonempty (A \ B)
[PROOFSTEP]
rw [← card_pos, card_sdiff h₂, ← h, Nat.add_right_comm, add_tsub_cancel_right, Nat.add_succ]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
⊢ 0 < succ (i + k)
[PROOFSTEP]
apply Nat.succ_pos
[GOAL]
case intro.succ.intro
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
a : α
ha : a ∈ A \ B
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
[PROOFSTEP]
have z : i + card B + k = card (erase A a) := by
  rw [card_erase_of_mem (mem_sdiff.1 ha).1, ← h, Nat.add_sub_assoc (Nat.one_le_iff_ne_zero.mpr k.succ_ne_zero), ←
    pred_eq_sub_one, k.pred_succ]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
a : α
ha : a ∈ A \ B
⊢ i + card B + k = card (erase A a)
[PROOFSTEP]
rw [card_erase_of_mem (mem_sdiff.1 ha).1, ← h, Nat.add_sub_assoc (Nat.one_le_iff_ne_zero.mpr k.succ_ne_zero), ←
  pred_eq_sub_one, k.pred_succ]
[GOAL]
case intro.succ.intro
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
a : α
ha : a ∈ A \ B
z : i + card B + k = card (erase A a)
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
[PROOFSTEP]
have : B ⊆ A.erase a := by
  rintro t th
  apply mem_erase_of_ne_of_mem _ (h₂ th)
  rintro rfl
  exact not_mem_sdiff_of_mem_right th ha
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
a : α
ha : a ∈ A \ B
z : i + card B + k = card (erase A a)
⊢ B ⊆ erase A a
[PROOFSTEP]
rintro t th
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
a : α
ha : a ∈ A \ B
z : i + card B + k = card (erase A a)
t : α
th : t ∈ B
⊢ t ∈ erase A a
[PROOFSTEP]
apply mem_erase_of_ne_of_mem _ (h₂ th)
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
a : α
ha : a ∈ A \ B
z : i + card B + k = card (erase A a)
t : α
th : t ∈ B
⊢ t ≠ a
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
t : α
th : t ∈ B
ha : t ∈ A \ B
z : i + card B + k = card (erase A t)
⊢ False
[PROOFSTEP]
exact not_mem_sdiff_of_mem_right th ha
[GOAL]
case intro.succ.intro
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
a : α
ha : a ∈ A \ B
z : i + card B + k = card (erase A a)
this : B ⊆ erase A a
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
[PROOFSTEP]
rcases ih this z with ⟨B', hB', B'subA', cards⟩
[GOAL]
case intro.succ.intro.intro.intro.intro
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
a : α
ha : a ∈ A \ B
z : i + card B + k = card (erase A a)
this : B ⊆ erase A a
B' : Finset α
hB' : B ⊆ B'
B'subA' : B' ⊆ erase A a
cards : card B' = i + card B
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
[PROOFSTEP]
exact ⟨B', hB', B'subA'.trans (erase_subset _ _), cards⟩
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
A : Finset α
i : ℕ
h₁ : i ≤ card A
⊢ i + card ∅ ≤ card A
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n✝ : ℕ
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : 2 * n < card (X ∪ Y)
⊢ ∃ C, n < card C ∧ (C ⊆ X ∨ C ⊆ Y)
[PROOFSTEP]
have h₁ : (X ∩ (Y \ X)).card = 0 := Finset.card_eq_zero.mpr (Finset.inter_sdiff_self X Y)
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n✝ : ℕ
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : 2 * n < card (X ∪ Y)
h₁ : card (X ∩ (Y \ X)) = 0
⊢ ∃ C, n < card C ∧ (C ⊆ X ∨ C ⊆ Y)
[PROOFSTEP]
have h₂ : (X ∪ Y).card = X.card + (Y \ X).card := by
  rw [← card_union_add_card_inter X (Y \ X), Finset.union_sdiff_self_eq_union, h₁, add_zero]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n✝ : ℕ
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : 2 * n < card (X ∪ Y)
h₁ : card (X ∩ (Y \ X)) = 0
⊢ card (X ∪ Y) = card X + card (Y \ X)
[PROOFSTEP]
rw [← card_union_add_card_inter X (Y \ X), Finset.union_sdiff_self_eq_union, h₁, add_zero]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n✝ : ℕ
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : 2 * n < card (X ∪ Y)
h₁ : card (X ∩ (Y \ X)) = 0
h₂ : card (X ∪ Y) = card X + card (Y \ X)
⊢ ∃ C, n < card C ∧ (C ⊆ X ∨ C ⊆ Y)
[PROOFSTEP]
rw [h₂, two_mul] at hXY
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n✝ : ℕ
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : n + n < card X + card (Y \ X)
h₁ : card (X ∩ (Y \ X)) = 0
h₂ : card (X ∪ Y) = card X + card (Y \ X)
⊢ ∃ C, n < card C ∧ (C ⊆ X ∨ C ⊆ Y)
[PROOFSTEP]
rcases lt_or_lt_of_add_lt_add hXY with (h | h)
[GOAL]
case inl
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n✝ : ℕ
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : n + n < card X + card (Y \ X)
h₁ : card (X ∩ (Y \ X)) = 0
h₂ : card (X ∪ Y) = card X + card (Y \ X)
h : n < card X
⊢ ∃ C, n < card C ∧ (C ⊆ X ∨ C ⊆ Y)
[PROOFSTEP]
exact ⟨X, h, Or.inl (Finset.Subset.refl X)⟩
[GOAL]
case inr
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n✝ : ℕ
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : n + n < card X + card (Y \ X)
h₁ : card (X ∩ (Y \ X)) = 0
h₂ : card (X ∪ Y) = card X + card (Y \ X)
h : n < card (Y \ X)
⊢ ∃ C, n < card C ∧ (C ⊆ X ∨ C ⊆ Y)
[PROOFSTEP]
exact ⟨Y \ X, h, Or.inr (Finset.sdiff_subset Y X)⟩
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
⊢ card s = 1 ↔ ∃ a, s = {a}
[PROOFSTEP]
cases s
[GOAL]
case mk
α : Type u_1
β : Type u_2
t : Finset α
f : α → β
n : ℕ
val✝ : Multiset α
nodup✝ : Nodup val✝
⊢ card { val := val✝, nodup := nodup✝ } = 1 ↔ ∃ a, { val := val✝, nodup := nodup✝ } = {a}
[PROOFSTEP]
simp only [Multiset.card_eq_one, Finset.card, ← val_inj, singleton_val]
[GOAL]
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
⊢ (∃ a x, insert a s = t) ↔ s ⊆ t ∧ card s + 1 = card t
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
⊢ (∃ a x, insert a s = t) → s ⊆ t ∧ card s + 1 = card t
[PROOFSTEP]
rintro ⟨a, ha, rfl⟩
[GOAL]
case mp.intro.intro
α : Type u_1
β : Type u_2
s✝ t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s : Finset α
a : α
ha : ¬a ∈ s
⊢ s ⊆ insert a s ∧ card s + 1 = card (insert a s)
[PROOFSTEP]
exact ⟨subset_insert _ _, (card_insert_of_not_mem ha).symm⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
⊢ s ⊆ t ∧ card s + 1 = card t → ∃ a x, insert a s = t
[PROOFSTEP]
rintro ⟨hst, h⟩
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : card s + 1 = card t
⊢ ∃ a x, insert a s = t
[PROOFSTEP]
obtain ⟨a, ha⟩ : ∃ a, t \ s = { a } := card_eq_one.1 (by rw [card_sdiff hst, ← h, add_tsub_cancel_left])
[GOAL]
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : card s + 1 = card t
⊢ card (t \ s) = 1
[PROOFSTEP]
rw [card_sdiff hst, ← h, add_tsub_cancel_left]
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : card s + 1 = card t
a : α
ha : t \ s = {a}
⊢ ∃ a x, insert a s = t
[PROOFSTEP]
refine' ⟨a, fun hs => (_ : a ∉ { a }) <| mem_singleton_self _, by rw [insert_eq, ← ha, sdiff_union_of_subset hst]⟩
[GOAL]
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : card s + 1 = card t
a : α
ha : t \ s = {a}
⊢ insert a s = t
[PROOFSTEP]
rw [insert_eq, ← ha, sdiff_union_of_subset hst]
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : card s + 1 = card t
a : α
ha : t \ s = {a}
hs : a ∈ s
⊢ ¬a ∈ {a}
[PROOFSTEP]
rw [← ha]
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : card s + 1 = card t
a : α
ha : t \ s = {a}
hs : a ∈ s
⊢ ¬a ∈ t \ s
[PROOFSTEP]
exact not_mem_sdiff_of_mem_right hs
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
⊢ card s ≤ 1 ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a = b
[PROOFSTEP]
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
[GOAL]
case inl
α : Type u_1
β : Type u_2
t : Finset α
f : α → β
n : ℕ
⊢ card ∅ ≤ 1 ↔ ∀ (a : α), a ∈ ∅ → ∀ (b : α), b ∈ ∅ → a = b
[PROOFSTEP]
simp
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
x : α
hx : x ∈ s
⊢ card s ≤ 1 ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a = b
[PROOFSTEP]
refine' (Nat.succ_le_of_lt (card_pos.2 ⟨x, hx⟩)).le_iff_eq.trans (card_eq_one.trans ⟨_, _⟩)
[GOAL]
case inr.intro.refine'_1
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
x : α
hx : x ∈ s
⊢ (∃ a, s = {a}) → ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a = b
[PROOFSTEP]
rintro ⟨y, rfl⟩
[GOAL]
case inr.intro.refine'_1.intro
α : Type u_1
β : Type u_2
t : Finset α
f : α → β
n : ℕ
x y : α
hx : x ∈ {y}
⊢ ∀ (a : α), a ∈ {y} → ∀ (b : α), b ∈ {y} → a = b
[PROOFSTEP]
simp
[GOAL]
case inr.intro.refine'_2
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
x : α
hx : x ∈ s
⊢ (∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a = b) → ∃ a, s = {a}
[PROOFSTEP]
exact fun h => ⟨x, eq_singleton_iff_unique_mem.2 ⟨hx, fun y hy => h _ hy _ hx⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
⊢ card s ≤ 1 ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b
[PROOFSTEP]
rw [card_le_one]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
⊢ (∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a = b) ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : Nonempty α
⊢ card s ≤ 1 ↔ ∃ x, s ⊆ {x}
[PROOFSTEP]
refine' ⟨fun H => _, _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : Nonempty α
H : card s ≤ 1
⊢ ∃ x, s ⊆ {x}
[PROOFSTEP]
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
[GOAL]
case refine'_1.inl
α : Type u_1
β : Type u_2
t : Finset α
f : α → β
n : ℕ
inst✝ : Nonempty α
H : card ∅ ≤ 1
⊢ ∃ x, ∅ ⊆ {x}
[PROOFSTEP]
exact ⟨Classical.arbitrary α, empty_subset _⟩
[GOAL]
case refine'_1.inr.intro
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : Nonempty α
H : card s ≤ 1
x : α
hx : x ∈ s
⊢ ∃ x, s ⊆ {x}
[PROOFSTEP]
exact ⟨x, fun y hy => by rw [card_le_one.1 H y hy x hx, mem_singleton]⟩
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : Nonempty α
H : card s ≤ 1
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ y ∈ {x}
[PROOFSTEP]
rw [card_le_one.1 H y hy x hx, mem_singleton]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : Nonempty α
⊢ (∃ x, s ⊆ {x}) → card s ≤ 1
[PROOFSTEP]
rintro ⟨x, hx⟩
[GOAL]
case refine'_2.intro
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : Nonempty α
x : α
hx : s ⊆ {x}
⊢ card s ≤ 1
[PROOFSTEP]
rw [← card_singleton x]
[GOAL]
case refine'_2.intro
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : Nonempty α
x : α
hx : s ⊆ {x}
⊢ card s ≤ card {x}
[PROOFSTEP]
exact card_le_of_subset hx
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
⊢ 1 < card s ↔ ∃ a, a ∈ s ∧ ∃ b, b ∈ s ∧ a ≠ b
[PROOFSTEP]
rw [← not_iff_not]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
⊢ ¬1 < card s ↔ ¬∃ a, a ∈ s ∧ ∃ b, b ∈ s ∧ a ≠ b
[PROOFSTEP]
push_neg
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
⊢ card s ≤ 1 ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a = b
[PROOFSTEP]
exact card_le_one
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
⊢ 1 < card s ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
[PROOFSTEP]
rw [one_lt_card]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
⊢ (∃ a, a ∈ s ∧ ∃ b, b ∈ s ∧ a ≠ b) ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
[PROOFSTEP]
simp only [exists_prop, exists_and_left]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
⊢ 2 < card s ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
[PROOFSTEP]
classical
refine' ⟨fun h => _, _⟩
· obtain ⟨c, hc⟩ := card_pos.mp (pos_of_gt h)
  have : 1 < (s.erase c).card := by rwa [← add_lt_add_iff_right 1, card_erase_add_one hc]
  obtain ⟨a, b, ha, hb, hab⟩ := one_lt_card_iff.mp this
  exact ⟨a, b, c, mem_of_mem_erase ha, mem_of_mem_erase hb, hc, hab, ne_of_mem_erase ha, ne_of_mem_erase hb⟩
· rintro ⟨a, b, c, ha, hb, hc, hab, hac, hbc⟩
  rw [← card_erase_add_one hc, ← card_erase_add_one (mem_erase_of_ne_of_mem hbc hb), ←
    card_erase_add_one (mem_erase_of_ne_of_mem hab (mem_erase_of_ne_of_mem hac ha))]
  apply Nat.le_add_left
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
⊢ 2 < card s ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
h : 2 < card s
⊢ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
[PROOFSTEP]
obtain ⟨c, hc⟩ := card_pos.mp (pos_of_gt h)
[GOAL]
case refine'_1.intro
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
h : 2 < card s
c : α
hc : c ∈ s
⊢ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
[PROOFSTEP]
have : 1 < (s.erase c).card := by rwa [← add_lt_add_iff_right 1, card_erase_add_one hc]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
h : 2 < card s
c : α
hc : c ∈ s
⊢ 1 < card (erase s c)
[PROOFSTEP]
rwa [← add_lt_add_iff_right 1, card_erase_add_one hc]
[GOAL]
case refine'_1.intro
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
h : 2 < card s
c : α
hc : c ∈ s
this : 1 < card (erase s c)
⊢ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
[PROOFSTEP]
obtain ⟨a, b, ha, hb, hab⟩ := one_lt_card_iff.mp this
[GOAL]
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
h : 2 < card s
c : α
hc : c ∈ s
this : 1 < card (erase s c)
a b : α
ha : a ∈ erase s c
hb : b ∈ erase s c
hab : a ≠ b
⊢ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
[PROOFSTEP]
exact ⟨a, b, c, mem_of_mem_erase ha, mem_of_mem_erase hb, hc, hab, ne_of_mem_erase ha, ne_of_mem_erase hb⟩
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
⊢ (∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c) → 2 < card s
[PROOFSTEP]
rintro ⟨a, b, c, ha, hb, hc, hab, hac, hbc⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ 2 < card s
[PROOFSTEP]
rw [← card_erase_add_one hc, ← card_erase_add_one (mem_erase_of_ne_of_mem hbc hb), ←
  card_erase_add_one (mem_erase_of_ne_of_mem hab (mem_erase_of_ne_of_mem hac ha))]
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ 2 < card (erase (erase (erase s c) b) a) + 1 + 1 + 1
[PROOFSTEP]
apply Nat.le_add_left
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
⊢ 2 < card s ↔ ∃ a, a ∈ s ∧ ∃ b, b ∈ s ∧ ∃ c, c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
[PROOFSTEP]
simp_rw [two_lt_card_iff, exists_and_left]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
hs : 1 < card s
a : α
⊢ ∃ b, b ∈ s ∧ b ≠ a
[PROOFSTEP]
obtain ⟨x, hx, y, hy, hxy⟩ := Finset.one_lt_card.mp hs
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
hs : 1 < card s
a x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
⊢ ∃ b, b ∈ s ∧ b ≠ a
[PROOFSTEP]
by_cases ha : y = a
[GOAL]
case pos
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
hs : 1 < card s
a x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
ha : y = a
⊢ ∃ b, b ∈ s ∧ b ≠ a
[PROOFSTEP]
exact ⟨x, hx, ne_of_ne_of_eq hxy ha⟩
[GOAL]
case neg
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
hs : 1 < card s
a x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
ha : ¬y = a
⊢ ∃ b, b ∈ s ∧ b ≠ a
[PROOFSTEP]
exact ⟨y, hy, ha⟩
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
h : card s = n + 1
a : α
has : a ∈ s
⊢ card (erase s a) = n
[PROOFSTEP]
simp only [h, card_erase_of_mem has, add_tsub_cancel_right]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ card s = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y}
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ card s = 2 → ∃ x y, x ≠ y ∧ s = {x, y}
[PROOFSTEP]
rw [card_eq_succ]
[GOAL]
case mp
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ (∃ a t, ¬a ∈ t ∧ insert a t = s ∧ card t = 1) → ∃ x y, x ≠ y ∧ s = {x, y}
[PROOFSTEP]
simp_rw [card_eq_one]
[GOAL]
case mp
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ (∃ a t, ¬a ∈ t ∧ insert a t = s ∧ ∃ a, t = {a}) → ∃ x y, x ≠ y ∧ s = {x, y}
[PROOFSTEP]
rintro ⟨a, _, hab, rfl, b, rfl⟩
[GOAL]
case mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
a b : α
hab : ¬a ∈ {b}
⊢ ∃ x y, x ≠ y ∧ {a, b} = {x, y}
[PROOFSTEP]
exact ⟨a, b, not_mem_singleton.1 hab, rfl⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ (∃ x y, x ≠ y ∧ s = {x, y}) → card s = 2
[PROOFSTEP]
rintro ⟨x, y, h, rfl⟩
[GOAL]
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
x y : α
h : x ≠ y
⊢ card {x, y} = 2
[PROOFSTEP]
exact card_doubleton h
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ card s = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ card s = 3 → ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
[PROOFSTEP]
rw [card_eq_succ]
[GOAL]
case mp
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ (∃ a t, ¬a ∈ t ∧ insert a t = s ∧ card t = 2) → ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
[PROOFSTEP]
simp_rw [card_eq_two]
[GOAL]
case mp
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ (∃ a t, ¬a ∈ t ∧ insert a t = s ∧ ∃ x y, x ≠ y ∧ t = {x, y}) → ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
[PROOFSTEP]
rintro ⟨a, _, abc, rfl, b, c, bc, rfl⟩
[GOAL]
case mp.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
a b c : α
bc : b ≠ c
abc : ¬a ∈ {b, c}
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ {a, b, c} = {x, y, z}
[PROOFSTEP]
rw [mem_insert, mem_singleton, not_or] at abc
[GOAL]
case mp.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
a b c : α
bc : b ≠ c
abc : ¬a = b ∧ ¬a = c
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ {a, b, c} = {x, y, z}
[PROOFSTEP]
exact ⟨a, b, c, abc.1, abc.2, bc, rfl⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ (∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}) → card s = 3
[PROOFSTEP]
rintro ⟨x, y, z, xy, xz, yz, rfl⟩
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
x y z : α
xy : x ≠ y
xz : x ≠ z
yz : y ≠ z
⊢ card {x, y, z} = 3
[PROOFSTEP]
simp only [xy, xz, yz, mem_insert, card_insert_of_not_mem, not_false_iff, mem_singleton, or_self_iff, card_singleton]
[GOAL]
α : Type u_1
β : Type u_2
s✝ t : Finset α
f : α → β
n : ℕ
p : Finset α → Sort u_3
H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s
s : Finset α
⊢ strongInduction H s = H s fun t x => strongInduction H t
[PROOFSTEP]
rw [strongInduction]
[GOAL]
α : Type u_1
β : Type u_2
s✝ t : Finset α
f : α → β
n : ℕ
p : Finset α → Sort u_3
s : Finset α
H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s
⊢ strongInductionOn s H = H s fun t x => strongInductionOn t H
[PROOFSTEP]
dsimp only [strongInductionOn]
[GOAL]
α : Type u_1
β : Type u_2
s✝ t : Finset α
f : α → β
n : ℕ
p : Finset α → Sort u_3
s : Finset α
H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s
⊢ strongInduction H s = H s fun t x => strongInduction H t
[PROOFSTEP]
rw [strongInduction]
[GOAL]
α : Type u_1
β : Type u_2
s✝ t : Finset α
f : α → β
n : ℕ
p : Finset α → Sort u_3
H : (t₁ : Finset α) → ({t₂ : Finset α} → card t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → card t₁ ≤ n → p t₁
s : Finset α
⊢ strongDownwardInduction H s = H s fun {t} ht x => strongDownwardInduction H t ht
[PROOFSTEP]
rw [strongDownwardInduction]
[GOAL]
α : Type u_1
β : Type u_2
s✝ t : Finset α
f : α → β
n : ℕ
p : Finset α → Sort u_3
s : Finset α
H : (t₁ : Finset α) → ({t₂ : Finset α} → card t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → card t₁ ≤ n → p t₁
⊢ (fun a => strongDownwardInductionOn s H a) = H s fun {t} ht x => strongDownwardInductionOn t H ht
[PROOFSTEP]
dsimp only [strongDownwardInductionOn]
[GOAL]
α : Type u_1
β : Type u_2
s✝ t : Finset α
f : α → β
n : ℕ
p : Finset α → Sort u_3
s : Finset α
H : (t₁ : Finset α) → ({t₂ : Finset α} → card t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → card t₁ ≤ n → p t₁
⊢ (fun a => strongDownwardInduction H s a) = H s fun {t} ht x => strongDownwardInduction H t ht
[PROOFSTEP]
rw [strongDownwardInduction]