case intro
ι : Type u_2
α : ι → Type u_1
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
ι : Type u_2
α : ι → Type u_1
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
cases nonempty_fintype ι
case intro.a
ι : Type u_2
α : ι → Type u_1
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
case intro
ι : Type u_2
α : ι → Type u_1
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
induction' hs : univ.sigma f using Finset.strongInductionOn with s ihs generalizing f
case intro.a
ι : Type u_2
α : ι → Type u_1
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
case intro.a
ι : Type u_2
α : ι → Type u_1
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
subst s
case intro.a.inl
ι : Type u_2
α : ι → Type u_1
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

case intro.a.inr
ι : Type u_2
α : ι → Type u_1
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
case intro.a
ι : Type u_2
α : ι → Type u_1
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
cases' eq_empty_or_nonempty (univ.sigma f) with he hne
case h.e'_1
ι : Type u_2
α : ι → Type u_1
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 => ∅
case intro.a.inl
ι : Type u_2
α : ι → Type u_1
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
convert h0 using 1
no goals
case h.e'_1
ι : Type u_2
α : ι → Type u_1
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 => ∅
simpa [funext_iff] using he
case intro.a.inr.intro.intro
ι : Type u_2
α : ι → Type u_1
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
case intro.a.inr
ι : Type u_2
α : ι → Type u_1
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
rcases sigma_nonempty.1 hne with ⟨i, -, hi⟩
case intro.a.inr.intro.intro.intro.intro
ι : Type u_2
α : ι → Type u_1
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
case intro.a.inr.intro.intro
ι : Type u_2
α : ι → Type u_1
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
rcases H_ex i (f i) hi with ⟨x, x_mem, hr⟩
case intro.a.inr.intro.intro.intro.intro
ι : Type u_2
α : ι → Type u_1
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
case intro.a.inr.intro.intro.intro.intro
ι : Type u_2
α : ι → Type u_1
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
set g := update f i ((f i).erase x) with hg
case intro.a.inr.intro.intro.intro.intro
ι : Type u_2
α : ι → Type u_1
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
case intro.a.inr.intro.intro.intro.intro
ι : Type u_2
α : ι → Type u_1
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
have hx' : x ∉ g i := by
  rw [hg, update_same]
  apply not_mem_erase
case intro.a.inr.intro.intro.intro.intro
ι : Type u_2
α : ι → Type u_1
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)))
case intro.a.inr.intro.intro.intro.intro
ι : Type u_2
α : ι → Type u_1
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
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 ⊢
case intro.a.inr.intro.intro.intro.intro
ι : Type u_2
α : ι → Type u_1
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)))
case intro.a.inr.intro.intro.intro.intro
ι : Type u_2
α : ι → Type u_1
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)))
clear hg
case intro.a.inr.intro.intro.intro.intro
ι : Type u_2
α : ι → Type u_1
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)))
case intro.a.inr.intro.intro.intro.intro
ι : Type u_2
α : ι → Type u_1
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)))
rw [update_same, erase_insert hx'] at hr
case intro.a.inr.intro.intro.intro.intro
ι : Type u_2
α : ι → Type u_1
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)))
case intro.a.inr.intro.intro.intro.intro
ι : Type u_2
α : ι → Type u_1
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)))
refine step _ _ _ hr (ihs (univ.sigma g) ?_ _ rfl)
case intro.a.inr.intro.intro.intro.intro
ι : Type u_2
α : ι → Type u_1
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_2
α : ι → Type u_1
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
case intro.a.inr.intro.intro.intro.intro
ι : Type u_2
α : ι → Type u_1
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)))
rw [ssubset_iff_of_subset (sigma_mono (Subset.refl _) _)]
no goals
case intro.a.inr.intro.intro.intro.intro
ι : Type u_2
α : ι → Type u_1
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_2
α : ι → Type u_1
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
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⟩]
ι : Type u_2
α : ι → Type u_1
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
ι : Type u_2
α : ι → Type u_1
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
rw [hg, update_same]
no goals
ι : Type u_2
α : ι → Type u_1
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
apply not_mem_erase
no goals
ι : Type u_2
α : ι → Type u_1
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))
rw [hg, update_idem, update_same, insert_erase x_mem, update_eq_self]
no goals
ι : Type u_2
α : ι → Type u_1
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
simp
no goals
ι : Type u_2
α : ι → Type u_1
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
simp [hx']