awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
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 α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
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
-- 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ℬ : IsUpperSet (↑ℬ : Set (Finset α))
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
have rw : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(ℬ ∩ 𝒜) ≤ #ℬ * #𝒜
Tactic: rw [inter_comm, mul_comm #𝒜]
-- 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ℬ : IsUpperSet (↑ℬ : 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ℬ : IsUpperSet (↑ℬ : Set (Finset α))
⊢ #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ)
have this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ) ≤ #𝒜ᶜ * #ℬ
Tactic: have := h𝒜.card_inter_le_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ℬ : IsUpperSet (↑ℬ : Set (Finset α))
this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ) ≤ #𝒜ᶜ * #ℬ
⊢ #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ)
have h₁ : ∀ (this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ - #𝒜 * #ℬ),
  HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ
Tactic: rwa [card_compl, Fintype.card_finset, tsub_mul, le_tsub_iff_le_tsub, ← 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ℬ : IsUpperSet (↑ℬ : Set (Finset α))
this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ) ≤ #𝒜ᶜ * #ℬ
h₁ :
  ∀ (this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ - #𝒜 * #ℬ),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ
⊢ #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ)
have h₂ : ∀ (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, le_tsub_iff_le_tsub, ← 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ℬ : IsUpperSet (↑ℬ : Set (Finset α))
this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ - #𝒜 * #ℬ
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ
have h₁ : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ
Tactic: grw [inter_subset_right]
-- 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ℬ : IsUpperSet (↑ℬ : Set (Finset α))
this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ - #𝒜 * #ℬ
⊢ #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ
have h₂ : #𝒜 * #ℬ ≤ Fintype.card.{u_1} (Finset α) * #ℬ
Tactic: grw [← Fintype.card_finset, card_le_univ]
-- 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ℬ : IsUpperSet (↑ℬ : Set (Finset α))
this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ - #𝒜 * #ℬ
h₂ : #𝒜 * #ℬ ≤ Fintype.card.{u_1} (Finset α) * #ℬ
⊢ #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ
have h₃ : Fintype.card.{u_1} (Finset α) * #ℬ ≤ Fintype.card.{u_1} (Finset α) * #ℬ
Tactic: grw [← Fintype.card_finset, card_le_univ]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
hs : s.Intersecting
c : α
ha : c ≠ ⊥
h : ∀ b ∈ s, ¬Disjoint c b
⊢ ¬Disjoint c c
have inl : ¬c = ⊥
Tactic: rwa [disjoint_self]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
⊢ s.Intersecting ↔ (s.Pairwise fun (a b : α) ↦ ¬Disjoint a b) ∧ s ≠ {⊥}
have refine_1 : ∀ (h : s.Intersecting), s ≠ {⊥}
Tactic: refine ⟨fun h => ⟨fun a ha b hb _ => h ha hb, ?_⟩, fun h a ha b hb hab => ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
refine_1 : ∀ (h : s.Intersecting), s ≠ {⊥}
⊢ s.Intersecting ↔ (s.Pairwise fun (a b : α) ↦ ¬Disjoint a b) ∧ s ≠ {⊥}
have refine_2 : ∀ (h : (s.Pairwise fun (a b : α) ↦ ¬Disjoint a b) ∧ s ≠ {⊥}) (a : α) (ha : a ∈ s) (b : α) (hb : b ∈ s)
  (hab : Disjoint a b), False
Tactic: refine ⟨fun h => ⟨fun a ha b hb _ => h ha hb, ?_⟩, fun h a ha b hb hab => ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (hypothesis)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
h : (s.Pairwise fun (a b : α) ↦ ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : Disjoint a b
⊢ False
have this : a = b
Tactic: have := h.1.eq ha hb (Classical.not_not.2 hab)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (hypothesis)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
h : (s.Pairwise fun (a b : α) ↦ ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : Disjoint a b
this : a = b
⊢ False
have hab₁ : b = ⊥
Tactic: rw [this, disjoint_self] at hab
Cleared hypotheses: hab, this
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (hypothesis)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
h : (s.Pairwise fun (a b : α) ↦ ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : b = ⊥
this : a = b
⊢ False
have hb₁ : ⊥ ∈ s
Tactic: rw [hab] at hb
Cleared hypotheses: hb, hab, this
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
inst_2 : Subsingleton α
s : Set α
⊢ s.Intersecting ↔ s = ∅
have refine_1 : ∀ (h : ¬s = ∅), ⊥ ∈ s
Tactic: refine
    subsingleton_of_subsingleton.intersecting.trans
      ⟨not_imp_comm.2 fun h => subsingleton_of_subsingleton.eq_singleton_of_mem ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
inst_2 : Subsingleton α
s : Set α
refine_1 : ∀ (h : ¬s = ∅), ⊥ ∈ s
⊢ s.Intersecting ↔ s = ∅
have refine_2 : s = ∅ → s ≠ {⊥}
Tactic: refine
    subsingleton_of_subsingleton.intersecting.trans
      ⟨not_imp_comm.2 fun h => subsingleton_of_subsingleton.eq_singleton_of_mem ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
inst_2 : Subsingleton α
s : Set α
h : ¬s = ∅
⊢ ⊥ ∈ s
have refine_1 : ∀ (a : α) (ha : a ∈ s), ⊥ ∈ s
Tactic: obtain ⟨a, ha⟩ := nonempty_iff_ne_empty.2 h
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
hs : s.Intersecting
h : ∀ (t : Set α), t.Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ b ∈ s
have rw : b ∈ insert b s
Tactic: rw [h (Insert.insert b s) _ (subset_insert _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
hs : s.Intersecting
h : ∀ (t : Set α), t.Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
rw : b ∈ insert b s
⊢ b ∈ s
have rw₁ : (insert b s).Intersecting
Tactic: rw [h (Insert.insert b s) _ (subset_insert _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
hs : s.Intersecting
h : ∀ (t : Set α), t.Intersecting → s ⊆ t → s = t
⊢ IsUpperSet s
have rintro : ∀ ⦃a b : α⦄ (hab : a ≤ b) (ha : a ∈ s), b ∈ s
Tactic: classical
    rintro a b hab ha
    rw [h (Insert.insert b s) _ (subset_insert _ _)]
    · exact mem_insert _ _
    exact
      hs.insert (mt (eq_bot_mono hab) <| hs.ne_bot ha) fun c hc hbc => hs ha hc <| hbc.mono_left hab
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
hs : s.Intersecting
h : ∀ (t : Set α), t.Intersecting → s ⊆ t → s = t
rintro : ∀ ⦃a b : α⦄ (hab : a ≤ b) (ha : a ∈ s), b ∈ s
⊢ IsUpperSet s
have rintro₁ : ∀ ⦃a b : α⦄ (hab : a ≤ b) (ha : a ∈ s), b ∈ insert b s
Tactic: classical
    rintro a b hab ha
    rw [h (Insert.insert b s) _ (subset_insert _ _)]
    · exact mem_insert _ _
    exact
      hs.insert (mt (eq_bot_mono hab) <| hs.ne_bot ha) fun c hc hbc => hs ha hc <| hbc.mono_left hab
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
hs : s.Intersecting
h : ∀ (t : Set α), t.Intersecting → s ⊆ t → s = t
rintro : ∀ ⦃a b : α⦄ (hab : a ≤ b) (ha : a ∈ s), b ∈ s
rintro₁ : ∀ ⦃a b : α⦄ (hab : a ≤ b) (ha : a ∈ s), b ∈ insert b s
⊢ IsUpperSet s
have rintro₂ : ∀ ⦃a b : α⦄ (hab : a ≤ b) (ha : a ∈ s), (insert b s).Intersecting
Tactic: classical
    rintro a b hab ha
    rw [h (Insert.insert b s) _ (subset_insert _ _)]
    · exact mem_insert _ _
    exact
      hs.insert (mt (eq_bot_mono hab) <| hs.ne_bot ha) fun c hc hbc => hs ha hc <| hbc.mono_left hab
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ (↑s : Set α)
⊢ b ∈ (↑s : Set α)
have rw : b ∈ (↑(insert b s) : Set α)
Tactic: rw [h (Insert.insert b s) _ (Finset.subset_insert _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ (↑s : Set α)
rw : b ∈ (↑(insert b s) : Set α)
⊢ b ∈ (↑s : Set α)
have rw₁ : (↑(insert b s) : Set α).Intersecting
Tactic: rw [h (Insert.insert b s) _ (Finset.subset_insert _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ (↑s : Set α)
⊢ (↑(insert b s) : Set α).Intersecting
have rw : (insert b (↑s : Set α)).Intersecting
Tactic: rw [coe_insert]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
⊢ IsUpperSet (↑s : Set α)
have rintro : ∀ ⦃a b : α⦄ (hab : a ≤ b) (ha : a ∈ (↑s : Set α)), b ∈ (↑s : Set α)
Tactic: classical
    rintro a b hab ha
    rw [h (Insert.insert b s) _ (Finset.subset_insert _ _)]
    · exact mem_insert_self _ _
    rw [coe_insert]
    exact
      hs.insert (mt (eq_bot_mono hab) <| hs.ne_bot ha) fun c hc hbc => hs ha hc <| hbc.mono_left hab
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
rintro : ∀ ⦃a b : α⦄ (hab : a ≤ b) (ha : a ∈ (↑s : Set α)), b ∈ (↑s : Set α)
⊢ IsUpperSet (↑s : Set α)
have rintro₁ : ∀ ⦃a b : α⦄ (hab : a ≤ b) (ha : a ∈ (↑s : Set α)), b ∈ (↑(insert b s) : Set α)
Tactic: classical
    rintro a b hab ha
    rw [h (Insert.insert b s) _ (Finset.subset_insert _ _)]
    · exact mem_insert_self _ _
    rw [coe_insert]
    exact
      hs.insert (mt (eq_bot_mono hab) <| hs.ne_bot ha) fun c hc hbc => hs ha hc <| hbc.mono_left hab
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
rintro : ∀ ⦃a b : α⦄ (hab : a ≤ b) (ha : a ∈ (↑s : Set α)), b ∈ (↑s : Set α)
rintro₁ : ∀ ⦃a b : α⦄ (hab : a ≤ b) (ha : a ∈ (↑s : Set α)), b ∈ (↑(insert b s) : Set α)
⊢ IsUpperSet (↑s : Set α)
have rintro₂ : ∀ ⦃a b : α⦄ (hab : a ≤ b) (ha : a ∈ (↑s : Set α)), (↑(insert b s) : Set α).Intersecting
Tactic: classical
    rintro a b hab ha
    rw [h (Insert.insert b s) _ (Finset.subset_insert _ _)]
    · exact mem_insert_self _ _
    rw [coe_insert]
    exact
      hs.insert (mt (eq_bot_mono hab) <| hs.ne_bot ha) fun c hc hbc => hs ha hc <| hbc.mono_left hab
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
rintro : ∀ ⦃a b : α⦄ (hab : a ≤ b) (ha : a ∈ (↑s : Set α)), b ∈ (↑s : Set α)
rintro₁ : ∀ ⦃a b : α⦄ (hab : a ≤ b) (ha : a ∈ (↑s : Set α)), b ∈ (↑(insert b s) : Set α)
rintro₂ rintro₃ : ∀ ⦃a b : α⦄ (hab : a ≤ b) (ha : a ∈ (↑s : Set α)), (↑(insert b s) : Set α).Intersecting
⊢ IsUpperSet (↑s : Set α)
have rintro₄ : ∀ ⦃a b : α⦄ (hab : a ≤ b) (ha : a ∈ (↑s : Set α)), (insert b (↑s : Set α)).Intersecting
Tactic: classical
    rintro a b hab ha
    rw [h (Insert.insert b s) _ (Finset.subset_insert _ _)]
    · exact mem_insert_self _ _
    rw [coe_insert]
    exact
      hs.insert (mt (eq_bot_mono hab) <| hs.ne_bot ha) fun c hc hbc => hs ha hc <| hbc.mono_left hab
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : BooleanAlgebra α
s : Finset α
hs : (↑s : Set α).Intersecting
⊢ Disjoint s (map { toFun := compl, inj' := ⋯ } s)
have rw : ∀ ⦃a : α⦄, a ∈ s → a ∉ map { toFun := compl, inj' := sorry : α ↪ α } s
Tactic: rw [Finset.disjoint_left]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : BooleanAlgebra α
s : Finset α
hs : (↑s : Set α).Intersecting
x : α
hx : x ∈ s
hxc : x ∈ map { toFun := compl, inj' := ⋯ : α ↪ α } s
⊢ False
have obtain : ∀ (x : α) (hx' : x ∈ s) (hx : Membership.mem (α := α) s (({ toFun := compl, inj' := sorry } : (a : α) → α) x : α))
  (hxc :
    Membership.mem (α := α) (map { toFun := compl, inj' := sorry : α ↪ α } s)
      (({ toFun := compl, inj' := sorry } : (a : α) → α) x : α)),
  False
Tactic: obtain ⟨x, hx', rfl⟩ := mem_map.mp hxc
Cleared hypotheses: x, hx, hxc
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
⊢ 2 * #s ≤ Fintype.card α
have refine : #(s.disjUnion (map { toFun := compl, inj' := sorry : α ↪ α } s) sorry) = 2 * #s
Tactic: refine (s.disjUnion _ hs.disjoint_map_compl).card_le_univ.trans_eq' ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
⊢ #(s.disjUnion (map { toFun := compl, inj' := ⋯ : α ↪ α } s) ⋯) = 2 * #s
have rw : #(s.disjUnion (map { toFun := compl, inj' := sorry : α ↪ α } s) sorry) = #s + #s
Tactic: rw [Nat.two_mul, card_disjUnion, card_map]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
rw : #(s.disjUnion (map { toFun := compl, inj' := ⋯ : α ↪ α } s) ⋯) = #s + #s
⊢ #(s.disjUnion (map { toFun := compl, inj' := ⋯ : α ↪ α } s) ⋯) = 2 * #s
have rw₁ : #s + #(map { toFun := compl, inj' := sorry : α ↪ α } s) = #s + #s
Tactic: rw [Nat.two_mul, card_disjUnion, card_map]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
rw : #(s.disjUnion (map { toFun := compl, inj' := ⋯ : α ↪ α } s) ⋯) = #s + #s
rw₁ : #s + #(map { toFun := compl, inj' := ⋯ : α ↪ α } s) = #s + #s
⊢ #(s.disjUnion (map { toFun := compl, inj' := ⋯ : α ↪ α } s) ⋯) = 2 * #s
have rw₂ : #s + #s = #s + #s
Tactic: rw [Nat.two_mul, card_disjUnion, card_map]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
⊢ 2 * #s ≤ Fintype.card α
have refine : #(s.disjUnion (map { toFun := compl, inj' := sorry : α ↪ α } s) sorry) = 2 * #s
Tactic: classical
    refine (s.disjUnion _ hs.disjoint_map_compl).card_le_univ.trans_eq' ?_
    rw [Nat.two_mul, card_disjUnion, card_map]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
⊢ (∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) ↔ 2 * #s = Fintype.card α
have refine : ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t), 2 * #s = Fintype.card α
Tactic: refine ⟨fun h ↦ ?_, fun h t ht hst ↦ Finset.eq_of_subset_of_card_le hst <|
      Nat.le_of_mul_le_mul_left (ht.card_le.trans_eq h.symm) Nat.two_pos⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
this : s.disjUnion (map { toFun := compl, inj' := ⋯ : α ↪ α } s) ⋯ = Finset.univ
⊢ 2 * #s = Fintype.card α
have rw : 2 * #s = card.{u_1} (α := α) Finset.univ
Tactic: rw [Fintype.card, ← this, Nat.two_mul, card_disjUnion, card_map]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
this : s.disjUnion (map { toFun := compl, inj' := ⋯ : α ↪ α } s) ⋯ = Finset.univ
rw : 2 * #s = card.{u_1} (α := α) Finset.univ
⊢ 2 * #s = Fintype.card α
have rw₁ : 2 * #s = #(s.disjUnion (map { toFun := compl, inj' := sorry : α ↪ α } s) sorry)
Tactic: rw [Fintype.card, ← this, Nat.two_mul, card_disjUnion, card_map]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
this : s.disjUnion (map { toFun := compl, inj' := ⋯ : α ↪ α } s) ⋯ = Finset.univ
rw : 2 * #s = card.{u_1} (α := α) Finset.univ
rw₁ : 2 * #s = #(s.disjUnion (map { toFun := compl, inj' := ⋯ : α ↪ α } s) ⋯)
⊢ 2 * #s = Fintype.card α
have rw₂ : #s + #s = #(s.disjUnion (map { toFun := compl, inj' := sorry : α ↪ α } s) sorry)
Tactic: rw [Fintype.card, ← this, Nat.two_mul, card_disjUnion, card_map]