mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
⊢ 0 ≤ ↑N ^ (↑(nValue N))⁻¹ / 2

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 2 ≤ N
⊢ (2 * dValue N - 1) ^ nValue N ≤ N

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
⊢ 1 < 4096

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
⊢ 0 < 2 ^ 12

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
⊢ ↑12 * log 2 ≤ log ↑N

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ (50 / 19) ^ 2 / ↑12 ≤ 0.6931471803

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
⊢ 0 < 4096

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
⊢ ↑N ^ (↑(nValue N))⁻¹ / rexp 1 < ↑(dValue N)

Tactic:
apply div_lt_floor _
  rw [← log_le_log_iff, log_rpow, mul_comm, ← div_eq_mul_inv, nValue]
  · grw [ceil_lt_mul]
    · rw [mul_comm, ← div_div, div_sqrt, le_div_iff₀]
      · norm_num [le_sqrt_log hN]
      · norm_num1
    · rw [cast_pos, lt_ceil, cast_zero, Real.sqrt_pos]
      refine log_pos ?_
      rw [one_lt_cast]
      exact hN.trans_lt' (by norm_num1)
    apply le_sqrt_of_sq_le
    have : (12 : ℕ) * log 2 ≤ log N := by
      rw [← log_rpow zero_lt_two, rpow_natCast]
      exact log_le_log (by positivity) (mod_cast hN)
    refine le_trans ?_ this
    rw [← div_le_iff₀']
    · exact log_two_gt_d9.le.trans' (by norm_num1)
    · norm_num1
  · rw [cast_pos]
    exact hN.trans_lt' (by norm_num1)
  · refine div_pos zero_lt_two ?_
    rw [sub_pos, div_lt_one (exp_pos _)]
    exact exp_one_gt_two
  positivity

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
⊢ ↑N ^ (↑(nValue N))⁻¹ / rexp 1 < ↑(dValue N)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
⊢ 2 ≤ 4096

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
⊢ 8 ≤ 4096

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
⊢ succ 0 ≤ 4096

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
⊢ 64 ≤ 4096

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
⊢ 2 ≤ 4096

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ (↑N ^ (↑(nValue N))⁻¹ / rexp 1) ^ (n - 2) / ↑n < ↑(dValue N) ^ (n - 2) / ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: case refine_1.refine_1
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
a : G
ha : a ∈ A
c : G
hc : c ∈ C
hx : a / c ∈ A / C
b : G
hb : b ∈ ↑B
⊢ (fun b ↦ (a / b, c / b)) b ∈ (A / B) ×ˢ (C / B) ∧
    match (fun b ↦ (a / b, c / b)) b with
    | (a_1, c_1) => a_1 / c_1 = a / c

Tactic:
exact ⟨mk_mem_product (div_mem_div ha hb) (div_mem_div hc hb), div_div_div_cancel_right ..⟩

Goal state after:
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
⊢ #(A / C) * #B ≤ #(A / B) * #(C / B)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
⊢ #(A * C⁻¹) * #B ≤ #(A * B⁻¹) * #(C * B⁻¹)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
⊢ #B * #(A⁻¹ * C) ≤ #(B⁻¹ * A) * #(B⁻¹ * C)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
⊢ #(A / C) * #B ≤ #(A * B) * #(C * B)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
⊢ #(A * C⁻¹) * #B ≤ #(A * B) * #(C * B)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
⊢ #B * #(A⁻¹ * C) ≤ #(B * A) * #(B * C)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
⊢ #B * #(A * C) ≤ #(B / A) * #(B * C)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
⊢ #B * #(A * C) ≤ #(B * A⁻¹) * #(B * C)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
⊢ #(A * C) * #B ≤ #(A * B) * #(C⁻¹ * B)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
⊢ {x} * A' = {x} * A ∩ (C * A)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
⊢ C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case h₁
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ 2 * √(log ↑N) ≤ 2 * ↑n

Tactic:
gcongr
      apply le_ceil

Goal state after:
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
⊢ {x} * A' * B ⊆ {x} * A * B

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ 1 < 4096

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
⊢ ↑N * rexp (-4 * √(log ↑N)) < ↑(rothNumberNat N)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
⊢ #(C' * A * B) * #A ≤ (#(C * A * B) + #(A * B) - #(A' * B)) * #A

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: ⊢ 4 / ↑6 ≤ 0.6931471803

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: ⊢ rexp 4 < 64

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: ⊢ 4096 < rexp 16

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 1 ≤ N
hN' : N ≤ 4096
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
⊢ (#(C * A * B) + #(A * B) - #(A' * B)) * #A = #(C * A * B) * #A + #(A * B) * #A - #(A' * B) * #A

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ ↑(rothNumberNat N)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A : Set G
K : ℝ
hA : IsApproximateSubgroup K A
F : Finset G
hF : ↑(#F) ≤ K
hSF : A ^ 2 ⊆ ↑F • A
⊢ F.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A : Set G
K : ℝ
hA : IsApproximateSubgroup K A
⊢ 1 ≤ K

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K ↑A
⊢ ↑(#(A ^ 0)) ≤ K ^ (0 - 1) * ↑(#A)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K ↑A
⊢ ↑(#(A ^ 1)) ≤ K ^ (1 - 1) * ↑(#A)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K ↑A
n : ℕ
F : Finset G
hF : ↑(#F) ≤ K
hSF : ↑A ^ 2 ⊆ ↑F • ↑A
⊢ n + 2 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K ↑A
n : ℕ
F : Finset G
hF : ↑(#F) ≤ K
hSF : ↑A ^ 2 ⊆ ↑F • ↑A
⊢ ↑(#(A ^ (n + 2))) ≤ ↑(#(F ^ (n + 1) * A))

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
⊢ #(C * A * B) * #A + #(A * B) * #A - #(A' * B) * #A ≤
    #(A * B) * #(C * A) + #(A * B) * #A - #(A * B) * #(A ∩ ({x}⁻¹ * C * A))

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K ↑A
n : ℕ
F : Finset G
hF : ↑(#F) ≤ K
hSF : ↑A ^ 2 ⊆ ↑F • ↑A
⊢ ↑(#(F ^ (n + 1))) * ↑(#A) ≤ ↑(#F) ^ (n + 1) * ↑(#A)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K ↑A
n : ℕ
F : Finset G
hF : ↑(#F) ≤ K
hSF : ↑A ^ 2 ⊆ ↑F • ↑A
⊢ ↑(#F) ^ (n + 1) * ↑(#A) ≤ K ^ (n + 1) * ↑(#A)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K ↑A
n : ℕ
⊢ ↑(#(A ^ (n + 2))) ≤ K ^ (n + 2 - 1) * ↑(#A)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K ↑A
⊢ ↑(#(A * A)) ≤ K * ↑(#A)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
A : Set G
K : ℝ
F : Type u_2
H : Type u_3
inst✝² : Group H
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
hA : IsApproximateSubgroup K A
⊢ (⇑f '' A)⁻¹ = ⇑f '' A

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
A : Set G
K : ℝ
F : Type u_2
H : Type u_3
inst✝² : Group H
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
hA : IsApproximateSubgroup K A
⊢ CovBySMul H K ((⇑f '' A) ^ 2) (⇑f '' A)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝² : Group G
S : Type u_2
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
H : S
⊢ ↑(#{1}) ≤ 1 ∧ ↑H ^ 2 ⊆ ↑{1} • ↑H

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ 1 ∈ ↑A ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ (↑A ^ 2)⁻¹ = ↑A ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ ↑(#(A ^ 4 * A)) = ↑(#(A ^ 5))

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ 3 ≤ 5

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
x y z : EInt
f : x ⟶ y
g : y ⟶ z
⊢ WithBotTop.rec (motive := fun {x} ↦
      (x ⟶ z) → (WithBotTop.rec 0 t.truncLT (𝟭 C) x ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) z))
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊥ ⟶ y) → (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊥ ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) y))
          (fun f ↦ 𝟙 (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊥)) (fun b f ↦ 0) (fun f ↦ 0) z f)
      (fun a f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (WithBotTop.coe a ⟶ y) →
            (WithBotTop.rec 0 t.truncLT (𝟭 C) (WithBotTop.coe a) ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) y))
          (fun f ↦ 0) (fun b f ↦ t.natTransTruncLTOfLE a b ⋯) (fun f ↦ t.truncLTι a) z f)
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊤ ⟶ y) → (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊤ ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) y)) (fun f ↦ 0) (fun b f ↦ 0)
          (fun f ↦ 𝟙 (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊤)) z f)
      x (f ≫ g) =
    WithBotTop.rec (motive := fun {x} ↦
        (x ⟶ y) → (WithBotTop.rec 0 t.truncLT (𝟭 C) x ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) y))
        (fun f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (⊥ ⟶ y) → (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊥ ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) y))
            (fun f ↦ 𝟙 (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊥)) (fun b f ↦ 0) (fun f ↦ 0) y f)
        (fun a f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (WithBotTop.coe a ⟶ y) →
              (WithBotTop.rec 0 t.truncLT (𝟭 C) (WithBotTop.coe a) ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) y))
            (fun f ↦ 0) (fun b f ↦ t.natTransTruncLTOfLE a b ⋯) (fun f ↦ t.truncLTι a) y f)
        (fun f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (⊤ ⟶ y) → (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊤ ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) y)) (fun f ↦ 0)
            (fun b f ↦ 0) (fun f ↦ 𝟙 (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊤)) y f)
        x f ≫
      WithBotTop.rec (motive := fun {x} ↦
        (x ⟶ z) → (WithBotTop.rec 0 t.truncLT (𝟭 C) x ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) z))
        (fun f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (⊥ ⟶ y) → (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊥ ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) y))
            (fun f ↦ 𝟙 (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊥)) (fun b f ↦ 0) (fun f ↦ 0) z f)
        (fun a f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (WithBotTop.coe a ⟶ y) →
              (WithBotTop.rec 0 t.truncLT (𝟭 C) (WithBotTop.coe a) ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) y))
            (fun f ↦ 0) (fun b f ↦ t.natTransTruncLTOfLE a b ⋯) (fun f ↦ t.truncLTι a) z f)
        (fun f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (⊤ ⟶ y) → (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊤ ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) y)) (fun f ↦ 0)
            (fun b f ↦ 0) (fun f ↦ 𝟙 (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊤)) z f)
        y g

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : ↑(#(A ^ 4 * A)) ≤ K ^ 3 * ↑(#A)
hA₀ : A.Nonempty
F : Finset G
hF : ↑(#F) ≤ K ^ 3
hAF : A ^ 4 ⊆ F * (A / A)
⊢ (↑A ^ 2) ^ 2 ⊆ ↑F • ↑A ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ CovBySMul G (K ^ 3) ((↑A ^ 2) ^ 2) (↑A ^ 2)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
i : EInt
⊢ (t.eTruncLT.obj i).Additive

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
F₁ : Finset G
hF₁ : ↑(#F₁) ≤ K
hAF₁ : A ^ 2 ⊆ ↑F₁ • A
F₂ : Finset G
hF₂ : ↑(#F₂) ≤ L
hBF₂ : B ^ 2 ⊆ ↑F₂ • B
this : 1 ≤ K
f : G → G → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ ↑(#(F₁ ^ (m - 1))) * ↑(#(F₂ ^ (n - 1))) ≤ ↑(#F₁) ^ (m - 1) * ↑(#F₂) ^ (n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
F₁ : Finset G
hF₁ : ↑(#F₁) ≤ K
hAF₁ : A ^ 2 ⊆ ↑F₁ • A
F₂ : Finset G
hF₂ : ↑(#F₂) ≤ L
hBF₂ : B ^ 2 ⊆ ↑F₂ • B
this : 1 ≤ K
f : G → G → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ ↑(#F₁) ^ (m - 1) * ↑(#F₂) ^ (n - 1) ≤ K ^ (m - 1) * L ^ (n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
x y : EInt
f : x ⟶ y
⊢ WithBotTop.rec (𝟭 C) t.truncGE 0 x ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
⊢ #(A * B) * #(C * A) + #(A * B) * #A - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) = #(A * B) * #(C' * A)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
⊢ #(C * A * B) * #A ≤ #(A * B) * #(C * A)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n : EInt
⊢ WithBotTop.rec (motive := fun {x} ↦
      (x ⟶ n) → (WithBotTop.rec (𝟭 C) t.truncGE 0 x ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 n))
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊥ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
          (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥)) (fun b f ↦ t.truncGEπ b) (fun f ↦ 0) n f)
      (fun a f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (WithBotTop.coe a ⟶ y) →
            (WithBotTop.rec (𝟭 C) t.truncGE 0 (WithBotTop.coe a) ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
          (fun f ↦ 0) (fun b f ↦ t.natTransTruncGEOfLE a b ⋯) (fun f ↦ 0) n f)
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊤ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y)) (fun f ↦ 0) (fun b f ↦ 0)
          (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤)) n f)
      n (𝟙 n) =
    𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 n)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hA : A.Nonempty
hAB : A ⊆ B
h : ∀ A' ∈ B.powerset.erase ∅, ↑(#(A * C)) / ↑(#A) ≤ ↑(#(A' * C)) / ↑(#A')
⊢ ∀ A' ⊆ A, #(A * C) * #A' ≤ #(A' * C) * #A

Tactic:
by

Goal state after: