awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose (n - r - (n - 2 * r)) ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this : n - r - (n - 2 * r) = r
kk₁ : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
⊢ n - r - (n - 2 * r) = r

Tactic:
rw [this] at kk
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this : n - r - (n - 2 * r) = r
⊢ (n - 1).succ.choose (r - 1).succ = (n - 1).choose (r - 1) + (n - 1).choose (r - 1).succ

Tactic:
Nat.choose_succ_succ _ _

Premises used: Nat.choose_succ_succ
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this : n - r - (n - 2 * r) = r
h : n = (n - 1).succ
h₁ h₄ : r = (r - 1).succ
⊢ n.choose r = (n - 1).choose (r - 1) + (n - 1).choose r

Tactic:
convert! Nat.choose_succ_succ _ _ using 3

Premises used: Nat.choose_succ_succ
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this : n - r - (n - 2 * r) = r
h : n = n.pred.succ
h₁ : n = n
h₄ : 0 < n
h₅ : n = n
h₆ h₇ h₈ : 0 < n
⊢ n = (n - 1).succ

Tactic:
rwa [Nat.sub_one, Nat.succ_pred_eq_of_pos]

Premises used: Nat.succ_pred_eq_of_pos, Nat.sub_one
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this : n - r - (n - 2 * r) = r
h : r = r.pred.succ
h₁ : r = r
h₄ : 0 < r
h₅ : r = r
h₆ h₇ h₈ : 0 < r
⊢ r = (r - 1).succ

Tactic:
rwa [Nat.sub_one, Nat.succ_pred_eq_of_pos]

Premises used: Nat.succ_pred_eq_of_pos, Nat.sub_one
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this : n - r - (n - 2 * r) = r
rw rw₁ : #𝒜 + #(∂^[n - 2 * r] 𝒜ᶜˢ) = #𝒜 + #(∂^[n - 2 * r] 𝒜ᶜˢ)
⊢ #𝒜 + #(∂^[n - 2 * r] 𝒜ᶜˢ) = #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)

Tactic:
rw [card_union_of_disjoint ‹_›]

Premises used: Finset.card_union_of_disjoint
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this : n - r - (n - 2 * r) = r
⊢ n.choose r < #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)

Tactic:
have := calc
    n.choose r = (n - 1).choose (r - 1) + (n - 1).choose r := by
      convert! Nat.choose_succ_succ _ _ using 3 <;> rwa [Nat.sub_one, Nat.succ_pred_eq_of_pos]
    _ < #𝒜 + #(∂^[n - 2 * r] 𝒜ᶜˢ) := add_lt_add_of_lt_of_le size kk
    _ = #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ) := by rw [card_union_of_disjoint ‹_›]
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this_4 : n - r - (n - 2 * r) = r
this : n.choose r < #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)
inr : #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ) ≤ n.choose r
⊢ False

Tactic:
apply this.not_ge

Premises used: LT.lt.not_ge
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this_4 : n - r - (n - 2 * r) = r
this : n.choose r < #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)
⊢ #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ) ≤ (Fintype.card (Fin n)).choose r

Tactic:
Set.Sized.card_le _

Premises used: Set.Sized.card_le
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this_4 : n - r - (n - 2 * r) = r
this : n.choose r < #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)
h : n = Fintype.card (Fin n)
inr : Fintype (Fin n)
inr₁ : Set.Sized r (↑(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ) : Set (Finset (Fin n)))
⊢ #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ) ≤ n.choose r

Tactic:
convert! Set.Sized.card_le _

Premises used: Set.Sized.card_le
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this_4 : n - r - (n - 2 * r) = r
this : n.choose r < #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)
h h₁ : n = n
⊢ n = Fintype.card (Fin n)

Tactic:
rw [Fintype.card_fin]

Premises used: Fintype.card_fin
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this_4 : n - r - (n - 2 * r) = r
this : n.choose r < #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)
inr : Set.Sized r (↑𝒜 : Set (Finset (Fin n))) ∧ Set.Sized r (↑(∂^[n - 2 * r] 𝒜ᶜˢ) : Set (Finset (Fin n)))
⊢ Set.Sized r (↑(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ) : Set (Finset (Fin n)))

Tactic:
rw [coe_union, Set.sized_union]

Premises used: Finset.coe_union, Set.sized_union
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this_4 : n - r - (n - 2 * r) = r
this : n.choose r < #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)
⊢ Set.Sized r (↑𝒜 : Set (Finset (Fin n))) ∧ Set.Sized r (↑(∂^[n - 2 * r] 𝒜ᶜˢ) : Set (Finset (Fin n)))

