awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
a : α
hat : a ∈ t
u : Finset α
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[#u] 𝒜 ↔ ∃ (u_1 : Finset α), #u_1 = #u ∧ u_1 ⊆ t ∧ t \ u_1 ∈ 𝒜
htu : t \ insert a u ∈ 𝒜
hut : u ⊆ t
hau : a ∉ u
⊢ ∃ (u_1 : Finset α), (∃ (a : α) (t : Finset α), a ∉ t ∧ insert a t = u_1 ∧ #t = #u) ∧ u_1 ⊆ t ∧ t \ u_1 ∈ 𝒜

Tactic:
⟨_, ⟨_, _, hau, rfl, rfl⟩, insert_subset hat hut, htu⟩

Premises used: Finset.insert_subset, And.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
a : α
hat : a ∈ t
u : Finset α
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[#u] 𝒜 ↔ ∃ (u_1 : Finset α), #u_1 = #u ∧ u_1 ⊆ t ∧ t \ u_1 ∈ 𝒜
htu : t \ insert a u ∈ 𝒜
hut : u ⊆ t
hau : a ∉ u
⊢ ∃ (u_1 : Finset α), (∃ (a : α) (t : Finset α), a ∉ t ∧ insert a t = u_1 ∧ #t = #u) ∧ u_1 ⊆ t ∧ t \ u_1 ∈ 𝒜

Tactic:
exact ⟨_, ⟨_, _, hau, rfl, rfl⟩, insert_subset hat hut, htu⟩
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
a : α
u : Finset α
hau : a ∉ u
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[#u] 𝒜 ↔ ∃ (u_1 : Finset α), #u_1 = #u ∧ u_1 ⊆ t ∧ t \ u_1 ∈ 𝒜
hut : insert a u ⊆ t
htu : t \ insert a u ∈ 𝒜
⊢ a ∈ t ∧ u ⊆ t

Tactic:
rw [insert_subset_iff] at hut

Premises used: Finset.insert_subset_iff
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
a : α
u : Finset α
hau : a ∉ u
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[#u] 𝒜 ↔ ∃ (u_1 : Finset α), #u_1 = #u ∧ u_1 ⊆ t ∧ t \ u_1 ∈ 𝒜
hut : insert a u ⊆ t
htu : t \ insert a u ∈ 𝒜
hut₁ : a ∈ t ∧ u ⊆ t
⊢ t \ insert a u ∈ 𝒜

Tactic:
rw [insert_subset_iff] at hut

Premises used: Finset.insert_subset_iff
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
a : α
u : Finset α
hau : a ∉ u
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[#u] 𝒜 ↔ ∃ (u_1 : Finset α), #u_1 = #u ∧ u_1 ⊆ t ∧ t \ u_1 ∈ 𝒜
hut : a ∈ t ∧ u ⊆ t
htu : t \ insert a u ∈ 𝒜
⊢ ∃ a ∈ t, ∃ (u_1 : Finset α), #u_1 = #u ∧ (u_1 ⊆ t ∧ a ∉ u_1) ∧ t \ insert a u_1 ∈ 𝒜

Tactic:
⟨a, hut.1, _, rfl, ⟨hut.2, hau⟩, htu⟩

Premises used: And.right, And.left, And.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
a : α
u : Finset α
hau : a ∉ u
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[#u] 𝒜 ↔ ∃ (u_1 : Finset α), #u_1 = #u ∧ u_1 ⊆ t ∧ t \ u_1 ∈ 𝒜
hut : a ∈ t ∧ u ⊆ t
htu : t \ insert a u ∈ 𝒜
⊢ ∃ a ∈ t, ∃ (u_1 : Finset α), #u_1 = #u ∧ (u_1 ⊆ t ∧ a ∉ u_1) ∧ t \ insert a u_1 ∈ 𝒜

Tactic:
exact ⟨a, hut.1, _, rfl, ⟨hut.2, hau⟩, htu⟩
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
zero : ∀ {t : Finset α}, t ∈ ∂⁺ ^[0] 𝒜 ↔ ∃ (u : Finset α), #u = 0 ∧ u ⊆ t ∧ t \ u ∈ 𝒜
succ :
  ∀ (k : ℕ) (ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ (u : Finset α), #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜) {t : Finset α},
    t ∈ ∂⁺ ^[k + 1] 𝒜 ↔ ∃ (u : Finset α), #u = k + 1 ∧ u ⊆ t ∧ t \ u ∈ 𝒜
⊢ t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ (u : Finset α), #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜

Tactic:
induction k generalizing t with
  | zero => simp
  | succ k ih =>
    simp only [mem_upShadow_iff_erase_mem, ih, Function.iterate_succ_apply', card_eq_succ,
      subset_erase, erase_sdiff_comm, ← sdiff_insert]
    constructor
    · rintro ⟨a, hat, u, rfl, ⟨hut, hau⟩, htu⟩
      exact ⟨_, ⟨_, _, hau, rfl, rfl⟩, insert_subset hat hut, htu⟩
    · rintro ⟨_, ⟨a, u, hau, rfl, rfl⟩, hut, htu⟩
      rw [insert_subset_iff] at hut
      exact ⟨a, hut.1, _, rfl, ⟨hut.2, hau⟩, htu⟩

Premises used: Function.iterate_succ_apply', Finset.insert_subset_iff, Finset.sdiff_insert, Finset.card_eq_succ, Finset.subset_erase, Finset.mem_upShadow_iff_erase_mem, Nat.zero, Nat.succ, Finset.erase_sdiff_comm, rfl
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
rw : (∃ (u : Finset α), #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜) ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = k
⊢ t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = k

Tactic:
rw [mem_upShadow_iterate_iff_exists_card]

Premises used: Finset.mem_upShadow_iterate_iff_exists_card
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
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
mpr : (∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = k) → ∃ (u : Finset α), #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜
⊢ (∃ (u : Finset α), #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜) ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = k

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t u : Finset α
hut : u ⊆ t
htu : t \ u ∈ 𝒜
rw rw₁ : #u = #u
⊢ #(t \ (t \ u)) = #u

Tactic:
rw [sdiff_sdiff_eq_self hut]

Premises used: Finset.sdiff_sdiff_eq_self
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t u : Finset α
hut : u ⊆ t
htu : t \ u ∈ 𝒜
⊢ ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = #u

Tactic:
exact ⟨_, htu, sdiff_subset, by rw [sdiff_sdiff_eq_self hut]⟩
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t s : Finset α
hs : s ∈ 𝒜
hst : s ⊆ t
rwa rwa₁ rwa₂ rwa₃ : s ∈ 𝒜
⊢ t \ (t \ s) ∈ 𝒜

Tactic:
rwa [sdiff_sdiff_eq_self hst]

Premises used: Finset.sdiff_sdiff_eq_self
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t s : Finset α
hs : s ∈ 𝒜
hst : s ⊆ t
⊢ ∃ (u : Finset α), #u = #(t \ s) ∧ u ⊆ t ∧ t \ u ∈ 𝒜

Tactic:
exact ⟨_, rfl, sdiff_subset, by rwa [sdiff_sdiff_eq_self hst]⟩
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #t = #s + k

Tactic:
mem_upShadow_iterate_iff_exists_sdiff.trans <| exists_congr fun t ↦ and_congr_right fun _ ↦
    and_congr_right fun hst ↦ ?_

Premises used: and_congr_right, exists_congr, Iff.trans, Finset.mem_upShadow_iterate_iff_exists_sdiff
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
refine : ∀ t_1 ∈ 𝒜, ∀ (hst : t_1 ⊆ t), #(t \ t_1) = k ↔ #t = #t_1 + k
⊢ t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #t = #s + k

Tactic:
refine mem_upShadow_iterate_iff_exists_sdiff.trans <| exists_congr fun t ↦ and_congr_right fun _ ↦
    and_congr_right fun hst ↦ ?_

Premises used: and_congr_right, exists_congr, Iff.trans, Finset.mem_upShadow_iterate_iff_exists_sdiff
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t_1 : Finset α
k : ℕ
t : Finset α
h : t ∈ 𝒜
hst : t ⊆ t_1
rw : #t ≤ #t_1
⊢ #(t_1 \ t) = k ↔ #t_1 = #t + k

Tactic:
rw [card_sdiff_of_subset hst, tsub_eq_iff_eq_add_of_le, add_comm]

Premises used: Finset.card_sdiff_of_subset, add_comm, tsub_eq_iff_eq_add_of_le
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t_1 : Finset α
k : ℕ
t : Finset α
h : t ∈ 𝒜
hst : t ⊆ t_1
⊢ #t ≤ #t_1

Tactic:
card_mono hst

Premises used: Finset.card_mono
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t_1 : Finset α
k : ℕ
t : Finset α
h : t ∈ 𝒜
hst : t ⊆ t_1
⊢ #t ≤ #t_1

Tactic:
exact card_mono hst

Premises used: Finset.card_mono
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
A : Finset α
h : A ∈ (↑(∂⁺ 𝒜) : Set (Finset α))
obtain :
  ∀ (A : Finset α) (hA : A ∈ 𝒜) (i : α) (hi : i ∉ A) (h : insert i A ∈ (↑(∂⁺ 𝒜) : Set (Finset α))),
    #(insert i A) = r + 1
⊢ #A = r + 1

Tactic:
obtain ⟨A, hA, i, hi, rfl⟩ := mem_upShadow_iff.1 h

Premises used: Iff.mp, Finset.mem_upShadow_iff, rfl
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
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
rw₁ rw₂ : r + 1 = r + 1
⊢ #(insert i A) = r + 1

Tactic:
rw [card_insert_of_notMem hi, h𝒜 hA]

Premises used: Finset.card_insert_of_notMem
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ ∂⁺ 𝒜
⊢ ∃ t ∈ 𝒜, t ⊆ s

Tactic:
let ⟨t, ht, hts, _⟩ := mem_upShadow_iff_exists_mem_card_add_one.1 hs
  ⟨t, ht, hts⟩

Premises used: Membership.mem, Exists, _private.0.Finset.exists_subset_of_mem_upShadow.match_1, HasSubset.Subset, And, And.intro, Exists.intro, Iff.mp, Finset.mem_upShadow_iff_exists_mem_card_add_one
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ ∂⁺ ^[0] 𝒜 ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + 0 = #s

Tactic:
⟨fun hs => ⟨s, hs, Subset.refl _, rfl⟩, ?_⟩

Premises used: Finset.Subset.refl, And.intro, Iff.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
zero : (∃ t ∈ 𝒜, t ⊆ s ∧ #t + 0 = #s) → s ∈ ∂⁺ ^[0] 𝒜
⊢ s ∈ ∂⁺ ^[0] 𝒜 ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + 0 = #s

Tactic:
refine ⟨fun hs => ⟨s, hs, Subset.refl _, rfl⟩, ?_⟩
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : t ⊆ s
hcard : #t + 0 = #s
zero zero₁ zero₂ zero₃ : t ∈ ∂⁺ ^[0] 𝒜
⊢ s ∈ ∂⁺ ^[0] 𝒜

Tactic:
rwa [← eq_of_subset_of_card_le hst hcard.ge]

Premises used: Eq.ge, Finset.eq_of_subset_of_card_le
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
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 α
succ : s ∈ ∂⁺ ^[k] (∂⁺ 𝒜) ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s
⊢ s ∈ ∂⁺ ^[k + 1] 𝒜 ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s

Tactic:
simp only [Function.comp_apply, Function.iterate_succ]

Premises used: Function.iterate_succ, Function.comp_apply
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
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

Tactic:
ih.trans ?_

Premises used: Iff.trans
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
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 α
succ : (∃ t ∈ ∂⁺ 𝒜, t ⊆ s ∧ #t + k = #s) ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s
⊢ s ∈ ∂⁺ ^[k] (∂⁺ 𝒜) ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s

Tactic:
refine ih.trans ?_

Premises used: Iff.trans
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
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
succ₁ : (∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s) → ∃ t ∈ ∂⁺ 𝒜, t ⊆ s ∧ #t + k = #s
⊢ (∃ t ∈ ∂⁺ 𝒜, t ⊆ s ∧ #t + k = #s) ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ ∂⁺ 𝒜
hts : t ⊆ s
hcardst : #t + k = #s
succ : ∀ (u : Finset α) (hu : u ∈ 𝒜) (hut : u ⊆ t) (hcardtu : #t = #u + 1), ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s
⊢ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s

Tactic:
obtain ⟨u, hu, hut, hcardtu⟩ := mem_upShadow_iff_exists_mem_card_add_one.1 ht

Premises used: Iff.mp, Finset.mem_upShadow_iff_exists_mem_card_add_one
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
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

Tactic:
⟨u, hu, hut.trans hts, ?_⟩

Premises used: HasSubset.Subset.trans, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
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
succ : #u + (k + 1) = #s
⊢ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s

Tactic:
refine ⟨u, hu, hut.trans hts, ?_⟩
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
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
succ : #u + (k + 1) = #u + k + 1
⊢ #u + (k + 1) = #s

Tactic:
rw [← hcardst, hcardtu, add_right_comm]

Premises used: add_right_comm
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
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) = #u + k + 1

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
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 + 1 ≤ #s

Tactic:
lia
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
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
succ : ∀ (u : Finset α) (htu : t ⊆ u) (hus : u ⊆ s) (hu : #u = #t + 1), ∃ t ∈ ∂⁺ 𝒜, t ⊆ s ∧ #t + k = #s
⊢ ∃ 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)

Premises used: Nat.le_add_right, OfNat.ofNat, Finset.exists_subsuperset_card_eq
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
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

Tactic:
⟨u, mem_upShadow_iff_exists_mem_card_add_one.2 ⟨t, ht, htu, hu⟩, hus, ?_⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Finset.mem_upShadow_iff_exists_mem_card_add_one
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
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
succ : #u + k = #s
⊢ ∃ t ∈ ∂⁺ 𝒜, t ⊆ s ∧ #t + k = #s

Tactic:
refine ⟨u, mem_upShadow_iff_exists_mem_card_add_one.2 ⟨t, ht, htu, hu⟩, hus, ?_⟩
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
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
succ : #t + k + 1 = #t + (k + 1)
⊢ #u + k = #s

Tactic:
rw [hu, ← hcard, add_right_comm]

Premises used: add_right_comm
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
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 + k + 1 = #t + (k + 1)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
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
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
⊢ s ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + k = #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

Premises used: Function.iterate_succ, add_right_comm, Nat.zero, Function.comp_apply, Nat.succ
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
h : ∀ (s : Finset α), s ∈ ∂ 𝒜ᶜˢ ↔ s ∈ (∂⁺ 𝒜)ᶜˢ
⊢ ∂ 𝒜ᶜˢ = (∂⁺ 𝒜)ᶜˢ

Tactic:
ext s
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
h : (∃ (s_1 : Finset α), s_1ᶜ ∈ 𝒜 ∧ ∃ a ∈ s_1, s_1.erase a = s) ↔ ∃ s_1 ∈ 𝒜, ∃ a ∉ s_1, insert a s_1 = sᶜ
⊢ s ∈ ∂ 𝒜ᶜˢ ↔ s ∈ (∂⁺ 𝒜)ᶜˢ

Tactic:
simp only [mem_shadow_iff, mem_upShadow_iff, mem_compls]

Premises used: Finset.mem_compls, Finset.mem_shadow_iff, Finset.mem_upShadow_iff
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
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ᶜ

Tactic:
(compl_involutive.toPerm _).exists_congr_left.trans ?_

Premises used: Equiv.exists_congr_left, Function.Involutive.toPerm, compl_involutive, Iff.trans
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
h :
  (∃ (b : Finset α),
      Membership.mem (α := Finset α) 𝒜
          (((Equiv.symm (Function.Involutive.toPerm compl ⋯) : (a : Finset α) → Finset α) b)ᶜ : Finset α) ∧
        ∃ (a : α),
          Membership.mem (γ := Finset α)
              ((Equiv.symm (Function.Involutive.toPerm compl ⋯) : (a : Finset α) → Finset α) b : Finset α) a ∧
            erase ((Equiv.symm (Function.Involutive.toPerm compl ⋯) : (a : Finset α) → Finset α) b) a = s) ↔
    ∃ s_1 ∈ 𝒜, ∃ a ∉ s_1, insert a s_1 = sᶜ
⊢ (∃ (s_1 : Finset α), s_1ᶜ ∈ 𝒜 ∧ ∃ a ∈ s_1, s_1.erase a = s) ↔ ∃ s_1 ∈ 𝒜, ∃ a ∉ s_1, insert a s_1 = sᶜ

Tactic:
refine (compl_involutive.toPerm _).exists_congr_left.trans ?_

Premises used: Equiv.exists_congr_left, Function.Involutive.toPerm, compl_involutive, Iff.trans
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ (b : Finset α),
      Membership.mem (α := Finset α) 𝒜
          (((Equiv.symm (Function.Involutive.toPerm compl ⋯) : (a : Finset α) → Finset α) b)ᶜ : Finset α) ∧
        ∃ (a : α),
          Membership.mem (γ := Finset α)
              ((Equiv.symm (Function.Involutive.toPerm compl ⋯) : (a : Finset α) → Finset α) b : Finset α) a ∧
            erase ((Equiv.symm (Function.Involutive.toPerm compl ⋯) : (a : Finset α) → Finset α) b) a = s) ↔
    ∃ s_1 ∈ 𝒜, ∃ a ∉ s_1, insert a s_1 = sᶜ

Tactic:
simp [← compl_involutive.eq_iff]

Premises used: compl_involutive, Function.Involutive.eq_iff
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
h : ∀ (s : Finset α), s ∈ ∂⁺ 𝒜ᶜˢ ↔ s ∈ (∂ 𝒜)ᶜˢ
⊢ ∂⁺ 𝒜ᶜˢ = (∂ 𝒜)ᶜˢ

Tactic:
ext s
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
h : (∃ (s_1 : Finset α), s_1ᶜ ∈ 𝒜 ∧ ∃ a ∉ s_1, insert a s_1 = s) ↔ ∃ s_1 ∈ 𝒜, ∃ a ∈ s_1, s_1.erase a = sᶜ
⊢ s ∈ ∂⁺ 𝒜ᶜˢ ↔ s ∈ (∂ 𝒜)ᶜˢ

Tactic:
simp only [mem_shadow_iff, mem_upShadow_iff, mem_compls]

Premises used: Finset.mem_compls, Finset.mem_shadow_iff, Finset.mem_upShadow_iff
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
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ᶜ

Tactic:
(compl_involutive.toPerm _).exists_congr_left.trans ?_

Premises used: Equiv.exists_congr_left, Function.Involutive.toPerm, compl_involutive, Iff.trans
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
h :
  (∃ (b : Finset α),
      Membership.mem (α := Finset α) 𝒜
          (((Equiv.symm (Function.Involutive.toPerm compl ⋯) : (a : Finset α) → Finset α) b)ᶜ : Finset α) ∧
        ∃ a ∉ ((Equiv.symm (Function.Involutive.toPerm compl ⋯) : (a : Finset α) → Finset α) b : Finset α),
          insert a ((Equiv.symm (Function.Involutive.toPerm compl ⋯) : (a : Finset α) → Finset α) b) = s) ↔
    ∃ s_1 ∈ 𝒜, ∃ a ∈ s_1, s_1.erase a = sᶜ
⊢ (∃ (s_1 : Finset α), s_1ᶜ ∈ 𝒜 ∧ ∃ a ∉ s_1, insert a s_1 = s) ↔ ∃ s_1 ∈ 𝒜, ∃ a ∈ s_1, s_1.erase a = sᶜ

Tactic:
refine (compl_involutive.toPerm _).exists_congr_left.trans ?_

Premises used: Equiv.exists_congr_left, Function.Involutive.toPerm, compl_involutive, Iff.trans
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ (b : Finset α),
      Membership.mem (α := Finset α) 𝒜
          (((Equiv.symm (Function.Involutive.toPerm compl ⋯) : (a : Finset α) → Finset α) b)ᶜ : Finset α) ∧
        ∃ a ∉ ((Equiv.symm (Function.Involutive.toPerm compl ⋯) : (a : Finset α) → Finset α) b : Finset α),
          insert a ((Equiv.symm (Function.Involutive.toPerm compl ⋯) : (a : Finset α) → Finset α) b) = s) ↔
    ∃ s_1 ∈ 𝒜, ∃ a ∈ s_1, s_1.erase a = sᶜ

Tactic:
simp [← compl_involutive.eq_iff]

Premises used: compl_involutive, Function.Involutive.eq_iff
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : 𝒜.Shatters s
ha : a ∈ s
⊢ ∃ t ∈ 𝒜, s ∩ t = {a}

Tactic:
hs <| singleton_subset_iff.2 ha

Premises used: Iff.mpr, Finset.singleton_subset_iff
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h : 𝒜 ⊆ ℬ
h𝒜 : 𝒜.Shatters s
⊢ ℬ.Shatters s

Tactic:
fun _t ht ↦ let ⟨u, hu, hut⟩ := h𝒜 ht; ⟨u, h hu, hut⟩

Premises used: Membership.mem, Exists, Inter.inter, And, And.intro, Exists.intro, _private.0.Finset.Shatters.mono_left.match_1, Finset.Shatters, Eq
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
h : t ⊆ s
hs : 𝒜.Shatters s
u : Finset α
hu : u ⊆ t
obtain : ∀ (v : Finset α) (hv : v ∈ 𝒜) (hu : s ∩ v ⊆ t), ∃ u ∈ 𝒜, t ∩ u = s ∩ v
⊢ ∃ u_1 ∈ 𝒜, t ∩ u_1 = u

Tactic:
obtain ⟨v, hv, rfl⟩ := hs (hu.trans h)

Premises used: HasSubset.Subset.trans, rfl
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
h : t ⊆ s
hs : 𝒜.Shatters s
v : Finset α
hv : v ∈ 𝒜
hu : s ∩ v ⊆ t
⊢ ∃ u ∈ 𝒜, t ∩ u = s ∩ v

Tactic:
⟨v, hv, inf_congr_right hu <| inf_le_of_left_le h⟩

Premises used: inf_le_of_left_le, inf_congr_right, And.intro, Exists.intro