[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), Finset.Nonempty s → ∃ x, x ∈ s ∧ r i x (erase s x)
p : ((i : ι) → Finset (α i)) → Prop
f : (i : ι) → Finset (α i)
h0 : p fun x => ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
⊢ p f
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), Finset.Nonempty s → ∃ x, x ∈ s ∧ r i x (erase s x)
p : ((i : ι) → Finset (α i)) → Prop
f : (i : ι) → Finset (α i)
h0 : p fun x => ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
⊢ p f
[PROOFSTEP]
induction' hs : univ.sigma f using Finset.strongInductionOn with s ihs generalizing f
[GOAL]
case intro.a
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), Finset.Nonempty s → ∃ x, x ∈ s ∧ r i x (erase s x)
p : ((i : ι) → Finset (α i)) → Prop
f✝ : (i : ι) → Finset (α i)
h0 : p fun x => ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
x✝ : Finset ((i : ι) × α i)
hs✝ : Finset.sigma univ f✝ = x✝
s : Finset ((i : ι) × α i)
ihs : ∀ (t : Finset ((i : ι) × α i)), t ⊂ s → ∀ (f : (i : ι) → Finset (α i)), Finset.sigma univ f = t → p f
f : (i : ι) → Finset (α i)
hs : Finset.sigma univ f = s
⊢ p f
[PROOFSTEP]
subst s
[GOAL]
case intro.a
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), Finset.Nonempty s → ∃ x, x ∈ s ∧ r i x (erase s x)
p : ((i : ι) → Finset (α i)) → Prop
f✝ : (i : ι) → Finset (α i)
h0 : p fun x => ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
x✝ : Finset ((i : ι) × α i)
hs : Finset.sigma univ f✝ = x✝
f : (i : ι) → Finset (α i)
ihs :
  ∀ (t : Finset ((i : ι) × α i)),
    t ⊂ Finset.sigma univ f → ∀ (f : (i : ι) → Finset (α i)), Finset.sigma univ f = t → p f
⊢ p f
[PROOFSTEP]
cases' eq_empty_or_nonempty (univ.sigma f) with he hne
[GOAL]
case intro.a.inl
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), Finset.Nonempty s → ∃ x, x ∈ s ∧ r i x (erase s x)
p : ((i : ι) → Finset (α i)) → Prop
f✝ : (i : ι) → Finset (α i)
h0 : p fun x => ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
x✝ : Finset ((i : ι) × α i)
hs : Finset.sigma univ f✝ = x✝
f : (i : ι) → Finset (α i)
ihs :
  ∀ (t : Finset ((i : ι) × α i)),
    t ⊂ Finset.sigma univ f → ∀ (f : (i : ι) → Finset (α i)), Finset.sigma univ f = t → p f
he : Finset.sigma univ f = ∅
⊢ p f
[PROOFSTEP]
convert h0 using 1
[GOAL]
case h.e'_1
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), Finset.Nonempty s → ∃ x, x ∈ s ∧ r i x (erase s x)
p : ((i : ι) → Finset (α i)) → Prop
f✝ : (i : ι) → Finset (α i)
h0 : p fun x => ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
x✝ : Finset ((i : ι) × α i)
hs : Finset.sigma univ f✝ = x✝
f : (i : ι) → Finset (α i)
ihs :
  ∀ (t : Finset ((i : ι) × α i)),
    t ⊂ Finset.sigma univ f → ∀ (f : (i : ι) → Finset (α i)), Finset.sigma univ f = t → p f
he : Finset.sigma univ f = ∅
⊢ f = fun x => ∅
[PROOFSTEP]
simpa [funext_iff] using he
[GOAL]
case intro.a.inr
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), Finset.Nonempty s → ∃ x, x ∈ s ∧ r i x (erase s x)
p : ((i : ι) → Finset (α i)) → Prop
f✝ : (i : ι) → Finset (α i)
h0 : p fun x => ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
x✝ : Finset ((i : ι) × α i)
hs : Finset.sigma univ f✝ = x✝
f : (i : ι) → Finset (α i)
ihs :
  ∀ (t : Finset ((i : ι) × α i)),
    t ⊂ Finset.sigma univ f → ∀ (f : (i : ι) → Finset (α i)), Finset.sigma univ f = t → p f
