awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
K : ℝ
F_1 : Type u_2
H : Type u_3
inst_1 : Group H
inst_2 : FunLike F_1 G H
inst_3 : MonoidHomClass F_1 G H
f : F_1
hA : IsApproximateSubgroup K A
F : Finset G
hF : (↑(#F) : ℝ) ≤ K
hAF : HPow.hPow (β := ℕ) A 2 ⊆ (↑F : Set G) • A
refine_1 : (↑(Finset.card.{u_3} (α := H) (Finset.image (⇑f : (a : G) → H) F)) : ℝ) ≤ K
refine_2 :
  HPow.hPow (α := Set H) (β := ℕ) ((⇑f : (a : G) → H) '' A) 2 ⊆
    HSMul.hSMul (β := Set H) (↑(Finset.image (⇑f : (a : G) → H) F) : Set H) ((⇑f : (a : G) → H) '' A)
⊢ CovBySMul H K (HPow.hPow (α := Set H) (β := ℕ) ((⇑f : (a : G) → H) '' A) 2) ((⇑f : (a : G) → H) '' A)

Tactic:
refine ⟨F.image f, ?_, ?_⟩
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
K : ℝ
F_1 : Type u_2
H : Type u_3
inst_1 : Group H
inst_2 : FunLike F_1 G H
inst_3 : MonoidHomClass F_1 G H
f : F_1
hA : IsApproximateSubgroup K A
F : Finset G
hF : (↑(#F) : ℝ) ≤ K
hAF : HPow.hPow (β := ℕ) A 2 ⊆ (↑F : Set G) • A
⊢ LE.le (α := ℝ) (↑(Finset.card.{u_3} (α := H) (Finset.image (⇑f : (a : G) → H) F)) : ℝ) (↑(#F) : ℝ)

Tactic:
mod_cast F.card_image_le

Premises used: cast, Nat.cast_le._simp_1, Finset.card_image_le, Eq.symm
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
K : ℝ
F_1 : Type u_2
H : Type u_3
inst_1 : Group H
inst_2 : FunLike F_1 G H
inst_3 : MonoidHomClass F_1 G H
f : F_1
hA : IsApproximateSubgroup K A
F : Finset G
hF : (↑(#F) : ℝ) ≤ K
hAF : HPow.hPow (β := ℕ) A 2 ⊆ (↑F : Set G) • A
⊢ (↑(#F) : ℝ) ≤ K

Tactic:
hF
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
K : ℝ
F_1 : Type u_2
H : Type u_3
inst_1 : Group H
inst_2 : FunLike F_1 G H
inst_3 : MonoidHomClass F_1 G H
f : F_1
hA : IsApproximateSubgroup K A
F : Finset G
hF : (↑(#F) : ℝ) ≤ K
hAF : HPow.hPow (β := ℕ) A 2 ⊆ (↑F : Set G) • A
⊢ (↑(Finset.card.{u_3} (α := H) (Finset.image (⇑f : (a : G) → H) F)) : ℝ) ≤ K

Tactic:
calc
        (#(F.image f) : ℝ) ≤ #F := mod_cast F.card_image_le
        _ ≤ K := hF

Premises used: Nat.cast, Finset.card_image_le, Finset.card, DFunLike.coe, Finset.image
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
K : ℝ
F_1 : Type u_2
H : Type u_3
inst_1 : Group H
inst_2 : FunLike F_1 G H
inst_3 : MonoidHomClass F_1 G H
f : F_1
hA : IsApproximateSubgroup K A
F : Finset G
hF : (↑(#F) : ℝ) ≤ K
hAF : HPow.hPow (β := ℕ) A 2 ⊆ (↑F : Set G) • A
refine_2 :
  Subset.{u_3} (α := Set H) ((⇑f : (a : G) → H) '' HPow.hPow (β := ℕ) A 2) ((⇑f : (a : G) → H) '' ((↑F : Set G) * A))
⊢ HPow.hPow (α := Set H) (β := ℕ) ((⇑f : (a : G) → H) '' A) 2 ⊆
    HSMul.hSMul (β := Set H) (↑(Finset.image (⇑f : (a : G) → H) F) : Set H) ((⇑f : (a : G) → H) '' A)

Tactic:
simp only [← Set.image_pow, Finset.coe_image, ← Set.image_mul, smul_eq_mul] at hAF ⊢

Premises used: Finset.coe_image, Set.image_mul, smul_eq_mul, Set.image_pow
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
K : ℝ
F_1 : Type u_2
H : Type u_3
inst_1 : Group H
inst_2 : FunLike F_1 G H
inst_3 : MonoidHomClass F_1 G H
f : F_1
hA : IsApproximateSubgroup K A
F : Finset G
hF : (↑(#F) : ℝ) ≤ K
hAF : HPow.hPow (β := ℕ) A 2 ⊆ (↑F : Set G) * A
⊢ Subset.{u_3} (α := Set H) ((⇑f : (a : G) → H) '' HPow.hPow (β := ℕ) A 2) ((⇑f : (a : G) → H) '' ((↑F : Set G) * A))

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
K : ℝ
F : Type u_2
H : Type u_3
inst_1 : Group H
inst_2 : FunLike F G H
inst_3 : MonoidHomClass F G H
f : F
hA : IsApproximateSubgroup K A
obtain :
  ∀ (F_1 : Finset G) (hF : (↑(#F_1) : ℝ) ≤ K) (hAF : HPow.hPow (β := ℕ) A 2 ⊆ (↑F_1 : Set G) • A),
    CovBySMul H K (HPow.hPow (α := Set H) (β := ℕ) ((⇑f : (a : G) → H) '' A) 2) ((⇑f : (a : G) → H) '' A)
refine_1 :
  ∀ (F_1 : Finset G) (hF : (↑(#F_1) : ℝ) ≤ K) (hAF : HPow.hPow (β := ℕ) A 2 ⊆ (↑F_1 : Set G) • A),
    (↑(Finset.card.{u_3} (α := H) (Finset.image (⇑f : (a : G) → H) F_1)) : ℝ) ≤ K
refine_2 refine_2₁ :
  ∀ (F_1 : Finset G) (hF : (↑(#F_1) : ℝ) ≤ K) (hAF : HPow.hPow (β := ℕ) A 2 ⊆ (↑F_1 : Set G) • A),
    HPow.hPow (α := Set H) (β := ℕ) ((⇑f : (a : G) → H) '' A) 2 ⊆
      HSMul.hSMul (β := Set H) (↑(Finset.image (⇑f : (a : G) → H) F_1) : Set H) ((⇑f : (a : G) → H) '' A)
⊢ CovBySMul H K (HPow.hPow (α := Set H) (β := ℕ) ((⇑f : (a : G) → H) '' A) 2) ((⇑f : (a : G) → H) '' A)

Tactic:
classical
    obtain ⟨F, hF, hAF⟩ := hA.sq_covBySMul
    refine ⟨F.image f, ?_, ?_⟩
    · calc
        (#(F.image f) : ℝ) ≤ #F := mod_cast F.card_image_le
        _ ≤ K := hF
    · simp only [← Set.image_pow, Finset.coe_image, ← Set.image_mul, smul_eq_mul] at hAF ⊢
      gcongr

Premises used: Finset.coe_image, Set.image_mul, IsApproximateSubgroup.sq_covBySMul, smul_eq_mul, Set.image_pow
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
S : Type u_2
inst_1 : SetLike S G
inst_2 : SubgroupClass S G
H : S
⊢ LE.le (α := ℝ) (↑(Finset.card (α := G) {1}) : ℝ) 1 ∧ HPow.hPow (β := ℕ) (↑H : Set G) 2 ⊆ (↑{1} : Set G) • (↑H : Set G)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
rw : HMul.hMul (α := G) 1 1 ∈ (↑A : Set G) * (↑A : Set G)
⊢ 1 ∈ HPow.hPow (β := ℕ) (↑A : Set G) 2

Tactic:
rw [sq, ← one_mul 1]

Premises used: sq, OfNat.ofNat, one_mul
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
⊢ HMul.hMul (α := G) 1 1 ∈ (↑A : Set G) * (↑A : Set G)

Tactic:
Set.mul_mem_mul hA₁ hA₁

Premises used: Set.Mem, Set.mul_mem_mul
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
⊢ HMul.hMul (α := G) 1 1 ∈ (↑A : Set G) * (↑A : Set G)

Tactic:
exact Set.mul_mem_mul hA₁ hA₁

Premises used: Set.mul_mem_mul
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
⊢ (HPow.hPow (β := ℕ) (↑A : Set G) 2)⁻¹ = HPow.hPow (β := ℕ) (↑A : Set G) 2

Tactic:
simp [← inv_pow, hAsymm, ← coe_inv]

Premises used: inv_pow, Finset.coe_inv
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
rw rw₁ : Eq (α := ℝ) (↑(#(A ^ HAdd.hAdd (α := ℕ) 4 1)) : ℝ) (↑(#(HPow.hPow (β := ℕ) A 5)) : ℝ)
⊢ Eq (α := ℝ) (↑(#(HPow.hPow (β := ℕ) A 4 * A)) : ℝ) (↑(#(HPow.hPow (β := ℕ) A 5)) : ℝ)

Tactic:
rw [← pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
⊢ LE.le (α := ℕ) 3 5

Tactic:
lia
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
⊢ (↑(#(HPow.hPow (β := ℕ) A 4 * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)

Tactic:
replace hA := calc (#(A ^ 4 * A) : ℝ)
      _ = #(A ^ 5) := by rw [← pow_succ]
      _ ≤ K ^ 3 * #A := small_pow_of_small_tripling (by lia) hA hAsymm
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : (↑(#(HPow.hPow (β := ℕ) A 4 * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
⊢ A.Nonempty

Tactic:
have hA₀ : A.Nonempty := ⟨1, hA₁⟩
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : (↑(#(HPow.hPow (β := ℕ) A 4 * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
hA₀ : A.Nonempty
obtain :
  ∀ (F : Finset G) (hF : (↑(#F) : ℝ) ≤ HPow.hPow (β := ℕ) K 3) (hAF : HPow.hPow (β := ℕ) A 4 ⊆ F * (A / A)),
    CovBySMul G (HPow.hPow (β := ℕ) K 3) (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑A : Set G) 2) 2)
      (HPow.hPow (β := ℕ) (↑A : Set G) 2)
⊢ CovBySMul G (HPow.hPow (β := ℕ) K 3) (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑A : Set G) 2) 2)
    (HPow.hPow (β := ℕ) (↑A : Set G) 2)

Tactic:
obtain ⟨F, -, hF, hAF⟩ := ruzsa_covering_mul hA₀ hA

Premises used: Finset.ruzsa_covering_mul
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : (↑(#(HPow.hPow (β := ℕ) A 4 * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
hA₀ : A.Nonempty
F : Finset G
hF : (↑(#F) : ℝ) ≤ HPow.hPow (β := ℕ) K 3
hAF : HPow.hPow (β := ℕ) A 4 ⊆ F * (A / A)
norm_cast : HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) A 2) 2 ≤ F • HPow.hPow (β := ℕ) A 2
⊢ HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑A : Set G) 2) 2 ⊆ (↑F : Set G) • HPow.hPow (β := ℕ) (↑A : Set G) 2

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : (↑(#(HPow.hPow (β := ℕ) A 4 * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
hA₀ : A.Nonempty
F : Finset G
hF : (↑(#F) : ℝ) ≤ HPow.hPow (β := ℕ) K 3
hAF : HPow.hPow (β := ℕ) A 4 ⊆ F * (A / A)
⊢ HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) A 2) 2 ≤ F • HPow.hPow (β := ℕ) A 2

Tactic:
simpa [div_eq_mul_inv, pow_succ, mul_assoc, hAsymm] using hAF

Premises used: pow_succ, mul_assoc, div_eq_mul_inv
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : (↑(#(HPow.hPow (β := ℕ) A 4 * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
hA₀ : A.Nonempty
F : Finset G
hF : (↑(#F) : ℝ) ≤ HPow.hPow (β := ℕ) K 3
hAF : HPow.hPow (β := ℕ) A 4 ⊆ F * (A / A)
⊢ CovBySMul G (HPow.hPow (β := ℕ) K 3) (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑A : Set G) 2) 2)
    (HPow.hPow (β := ℕ) (↑A : Set G) 2)

Tactic:
exact ⟨F, hF, by norm_cast; simpa [div_eq_mul_inv, pow_succ, mul_assoc, hAsymm] using hAF⟩
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
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
obtain :
  ∀ (F₁ : Finset G) (hF₁ : (↑(#F₁) : ℝ) ≤ K) (hAF₁ : HPow.hPow (β := ℕ) A 2 ⊆ (↑F₁ : Set G) • A),
    CovBySMul G (K ^ (m - 1) * L ^ (n - 1)) (A ^ m ∩ B ^ n) (HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2)
⊢ CovBySMul G (K ^ (m - 1) * L ^ (n - 1)) (A ^ m ∩ B ^ n) (HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2)

Tactic:
obtain ⟨F₁, hF₁, hAF₁⟩ := hA.sq_covBySMul

Premises used: IsApproximateSubgroup.sq_covBySMul
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
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₁ : HPow.hPow (β := ℕ) A 2 ⊆ (↑F₁ : Set G) • A
obtain :
  ∀ (F₂ : Finset G) (hF₂ : (↑(#F₂) : ℝ) ≤ L) (hBF₂ : HPow.hPow (β := ℕ) B 2 ⊆ (↑F₂ : Set G) • B),
    CovBySMul G (K ^ (m - 1) * L ^ (n - 1)) (A ^ m ∩ B ^ n) (HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2)
⊢ CovBySMul G (K ^ (m - 1) * L ^ (n - 1)) (A ^ m ∩ B ^ n) (HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2)

Tactic:
obtain ⟨F₂, hF₂, hBF₂⟩ := hB.sq_covBySMul

Premises used: IsApproximateSubgroup.sq_covBySMul
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
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₁ : HPow.hPow (β := ℕ) A 2 ⊆ (↑F₁ : Set G) • A
F₂ : Finset G
hF₂ : (↑(#F₂) : ℝ) ≤ L
hBF₂ : HPow.hPow (β := ℕ) B 2 ⊆ (↑F₂ : Set G) • B
⊢ 1 ≤ K

Tactic:
have := hA.one_le
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
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₁ : HPow.hPow (β := ℕ) A 2 ⊆ (↑F₁ : Set G) • A
F₂ : Finset G
hF₂ : (↑(#F₂) : ℝ) ≤ L
hBF₂ : HPow.hPow (β := ℕ) B 2 ⊆ (↑F₂ : Set G) • B
this : 1 ≤ K
choose :
  ∀ (f : (a b : G) → G) (hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))),
    CovBySMul G (K ^ (m - 1) * L ^ (n - 1)) (A ^ m ∩ B ^ n) (HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2)
⊢ CovBySMul G (K ^ (m - 1) * L ^ (n - 1)) (A ^ m ∩ B ^ n) (HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2)

Tactic:
choose f hf using exists_smul_inter_smul_subset_smul_inv_mul_inter_inv_mul A B

Premises used: Set.exists_smul_inter_smul_subset_smul_inv_mul_inter_inv_mul
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
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₁ : HPow.hPow (β := ℕ) A 2 ⊆ (↑F₁ : Set G) • A
F₂ : Finset G
hF₂ : (↑(#F₂) : ℝ) ≤ L
hBF₂ : HPow.hPow (β := ℕ) B 2 ⊆ (↑F₂ : Set G) • B
this : 1 ≤ K
f : (a b : G) → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ CovBySMul G (K ^ (m - 1) * L ^ (n - 1)) (A ^ m ∩ B ^ n) (HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2)

Tactic:
⟨.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1)), ?_, ?_⟩

Premises used: HSub.hSub, HPow.hPow, CovBySMul, And.intro, Exists.intro, OfNat.ofNat, Finset.image₂
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
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₁ : HPow.hPow (β := ℕ) A 2 ⊆ (↑F₁ : Set G) • A
F₂ : Finset G
hF₂ : (↑(#F₂) : ℝ) ≤ L
hBF₂ : HPow.hPow (β := ℕ) B 2 ⊆ (↑F₂ : Set G) • B
this : 1 ≤ K
f : (a b : G) → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
refine_1 : (↑(#(Finset.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1)))) : ℝ) ≤ K ^ (m - 1) * L ^ (n - 1)
refine_2 :
  A ^ m ∩ B ^ n ⊆
    (↑(Finset.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1))) : Set G) • (HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2)
⊢ CovBySMul G (K ^ (m - 1) * L ^ (n - 1)) (A ^ m ∩ B ^ n) (HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2)

Tactic:
refine ⟨.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1)), ?_, ?_⟩
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
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₁ : HPow.hPow (β := ℕ) A 2 ⊆ (↑F₁ : Set G) • A
F₂ : Finset G
hF₂ : (↑(#F₂) : ℝ) ≤ L
hBF₂ : HPow.hPow (β := ℕ) B 2 ⊆ (↑F₂ : Set G) • B
this : 1 ≤ K
f : (a b : G) → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ (↑(#(Finset.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1)))) : ℝ) ≤
    HMul.hMul (α := ℝ) (↑(#(F₁ ^ (m - 1))) : ℝ) (↑(#(F₂ ^ (n - 1))) : ℝ)

Tactic:
mod_cast Finset.card_image₂_le ..

Premises used: Nat.cast_mul._simp_1, congrArg, Finset.card_image₂_le, HSub.hSub, cast, Nat.cast_le._simp_1, LE.le, Nat.cast, HPow.hPow, Finset.card, OfNat.ofNat, Eq.symm, Eq.trans, Finset.image₂
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
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₁ : HPow.hPow (β := ℕ) A 2 ⊆ (↑F₁ : Set G) • A
F₂ : Finset G
hF₂ : (↑(#F₂) : ℝ) ≤ L
hBF₂ : HPow.hPow (β := ℕ) B 2 ⊆ (↑F₂ : Set G) • B
this : 1 ≤ K
f : (a b : G) → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
h₁ : (↑(#(F₁ ^ (m - 1))) : ℝ) ≤ HPow.hPow (α := ℝ) (↑(#F₁) : ℝ) (m - 1)
h₂ : (↑(#(F₂ ^ (n - 1))) : ℝ) ≤ HPow.hPow (α := ℝ) (↑(#F₂) : ℝ) (n - 1)
⊢ HMul.hMul (α := ℝ) (↑(#(F₁ ^ (m - 1))) : ℝ) (↑(#(F₂ ^ (n - 1))) : ℝ) ≤
    HPow.hPow (α := ℝ) (↑(#F₁) : ℝ) (m - 1) * HPow.hPow (α := ℝ) (↑(#F₂) : ℝ) (n - 1)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
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₁ : HPow.hPow (β := ℕ) A 2 ⊆ (↑F₁ : Set G) • A
F₂ : Finset G
hF₂ : (↑(#F₂) : ℝ) ≤ L
hBF₂ : HPow.hPow (β := ℕ) B 2 ⊆ (↑F₂ : Set G) • B
this : 1 ≤ K
f : (a b : G) → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ (↑(#(F₁ ^ (m - 1))) : ℝ) ≤ HPow.hPow (α := ℝ) (↑(#F₁) : ℝ) (m - 1)

Tactic:
mod_cast Finset.card_pow_le

Premises used: Finset.card_pow_le, congrArg, HSub.hSub, cast, Nat.cast_le._simp_1, LE.le, Nat.cast, HPow.hPow, Finset.card, OfNat.ofNat, Eq.symm, Eq.trans, Nat.cast_pow._simp_1
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
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₁ : HPow.hPow (β := ℕ) A 2 ⊆ (↑F₁ : Set G) • A
F₂ : Finset G
hF₂ : (↑(#F₂) : ℝ) ≤ L
hBF₂ : HPow.hPow (β := ℕ) B 2 ⊆ (↑F₂ : Set G) • B
this : 1 ≤ K
f : (a b : G) → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ (↑(#(F₁ ^ (m - 1))) : ℝ) ≤ HPow.hPow (α := ℝ) (↑(#F₁) : ℝ) (m - 1)

Tactic:
exact mod_cast Finset.card_pow_le

Premises used: Finset.card_pow_le
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
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₁ : HPow.hPow (β := ℕ) A 2 ⊆ (↑F₁ : Set G) • A
F₂ : Finset G
hF₂ : (↑(#F₂) : ℝ) ≤ L
hBF₂ : HPow.hPow (β := ℕ) B 2 ⊆ (↑F₂ : Set G) • B
this : 1 ≤ K
f : (a b : G) → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ (↑(#(F₂ ^ (n - 1))) : ℝ) ≤ HPow.hPow (α := ℝ) (↑(#F₂) : ℝ) (n - 1)

Tactic:
mod_cast Finset.card_pow_le

Premises used: Finset.card_pow_le, congrArg, HSub.hSub, cast, Nat.cast_le._simp_1, LE.le, Nat.cast, HPow.hPow, Finset.card, OfNat.ofNat, Eq.symm, Eq.trans, Nat.cast_pow._simp_1
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
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₁ : HPow.hPow (β := ℕ) A 2 ⊆ (↑F₁ : Set G) • A
F₂ : Finset G
hF₂ : (↑(#F₂) : ℝ) ≤ L
hBF₂ : HPow.hPow (β := ℕ) B 2 ⊆ (↑F₂ : Set G) • B
this : 1 ≤ K
f : (a b : G) → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ (↑(#(F₂ ^ (n - 1))) : ℝ) ≤ HPow.hPow (α := ℝ) (↑(#F₂) : ℝ) (n - 1)

Tactic:
exact mod_cast Finset.card_pow_le

Premises used: Finset.card_pow_le
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
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₁ : HPow.hPow (β := ℕ) A 2 ⊆ (↑F₁ : Set G) • A
F₂ : Finset G
hF₂ : (↑(#F₂) : ℝ) ≤ L
hBF₂ : HPow.hPow (β := ℕ) B 2 ⊆ (↑F₂ : Set G) • B
this : 1 ≤ K
f : (a b : G) → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
c0 : 0 ≤ HPow.hPow (α := ℝ) (↑(#F₂) : ℝ) (n - 1)
b0 : 0 ≤ K ^ (m - 1)
h₁ : LE.le (α := ℝ) 0 (↑(#F₁) : ℝ)
h₂ : LE.le (α := ℝ) 0 (↑(#F₂) : ℝ)
⊢ HPow.hPow (α := ℝ) (↑(#F₁) : ℝ) (m - 1) * HPow.hPow (α := ℝ) (↑(#F₂) : ℝ) (n - 1) ≤ K ^ (m - 1) * L ^ (n - 1)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
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₁ : HPow.hPow (β := ℕ) A 2 ⊆ (↑F₁ : Set G) • A
F₂ : Finset G
hF₂ : (↑(#F₂) : ℝ) ≤ L
hBF₂ : HPow.hPow (β := ℕ) B 2 ⊆ (↑F₂ : Set G) • B
this : 1 ≤ K
f : (a b : G) → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
f₁ :
  HMul.hMul (α := ℝ) (↑(#(F₁ ^ (m - 1))) : ℝ) (↑(#(F₂ ^ (n - 1))) : ℝ) ≤
    HPow.hPow (α := ℝ) (↑(#F₁) : ℝ) (m - 1) * HPow.hPow (α := ℝ) (↑(#F₂) : ℝ) (n - 1)
f₂ : HPow.hPow (α := ℝ) (↑(#F₁) : ℝ) (m - 1) * HPow.hPow (α := ℝ) (↑(#F₂) : ℝ) (n - 1) ≤ K ^ (m - 1) * L ^ (n - 1)
⊢ (↑(#(Finset.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1)))) : ℝ) ≤ K ^ (m - 1) * L ^ (n - 1)

Tactic:
calc
      (#(.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1))) : ℝ)
      _ ≤ #(F₁ ^ (m - 1)) * #(F₂ ^ (n - 1)) := mod_cast Finset.card_image₂_le ..
      _ ≤ #F₁ ^ (m - 1) * #F₂ ^ (n - 1) := by gcongr <;> exact mod_cast Finset.card_pow_le
      _ ≤ K ^ (m - 1) * L ^ (n - 1) := by gcongr

Premises used: Finset.card_image₂_le, HSub.hSub, Nat.cast, HPow.hPow, Finset.card, OfNat.ofNat, Finset.image₂
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
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₁ : HPow.hPow (β := ℕ) A 2 ⊆ (↑F₁ : Set G) • A
F₂ : Finset G
hF₂ : (↑(#F₂) : ℝ) ≤ L
hBF₂ : HPow.hPow (β := ℕ) B 2 ⊆ (↑F₂ : Set G) • B
this : 1 ≤ K
f : (a b : G) → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
h₁ : A ^ m ⊆ (↑F₁ : Set G) ^ (m - 1) * A
h₂ : B ^ n ⊆ (↑F₂ : Set G) ^ (n - 1) * B
⊢ A ^ m ∩ B ^ n ⊆ (↑F₁ : Set G) ^ (m - 1) * A ∩ ((↑F₂ : Set G) ^ (n - 1) * B)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
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₁ : HPow.hPow (β := ℕ) A 2 ⊆ (↑F₁ : Set G) • A
F₂ : Finset G
hF₂ : (↑(#F₂) : ℝ) ≤ L
hBF₂ : HPow.hPow (β := ℕ) B 2 ⊆ (↑F₂ : Set G) • B
this : 1 ≤ K
f : (a b : G) → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
h₁ : HPow.hPow (β := ℕ) A 2 ⊆ (↑F₁ : Set G) * A
h₂ : m ≠ 0
⊢ A ^ m ⊆ (↑F₁ : Set G) ^ (m - 1) * A

Tactic:
apply pow_subset_pow_mul_of_sq_subset_mul

Premises used: Set.pow_subset_pow_mul_of_sq_subset_mul
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
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₁ : HPow.hPow (β := ℕ) A 2 ⊆ (↑F₁ : Set G) • A
F₂ : Finset G
hF₂ : (↑(#F₂) : ℝ) ≤ L
hBF₂ : HPow.hPow (β := ℕ) B 2 ⊆ (↑F₂ : Set G) • B
this : 1 ≤ K
f : (a b : G) → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
h₂ : HPow.hPow (β := ℕ) B 2 ⊆ (↑F₂ : Set G) * B
h₃ : n ≠ 0
⊢ B ^ n ⊆ (↑F₂ : Set G) ^ (n - 1) * B

Tactic:
apply pow_subset_pow_mul_of_sq_subset_mul

Premises used: Set.pow_subset_pow_mul_of_sq_subset_mul
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
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₁ : HPow.hPow (β := ℕ) A 2 ⊆ (↑F₁ : Set G) • A
F₂ : Finset G
hF₂ : (↑(#F₂) : ℝ) ≤ L
hBF₂ : HPow.hPow (β := ℕ) B 2 ⊆ (↑F₂ : Set G) • B
this : 1 ≤ K
f : (a b : G) → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ HPow.hPow (β := ℕ) A 2 ⊆ (↑F₁ : Set G) * A

Tactic:
norm_cast