awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (β := ℕ) B 2 ⊆ (↑F₂ : Set G) * B

Tactic:
norm_cast
-- 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))
⊢ ¬m = 0

Tactic:
lia
-- 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))
⊢ ¬n = 0

Tactic:
lia
-- 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))
simp_rw :
  Eq.{u_1 + 1} (α := Set G) (⋃ i₁ ∈ (↑F₁ : Set G) ^ (m - 1), ⋃ j₁ ∈ (↑F₂ : Set G) ^ (n - 1), i₁ • A ∩ j₁ • B)
    (⋃ a ∈ F₁ ^ (m - 1), ⋃ b ∈ F₂ ^ (n - 1), a • A ∩ b • B)
⊢ (↑F₁ : Set G) ^ (m - 1) * A ∩ ((↑F₂ : Set G) ^ (n - 1) * B) = ⋃ a ∈ F₁ ^ (m - 1), ⋃ b ∈ F₂ ^ (n - 1), a • A ∩ b • B

Tactic:
simp_rw [← smul_eq_mul, ← iUnion_smul_set, iUnion₂_inter_iUnion₂]

Premises used: Set.iUnion_smul_set, smul_eq_mul, Set.iUnion₂_inter_iUnion₂
-- 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))
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  Eq.{u_1 + 1} (α := Set G) (⋃ i₁ ∈ F₁ ^ (m - 1), ⋃ j₁ ∈ F₂ ^ (n - 1), i₁ • A ∩ j₁ • B)
    (⋃ a ∈ F₁ ^ (m - 1), ⋃ b ∈ F₂ ^ (n - 1), a • A ∩ b • B)
⊢ Eq.{u_1 + 1} (α := Set G) (⋃ i₁ ∈ (↑F₁ : Set G) ^ (m - 1), ⋃ j₁ ∈ (↑F₂ : Set G) ^ (n - 1), i₁ • A ∩ j₁ • B)
    (⋃ a ∈ F₁ ^ (m - 1), ⋃ b ∈ F₂ ^ (n - 1), a • A ∩ b • B)

Tactic:
norm_cast
-- 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 : ∀ i ∈ F₁ ^ (m - 1), ∀ i_2 ∈ F₂ ^ (n - 1), i • A ∩ i_2 • B ⊆ f i i_2 • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ Subset.{u_1} (α := Set G) (⋃ a ∈ F₁ ^ (m - 1), ⋃ b ∈ F₂ ^ (n - 1), a • A ∩ b • B)
    (⋃ a ∈ F₁ ^ (m - 1), ⋃ b ∈ F₂ ^ (n - 1), f a b • (A⁻¹ * A ∩ (B⁻¹ * 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))
i : G
i_1 : i ∈ F₁ ^ (m - 1)
i_2 : G
i_3 : i_2 ∈ F₂ ^ (n - 1)
⊢ i • A ∩ i_2 • B ⊆ f i i_2 • (A⁻¹ * A ∩ (B⁻¹ * B))

Tactic:
hf ..
-- 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))
i : G
i_1 : i ∈ F₁ ^ (m - 1)
i_2 : G
i_3 : i_2 ∈ F₂ ^ (n - 1)
⊢ i • A ∩ i_2 • B ⊆ f i i_2 • (A⁻¹ * A ∩ (B⁻¹ * B))

Tactic:
exact hf ..
-- 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))
simp_rw :
  ⋃ a ∈ F₁ ^ (m - 1), ⋃ b ∈ F₂ ^ (n - 1), f a b • (HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2) =
    (↑(Finset.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1))) : Set G) * (HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2)
⊢ ⋃ a ∈ F₁ ^ (m - 1), ⋃ b ∈ F₂ ^ (n - 1), f a b • (A⁻¹ * A ∩ (B⁻¹ * B)) =
    (↑(Finset.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1))) : Set G) * (HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2)

Tactic:
simp_rw [hA.inv_eq_self, hB.inv_eq_self, ← sq]

Premises used: IsApproximateSubgroup.inv_eq_self, sq
-- 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))
rw :
  Eq.{u_1 + 1} (α := Set G)
    (⋃ a ∈ F₁ ^ (m - 1), ⋃ b ∈ F₂ ^ (n - 1), f a b • (HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2))
    (⋃ a ∈ (↑(F₁ ^ (m - 1)) : Set G),
      ⋃ b ∈ (↑(F₂ ^ (n - 1)) : Set G), f a b • (HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2))
⊢ ⋃ a ∈ F₁ ^ (m - 1), ⋃ b ∈ F₂ ^ (n - 1), f a b • (HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2) =
    (↑(Finset.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1))) : Set G) * (HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2)

Tactic:
rw [Finset.coe_image₂, ← smul_eq_mul, ← iUnion_smul_set, biUnion_image2]

Premises used: Set.iUnion_smul_set, smul_eq_mul, Set.biUnion_image2, Finset.coe_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))
⊢ Eq.{u_1 + 1} (α := Set G)
    (⋃ a ∈ F₁ ^ (m - 1), ⋃ b ∈ F₂ ^ (n - 1), f a b • (HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2))
    (⋃ a ∈ (↑(F₁ ^ (m - 1)) : Set G),
      ⋃ b ∈ (↑(F₂ ^ (n - 1)) : Set G), f a b • (HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2))

Tactic:
simp_rw [Finset.mem_coe]

Premises used: Finset.mem_coe
-- 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))
A₁ : A ^ m ∩ B ^ n ⊆ (↑F₁ : Set G) ^ (m - 1) * A ∩ ((↑F₂ : Set G) ^ (n - 1) * B)
A₂ : (↑F₁ : Set G) ^ (m - 1) * A ∩ ((↑F₂ : Set G) ^ (n - 1) * B) = ⋃ a ∈ F₁ ^ (m - 1), ⋃ b ∈ F₂ ^ (n - 1), a • A ∩ b • B
A₃ :
  Subset.{u_1} (α := Set G) (⋃ a ∈ F₁ ^ (m - 1), ⋃ b ∈ F₂ ^ (n - 1), a • A ∩ b • B)
    (⋃ a ∈ F₁ ^ (m - 1), ⋃ b ∈ F₂ ^ (n - 1), f a b • (A⁻¹ * A ∩ (B⁻¹ * B)))
A₄ :
  ⋃ a ∈ F₁ ^ (m - 1), ⋃ b ∈ F₂ ^ (n - 1), f a b • (A⁻¹ * A ∩ (B⁻¹ * B)) =
    (↑(Finset.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1))) : Set G) * (HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2)
⊢ A ^ m ∩ B ^ n ⊆
    (↑(Finset.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1))) : Set G) • (HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2)

Tactic:
calc
      A ^ m ∩ B ^ n ⊆ (F₁ ^ (m - 1) * A) ∩ (F₂ ^ (n - 1) * B) := by
        gcongr <;> apply pow_subset_pow_mul_of_sq_subset_mul <;> norm_cast <;> lia
      _ = ⋃ (a ∈ F₁ ^ (m - 1)) (b ∈ F₂ ^ (n - 1)), a • A ∩ b • B := by
        simp_rw [← smul_eq_mul, ← iUnion_smul_set, iUnion₂_inter_iUnion₂]; norm_cast
      _ ⊆ ⋃ (a ∈ F₁ ^ (m - 1)) (b ∈ F₂ ^ (n - 1)), f a b • (A⁻¹ * A ∩ (B⁻¹ * B)) := by
        gcongr; exact hf ..
      _ = (Finset.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1))) * (A ^ 2 ∩ B ^ 2) := by
        simp_rw [hA.inv_eq_self, hB.inv_eq_self, ← sq]
        rw [Finset.coe_image₂, ← smul_eq_mul, ← iUnion_smul_set, biUnion_image2]
        simp_rw [Finset.mem_coe]

Premises used: HMul.hMul, HSub.hSub, Inter.inter, Inv.inv, SetLike.coe, HPow.hPow, 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
simp_rw : (A ^ m)⁻¹ ∩ (B ^ n)⁻¹ = A ^ m ∩ B ^ n
simp_rw₁ : A⁻¹ ^ m ∩ B⁻¹ ^ n = A ^ m ∩ B ^ n
simp_rw₂ : A ^ m ∩ B⁻¹ ^ n = A ^ m ∩ B ^ n
⊢ (A ^ m ∩ B ^ n)⁻¹ = A ^ m ∩ B ^ n

Tactic:
simp_rw [inter_inv, ← inv_pow, hA.inv_eq_self, hB.inv_eq_self]

Premises used: IsApproximateSubgroup.inv_eq_self, Set.inter_inv, inv_pow
-- 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
⊢ 2 ≤ 2 * m

Tactic:
lia
-- 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
⊢ 2 ≤ 2 * n

Tactic:
lia
-- 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
h₁ : 1 ∈ A
h₂ : 1 ∈ B
⊢ HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2 ⊆ A ^ m ∩ B ^ n

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
⊢ 1 ∈ A