hne : Finset.Nonempty (Finset.sigma univ f)
⊢ p f
[PROOFSTEP]
rcases sigma_nonempty.1 hne with ⟨i, -, hi⟩
[GOAL]
case intro.a.inr.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), Finset.Nonempty s → ∃ x, x ∈ s ∧ r i x (erase s x)
p : ((i : ι) → Finset (α i)) → Prop
f✝ : (i : ι) → Finset (α i)
h0 : p fun x => ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
x✝ : Finset ((i : ι) × α i)
hs : Finset.sigma univ f✝ = x✝
f : (i : ι) → Finset (α i)
ihs :
  ∀ (t : Finset ((i : ι) × α i)),
    t ⊂ Finset.sigma univ f → ∀ (f : (i : ι) → Finset (α i)), Finset.sigma univ f = t → p f
hne : Finset.Nonempty (Finset.sigma univ f)
i : ι
hi : Finset.Nonempty (f i)
⊢ p f
[PROOFSTEP]
rcases H_ex i (f i) hi with ⟨x, x_mem, hr⟩
[GOAL]
case intro.a.inr.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), Finset.Nonempty s → ∃ x, x ∈ s ∧ r i x (erase s x)
p : ((i : ι) → Finset (α i)) → Prop
f✝ : (i : ι) → Finset (α i)
h0 : p fun x => ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
x✝ : Finset ((i : ι) × α i)
hs : Finset.sigma univ f✝ = x✝
f : (i : ι) → Finset (α i)
ihs :
  ∀ (t : Finset ((i : ι) × α i)),
    t ⊂ Finset.sigma univ f → ∀ (f : (i : ι) → Finset (α i)), Finset.sigma univ f = t → p f
hne : Finset.Nonempty (Finset.sigma univ f)
i : ι
hi : Finset.Nonempty (f i)
x : α i
x_mem : x ∈ f i
hr : r i x (erase (f i) x)
⊢ p f
[PROOFSTEP]
set g := update f i ((f i).erase x) with hg
[GOAL]
case intro.a.inr.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), Finset.Nonempty s → ∃ x, x ∈ s ∧ r i x (erase s x)
p : ((i : ι) → Finset (α i)) → Prop
f✝ : (i : ι) → Finset (α i)
h0 : p fun x => ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
x✝ : Finset ((i : ι) × α i)
hs : Finset.sigma univ f✝ = x✝
f : (i : ι) → Finset (α i)
ihs :
  ∀ (t : Finset ((i : ι) × α i)),
    t ⊂ Finset.sigma univ f → ∀ (f : (i : ι) → Finset (α i)), Finset.sigma univ f = t → p f
hne : Finset.Nonempty (Finset.sigma univ f)
i : ι
hi : Finset.Nonempty (f i)
x : α i
x_mem : x ∈ f i
hr : r i x (erase (f i) x)
g : (a : ι) → Finset (α a) := update f i (erase (f i) x)
hg : g = update f i (erase (f i) x)
⊢ p f
[PROOFSTEP]
have hx' : x ∉ g i := by
  rw [hg, update_same]
  apply not_mem_erase
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), Finset.Nonempty s → ∃ x, x ∈ s ∧ r i x (erase s x)
p : ((i : ι) → Finset (α i)) → Prop
f✝ : (i : ι) → Finset (α i)
h0 : p fun x => ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
x✝ : Finset ((i : ι) × α i)
hs : Finset.sigma univ f✝ = x✝
f : (i : ι) → Finset (α i)
ihs :
  ∀ (t : Finset ((i : ι) × α i)),
    t ⊂ Finset.sigma univ f → ∀ (f : (i : ι) → Finset (α i)), Finset.sigma univ f = t → p f
hne : Finset.Nonempty (Finset.sigma univ f)
i : ι
hi : Finset.Nonempty (f i)
x : α i
x_mem : x ∈ f i
hr : r i x (erase (f i) x)
g : (a : ι) → Finset (α a) := update f i (erase (f i) x)
hg : g = update f i (erase (f i) x)
⊢ ¬x ∈ g i
[PROOFSTEP]
rw [hg, update_same]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), Finset.Nonempty s → ∃ x, x ∈ s ∧ r i x (erase s x)
p : ((i : ι) → Finset (α i)) → Prop
f✝ : (i : ι) → Finset (α i)
h0 : p fun x => ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
x✝ : Finset ((i : ι) × α i)
hs : Finset.sigma univ f✝ = x✝
f : (i : ι) → Finset (α i)
ihs :
  ∀ (t : Finset ((i : ι) × α i)),
    t ⊂ Finset.sigma univ f → ∀ (f : (i : ι) → Finset (α i)), Finset.sigma univ f = t → p f
