awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
⊢ LE.le.{u_1} (α := 𝕜) (∑ s ∈ 𝒜, (↑((Fintype.card α).choose #s) : 𝕜)⁻¹) 1
have _ : Eq.{u_1 + 1} (α := 𝕜) (∑ s ∈ 𝒜, (↑((Fintype.card α).choose #s) : 𝕜)⁻¹)
  (∑ r ∈ range (Fintype.card α + 1), ∑ s ∈ 𝒜 with #s = r, (↑((Fintype.card α).choose r) : 𝕜)⁻¹)
Tactic: calc
    _ = ∑ r ∈ range (Fintype.card α + 1),
        ∑ s ∈ 𝒜 with #s = r, ((Fintype.card α).choose r : 𝕜)⁻¹ := by
      rw [sum_fiberwise_of_maps_to']; simp [card_le_univ]
    _ = ∑ r ∈ range (Fintype.card α + 1), (#(𝒜 # r) / (Fintype.card α).choose r : 𝕜) := by
      simp [slice, div_eq_mul_inv]
    _ ≤ 1 := lubell_yamamoto_meshalkin_inequality_sum_card_div_choose h𝒜
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
_ :
  Eq.{u_1 + 1} (α := 𝕜) (∑ s ∈ 𝒜, (↑((Fintype.card α).choose #s) : 𝕜)⁻¹)
    (∑ r ∈ range (Fintype.card α + 1), ∑ s ∈ 𝒜 with #s = r, (↑((Fintype.card α).choose r) : 𝕜)⁻¹)
⊢ LE.le.{u_1} (α := 𝕜) (∑ s ∈ 𝒜, (↑((Fintype.card α).choose #s) : 𝕜)⁻¹) 1
have _₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ r ∈ range (Fintype.card α + 1), ∑ s ∈ 𝒜 with #s = r, (↑((Fintype.card α).choose r) : 𝕜)⁻¹)
  (∑ r ∈ range (Fintype.card α + 1), HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # r)) : 𝕜) (↑((Fintype.card α).choose r) : 𝕜))
Tactic: calc
    _ = ∑ r ∈ range (Fintype.card α + 1),
        ∑ s ∈ 𝒜 with #s = r, ((Fintype.card α).choose r : 𝕜)⁻¹ := by
      rw [sum_fiberwise_of_maps_to']; simp [card_le_univ]
    _ = ∑ r ∈ range (Fintype.card α + 1), (#(𝒜 # r) / (Fintype.card α).choose r : 𝕜) := by
      simp [slice, div_eq_mul_inv]
    _ ≤ 1 := lubell_yamamoto_meshalkin_inequality_sum_card_div_choose h𝒜
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (hypothesis)
Goal:
α : Type u_2
inst : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
⊢ #𝒜 ≤ (Fintype.card α).choose (Fintype.card α / 2)
have this : LT.lt (α := ℚ≥0) 0 (↑((Fintype.card α).choose (Fintype.card α / 2)) : ℚ≥0)
Tactic: have : 0 < ((Fintype.card α).choose (Fintype.card α / 2) : ℚ≥0) :=
    Nat.cast_pos.2 <| choose_pos (Nat.div_le_self _ _)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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)⁻¹)
    (∑ s ∈ 𝒜, (↑((Fintype.card α).choose #s) : ℚ≥0)⁻¹)
have h : ∀ (s : Finset α) (hs : s ∈ 𝒜), LT.lt (α := ℚ≥0) 0 (↑((Fintype.card α).choose #s) : ℚ≥0)
Tactic: gcongr with s hs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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 : ∀ (s : Finset α) (hs : s ∈ 𝒜), LT.lt (α := ℚ≥0) 0 (↑((Fintype.card α).choose #s) : ℚ≥0)
⊢ LE.le (α := ℚ≥0) (∑ s ∈ 𝒜, (↑((Fintype.card α).choose (Fintype.card α / 2)) : ℚ≥0)⁻¹)
    (∑ s ∈ 𝒜, (↑((Fintype.card α).choose #s) : ℚ≥0)⁻¹)
have h₁ : ∀ (s : Finset α) (hs : s ∈ 𝒜), (Fintype.card α).choose #s ≤ (Fintype.card α).choose (Fintype.card α / 2)
Tactic: gcongr with s hs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (hypothesis)
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)
⊢ #𝒜 ≤ (Fintype.card α).choose (Fintype.card α / 2)
have h : 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𝒜
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
k : ℕ
⊢ Eq.{u_1 + 1} (α := Finset (Finset α)) (∂^[k] ∅) ∅
have zero : Eq.{u_1 + 1} (α := Finset (Finset α)) (∂^[0] ∅) ∅
Tactic: induction k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
k : ℕ
zero : Eq.{u_1 + 1} (α := Finset (Finset α)) (∂^[0] ∅) ∅
⊢ Eq.{u_1 + 1} (α := Finset (Finset α)) (∂^[k] ∅) ∅
have succ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := Finset (Finset α)) (∂^[n] ∅) ∅ → Eq.{u_1 + 1} (α := Finset (Finset α)) (∂^[n + 1] ∅) ∅
Tactic: induction k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ ∂ 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = 1
have simp_rw : (∃ s ∈ 𝒜, ∃ a ∈ s, s.erase a = t) ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = 1
Tactic: simp_rw [mem_shadow_iff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_erase]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
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
⊢ t ∈ ∂ 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = 1
have simp_rw₁ : (∃ s ∈ 𝒜, ∃ a ∈ s, s.erase a = t) ↔ ∃ s ∈ 𝒜, t ⋖ s
Tactic: simp_rw [mem_shadow_iff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_erase]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ ∂ 𝒜 ↔ ∃ a ∉ t, insert a t ∈ 𝒜
have simp_rw : (∃ s ∈ 𝒜, ∃ a ∉ t, insert a t = s) ↔ ∃ a ∉ t, insert a t ∈ 𝒜
Tactic: simp_rw [mem_shadow_iff_exists_sdiff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_insert]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ ∂ 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #s = #t + 1
have refine : ∀ t_1 ∈ 𝒜, ∀ (hst : t ⊆ t_1), #(t_1 \ t) = 1 ↔ #t_1 = #t + 1
Tactic: refine mem_shadow_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 α
𝒜 : Finset (Finset α)
t_1 t : Finset α
h : t ∈ 𝒜
hst : t_1 ⊆ t
⊢ #(t \ t_1) = 1 ↔ #t = #t_1 + 1
have rw : #t_1 ≤ #t
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 α
𝒜 : Finset (Finset α)
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 ∈ 𝒜
have 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 ∈ 𝒜
Tactic: simp only [mem_shadow_iff_insert_mem, ih, Function.iterate_succ_apply', card_eq_succ]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ t ∈ ∂^[k] 𝒜 ↔ ∃ (u : Finset α), #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜
have zero : ∀ {t : Finset α}, t ∈ ∂^[0] 𝒜 ↔ ∃ (u : Finset α), #u = 0 ∧ 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
Cleared hypotheses: t, k
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
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 ∈ 𝒜
⊢ t ∈ ∂^[k] 𝒜 ↔ ∃ (u : Finset α), #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜
have 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 ∈ 𝒜
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
Cleared hypotheses: t, k
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ t ∈ ∂^[k] 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = k
have rw : (∃ (u : Finset α), #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜) ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = k
Tactic: rw [mem_shadow_iterate_iff_exists_card]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ (∃ (u : Finset α), #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜) ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = k
have mp : (∃ (u : Finset α), #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜) → ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = k
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
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
⊢ (∃ (u : Finset α), #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜) ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = k
have mpr : (∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = k) → ∃ (u : Finset α), #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
t u : Finset α
htu : Disjoint t u
hsuA : t ∪ u ∈ 𝒜
⊢ #((t ∪ u) \ t) = #u
have rw : #u = #u
Tactic: rw [union_sdiff_cancel_left htu]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
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 ∈ 𝒜
have mpr : t ∪ s \ t ∈ 𝒜
Tactic: refine ⟨s \ t, rfl, disjoint_sdiff, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
t s : Finset α
hs : s ∈ 𝒜
hts : t ⊆ s
⊢ t ∪ s \ t ∈ 𝒜
have mpr : t ∪ s ∈ 𝒜
Tactic: rwa [union_sdiff_self_eq_union, union_eq_right.2 hts]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ t ∈ ∂^[k] 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #s = #t + k
have refine : ∀ t_1 ∈ 𝒜, ∀ (hst : t ⊆ t_1), #(t_1 \ t) = k ↔ #t_1 = #t + k
Tactic: refine mem_shadow_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 α
𝒜 : Finset (Finset α)
t_1 : Finset α
k : ℕ
t : Finset α
h : t ∈ 𝒜
hst : t_1 ⊆ t
⊢ #(t \ t_1) = k ↔ #t = #t_1 + k
have rw : #t_1 ≤ #t
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 α
𝒜 : 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 : A.erase i ∈ (↑(∂ 𝒜) : Set (Finset α))), #(A.erase i) = r - 1
Tactic: obtain ⟨A, hA, i, hi, rfl⟩ := mem_shadow_iff.1 h
Cleared hypotheses: A, h
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
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 α))
⊢ #(A.erase i) = r - 1
have rw : #A - 1 = r - 1
Tactic: rw [card_erase_of_mem hi, h𝒜 hA]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
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
⊢ #(A.erase i) = r - 1
have rw₁ : r - 1 = r - 1
Tactic: rw [card_erase_of_mem hi, h𝒜 hA]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
k r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
⊢ Set.Sized (r - k) (↑(∂^[k] 𝒜) : Set (Finset α))
have simp_rw : ∀ ⦃x : Finset α⦄, (∃ s ∈ 𝒜, x ⊆ s ∧ #(s \ x) = k) → #x = r - k
Tactic: simp_rw [Set.Sized, mem_coe, mem_shadow_iterate_iff_exists_sdiff]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
t s : Finset α
hs : s ∈ 𝒜
hts : t ⊆ s
⊢ #t = r - #(s \ t)
have rw : #t = r - (#s - #t)
Tactic: rw [card_sdiff_of_subset hts, ← h𝒜 hs, Nat.sub_sub_self (card_le_card hts)]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
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)
⊢ #t = r - #(s \ t)
have rw₁ : #t = #s - (#s - #t)
Tactic: rw [card_sdiff_of_subset hts, ← h𝒜 hs, Nat.sub_sub_self (card_le_card hts)]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
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)
⊢ #t = r - #(s \ t)
have rw₂ : #t = #t
Tactic: rw [card_sdiff_of_subset hts, ← h𝒜 hs, Nat.sub_sub_self (card_le_card hts)]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h : ∅ ∉ 𝒜
⊢ Set.Sized r (↑(∂ 𝒜) : Set (Finset α)) ↔ Set.Sized (r + 1) (↑𝒜 : Set (Finset α))
have refine : ∀ (h𝒜 : Set.Sized r (↑(∂ 𝒜) : Set (Finset α))) (s : Finset α) (hs : s ∈ (↑𝒜 : Set (Finset α))), #s = r + 1
Tactic: refine ⟨fun h𝒜 s hs => ?_, Set.Sized.shadow⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h : ∅ ∉ 𝒜
h𝒜 : Set.Sized r (↑(∂ 𝒜) : Set (Finset α))
s : Finset α
hs : s ∈ (↑𝒜 : Set (Finset α))
⊢ #s = r + 1
have obtain : ∀ (a : α) (ha : a ∈ s), #s = r + 1
Tactic: obtain ⟨a, ha⟩ := nonempty_iff_ne_empty.2 (ne_of_mem_of_not_mem hs h)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
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
⊢ #s = r + 1
have rw : #s = #(s.erase a) + 1
Tactic: rw [← h𝒜 (erase_mem_shadow hs ha), card_erase_add_one ha]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
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
⊢ #s = r + 1
have rw₁ : #s = #s
Tactic: rw [← h𝒜 (erase_mem_shadow hs ha), card_erase_add_one ha]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, ∃ a ∉ s, insert a s = t
have 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
Tactic: simp_rw [upShadow, mem_sup, mem_image, mem_compl]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
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
⊢ t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, ∃ a ∉ s, insert a s = t
have simp_rw₁ : (∃ i ∈ 𝒜, Membership.mem (γ := Finset (Finset α)) (image (fun (a : α) ↦ insert a i) iᶜ) t) ↔
  ∃ s ∈ 𝒜, ∃ a ∉ s, insert a s = t
Tactic: simp_rw [upShadow, mem_sup, mem_image, mem_compl]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
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
⊢ t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, ∃ a ∉ s, insert a s = t
have simp_rw₂ : (∃ i ∈ 𝒜, ∃ a ∈ iᶜ, insert a i = t) ↔ ∃ s ∈ 𝒜, ∃ a ∉ s, insert a s = t
Tactic: simp_rw [upShadow, mem_sup, mem_image, mem_compl]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = 1
have simp_rw : (∃ s ∈ 𝒜, ∃ a ∉ s, insert a s = t) ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = 1
Tactic: simp_rw [mem_upShadow_iff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_insert]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
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
⊢ t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = 1
have simp_rw₁ : (∃ s ∈ 𝒜, ∃ a ∉ s, insert a s = t) ↔ ∃ s ∈ 𝒜, s ⋖ t
Tactic: simp_rw [mem_upShadow_iff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_insert]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ ∂⁺ 𝒜 ↔ ∃ a ∈ t, t.erase a ∈ 𝒜
have simp_rw : (∃ s ∈ 𝒜, ∃ a ∈ t, t.erase a = s) ↔ ∃ a ∈ t, t.erase a ∈ 𝒜
Tactic: simp_rw [mem_upShadow_iff_exists_sdiff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_erase]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #t = #s + 1
have refine : ∀ t_1 ∈ 𝒜, ∀ (hst : t_1 ⊆ t), #(t \ t_1) = 1 ↔ #t = #t_1 + 1
Tactic: refine mem_upShadow_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 t : Finset α
h : t ∈ 𝒜
hst : t ⊆ t_1
⊢ #(t_1 \ t) = 1 ↔ #t_1 = #t + 1
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 α)
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 ∈ 𝒜
have 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 ∈ 𝒜
Tactic: simp only [mem_upShadow_iff_erase_mem, ih, Function.iterate_succ_apply', card_eq_succ,
      subset_erase, erase_sdiff_comm, ← sdiff_insert]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
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 α
⊢ (∃ 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 ∈ 𝒜
have 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 ∈ 𝒜
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
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 ∈ 𝒜
⊢ (∃ 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 ∈ 𝒜
have 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 ∈ 𝒜
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (hypothesis)
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_1 : Finset α), #u_1 = #u ∧ (u_1 ⊆ t ∧ a ∉ u_1) ∧ t \ insert a u_1 ∈ 𝒜
have hut₁ : a ∈ t ∧ u ⊆ t
Tactic: rw [insert_subset_iff] at hut
Cleared hypotheses: hut, htu
-- 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] 𝒜 ↔ ∃ (u : Finset α), #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜
have zero : ∀ {t : Finset α}, t ∈ ∂⁺ ^[0] 𝒜 ↔ ∃ (u : Finset α), #u = 0 ∧ 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⟩
Cleared hypotheses: t, k
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Shadow (goal)
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 ∈ 𝒜
⊢ t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ (u : Finset α), #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜
have 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 ∈ 𝒜
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⟩
Cleared hypotheses: t, k
-- 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 rw : (∃ (u : Finset α), #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜) ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = k
Tactic: rw [mem_upShadow_iterate_iff_exists_card]