case inl
α✝ : Type ?u.99967
inst✝³ : CommGroup α✝
inst✝² : DecidableEq α✝
A B✝ C : Finset α✝
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : DecidableEq α
B : Finset α
n : ℕ
hAB : ∀ (A' : Finset α), A' ⊆ ∅ → card (∅ + B) * card A' ≤ card (A' + B) * card ∅
⊢ ↑(card (∅ + n • B)) ≤ (↑(card (∅ + B)) / ↑(card ∅)) ^ n * ↑(card ∅)

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

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

case inr.succ
α✝ : Type ?u.99967
inst✝³ : CommGroup α✝
inst✝² : DecidableEq α✝
A✝ B✝ C : Finset α✝
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : DecidableEq α
A B : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A + B) * card A' ≤ card (A' + B) * card A
hA : Finset.Nonempty A
n : ℕ
ih : ↑(card (A + n • B)) ≤ (↑(card (A + B)) / ↑(card A)) ^ n * ↑(card A)
⊢ 0 < ↑(card A)
case inr.succ
α✝ : Type ?u.99967
inst✝³ : CommGroup α✝
inst✝² : DecidableEq α✝
A✝ B✝ C : Finset α✝
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : DecidableEq α
A B : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A + B) * card A' ≤ card (A' + B) * card A
hA : Finset.Nonempty A
n : ℕ
ih : ↑(card (A + n • B)) ≤ (↑(card (A + B)) / ↑(card A)) ^ n * ↑(card A)
⊢ ↑(card (A + succ n • B)) ≤ (↑(card (A + B)) / ↑(card A)) ^ succ n * ↑(card A)
rw [succ_nsmul, ← add_assoc, _root_.pow_succ, mul_assoc, ← mul_div_right_comm, le_div_iff,
  ← cast_mul]
case inr.succ
α✝ : Type ?u.99967
inst✝³ : CommGroup α✝
inst✝² : DecidableEq α✝
A✝ B✝ C : Finset α✝
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : DecidableEq α
A B : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A + B) * card A' ≤ card (A' + B) * card A
hA : Finset.Nonempty A
n : ℕ
ih : ↑(card (A + n • B)) ≤ (↑(card (A + B)) / ↑(card A)) ^ n * ↑(card A)
⊢ 0 < ↑(card A)

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

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

case inr.succ
α✝ : Type ?u.99967
inst✝³ : CommGroup α✝
inst✝² : DecidableEq α✝
A✝ B✝ C : Finset α✝
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : DecidableEq α
A B : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A + B) * card A' ≤ card (A' + B) * card A
hA : Finset.Nonempty A
n : ℕ
ih : ↑(card (A + n • B)) ≤ (↑(card (A + B)) / ↑(card A)) ^ n * ↑(card A)
⊢ ↑(card (A + B + n • B) * 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.99967
inst✝³ : CommGroup α✝
inst✝² : DecidableEq α✝
A✝ B✝ C : Finset α✝
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : DecidableEq α
A B : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A + B) * card A' ≤ card (A' + B) * card A
hA : Finset.Nonempty A
n : ℕ
ih : ↑(card (A + n • B)) ≤ (↑(card (A + B)) / ↑(card A)) ^ n * ↑(card A)
⊢ ↑(card (A + B) * card (A + n • B)) ≤ ↑(card (A + B)) * ((↑(card (A + B)) / ↑(card A)) ^ n * ↑(card A))
case inr.succ
α✝ : Type ?u.99967
inst✝³ : CommGroup α✝
inst✝² : DecidableEq α✝
A✝ B✝ C : Finset α✝
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : DecidableEq α
A B : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A + B) * card A' ≤ card (A' + B) * card A
hA : Finset.Nonempty A
n : ℕ
ih : ↑(card (A + n • B)) ≤ (↑(card (A + B)) / ↑(card A)) ^ n * ↑(card A)
⊢ ↑(card (A + B + n • B) * card A) ≤ ↑(card (A + B)) * ((↑(card (A + B)) / ↑(card A)) ^ n * ↑(card A))
refine' (cast_le.2 <| add_pluennecke_petridis _ hAB).trans _
case inr.succ
α✝ : Type ?u.99967
inst✝³ : CommGroup α✝
inst✝² : DecidableEq α✝
A✝ B✝ C : Finset α✝
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : DecidableEq α
A B : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A + B) * card A' ≤ card (A' + B) * card A
hA : Finset.Nonempty A
n : ℕ
ih : ↑(card (A + n • B)) ≤ (↑(card (A + B)) / ↑(card A)) ^ n * ↑(card A)
⊢ ↑(card (A + B)) * ↑(card (A + n • B)) ≤ ↑(card (A + B)) * ((↑(card (A + B)) / ↑(card A)) ^ n * ↑(card A))
case inr.succ
α✝ : Type ?u.99967
inst✝³ : CommGroup α✝
inst✝² : DecidableEq α✝
A✝ B✝ C : Finset α✝
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : DecidableEq α
A B : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A + B) * card A' ≤ card (A' + B) * card A
hA : Finset.Nonempty A
n : ℕ
ih : ↑(card (A + n • B)) ≤ (↑(card (A + B)) / ↑(card A)) ^ n * ↑(card A)
⊢ ↑(card (A + B) * card (A + n • B)) ≤ ↑(card (A + B)) * ((↑(card (A + B)) / ↑(card A)) ^ n * ↑(card A))
rw [cast_mul]
no goals
case inr.succ
α✝ : Type ?u.99967
inst✝³ : CommGroup α✝
inst✝² : DecidableEq α✝
A✝ B✝ C : Finset α✝
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : DecidableEq α
A B : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A + B) * card A' ≤ card (A' + B) * card A
hA : Finset.Nonempty A
n : ℕ
ih : ↑(card (A + n • B)) ≤ (↑(card (A + B)) / ↑(card A)) ^ n * ↑(card A)
⊢ ↑(card (A + B)) * ↑(card (A + n • B)) ≤ ↑(card (A + B)) * ((↑(card (A + B)) / ↑(card A)) ^ n * ↑(card A))
gcongr
no goals
case inl
α✝ : Type ?u.99967
inst✝³ : CommGroup α✝
inst✝² : DecidableEq α✝
A B✝ C : Finset α✝
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : DecidableEq α
B : Finset α
n : ℕ
hAB : ∀ (A' : Finset α), A' ⊆ ∅ → card (∅ + B) * card A' ≤ card (A' + B) * card ∅
⊢ ↑(card (∅ + n • B)) ≤ (↑(card (∅ + B)) / ↑(card ∅)) ^ n * ↑(card ∅)
simp
no goals
case inr.zero
α✝ : Type ?u.99967
inst✝³ : CommGroup α✝
inst✝² : DecidableEq α✝
A✝ B✝ C : Finset α✝
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : DecidableEq α
A B : Finset α
hAB : ∀ (A' : Finset α), A' ⊆ A → card (A + B) * card A' ≤ card (A' + B) * card A
hA : Finset.Nonempty A
⊢ ↑(card (A + zero • B)) ≤ (↑(card (A + B)) / ↑(card A)) ^ zero * ↑(card A)
simp