hne : Finset.Nonempty (Finset.sigma univ f)
i : ι
hi : Finset.Nonempty (f i)
x : α i
x_mem : x ∈ f i
hr : r i x (erase (f i) x)
g : (a : ι) → Finset (α a) := update f i (erase (f i) x)
hg : g = update f i (erase (f i) x)
⊢ ¬x ∈ erase (f i) x
[PROOFSTEP]
apply not_mem_erase
[GOAL]
case intro.a.inr.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), Finset.Nonempty s → ∃ x, x ∈ s ∧ r i x (erase s x)
p : ((i : ι) → Finset (α i)) → Prop
f✝ : (i : ι) → Finset (α i)
h0 : p fun x => ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
x✝ : Finset ((i : ι) × α i)
hs : Finset.sigma univ f✝ = x✝
f : (i : ι) → Finset (α i)
ihs :
  ∀ (t : Finset ((i : ι) × α i)),
    t ⊂ Finset.sigma univ f → ∀ (f : (i : ι) → Finset (α i)), Finset.sigma univ f = t → p f
hne : Finset.Nonempty (Finset.sigma univ f)
i : ι
hi : Finset.Nonempty (f i)
x : α i
x_mem : x ∈ f i
hr : r i x (erase (f i) x)
g : (a : ι) → Finset (α a) := update f i (erase (f i) x)
hg : g = update f i (erase (f i) x)
hx' : ¬x ∈ g i
⊢ p f
[PROOFSTEP]
rw [show f = update g i (insert x (g i)) by rw [hg, update_idem, update_same, insert_erase x_mem, update_eq_self]] at hr
  ihs ⊢
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), Finset.Nonempty s → ∃ x, x ∈ s ∧ r i x (erase s x)
p : ((i : ι) → Finset (α i)) → Prop
f✝ : (i : ι) → Finset (α i)
h0 : p fun x => ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
x✝ : Finset ((i : ι) × α i)
hs : Finset.sigma univ f✝ = x✝
f : (i : ι) → Finset (α i)
ihs :
  ∀ (t : Finset ((i : ι) × α i)),
    t ⊂ Finset.sigma univ f → ∀ (f : (i : ι) → Finset (α i)), Finset.sigma univ f = t → p f
hne : Finset.Nonempty (Finset.sigma univ f)
i : ι
hi : Finset.Nonempty (f i)
x : α i
x_mem : x ∈ f i
hr : r i x (erase (f i) x)
g : (a : ι) → Finset (α a) := update f i (erase (f i) x)
hg : g = update f i (erase (f i) x)
hx' : ¬x ∈ g i
⊢ f = update g i (insert x (g i))
[PROOFSTEP]
rw [hg, update_idem, update_same, insert_erase x_mem, update_eq_self]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), Finset.Nonempty s → ∃ x, x ∈ s ∧ r i x (erase s x)
p : ((i : ι) → Finset (α i)) → Prop
f✝ : (i : ι) → Finset (α i)
h0 : p fun x => ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
x✝ : Finset ((i : ι) × α i)
hs : Finset.sigma univ f✝ = x✝
f : (i : ι) → Finset (α i)
ihs :
  ∀ (t : Finset ((i : ι) × α i)),
    t ⊂ Finset.sigma univ f → ∀ (f : (i : ι) → Finset (α i)), Finset.sigma univ f = t → p f
hne : Finset.Nonempty (Finset.sigma univ f)
i : ι
hi : Finset.Nonempty (f i)
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a) := update f i (erase (f i) x)
hr : r i x (erase (update g i (insert x (g i)) i) x)
hg : g = update f i (erase (f i) x)
hx' : ¬x ∈ g i
⊢ f = update g i (insert x (g i))
[PROOFSTEP]
rw [hg, update_idem, update_same, insert_erase x_mem, update_eq_self]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), Finset.Nonempty s → ∃ x, x ∈ s ∧ r i x (erase s x)
p : ((i : ι) → Finset (α i)) → Prop
f✝ : (i : ι) → Finset (α i)
h0 : p fun x => ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
x✝ : Finset ((i : ι) × α i)
hs : Finset.sigma univ f✝ = x✝
f : (i : ι) → Finset (α i)
hne : Finset.Nonempty (Finset.sigma univ f)
i : ι
hi : Finset.Nonempty (f i)
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a) := update f i (erase (f i) x)
ihs :
  ∀ (t : Finset ((i : ι) × α i)),
    t ⊂ Finset.sigma univ (update g i (insert x (g i))) → ∀ (f : (i : ι) → Finset (α i)), Finset.sigma univ f = t → p f
