awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DistribLattice α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : ExistsAddOfLE β
f g μ : α → β
inst_5 : Fintype α
hμ₀ : 0 ≤ μ
hf : 0 ≤ f
hg : 0 ≤ g
hμ : Monotone μ
hfg : Eq.{u_2 + 1} (α := β) (∑ a : α, f a) (∑ a : α, g a)
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
inl :
  ∀ (hf : LE.le (α := α → β) 0 0) (hfg : Eq.{u_2 + 1} (α := β) (∑ a : α, 0 a) (∑ a : α, g a))
    (h : ∀ (a b : α), 0 a * g b ≤ 0 (a ⊓ b) * g (a ⊔ b)), LE.le.{u_2} (α := β) (∑ a : α, μ a * 0 a) (∑ a : α, μ a * g a)
inr inr₁ : ∀ (hf : 0 < f), LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)
⊢ LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)
have inr₂ : ∀ (hf : 0 < f) (hg : LE.le (α := α → β) 0 0) (hfg : Eq.{u_2 + 1} (α := β) (∑ a : α, f a) (∑ a : α, 0 a))
  (h : ∀ (a b : α), f a * 0 b ≤ f (a ⊓ b) * 0 (a ⊔ b)), LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * 0 a)
Tactic: classical
  obtain rfl | hf := hf.eq_or_lt
  · simp only [Pi.zero_apply, sum_const_zero, eq_comm, Fintype.sum_eq_zero_iff_of_nonneg hg] at hfg
    simp [hfg]
  obtain rfl | hg := hg.eq_or_lt
  · simp only [Pi.zero_apply, sum_const_zero, Fintype.sum_eq_zero_iff_of_nonneg hf.le] at hfg
    simp [hfg]
  have := four_functions_theorem g (μ * f) f (μ * g) hg.le (mul_nonneg hμ₀ hf.le) hf.le
    (mul_nonneg hμ₀ hg.le) (fun a b ↦ ?_) univ univ
  · simpa [hfg, sum_pos hg] using this
  · simp_rw [Pi.mul_apply, mul_left_comm _ (μ _), mul_comm (g _)]
    rw [sup_comm, inf_comm]
    exact mul_le_mul (hμ le_sup_left) (h _ _) (mul_nonneg (hf.le _) <| hg.le _) <| hμ₀ _
Cleared hypotheses: g, hg, hfg, h
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DistribLattice α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : ExistsAddOfLE β
f g μ : α → β
inst_5 : Fintype α
hμ₀ : 0 ≤ μ
hf : 0 ≤ f
hg : 0 ≤ g
hμ : Monotone μ
hfg : Eq.{u_2 + 1} (α := β) (∑ a : α, f a) (∑ a : α, g a)
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
inl :
  ∀ (hf : LE.le (α := α → β) 0 0) (hfg : Eq.{u_2 + 1} (α := β) (∑ a : α, 0 a) (∑ a : α, g a))
    (h : ∀ (a b : α), 0 a * g b ≤ 0 (a ⊓ b) * g (a ⊔ b)), LE.le.{u_2} (α := β) (∑ a : α, μ a * 0 a) (∑ a : α, μ a * g a)
inr inr₁ : ∀ (hf : 0 < f), LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)
inr₂ :
  ∀ (hf : 0 < f) (hg : LE.le (α := α → β) 0 0) (hfg : Eq.{u_2 + 1} (α := β) (∑ a : α, f a) (∑ a : α, 0 a))
    (h : ∀ (a b : α), f a * 0 b ≤ f (a ⊓ b) * 0 (a ⊔ b)), LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * 0 a)