Tactic:
⟨‹_›, ?_⟩

Premises used: And.intro
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this_4 : n - r - (n - 2 * r) = r
this : n.choose r < #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)
inr : Set.Sized r (↑(∂^[n - 2 * r] 𝒜ᶜˢ) : Set (Finset (Fin n)))
⊢ Set.Sized r (↑𝒜 : Set (Finset (Fin n))) ∧ Set.Sized r (↑(∂^[n - 2 * r] 𝒜ᶜˢ) : Set (Finset (Fin n)))

Tactic:
refine ⟨‹_›, ?_⟩
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this_4 : n - r - (n - 2 * r) = r
this : n.choose r < #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)
⊢ Set.Sized (n - r - (n - 2 * r)) (↑(∂^[n - 2 * r] 𝒜ᶜˢ) : Set (Finset (Fin n)))

Tactic:
h𝒜bar.shadow_iterate

Premises used: Set.Sized.shadow_iterate
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this_4 : n - r - (n - 2 * r) = r
this : n.choose r < #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)
h : r = n - r - (n - 2 * r)
⊢ Set.Sized r (↑(∂^[n - 2 * r] 𝒜ᶜˢ) : Set (Finset (Fin n)))

Tactic:
convert! h𝒜bar.shadow_iterate

Premises used: Set.Sized.shadow_iterate
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this_4 : n - r - (n - 2 * r) = r
this : n.choose r < #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)
⊢ r = n - r - (n - 2 * r)

Tactic:
lia
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
i : DecidableRel fun (x1 x2 : Finset α) ↦ x1 ⊆ x2 :=
  fun (x x_1 : Finset α) ↦ Classical.dec ((fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) x x_1)
⊢ #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)

Tactic:
card_mul_le_card_mul' (· ⊆ ·) (fun s hs => ?_) (fun s hs => ?_)

Premises used: HasSubset.Subset, Finset.card_mul_le_card_mul'
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
i : DecidableRel fun (x1 x2 : Finset α) ↦ x1 ⊆ x2 :=
  fun (x x_1 : Finset α) ↦ Classical.dec ((fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) x x_1)
refine_1 : ∀ (s : Finset α) (hs : s ∈ 𝒜), r ≤ #(bipartiteBelow (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (∂ 𝒜) s)
refine_2 :
  ∀ (s : Finset α) (hs : s ∈ ∂ 𝒜), #(bipartiteAbove (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) 𝒜 s) ≤ Fintype.card α - r + 1
⊢ #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)

Tactic:
refine card_mul_le_card_mul' (· ⊆ ·) (fun s hs => ?_) (fun s hs => ?_)

