awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
this : LT.lt (α := ℚ≥0) 0 (↑((Fintype.card α).choose (Fintype.card α / 2)) : ℚ≥0)
s : Finset α
hs : s ∈ 𝒜
⊢ LT.lt (α := ℚ≥0) 0 (↑((Fintype.card α).choose #s) : ℚ≥0)

Tactic:
exact mod_cast choose_pos s.card_le_univ

Premises used: Nat.choose_pos, Finset.card_le_univ
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
this : LT.lt (α := ℚ≥0) 0 (↑((Fintype.card α).choose (Fintype.card α / 2)) : ℚ≥0)
s : Finset α
hs : s ∈ 𝒜
⊢ (Fintype.card α).choose #s ≤ (Fintype.card α).choose (Fintype.card α / 2)

Tactic:
choose_le_middle _ _

Premises used: Nat.choose_le_middle
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
this : LT.lt (α := ℚ≥0) 0 (↑((Fintype.card α).choose (Fintype.card α / 2)) : ℚ≥0)
s : Finset α
hs : s ∈ 𝒜
⊢ (Fintype.card α).choose #s ≤ (Fintype.card α).choose (Fintype.card α / 2)

Tactic:
exact choose_le_middle _ _

Premises used: Nat.choose_le_middle
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
this : LT.lt (α := ℚ≥0) 0 (↑((Fintype.card α).choose (Fintype.card α / 2)) : ℚ≥0)
⊢ LE.le (α := ℚ≥0) (∑ s ∈ 𝒜, (↑((Fintype.card α).choose (Fintype.card α / 2)) : ℚ≥0)⁻¹) 1

Tactic:
have h := calc
    ∑ s ∈ 𝒜, ((Fintype.card α).choose (Fintype.card α / 2) : ℚ≥0)⁻¹
    _ ≤ ∑ s ∈ 𝒜, ((Fintype.card α).choose #s : ℚ≥0)⁻¹ := by
      gcongr with s hs
      · exact mod_cast choose_pos s.card_le_univ
      · exact choose_le_middle _ _
    _ ≤ 1 := lubell_yamamoto_meshalkin_inequality_sum_inv_choose h𝒜
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
this : LT.lt (α := ℚ≥0) 0 (↑((Fintype.card α).choose (Fintype.card α / 2)) : ℚ≥0)
h : LE.le (α := ℚ≥0) (∑ s ∈ 𝒜, (↑((Fintype.card α).choose (Fintype.card α / 2)) : ℚ≥0)⁻¹) 1
⊢ #𝒜 ≤ (Fintype.card α).choose (Fintype.card α / 2)

Tactic:
simpa [mul_inv_le_iff₀' this] using h

Premises used: mul_inv_le_iff₀'
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
⊢ Eq.{u_1 + 1} (α := Finset (Finset α)) (∂ ∅) ∅

Tactic:
rfl

Premises used: Multiset.foldr, Finset.shadow, Finset.fold, Finset.sup, List.foldr, rfl, Multiset.fold
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
k : ℕ
zero : Eq.{u_1 + 1} (α := Finset (Finset α)) (∂^[0] ∅) ∅
succ :
  ∀ (n : ℕ), Eq.{u_1 + 1} (α := Finset (Finset α)) (∂^[n] ∅) ∅ → Eq.{u_1 + 1} (α := Finset (Finset α)) (∂^[n + 1] ∅) ∅
⊢ Eq.{u_1 + 1} (α := Finset (Finset α)) (∂^[k] ∅) ∅

Tactic:
induction k
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
⊢ Eq.{u_1 + 1} (α := Finset (Finset α)) (∂^[0] ∅) ∅

Tactic:
simp [*, shadow_empty]

Premises used: Finset.shadow_empty
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
h : Eq.{u_1 + 1} (α := Finset (Finset α)) (∂^[n] ∅) ∅
⊢ Eq.{u_1 + 1} (α := Finset (Finset α)) (∂^[n + 1] ∅) ∅

Tactic:
simp [*, shadow_empty]

Premises used: Finset.shadow_empty
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
⊢ Eq (α := Finset (Finset α)) (∂ {∅}) ∅

Tactic:
rfl

Premises used: Multiset.foldr, Finset.shadow, Finset.fold, Multiset.zero, Finset.empty, Multiset.ofList, Finset.sup, List.foldr, Multiset.ndunion, rfl, Multiset.fold
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
a : α
⊢ Eq (α := Finset (Finset α)) (∂ {{a}}) {∅}

Tactic:
simp [shadow]

Premises used: Finset.shadow
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
⊢ Monotone.{u_1, u_1} (α := Finset (Finset α)) ∂

Tactic:
fun _ _ =>
  sup_mono

Premises used: Set.Mem, Monotone, setOf, Finset.sup_mono
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜ℬ : 𝒜 ⊆ ℬ
⊢ ∂ 𝒜 ⊆ ∂ ℬ

Tactic:
shadow_monotone h𝒜ℬ

Premises used: Finset.shadow_monotone
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ ∂ 𝒜 ↔ ∃ s ∈ 𝒜, ∃ a ∈ s, s.erase a = t

Tactic:
simp only [shadow, mem_sup, mem_image]

Premises used: Finset.shadow, Finset.mem_sup, Finset.mem_image
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : s ∈ 𝒜
ha : a ∈ s
⊢ s.erase a ∈ ∂ 𝒜

Tactic:
mem_shadow_iff.2 ⟨s, hs, a, ha, rfl⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Finset.mem_shadow_iff, rfl
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
simp_rw : (∃ s ∈ 𝒜, ∃ a ∈ s, s.erase a = t) ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = 1
simp_rw₁ : (∃ s ∈ 𝒜, ∃ a ∈ s, s.erase a = t) ↔ ∃ s ∈ 𝒜, t ⋖ s
⊢ t ∈ ∂ 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = 1

Tactic:
simp_rw [mem_shadow_iff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_erase]

Premises used: Finset.covBy_iff_card_sdiff_eq_one, Finset.covBy_iff_exists_erase, Finset.mem_shadow_iff
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
simp_rw : (∃ s ∈ 𝒜, ∃ a ∉ t, insert a t = s) ↔ ∃ a ∉ t, insert a t ∈ 𝒜
⊢ t ∈ ∂ 𝒜 ↔ ∃ a ∉ t, insert a t ∈ 𝒜

Tactic:
simp_rw [mem_shadow_iff_exists_sdiff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_insert]

Premises used: Finset.covBy_iff_exists_insert, Finset.covBy_iff_card_sdiff_eq_one, Finset.mem_shadow_iff_exists_sdiff
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
⊢ (∃ s ∈ 𝒜, ∃ a ∉ t, insert a t = s) ↔ ∃ a ∉ t, insert a t ∈ 𝒜

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ ∂ 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #s = #t + 1

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

Premises used: and_congr_right, exists_congr, Finset.mem_shadow_iff_exists_sdiff, Iff.trans
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
refine : ∀ t_1 ∈ 𝒜, ∀ (hst : t ⊆ t_1), #(t_1 \ t) = 1 ↔ #t_1 = #t + 1
⊢ t ∈ ∂ 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #s = #t + 1

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

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

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 α
𝒜 : Finset (Finset α)
t_1 t : Finset α
h : t ∈ 𝒜
hst : t_1 ⊆ t
⊢ #t_1 ≤ #t

Tactic:
card_mono hst

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

Tactic:
exact card_mono hst

Premises used: Finset.card_mono
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ ∂^[0] 𝒜 ↔ ∃ (u : Finset α), #u = 0 ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜

Tactic:
simp
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
k : ℕ
ih : ∀ {t : Finset α}, t ∈ ∂^[k] 𝒜 ↔ ∃ (u : Finset α), #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜
t : Finset α
succ :
  (∃ a ∉ t, ∃ (u : Finset α), #u = k ∧ Disjoint (insert a t) u ∧ insert a t ∪ u ∈ 𝒜) ↔
    ∃ (u : Finset α), (∃ (a : α) (t : Finset α), a ∉ t ∧ insert a t = u ∧ #t = k) ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜
⊢ t ∈ ∂^[k + 1] 𝒜 ↔ ∃ (u : Finset α), #u = k + 1 ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜

Tactic:
simp only [mem_shadow_iff_insert_mem, ih, Function.iterate_succ_apply', card_eq_succ]

Premises used: Function.iterate_succ_apply', Finset.mem_shadow_iff_insert_mem, Finset.card_eq_succ
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
k : ℕ
ih : ∀ {t : Finset α}, t ∈ ∂^[k] 𝒜 ↔ ∃ (u : Finset α), #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜
t : Finset α
⊢ (∃ a ∉ t, ∃ (u : Finset α), #u = k ∧ Disjoint (insert a t) u ∧ insert a t ∪ u ∈ 𝒜) ↔
    ∃ (u : Finset α), (∃ (a : α) (t : Finset α), a ∉ t ∧ insert a t = u ∧ #t = k) ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
zero : ∀ {t : Finset α}, t ∈ ∂^[0] 𝒜 ↔ ∃ (u : Finset α), #u = 0 ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜
succ :
  ∀ (k : ℕ) (ih : ∀ {t : Finset α}, t ∈ ∂^[k] 𝒜 ↔ ∃ (u : Finset α), #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜) {t : Finset α},
    t ∈ ∂^[k + 1] 𝒜 ↔ ∃ (u : Finset α), #u = k + 1 ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜
⊢ t ∈ ∂^[k] 𝒜 ↔ ∃ (u : Finset α), #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜

Tactic:
induction k generalizing t with
  | zero => simp
  | succ k ih =>
    simp only [mem_shadow_iff_insert_mem, ih, Function.iterate_succ_apply', card_eq_succ]
    aesop

Premises used: Function.iterate_succ_apply', Finset.mem_shadow_iff_insert_mem, Finset.card_eq_succ, Nat.zero, Nat.succ
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
rw : (∃ (u : Finset α), #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜) ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = k
⊢ t ∈ ∂^[k] 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = k

Tactic:
rw [mem_shadow_iterate_iff_exists_card]

Premises used: Finset.mem_shadow_iterate_iff_exists_card
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
mp : (∃ (u : Finset α), #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜) → ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = k
mpr : (∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = k) → ∃ (u : Finset α), #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜
⊢ (∃ (u : Finset α), #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜) ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = k

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

Tactic:
rw [union_sdiff_cancel_left htu]

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

Tactic:
exact ⟨_, hsuA, subset_union_left, by rw [union_sdiff_cancel_left htu]⟩
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
t s : Finset α
hs : s ∈ 𝒜
hts : t ⊆ s
⊢ ∃ (u : Finset α), #u = #(s \ t) ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜

Tactic:
⟨s \ t, rfl, disjoint_sdiff, ?_⟩

Premises used: Finset.disjoint_sdiff, SDiff.sdiff, And.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
t s : Finset α
hs : s ∈ 𝒜
hts : t ⊆ s
mpr : t ∪ s \ t ∈ 𝒜
⊢ ∃ (u : Finset α), #u = #(s \ t) ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜

Tactic:
refine ⟨s \ t, rfl, disjoint_sdiff, ?_⟩
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
t s : Finset α
hs : s ∈ 𝒜
hts : t ⊆ s
mpr : t ∪ s ∈ 𝒜
mpr₁ mpr₂ mpr₃ mpr₄ : s ∈ 𝒜
⊢ t ∪ s \ t ∈ 𝒜

Tactic:
rwa [union_sdiff_self_eq_union, union_eq_right.2 hts]

Premises used: Iff.mpr, Finset.union_sdiff_self_eq_union, Finset.union_eq_right
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ t ∈ ∂^[k] 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #s = #t + k

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

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

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

Premises used: Finset.mem_shadow_iterate_iff_exists_sdiff, and_congr_right, exists_congr, Iff.trans
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
t_1 : Finset α
k : ℕ
t : Finset α
h : t ∈ 𝒜
hst : t_1 ⊆ t
rw : #t_1 ≤ #t
⊢ #(t \ t_1) = k ↔ #t = #t_1 + 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 α
𝒜 : Finset (Finset α)
t_1 : Finset α
k : ℕ
t : Finset α
h : t ∈ 𝒜
hst : t_1 ⊆ t
⊢ #t_1 ≤ #t

Tactic:
card_mono hst

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

Tactic:
exact card_mono hst

Premises used: Finset.card_mono
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : 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 : A.erase i ∈ (↑(∂ 𝒜) : Set (Finset α))), #(A.erase i) = r - 1
⊢ #A = r - 1

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

Premises used: Iff.mp, Finset.mem_shadow_iff, rfl
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
A : Finset α
hA : A ∈ 𝒜
i : α
hi : i ∈ A
h : A.erase i ∈ (↑(∂ 𝒜) : Set (Finset α))
rw : #A - 1 = r - 1
rw₁ rw₂ : r - 1 = r - 1
⊢ #(A.erase i) = r - 1

Tactic:
rw [card_erase_of_mem hi, h𝒜 hA]

Premises used: Finset.card_erase_of_mem
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
k r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
simp_rw : ∀ ⦃x : Finset α⦄, (∃ s ∈ 𝒜, x ⊆ s ∧ #(s \ x) = k) → #x = r - k
⊢ Set.Sized (r - k) (↑(∂^[k] 𝒜) : Set (Finset α))

Tactic:
simp_rw [Set.Sized, mem_coe, mem_shadow_iterate_iff_exists_sdiff]

Premises used: Finset.mem_shadow_iterate_iff_exists_sdiff, Set.Sized, Finset.mem_coe
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
t s : Finset α
hs : s ∈ 𝒜
hts : t ⊆ s
rw : #t = r - (#s - #t)
rw₁ : #t = #s - (#s - #t)
rw₂ rw₃ : #t = #t
⊢ #t = r - #(s \ t)

Tactic:
rw [card_sdiff_of_subset hts, ← h𝒜 hs, Nat.sub_sub_self (card_le_card hts)]

Premises used: Nat.sub_sub_self, Finset.card_le_card, Finset.card_sdiff_of_subset
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h : ∅ ∉ 𝒜
⊢ Set.Sized r (↑(∂ 𝒜) : Set (Finset α)) ↔ Set.Sized (r + 1) (↑𝒜 : Set (Finset α))

Tactic:
⟨fun h𝒜 s hs => ?_, Set.Sized.shadow⟩

Premises used: Iff.intro, Set.Sized.shadow
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h : ∅ ∉ 𝒜
refine : ∀ (h𝒜 : Set.Sized r (↑(∂ 𝒜) : Set (Finset α))) (s : Finset α) (hs : s ∈ (↑𝒜 : Set (Finset α))), #s = r + 1
⊢ Set.Sized r (↑(∂ 𝒜) : Set (Finset α)) ↔ Set.Sized (r + 1) (↑𝒜 : Set (Finset α))

Tactic:
refine ⟨fun h𝒜 s hs => ?_, Set.Sized.shadow⟩
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h : ∅ ∉ 𝒜
h𝒜 : Set.Sized r (↑(∂ 𝒜) : Set (Finset α))
s : Finset α
hs : s ∈ (↑𝒜 : Set (Finset α))
obtain : ∀ (a : α) (ha : a ∈ s), #s = r + 1
⊢ #s = r + 1

Tactic:
obtain ⟨a, ha⟩ := nonempty_iff_ne_empty.2 (ne_of_mem_of_not_mem hs h)

Premises used: Iff.mpr, Finset.nonempty_iff_ne_empty, ne_of_mem_of_not_mem
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h : ∅ ∉ 𝒜
h𝒜 : Set.Sized r (↑(∂ 𝒜) : Set (Finset α))
s : Finset α
hs : s ∈ (↑𝒜 : Set (Finset α))
a : α
ha : a ∈ s
rw : #s = #(s.erase a) + 1
rw₁ rw₂ : #s = #s
⊢ #s = r + 1

Tactic:
rw [← h𝒜 (erase_mem_shadow hs ha), card_erase_add_one ha]

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

Tactic:
let ⟨t, ht, hst⟩ := mem_shadow_iff_exists_mem_card_add_one.1 hs
  ⟨t, ht, hst.1⟩

Premises used: Membership.mem, Exists, HasSubset.Subset, And, _private.0.Finset.exists_subset_of_mem_shadow.match_1, And.left, And.intro, Exists.intro, Iff.mp, Finset.mem_shadow_iff_exists_mem_card_add_one
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
⊢ Eq.{u_1 + 1} (α := Finset (Finset α)) (∂⁺ ∅) ∅

Tactic:
rfl

Premises used: Multiset.foldr, Finset.fold, Finset.upShadow, Finset.sup, List.foldr, rfl, Multiset.fold
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
⊢ Monotone.{u_1, u_1} (α := Finset (Finset α)) ∂⁺

Tactic:
fun _ _ => sup_mono

Premises used: Set.Mem, Monotone, setOf, Finset.sup_mono
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
simp_rw :
  Membership.mem (γ := Finset (Finset α)) (𝒜.sup fun (s : Finset α) ↦ image (fun (a : α) ↦ insert a s) sᶜ) t ↔
    ∃ s ∈ 𝒜, ∃ a ∉ s, insert a s = t
simp_rw₁ :
  (∃ i ∈ 𝒜, Membership.mem (γ := Finset (Finset α)) (image (fun (a : α) ↦ insert a i) iᶜ) t) ↔
    ∃ s ∈ 𝒜, ∃ a ∉ s, insert a s = t
simp_rw₂ : (∃ i ∈ 𝒜, ∃ a ∈ iᶜ, insert a i = t) ↔ ∃ s ∈ 𝒜, ∃ a ∉ s, insert a s = t
⊢ t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, ∃ a ∉ s, insert a s = t

Tactic:
simp_rw [upShadow, mem_sup, mem_image, mem_compl]

Premises used: Finset.mem_sup, Finset.mem_image, Finset.upShadow, Finset.mem_compl
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : s ∈ 𝒜
ha : a ∉ s
⊢ insert a s ∈ ∂⁺ 𝒜

Tactic:
mem_upShadow_iff.2 ⟨s, hs, a, ha, rfl⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Finset.mem_upShadow_iff, rfl
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
simp_rw : (∃ s ∈ 𝒜, ∃ a ∉ s, insert a s = t) ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = 1
simp_rw₁ : (∃ s ∈ 𝒜, ∃ a ∉ s, insert a s = t) ↔ ∃ s ∈ 𝒜, s ⋖ t
⊢ t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = 1

Tactic:
simp_rw [mem_upShadow_iff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_insert]

Premises used: Finset.covBy_iff_exists_insert, Finset.covBy_iff_card_sdiff_eq_one, Finset.mem_upShadow_iff
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
simp_rw : (∃ s ∈ 𝒜, ∃ a ∈ t, t.erase a = s) ↔ ∃ a ∈ t, t.erase a ∈ 𝒜
⊢ t ∈ ∂⁺ 𝒜 ↔ ∃ a ∈ t, t.erase a ∈ 𝒜

Tactic:
simp_rw [mem_upShadow_iff_exists_sdiff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_erase]

Premises used: Finset.covBy_iff_card_sdiff_eq_one, Finset.mem_upShadow_iff_exists_sdiff, Finset.covBy_iff_exists_erase
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
⊢ (∃ s ∈ 𝒜, ∃ a ∈ t, t.erase a = s) ↔ ∃ a ∈ t, t.erase a ∈ 𝒜

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #t = #s + 1

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

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

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

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

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 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 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 α)
t : Finset α
⊢ t ∈ ∂⁺ ^[0] 𝒜 ↔ ∃ (u : Finset α), #u = 0 ∧ u ⊆ t ∧ t \ u ∈ 𝒜

Tactic:
simp
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
k : ℕ
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ (u : Finset α), #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜
t : Finset α
succ :
  (∃ a ∈ t, ∃ (u : Finset α), #u = k ∧ (u ⊆ t ∧ a ∉ u) ∧ t \ insert a u ∈ 𝒜) ↔
    ∃ (u : Finset α), (∃ (a : α) (t : Finset α), a ∉ t ∧ insert a t = u ∧ #t = k) ∧ u ⊆ t ∧ t \ u ∈ 𝒜
⊢ t ∈ ∂⁺ ^[k + 1] 𝒜 ↔ ∃ (u : Finset α), #u = k + 1 ∧ u ⊆ t ∧ t \ u ∈ 𝒜

Tactic:
simp only [mem_upShadow_iff_erase_mem, ih, Function.iterate_succ_apply', card_eq_succ,
      subset_erase, erase_sdiff_comm, ← sdiff_insert]

Premises used: Function.iterate_succ_apply', Finset.sdiff_insert, Finset.card_eq_succ, Finset.subset_erase, Finset.mem_upShadow_iff_erase_mem, Finset.erase_sdiff_comm
-- Module: Mathlib.Combinatorics.SetFamily.Shadow
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
k : ℕ
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ (u : Finset α), #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜
t : Finset α
succ :
  (∃ a ∈ t, ∃ (u : Finset α), #u = k ∧ (u ⊆ t ∧ a ∉ u) ∧ t \ insert a u ∈ 𝒜) →
    ∃ (u : Finset α), (∃ (a : α) (t : Finset α), a ∉ t ∧ insert a t = u ∧ #t = k) ∧ u ⊆ t ∧ t \ u ∈ 𝒜
succ₁ :
  (∃ (u : Finset α), (∃ (a : α) (t : Finset α), a ∉ t ∧ insert a t = u ∧ #t = k) ∧ u ⊆ t ∧ t \ u ∈ 𝒜) →
    ∃ a ∈ t, ∃ (u : Finset α), #u = k ∧ (u ⊆ t ∧ a ∉ u) ∧ t \ insert a u ∈ 𝒜
⊢ (∃ a ∈ t, ∃ (u : Finset α), #u = k ∧ (u ⊆ t ∧ a ∉ u) ∧ t \ insert a u ∈ 𝒜) ↔
    ∃ (u : Finset α), (∃ (a : α) (t : Finset α), a ∉ t ∧ insert a t = u ∧ #t = k) ∧ u ⊆ t ∧ t \ u ∈ 𝒜

Tactic:
constructor