⊢ LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)
have inr₃ : ∀ (hf : 0 < f) (hg : 0 < g), LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)
Tactic: classical
  obtain rfl | hf := hf.eq_or_lt
  · simp only [Pi.zero_apply, sum_const_zero, eq_comm, Fintype.sum_eq_zero_iff_of_nonneg hg] at hfg
    simp [hfg]
  obtain rfl | hg := hg.eq_or_lt
  · simp only [Pi.zero_apply, sum_const_zero, Fintype.sum_eq_zero_iff_of_nonneg hf.le] at hfg
    simp [hfg]
  have := four_functions_theorem g (μ * f) f (μ * g) hg.le (mul_nonneg hμ₀ hf.le) hf.le
    (mul_nonneg hμ₀ hg.le) (fun a b ↦ ?_) univ univ
  · simpa [hfg, sum_pos hg] using this
  · simp_rw [Pi.mul_apply, mul_left_comm _ (μ _), mul_comm (g _)]
    rw [sup_comm, inf_comm]
    exact mul_le_mul (hμ le_sup_left) (h _ _) (mul_nonneg (hf.le _) <| hg.le _) <| hμ₀ _
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DistribLattice α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : ExistsAddOfLE β
f g μ : α → β
inst_5 : Fintype α
hμ₀ : 0 ≤ μ
hf : 0 ≤ f
hg : 0 ≤ g
hμ : Monotone μ
hfg : Eq.{u_2 + 1} (α := β) (∑ a : α, f a) (∑ a : α, g a)
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
inl :
  ∀ (hf : LE.le (α := α → β) 0 0) (hfg : Eq.{u_2 + 1} (α := β) (∑ a : α, 0 a) (∑ a : α, g a))
    (h : ∀ (a b : α), 0 a * g b ≤ 0 (a ⊓ b) * g (a ⊔ b)), LE.le.{u_2} (α := β) (∑ a : α, μ a * 0 a) (∑ a : α, μ a * g a)
inr inr₁ : ∀ (hf : 0 < f), LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)
inr₂ :
  ∀ (hf : 0 < f) (hg : LE.le (α := α → β) 0 0) (hfg : Eq.{u_2 + 1} (α := β) (∑ a : α, f a) (∑ a : α, 0 a))
    (h : ∀ (a b : α), f a * 0 b ≤ f (a ⊓ b) * 0 (a ⊔ b)), LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * 0 a)
inr₃ inr₄ : ∀ (hf : 0 < f) (hg : 0 < g), LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)
⊢ LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)
have inr₅ : ∀ (hf : 0 < f) (hg : 0 < g)
  (this :
    HMul.hMul (α := β) (∑ a : α, g a) (∑ a : α, (μ * f) a) ≤
      HMul.hMul (α := β) (∑ a ∈ univ ⊼ univ, f a) (∑ a ∈ univ ⊻ univ, (μ * g) a)),
  LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)
Tactic: classical
  obtain rfl | hf := hf.eq_or_lt
  · simp only [Pi.zero_apply, sum_const_zero, eq_comm, Fintype.sum_eq_zero_iff_of_nonneg hg] at hfg
    simp [hfg]
  obtain rfl | hg := hg.eq_or_lt
  · simp only [Pi.zero_apply, sum_const_zero, Fintype.sum_eq_zero_iff_of_nonneg hf.le] at hfg
    simp [hfg]
  have := four_functions_theorem g (μ * f) f (μ * g) hg.le (mul_nonneg hμ₀ hf.le) hf.le
    (mul_nonneg hμ₀ hg.le) (fun a b ↦ ?_) univ univ
  · simpa [hfg, sum_pos hg] using this
  · simp_rw [Pi.mul_apply, mul_left_comm _ (μ _), mul_comm (g _)]
    rw [sup_comm, inf_comm]
    exact mul_le_mul (hμ le_sup_left) (h _ _) (mul_nonneg (hf.le _) <| hg.le _) <| hμ₀ _
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DistribLattice α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : ExistsAddOfLE β
f g μ : α → β
inst_5 : Fintype α
hμ₀ : 0 ≤ μ
hf : 0 ≤ f
hg : 0 ≤ g
hμ : Monotone μ
hfg : Eq.{u_2 + 1} (α := β) (∑ a : α, f a) (∑ a : α, g a)
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
inl :
  ∀ (hf : LE.le (α := α → β) 0 0) (hfg : Eq.{u_2 + 1} (α := β) (∑ a : α, 0 a) (∑ a : α, g a))
    (h : ∀ (a b : α), 0 a * g b ≤ 0 (a ⊓ b) * g (a ⊔ b)), LE.le.{u_2} (α := β) (∑ a : α, μ a * 0 a) (∑ a : α, μ a * g a)
inr inr₁ : ∀ (hf : 0 < f), LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)
inr₂ :
  ∀ (hf : 0 < f) (hg : LE.le (α := α → β) 0 0) (hfg : Eq.{u_2 + 1} (α := β) (∑ a : α, f a) (∑ a : α, 0 a))
    (h : ∀ (a b : α), f a * 0 b ≤ f (a ⊓ b) * 0 (a ⊔ b)), LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * 0 a)
