case inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
B C : Finset α
n : ℕ
hAB : ∀ (A' : Finset α), A' ⊆ ∅ → card (∅ * B) * card A' ≤ card (A' * B) * card ∅
⊢ ↑(card (∅ * B ^ n)) ≤ (↑(card (∅ * B)) / ↑(card ∅)) ^ n * ↑(card ∅)

case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
n : ℕ
hA : Finset.Nonempty A
⊢ ↑(card (A * B ^ n)) ≤ (↑(card (A * B)) / ↑(card A)) ^ n * ↑(card A)
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
n : ℕ
⊢ ↑(card (A * B ^ n)) ≤ (↑(card (A * B)) / ↑(card A)) ^ n * ↑(card A)
obtain rfl | hA := A.eq_empty_or_nonempty
case inr.zero
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
hA : Finset.Nonempty A
⊢ ↑(card (A * B ^ zero)) ≤ (↑(card (A * B)) / ↑(card A)) ^ zero * ↑(card A)

case inr.succ
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
hA : Finset.Nonempty A
n : ℕ
ih : ↑(card (A * B ^ n)) ≤ (↑(card (A * B)) / ↑(card A)) ^ n * ↑(card A)
⊢ ↑(card (A * B ^ succ n)) ≤ (↑(card (A * B)) / ↑(card A)) ^ succ n * ↑(card A)
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
n : ℕ
hA : Finset.Nonempty A
⊢ ↑(card (A * B ^ n)) ≤ (↑(card (A * B)) / ↑(card A)) ^ n * ↑(card A)
induction' n with n ih
case inr.succ
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
hA : Finset.Nonempty A
n : ℕ
ih : ↑(card (A * B ^ n)) ≤ (↑(card (A * B)) / ↑(card A)) ^ n * ↑(card A)
⊢ ↑(card (A * B * B ^ n) * card A) ≤ ↑(card (A * B)) * ((↑(card (A * B)) / ↑(card A)) ^ n * ↑(card A))

case inr.succ
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
hA : Finset.Nonempty A
n : ℕ
ih : ↑(card (A * B ^ n)) ≤ (↑(card (A * B)) / ↑(card A)) ^ n * ↑(card A)
⊢ 0 < ↑(card A)
case inr.succ
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
hA : Finset.Nonempty A
n : ℕ
ih : ↑(card (A * B ^ n)) ≤ (↑(card (A * B)) / ↑(card A)) ^ n * ↑(card A)
⊢ ↑(card (A * B ^ succ n)) ≤ (↑(card (A * B)) / ↑(card A)) ^ succ n * ↑(card A)
rw [_root_.pow_succ, ← mul_assoc, _root_.pow_succ, @mul_assoc ℚ≥0, ← mul_div_right_comm,
  le_div_iff, ← cast_mul]
case inr.succ
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
hA : Finset.Nonempty A
n : ℕ
ih : ↑(card (A * B ^ n)) ≤ (↑(card (A * B)) / ↑(card A)) ^ n * ↑(card A)
⊢ 0 < ↑(card A)

case inr.succ
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
hA : Finset.Nonempty A
n : ℕ
ih : ↑(card (A * B ^ n)) ≤ (↑(card (A * B)) / ↑(card A)) ^ n * ↑(card A)
⊢ ↑(card (A * B * B ^ n) * card A) ≤ ↑(card (A * B)) * ((↑(card (A * B)) / ↑(card A)) ^ n * ↑(card A))
case inr.succ
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
hA : Finset.Nonempty A
n : ℕ
ih : ↑(card (A * B ^ n)) ≤ (↑(card (A * B)) / ↑(card A)) ^ n * ↑(card A)
⊢ ↑(card (A * B * B ^ n) * card A) ≤ ↑(card (A * B)) * ((↑(card (A * B)) / ↑(card A)) ^ n * ↑(card A))

