awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.HarrisKleitman (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)} (h𝒜 : IsLowerSet (↑𝒜 : Set (Finset α))) (hℬ : IsLowerSet (↑ℬ : Set (Finset α)))
    (h𝒜s : ∀ t ∈ 𝒜, t ⊆ s) (hℬs : ∀ t ∈ ℬ, t ⊆ s), #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet (↑𝒜 : Set (Finset α))
hℬ : IsLowerSet (↑ℬ : Set (Finset α))
h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ insert a s
h₀ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.nonMemberSubfamily a 𝒞, t ⊆ s
h₁ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.memberSubfamily a 𝒞, t ⊆ s
⊢ #(Finset.memberSubfamily a 𝒜) * #(Finset.memberSubfamily a ℬ) +
      #(Finset.nonMemberSubfamily a 𝒜) * #(Finset.nonMemberSubfamily a ℬ) ≤
    HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
have insert : HPow.hPow (α := ℕ) 2 #s * #(Finset.memberSubfamily a 𝒜 ∩ Finset.memberSubfamily a ℬ) +
    HPow.hPow (α := ℕ) 2 #s * #(Finset.nonMemberSubfamily a 𝒜 ∩ Finset.nonMemberSubfamily a ℬ) =
  HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
Tactic: refine (add_le_add (ih h𝒜.memberSubfamily hℬ.memberSubfamily (h₁ _ h𝒜s) <| h₁ _ hℬs) <|
    ih h𝒜.nonMemberSubfamily hℬ.nonMemberSubfamily (h₀ _ h𝒜s) <| h₀ _ hℬs).trans_eq ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.HarrisKleitman (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)} (h𝒜 : IsLowerSet (↑𝒜 : Set (Finset α))) (hℬ : IsLowerSet (↑ℬ : Set (Finset α)))
    (h𝒜s : ∀ t ∈ 𝒜, t ⊆ s) (hℬs : ∀ t ∈ ℬ, t ⊆ s), #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet (↑𝒜 : Set (Finset α))
hℬ : IsLowerSet (↑ℬ : Set (Finset α))
h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ insert a s
h₀ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.nonMemberSubfamily a 𝒞, t ⊆ s
h₁ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.memberSubfamily a 𝒞, t ⊆ s
⊢ HPow.hPow (α := ℕ) 2 #s * #(Finset.memberSubfamily a 𝒜 ∩ Finset.memberSubfamily a ℬ) +
      HPow.hPow (α := ℕ) 2 #s * #(Finset.nonMemberSubfamily a 𝒜 ∩ Finset.nonMemberSubfamily a ℬ) =
    HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
have insert : HPow.hPow (α := ℕ) 2 #s *
    (#(Finset.memberSubfamily a 𝒜 ∩ Finset.memberSubfamily a ℬ) +
      #(Finset.nonMemberSubfamily a 𝒜 ∩ Finset.nonMemberSubfamily a ℬ)) =
  HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
Tactic: rw [← mul_add, ← memberSubfamily_inter, ← nonMemberSubfamily_inter,
    card_memberSubfamily_add_card_nonMemberSubfamily]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.HarrisKleitman (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)} (h𝒜 : IsLowerSet (↑𝒜 : Set (Finset α))) (hℬ : IsLowerSet (↑ℬ : Set (Finset α)))
    (h𝒜s : ∀ t ∈ 𝒜, t ⊆ s) (hℬs : ∀ t ∈ ℬ, t ⊆ s), #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet (↑𝒜 : Set (Finset α))
