awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.PiInduction
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
    r i x (g i) → p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
val : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ Finset.sigma (α := α) univ f, ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f
he : Finset.sigma (α := α) univ f = ∅
⊢ f = fun (x : ι) ↦ ∅

Tactic:
simpa [funext_iff] using he

Premises used: funext_iff
-- Module: Mathlib.Data.Finset.PiInduction
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
    r i x (g i) → p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
val : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ Finset.sigma (α := α) univ f, ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f
hne : (Finset.sigma (α := α) univ f).Nonempty
intro : ∀ (i : ι) (hi : (f i).Nonempty), p f
⊢ p f

Tactic:
rcases sigma_nonempty.1 hne with ⟨i, -, hi⟩

Premises used: Finset.sigma_nonempty, Iff.mp
-- Module: Mathlib.Data.Finset.PiInduction
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
    r i x (g i) → p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
val : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ Finset.sigma (α := α) univ f, ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f
hne : (Finset.sigma (α := α) univ f).Nonempty
i : ι
hi : (f i).Nonempty
intro : ∀ (x : α i) (x_mem : x ∈ f i) (hr : r i x ((f i).erase x)), p f
⊢ p f

Tactic:
rcases H_ex i (f i) hi with ⟨x, x_mem, hr⟩
-- Module: Mathlib.Data.Finset.PiInduction
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
    r i x (g i) → p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
val : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ Finset.sigma (α := α) univ f, ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f
hne : (Finset.sigma (α := α) univ f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
hr : r i x ((f i).erase x)
intro :
  let g := update (β := fun (a : ι) ↦ Finset (α a)) f i ((f i).erase x);
  ∀ (hg : g = update (β := fun (a : ι) ↦ Finset (α a)) f i ((f i).erase x)), p f
⊢ p f

Tactic:
set g := update f i ((f i).erase x) with hg

Premises used: Function.update, Finset.erase
-- Module: Mathlib.Data.Finset.PiInduction
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
    r i x (g i) → p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
val : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ Finset.sigma (α := α) univ f, ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f
hne : (Finset.sigma (α := α) univ f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
hr : r i x ((f i).erase x)
g : (a : ι) → Finset (α a) := update (β := fun (a : ι) ↦ Finset (α a)) f i ((f i).erase x)
hg : g = update (β := fun (a : ι) ↦ Finset (α a)) f i ((f i).erase x)
intro : ∀ (g : (a : ι) → Finset (α a)) (hg : g = update (β := fun (a : ι) ↦ Finset (α a)) f i ((f i).erase x)), p f
⊢ p f

Tactic:
clear_value g
-- Module: Mathlib.Data.Finset.PiInduction
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
    r i x (g i) → p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
val : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ Finset.sigma (α := α) univ f, ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f
hne : (Finset.sigma (α := α) univ f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
hr : r i x ((f i).erase x)
g : (a : ι) → Finset (α a)
hg : g = update (β := fun (a : ι) ↦ Finset (α a)) f i ((f i).erase x)
rw : x ∉ (f i).erase x
⊢ x ∉ g i

Tactic:
rw [hg, update_self]

Premises used: Function.update_self
-- Module: Mathlib.Data.Finset.PiInduction
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
    r i x (g i) → p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
val : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ Finset.sigma (α := α) univ f, ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f
hne : (Finset.sigma (α := α) univ f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
hr : r i x ((f i).erase x)
g : (a : ι) → Finset (α a)
hg : g = update (β := fun (a : ι) ↦ Finset (α a)) f i ((f i).erase x)
⊢ x ∉ (f i).erase x

Tactic:
apply notMem_erase

Premises used: Finset.notMem_erase
-- Module: Mathlib.Data.Finset.PiInduction
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
    r i x (g i) → p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
val : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ Finset.sigma (α := α) univ f, ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f
hne : (Finset.sigma (α := α) univ f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
hr : r i x ((f i).erase x)
g : (a : ι) → Finset (α a)
hg : g = update (β := fun (a : ι) ↦ Finset (α a)) f i ((f i).erase x)
⊢ x ∉ g i

Tactic:
have hx' : x ∉ g i := by
      rw [hg, update_self]
      apply notMem_erase
-- Module: Mathlib.Data.Finset.PiInduction
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
    r i x (g i) → p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
val : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ Finset.sigma (α := α) univ f, ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f
hne : (Finset.sigma (α := α) univ f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
hr : r i x ((f i).erase x)
g : (a : ι) → Finset (α a)
hg : g = update (β := fun (a : ι) ↦ Finset (α a)) f i ((f i).erase x)
hx' : x ∉ g i
rw :
  f =
    update (β := fun (a : ι) ↦ Finset (α a)) (update (β := fun (a : ι) ↦ Finset (α a)) f i ((f i).erase x)) i
      (insert x (update (β := fun (a : ι) ↦ Finset (α a)) f i ((f i).erase x) i))
rw₁ :
  f =
    update (β := fun (a : ι) ↦ Finset (α a)) f i
      (insert x (update (β := fun (a : ι) ↦ Finset (α a)) f i ((f i).erase x) i))
rw₂ : f = update (β := fun (a : ι) ↦ Finset (α a)) f i (insert x ((f i).erase x))
rw₃ : f = update (β := fun (a : ι) ↦ Finset (α a)) f i (f i)
rw₄ rw₅ : f = f
⊢ f = update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))

Tactic:
rw [hg, update_idem, update_self, insert_erase x_mem, update_eq_self]

Premises used: Function.update_eq_self, Function.update_idem, Function.update_self, Finset.insert_erase
-- Module: Mathlib.Data.Finset.PiInduction
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
    r i x (g i) → p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
val : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ Finset.sigma (α := α) univ f, ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f
hne : (Finset.sigma (α := α) univ f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a)
hr : r i x ((update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i)) i).erase x)
hg : g = update (β := fun (a : ι) ↦ Finset (α a)) f i ((f i).erase x)
hx' : x ∉ g i
rw :
  f =
    update (β := fun (a : ι) ↦ Finset (α a)) (update (β := fun (a : ι) ↦ Finset (α a)) f i ((f i).erase x)) i
      (insert x (update (β := fun (a : ι) ↦ Finset (α a)) f i ((f i).erase x) i))
rw₁ :
  f =
    update (β := fun (a : ι) ↦ Finset (α a)) f i
      (insert x (update (β := fun (a : ι) ↦ Finset (α a)) f i ((f i).erase x) i))
rw₂ : f = update (β := fun (a : ι) ↦ Finset (α a)) f i (insert x ((f i).erase x))
rw₃ : f = update (β := fun (a : ι) ↦ Finset (α a)) f i (f i)
rw₄ rw₅ : f = f
⊢ f = update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))

Tactic:
rw [hg, update_idem, update_self, insert_erase x_mem, update_eq_self]

Premises used: Function.update_eq_self, Function.update_idem, Function.update_self, Finset.insert_erase
-- Module: Mathlib.Data.Finset.PiInduction
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
    r i x (g i) → p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
val : Fintype ι
f : (i : ι) → Finset (α i)
hne : (Finset.sigma (α := α) univ f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a)
ihs :
  ∀ t ⊂ Finset.sigma (α := α) univ (update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))),
    ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f
hr : r i x ((update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i)) i).erase x)
hg : g = update (β := fun (a : ι) ↦ Finset (α a)) f i ((f i).erase x)
hx' : x ∉ g i
rw :
  f =
    update (β := fun (a : ι) ↦ Finset (α a)) (update (β := fun (a : ι) ↦ Finset (α a)) f i ((f i).erase x)) i
      (insert x (update (β := fun (a : ι) ↦ Finset (α a)) f i ((f i).erase x) i))
