awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s_1 t_1 s t : Finset α
simp_rw :
  Eq (α := Finset (Booleanisation α))
    (image (⇑{ toFun := (⇑liftLatticeHom : (a : α) → Booleanisation α), inj' := ⋯ } : (a : α) → Booleanisation α)
      (s \\ t))
    (image (⇑{ toFun := (⇑liftLatticeHom : (a : α) → Booleanisation α), inj' := ⋯ } : (a : α) → Booleanisation α) s \\
      image (⇑{ toFun := (⇑liftLatticeHom : (a : α) → Booleanisation α), inj' := ⋯ } : (a : α) → Booleanisation α) t)
⊢ map { toFun := (⇑liftLatticeHom : (a : α) → Booleanisation α), inj' := ⋯ : α ↪ Booleanisation α } (s \\ t) =
    map { toFun := (⇑liftLatticeHom : (a : α) → Booleanisation α), inj' := ⋯ } s \\
      map { toFun := (⇑liftLatticeHom : (a : α) → Booleanisation α), inj' := ⋯ } t

Tactic:
simp_rw [map_eq_image]

Premises used: Finset.map_eq_image
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s_1 t_1 s t : Finset α
⊢ Eq (α := Finset (Booleanisation α))
    (image (⇑{ toFun := (⇑liftLatticeHom : (a : α) → Booleanisation α), inj' := ⋯ } : (a : α) → Booleanisation α)
      (s \\ t))
    (image (⇑{ toFun := (⇑liftLatticeHom : (a : α) → Booleanisation α), inj' := ⋯ } : (a : α) → Booleanisation α) s \\
      image (⇑{ toFun := (⇑liftLatticeHom : (a : α) → Booleanisation α), inj' := ⋯ } : (a : α) → Booleanisation α) t)

Tactic:
image_image₂_distrib fun a b ↦ rfl

Premises used: Finset.diffs, rfl, Finset.image_image₂_distrib
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s_1 t_1 s t : Finset α
⊢ Eq (α := Finset (Booleanisation α))
    (image (⇑{ toFun := (⇑liftLatticeHom : (a : α) → Booleanisation α), inj' := ⋯ } : (a : α) → Booleanisation α)
      (s \\ t))
    (image (⇑{ toFun := (⇑liftLatticeHom : (a : α) → Booleanisation α), inj' := ⋯ } : (a : α) → Booleanisation α) s \\
      image (⇑{ toFun := (⇑liftLatticeHom : (a : α) → Booleanisation α), inj' := ⋯ } : (a : α) → Booleanisation α) t)

Tactic:
exact image_image₂_distrib fun a b ↦ rfl

Premises used: rfl, Finset.image_image₂_distrib
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s t : Finset α
⊢ ∀ (s t : Finset α),
    map { toFun := (⇑liftLatticeHom : (a : α) → Booleanisation α), inj' := ⋯ : α ↪ Booleanisation α } (s \\ t) =
      map { toFun := (⇑liftLatticeHom : (a : α) → Booleanisation α), inj' := ⋯ } s \\
        map { toFun := (⇑liftLatticeHom : (a : α) → Booleanisation α), inj' := ⋯ } t

Tactic:
have : ∀ s t : Finset α, (s \\ t).map ⟨_, liftLatticeHom_injective⟩ =
      s.map ⟨_, liftLatticeHom_injective⟩ \\ t.map ⟨_, liftLatticeHom_injective⟩ := by
    rintro s t
    simp_rw [map_eq_image]
    exact image_image₂_distrib fun a b ↦ rfl
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s t : Finset α
this :
  ∀ (s t : Finset α),
    map { toFun := (⇑liftLatticeHom : (a : α) → Booleanisation α), inj' := ⋯ : α ↪ Booleanisation α } (s \\ t) =
      map { toFun := (⇑liftLatticeHom : (a : α) → Booleanisation α), inj' := ⋯ } s \\
        map { toFun := (⇑liftLatticeHom : (a : α) → Booleanisation α), inj' := ⋯ } t
⊢ #s * #t ≤ #(s \\ t) * #(t \\ s)

Tactic:
simpa [← card_compls (_ ⊻ _), ← map_sup, ← map_inf, ← this] using
    (s.map ⟨_, liftLatticeHom_injective⟩).le_card_infs_mul_card_sups
      (t.map ⟨_, liftLatticeHom_injective⟩)ᶜˢ

Premises used: Finset.card_compls, Finset.compls, Finset.map, Function.Embedding.mk, InfHomClass.map_inf, Booleanisation.liftLatticeHom_injective, Finset.le_card_infs_mul_card_sups, SupHomClass.map_sup, HasSups.sups
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s : Finset α
⊢ HPow.hPow (β := ℕ) (#s) 2 ≤ HPow.hPow (β := ℕ) (#(s \\ s)) 2

Tactic:
simpa [← sq] using s.le_card_diffs_mul_card_diffs s

Premises used: sq, Finset.le_card_diffs_mul_card_diffs
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : IsLowerSet (↑𝒜 : Set (Finset α))
s t : Finset α
hts : t ≤ s
simp_rw : s ∈ 𝒜 ∧ a ∉ s → t ∈ 𝒜 ∧ a ∉ t
⊢ s ∈ (↑(Finset.nonMemberSubfamily a 𝒜) : Set (Finset α)) → t ∈ (↑(Finset.nonMemberSubfamily a 𝒜) : Set (Finset α))

Tactic:
simp_rw [mem_coe, mem_nonMemberSubfamily]

Premises used: Finset.mem_nonMemberSubfamily, Finset.mem_coe
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : IsLowerSet (↑𝒜 : Set (Finset α))
s t : Finset α
hts : t ≤ s
⊢ s ∈ 𝒜 ∧ a ∉ s → t ∈ 𝒜 ∧ a ∉ t

Tactic:
And.imp (h hts) (mt <| @hts _)

Premises used: And.imp, mt
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : IsLowerSet (↑𝒜 : Set (Finset α))
s t : Finset α
hts : t ≤ s
⊢ s ∈ 𝒜 ∧ a ∉ s → t ∈ 𝒜 ∧ a ∉ t

Tactic:
exact And.imp (h hts) (mt <| @hts _)

Premises used: And.imp, mt
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : IsLowerSet (↑𝒜 : Set (Finset α))
s t : Finset α
hts : t ≤ s
simp_rw : insert a s ∈ 𝒜 ∧ a ∉ s → insert a t ∈ 𝒜 ∧ a ∉ t
⊢ s ∈ (↑(Finset.memberSubfamily a 𝒜) : Set (Finset α)) → t ∈ (↑(Finset.memberSubfamily a 𝒜) : Set (Finset α))

Tactic:
simp_rw [mem_coe, mem_memberSubfamily]

Premises used: Finset.mem_memberSubfamily, Finset.mem_coe
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : IsLowerSet (↑𝒜 : Set (Finset α))
s t : Finset α
hts : t ≤ s
⊢ insert a s ∈ 𝒜 ∧ a ∉ s → insert a t ∈ 𝒜 ∧ a ∉ t

Tactic:
And.imp (h <| insert_subset_insert _ hts) (mt <| @hts _)

Premises used: And.imp, Finset.insert_subset_insert, mt
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : IsLowerSet (↑𝒜 : Set (Finset α))
s t : Finset α
hts : t ≤ s
⊢ insert a s ∈ 𝒜 ∧ a ∉ s → insert a t ∈ 𝒜 ∧ a ∉ t

Tactic:
exact And.imp (h <| insert_subset_insert _ hts) (mt <| @hts _)

Premises used: And.imp, Finset.insert_subset_insert, mt
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : IsLowerSet (↑𝒜 : Set (Finset α))
s : Finset α
rw : insert a s ∈ 𝒜 ∧ a ∉ s → s ∈ 𝒜 ∧ a ∉ s
⊢ s ∈ Finset.memberSubfamily a 𝒜 → s ∈ Finset.nonMemberSubfamily a 𝒜

Tactic:
rw [mem_memberSubfamily, mem_nonMemberSubfamily]

Premises used: Finset.mem_nonMemberSubfamily, Finset.mem_memberSubfamily
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : IsLowerSet (↑𝒜 : Set (Finset α))
s : Finset α
⊢ insert a s ∈ 𝒜 ∧ a ∉ s → s ∈ 𝒜 ∧ a ∉ s

Tactic:
And.imp_left (h <| subset_insert _ _)

Premises used: And.imp_left, Finset.subset_insert
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : IsLowerSet (↑𝒜 : Set (Finset α))
s : Finset α
⊢ insert a s ∈ 𝒜 ∧ a ∉ s → s ∈ 𝒜 ∧ a ∉ s

Tactic:
exact And.imp_left (h <| subset_insert _ _)

Premises used: And.imp_left, Finset.subset_insert
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet (↑𝒜 : Set (Finset α))
hℬ : IsLowerSet (↑ℬ : Set (Finset α))
h𝒜s : ∀ t ∈ 𝒜, t ⊆ ∅
hℬs : ∀ t ∈ ℬ, t ⊆ ∅
⊢ 𝒜 = ∅ ∨ 𝒜 = {∅}

Tactic:
simp_rw [subset_empty, ← subset_singleton_iff', subset_singleton_iff] at h𝒜s hℬs

Premises used: Finset.subset_empty, Finset.subset_singleton_iff, Finset.subset_singleton_iff'
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet (↑𝒜 : Set (Finset α))
hℬ : IsLowerSet (↑ℬ : Set (Finset α))
h𝒜s : ∀ t ∈ 𝒜, t ⊆ ∅
hℬs : ∀ t ∈ ℬ, t ⊆ ∅
h𝒜s₁ : 𝒜 = ∅ ∨ 𝒜 = {∅}
⊢ ℬ = ∅ ∨ ℬ = {∅}

Tactic:
simp_rw [subset_empty, ← subset_singleton_iff', subset_singleton_iff] at h𝒜s hℬs

Premises used: Finset.subset_empty, Finset.subset_singleton_iff, Finset.subset_singleton_iff'
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet (↑𝒜 : Set (Finset α))
hℬ : IsLowerSet (↑ℬ : Set (Finset α))
h𝒜s : 𝒜 = ∅ ∨ 𝒜 = {∅}
hℬs : ℬ = ∅ ∨ ℬ = {∅}
empty :
  ∀ (h𝒜 : IsLowerSet (↑∅ : Set (Finset α))),
    card.{u_1} (α := Finset α) ∅ * #ℬ ≤ HPow.hPow (α := ℕ) 2 (card.{u_1} (α := α) ∅) * #(∅ ∩ ℬ)
empty₁ :
  ∀ (h𝒜 : IsLowerSet (↑{∅} : Set (Finset α))),
    card (α := Finset α) {∅} * #ℬ ≤ HPow.hPow (α := ℕ) 2 (card.{u_1} (α := α) ∅) * #({∅} ∩ ℬ)
⊢ #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 (card.{u_1} (α := α) ∅) * #(𝒜 ∩ ℬ)

Tactic:
obtain rfl | rfl := h𝒜s

Premises used: rfl
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
ℬ : Finset (Finset α)
hℬ : IsLowerSet (↑ℬ : Set (Finset α))
hℬs : ℬ = ∅ ∨ ℬ = {∅}
h𝒜 : IsLowerSet (↑∅ : Set (Finset α))
⊢ card.{u_1} (α := Finset α) ∅ * #ℬ ≤ HPow.hPow (α := ℕ) 2 (card.{u_1} (α := α) ∅) * #(∅ ∩ ℬ)

Tactic:
simp only [card_empty, zero_mul, empty_inter, mul_zero, le_refl]

Premises used: Finset.empty_inter, le_refl, MulZeroClass.zero_mul, MulZeroClass.mul_zero, Finset.card_empty
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
ℬ : Finset (Finset α)
hℬ : IsLowerSet (↑ℬ : Set (Finset α))
hℬs : ℬ = ∅ ∨ ℬ = {∅}
h𝒜 : IsLowerSet (↑{∅} : Set (Finset α))
empty :
  ∀ (hℬ : IsLowerSet (↑∅ : Set (Finset α))),
    card (α := Finset α) {∅} * card.{u_1} (α := Finset α) ∅ ≤
      HPow.hPow (α := ℕ) 2 (card.{u_1} (α := α) ∅) * card (α := Finset α) ({∅} ∩ ∅)
empty₁ :
  ∀ (hℬ : IsLowerSet (↑{∅} : Set (Finset α))),
    card (α := Finset α) {∅} * card (α := Finset α) {∅} ≤
      HPow.hPow (α := ℕ) 2 (card.{u_1} (α := α) ∅) * card (α := Finset α) ({∅} ∩ {∅})
⊢ card (α := Finset α) {∅} * #ℬ ≤ HPow.hPow (α := ℕ) 2 (card.{u_1} (α := α) ∅) * #({∅} ∩ ℬ)

Tactic:
obtain rfl | rfl := hℬs

Premises used: rfl
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
h𝒜 : IsLowerSet (↑{∅} : Set (Finset α))
hℬ : IsLowerSet (↑∅ : Set (Finset α))
⊢ card (α := Finset α) {∅} * card.{u_1} (α := Finset α) ∅ ≤
    HPow.hPow (α := ℕ) 2 (card.{u_1} (α := α) ∅) * card (α := Finset α) ({∅} ∩ ∅)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
h𝒜 hℬ : IsLowerSet (↑{∅} : Set (Finset α))
⊢ card (α := Finset α) {∅} * card (α := Finset α) {∅} ≤
    HPow.hPow (α := ℕ) 2 (card.{u_1} (α := α) ∅) * card (α := Finset α) ({∅} ∩ {∅})

Tactic:
simp only [card_empty, pow_zero, inter_singleton_of_mem, mem_singleton, card_singleton,
        le_refl]

Premises used: Finset.mem_singleton, le_refl, Finset.inter_singleton_of_mem, pow_zero, Finset.card_empty, Finset.card_singleton
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
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
insert :
  #(Finset.memberSubfamily a 𝒜) * #(Finset.nonMemberSubfamily a ℬ) +
        #(Finset.nonMemberSubfamily a 𝒜) * #(Finset.memberSubfamily a ℬ) +
      (#(Finset.memberSubfamily a 𝒜) * #(Finset.memberSubfamily a ℬ) +
        #(Finset.nonMemberSubfamily a 𝒜) * #(Finset.nonMemberSubfamily a ℬ)) ≤
    HPow.hPow (α := ℕ) 2 (#s + 1) * #(𝒜 ∩ ℬ)
⊢ #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 #(Insert.insert a s) * #(𝒜 ∩ ℬ)

Tactic:
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]

Premises used: add_mul, Finset.card_memberSubfamily_add_card_nonMemberSubfamily, HMul.hMul, Finset.card_insert_of_notMem, add_comm, mul_add, add_add_add_comm
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
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
insert :
  2 *
      (#(Finset.memberSubfamily a 𝒜) * #(Finset.memberSubfamily a ℬ) +
        #(Finset.nonMemberSubfamily a 𝒜) * #(Finset.nonMemberSubfamily a ℬ)) ≤
    2 * (HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ))
⊢ #(Finset.memberSubfamily a 𝒜) * #(Finset.nonMemberSubfamily a ℬ) +
        #(Finset.nonMemberSubfamily a 𝒜) * #(Finset.memberSubfamily a ℬ) +
      (#(Finset.memberSubfamily a 𝒜) * #(Finset.memberSubfamily a ℬ) +
        #(Finset.nonMemberSubfamily a 𝒜) * #(Finset.nonMemberSubfamily a ℬ)) ≤
    HPow.hPow (α := ℕ) 2 (#s + 1) * #(𝒜 ∩ ℬ)

Tactic:
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]

Premises used: Finset.card_le_card, mul_assoc, two_mul, IsLowerSet.memberSubfamily_subset_nonMemberSubfamily, mul_add_mul_le_mul_add_mul, pow_succ'
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
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
𝒞 : Finset (Finset α)
h𝒞 : ∀ t ∈ 𝒞, t ⊆ insert a s
t : Finset α
ht : t ∈ Finset.nonMemberSubfamily a 𝒞
⊢ t ∈ 𝒞 ∧ a ∉ t

Tactic:
rw [mem_nonMemberSubfamily] at ht

Premises used: Finset.mem_nonMemberSubfamily
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
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
𝒞 : Finset (Finset α)
h𝒞 : ∀ t ∈ 𝒞, t ⊆ insert a s
t : Finset α
ht : t ∈ 𝒞 ∧ a ∉ t
⊢ t ⊆ s

Tactic:
(subset_insert_iff_of_notMem ht.2).1 (h𝒞 _ ht.1)

Premises used: Finset.subset_insert_iff_of_notMem, And.right, And.left, Iff.mp
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
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
𝒞 : Finset (Finset α)
h𝒞 : ∀ t ∈ 𝒞, t ⊆ insert a s
t : Finset α
ht : t ∈ 𝒞 ∧ a ∉ t
⊢ t ⊆ s

Tactic:
exact (subset_insert_iff_of_notMem ht.2).1 (h𝒞 _ ht.1)

Premises used: Finset.subset_insert_iff_of_notMem, And.right, And.left, Iff.mp
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
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
⊢ ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.nonMemberSubfamily a 𝒞, t ⊆ s

Tactic:
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)
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
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
𝒞 : Finset (Finset α)
h𝒞 : ∀ t ∈ 𝒞, t ⊆ insert a s
t : Finset α
ht : t ∈ Finset.memberSubfamily a 𝒞
⊢ insert a t ∈ 𝒞 ∧ a ∉ t

Tactic:
rw [mem_memberSubfamily] at ht

Premises used: Finset.mem_memberSubfamily
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
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
𝒞 : Finset (Finset α)
h𝒞 : ∀ t ∈ 𝒞, t ⊆ insert a s
t : Finset α
ht : insert a t ∈ 𝒞 ∧ a ∉ t
⊢ t ⊆ s

Tactic:
(subset_insert_iff_of_notMem ht.2).1 ((subset_insert _ _).trans <| h𝒞 _ ht.1)

Premises used: Finset.subset_insert_iff_of_notMem, HasSubset.Subset.trans, And.right, And.left, Iff.mp, Finset.subset_insert
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
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
𝒞 : Finset (Finset α)
h𝒞 : ∀ t ∈ 𝒞, t ⊆ insert a s
t : Finset α
ht : insert a t ∈ 𝒞 ∧ a ∉ t
⊢ t ⊆ s

Tactic:
exact (subset_insert_iff_of_notMem ht.2).1 ((subset_insert _ _).trans <| h𝒞 _ ht.1)

Premises used: Finset.subset_insert_iff_of_notMem, HasSubset.Subset.trans, And.right, And.left, Iff.mp, Finset.subset_insert
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
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
⊢ ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.memberSubfamily a 𝒞, t ⊆ s

Tactic:
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)
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
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 :
  #(Finset.memberSubfamily a 𝒜) * #(Finset.memberSubfamily a ℬ) +
      #(Finset.nonMemberSubfamily a 𝒜) * #(Finset.nonMemberSubfamily a ℬ) ≤
    HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
⊢ 2 *
      (#(Finset.memberSubfamily a 𝒜) * #(Finset.memberSubfamily a ℬ) +
        #(Finset.nonMemberSubfamily a 𝒜) * #(Finset.nonMemberSubfamily a ℬ)) ≤
    2 * (HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ))

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
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 * #(𝒜 ∩ ℬ)

Tactic:
(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 ?_

Premises used: LE.le.trans_eq, IsLowerSet.memberSubfamily, add_le_add, IsLowerSet.nonMemberSubfamily
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
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 ℬ) +
      HPow.hPow (α := ℕ) 2 #s * #(Finset.nonMemberSubfamily a 𝒜 ∩ Finset.nonMemberSubfamily a ℬ) =
    HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
⊢ #(Finset.memberSubfamily a 𝒜) * #(Finset.memberSubfamily a ℬ) +
      #(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 ?_

Premises used: LE.le.trans_eq, IsLowerSet.memberSubfamily, add_le_add, IsLowerSet.nonMemberSubfamily