hℬ : IsLowerSet (↑ℬ : Set (Finset α))
h𝒜s : ∀ t ∈ 𝒜, t ⊆ Insert.insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ Insert.insert a s
h₀ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ Insert.insert a s) → ∀ t ∈ Finset.nonMemberSubfamily a 𝒞, t ⊆ s
h₁ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ Insert.insert a s) → ∀ t ∈ Finset.memberSubfamily a 𝒞, t ⊆ s
insert :
  HPow.hPow (α := ℕ) 2 #s *
      (#(Finset.memberSubfamily a 𝒜 ∩ Finset.memberSubfamily a ℬ) +
        #(Finset.nonMemberSubfamily a 𝒜 ∩ Finset.nonMemberSubfamily a ℬ)) =
    HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
⊢ HPow.hPow (α := ℕ) 2 #s * #(Finset.memberSubfamily a 𝒜 ∩ Finset.memberSubfamily a ℬ) +
      HPow.hPow (α := ℕ) 2 #s * #(Finset.nonMemberSubfamily a 𝒜 ∩ Finset.nonMemberSubfamily a ℬ) =
    HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
have insert₁ : HPow.hPow (α := ℕ) 2 #s *
    (#(Finset.memberSubfamily a (𝒜 ∩ ℬ)) + #(Finset.nonMemberSubfamily a 𝒜 ∩ Finset.nonMemberSubfamily a ℬ)) =
  HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
Tactic: rw [← mul_add, ← memberSubfamily_inter, ← nonMemberSubfamily_inter,
    card_memberSubfamily_add_card_nonMemberSubfamily]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.HarrisKleitman (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)} (h𝒜 : IsLowerSet (↑𝒜 : Set (Finset α))) (hℬ : IsLowerSet (↑ℬ : Set (Finset α)))
    (h𝒜s : ∀ t ∈ 𝒜, t ⊆ s) (hℬs : ∀ t ∈ ℬ, t ⊆ s), #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet (↑𝒜 : Set (Finset α))
hℬ : IsLowerSet (↑ℬ : Set (Finset α))
h𝒜s : ∀ t ∈ 𝒜, t ⊆ Insert.insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ Insert.insert a s
h₀ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ Insert.insert a s) → ∀ t ∈ Finset.nonMemberSubfamily a 𝒞, t ⊆ s
h₁ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ Insert.insert a s) → ∀ t ∈ Finset.memberSubfamily a 𝒞, t ⊆ s
insert :
  HPow.hPow (α := ℕ) 2 #s *
      (#(Finset.memberSubfamily a 𝒜 ∩ Finset.memberSubfamily a ℬ) +
        #(Finset.nonMemberSubfamily a 𝒜 ∩ Finset.nonMemberSubfamily a ℬ)) =
    HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
insert₁ :
  HPow.hPow (α := ℕ) 2 #s *
      (#(Finset.memberSubfamily a (𝒜 ∩ ℬ)) + #(Finset.nonMemberSubfamily a 𝒜 ∩ Finset.nonMemberSubfamily a ℬ)) =
    HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
⊢ HPow.hPow (α := ℕ) 2 #s * #(Finset.memberSubfamily a 𝒜 ∩ Finset.memberSubfamily a ℬ) +
      HPow.hPow (α := ℕ) 2 #s * #(Finset.nonMemberSubfamily a 𝒜 ∩ Finset.nonMemberSubfamily a ℬ) =
    HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
have insert₂ : HPow.hPow (α := ℕ) 2 #s * (#(Finset.memberSubfamily a (𝒜 ∩ ℬ)) + #(Finset.nonMemberSubfamily a (𝒜 ∩ ℬ))) =
  HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
Tactic: rw [← mul_add, ← memberSubfamily_inter, ← nonMemberSubfamily_inter,
    card_memberSubfamily_add_card_nonMemberSubfamily]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.HarrisKleitman (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)} (h𝒜 : IsLowerSet (↑𝒜 : Set (Finset α))) (hℬ : IsLowerSet (↑ℬ : Set (Finset α)))
    (h𝒜s : ∀ t ∈ 𝒜, t ⊆ s) (hℬs : ∀ t ∈ ℬ, t ⊆ s), #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet (↑𝒜 : Set (Finset α))
hℬ : IsLowerSet (↑ℬ : Set (Finset α))
h𝒜s : ∀ t ∈ 𝒜, t ⊆ Insert.insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ Insert.insert a s
h₀ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ Insert.insert a s) → ∀ t ∈ Finset.nonMemberSubfamily a 𝒞, t ⊆ s
h₁ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ Insert.insert a s) → ∀ t ∈ Finset.memberSubfamily a 𝒞, t ⊆ s
insert :
  HPow.hPow (α := ℕ) 2 #s *
      (#(Finset.memberSubfamily a 𝒜 ∩ Finset.memberSubfamily a ℬ) +
        #(Finset.nonMemberSubfamily a 𝒜 ∩ Finset.nonMemberSubfamily a ℬ)) =
    HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
insert₁ :
  HPow.hPow (α := ℕ) 2 #s *
      (#(Finset.memberSubfamily a (𝒜 ∩ ℬ)) + #(Finset.nonMemberSubfamily a 𝒜 ∩ Finset.nonMemberSubfamily a ℬ)) =
    HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
insert₂ :
  HPow.hPow (α := ℕ) 2 #s * (#(Finset.memberSubfamily a (𝒜 ∩ ℬ)) + #(Finset.nonMemberSubfamily a (𝒜 ∩ ℬ))) =
    HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
⊢ HPow.hPow (α := ℕ) 2 #s * #(Finset.memberSubfamily a 𝒜 ∩ Finset.memberSubfamily a ℬ) +
      HPow.hPow (α := ℕ) 2 #s * #(Finset.nonMemberSubfamily a 𝒜 ∩ Finset.nonMemberSubfamily a ℬ) =
    HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
have insert₃ : HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ) = HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
Tactic: rw [← mul_add, ← memberSubfamily_inter, ← nonMemberSubfamily_inter,
    card_memberSubfamily_add_card_nonMemberSubfamily]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.HarrisKleitman (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : IsLowerSet (↑𝒜 : Set (Finset α))
hℬ : IsLowerSet (↑ℬ : Set (Finset α))
h𝒜s : ∀ t ∈ 𝒜, t ⊆ s
hℬs : ∀ t ∈ ℬ, t ⊆ s
⊢ #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
have empty : ∀ {𝒜 ℬ : Finset (Finset α)} (h𝒜 : IsLowerSet (↑𝒜 : Set (Finset α))) (hℬ : IsLowerSet (↑ℬ : Set (Finset α)))
  (h𝒜s : ∀ t ∈ 𝒜, t ⊆ ∅) (hℬs : ∀ t ∈ ℬ, t ⊆ ∅), #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 (card.{u_1} (α := α) ∅) * #(𝒜 ∩ ℬ)
Tactic: induction s using Finset.induction generalizing 𝒜 ℬ with
  | empty =>
    simp_rw [subset_empty, ← subset_singleton_iff', subset_singleton_iff] at h𝒜s hℬs
    obtain rfl | rfl := h𝒜s
    · simp only [card_empty, zero_mul, empty_inter, mul_zero, le_refl]
    obtain rfl | rfl := hℬs
    · simp
    · simp only [card_empty, pow_zero, inter_singleton_of_mem, mem_singleton, card_singleton,
        le_refl]
  | insert a s hs ih =>
  rw [card_insert_of_notMem hs, ← card_memberSubfamily_add_card_nonMemberSubfamily a 𝒜, ←
    card_memberSubfamily_add_card_nonMemberSubfamily a ℬ, add_mul, mul_add, mul_add,
    add_comm (_ * _), add_add_add_comm]
  grw [mul_add_mul_le_mul_add_mul
    (card_le_card h𝒜.memberSubfamily_subset_nonMemberSubfamily) <|
      card_le_card hℬ.memberSubfamily_subset_nonMemberSubfamily, ← two_mul, pow_succ', mul_assoc]
  have h₀ : ∀ 𝒞 : Finset (Finset α), (∀ t ∈ 𝒞, t ⊆ insert a s) →
      ∀ t ∈ 𝒞.nonMemberSubfamily a, t ⊆ s := by
    rintro 𝒞 h𝒞 t ht
    rw [mem_nonMemberSubfamily] at ht
    exact (subset_insert_iff_of_notMem ht.2).1 (h𝒞 _ ht.1)
  have h₁ : ∀ 𝒞 : Finset (Finset α), (∀ t ∈ 𝒞, t ⊆ insert a s) →
      ∀ t ∈ 𝒞.memberSubfamily a, t ⊆ s := by
    rintro 𝒞 h𝒞 t ht
    rw [mem_memberSubfamily] at ht
    exact (subset_insert_iff_of_notMem ht.2).1 ((subset_insert _ _).trans <| h𝒞 _ ht.1)
  gcongr
  refine (add_le_add (ih h𝒜.memberSubfamily hℬ.memberSubfamily (h₁ _ h𝒜s) <| h₁ _ hℬs) <|
    ih h𝒜.nonMemberSubfamily hℬ.nonMemberSubfamily (h₀ _ h𝒜s) <| h₀ _ hℬs).trans_eq ?_
  rw [← mul_add, ← memberSubfamily_inter, ← nonMemberSubfamily_inter,
    card_memberSubfamily_add_card_nonMemberSubfamily]
Cleared hypotheses: 𝒜, ℬ, s, h𝒜, hℬ, h𝒜s, hℬs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.HarrisKleitman (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : IsLowerSet (↑𝒜 : Set (Finset α))
hℬ : IsLowerSet (↑ℬ : Set (Finset α))
h𝒜s : ∀ t ∈ 𝒜, t ⊆ s
hℬs : ∀ t ∈ ℬ, t ⊆ s
empty :
  ∀ {𝒜 ℬ : Finset (Finset α)} (h𝒜 : IsLowerSet (↑𝒜 : Set (Finset α))) (hℬ : IsLowerSet (↑ℬ : Set (Finset α)))
    (h𝒜s : ∀ t ∈ 𝒜, t ⊆ ∅) (hℬs : ∀ t ∈ ℬ, t ⊆ ∅), #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 (card.{u_1} (α := α) ∅) * #(𝒜 ∩ ℬ)
⊢ #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
have insert : ∀ (a : α) (s : Finset α) (hs : a ∉ s)
  (ih :
    ∀ {𝒜 ℬ : Finset (Finset α)} (h𝒜 : IsLowerSet (↑𝒜 : Set (Finset α))) (hℬ : IsLowerSet (↑ℬ : Set (Finset α)))
      (h𝒜s : ∀ t ∈ 𝒜, t ⊆ s) (hℬs : ∀ t ∈ ℬ, t ⊆ s), #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ))
  {𝒜 ℬ : Finset (Finset α)} (h𝒜 : IsLowerSet (↑𝒜 : Set (Finset α))) (hℬ : IsLowerSet (↑ℬ : Set (Finset α)))
  (h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s) (hℬs : ∀ t ∈ ℬ, t ⊆ insert a s),
  #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 #(insert a s) * #(𝒜 ∩ ℬ)
Tactic: induction s using Finset.induction generalizing 𝒜 ℬ with
  | empty =>
    simp_rw [subset_empty, ← subset_singleton_iff', subset_singleton_iff] at h𝒜s hℬs
    obtain rfl | rfl := h𝒜s
    · simp only [card_empty, zero_mul, empty_inter, mul_zero, le_refl]
    obtain rfl | rfl := hℬs
    · simp
    · simp only [card_empty, pow_zero, inter_singleton_of_mem, mem_singleton, card_singleton,
        le_refl]
  | insert a s hs ih =>
  rw [card_insert_of_notMem hs, ← card_memberSubfamily_add_card_nonMemberSubfamily a 𝒜, ←
    card_memberSubfamily_add_card_nonMemberSubfamily a ℬ, add_mul, mul_add, mul_add,
    add_comm (_ * _), add_add_add_comm]
  grw [mul_add_mul_le_mul_add_mul
    (card_le_card h𝒜.memberSubfamily_subset_nonMemberSubfamily) <|
      card_le_card hℬ.memberSubfamily_subset_nonMemberSubfamily, ← two_mul, pow_succ', mul_assoc]
  have h₀ : ∀ 𝒞 : Finset (Finset α), (∀ t ∈ 𝒞, t ⊆ insert a s) →
      ∀ t ∈ 𝒞.nonMemberSubfamily a, t ⊆ s := by
    rintro 𝒞 h𝒞 t ht
    rw [mem_nonMemberSubfamily] at ht
    exact (subset_insert_iff_of_notMem ht.2).1 (h𝒞 _ ht.1)
  have h₁ : ∀ 𝒞 : Finset (Finset α), (∀ t ∈ 𝒞, t ⊆ insert a s) →
      ∀ t ∈ 𝒞.memberSubfamily a, t ⊆ s := by
    rintro 𝒞 h𝒞 t ht
    rw [mem_memberSubfamily] at ht
    exact (subset_insert_iff_of_notMem ht.2).1 ((subset_insert _ _).trans <| h𝒞 _ ht.1)
  gcongr
  refine (add_le_add (ih h𝒜.memberSubfamily hℬ.memberSubfamily (h₁ _ h𝒜s) <| h₁ _ hℬs) <|
    ih h𝒜.nonMemberSubfamily hℬ.nonMemberSubfamily (h₀ _ h𝒜s) <| h₀ _ hℬs).trans_eq ?_
  rw [← mul_add, ← memberSubfamily_inter, ← nonMemberSubfamily_inter,
    card_memberSubfamily_add_card_nonMemberSubfamily]
Cleared hypotheses: 𝒜, ℬ, s, h𝒜, hℬ, h𝒜s, hℬs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.HarrisKleitman (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst_1 : Fintype α
h𝒜 : IsUpperSet (↑𝒜 : Set (Finset α))
hℬ : IsLowerSet (↑ℬ : Set (Finset α))
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
have h𝒜₁ : IsLowerSet (↑𝒜ᶜ : Set (Finset α))
Tactic: rw [← isLowerSet_compl, ← coe_compl] at h𝒜
Cleared hypotheses: h𝒜, hℬ
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.HarrisKleitman (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst_1 : Fintype α
h𝒜 : IsLowerSet (↑𝒜ᶜ : Set (Finset α))
hℬ : IsLowerSet (↑ℬ : Set (Finset α))
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
have this : #𝒜ᶜ * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)
Tactic: have := h𝒜.le_card_inter_finset hℬ
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.HarrisKleitman (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst_1 : Fintype α
h𝒜 : IsLowerSet (↑𝒜ᶜ : Set (Finset α))
hℬ : IsLowerSet (↑ℬ : Set (Finset α))
this : #𝒜ᶜ * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
have rwa : ∀ (this : (Fintype.card.{u_1} (Finset α) - #𝒜) * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)),
  HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
Tactic: rwa [card_compl, Fintype.card_finset, tsub_mul, tsub_le_iff_tsub_le, ← mul_tsub, ←
    card_sdiff_of_subset inter_subset_right, sdiff_inter_self_right, sdiff_compl,
    _root_.inf_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.HarrisKleitman (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst_1 : Fintype α
h𝒜 : IsLowerSet (↑𝒜ᶜ : Set (Finset α))
hℬ : IsLowerSet (↑ℬ : Set (Finset α))
this : #𝒜ᶜ * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)
rwa :
  ∀ (this : (Fintype.card.{u_1} (Finset α) - #𝒜) * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
have rwa₁ : ∀ (this : (HPow.hPow (α := ℕ) 2 (Fintype.card α) - #𝒜) * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)),
  HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
Tactic: rwa [card_compl, Fintype.card_finset, tsub_mul, tsub_le_iff_tsub_le, ← mul_tsub, ←
    card_sdiff_of_subset inter_subset_right, sdiff_inter_self_right, sdiff_compl,
    _root_.inf_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.HarrisKleitman (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst_1 : Fintype α
h𝒜 : IsLowerSet (↑𝒜ᶜ : Set (Finset α))
hℬ : IsLowerSet (↑ℬ : Set (Finset α))
this : #𝒜ᶜ * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)
rwa :
  ∀ (this : (Fintype.card.{u_1} (Finset α) - #𝒜) * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
rwa₁ :
  ∀ (this : (HPow.hPow (α := ℕ) 2 (Fintype.card α) - #𝒜) * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
have rwa₂ : ∀ (this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ - #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)),
  HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
Tactic: rwa [card_compl, Fintype.card_finset, tsub_mul, tsub_le_iff_tsub_le, ← mul_tsub, ←
    card_sdiff_of_subset inter_subset_right, sdiff_inter_self_right, sdiff_compl,
    _root_.inf_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.HarrisKleitman (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst_1 : Fintype α
h𝒜 : IsLowerSet (↑𝒜ᶜ : Set (Finset α))
hℬ : IsLowerSet (↑ℬ : Set (Finset α))
this : #𝒜ᶜ * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)
rwa :
  ∀ (this : (Fintype.card.{u_1} (Finset α) - #𝒜) * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
rwa₁ :
  ∀ (this : (HPow.hPow (α := ℕ) 2 (Fintype.card α) - #𝒜) * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
rwa₂ :
  ∀ (this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ - #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
have rwa₃ : ∀ (this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ - HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ) ≤ #𝒜 * #ℬ),
  HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
Tactic: rwa [card_compl, Fintype.card_finset, tsub_mul, tsub_le_iff_tsub_le, ← mul_tsub, ←
    card_sdiff_of_subset inter_subset_right, sdiff_inter_self_right, sdiff_compl,
    _root_.inf_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.HarrisKleitman (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst_1 : Fintype α
h𝒜 : IsLowerSet (↑𝒜ᶜ : Set (Finset α))
hℬ : IsLowerSet (↑ℬ : Set (Finset α))
this : #𝒜ᶜ * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)
rwa :
  ∀ (this : (Fintype.card.{u_1} (Finset α) - #𝒜) * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
rwa₁ :
  ∀ (this : (HPow.hPow (α := ℕ) 2 (Fintype.card α) - #𝒜) * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
rwa₂ :
  ∀ (this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ - #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
rwa₃ :
  ∀ (this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ - HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ) ≤ #𝒜 * #ℬ),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
have rwa₄ : ∀ (this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * (#ℬ - #(𝒜ᶜ ∩ ℬ)) ≤ #𝒜 * #ℬ),
  HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
Tactic: rwa [card_compl, Fintype.card_finset, tsub_mul, tsub_le_iff_tsub_le, ← mul_tsub, ←
    card_sdiff_of_subset inter_subset_right, sdiff_inter_self_right, sdiff_compl,
    _root_.inf_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.HarrisKleitman (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst_1 : Fintype α
h𝒜 : IsLowerSet (↑𝒜ᶜ : Set (Finset α))
hℬ : IsLowerSet (↑ℬ : Set (Finset α))
this : #𝒜ᶜ * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)
rwa :
  ∀ (this : (Fintype.card.{u_1} (Finset α) - #𝒜) * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
rwa₁ :
  ∀ (this : (HPow.hPow (α := ℕ) 2 (Fintype.card α) - #𝒜) * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
rwa₂ :
  ∀ (this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ - #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
rwa₃ :
  ∀ (this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ - HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ) ≤ #𝒜 * #ℬ),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
rwa₄ :
  ∀ (this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * (#ℬ - #(𝒜ᶜ ∩ ℬ)) ≤ #𝒜 * #ℬ),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
have rwa₅ : ∀ (this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(ℬ \ (𝒜ᶜ ∩ ℬ)) ≤ #𝒜 * #ℬ),
  HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
Tactic: rwa [card_compl, Fintype.card_finset, tsub_mul, tsub_le_iff_tsub_le, ← mul_tsub, ←
    card_sdiff_of_subset inter_subset_right, sdiff_inter_self_right, sdiff_compl,
    _root_.inf_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.HarrisKleitman (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst_1 : Fintype α
h𝒜 : IsLowerSet (↑𝒜ᶜ : Set (Finset α))
hℬ : IsLowerSet (↑ℬ : Set (Finset α))
this : #𝒜ᶜ * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)
rwa :
  ∀ (this : (Fintype.card.{u_1} (Finset α) - #𝒜) * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
rwa₁ :
  ∀ (this : (HPow.hPow (α := ℕ) 2 (Fintype.card α) - #𝒜) * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
rwa₂ :
  ∀ (this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ - #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
rwa₃ :
  ∀ (this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ - HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ) ≤ #𝒜 * #ℬ),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
rwa₄ :
  ∀ (this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * (#ℬ - #(𝒜ᶜ ∩ ℬ)) ≤ #𝒜 * #ℬ),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
rwa₅ :
  ∀ (this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(ℬ \ (𝒜ᶜ ∩ ℬ)) ≤ #𝒜 * #ℬ),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
have rwa₆ : ∀ (this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(ℬ \ 𝒜ᶜ) ≤ #𝒜 * #ℬ),
  HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
Tactic: rwa [card_compl, Fintype.card_finset, tsub_mul, tsub_le_iff_tsub_le, ← mul_tsub, ←
    card_sdiff_of_subset inter_subset_right, sdiff_inter_self_right, sdiff_compl,
    _root_.inf_comm] at this
Cleared hypotheses: this