-- Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean
@[to_additive]
private lemma card_mul_pow_le (hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A) (n : ℕ) :
    #(A * B ^ n) ≤ (#(A * B) / #A : ℚ≥0) ^ n * #A

Proof state:
case inr.succ
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
hA : A.Nonempty
n : ℕ
ih : ↑(#(A * B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ n * ↑(#A)
⊢ ↑(#(A * B ^ (n + 1))) * ↑(#A) ≤ (↑(#(A * B)) / ↑(#A)) ^ (n + 1) * ↑(#A) * ↑(#A)

Tactic:
calc
  ((#(A * B ^ (n + 1))) * #A : ℚ≥0)
    = #(A * B * B ^ n) * #A := by rw [_root_.pow_succ', ← mul_assoc]
  _ ≤ #(A * B) * #(A * B ^ n) := mod_cast pluennecke_petridis_inequality_mul _ hAB
  _ ≤ #(A * B) * ((#(A * B) / #A) ^ n * #A) := by gcongr
  _ = (#(A * B) / #A) ^ (n + 1) * #A * #A := by field_simp; ring

Result:
no goals

Proof state:
case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
n : ℕ
hA : A.Nonempty
⊢ ↑(#(A * B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ n * ↑(#A)

Tactic:
induction n with
| zero => simp
| succ n ih =>
  refine le_of_mul_le_mul_right ?_ (by positivity : (0 : ℚ≥0) < #A)
  calc
    ((#(A * B ^ (n + 1))) * #A : ℚ≥0)
      = #(A * B * B ^ n) * #A := by rw [_root_.pow_succ', ← mul_assoc]
    _ ≤ #(A * B) * #(A * B ^ n) := mod_cast pluennecke_petridis_inequality_mul _ hAB
    _ ≤ #(A * B) * ((#(A * B) / #A) ^ n * #A) := by gcongr
    _ = (#(A * B) / #A) ^ (n + 1) * #A * #A := by field_simp; ring

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
hA : A.Nonempty
n : ℕ
ih : ↑(#(A * B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ n * ↑(#A)
⊢ ↑(#(A * B)) * ↑(#(A * B ^ n)) ≤ ↑(#(A * B)) * ((↑(#(A * B)) / ↑(#A)) ^ n * ↑(#A))

Tactic:
gcongr

Result:
no goals

Proof state:
case inr.succ
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
hA : A.Nonempty
n : ℕ
ih : ↑(#(A * B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ n * ↑(#A)
⊢ ↑(#(A * B ^ (n + 1))) ≤ (↑(#(A * B)) / ↑(#A)) ^ (n + 1) * ↑(#A)

Tactic:
refine le_of_mul_le_mul_right ?_ (by positivity : (0 : ℚ≥0) < #A)

Result:
case inr.succ
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
hA : A.Nonempty
n : ℕ
ih : ↑(#(A * B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ n * ↑(#A)
⊢ ↑(#(A * B ^ (n + 1))) * ↑(#A) ≤ (↑(#(A * B)) / ↑(#A)) ^ (n + 1) * ↑(#A) * ↑(#A)

Proof state:
case inr.zero
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
hA : A.Nonempty
⊢ ↑(#(A * B ^ 0)) ≤ (↑(#(A * B)) / ↑(#A)) ^ 0 * ↑(#A)

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
hA : A.Nonempty
n : ℕ
ih : ↑(#(A * B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ n * ↑(#A)
⊢ ↑(#(A * B ^ (n + 1))) * ↑(#A) = ↑(#(A * B * B ^ n)) * ↑(#A)

Tactic:
rw [_root_.pow_succ', ← mul_assoc]

Result:
no goals

Proof state:
case inl
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
B : Finset G
n : ℕ
hAB : ∀ A' ⊆ ∅, #(∅ * B) * #A' ≤ #(A' * B) * #∅
⊢ ↑(#(∅ * B ^ n)) ≤ (↑(#(∅ * B)) / ↑(#∅)) ^ n * ↑(#∅)

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
hA : A.Nonempty
n : ℕ
ih : ↑(#(A * B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ n * ↑(#A)
⊢ ↑(#(A * B)) * ((↑(#(A * B)) / ↑(#A)) ^ n * ↑(#A)) = (↑(#(A * B)) / ↑(#A)) ^ (n + 1) * ↑(#A) * ↑(#A)

Tactic:
field_simp

Result:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
hA : A.Nonempty
n : ℕ
ih : ↑(#(A * B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ n * ↑(#A)
⊢ ↑(#(A * B)) * (↑(#(A * B)) ^ n * ↑(#A)) * ↑(#A) ^ (n + 1) = ↑(#(A * B)) ^ (n + 1) * ↑(#A) * ↑(#A) * ↑(#A) ^ n

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
n : ℕ
⊢ ↑(#(A * B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ n * ↑(#A)

Tactic:
obtain rfl | hA := A.eq_empty_or_nonempty

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

case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
n : ℕ
hA : A.Nonempty
⊢ ↑(#(A * B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ n * ↑(#A)

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
hA : A.Nonempty
n : ℕ
ih : ↑(#(A * B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ n * ↑(#A)
⊢ ↑(#(A * B)) * (↑(#(A * B)) ^ n * ↑(#A)) * ↑(#A) ^ (n + 1) = ↑(#(A * B)) ^ (n + 1) * ↑(#A) * ↑(#A) * ↑(#A) ^ n

Tactic:
ring

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
hA : A.Nonempty
n : ℕ
ih : ↑(#(A * B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ n * ↑(#A)
⊢ 0 < ↑(#A)

Tactic:
positivity

Result:
no goals