Tactic:
hA.one_mem

Premises used: Set.Mem, IsApproximateSubgroup.one_mem
-- 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
⊢ 1 ∈ B

Tactic:
hB.one_mem

Premises used: Set.Mem, IsApproximateSubgroup.one_mem
-- 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
⊢ 1 ∈ A

Tactic:
exacts [hA.one_mem, hB.one_mem]

Premises used: IsApproximateSubgroup.one_mem
-- 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
refine : HPow.hPow (β := ℕ) (A ^ m ∩ B ^ n) 2 ⊆ A ^ (2 * m) ∩ B ^ (2 * n)
⊢ CovBySMul G (K ^ (2 * m - 1) * L ^ (2 * n - 1)) (HPow.hPow (β := ℕ) (A ^ m ∩ B ^ n) 2) (A ^ m ∩ B ^ n)

Tactic:
refine (hA.pow_inter_pow_covBySMul_sq_inter_sq hB (by lia) (by lia)).subset ?_
      (by gcongr; exacts [hA.one_mem, hB.one_mem])

Premises used: CovBySMul.subset, IsApproximateSubgroup.pow_inter_pow_covBySMul_sq_inter_sq
-- 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
⊢ HPow.hPow (β := ℕ) (A ^ m ∩ B ^ n) 2 ⊆ HPow.hPow (β := ℕ) (A ^ m) 2 ∩ HPow.hPow (β := ℕ) (B ^ n) 2

Tactic:
Set.inter_pow_subset

Premises used: Set.inter_pow_subset
-- 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
⊢ HPow.hPow (β := ℕ) (A ^ m) 2 ∩ HPow.hPow (β := ℕ) (B ^ n) 2 = A ^ (2 * m) ∩ B ^ (2 * n)

