case inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B C✝ A C : Finset α
⊢ card (A * C) * card ∅ ≤ card (A * ∅) * card (∅ * C)

case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
hB : Finset.Nonempty B
⊢ card (A * C) * card B ≤ card (A * B) * card (B * C)
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
⊢ card (A * C) * card B ≤ card (A * B) * card (B * C)
obtain rfl | hB := B.eq_empty_or_nonempty
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
hB : Finset.Nonempty B
hB' : B ∈ erase (powerset B) ∅
⊢ card (A * C) * card B ≤ card (A * B) * card (B * C)
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
hB : Finset.Nonempty B
⊢ card (A * C) * card B ≤ card (A * B) * card (B * C)
have hB' : B ∈ B.powerset.erase ∅ := mem_erase_of_ne_of_mem hB.ne_empty (mem_powerset_self _)
case inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
hB : Finset.Nonempty B
hB' : B ∈ erase (powerset B) ∅
U : Finset α
hU : U ∈ erase (powerset B) ∅
hUA : ∀ (x' : Finset α), x' ∈ erase (powerset B) ∅ → ↑(card (U * A)) / ↑(card U) ≤ ↑(card (x' * A)) / ↑(card x')
⊢ card (A * C) * card B ≤ card (A * B) * card (B * C)
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
hB : Finset.Nonempty B
hB' : B ∈ erase (powerset B) ∅
⊢ card (A * C) * card B ≤ card (A * B) * card (B * C)
obtain ⟨U, hU, hUA⟩ :=
  exists_min_image (B.powerset.erase ∅) (fun U ↦ (U * A).card / U.card : _ → ℚ≥0) ⟨B, hB'⟩
case inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
hB : Finset.Nonempty B
hB' : B ∈ erase (powerset B) ∅
U : Finset α
hU : Finset.Nonempty U ∧ U ⊆ B
hUA : ∀ (x' : Finset α), x' ∈ erase (powerset B) ∅ → ↑(card (U * A)) / ↑(card U) ≤ ↑(card (x' * A)) / ↑(card x')
⊢ card (A * C) * card B ≤ card (A * B) * card (B * C)
case inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
hB : Finset.Nonempty B
hB' : B ∈ erase (powerset B) ∅
U : Finset α
hU : U ∈ erase (powerset B) ∅
hUA : ∀ (x' : Finset α), x' ∈ erase (powerset B) ∅ → ↑(card (U * A)) / ↑(card U) ≤ ↑(card (x' * A)) / ↑(card x')
⊢ card (A * C) * card B ≤ card (A * B) * card (B * C)
rw [mem_erase, mem_powerset, ← nonempty_iff_ne_empty] at hU
case inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
hB : Finset.Nonempty B
hB' : B ∈ erase (powerset B) ∅
U : Finset α
hU : Finset.Nonempty U ∧ U ⊆ B
hUA : ∀ (x' : Finset α), x' ∈ erase (powerset B) ∅ → ↑(card (U * A)) / ↑(card U) ≤ ↑(card (x' * A)) / ↑(card x')
⊢ ↑(card (A * C) * card B) ≤ ↑(card (A * B) * card (B * C))
case inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
hB : Finset.Nonempty B
hB' : B ∈ erase (powerset B) ∅
U : Finset α
hU : Finset.Nonempty U ∧ U ⊆ B
hUA : ∀ (x' : Finset α), x' ∈ erase (powerset B) ∅ → ↑(card (U * A)) / ↑(card U) ≤ ↑(card (x' * A)) / ↑(card x')
⊢ card (A * C) * card B ≤ card (A * B) * card (B * C)
refine' cast_le.1 (_ : (_ : ℚ≥0) ≤ _)
case inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
hB : Finset.Nonempty B
hB' : B ∈ erase (powerset B) ∅
U : Finset α
hU : Finset.Nonempty U ∧ U ⊆ B
hUA : ∀ (x' : Finset α), x' ∈ erase (powerset B) ∅ → ↑(card (U * A)) / ↑(card U) ≤ ↑(card (x' * A)) / ↑(card x')
⊢ ↑(card (A * C)) * ↑(card B) ≤ ↑(card (A * B)) * ↑(card (B * C))
case inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
hB : Finset.Nonempty B
hB' : B ∈ erase (powerset B) ∅
U : Finset α
hU : Finset.Nonempty U ∧ U ⊆ B
hUA : ∀ (x' : Finset α), x' ∈ erase (powerset B) ∅ → ↑(card (U * A)) / ↑(card U) ≤ ↑(card (x' * A)) / ↑(card x')
⊢ ↑(card (A * C) * card B) ≤ ↑(card (A * B) * card (B * C))
push_cast
case inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
hB : Finset.Nonempty B
hB' : B ∈ erase (powerset B) ∅
U : Finset α
hU : Finset.Nonempty U ∧ U ⊆ B
hUA : ∀ (x' : Finset α), x' ∈ erase (powerset B) ∅ → ↑(card (U * A)) / ↑(card U) ≤ ↑(card (x' * A)) / ↑(card x')
⊢ ↑(card (A * C)) ≤ ↑(card (A * B)) * ↑(card (B * C)) / ↑(card B)
case inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
hB : Finset.Nonempty B
hB' : B ∈ erase (powerset B) ∅
U : Finset α
hU : Finset.Nonempty U ∧ U ⊆ B
hUA : ∀ (x' : Finset α), x' ∈ erase (powerset B) ∅ → ↑(card (U * A)) / ↑(card U) ≤ ↑(card (x' * A)) / ↑(card x')
⊢ ↑(card (A * C)) * ↑(card B) ≤ ↑(card (A * B)) * ↑(card (B * C))
refine' (le_div_iff <| cast_pos.2 hB.card_pos).1 _
case inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
hB : Finset.Nonempty B
hB' : B ∈ erase (powerset B) ∅
U : Finset α
hU : Finset.Nonempty U ∧ U ⊆ B
hUA : ∀ (x' : Finset α), x' ∈ erase (powerset B) ∅ → ↑(card (U * A)) / ↑(card U) ≤ ↑(card (x' * A)) / ↑(card x')
⊢ ↑(card (A * C)) ≤ ↑(card (B * A)) / ↑(card B) * ↑(card (B * C))
case inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
hB : Finset.Nonempty B
hB' : B ∈ erase (powerset B) ∅
U : Finset α
hU : Finset.Nonempty U ∧ U ⊆ B
hUA : ∀ (x' : Finset α), x' ∈ erase (powerset B) ∅ → ↑(card (U * A)) / ↑(card U) ≤ ↑(card (x' * A)) / ↑(card x')
⊢ ↑(card (A * C)) ≤ ↑(card (A * B)) * ↑(card (B * C)) / ↑(card B)
rw [mul_div_right_comm, mul_comm _ B]
case inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
hB : Finset.Nonempty B
hB' : B ∈ erase (powerset B) ∅
U : Finset α
hU : Finset.Nonempty U ∧ U ⊆ B
hUA : ∀ (x' : Finset α), x' ∈ erase (powerset B) ∅ → ↑(card (U * A)) / ↑(card U) ≤ ↑(card (x' * A)) / ↑(card x')
⊢ ↑(card (U * (A * C))) ≤ ↑(card (B * A)) / ↑(card B) * ↑(card (B * C))
case inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
hB : Finset.Nonempty B
hB' : B ∈ erase (powerset B) ∅
U : Finset α
hU : Finset.Nonempty U ∧ U ⊆ B
hUA : ∀ (x' : Finset α), x' ∈ erase (powerset B) ∅ → ↑(card (U * A)) / ↑(card U) ≤ ↑(card (x' * A)) / ↑(card x')
⊢ ↑(card (A * C)) ≤ ↑(card (B * A)) / ↑(card B) * ↑(card (B * C))
refine' (cast_le.2 <| card_le_card_mul_left _ hU.1).trans _
case inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
hB : Finset.Nonempty B
hB' : B ∈ erase (powerset B) ∅
U : Finset α
hU : Finset.Nonempty U ∧ U ⊆ B
hUA : ∀ (x' : Finset α), x' ∈ erase (powerset B) ∅ → ↑(card (U * A)) / ↑(card U) ≤ ↑(card (x' * A)) / ↑(card x')
⊢ ↑(card (U * (A * C))) ≤ ↑(card (U * A)) / ↑(card U) * ↑(card (U * C))
case inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
hB : Finset.Nonempty B
hB' : B ∈ erase (powerset B) ∅
U : Finset α
hU : Finset.Nonempty U ∧ U ⊆ B
hUA : ∀ (x' : Finset α), x' ∈ erase (powerset B) ∅ → ↑(card (U * A)) / ↑(card U) ≤ ↑(card (x' * A)) / ↑(card x')
⊢ ↑(card (U * (A * C))) ≤ ↑(card (B * A)) / ↑(card B) * ↑(card (B * C))
refine' le_trans _
  (mul_le_mul (hUA _ hB') (cast_le.2 <| card_le_of_subset <| mul_subset_mul_right hU.2)
    (zero_le _) (zero_le _))
case inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
hB : Finset.Nonempty B
hB' : B ∈ erase (powerset B) ∅
U : Finset α
hU : Finset.Nonempty U ∧ U ⊆ B
hUA : ∀ (x' : Finset α), x' ∈ erase (powerset B) ∅ → ↑(card (U * A)) / ↑(card U) ≤ ↑(card (x' * A)) / ↑(card x')
⊢ ↑(card (U * A * C)) ≤ ↑(card (U * A)) * ↑(card (U * C)) / ↑(card U)
case inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
hB : Finset.Nonempty B
hB' : B ∈ erase (powerset B) ∅
U : Finset α
hU : Finset.Nonempty U ∧ U ⊆ B
hUA : ∀ (x' : Finset α), x' ∈ erase (powerset B) ∅ → ↑(card (U * A)) / ↑(card U) ≤ ↑(card (x' * A)) / ↑(card x')
⊢ ↑(card (U * (A * C))) ≤ ↑(card (U * A)) / ↑(card U) * ↑(card (U * C))
rw [← mul_div_right_comm, ← mul_assoc]
case inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
hB : Finset.Nonempty B
hB' : B ∈ erase (powerset B) ∅
U : Finset α
hU : Finset.Nonempty U ∧ U ⊆ B
hUA : ∀ (x' : Finset α), x' ∈ erase (powerset B) ∅ → ↑(card (U * A)) / ↑(card U) ≤ ↑(card (x' * A)) / ↑(card x')
⊢ ↑(card (U * A * C)) * ↑(card U) ≤ ↑(card (U * A)) * ↑(card (U * C))
case inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
hB : Finset.Nonempty B
hB' : B ∈ erase (powerset B) ∅
U : Finset α
hU : Finset.Nonempty U ∧ U ⊆ B
hUA : ∀ (x' : Finset α), x' ∈ erase (powerset B) ∅ → ↑(card (U * A)) / ↑(card U) ≤ ↑(card (x' * A)) / ↑(card x')
⊢ ↑(card (U * A * C)) ≤ ↑(card (U * A)) * ↑(card (U * C)) / ↑(card U)
refine' (le_div_iff <| cast_pos.2 hU.1.card_pos).2 _
no goals
case inr.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
hB : Finset.Nonempty B
hB' : B ∈ erase (powerset B) ∅
U : Finset α
hU : Finset.Nonempty U ∧ U ⊆ B
hUA : ∀ (x' : Finset α), x' ∈ erase (powerset B) ∅ → ↑(card (U * A)) / ↑(card U) ≤ ↑(card (x' * A)) / ↑(card x')
⊢ ↑(card (U * A * C)) * ↑(card U) ≤ ↑(card (U * A)) * ↑(card (U * C))
exact_mod_cast mul_pluennecke_petridis C (mul_aux hU.1 hU.2 hUA)
no goals
case inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B C✝ A C : Finset α
⊢ card (A * C) * card ∅ ≤ card (A * ∅) * card (∅ * C)
simp