rw₁ :
  f =
    update (β := fun (a : ι) ↦ Finset (α a)) f i
      (insert x (update (β := fun (a : ι) ↦ Finset (α a)) f i ((f i).erase x) i))
rw₂ : f = update (β := fun (a : ι) ↦ Finset (α a)) f i (insert x ((f i).erase x))
rw₃ : f = update (β := fun (a : ι) ↦ Finset (α a)) f i (f i)
rw₄ rw₅ : f = f
⊢ f = update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))

Tactic:
rw [hg, update_idem, update_self, insert_erase x_mem, update_eq_self]

Premises used: Function.update_eq_self, Function.update_idem, Function.update_self, Finset.insert_erase
-- Module: Mathlib.Data.Finset.PiInduction
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
    r i x (g i) → p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
val : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ Finset.sigma (α := α) univ f, ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f
hne : (Finset.sigma (α := α) univ f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
hr : r i x ((f i).erase x)
g : (a : ι) → Finset (α a)
hg : g = update (β := fun (a : ι) ↦ Finset (α a)) f i ((f i).erase x)
hx' : x ∉ g i
intro :
  ∀
    (ihs :
      ∀ t ⊂ Finset.sigma (α := α) univ (update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))),
        ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f)
    (hr : r i x ((update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i)) i).erase x))
    (hg : g = update (β := fun (a : ι) ↦ Finset (α a)) f i ((f i).erase x)) (hx' : x ∉ g i),
    p (update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i)))
⊢ p f

Tactic:
rw [show f = update g i (insert x (g i)) by
      rw [hg, update_idem, update_self, insert_erase x_mem, update_eq_self]] at hr ihs ⊢
-- Module: Mathlib.Data.Finset.PiInduction
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
    r i x (g i) → p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
val : Fintype ι
f : (i : ι) → Finset (α i)
hne : (Finset.sigma (α := α) univ f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a)
ihs :
  ∀ t ⊂ Finset.sigma (α := α) univ (update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))),
    ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f
hr : r i x ((update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i)) i).erase x)
hx' : x ∉ g i
⊢ r i x (g i)

Tactic:
rw [update_self, erase_insert hx'] at hr

Premises used: Finset.erase_insert, Function.update_self
-- Module: Mathlib.Data.Finset.PiInduction
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
    r i x (g i) → p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
val : Fintype ι
f : (i : ι) → Finset (α i)
hne : (Finset.sigma (α := α) univ f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a)
ihs :
  ∀ t ⊂ Finset.sigma (α := α) univ (update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))),
    ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f
hr : r i x ((update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i)) i).erase x)
hx' : x ∉ g i
hr₁ : r i x (g i)
⊢ x ∉ g i

Tactic:
rw [update_self, erase_insert hx'] at hr

Premises used: Finset.erase_insert, Function.update_self
-- Module: Mathlib.Data.Finset.PiInduction
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
    r i x (g i) → p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
val : Fintype ι
f : (i : ι) → Finset (α i)
hne : (Finset.sigma (α := α) univ f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a)
ihs :
  ∀ t ⊂ Finset.sigma (α := α) univ (update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))),
    ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f
hr : r i x (g i)
hx' : x ∉ g i
⊢ p (update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i)))

Tactic:
step _ _ _ hr (ihs (univ.sigma g) ?_ _ rfl)

Premises used: Finset.univ, Finset.sigma, rfl
-- Module: Mathlib.Data.Finset.PiInduction
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
    r i x (g i) → p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
val : Fintype ι
f : (i : ι) → Finset (α i)
hne : (Finset.sigma (α := α) univ f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a)
ihs :
  ∀ t ⊂ Finset.sigma (α := α) univ (update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))),
    ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f
hr : r i x (g i)
hx' : x ∉ g i
intro :
  Finset.sigma (α := α) univ g ⊂
    Finset.sigma (α := α) univ (update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i)))
⊢ p (update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i)))