Tactic:
simp [pow_mul']

Premises used: pow_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
m₁ : HPow.hPow (β := ℕ) (A ^ m) 2 ∩ HPow.hPow (β := ℕ) (B ^ n) 2 = A ^ (2 * m) ∩ B ^ (2 * n)
⊢ HPow.hPow (β := ℕ) (A ^ m ∩ B ^ n) 2 ⊆ A ^ (2 * m) ∩ B ^ (2 * n)

Tactic:
calc
      (A ^ m ∩ B ^ n) ^ 2 ⊆ (A ^ m) ^ 2 ∩ (B ^ n) ^ 2 := Set.inter_pow_subset
      _ = A ^ (2 * m) ∩ B ^ (2 * n) := by simp [pow_mul']

Premises used: HMul.hMul, Set.inter_pow_subset, Inter.inter, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
this : A * A ⊆ A
x : G
hx : x ∈ A
rwa : x⁻¹ ∈ A⁻¹
rwa₁ rwa₂ rwa₃ rwa₄ : x ∈ A
⊢ x⁻¹ ∈ A

Tactic:
rwa [← hA.inv_eq_self, inv_mem_inv]

Premises used: Set.inv_mem_inv, IsApproximateSubgroup.inv_eq_self
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
suffices : A * A ⊆ A
⊢ ∃ (H : Subgroup G), (↑H : Set G) = A

Tactic:
suffices A * A ⊆ A from
      let H : Subgroup G :=
        { carrier := A
          one_mem' := hA.one_mem
          inv_mem' hx := by rwa [← hA.inv_eq_self, inv_mem_inv]
          mul_mem' hx hy := this (mul_mem_mul hx hy) }
      ⟨H, rfl⟩
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
obtain :
  ∀ (K : Finset G) (hK : LE.le (α := ℝ) (↑(#K) : ℝ) 1) (hKA : HPow.hPow (β := ℕ) A 2 ⊆ (↑K : Set G) • A),
    ∃ (x : G), A * A ⊆ x • A
⊢ ∃ (x : G), A * A ⊆ x • A

Tactic:
obtain ⟨K, hK, hKA⟩ := hA.sq_covBySMul

Premises used: IsApproximateSubgroup.sq_covBySMul
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
K : Finset G
hK : LE.le (α := ℝ) (↑(#K) : ℝ) 1
hKA : HPow.hPow (β := ℕ) A 2 ⊆ (↑K : Set G) • A
⊢ ∃ (x : G), K = ∅ ∨ K = {x}

Tactic:
simp only [Nat.cast_le_one, Finset.card_le_one_iff_subset_singleton,
        Finset.subset_singleton_iff] at hK

Premises used: Finset.card_le_one_iff_subset_singleton, Finset.subset_singleton_iff, Nat.cast_le_one
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
K : Finset G
hKA : HPow.hPow (β := ℕ) A 2 ⊆ (↑K : Set G) • A
hK : ∃ (x : G), K = ∅ ∨ K = {x}
inl : ∀ (x : G) (hKA : HPow.hPow (β := ℕ) A 2 ⊆ (↑∅ : Set G) • A), ∃ (x : G), A * A ⊆ x • A
inr : ∀ (x : G) (hKA : HPow.hPow (β := ℕ) A 2 ⊆ (↑{x} : Set G) • A), ∃ (x : G), A * A ⊆ x • A
⊢ ∃ (x : G), A * A ⊆ x • A

Tactic:
obtain ⟨x, rfl | rfl⟩ := hK

Premises used: rfl
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hKA : HPow.hPow (β := ℕ) A 2 ⊆ (↑∅ : Set G) • A
⊢ ∃ (x : G), A * A ⊆ x • A

Tactic:
simp [hA.nonempty.ne_empty] at hKA

Premises used: Set.Nonempty.ne_empty, IsApproximateSubgroup.nonempty
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hKA : HPow.hPow (β := ℕ) A 2 ⊆ (↑{x} : Set G) • A
⊢ A * A ⊆ x • A

Tactic:
rw [Finset.coe_singleton, singleton_smul, sq] at hKA

Premises used: Finset.coe_singleton, Set.singleton_smul, sq
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hKA : A * A ⊆ x • A
w : G
h : A * A ⊆ x • A
⊢ ∃ (x : G), A * A ⊆ x • A

Tactic:
use x
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
obtain : ∀ (x : G) (hx : A * A ⊆ x • A), A * A ⊆ A
⊢ A * A ⊆ A

Tactic:
obtain ⟨x, hx⟩ : ∃ x : G, A * A ⊆ x • A := by
      obtain ⟨K, hK, hKA⟩ := hA.sq_covBySMul
      simp only [Nat.cast_le_one, Finset.card_le_one_iff_subset_singleton,
        Finset.subset_singleton_iff] at hK
      obtain ⟨x, rfl | rfl⟩ := hK
      · simp [hA.nonempty.ne_empty] at hKA
      · rw [Finset.coe_singleton, singleton_smul, sq] at hKA
        use x
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
rwa rwa₁ rwa₂ rwa₃ : A * A ⊆ x • A
⊢ x⁻¹ • (A * A) ⊆ A

Tactic:
rwa [← subset_smul_set_iff]

Premises used: Set.subset_smul_set_iff
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
⊢ x⁻¹ • (A * A) ⊆ A

Tactic:
have hx' : x⁻¹ • (A * A) ⊆ A := by rwa [← subset_smul_set_iff]
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
hx' : x⁻¹ • (A * A) ⊆ A
⊢ x⁻¹ ∈ A

Tactic:
simpa using hx' (smul_mem_smul_set (mul_mem_mul hA.one_mem hA.one_mem))

Premises used: IsApproximateSubgroup.one_mem, Set.mul_mem_mul, Set.smul_mem_smul_set
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
hx' : x⁻¹ • (A * A) ⊆ A
⊢ x⁻¹ ∈ A

Tactic:
have hx_inv : x⁻¹ ∈ A := by
      simpa using hx' (smul_mem_smul_set (mul_mem_mul hA.one_mem hA.one_mem))
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
hx' : x⁻¹ • (A * A) ⊆ A
hx_inv : x⁻¹ ∈ A
rw : x * x ∈ A⁻¹
⊢ x * x ∈ A

Tactic:
rw [← hA.inv_eq_self]

Premises used: IsApproximateSubgroup.inv_eq_self
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
hx' : x⁻¹ • (A * A) ⊆ A
hx_inv : x⁻¹ ∈ A
⊢ x * x ∈ A⁻¹

Tactic:
simpa using hx' (smul_mem_smul_set (mul_mem_mul hx_inv hA.one_mem))

Premises used: IsApproximateSubgroup.one_mem, Set.mul_mem_mul, Set.smul_mem_smul_set
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
hx' : x⁻¹ • (A * A) ⊆ A
hx_inv : x⁻¹ ∈ A
⊢ x * x ∈ A

Tactic:
have hx_sq : x * x ∈ A := by
      rw [← hA.inv_eq_self]
      simpa using hx' (smul_mem_smul_set (mul_mem_mul hx_inv hA.one_mem))
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
hx' : x⁻¹ • (A * A) ⊆ A
hx_inv : x⁻¹ ∈ A
hx_sq : x * x ∈ A
⊢ A * A ⊆ x • A

Tactic:
assumption
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
hx' : x⁻¹ • (A * A) ⊆ A
hx_inv : x⁻¹ ∈ A
hx_sq : x * x ∈ A
⊢ x • A = x⁻¹ • (x * x) • A

Tactic:
simp [smul_smul]

Premises used: smul_smul
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
hx' : x⁻¹ • (A * A) ⊆ A
hx_inv : x⁻¹ ∈ A
hx_sq : x * x ∈ A
⊢ x⁻¹ • (x * x) • A ⊆ x⁻¹ • A • A

Tactic:
smul_set_mono (smul_set_subset_smul hx_sq)

Premises used: Set.smul_set_mono, Set.smul_set_subset_smul
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
hx' : x⁻¹ • (A * A) ⊆ A
hx_inv : x⁻¹ ∈ A
hx_sq : x * x ∈ A
⊢ x⁻¹ • A • A ⊆ A

Tactic:
hx'
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
hx' : x⁻¹ • (A * A) ⊆ A
hx_inv : x⁻¹ ∈ A
hx_sq : x * x ∈ A
calc : A * A ⊆ x • A
calc₁ : x • A = x⁻¹ • (x * x) • A
⊢ A * A ⊆ A

Tactic:
calc A * A ⊆ x • A := by assumption
      _ = x⁻¹ • (x * x) • A := by simp [smul_smul]
      _ ⊆ x⁻¹ • (A • A) := smul_set_mono (smul_set_subset_smul hx_sq)
      _ ⊆ A := hx'

Premises used: HMul.hMul, Set.smul_set_mono, Set.smul_set_subset_smul, HSMul.hSMul
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ IsApproximateSubgroup 1 (↑H : Set G)

Tactic:
.subgroup

Premises used: IsApproximateSubgroup.subgroup
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ IsApproximateSubgroup 1 (↑H : Set G)

Tactic:
exact .subgroup
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
x y : Finset α × Finset α
⊢ DevosMulRel x y ↔
    #(x.1 * x.2) < #(y.1 * y.2) ∨
      #(x.1 * x.2) = #(y.1 * y.2) ∧ #y.1 + #y.2 < #x.1 + #x.2 ∨
        #(x.1 * x.2) = #(y.1 * y.2) ∧ #x.1 + #x.2 = #y.1 + #y.2 ∧ #x.1 < #y.1

Tactic:
simp [DevosMulRel, Prod.lex_iff, and_or_left]

Premises used: and_or_left, _private.0.DevosMulRel, Prod.lex_iff
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
x y : Finset α × Finset α
mul : #(x.1 * x.2) ≤ #(y.1 * y.2)
hadd : #y.1 + #y.2 < #x.1 + #x.2
⊢ DevosMulRel x y

Tactic:
devosMulRel_iff.2 <| mul.lt_or_eq.imp_right fun h ↦ Or.inl ⟨h, hadd⟩

Premises used: Iff.mpr, _private.0.devosMulRel_iff, LE.le.lt_or_eq, And.intro, Or.inl, Or.imp_right
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
x y : Finset α × Finset α
mul : #(x.1 * x.2) ≤ #(y.1 * y.2)
hadd : #y.1 + #y.2 ≤ #x.1 + #x.2
hone : #x.1 < #y.1
⊢ DevosMulRel x y

Tactic:
devosMulRel_iff.2 <|
    mul.lt_or_eq.imp_right fun h ↦ hadd.lt_or_eq'.imp (And.intro h) fun h' ↦ ⟨h, h', hone⟩

Premises used: Iff.mpr, LE.le.lt_or_eq', _private.0.devosMulRel_iff, LE.le.lt_or_eq, And.intro, Or.imp, Or.imp_right
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
⊢ Set.WellFoundedOn.{u_2} (α := Finset α × Finset α) {x : Finset α × Finset α | x.1.Nonempty ∧ x.2.Nonempty} DevosMulRel

Tactic:
wellFounded_lt.onFun.wellFoundedOn.prod_lex_of_wellFoundedOn_fiber fun n ↦
    Set.WellFoundedOn.prod_lex_of_wellFoundedOn_fiber ?_ fun n ↦
      wellFounded_lt.onFun.wellFoundedOn

Premises used: WellFounded.wellFoundedOn, _private.0.DevosMulRel, wellFounded_lt, WellFounded.onFun, Set.WellFoundedOn.prod_lex_of_wellFoundedOn_fiber