awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ (∃ (u : Finset α), #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜) ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = k
have mp : (∃ (u : Finset α), #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜) → ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = k
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
mp : (∃ (u : Finset α), #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜) → ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = k
⊢ (∃ (u : Finset α), #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜) ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = k
have mpr : (∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = k) → ∃ (u : Finset α), #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t u : Finset α
hut : u ⊆ t
htu : t \ u ∈ 𝒜
⊢ #(t \ (t \ u)) = #u
have rw : #u = #u
Tactic: rw [sdiff_sdiff_eq_self hut]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #t = #s + k
have refine : ∀ t_1 ∈ 𝒜, ∀ (hst : t_1 ⊆ t), #(t \ t_1) = k ↔ #t = #t_1 + k
Tactic: refine mem_upShadow_iterate_iff_exists_sdiff.trans <| exists_congr fun t ↦ and_congr_right fun _ ↦
    and_congr_right fun hst ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t_1 : Finset α
k : ℕ
t : Finset α
h : t ∈ 𝒜
hst : t ⊆ t_1
⊢ #(t_1 \ t) = k ↔ #t_1 = #t + k
have rw : #t ≤ #t_1
Tactic: rw [card_sdiff_of_subset hst, tsub_eq_iff_eq_add_of_le, add_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
A : Finset α
h : A ∈ (↑(∂⁺ 𝒜) : Set (Finset α))
⊢ #A = r + 1
have obtain : ∀ (A : Finset α) (hA : A ∈ 𝒜) (i : α) (hi : i ∉ A) (h : insert i A ∈ (↑(∂⁺ 𝒜) : Set (Finset α))), #(insert i A) = r + 1
Tactic: obtain ⟨A, hA, i, hi, rfl⟩ := mem_upShadow_iff.1 h
Cleared hypotheses: A, h
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
A : Finset α
hA : A ∈ 𝒜
i : α
hi : i ∉ A
h : insert i A ∈ (↑(∂⁺ 𝒜) : Set (Finset α))
⊢ #(insert i A) = r + 1
have rw : #A + 1 = r + 1
Tactic: rw [card_insert_of_notMem hi, h𝒜 hA]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
A : Finset α
hA : A ∈ 𝒜
i : α
hi : i ∉ A
h : insert i A ∈ (↑(∂⁺ 𝒜) : Set (Finset α))
rw : #A + 1 = r + 1
⊢ #(insert i A) = r + 1
have rw₁ : r + 1 = r + 1
Tactic: rw [card_insert_of_notMem hi, h𝒜 hA]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ ∂⁺ ^[0] 𝒜 ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + 0 = #s
have zero : (∃ t ∈ 𝒜, t ⊆ s ∧ #t + 0 = #s) → s ∈ ∂⁺ ^[0] 𝒜
Tactic: refine ⟨fun hs => ⟨s, hs, Subset.refl _, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : t ⊆ s
hcard : #t + 0 = #s
⊢ s ∈ ∂⁺ ^[0] 𝒜
have zero : t ∈ ∂⁺ ^[0] 𝒜
Tactic: rwa [← eq_of_subset_of_card_le hst hcard.ge]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k : ℕ
ih : ∀ {𝒜 : Finset (Finset α)} {s : Finset α}, s ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + k = #s
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ ∂⁺ ^[k + 1] 𝒜 ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s
have succ : s ∈ ∂⁺ ^[k] (∂⁺ 𝒜) ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s
Tactic: simp only [Function.comp_apply, Function.iterate_succ]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k : ℕ
ih : ∀ {𝒜 : Finset (Finset α)} {s : Finset α}, s ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + k = #s
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ ∂⁺ ^[k] (∂⁺ 𝒜) ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s
have succ : (∃ t ∈ ∂⁺ 𝒜, t ⊆ s ∧ #t + k = #s) ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s
Tactic: refine ih.trans ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t ∈ ∂⁺ 𝒜, t ⊆ s ∧ #t + k = #s) ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s
have succ : (∃ t ∈ ∂⁺ 𝒜, t ⊆ s ∧ #t + k = #s) → ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
succ : (∃ t ∈ ∂⁺ 𝒜, t ⊆ s ∧ #t + k = #s) → ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s
⊢ (∃ t ∈ ∂⁺ 𝒜, t ⊆ s ∧ #t + k = #s) ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s
have succ₁ : (∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s) → ∃ t ∈ ∂⁺ 𝒜, t ⊆ s ∧ #t + k = #s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ ∂⁺ 𝒜
hts : t ⊆ s
hcardst : #t + k = #s
⊢ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s
have succ : ∀ (u : Finset α) (hu : u ∈ 𝒜) (hut : u ⊆ t) (hcardtu : #t = #u + 1), ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s
Tactic: obtain ⟨u, hu, hut, hcardtu⟩ := mem_upShadow_iff_exists_mem_card_add_one.1 ht
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ ∂⁺ 𝒜
hts : t ⊆ s
hcardst : #t + k = #s
u : Finset α
hu : u ∈ 𝒜
hut : u ⊆ t
hcardtu : #t = #u + 1
⊢ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s
have succ : #u + (k + 1) = #s
Tactic: refine ⟨u, hu, hut.trans hts, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ ∂⁺ 𝒜
hts : t ⊆ s
hcardst : #t + k = #s
u : Finset α
hu : u ∈ 𝒜
hut : u ⊆ t
hcardtu : #t = #u + 1
⊢ #u + (k + 1) = #s
have succ : #u + (k + 1) = #u + k + 1
Tactic: rw [← hcardst, hcardtu, add_right_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
hcard : #t + (k + 1) = #s
⊢ ∃ t ∈ ∂⁺ 𝒜, t ⊆ s ∧ #t + k = #s
have succ : ∀ (u : Finset α) (htu : t ⊆ u) (hus : u ⊆ s) (hu : #u = #t + 1), ∃ t ∈ ∂⁺ 𝒜, t ⊆ s ∧ #t + k = #s
Tactic: obtain ⟨u, htu, hus, hu⟩ := Finset.exists_subsuperset_card_eq hts (Nat.le_add_right _ 1)
        (by lia)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
hcard : #t + (k + 1) = #s
u : Finset α
htu : t ⊆ u
hus : u ⊆ s
hu : #u = #t + 1
⊢ ∃ t ∈ ∂⁺ 𝒜, t ⊆ s ∧ #t + k = #s
have succ : #u + k = #s
Tactic: refine ⟨u, mem_upShadow_iff_exists_mem_card_add_one.2 ⟨t, ht, htu, hu⟩, hus, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
hcard : #t + (k + 1) = #s
u : Finset α
htu : t ⊆ u
hus : u ⊆ s
hu : #u = #t + 1
⊢ #u + k = #s
have succ : #t + k + 1 = #t + (k + 1)
Tactic: rw [hu, ← hcard, add_right_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
k : ℕ
⊢ s ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + k = #s
have zero : ∀ {𝒜 : Finset (Finset α)} {s : Finset α}, s ∈ ∂⁺ ^[0] 𝒜 ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + 0 = #s
Tactic: induction k generalizing 𝒜 s with
  | zero =>
    refine ⟨fun hs => ⟨s, hs, Subset.refl _, rfl⟩, ?_⟩
    rintro ⟨t, ht, hst, hcard⟩
    rwa [← eq_of_subset_of_card_le hst hcard.ge]
  | succ k ih =>
    simp only [Function.comp_apply, Function.iterate_succ]
    refine ih.trans ?_
    clear ih
    constructor
    · rintro ⟨t, ht, hts, hcardst⟩
      obtain ⟨u, hu, hut, hcardtu⟩ := mem_upShadow_iff_exists_mem_card_add_one.1 ht
      refine ⟨u, hu, hut.trans hts, ?_⟩
      rw [← hcardst, hcardtu, add_right_comm]
      rfl
    · rintro ⟨t, ht, hts, hcard⟩
      obtain ⟨u, htu, hus, hu⟩ := Finset.exists_subsuperset_card_eq hts (Nat.le_add_right _ 1)
        (by lia)
      refine ⟨u, mem_upShadow_iff_exists_mem_card_add_one.2 ⟨t, ht, htu, hu⟩, hus, ?_⟩
      rw [hu, ← hcard, add_right_comm]
      rfl
Cleared hypotheses: 𝒜, s, k
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
k : ℕ
zero : ∀ {𝒜 : Finset (Finset α)} {s : Finset α}, s ∈ ∂⁺ ^[0] 𝒜 ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + 0 = #s
⊢ s ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + k = #s
have succ : ∀ (k : ℕ) (ih : ∀ {𝒜 : Finset (Finset α)} {s : Finset α}, s ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + k = #s)
  {𝒜 : Finset (Finset α)} {s : Finset α}, s ∈ ∂⁺ ^[k + 1] 𝒜 ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s
Tactic: induction k generalizing 𝒜 s with
  | zero =>
    refine ⟨fun hs => ⟨s, hs, Subset.refl _, rfl⟩, ?_⟩
    rintro ⟨t, ht, hst, hcard⟩
    rwa [← eq_of_subset_of_card_le hst hcard.ge]
  | succ k ih =>
    simp only [Function.comp_apply, Function.iterate_succ]
    refine ih.trans ?_
    clear ih
    constructor
    · rintro ⟨t, ht, hts, hcardst⟩
      obtain ⟨u, hu, hut, hcardtu⟩ := mem_upShadow_iff_exists_mem_card_add_one.1 ht
      refine ⟨u, hu, hut.trans hts, ?_⟩
      rw [← hcardst, hcardtu, add_right_comm]
      rfl
    · rintro ⟨t, ht, hts, hcard⟩
      obtain ⟨u, htu, hus, hu⟩ := Finset.exists_subsuperset_card_eq hts (Nat.le_add_right _ 1)
        (by lia)
      refine ⟨u, mem_upShadow_iff_exists_mem_card_add_one.2 ⟨t, ht, htu, hu⟩, hus, ?_⟩
      rw [hu, ← hcard, add_right_comm]
      rfl
Cleared hypotheses: 𝒜, s, k
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
⊢ ∂ 𝒜ᶜˢ = (∂⁺ 𝒜)ᶜˢ
have h : ∀ (s : Finset α), s ∈ ∂ 𝒜ᶜˢ ↔ s ∈ (∂⁺ 𝒜)ᶜˢ
Tactic: ext s
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ ∂ 𝒜ᶜˢ ↔ s ∈ (∂⁺ 𝒜)ᶜˢ
have h : (∃ (s_1 : Finset α), s_1ᶜ ∈ 𝒜 ∧ ∃ a ∈ s_1, s_1.erase a = s) ↔ ∃ s_1 ∈ 𝒜, ∃ a ∉ s_1, insert a s_1 = sᶜ
Tactic: simp only [mem_shadow_iff, mem_upShadow_iff, mem_compls]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ (s_1 : Finset α), s_1ᶜ ∈ 𝒜 ∧ ∃ a ∈ s_1, s_1.erase a = s) ↔ ∃ s_1 ∈ 𝒜, ∃ a ∉ s_1, insert a s_1 = sᶜ
have h : (∃ (b : Finset α),
    Membership.mem (α := Finset α) 𝒜
        (((Equiv.symm (Function.Involutive.toPerm compl sorry) : (a : Finset α) → Finset α) b)ᶜ : Finset α) ∧
      ∃ (a : α),
        Membership.mem (γ := Finset α)
            ((Equiv.symm (Function.Involutive.toPerm compl sorry) : (a : Finset α) → Finset α) b : Finset α) a ∧
          erase ((Equiv.symm (Function.Involutive.toPerm compl sorry) : (a : Finset α) → Finset α) b) a = s) ↔
  ∃ s_1 ∈ 𝒜, ∃ a ∉ s_1, insert a s_1 = sᶜ
Tactic: refine (compl_involutive.toPerm _).exists_congr_left.trans ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
⊢ ∂⁺ 𝒜ᶜˢ = (∂ 𝒜)ᶜˢ
have h : ∀ (s : Finset α), s ∈ ∂⁺ 𝒜ᶜˢ ↔ s ∈ (∂ 𝒜)ᶜˢ
Tactic: ext s
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ ∂⁺ 𝒜ᶜˢ ↔ s ∈ (∂ 𝒜)ᶜˢ
have h : (∃ (s_1 : Finset α), s_1ᶜ ∈ 𝒜 ∧ ∃ a ∉ s_1, insert a s_1 = s) ↔ ∃ s_1 ∈ 𝒜, ∃ a ∈ s_1, s_1.erase a = sᶜ
Tactic: simp only [mem_shadow_iff, mem_upShadow_iff, mem_compls]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ (s_1 : Finset α), s_1ᶜ ∈ 𝒜 ∧ ∃ a ∉ s_1, insert a s_1 = s) ↔ ∃ s_1 ∈ 𝒜, ∃ a ∈ s_1, s_1.erase a = sᶜ
have h : (∃ (b : Finset α),
    Membership.mem (α := Finset α) 𝒜
        (((Equiv.symm (Function.Involutive.toPerm compl sorry) : (a : Finset α) → Finset α) b)ᶜ : Finset α) ∧
      ∃ a ∉ ((Equiv.symm (Function.Involutive.toPerm compl sorry) : (a : Finset α) → Finset α) b : Finset α),
        insert a ((Equiv.symm (Function.Involutive.toPerm compl sorry) : (a : Finset α) → Finset α) b) = s) ↔
  ∃ s_1 ∈ 𝒜, ∃ a ∈ s_1, s_1.erase a = sᶜ
Tactic: refine (compl_involutive.toPerm _).exists_congr_left.trans ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
h : t ⊆ s
hs : 𝒜.Shatters s
u : Finset α
hu : u ⊆ t
⊢ ∃ u_1 ∈ 𝒜, t ∩ u_1 = u
have obtain : ∀ (v : Finset α) (hv : v ∈ 𝒜) (hu : s ∩ v ⊆ t), ∃ u ∈ 𝒜, t ∩ u = s ∩ v
Tactic: obtain ⟨v, hv, rfl⟩ := hs (hu.trans h)
Cleared hypotheses: u, hu
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
h : 𝒜.Nonempty
t : Finset α
ht : t ⊆ ∅
s : Finset α
hs : s ∈ 𝒜
⊢ ∅ ∩ s = t
have rwa : ∅ = t
Tactic: rwa [empty_inter, eq_comm, ← subset_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
h : 𝒜.Nonempty
t : Finset α
ht : t ⊆ ∅
s : Finset α
hs : s ∈ 𝒜
rwa : ∅ = t
⊢ ∅ ∩ s = t
have rwa₁ : t = ∅
Tactic: rwa [empty_inter, eq_comm, ← subset_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
⊢ image (fun (t : Finset α) ↦ s ∩ t) 𝒜 = s.powerset
have h₁ : ∀ (t : Finset α), Membership.mem (γ := Finset (Finset α)) (image (fun (t : Finset α) ↦ s ∩ t) 𝒜) t ↔ t ∈ s.powerset
Tactic: ext t
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
t : Finset α
⊢ Membership.mem (γ := Finset (Finset α)) (image (fun (t : Finset α) ↦ s ∩ t) 𝒜) t ↔ t ∈ s.powerset
have h₁ : (∃ a ∈ 𝒜, s ∩ a = t) ↔ t ∈ s.powerset
Tactic: rw [mem_image, mem_powerset, h.subset_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
t : Finset α
h₁ : (∃ a ∈ 𝒜, s ∩ a = t) ↔ t ∈ s.powerset
⊢ Membership.mem (γ := Finset (Finset α)) (image (fun (t : Finset α) ↦ s ∩ t) 𝒜) t ↔ t ∈ s.powerset
have h₂ : (∃ a ∈ 𝒜, s ∩ a = t) ↔ t ⊆ s
Tactic: rw [mem_image, mem_powerset, h.subset_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
t : Finset α
h₁ : (∃ a ∈ 𝒜, s ∩ a = t) ↔ t ∈ s.powerset
h₂ : (∃ a ∈ 𝒜, s ∩ a = t) ↔ t ⊆ s
⊢ Membership.mem (γ := Finset (Finset α)) (image (fun (t : Finset α) ↦ s ∩ t) 𝒜) t ↔ t ∈ s.powerset
have h₃ : (∃ a ∈ 𝒜, s ∩ a = t) ↔ ∃ u ∈ 𝒜, s ∩ u = t
Tactic: rw [mem_image, mem_powerset, h.subset_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : image (fun (t : Finset α) ↦ s ∩ t) 𝒜 = s.powerset
t : Finset α
ht : t ⊆ s
⊢ ∃ u ∈ 𝒜, s ∩ u = t
have rwa : ∀ (ht : t ∈ s.powerset), ∃ u ∈ 𝒜, s ∩ u = t
Tactic: rwa [← mem_powerset, ← h, mem_image] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : image (fun (t : Finset α) ↦ s ∩ t) 𝒜 = s.powerset
t : Finset α
ht : t ⊆ s
rwa : ∀ (ht : t ∈ s.powerset), ∃ u ∈ 𝒜, s ∩ u = t
⊢ ∃ u ∈ 𝒜, s ∩ u = t
have rwa₁ : ∀ (ht : Membership.mem (γ := Finset (Finset α)) (image (fun (t : Finset α) ↦ s ∩ t) 𝒜) t), ∃ u ∈ 𝒜, s ∩ u = t
Tactic: rwa [← mem_powerset, ← h, mem_image] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : image (fun (t : Finset α) ↦ s ∩ t) 𝒜 = s.powerset
t : Finset α
ht : t ⊆ s
rwa : ∀ (ht : t ∈ s.powerset), ∃ u ∈ 𝒜, s ∩ u = t
rwa₁ : ∀ (ht : Membership.mem (γ := Finset (Finset α)) (image (fun (t : Finset α) ↦ s ∩ t) 𝒜) t), ∃ u ∈ 𝒜, s ∩ u = t
⊢ ∃ u ∈ 𝒜, s ∩ u = t
have rwa₂ : ∀ (ht : ∃ a ∈ 𝒜, s ∩ a = t), ∃ u ∈ 𝒜, s ∩ u = t
Tactic: rwa [← mem_powerset, ← h, mem_image] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
inst_1 : Fintype α
⊢ 𝒜.Shatters univ ↔ 𝒜 = univ
have rw : Eq (α := Finset (Finset α)) (image (fun (t : Finset α) ↦ univ ∩ t) 𝒜) univ ↔ 𝒜 = univ
Tactic: rw [shatters_iff, powerset_univ]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
inst_1 : Fintype α
⊢ Eq (α := Finset (Finset α)) (image (fun (t : Finset α) ↦ univ ∩ t) 𝒜) univ ↔ 𝒜 = univ
have simp_rw : Eq (α := Finset (Finset α)) (image (fun (t : Finset α) ↦ t) 𝒜) univ ↔ 𝒜 = univ
Tactic: simp_rw [univ_inter, image_id']
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ 𝒜.shatterer ↔ 𝒜.Shatters s
have refine : ∀ (h : 𝒜.Shatters s), s ∈ 𝒜.biUnion powerset
Tactic: refine mem_filter.trans <| and_iff_right_of_imp fun h ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
⊢ s ∈ 𝒜.biUnion powerset
have simp_rw : ∃ a ∈ 𝒜, s ⊆ a
Tactic: simp_rw [mem_biUnion, mem_powerset]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
⊢ 𝒜.shatterer = 𝒜 ↔ IsLowerSet (↑𝒜 : Set (Finset α))
have refine_1 : ∀ (h : 𝒜.shatterer = 𝒜), IsLowerSet (↑𝒜 : Set (Finset α))
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ Subset.antisymm (fun s hs ↦ ?_) <| subset_shatterer h⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
refine_1 : ∀ (h : 𝒜.shatterer = 𝒜), IsLowerSet (↑𝒜 : Set (Finset α))
⊢ 𝒜.shatterer = 𝒜 ↔ IsLowerSet (↑𝒜 : Set (Finset α))
have refine_2 : ∀ (h : IsLowerSet (↑𝒜 : Set (Finset α))) (s : Finset α) (hs : s ∈ 𝒜.shatterer), s ∈ 𝒜
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ Subset.antisymm (fun s hs ↦ ?_) <| subset_shatterer h⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
h : 𝒜.shatterer = 𝒜
⊢ IsLowerSet (↑𝒜 : Set (Finset α))
have refine_1 : IsLowerSet (↑𝒜.shatterer : Set (Finset α))
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
h : IsLowerSet (↑𝒜 : Set (Finset α))
s : Finset α
hs : s ∈ 𝒜.shatterer
⊢ s ∈ 𝒜
have refine_2 : ∀ (t : Finset α) (ht : t ∈ 𝒜) (hst : s ⊆ t), s ∈ 𝒜
Tactic: obtain ⟨t, ht, hst⟩ := (mem_shatterer.1 hs).exists_superset
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
⊢ 𝒜.shatterer.Shatters s ↔ 𝒜.Shatters s
have simp_rw : s ∈ 𝒜.shatterer.shatterer ↔ s ∈ 𝒜.shatterer
Tactic: simp_rw [← mem_shatterer, shatterer_idem]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
a : α
h : ∀ t ∈ 𝒜, a ∉ t
ht : 𝒜.Shatters t
⊢ a ∉ t
have obtain : ∀ (u : Finset α) (hu : u ∈ 𝒜) (htu : t ⊆ u), a ∉ t
Tactic: obtain ⟨u, hu, htu⟩ := ht.exists_superset
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
⊢ #𝒜 ≤ #𝒜.shatterer
have refine_1 : card.{u_1} (α := Finset α) ∅ ≤ card.{u_1} (α := Finset α) (shatterer ∅)
Tactic: refine memberFamily_induction_on 𝒜 ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
refine_1 : card.{u_1} (α := Finset α) ∅ ≤ card.{u_1} (α := Finset α) (shatterer ∅)
⊢ #𝒜 ≤ #𝒜.shatterer
have refine_2 : card (α := Finset α) {∅} ≤ card (α := Finset α) {∅}
Tactic: refine memberFamily_induction_on 𝒜 ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
refine_1 : card.{u_1} (α := Finset α) ∅ ≤ card.{u_1} (α := Finset α) (shatterer ∅)
refine_2 : card (α := Finset α) {∅} ≤ card (α := Finset α) {∅}
⊢ #𝒜 ≤ #𝒜.shatterer
have refine_3 : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄,
  #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer →
    #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer → #𝒜 ≤ #𝒜.shatterer
Tactic: refine memberFamily_induction_on 𝒜 ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
⊢ #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
have refine : (↑((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer) : Set (Finset α)) ⊆ {s : Finset α | a ∉ s}
Tactic: refine card_image_of_injOn <| insert_erase_invOn.2.injOn.mono ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
⊢ (↑((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer) : Set (Finset α)) ⊆ {s : Finset α | a ∉ s}
have simp : ∀ (x : Finset α), (memberSubfamily a 𝒜).Shatters x → (nonMemberSubfamily a 𝒜).Shatters x → a ∉ x
Tactic: simp only [coe_inter, Set.subset_def, Set.mem_inter_iff, mem_coe, Set.mem_setOf_eq, and_imp,
      mem_shatterer]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shatter (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
⊢ #𝒜 ≤ #𝒜.shatterer
have hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
Tactic: have hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer) := by
    refine card_image_of_injOn <| insert_erase_invOn.2.injOn.mono ?_
    simp only [coe_inter, Set.subset_def, Set.mem_inter_iff, mem_coe, Set.mem_setOf_eq, and_imp,
      mem_shatterer]
    exact fun s _ ↦ aux (fun t ht ↦ (mem_filter.1 ht).2)