Tactic:
refine step _ _ _ hr (ihs (univ.sigma g) ?_ _ rfl)

Premises used: Finset.univ, Finset.sigma, rfl
-- Module: Mathlib.Data.Finset.PiInduction
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
    r i x (g i) → p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
val : Fintype ι
f : (i : ι) → Finset (α i)
hne : (Finset.sigma (α := α) univ f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a)
ihs :
  ∀ t ⊂ Finset.sigma (α := α) univ (update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))),
    ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f
hr : r i x (g i)
hx' : x ∉ g i
intro :
  ∃ x_1 ∈ Finset.sigma (α := α) univ (update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))),
    x_1 ∉ Finset.sigma (α := α) univ g
rw : ∀ (i_1 : ι), g i_1 ⊆ update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i)) i_1
⊢ Finset.sigma (α := α) univ g ⊂
    Finset.sigma (α := α) univ (update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i)))

Tactic:
rw [ssubset_iff_of_subset (sigma_mono (Subset.refl _) _)]

Premises used: Finset.Subset.refl, Finset.sigma_mono, Finset.ssubset_iff_of_subset
-- Module: Mathlib.Data.Finset.PiInduction
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
    r i x (g i) → p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
val : Fintype ι
f : (i : ι) → Finset (α i)
hne : (Finset.sigma (α := α) univ f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a)
ihs :
  ∀ t ⊂ Finset.sigma (α := α) univ (update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))),
    ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f
hr : r i x (g i)
hx' : x ∉ g i
⊢ Membership.mem (γ := Finset (α ((Sigma.mk (β := fun (i : ι) ↦ α i) i x).fst (β := fun (i : ι) ↦ α i))))
    (update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))
      ((Sigma.mk (β := fun (i : ι) ↦ α i) i x).fst (β := fun (i : ι) ↦ α i)))
    ((Sigma.mk (β := fun (i : ι) ↦ α i) i x).snd (β := fun (i : ι) ↦ α i))

Tactic:
simp
-- Module: Mathlib.Data.Finset.PiInduction
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
    r i x (g i) → p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
val : Fintype ι
f : (i : ι) → Finset (α i)
hne : (Finset.sigma (α := α) univ f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a)
ihs :
  ∀ t ⊂ Finset.sigma (α := α) univ (update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))),
    ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f
hr : r i x (g i)
hx' : x ∉ g i
⊢ Sigma.mk (β := fun (i : ι) ↦ α i) i x ∉ Finset.sigma (α := α) univ g

Tactic:
simp [hx']
-- Module: Mathlib.Data.Finset.PiInduction
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
    r i x (g i) → p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
val : Fintype ι
f : (i : ι) → Finset (α i)
hne : (Finset.sigma (α := α) univ f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a)
ihs :
  ∀ t ⊂ Finset.sigma (α := α) univ (update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))),
    ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f
hr : r i x (g i)
hx' : x ∉ g i
⊢ ∀ (i_1 : ι), g i_1 ⊆ update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i)) i_1

Tactic:
(@le_update_iff _ _ _ _ g g i _).2 ⟨subset_insert _ _, fun _ _ ↦ le_rfl⟩

Premises used: Iff.mpr, le_rfl, le_update_iff, And.intro, Finset.subset_insert
-- Module: Mathlib.Data.Finset.PiInduction
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
    r i x (g i) → p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
val : Fintype ι
f : (i : ι) → Finset (α i)
hne : (Finset.sigma (α := α) univ f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a)
ihs :
  ∀ t ⊂ Finset.sigma (α := α) univ (update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))),
    ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f
hr : r i x (g i)
hx' : x ∉ g i
⊢ ∃ x_1 ∈ Finset.sigma (α := α) univ (update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))),
    x_1 ∉ Finset.sigma (α := α) univ g

Tactic:
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⟩]

Premises used: Iff.mpr, le_rfl, le_update_iff, And.intro, Finset.subset_insert