case inr.succ
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
hA : Finset.Nonempty A
n : ℕ
ih : ↑(card (A * B ^ n)) ≤ (↑(card (A * B)) / ↑(card A)) ^ n * ↑(card A)
⊢ 0 < ↑(card A)
swap
case inr.succ
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
hA : Finset.Nonempty A
n : ℕ
ih : ↑(card (A * B ^ n)) ≤ (↑(card (A * B)) / ↑(card A)) ^ n * ↑(card A)
⊢ ↑(card (A * B * B ^ n) * card A) ≤ ↑(card (A * B)) * ((↑(card (A * B)) / ↑(card A)) ^ n * ↑(card A))
case inr.succ
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
hA : Finset.Nonempty A
n : ℕ
ih : ↑(card (A * B ^ n)) ≤ (↑(card (A * B)) / ↑(card A)) ^ n * ↑(card A)
⊢ 0 < ↑(card A)

case inr.succ
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
hA : Finset.Nonempty A
n : ℕ
ih : ↑(card (A * B ^ n)) ≤ (↑(card (A * B)) / ↑(card A)) ^ n * ↑(card A)
⊢ ↑(card (A * B * B ^ n) * card A) ≤ ↑(card (A * B)) * ((↑(card (A * B)) / ↑(card A)) ^ n * ↑(card A))
exact cast_pos.2 hA.card_pos
case inr.succ
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
hA : Finset.Nonempty A
n : ℕ
ih : ↑(card (A * B ^ n)) ≤ (↑(card (A * B)) / ↑(card A)) ^ n * ↑(card A)
⊢ ↑(card (A * B) * card (A * B ^ n)) ≤ ↑(card (A * B)) * ((↑(card (A * B)) / ↑(card A)) ^ n * ↑(card A))
case inr.succ
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
hA : Finset.Nonempty A
n : ℕ
ih : ↑(card (A * B ^ n)) ≤ (↑(card (A * B)) / ↑(card A)) ^ n * ↑(card A)
⊢ ↑(card (A * B * B ^ n) * card A) ≤ ↑(card (A * B)) * ((↑(card (A * B)) / ↑(card A)) ^ n * ↑(card A))
refine' (cast_le.2 <| mul_pluennecke_petridis _ hAB).trans _
case inr.succ
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
hA : Finset.Nonempty A
n : ℕ
ih : ↑(card (A * B ^ n)) ≤ (↑(card (A * B)) / ↑(card A)) ^ n * ↑(card A)
⊢ ↑(card (A * B)) * ↑(card (A * B ^ n)) ≤ ↑(card (A * B)) * ((↑(card (A * B)) / ↑(card A)) ^ n * ↑(card A))
case inr.succ
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
hA : Finset.Nonempty A
n : ℕ
ih : ↑(card (A * B ^ n)) ≤ (↑(card (A * B)) / ↑(card A)) ^ n * ↑(card A)
⊢ ↑(card (A * B) * card (A * B ^ n)) ≤ ↑(card (A * B)) * ((↑(card (A * B)) / ↑(card A)) ^ n * ↑(card A))
rw [cast_mul]
no goals
case inr.succ
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
hA : Finset.Nonempty A
n : ℕ
ih : ↑(card (A * B ^ n)) ≤ (↑(card (A * B)) / ↑(card A)) ^ n * ↑(card A)
⊢ ↑(card (A * B)) * ↑(card (A * B ^ n)) ≤ ↑(card (A * B)) * ((↑(card (A * B)) / ↑(card A)) ^ n * ↑(card A))
gcongr
no goals
case inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
B C : Finset α
n : ℕ
hAB : ∀ (A' : Finset α), A' ⊆ ∅ → card (∅ * B) * card A' ≤ card (A' * B) * card ∅
⊢ ↑(card (∅ * B ^ n)) ≤ (↑(card (∅ * B)) / ↑(card ∅)) ^ n * ↑(card ∅)
simp
no goals
case inr.zero
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
hA : Finset.Nonempty A
⊢ ↑(card (A * B ^ zero)) ≤ (↑(card (A * B)) / ↑(card A)) ^ zero * ↑(card A)
simp