awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)) (h𝒜 : #𝒜_1 < #𝒜 + 1) (h𝒜₁ : 𝒜_1.Nonempty) (h𝒜₂ : univ ∉ 𝒜_1),
    supSum 𝒜_1 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ supSum (insert s 𝒜) = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
have ind : Finset.card (α := Finset α) (image (fun (x : Finset α) ↦ s ⊓ x) 𝒜) < #𝒜 + 1
Tactic: rw [insert_eq, eq_sub_of_add_eq (supSum_union_add_supSum_infs _ _), singleton_infs,
    supSum_singleton (ne_of_mem_of_not_mem (mem_insert_self _ _) h𝒜₂), ih, ih, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)) (h𝒜 : #𝒜_1 < #𝒜 + 1) (h𝒜₁ : 𝒜_1.Nonempty) (h𝒜₂ : univ ∉ 𝒜_1),
    supSum 𝒜_1 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
ind : Finset.card (α := Finset α) (image (fun (x : Finset α) ↦ s ⊓ x) 𝒜) < #𝒜 + 1
⊢ supSum (insert s 𝒜) = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
have ind₁ : Finset.Nonempty (α := Finset α) (image (fun (x : Finset α) ↦ s ⊓ x) 𝒜)
Tactic: rw [insert_eq, eq_sub_of_add_eq (supSum_union_add_supSum_infs _ _), singleton_infs,
    supSum_singleton (ne_of_mem_of_not_mem (mem_insert_self _ _) h𝒜₂), ih, ih, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)) (h𝒜 : #𝒜_1 < #𝒜 + 1) (h𝒜₁ : 𝒜_1.Nonempty) (h𝒜₂ : univ ∉ 𝒜_1),
    supSum 𝒜_1 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
ind : Finset.card (α := Finset α) (image (fun (x : Finset α) ↦ s ⊓ x) 𝒜) < #𝒜 + 1
ind₁ : Finset.Nonempty (α := Finset α) (image (fun (x : Finset α) ↦ s ⊓ x) 𝒜)
⊢ supSum (insert s 𝒜) = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
have ind₂ : univ ∉ image (fun (x : Finset α) ↦ s ⊓ x) 𝒜
Tactic: rw [insert_eq, eq_sub_of_add_eq (supSum_union_add_supSum_infs _ _), singleton_infs,
    supSum_singleton (ne_of_mem_of_not_mem (mem_insert_self _ _) h𝒜₂), ih, ih, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)) (h𝒜 : #𝒜_1 < #𝒜 + 1) (h𝒜₁ : 𝒜_1.Nonempty) (h𝒜₂ : univ ∉ 𝒜_1),
    supSum 𝒜_1 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
ind : Finset.card (α := Finset α) (image (fun (x : Finset α) ↦ s ⊓ x) 𝒜) < #𝒜 + 1
ind₁ : Finset.Nonempty (α := Finset α) (image (fun (x : Finset α) ↦ s ⊓ x) 𝒜)
ind₂ : univ ∉ image (fun (x : Finset α) ↦ s ⊓ x) 𝒜
⊢ supSum (insert s 𝒜) = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
have ind₃ : #𝒜 < #𝒜 + 1
Tactic: rw [insert_eq, eq_sub_of_add_eq (supSum_union_add_supSum_infs _ _), singleton_infs,
    supSum_singleton (ne_of_mem_of_not_mem (mem_insert_self _ _) h𝒜₂), ih, ih, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)) (h𝒜 : #𝒜_1 < #𝒜 + 1) (h𝒜₁ : 𝒜_1.Nonempty) (h𝒜₂ : univ ∉ 𝒜_1),
    supSum 𝒜_1 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
ind : Finset.card (α := Finset α) (image (fun (x : Finset α) ↦ s ⊓ x) 𝒜) < #𝒜 + 1
ind₁ : Finset.Nonempty (α := Finset α) (image (fun (x : Finset α) ↦ s ⊓ x) 𝒜)
ind₂ : univ ∉ image (fun (x : Finset α) ↦ s ⊓ x) 𝒜
ind₃ : #𝒜 < #𝒜 + 1
ind₄ : 𝒜.Nonempty
⊢ supSum (insert s 𝒜) = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
have ind₅ : univ ∉ 𝒜
Tactic: rw [insert_eq, eq_sub_of_add_eq (supSum_union_add_supSum_infs _ _), singleton_infs,
    supSum_singleton (ne_of_mem_of_not_mem (mem_insert_self _ _) h𝒜₂), ih, ih, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
𝒜 : Finset (Finset α)
inst_2 : Nonempty α
h𝒜₁ : 𝒜.Nonempty
h𝒜₀ : ∅ ∉ 𝒜
⊢ infSum 𝒜 = 1
have rw : univ ∉ 𝒜ᶜˢ
Tactic: rw [← compls_compls 𝒜, eq_sub_of_add_eq (infSum_compls_add_supSum _),
    supSum_of_univ_notMem h𝒜₁.compls, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ memberSubfamily a 𝒜 ↔ insert a s ∈ 𝒜 ∧ a ∉ s
have simp_rw : (∃ (a_1 : Finset α), (a_1 ∈ 𝒜 ∧ a ∈ a_1) ∧ a_1.erase a = s) ↔ insert a s ∈ 𝒜 ∧ a ∉ s
Tactic: simp_rw [memberSubfamily, mem_image, mem_filter]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ (∃ (a_1 : Finset α), (a_1 ∈ 𝒜 ∧ a ∈ a_1) ∧ a_1.erase a = s) ↔ insert a s ∈ 𝒜 ∧ a ∉ s
have refine : (∃ (a_1 : Finset α), (a_1 ∈ 𝒜 ∧ a ∈ a_1) ∧ a_1.erase a = s) → insert a s ∈ 𝒜 ∧ a ∉ s
Tactic: refine ⟨?_, fun h => ⟨insert a s, ⟨h.1, by simp⟩, erase_insert h.2⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
hs1 : s ∈ 𝒜
hs2 : a ∈ s
⊢ insert a (s.erase a) ∈ 𝒜 ∧ a ∉ s.erase a
have rw : s ∈ 𝒜 ∧ a ∉ s.erase a
Tactic: rw [insert_erase hs2]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 ℬ : Finset (Finset α)
⊢ Eq (α := Finset (Finset α)) (image (fun (s : Finset α) ↦ s.erase a) ({s ∈ 𝒜 ∩ ℬ | a ∈ s}))
    (image (fun (s : Finset α) ↦ s.erase a) ({s ∈ 𝒜 | a ∈ s}) ∩
      image (fun (s : Finset α) ↦ s.erase a) ({s ∈ ℬ | a ∈ s}))
have rw : (↑({s ∈ 𝒜 | a ∈ s}) : Set (Finset α)) ∪ (↑({s ∈ ℬ | a ∈ s}) : Set (Finset α)) ⊆ {s : Finset α | a ∈ s}
Tactic: rw [filter_inter_distrib, image_inter_of_injOn _ _ ((erase_injOn' _).mono _)]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 ℬ : Finset (Finset α)
⊢ memberSubfamily a (𝒜 ∪ ℬ) = memberSubfamily a 𝒜 ∪ memberSubfamily a ℬ
have simp_rw : Eq (α := Finset (Finset α)) (image (fun (s : Finset α) ↦ s.erase a) ({s ∈ 𝒜 ∪ ℬ | a ∈ s}))
  (image (fun (s : Finset α) ↦ s.erase a) ({s ∈ 𝒜 | a ∈ s}) ∪ image (fun (s : Finset α) ↦ s.erase a) ({s ∈ ℬ | a ∈ s}))
Tactic: simp_rw [memberSubfamily, filter_union, image_union]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 ℬ : Finset (Finset α)
simp_rw :
  Eq (α := Finset (Finset α)) (image (fun (s : Finset α) ↦ s.erase a) ({s ∈ 𝒜 ∪ ℬ | a ∈ s}))
    (image (fun (s : Finset α) ↦ s.erase a) ({s ∈ 𝒜 | a ∈ s}) ∪
      image (fun (s : Finset α) ↦ s.erase a) ({s ∈ ℬ | a ∈ s}))
⊢ memberSubfamily a (𝒜 ∪ ℬ) = memberSubfamily a 𝒜 ∪ memberSubfamily a ℬ
have simp_rw₁ : Eq (α := Finset (Finset α)) (image (fun (s : Finset α) ↦ s.erase a) ({s ∈ 𝒜 | a ∈ s} ∪ {s ∈ ℬ | a ∈ s}))
  (image (fun (s : Finset α) ↦ s.erase a) ({s ∈ 𝒜 | a ∈ s}) ∪ image (fun (s : Finset α) ↦ s.erase a) ({s ∈ ℬ | a ∈ s}))
Tactic: simp_rw [memberSubfamily, filter_union, image_union]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ #(memberSubfamily a 𝒜) + #(nonMemberSubfamily a 𝒜) = #𝒜
have rw : #({s ∈ 𝒜 | a ∈ s}) + #({s ∈ 𝒜 | a ∉ s}) = #𝒜
Tactic: rw [memberSubfamily, nonMemberSubfamily, card_image_of_injOn]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
rw : #({s ∈ 𝒜 | a ∈ s}) + #({s ∈ 𝒜 | a ∉ s}) = #𝒜
⊢ #(memberSubfamily a 𝒜) + #(nonMemberSubfamily a 𝒜) = #𝒜
have rw₁ : Set.InjOn (β := Finset α) (fun (s : Finset α) ↦ s.erase a) (↑({s ∈ 𝒜 | a ∈ s}) : Set (Finset α))
Tactic: rw [memberSubfamily, nonMemberSubfamily, card_image_of_injOn]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
| #𝒜
have rw : #({s ∈ 𝒜 | a ∈ s}) + #({a_1 ∈ 𝒜 | a ∉ a_1})
Tactic: rw [← card_filter_add_card_filter_not (fun s => (a ∈ s))]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ #({s ∈ 𝒜 | a ∈ s}) + #({s ∈ 𝒜 | a ∉ s}) = #𝒜
have conv_rhs : #({s ∈ 𝒜 | a ∈ s}) + #({s ∈ 𝒜 | a ∉ s}) = #𝒜
Tactic: conv_rhs => rw [← card_filter_add_card_filter_not (fun s => (a ∈ s))]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
conv_rhs : #({s ∈ 𝒜 | a ∈ s}) + #({s ∈ 𝒜 | a ∉ s}) = #𝒜
⊢ #({s ∈ 𝒜 | a ∈ s}) + #({s ∈ 𝒜 | a ∉ s}) = #𝒜
have conv_rhs₁ : #({s ∈ 𝒜 | a ∈ s}) + #({s ∈ 𝒜 | a ∉ s}) = #({s ∈ 𝒜 | a ∈ s}) + #({a_1 ∈ 𝒜 | a ∉ a_1})
Tactic: conv_rhs => rw [← card_filter_add_card_filter_not (fun s => (a ∈ s))]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ Set.InjOn (β := Finset α) (fun (s : Finset α) ↦ s.erase a) (↑({s ∈ 𝒜 | a ∈ s}) : Set (Finset α))
have apply : (↑({s ∈ 𝒜 | a ∈ s}) : Set (Finset α)) ⊆ {s : Finset α | a ∈ s}
Tactic: apply (erase_injOn' _).mono
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ memberSubfamily a 𝒜 ∪ nonMemberSubfamily a 𝒜 = image (fun (s : Finset α) ↦ s.erase a) 𝒜
have h : ∀ (s : Finset α),
  s ∈ memberSubfamily a 𝒜 ∪ nonMemberSubfamily a 𝒜 ↔
    Membership.mem (γ := Finset (Finset α)) (image (fun (s : Finset α) ↦ s.erase a) 𝒜) s
Tactic: ext s
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ memberSubfamily a 𝒜 ∪ nonMemberSubfamily a 𝒜 ↔
    Membership.mem (γ := Finset (Finset α)) (image (fun (s : Finset α) ↦ s.erase a) 𝒜) s
have h : insert a s ∈ 𝒜 ∧ a ∉ s ∨ s ∈ 𝒜 ∧ a ∉ s ↔ ∃ a_1 ∈ 𝒜, a_1.erase a = s
Tactic: simp only [mem_union, mem_memberSubfamily, mem_nonMemberSubfamily, mem_image]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
⊢ insert a s ∈ 𝒜 ∧ a ∉ s ∨ s ∈ 𝒜 ∧ a ∉ s ↔ ∃ a_1 ∈ 𝒜, a_1.erase a = s
have h : insert a s ∈ 𝒜 ∧ a ∉ s ∨ s ∈ 𝒜 ∧ a ∉ s → ∃ a_2 ∈ 𝒜, a_2.erase a = s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
h : insert a s ∈ 𝒜 ∧ a ∉ s ∨ s ∈ 𝒜 ∧ a ∉ s → ∃ a_2 ∈ 𝒜, a_2.erase a = s
⊢ insert a s ∈ 𝒜 ∧ a ∉ s ∨ s ∈ 𝒜 ∧ a ∉ s ↔ ∃ a_1 ∈ 𝒜, a_1.erase a = s
have h₁ : (∃ a_1 ∈ 𝒜, a_1.erase a = s) → insert a s ∈ 𝒜 ∧ a ∉ s ∨ s ∈ 𝒜 ∧ a ∉ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜
⊢ insert a (s.erase a) ∈ 𝒜 ∧ a ∉ s.erase a ∨ s.erase a ∈ 𝒜 ∧ a ∉ s.erase a
have pos : ∀ (ha : a ∈ s), insert a (s.erase a) ∈ 𝒜 ∧ a ∉ s.erase a ∨ s.erase a ∈ 𝒜 ∧ a ∉ s.erase a
Tactic: by_cases ha : a ∈ s
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜
pos : ∀ (ha : a ∈ s), insert a (s.erase a) ∈ 𝒜 ∧ a ∉ s.erase a ∨ s.erase a ∈ 𝒜 ∧ a ∉ s.erase a
⊢ insert a (s.erase a) ∈ 𝒜 ∧ a ∉ s.erase a ∨ s.erase a ∈ 𝒜 ∧ a ∉ s.erase a
have neg : ∀ (ha : a ∉ s), insert a (s.erase a) ∈ 𝒜 ∧ a ∉ s.erase a ∨ s.erase a ∈ 𝒜 ∧ a ∉ s.erase a
Tactic: by_cases ha : a ∈ s
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
⊢ memberSubfamily a (memberSubfamily a 𝒜) = ∅
have h : ∀ (a_1 : Finset α), a_1 ∈ memberSubfamily a (memberSubfamily a 𝒜) ↔ Membership.mem (γ := Finset (Finset α)) ∅ a_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
⊢ memberSubfamily a (nonMemberSubfamily a 𝒜) = ∅
have h : ∀ (a_1 : Finset α), a_1 ∈ memberSubfamily a (nonMemberSubfamily a 𝒜) ↔ Membership.mem (γ := Finset (Finset α)) ∅ a_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
⊢ nonMemberSubfamily a (memberSubfamily a 𝒜) = memberSubfamily a 𝒜
have h : ∀ (a_1 : Finset α), a_1 ∈ nonMemberSubfamily a (memberSubfamily a 𝒜) ↔ a_1 ∈ memberSubfamily a 𝒜
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
⊢ nonMemberSubfamily a (nonMemberSubfamily a 𝒜) = nonMemberSubfamily a 𝒜
have h : ∀ (a_1 : Finset α), a_1 ∈ nonMemberSubfamily a (nonMemberSubfamily a 𝒜) ↔ a_1 ∈ nonMemberSubfamily a 𝒜
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h𝒜 : ∀ s ∈ 𝒜, a ∉ s
⊢ memberSubfamily a (image (insert a) 𝒜) = 𝒜
have h : ∀ (s : Finset α), s ∈ memberSubfamily a (image (insert a) 𝒜) ↔ s ∈ 𝒜
Tactic: ext s
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h𝒜 : ∀ s ∈ 𝒜, a ∉ s
s : Finset α
⊢ s ∈ memberSubfamily a (image (insert a) 𝒜) ↔ s ∈ 𝒜
have h : (∃ a_1 ∈ 𝒜, insert a a_1 = insert a s) ∧ a ∉ s ↔ s ∈ 𝒜
Tactic: simp only [mem_memberSubfamily, mem_image]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h𝒜 : ∀ s ∈ 𝒜, a ∉ s
s : Finset α
⊢ (∃ a_1 ∈ 𝒜, insert a a_1 = insert a s) ∧ a ∉ s ↔ s ∈ 𝒜
have h : (∃ a_1 ∈ 𝒜, insert a a_1 = insert a s) ∧ a ∉ s → s ∈ 𝒜
Tactic: refine ⟨?_, fun hs ↦ ⟨⟨s, hs, rfl⟩, h𝒜 _ hs⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
⊢ image (insert a) (memberSubfamily a 𝒜) = {s ∈ 𝒜 | a ∈ s}
have h : ∀ (s : Finset α), s ∈ image (insert a) (memberSubfamily a 𝒜) ↔ s ∈ {s ∈ 𝒜 | a ∈ s}
Tactic: ext s
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
⊢ s ∈ image (insert a) (memberSubfamily a 𝒜) ↔ s ∈ {s ∈ 𝒜 | a ∈ s}
have h : (∃ (a_1 : Finset α), (insert a a_1 ∈ 𝒜 ∧ a ∉ a_1) ∧ insert a a_1 = s) ↔ s ∈ 𝒜 ∧ a ∈ s
Tactic: simp only [mem_memberSubfamily, mem_image, mem_filter]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
⊢ (∃ (a_1 : Finset α), (insert a a_1 ∈ 𝒜 ∧ a ∉ a_1) ∧ insert a a_1 = s) ↔ s ∈ 𝒜 ∧ a ∈ s
have h : (∃ (a_1 : Finset α), (insert a a_1 ∈ 𝒜 ∧ a ∉ a_1) ∧ insert a a_1 = s) → s ∈ 𝒜 ∧ a ∈ s
Tactic: refine ⟨?_, fun ⟨hs, ha⟩ ↦ ⟨erase s a, ⟨?_, notMem_erase _ _⟩, insert_erase ha⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
h : (∃ (a_1 : Finset α), (insert a a_1 ∈ 𝒜 ∧ a ∉ a_1) ∧ insert a a_1 = s) → s ∈ 𝒜 ∧ a ∈ s
⊢ (∃ (a_1 : Finset α), (insert a a_1 ∈ 𝒜 ∧ a ∉ a_1) ∧ insert a a_1 = s) ↔ s ∈ 𝒜 ∧ a ∈ s
have h₁ : s ∈ 𝒜 ∧ a ∈ s → ∀ (hs : s ∈ 𝒜) (ha : a ∈ s), insert a (s.erase a) ∈ 𝒜
Tactic: refine ⟨?_, fun ⟨hs, ha⟩ ↦ ⟨erase s a, ⟨?_, notMem_erase _ _⟩, insert_erase ha⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
𝒜 : Finset (Finset α)
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
u : Finset α := 𝒜.sup id
⊢ p 𝒜
have have : ∀ (hu : ∀ s ∈ 𝒜, s ⊆ u), p 𝒜
Tactic: have hu : ∀ s ∈ 𝒜, s ⊆ u := fun s ↦ le_sup (f := id)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
𝒜 : Finset (Finset α)
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
u : Finset α := 𝒜.sup id
hu : ∀ s ∈ 𝒜, s ⊆ u
⊢ p 𝒜
have clear_value : ∀ (u : Finset α) (hu : ∀ s ∈ 𝒜, s ⊆ u), p 𝒜
Tactic: clear_value u
Cleared hypotheses: u, hu
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ ∅
⊢ p 𝒜
have hu₁ : ∀ s ∈ 𝒜, s = ∅
Tactic: simp_rw [subset_empty] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s = ∅
⊢ p 𝒜
have hu₁ : 𝒜 = ∅ ∨ 𝒜 = {∅}
Tactic: rw [← subset_singleton_iff', subset_singleton_iff] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
a : α
u : Finset α
h : a ∉ u
ih : ∀ (𝒜 : Finset (Finset α)) (hu : ∀ s ∈ 𝒜, s ⊆ u), p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ insert a u
⊢ p 𝒜
have insert : ∀ s ∈ nonMemberSubfamily a 𝒜, s ⊆ u
Tactic: refine subfamily a (ih _ ?_) (ih _ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
a : α
u : Finset α
h : a ∉ u
ih : ∀ (𝒜 : Finset (Finset α)) (hu : ∀ s ∈ 𝒜, s ⊆ u), p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ Insert.insert a u
insert : ∀ s ∈ nonMemberSubfamily a 𝒜, s ⊆ u
⊢ p 𝒜
have insert₁ : ∀ s ∈ memberSubfamily a 𝒜, s ⊆ u
Tactic: refine subfamily a (ih _ ?_) (ih _ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
a : α
u : Finset α
h : a ∉ u
ih : ∀ (𝒜 : Finset (Finset α)) (hu : ∀ s ∈ 𝒜, s ⊆ u), p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ insert a u
⊢ ∀ s ∈ nonMemberSubfamily a 𝒜, s ⊆ u
have insert : ∀ s ∈ 𝒜, a ∉ s → s ⊆ u
Tactic: simp only [mem_nonMemberSubfamily, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
a : α
u : Finset α
h : a ∉ u
ih : ∀ (𝒜 : Finset (Finset α)) (hu : ∀ s ∈ 𝒜, s ⊆ u), p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ insert a u
⊢ ∀ s ∈ memberSubfamily a 𝒜, s ⊆ u
have insert : ∀ (s : Finset α), insert a s ∈ 𝒜 → a ∉ s → s ⊆ u
Tactic: simp only [mem_memberSubfamily, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
𝒜 : Finset (Finset α)
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
u : Finset α
hu : ∀ s ∈ 𝒜, s ⊆ u
⊢ p 𝒜
have empty₁ : ∀ (𝒜 : Finset (Finset α)) (hu : ∀ s ∈ 𝒜, s ⊆ ∅), p 𝒜
Tactic: induction u using Finset.induction generalizing 𝒜 with
  | empty =>
    simp_rw [subset_empty] at hu
    rw [← subset_singleton_iff', subset_singleton_iff] at hu
    obtain rfl | rfl := hu <;> assumption
  | insert a u _ ih =>
    refine subfamily a (ih _ ?_) (ih _ ?_)
    · simp only [mem_nonMemberSubfamily, and_imp]
      exact fun s hs has ↦ (subset_insert_iff_of_notMem has).1 <| hu _ hs
    · simp only [mem_memberSubfamily, and_imp]
      exact fun s hs ha ↦ (insert_subset_insert_iff ha).1 <| hu _ hs
Cleared hypotheses: 𝒜, u, hu
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
𝒜 : Finset (Finset α)
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
u : Finset α
hu : ∀ s ∈ 𝒜, s ⊆ u
empty₁ : ∀ (𝒜 : Finset (Finset α)) (hu : ∀ s ∈ 𝒜, s ⊆ ∅), p 𝒜
⊢ p 𝒜
have insert : ∀ (a : α) (u : Finset α),
  a ∉ u →
    ∀ (ih : ∀ (𝒜 : Finset (Finset α)) (hu : ∀ s ∈ 𝒜, s ⊆ u), p 𝒜) (𝒜 : Finset (Finset α))
      (hu : ∀ s ∈ 𝒜, s ⊆ insert a u), p 𝒜
Tactic: induction u using Finset.induction generalizing 𝒜 with
  | empty =>
    simp_rw [subset_empty] at hu
    rw [← subset_singleton_iff', subset_singleton_iff] at hu
    obtain rfl | rfl := hu <;> assumption
  | insert a u _ ih =>
    refine subfamily a (ih _ ?_) (ih _ ?_)
    · simp only [mem_nonMemberSubfamily, and_imp]
      exact fun s hs has ↦ (subset_insert_iff_of_notMem has).1 <| hu _ hs
    · simp only [mem_memberSubfamily, and_imp]
      exact fun s hs ha ↦ (insert_subset_insert_iff ha).1 <| hu _ hs
Cleared hypotheses: 𝒜, u, hu
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
𝒜 : Finset (Finset α)
empty : p ∅
singleton_empty : p {∅}
image_insert : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, (∀ s ∈ 𝒜, a ∉ s) → p 𝒜 → p (image (insert a) 𝒜)
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p ({s ∈ 𝒜 | a ∉ s}) → p ({s ∈ 𝒜 | a ∈ s}) → p 𝒜
⊢ p 𝒜
have refine : ∀ (a : α) (𝒜 : Finset (Finset α)) (h𝒜₀ : p (nonMemberSubfamily a 𝒜)) (h𝒜₁ : p (memberSubfamily a 𝒜)),
  p ({s ∈ 𝒜 | a ∈ s})
Tactic: refine memberFamily_induction_on 𝒜 empty singleton_empty fun a 𝒜 h𝒜₀ h𝒜₁ ↦ subfamily a h𝒜₀ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
𝒜_1 : Finset (Finset α)
empty : p ∅
singleton_empty : p {∅}
image_insert : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, (∀ s ∈ 𝒜, a ∉ s) → p 𝒜 → p (image (insert a) 𝒜)
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p ({s ∈ 𝒜 | a ∉ s}) → p ({s ∈ 𝒜 | a ∈ s}) → p 𝒜
a : α
𝒜 : Finset (Finset α)
h𝒜₀ : p (nonMemberSubfamily a 𝒜)
h𝒜₁ : p (memberSubfamily a 𝒜)
⊢ p ({s ∈ 𝒜 | a ∈ s})
have rw : p (image (insert a) (memberSubfamily a 𝒜))
Tactic: rw [← image_insert_memberSubfamily]