Premises used: HasSubset.Subset, Finset.card_mul_le_card_mul'
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
i : DecidableRel fun (x1 x2 : Finset α) ↦ x1 ⊆ x2 :=
  fun (x x_1 : Finset α) ↦ Classical.dec ((fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ 𝒜
refine_1 : #(image s.erase s) ≤ #(bipartiteBelow (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (∂ 𝒜) s)
⊢ r ≤ #(bipartiteBelow (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (∂ 𝒜) s)

Tactic:
rw [← h𝒜 hs, ← card_image_of_injOn s.erase_injOn]

Premises used: Finset.erase_injOn, Finset.card_image_of_injOn
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
i : DecidableRel fun (x1 x2 : Finset α) ↦ x1 ⊆ x2 :=
  fun (x x_1 : Finset α) ↦ Classical.dec ((fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ #(image s.erase s) ≤ #(bipartiteBelow (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (∂ 𝒜) s)

Tactic:
card_le_card ?_

Premises used: Finset.card_le_card
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
i : DecidableRel fun (x1 x2 : Finset α) ↦ x1 ⊆ x2 :=
  fun (x x_1 : Finset α) ↦ Classical.dec ((fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ 𝒜
refine_1 : image s.erase s ⊆ bipartiteBelow (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (∂ 𝒜) s
⊢ #(image s.erase s) ≤ #(bipartiteBelow (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (∂ 𝒜) s)

Tactic:
refine card_le_card ?_

Premises used: Finset.card_le_card
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
i : DecidableRel fun (x1 x2 : Finset α) ↦ x1 ⊆ x2 :=
  fun (x x_1 : Finset α) ↦ Classical.dec ((fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ 𝒜
refine_1 : ∀ x ∈ s, s.erase x ∈ ∂ 𝒜 ∧ s.erase x ⊆ s
⊢ image s.erase s ⊆ bipartiteBelow (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (∂ 𝒜) s

Tactic:
simp_rw [image_subset_iff, mem_bipartiteBelow]

Premises used: Finset.image_subset_iff, Finset.mem_bipartiteBelow
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
i : DecidableRel fun (x1 x2 : Finset α) ↦ x1 ⊆ x2 :=
  fun (x x_1 : Finset α) ↦ Classical.dec ((fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ ∀ x ∈ s, s.erase x ∈ ∂ 𝒜 ∧ s.erase x ⊆ s

Tactic:
fun a ha => ⟨erase_mem_shadow hs ha, erase_subset _ _⟩

Premises used: Finset.erase_mem_shadow, And.intro, Finset.erase_subset
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
i : DecidableRel fun (x1 x2 : Finset α) ↦ x1 ⊆ x2 :=
  fun (x x_1 : Finset α) ↦ Classical.dec ((fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ ∀ x ∈ s, s.erase x ∈ ∂ 𝒜 ∧ s.erase x ⊆ s

Tactic:
exact fun a ha => ⟨erase_mem_shadow hs ha, erase_subset _ _⟩
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
i : DecidableRel fun (x1 x2 : Finset α) ↦ x1 ⊆ x2 :=
  fun (x x_1 : Finset α) ↦ Classical.dec ((fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
⊢ #(bipartiteAbove (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) 𝒜 s) ≤ Fintype.card α - r + 1

Tactic:
le_trans ?_ tsub_tsub_le_tsub_add

Premises used: tsub_tsub_le_tsub_add, le_trans
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
i : DecidableRel fun (x1 x2 : Finset α) ↦ x1 ⊆ x2 :=
  fun (x x_1 : Finset α) ↦ Classical.dec ((fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
refine_2 : #(bipartiteAbove (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) 𝒜 s) ≤ Fintype.card α - (r - 1)
⊢ #(bipartiteAbove (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) 𝒜 s) ≤ Fintype.card α - r + 1

Tactic:
refine le_trans ?_ tsub_tsub_le_tsub_add

Premises used: tsub_tsub_le_tsub_add, le_trans
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
i : DecidableRel fun (x1 x2 : Finset α) ↦ x1 ⊆ x2 :=
  fun (x x_1 : Finset α) ↦ Classical.dec ((fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
refine_2 :
  #(bipartiteAbove (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) 𝒜 s) ≤ card (α := Finset α) (image (fun (a : α) ↦ insert a s) sᶜ)
⊢ #(bipartiteAbove (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) 𝒜 s) ≤ Fintype.card α - (r - 1)

Tactic:
rw [← (Set.Sized.shadow h𝒜) hs, ← card_compl, ← card_image_of_injOn (insert_inj_on' _)]

Premises used: Finset.card_compl, Finset.card_image_of_injOn, Set.Sized.shadow, Finset.insert_inj_on'
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
i : DecidableRel fun (x1 x2 : Finset α) ↦ x1 ⊆ x2 :=
  fun (x x_1 : Finset α) ↦ Classical.dec ((fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
⊢ #(bipartiteAbove (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) 𝒜 s) ≤ card (α := Finset α) (image (fun (a : α) ↦ insert a s) sᶜ)

Tactic:
card_le_card fun t ht => ?_

Premises used: Finset.card_le_card
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
i : DecidableRel fun (x1 x2 : Finset α) ↦ x1 ⊆ x2 :=
  fun (x x_1 : Finset α) ↦ Classical.dec ((fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
refine_2 :
  ∀ (t : Finset α) (ht : t ∈ bipartiteAbove (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) 𝒜 s),
    Membership.mem (γ := Finset (Finset α)) (image (fun (a : α) ↦ insert a s) sᶜ) t
⊢ #(bipartiteAbove (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) 𝒜 s) ≤ card (α := Finset α) (image (fun (a : α) ↦ insert a s) sᶜ)

Tactic:
refine card_le_card fun t ht => ?_

Premises used: Finset.card_le_card
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
i : DecidableRel fun (x1 x2 : Finset α) ↦ x1 ⊆ x2 :=
  fun (x x_1 : Finset α) ↦ Classical.dec ((fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ bipartiteAbove (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) 𝒜 s
⊢ t ∈ 𝒜 ∧ s ⊆ t

Tactic:
rw [mem_bipartiteAbove] at ht

Premises used: Finset.mem_bipartiteAbove
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
i : DecidableRel fun (x1 x2 : Finset α) ↦ x1 ⊆ x2 :=
  fun (x x_1 : Finset α) ↦ Classical.dec ((fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
rw : ¬𝒜 = {∅}
⊢ ∅ ∉ 𝒜

Tactic:
rw [← mem_coe, h𝒜.empty_mem_iff, coe_eq_singleton]

Premises used: Finset.coe_eq_singleton, Set.Sized.empty_mem_iff, Finset.mem_coe
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
r : ℕ
i : DecidableRel fun (x1 x2 : Finset α) ↦ x1 ⊆ x2 :=
  fun (x x_1 : Finset α) ↦ Classical.dec ((fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) x x_1)
s t : Finset α
h𝒜 : Set.Sized r (↑{∅} : Set (Finset α))
hs : Membership.mem (γ := Finset (Finset α)) (∂ {∅}) s
ht : Membership.mem (γ := Finset (Finset α)) {∅} t ∧ s ⊆ t
⊢ Membership.mem (γ := Finset (Finset α)) ∅ s

Tactic:
rw [shadow_singleton_empty] at hs

Premises used: Finset.shadow_singleton_empty
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
r : ℕ
i : DecidableRel fun (x1 x2 : Finset α) ↦ x1 ⊆ x2 :=
  fun (x x_1 : Finset α) ↦ Classical.dec ((fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) x x_1)
s t : Finset α
h𝒜 : Set.Sized r (↑{∅} : Set (Finset α))
hs : Membership.mem (γ := Finset (Finset α)) (∂ {∅}) s
ht : Membership.mem (γ := Finset (Finset α)) {∅} t ∧ s ⊆ t
hs₁ : Membership.mem (γ := Finset (Finset α)) ∅ s
⊢ Membership.mem (γ := Finset (Finset α)) {∅} t ∧ s ⊆ t

Tactic:
rw [shadow_singleton_empty] at hs

Premises used: Finset.shadow_singleton_empty
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
r : ℕ
i : DecidableRel fun (x1 x2 : Finset α) ↦ x1 ⊆ x2 :=
  fun (x x_1 : Finset α) ↦ Classical.dec ((fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) x x_1)
s t : Finset α
h𝒜 : Set.Sized r (↑{∅} : Set (Finset α))
hs : Membership.mem (γ := Finset (Finset α)) ∅ s
ht : Membership.mem (γ := Finset (Finset α)) {∅} t ∧ s ⊆ t
⊢ False

Tactic:
notMem_empty s hs

Premises used: Finset.notMem_empty
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
r : ℕ
i : DecidableRel fun (x1 x2 : Finset α) ↦ x1 ⊆ x2 :=
  fun (x x_1 : Finset α) ↦ Classical.dec ((fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) x x_1)
s t : Finset α
h𝒜 : Set.Sized r (↑{∅} : Set (Finset α))
hs : Membership.mem (γ := Finset (Finset α)) ∅ s
ht : Membership.mem (γ := Finset (Finset α)) {∅} t ∧ s ⊆ t
⊢ False

Tactic:
exact notMem_empty s hs

Premises used: Finset.notMem_empty
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
i : DecidableRel fun (x1 x2 : Finset α) ↦ x1 ⊆ x2 :=
  fun (x x_1 : Finset α) ↦ Classical.dec ((fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
⊢ ∅ ∉ 𝒜

Tactic:
have : ∅ ∉ 𝒜 := by
    rw [← mem_coe, h𝒜.empty_mem_iff, coe_eq_singleton]
    rintro rfl
    rw [shadow_singleton_empty] at hs
    exact notMem_empty s hs
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
i : DecidableRel fun (x1 x2 : Finset α) ↦ x1 ⊆ x2 :=
  fun (x x_1 : Finset α) ↦ Classical.dec ((fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
this : ∅ ∉ 𝒜
rw : #s + 1 = r - 1 + 1
rw₁ rw₂ : r - 1 + 1 = r - 1 + 1
⊢ #s + 1 = #t

Tactic:
rw [(sized_shadow_iff this).1 (Set.Sized.shadow h𝒜) ht.1, (Set.Sized.shadow h𝒜) hs]

Premises used: And.left, Finset.sized_shadow_iff, Iff.mp, Set.Sized.shadow
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
i : DecidableRel fun (x1 x2 : Finset α) ↦ x1 ⊆ x2 :=
  fun (x x_1 : Finset α) ↦ Classical.dec ((fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
this : ∅ ∉ 𝒜
⊢ ∃ a ∉ s, insert a s = t

Tactic:
have h := exists_eq_insert_iff.2 ⟨ht.2, by
    rw [(sized_shadow_iff this).1 (Set.Sized.shadow h𝒜) ht.1, (Set.Sized.shadow h𝒜) hs]⟩