α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hA : Finset.Nonempty A
hAB : A ⊆ B
h : ∀ (A' : Finset α), A' ∈ erase (powerset B) ∅ → ↑(card (A * C)) / ↑(card A) ≤ ↑(card (A' * C)) / ↑(card A')
A' : Finset α
hAA' : A' ⊆ A
⊢ card (A * C) * card A' ≤ card (A' * C) * card A
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hA : Finset.Nonempty A
hAB : A ⊆ B
h : ∀ (A' : Finset α), A' ∈ erase (powerset B) ∅ → ↑(card (A * C)) / ↑(card A) ≤ ↑(card (A' * C)) / ↑(card A')
⊢ ∀ (A' : Finset α), A' ⊆ A → card (A * C) * card A' ≤ card (A' * C) * card A
rintro A' hAA'
case inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hA : Finset.Nonempty A
hAB : A ⊆ B
h : ∀ (A' : Finset α), A' ∈ erase (powerset B) ∅ → ↑(card (A * C)) / ↑(card A) ≤ ↑(card (A' * C)) / ↑(card A')
hAA' : ∅ ⊆ A
⊢ card (A * C) * card ∅ ≤ card (∅ * C) * card A

case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hA : Finset.Nonempty A
hAB : A ⊆ B
h : ∀ (A' : Finset α), A' ∈ erase (powerset B) ∅ → ↑(card (A * C)) / ↑(card A) ≤ ↑(card (A' * C)) / ↑(card A')
A' : Finset α
hAA' : A' ⊆ A
hA' : Finset.Nonempty A'
⊢ card (A * C) * card A' ≤ card (A' * C) * card A
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hA : Finset.Nonempty A
hAB : A ⊆ B
h : ∀ (A' : Finset α), A' ∈ erase (powerset B) ∅ → ↑(card (A * C)) / ↑(card A) ≤ ↑(card (A' * C)) / ↑(card A')
A' : Finset α
hAA' : A' ⊆ A
⊢ card (A * C) * card A' ≤ card (A' * C) * card A
obtain rfl | hA' := A'.eq_empty_or_nonempty
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hA : Finset.Nonempty A
hAB : A ⊆ B
h : ∀ (A' : Finset α), A' ∈ erase (powerset B) ∅ → ↑(card (A * C)) / ↑(card A) ≤ ↑(card (A' * C)) / ↑(card A')
A' : Finset α
hAA' : A' ⊆ A
hA' : Finset.Nonempty A'
hA₀ : 0 < ↑(card A)
⊢ card (A * C) * card A' ≤ card (A' * C) * card A
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hA : Finset.Nonempty A
hAB : A ⊆ B
h : ∀ (A' : Finset α), A' ∈ erase (powerset B) ∅ → ↑(card (A * C)) / ↑(card A) ≤ ↑(card (A' * C)) / ↑(card A')
A' : Finset α
hAA' : A' ⊆ A
hA' : Finset.Nonempty A'
⊢ card (A * C) * card A' ≤ card (A' * C) * card A
have hA₀ : (0 : ℚ≥0) < A.card := cast_pos.2 hA.card_pos
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hA : Finset.Nonempty A
hAB : A ⊆ B
h : ∀ (A' : Finset α), A' ∈ erase (powerset B) ∅ → ↑(card (A * C)) / ↑(card A) ≤ ↑(card (A' * C)) / ↑(card A')
A' : Finset α
hAA' : A' ⊆ A
hA' : Finset.Nonempty A'
hA₀ : 0 < ↑(card A)
hA₀' : 0 < ↑(card A')
⊢ card (A * C) * card A' ≤ card (A' * C) * card A
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hA : Finset.Nonempty A
hAB : A ⊆ B
h : ∀ (A' : Finset α), A' ∈ erase (powerset B) ∅ → ↑(card (A * C)) / ↑(card A) ≤ ↑(card (A' * C)) / ↑(card A')
A' : Finset α
hAA' : A' ⊆ A
hA' : Finset.Nonempty A'
hA₀ : 0 < ↑(card A)
⊢ card (A * C) * card A' ≤ card (A' * C) * card A
have hA₀' : (0 : ℚ≥0) < A'.card := cast_pos.2 hA'.card_pos
no goals
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hA : Finset.Nonempty A
hAB : A ⊆ B
h : ∀ (A' : Finset α), A' ∈ erase (powerset B) ∅ → ↑(card (A * C)) / ↑(card A) ≤ ↑(card (A' * C)) / ↑(card A')
A' : Finset α
hAA' : A' ⊆ A
hA' : Finset.Nonempty A'
hA₀ : 0 < ↑(card A)
hA₀' : 0 < ↑(card A')
⊢ card (A * C) * card A' ≤ card (A' * C) * card A
exact_mod_cast
  (div_le_div_iff hA₀ hA₀').1
    (h _ <| mem_erase_of_ne_of_mem hA'.ne_empty <| mem_powerset.2 <| hAA'.trans hAB)
no goals
case inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hA : Finset.Nonempty A
hAB : A ⊆ B
h : ∀ (A' : Finset α), A' ∈ erase (powerset B) ∅ → ↑(card (A * C)) / ↑(card A) ≤ ↑(card (A' * C)) / ↑(card A')
hAA' : ∅ ⊆ A
⊢ card (A * C) * card ∅ ≤ card (∅ * C) * card A
simp