hr : r i x (erase (update g i (insert x (g i)) i) x)
hg : g = update f i (erase (f i) x)
hx' : ¬x ∈ g i
⊢ f = update g i (insert x (g i))
[PROOFSTEP]
rw [hg, update_idem, update_same, insert_erase x_mem, update_eq_self]
[GOAL]
case intro.a.inr.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), Finset.Nonempty s → ∃ x, x ∈ s ∧ r i x (erase s x)
p : ((i : ι) → Finset (α i)) → Prop
f✝ : (i : ι) → Finset (α i)
h0 : p fun x => ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
x✝ : Finset ((i : ι) × α i)
hs : Finset.sigma univ f✝ = x✝
f : (i : ι) → Finset (α i)
hne : Finset.Nonempty (Finset.sigma univ f)
i : ι
hi : Finset.Nonempty (f i)
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a) := update f i (erase (f i) x)
ihs :
  ∀ (t : Finset ((i : ι) × α i)),
    t ⊂ Finset.sigma univ (update g i (insert x (g i))) → ∀ (f : (i : ι) → Finset (α i)), Finset.sigma univ f = t → p f
hr : r i x (erase (update g i (insert x (g i)) i) x)
hg : g = update f i (erase (f i) x)
hx' : ¬x ∈ g i
⊢ p (update g i (insert x (g i)))
[PROOFSTEP]
clear hg
[GOAL]
case intro.a.inr.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), Finset.Nonempty s → ∃ x, x ∈ s ∧ r i x (erase s x)
p : ((i : ι) → Finset (α i)) → Prop
f✝ : (i : ι) → Finset (α i)
h0 : p fun x => ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
x✝ : Finset ((i : ι) × α i)
hs : Finset.sigma univ f✝ = x✝
f : (i : ι) → Finset (α i)
hne : Finset.Nonempty (Finset.sigma univ f)
i : ι
hi : Finset.Nonempty (f i)
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a) := update f i (erase (f i) x)
ihs :
  ∀ (t : Finset ((i : ι) × α i)),
    t ⊂ Finset.sigma univ (update g i (insert x (g i))) → ∀ (f : (i : ι) → Finset (α i)), Finset.sigma univ f = t → p f
hr : r i x (erase (update g i (insert x (g i)) i) x)
hx' : ¬x ∈ g i
⊢ p (update g i (insert x (g i)))
[PROOFSTEP]
rw [update_same, erase_insert hx'] at hr
[GOAL]
case intro.a.inr.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), Finset.Nonempty s → ∃ x, x ∈ s ∧ r i x (erase s x)
p : ((i : ι) → Finset (α i)) → Prop
f✝ : (i : ι) → Finset (α i)
h0 : p fun x => ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
x✝ : Finset ((i : ι) × α i)
hs : Finset.sigma univ f✝ = x✝
f : (i : ι) → Finset (α i)
hne : Finset.Nonempty (Finset.sigma univ f)
i : ι
hi : Finset.Nonempty (f i)
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a) := update f i (erase (f i) x)
ihs :
  ∀ (t : Finset ((i : ι) × α i)),
    t ⊂ Finset.sigma univ (update g i (insert x (g i))) → ∀ (f : (i : ι) → Finset (α i)), Finset.sigma univ f = t → p f
hr : r i x (g i)
hx' : ¬x ∈ g i
⊢ p (update g i (insert x (g i)))
[PROOFSTEP]
refine step _ _ _ hr (ihs (univ.sigma g) ?_ _ rfl)
[GOAL]
case intro.a.inr.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), Finset.Nonempty s → ∃ x, x ∈ s ∧ r i x (erase s x)
p : ((i : ι) → Finset (α i)) → Prop
f✝ : (i : ι) → Finset (α i)
h0 : p fun x => ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
x✝ : Finset ((i : ι) × α i)
hs : Finset.sigma univ f✝ = x✝
f : (i : ι) → Finset (α i)
hne : Finset.Nonempty (Finset.sigma univ f)
i : ι
hi : Finset.Nonempty (f i)
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a) := update f i (erase (f i) x)
ihs :
  ∀ (t : Finset ((i : ι) × α i)),
    t ⊂ Finset.sigma univ (update g i (insert x (g i))) → ∀ (f : (i : ι) → Finset (α i)), Finset.sigma univ f = t → p f
