awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.PiInduction (goal)
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))
⊢ f = update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))
have rw₃ : f = update (β := fun (a : ι) ↦ Finset (α a)) f i (f i)
Tactic: rw [hg, update_idem, update_self, insert_erase x_mem, update_eq_self]
-- Lean 4 proof step from Mathlib.Data.Finset.PiInduction (goal)
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)
⊢ f = update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))
have rw₄ : f = f
Tactic: rw [hg, update_idem, update_self, insert_erase x_mem, update_eq_self]
-- Lean 4 proof step from Mathlib.Data.Finset.PiInduction (goal)
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
⊢ f = update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))
have 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))
Tactic: rw [hg, update_idem, update_self, insert_erase x_mem, update_eq_self]
-- Lean 4 proof step from Mathlib.Data.Finset.PiInduction (goal)
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))
⊢ f = update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))
have rw₁ : f =
  update (β := fun (a : ι) ↦ Finset (α a)) f i
    (insert x (update (β := fun (a : ι) ↦ Finset (α a)) f i ((f i).erase x) i))
Tactic: rw [hg, update_idem, update_self, insert_erase x_mem, update_eq_self]
-- Lean 4 proof step from Mathlib.Data.Finset.PiInduction (goal)
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))
⊢ f = update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))
have rw₂ : f = update (β := fun (a : ι) ↦ Finset (α a)) f i (insert x ((f i).erase x))
Tactic: rw [hg, update_idem, update_self, insert_erase x_mem, update_eq_self]
-- Lean 4 proof step from Mathlib.Data.Finset.PiInduction (goal)
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))
⊢ f = update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))
have rw₃ : f = update (β := fun (a : ι) ↦ Finset (α a)) f i (f i)
Tactic: rw [hg, update_idem, update_self, insert_erase x_mem, update_eq_self]
-- Lean 4 proof step from Mathlib.Data.Finset.PiInduction (goal)
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)
⊢ f = update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))
have rw₄ : f = f
Tactic: rw [hg, update_idem, update_self, insert_erase x_mem, update_eq_self]
-- Lean 4 proof step from Mathlib.Data.Finset.PiInduction (goal)
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
⊢ f = update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))
have 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))
Tactic: rw [hg, update_idem, update_self, insert_erase x_mem, update_eq_self]
-- Lean 4 proof step from Mathlib.Data.Finset.PiInduction (goal)
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))
⊢ f = update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))
have rw₁ : f =
  update (β := fun (a : ι) ↦ Finset (α a)) f i
    (insert x (update (β := fun (a : ι) ↦ Finset (α a)) f i ((f i).erase x) i))
Tactic: rw [hg, update_idem, update_self, insert_erase x_mem, update_eq_self]
-- Lean 4 proof step from Mathlib.Data.Finset.PiInduction (goal)
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))
⊢ f = update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))
have rw₂ : f = update (β := fun (a : ι) ↦ Finset (α a)) f i (insert x ((f i).erase x))
Tactic: rw [hg, update_idem, update_self, insert_erase x_mem, update_eq_self]
-- Lean 4 proof step from Mathlib.Data.Finset.PiInduction (goal)
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))
⊢ f = update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))
have rw₃ : f = update (β := fun (a : ι) ↦ Finset (α a)) f i (f i)
Tactic: rw [hg, update_idem, update_self, insert_erase x_mem, update_eq_self]
-- Lean 4 proof step from Mathlib.Data.Finset.PiInduction (goal)
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)
⊢ f = update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))
have rw₄ : f = f
Tactic: rw [hg, update_idem, update_self, insert_erase x_mem, update_eq_self]
-- Lean 4 proof step from Mathlib.Data.Finset.PiInduction (goal)
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
⊢ p f
have 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)))
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 ⊢
Cleared hypotheses: ihs, hr, hg, hx'
-- Lean 4 proof step from Mathlib.Data.Finset.PiInduction (hypothesis)
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
⊢ p (update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i)))
have hr₁ : r i x (g i)
Tactic: rw [update_self, erase_insert hx'] at hr
Cleared hypotheses: hr, hx'
-- Lean 4 proof step from Mathlib.Data.Finset.PiInduction (goal)
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)))
have intro : Finset.sigma (α := α) univ g ⊂
  Finset.sigma (α := α) univ (update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i)))
Tactic: refine step _ _ _ hr (ihs (univ.sigma g) ?_ _ rfl)
-- Lean 4 proof step from Mathlib.Data.Finset.PiInduction (goal)
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
⊢ Finset.sigma (α := α) univ g ⊂
    Finset.sigma (α := α) univ (update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i)))
have intro : ∃ x_1 ∈ Finset.sigma (α := α) univ (update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))),
  x_1 ∉ Finset.sigma (α := α) univ g
Tactic: rw [ssubset_iff_of_subset (sigma_mono (Subset.refl _) _)]