inr₃ inr₄ : ∀ (hf : 0 < f) (hg : 0 < g), LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)
inr₅ :
  ∀ (hf : 0 < f) (hg : 0 < g)
    (this :
      HMul.hMul (α := β) (∑ a : α, g a) (∑ a : α, (μ * f) a) ≤
        HMul.hMul (α := β) (∑ a ∈ univ ⊼ univ, f a) (∑ a ∈ univ ⊻ univ, (μ * g) a)),
    LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)
⊢ LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)
have inr₆ : ∀ (hf : 0 < f) (hg : 0 < g) (a b : α), g a * (μ * f) b ≤ f (a ⊓ b) * (μ * g) (a ⊔ b)
Tactic: classical
  obtain rfl | hf := hf.eq_or_lt
  · simp only [Pi.zero_apply, sum_const_zero, eq_comm, Fintype.sum_eq_zero_iff_of_nonneg hg] at hfg
    simp [hfg]
  obtain rfl | hg := hg.eq_or_lt
  · simp only [Pi.zero_apply, sum_const_zero, Fintype.sum_eq_zero_iff_of_nonneg hf.le] at hfg
    simp [hfg]
  have := four_functions_theorem g (μ * f) f (μ * g) hg.le (mul_nonneg hμ₀ hf.le) hf.le
    (mul_nonneg hμ₀ hg.le) (fun a b ↦ ?_) univ univ
  · simpa [hfg, sum_pos hg] using this
  · simp_rw [Pi.mul_apply, mul_left_comm _ (μ _), mul_comm (g _)]
    rw [sup_comm, inf_comm]
    exact mul_le_mul (hμ le_sup_left) (h _ _) (mul_nonneg (hf.le _) <| hg.le _) <| hμ₀ _
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DistribLattice α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : ExistsAddOfLE β
f g μ : α → β
inst_5 : Fintype α
hμ₀ : 0 ≤ μ
hf₀ : 0 ≤ f
hg₀ : 0 ≤ g
hf : Monotone f
hg : Monotone g
hμ : ∀ (a b : α), μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)
⊢ HMul.hMul (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a) ≤
    HMul.hMul (α := β) (∑ a : α, μ a) (∑ a : α, μ a * (f a * g a))