hr : r i x (g i)
hx' : ¬x ∈ g i
⊢ Finset.sigma univ g ⊂ Finset.sigma univ (update g i (insert x (g i)))
[PROOFSTEP]
rw [ssubset_iff_of_subset (sigma_mono (Subset.refl _) _)]
[GOAL]
case intro.a.inr.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), Finset.Nonempty s → ∃ x, x ∈ s ∧ r i x (erase s x)
p : ((i : ι) → Finset (α i)) → Prop
f✝ : (i : ι) → Finset (α i)
h0 : p fun x => ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
x✝ : Finset ((i : ι) × α i)
hs : Finset.sigma univ f✝ = x✝
f : (i : ι) → Finset (α i)
hne : Finset.Nonempty (Finset.sigma univ f)
i : ι
hi : Finset.Nonempty (f i)
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a) := update f i (erase (f i) x)
ihs :
  ∀ (t : Finset ((i : ι) × α i)),
    t ⊂ Finset.sigma univ (update g i (insert x (g i))) → ∀ (f : (i : ι) → Finset (α i)), Finset.sigma univ f = t → p f
hr : r i x (g i)
hx' : ¬x ∈ g i
⊢ ∃ x_1, x_1 ∈ Finset.sigma univ (update g i (insert x (g i))) ∧ ¬x_1 ∈ Finset.sigma univ g
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), Finset.Nonempty s → ∃ x, x ∈ s ∧ r i x (erase s x)
p : ((i : ι) → Finset (α i)) → Prop
f✝ : (i : ι) → Finset (α i)
h0 : p fun x => ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
x✝ : Finset ((i : ι) × α i)
hs : Finset.sigma univ f✝ = x✝
f : (i : ι) → Finset (α i)
hne : Finset.Nonempty (Finset.sigma univ f)
i : ι
hi : Finset.Nonempty (f i)
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a) := update f i (erase (f i) x)
ihs :
  ∀ (t : Finset ((i : ι) × α i)),
    t ⊂ Finset.sigma univ (update g i (insert x (g i))) → ∀ (f : (i : ι) → Finset (α i)), Finset.sigma univ f = t → p f
hr : r i x (g i)
hx' : ¬x ∈ g i
⊢ ∀ (i_1 : ι), g i_1 ⊆ update g i (insert x (g i)) i_1
[PROOFSTEP]
exacts [⟨⟨i, x⟩, mem_sigma.2 ⟨mem_univ _, by simp⟩, by simp [hx']⟩,
  (@le_update_iff _ _ _ _ g g i _).2 ⟨subset_insert _ _, fun _ _ ↦ le_rfl⟩]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), Finset.Nonempty s → ∃ x, x ∈ s ∧ r i x (erase s x)
p : ((i : ι) → Finset (α i)) → Prop
f✝ : (i : ι) → Finset (α i)
h0 : p fun x => ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
x✝ : Finset ((i : ι) × α i)
hs : Finset.sigma univ f✝ = x✝
f : (i : ι) → Finset (α i)
hne : Finset.Nonempty (Finset.sigma univ f)
i : ι
hi : Finset.Nonempty (f i)
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a) := update f i (erase (f i) x)
ihs :
  ∀ (t : Finset ((i : ι) × α i)),
    t ⊂ Finset.sigma univ (update g i (insert x (g i))) → ∀ (f : (i : ι) → Finset (α i)), Finset.sigma univ f = t → p f
hr : r i x (g i)
hx' : ¬x ∈ g i
⊢ { fst := i, snd := x }.snd ∈ update g i (insert x (g i)) { fst := i, snd := x }.fst
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), Finset.Nonempty s → ∃ x, x ∈ s ∧ r i x (erase s x)
p : ((i : ι) → Finset (α i)) → Prop
f✝ : (i : ι) → Finset (α i)
h0 : p fun x => ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
x✝ : Finset ((i : ι) × α i)
hs : Finset.sigma univ f✝ = x✝
f : (i : ι) → Finset (α i)
hne : Finset.Nonempty (Finset.sigma univ f)
i : ι
hi : Finset.Nonempty (f i)
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a) := update f i (erase (f i) x)
ihs :
  ∀ (t : Finset ((i : ι) × α i)),
    t ⊂ Finset.sigma univ (update g i (insert x (g i))) → ∀ (f : (i : ι) → Finset (α i)), Finset.sigma univ f = t → p f
hr : r i x (g i)
hx' : ¬x ∈ g i
⊢ ¬{ fst := i, snd := x } ∈ Finset.sigma univ g
[PROOFSTEP]
simp [hx']