awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.Pairwise (goal)
Goal:
α : Type u_1
inst : DecidableEq α
r : α → α → Prop
l : List α
hn : l.Nodup
hs : Symmetric r
this : Std.Symm r := ⋯
rw : Set.Pairwise {a : α | a ∈ l} r ↔ Pairwise r l
⊢ (↑l.toFinset : Set α).Pairwise r ↔ Pairwise r l
have rw₁ : Pairwise r l ↔ Pairwise r l
Tactic: rw [coe_toFinset, hn.pairwise_coe]
-- Lean 4 proof step from Mathlib.Data.Finset.Pi (goal)
Goal:
α : Type u_1
δ : α → Sort v
inst : DecidableEq α
a : α
b : δ a
s : Finset α
hs : a ∉ s
e₁ e₂ : (a : α) → a ∈ s → δ a
eq : Eq (α := (a' : α) → (h : a' ∈ insert a s) → δ a') (cons (δ := δ) s a b e₁) (cons (δ := δ) s a b e₂)
e : α
h : e ∈ a ::ₘ s.val
⊢ cons (δ := δ) s a b e₁ e ⋯ = cons (δ := δ) s a b e₂ e ⋯
have rw : cons (δ := δ) s a b e₂ e sorry = cons (δ := δ) s a b e₂ e sorry
Tactic: rw [eq]
-- Lean 4 proof step from Mathlib.Data.Finset.Pi (goal)
Goal:
α : Type u_1
β : α → Type u
s : Finset α
t : (a : α) → Finset (β a)
inst : DecidableEq α
⊢ s.pi (β := β) t = ∅ ↔ ∃ a ∈ s, t a = ∅
have contrapose! : (s.pi (β := β) t).Nonempty ↔ ∀ (a : α) (_ : a ∈ s), (t a).Nonempty
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Data.Finset.Pi (goal)
Goal:
α : Type u_1
β : α → Type u
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ (insert a s).pi (β := β) t = (t a).biUnion fun (b : β a) ↦ image (Pi.cons (δ := β) s a b) (s.pi (β := β) t)
have a₁ : ((insert a s).pi (β := β) t).val = val ((t a).biUnion fun (b : β a) ↦ image (Pi.cons (δ := β) s a b) (s.pi (β := β) t))
Tactic: apply eq_of_veq
-- Lean 4 proof step from Mathlib.Data.Finset.Pi (goal)
Goal:
α : Type u_1
β : α → Type u
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ ((insert a s).pi (β := β) t).val =
    val ((t a).biUnion fun (b : β a) ↦ image (Pi.cons (δ := β) s a b) (s.pi (β := β) t))
have a₁ : ((insert a s).pi (β := β) t).val.dedup =
  val ((t a).biUnion fun (b : β a) ↦ image (Pi.cons (δ := β) s a b) (s.pi (β := β) t))
Tactic: rw [← (pi (insert a s) t).2.dedup]
-- Lean 4 proof step from Mathlib.Data.Finset.Pi (goal)
Goal:
α : Type u_1
β : α → Type u
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ ((insert a s).pi (β := β) t).val.dedup =
    val ((t a).biUnion fun (b : β a) ↦ image (Pi.cons (δ := β) s a b) (s.pi (β := β) t))
have a₁ : ∀ (s' : Multiset α) (h : s' = a ::ₘ s.val),
  Eq (α := Multiset ((a : α) → a ∈ s' → β a)) (dedup (s'.pi (β := β) fun (a : α) ↦ (t a).val))
    (dedup
      ((t a).val.bind fun (b : β a) ↦
        dedup
          (Multiset.map
            (fun (f : (a : α) → a ∈ s.val → β a) (a' : α) (h' : a' ∈ s') ↦ Multiset.Pi.cons (δ := β) s.val a b f a' sorry)
            (s.val.pi (β := β) fun (a : α) ↦ (t a).val))))
Tactic: refine
    (fun s' (h : s' = a ::ₘ s.1) =>
        (?_ :
          dedup (Multiset.pi s' fun a => (t a).1) =
            dedup
              ((t a).1.bind fun b =>
                dedup <|
                  (Multiset.pi s.1 fun a : α => (t a).val).map fun f a' h' =>
                    Multiset.Pi.cons s.1 a b f a' (h ▸ h'))))
      _ (insert_val_of_notMem ha)
-- Lean 4 proof step from Mathlib.Data.Finset.Pi (goal)
Goal:
α : Type u_1
β : α → Type u
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
s' : Multiset α
h : s' = a ::ₘ s.val
⊢ Eq (α := Multiset ((a : α) → a ∈ s' → β a)) (dedup (s'.pi (β := β) fun (a : α) ↦ (t a).val))
    (dedup
      ((t a).val.bind fun (b : β a) ↦
        dedup
          (Multiset.map
            (fun (f : (a : α) → a ∈ s.val → β a) (a' : α) (h' : a' ∈ s') ↦ Multiset.Pi.cons (δ := β) s.val a b f a' ⋯)
            (s.val.pi (β := β) fun (a : α) ↦ (t a).val))))
have a₁ : Eq (α := Multiset ((a_1 : α) → a_1 ∈ a ::ₘ s.val → β a_1)) (dedup ((a ::ₘ s.val).pi (β := β) fun (a : α) ↦ (t a).val))
  (dedup
    ((t a).val.bind fun (b : β a) ↦
      dedup
        (Multiset.map
          (fun (f : (a : α) → a ∈ s.val → β a) (a' : α) (h' : a' ∈ a ::ₘ s.val) ↦
            Multiset.Pi.cons (δ := β) s.val a b f a' sorry)
          (s.val.pi (β := β) fun (a : α) ↦ (t a).val))))
Tactic: subst s'
Cleared hypotheses: s', h
-- Lean 4 proof step from Mathlib.Data.Finset.Pi (goal)
Goal:
α : Type u_1
β : α → Type u
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ Eq (α := Multiset ((a_1 : α) → a_1 ∈ a ::ₘ s.val → β a_1)) (dedup ((a ::ₘ s.val).pi (β := β) fun (a : α) ↦ (t a).val))
    (dedup
      ((t a).val.bind fun (b : β a) ↦
        dedup
          (Multiset.map
            (fun (f : (a : α) → a ∈ s.val → β a) (a' : α) (h' : a' ∈ a ::ₘ s.val) ↦
              Multiset.Pi.cons (δ := β) s.val a b f a' ⋯)
            (s.val.pi (β := β) fun (a : α) ↦ (t a).val))))
have a₁ : Eq (α := Multiset ((a_1 : α) → a_1 ∈ a ::ₘ s.val → β a_1))
  (dedup
    ((t a).val.bind fun (b : β a) ↦
      Multiset.map (Multiset.Pi.cons (δ := β) s.val a b) (s.val.pi (β := β) fun (a : α) ↦ (t a).val)))
  (dedup
    ((t a).val.bind fun (b : β a) ↦
      dedup
        (Multiset.map
          (fun (f : (a : α) → a ∈ s.val → β a) (a' : α) (h' : a' ∈ a ::ₘ s.val) ↦
            Multiset.Pi.cons (δ := β) s.val a b f a' sorry)
          (s.val.pi (β := β) fun (a : α) ↦ (t a).val))))
Tactic: rw [pi_cons]
-- Lean 4 proof step from Mathlib.Data.Finset.Pi (goal)
Goal:
α : Type u_1
β : α → Type u
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ Eq (α := Multiset ((a_1 : α) → a_1 ∈ a ::ₘ s.val → β a_1))
    (dedup
      ((t a).val.bind fun (b : β a) ↦
        Multiset.map (Multiset.Pi.cons (δ := β) s.val a b) (s.val.pi (β := β) fun (a : α) ↦ (t a).val)))
    (dedup
      ((t a).val.bind fun (b : β a) ↦
        dedup
          (Multiset.map
            (fun (f : (a : α) → a ∈ s.val → β a) (a' : α) (h' : a' ∈ a ::ₘ s.val) ↦
              Multiset.Pi.cons (δ := β) s.val a b f a' ⋯)
            (s.val.pi (β := β) fun (a : α) ↦ (t a).val))))
have a₁ : Eq (α := β a → Multiset ((a' : α) → a' ∈ a ::ₘ s.val → β a'))
  (fun (b : β a) ↦ Multiset.map (Multiset.Pi.cons (δ := β) s.val a b) (s.val.pi (β := β) fun (a : α) ↦ (t a).val))
  fun (b : β a) ↦
  dedup
    (Multiset.map
      (fun (f : (a : α) → a ∈ s.val → β a) (a' : α) (h' : a' ∈ a ::ₘ s.val) ↦
        Multiset.Pi.cons (δ := β) s.val a b f a' sorry)
      (s.val.pi (β := β) fun (a : α) ↦ (t a).val))
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Finset.Pi (goal)
Goal:
α : Type u_1
β : α → Type u
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ Eq (α := β a → Multiset ((a' : α) → a' ∈ a ::ₘ s.val → β a'))
    (fun (b : β a) ↦ Multiset.map (Multiset.Pi.cons (δ := β) s.val a b) (s.val.pi (β := β) fun (a : α) ↦ (t a).val))
    fun (b : β a) ↦
    dedup
      (Multiset.map
        (fun (f : (a : α) → a ∈ s.val → β a) (a' : α) (h' : a' ∈ a ::ₘ s.val) ↦
          Multiset.Pi.cons (δ := β) s.val a b f a' ⋯)
        (s.val.pi (β := β) fun (a : α) ↦ (t a).val))
have a₁ : ∀ (b : β a),
  Multiset.map (Multiset.Pi.cons (δ := β) s.val a b) (s.val.pi (β := β) fun (a : α) ↦ (t a).val) =
    dedup
      (Multiset.map
        (fun (f : (a : α) → a ∈ s.val → β a) (a' : α) (h' : a' ∈ a ::ₘ s.val) ↦
          Multiset.Pi.cons (δ := β) s.val a b f a' sorry)
        (s.val.pi (β := β) fun (a : α) ↦ (t a).val))
Tactic: funext b
-- Lean 4 proof step from Mathlib.Data.Finset.Pi (goal)
Goal:
α : Type u_1
s : Finset α
ι : Type u_3
inst : DecidableEq (ι → α)
inst_1 : Nonempty ι
⊢ #(s.piDiag ι) = #s
have rw : #(image (const ι) s) = #s
Tactic: rw [piDiag, card_image_of_injective _ const_injective]
-- Lean 4 proof step from Mathlib.Data.Finset.Pi (goal)
Goal:
α : Type u_1
s : Finset α
ι : Type u_3
inst : DecidableEq (ι → α)
inst_1 : Nonempty ι
rw : #(image (const ι) s) = #s
⊢ #(s.piDiag ι) = #s
have rw₁ : #s = #s
Tactic: rw [piDiag, card_image_of_injective _ const_injective]
-- Lean 4 proof step from Mathlib.Data.Finset.Pi (goal)
Goal:
ι : Type u_2
π : ι → Type u_3
s : Finset ι
inst : DecidablePred fun (x : ι) ↦ x ∈ s
t : (i : ↥s) → Set (π (↑i : ι))
⊢ s.restrict (π := π) ⁻¹' Set.pi (α := fun (i : ↥s) ↦ π (↑i : ι)) Set.univ t =
    (↑s : Set ι).pi (α := π) fun (i : ι) ↦ if h : i ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else Set.univ
have h : ∀ (x : (i : ι) → π i),
  x ∈ s.restrict (π := π) ⁻¹' Set.pi (α := fun (i : ↥s) ↦ π (↑i : ι)) Set.univ t ↔
    Membership.mem (γ := Set ((i : ι) → π i))
      ((↑s : Set ι).pi (α := π) fun (i : ι) ↦
        if h : i ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else Set.univ)
      x
Tactic: ext
-- 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
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 (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
⊢ p f
have intro : ∀ (val : Fintype ι), p f
Tactic: cases nonempty_fintype ι
-- 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
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 (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
val : Fintype ι
⊢ p f
have intro : ∀ (s : Finset ((i : ι) × α i))
  (ihs : ∀ t ⊂ s, ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f)
  (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = s), p f
Tactic: induction hs : univ.sigma f using Finset.strongInductionOn generalizing f with | _ s ihs
Cleared hypotheses: f
-- 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 ι
s : Finset ((i : ι) × α i)
ihs : ∀ t ⊂ s, ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f
f : (i : ι) → Finset (α i)
hs : Finset.sigma (α := α) univ f = s
⊢ p f
have ihs₁ : ∀ t ⊂ Finset.sigma (α := α) univ f, ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f
Tactic: subst s
Cleared hypotheses: s, ihs, hs
-- 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
⊢ p f
have intro : ∀ (he : Finset.sigma (α := α) univ f = ∅), p f
Tactic: rcases eq_empty_or_nonempty (univ.sigma f) with he | hne
-- 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
intro : ∀ (he : Finset.sigma (α := α) univ f = ∅), p f
⊢ p f
have intro₁ : ∀ (hne : (Finset.sigma (α := α) univ f).Nonempty), p f
Tactic: rcases eq_empty_or_nonempty (univ.sigma f) with he | hne
-- 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
he : Finset.sigma (α := α) univ f = ∅
⊢ p f
have h : f = fun (x : ι) ↦ ∅
Tactic: convert! h0 using 1
-- 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
⊢ p f
have intro : ∀ (i : ι) (hi : (f i).Nonempty), p f
Tactic: rcases sigma_nonempty.1 hne with ⟨i, -, hi⟩
-- 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
⊢ p f
have intro : ∀ (x : α i) (x_mem : x ∈ f i) (hr : r i x ((f i).erase x)), p f
Tactic: rcases H_ex i (f i) hi with ⟨x, x_mem, hr⟩
-- 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)
⊢ p f
have 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
Tactic: set g := update f i ((f i).erase x) with hg
-- 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) := 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
have intro : ∀ (g : (a : ι) → Finset (α a)) (hg : g = update (β := fun (a : ι) ↦ Finset (α a)) f i ((f i).erase x)), p f
Tactic: clear_value g
Cleared hypotheses: g, hg
-- 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)
⊢ x ∉ g i
have rw : x ∉ (f i).erase x
Tactic: rw [hg, update_self]
-- 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)
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)
⊢ p f
have hx' : x ∉ g i
Tactic: have hx' : x ∉ g i := by
      rw [hg, update_self]
      apply notMem_erase
-- 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
⊢ 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
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))
⊢ 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
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))
⊢ 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]