have refine : ∀ (a b : α), (μ * f) a * (μ * g) b ≤ μ (a ⊓ b) * (μ (a ⊔ b) * (f (a ⊔ b) * g (a ⊔ b)))
Tactic: refine four_functions_theorem_univ (μ * f) (μ * g) μ _ (mul_nonneg hμ₀ hf₀) (mul_nonneg hμ₀ hg₀)
    hμ₀ (mul_nonneg hμ₀ <| mul_nonneg hf₀ hg₀) (fun a b ↦ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DistribLattice α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : ExistsAddOfLE β
f g μ : α → β
inst_5 : Fintype α
hμ₀ : 0 ≤ μ
hf₀ : 0 ≤ f
hg₀ : 0 ≤ g
hf : Monotone f
hg : Monotone g
hμ : ∀ (a b : α), μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)
a b : α
⊢ (μ * f) a * (μ * g) b ≤ μ (a ⊓ b) * (μ (a ⊔ b) * (f (a ⊔ b) * g (a ⊔ b)))
have dsimp : μ a * f a * (μ b * g b) ≤ μ (a ⊓ b) * (μ (a ⊔ b) * (f (a ⊔ b) * g (a ⊔ b)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DistribLattice α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : ExistsAddOfLE β
f g μ : α → β
inst_5 : Fintype α
hμ₀ : 0 ≤ μ
hf₀ : 0 ≤ f
hg₀ : 0 ≤ g
hf : Monotone f
hg : Monotone g
hμ : ∀ (a b : α), μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)
a b : α
⊢ μ a * f a * (μ b * g b) ≤ μ (a ⊓ b) * (μ (a ⊔ b) * (f (a ⊔ b) * g (a ⊔ b)))
have rw : μ a * μ b * (f a * g b) ≤ μ (a ⊓ b) * μ (a ⊔ b) * (f (a ⊔ b) * g (a ⊔ b))
Tactic: rw [mul_mul_mul_comm, ← mul_assoc (μ (a ⊓ b))]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s_1 t_1 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
have simp_rw : Eq (α := Finset (Booleanisation α))
  (image (⇑{ toFun := (⇑liftLatticeHom : (a : α) → Booleanisation α), inj' := sorry } : (a : α) → Booleanisation α)
    (s \\ t))
  (image (⇑{ toFun := (⇑liftLatticeHom : (a : α) → Booleanisation α), inj' := sorry } : (a : α) → Booleanisation α) s \\
    image (⇑{ toFun := (⇑liftLatticeHom : (a : α) → Booleanisation α), inj' := sorry } : (a : α) → Booleanisation α) t)
Tactic: simp_rw [map_eq_image]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : GeneralizedBooleanAlgebra α
s t : Finset α
⊢ #s * #t ≤ #(s \\ t) * #(t \\ s)
have this : ∀ (s t : Finset α),
  map { toFun := (⇑liftLatticeHom : (a : α) → Booleanisation α), inj' := sorry : α ↪ Booleanisation α } (s \\ t) =
    map { toFun := (⇑liftLatticeHom : (a : α) → Booleanisation α), inj' := sorry } s \\
      map { toFun := (⇑liftLatticeHom : (a : α) → Booleanisation α), inj' := sorry } 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
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.HarrisKleitman (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : IsLowerSet (↑𝒜 : Set (Finset α))
s t : Finset α
hts : t ≤ s
⊢ s ∈ (↑(Finset.nonMemberSubfamily a 𝒜) : Set (Finset α)) → t ∈ (↑(Finset.nonMemberSubfamily a 𝒜) : Set (Finset α))
have simp_rw : s ∈ 𝒜 ∧ a ∉ s → t ∈ 𝒜 ∧ a ∉ t
Tactic: simp_rw [mem_coe, mem_nonMemberSubfamily]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.HarrisKleitman (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : IsLowerSet (↑𝒜 : Set (Finset α))
s t : Finset α
hts : t ≤ s
⊢ s ∈ (↑(Finset.memberSubfamily a 𝒜) : Set (Finset α)) → t ∈ (↑(Finset.memberSubfamily a 𝒜) : Set (Finset α))
have simp_rw : insert a s ∈ 𝒜 ∧ a ∉ s → insert a t ∈ 𝒜 ∧ a ∉ t
Tactic: simp_rw [mem_coe, mem_memberSubfamily]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.HarrisKleitman (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : IsLowerSet (↑𝒜 : Set (Finset α))
s : Finset α
⊢ s ∈ Finset.memberSubfamily a 𝒜 → s ∈ Finset.nonMemberSubfamily a 𝒜
have rw : insert a s ∈ 𝒜 ∧ a ∉ s → s ∈ 𝒜 ∧ a ∉ s
Tactic: rw [mem_memberSubfamily, mem_nonMemberSubfamily]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.HarrisKleitman (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet (↑𝒜 : Set (Finset α))
hℬ : IsLowerSet (↑ℬ : Set (Finset α))
h𝒜s : ∀ t ∈ 𝒜, t ⊆ ∅
hℬs : ∀ t ∈ ℬ, t ⊆ ∅
⊢ #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 (card.{u_1} (α := α) ∅) * #(𝒜 ∩ ℬ)
have h𝒜s₁ : 𝒜 = ∅ ∨ 𝒜 = {∅}
Tactic: simp_rw [subset_empty, ← subset_singleton_iff', subset_singleton_iff] at h𝒜s hℬs
Cleared hypotheses: h𝒜s, hℬs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.HarrisKleitman (hypothesis)
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₁ : 𝒜 = ∅ ∨ 𝒜 = {∅}
⊢ #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 (card.{u_1} (α := α) ∅) * #(𝒜 ∩ ℬ)
have hℬs₁ : ℬ = ∅ ∨ ℬ = {∅}
Tactic: simp_rw [subset_empty, ← subset_singleton_iff', subset_singleton_iff] at h𝒜s hℬs
Cleared hypotheses: h𝒜s, hℬs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.HarrisKleitman (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet (↑𝒜 : Set (Finset α))
hℬ : IsLowerSet (↑ℬ : Set (Finset α))
h𝒜s : 𝒜 = ∅ ∨ 𝒜 = {∅}
hℬs : ℬ = ∅ ∨ ℬ = {∅}
⊢ #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 (card.{u_1} (α := α) ∅) * #(𝒜 ∩ ℬ)
have empty : ∀ (h𝒜 : IsLowerSet (↑∅ : Set (Finset α))),
  card.{u_1} (α := Finset α) ∅ * #ℬ ≤ HPow.hPow (α := ℕ) 2 (card.{u_1} (α := α) ∅) * #(∅ ∩ ℬ)
Tactic: obtain rfl | rfl := h𝒜s
Cleared hypotheses: 𝒜, h𝒜, h𝒜s
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.HarrisKleitman (goal)
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} (α := α) ∅) * #(∅ ∩ ℬ)
⊢ #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 (card.{u_1} (α := α) ∅) * #(𝒜 ∩ ℬ)
have empty₁ : ∀ (h𝒜 : IsLowerSet (↑{∅} : Set (Finset α))),
  card (α := Finset α) {∅} * #ℬ ≤ HPow.hPow (α := ℕ) 2 (card.{u_1} (α := α) ∅) * #({∅} ∩ ℬ)
Tactic: obtain rfl | rfl := h𝒜s
Cleared hypotheses: 𝒜, h𝒜, h𝒜s
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.HarrisKleitman (goal)
Goal:
α : Type u_1
inst : DecidableEq α
ℬ : Finset (Finset α)
hℬ : IsLowerSet (↑ℬ : Set (Finset α))
hℬs : ℬ = ∅ ∨ ℬ = {∅}
h𝒜 : IsLowerSet (↑{∅} : Set (Finset α))
⊢ card (α := Finset α) {∅} * #ℬ ≤ HPow.hPow (α := ℕ) 2 (card.{u_1} (α := α) ∅) * #({∅} ∩ ℬ)
have empty : ∀ (hℬ : IsLowerSet (↑∅ : Set (Finset α))),
  card (α := Finset α) {∅} * card.{u_1} (α := Finset α) ∅ ≤
    HPow.hPow (α := ℕ) 2 (card.{u_1} (α := α) ∅) * card (α := Finset α) ({∅} ∩ ∅)
Tactic: obtain rfl | rfl := hℬs
Cleared hypotheses: ℬ, hℬ, hℬs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.HarrisKleitman (goal)
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 α) ({∅} ∩ ∅)
⊢ card (α := Finset α) {∅} * #ℬ ≤ HPow.hPow (α := ℕ) 2 (card.{u_1} (α := α) ∅) * #({∅} ∩ ℬ)
have empty₁ : ∀ (hℬ : IsLowerSet (↑{∅} : Set (Finset α))),
  card (α := Finset α) {∅} * card (α := Finset α) {∅} ≤
    HPow.hPow (α := ℕ) 2 (card.{u_1} (α := α) ∅) * card (α := Finset α) ({∅} ∩ {∅})
Tactic: obtain rfl | rfl := hℬs
Cleared hypotheses: ℬ, hℬ, hℬs
-- 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
⊢ #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 #(insert a s) * #(𝒜 ∩ ℬ)
have 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) * #(𝒜 ∩ ℬ)
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]
-- 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
⊢ #(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) * #(𝒜 ∩ ℬ)
have insert : 2 *
    (#(Finset.memberSubfamily a 𝒜) * #(Finset.memberSubfamily a ℬ) +
      #(Finset.nonMemberSubfamily a 𝒜) * #(Finset.nonMemberSubfamily a ℬ)) ≤
  2 * (HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ))
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.HarrisKleitman (hypothesis)
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 ⊆ s
have ht₁ : t ∈ 𝒞 ∧ a ∉ t
Tactic: rw [mem_nonMemberSubfamily] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.HarrisKleitman (hypothesis)
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
⊢ 2 *
      (#(Finset.memberSubfamily a 𝒜) * #(Finset.memberSubfamily a ℬ) +
        #(Finset.nonMemberSubfamily a 𝒜) * #(Finset.nonMemberSubfamily a ℬ)) ≤
    2 * (HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ))
have h₀ : ∀ (𝒞 : 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)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.HarrisKleitman (hypothesis)
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 𝒞
⊢ t ⊆ s
have ht₁ : insert a t ∈ 𝒞 ∧ a ∉ t
Tactic: rw [mem_memberSubfamily] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.HarrisKleitman (hypothesis)
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
⊢ 2 *
      (#(Finset.memberSubfamily a 𝒜) * #(Finset.memberSubfamily a ℬ) +
        #(Finset.nonMemberSubfamily a 𝒜) * #(Finset.nonMemberSubfamily a ℬ)) ≤
    2 * (HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ))
have h₁ : ∀ (𝒞 : 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)
-- 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
⊢ 2 *
      (#(Finset.memberSubfamily a 𝒜) * #(Finset.memberSubfamily a ℬ) +
        #(Finset.nonMemberSubfamily a 𝒜) * #(Finset.nonMemberSubfamily a ℬ)) ≤
    2 * (HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ))
have insert : #(Finset.memberSubfamily a 𝒜) * #(Finset.memberSubfamily a ℬ) +
    #(Finset.nonMemberSubfamily a 𝒜) * #(Finset.nonMemberSubfamily a ℬ) ≤
  HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
Tactic: gcongr