-- Mathlib/Combinatorics/Additive/ApproximateSubgroup.lean
@[to_additive]
lemma pow_inter_pow_covBySMul_sq_inter_sq
    (hA : IsApproximateSubgroup K A) (hB : IsApproximateSubgroup L B) (hm : 2 ≤ m) (hn : 2 ≤ n) :
    CovBySMul G (K ^ (m - 1) * L ^ (n - 1)) (A ^ m ∩ B ^ n) (A ^ 2 ∩ B ^ 2)

Proof state:
case intro.intro.intro.intro.refine_2
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))
⊢ A ^ m ∩ B ^ n ⊆ ↑(Finset.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1))) • (A ^ 2 ∩ 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 <;> omega
  _ = ⋃ (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]

Result:
no goals

Proof state:
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))
⊢ ⋃ a ∈ F₁ ^ (m - 1), ⋃ b ∈ F₂ ^ (n - 1), f a b • (A ^ 2 ∩ B ^ 2) =
    ⋃ a ∈ ↑(F₁ ^ (m - 1)), ⋃ b ∈ ↑(F₂ ^ (n - 1)), f a b • (A ^ 2 ∩ B ^ 2)

Tactic:
simp_rw [Finset.mem_coe]

Result:
no goals

Proof state:
case intro.intro
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
⊢ CovBySMul G (K ^ (m - 1) * L ^ (n - 1)) (A ^ m ∩ B ^ n) (A ^ 2 ∩ B ^ 2)

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

Result:
case intro.intro.intro.intro
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
⊢ CovBySMul G (K ^ (m - 1) * L ^ (n - 1)) (A ^ m ∩ B ^ n) (A ^ 2 ∩ B ^ 2)

Proof state:
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))
⊢ ⋃ a ∈ F₁ ^ (m - 1), ⋃ b ∈ F₂ ^ (n - 1), f a b • (A ^ 2 ∩ B ^ 2) =
    ↑(Finset.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1))) * (A ^ 2 ∩ B ^ 2)

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

Result:
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))
⊢ ⋃ a ∈ F₁ ^ (m - 1), ⋃ b ∈ F₂ ^ (n - 1), f a b • (A ^ 2 ∩ B ^ 2) =
    ⋃ a ∈ ↑(F₁ ^ (m - 1)), ⋃ b ∈ ↑(F₂ ^ (n - 1)), f a b • (A ^ 2 ∩ B ^ 2)

Proof state:
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))
⊢ ⋃ 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

Result:
case h.h.h.h
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))
i✝³ : G
i✝² : i✝³ ∈ F₁ ^ (m - 1)
i✝¹ : G
i✝ : i✝¹ ∈ F₂ ^ (n - 1)
⊢ i✝³ • A ∩ i✝¹ • B ⊆ f i✝³ i✝¹ • (A⁻¹ * A ∩ (B⁻¹ * B))

Proof state:
case h.h.h.h
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))
i✝³ : G
i✝² : i✝³ ∈ F₁ ^ (m - 1)
i✝¹ : G
i✝ : i✝¹ ∈ F₂ ^ (n - 1)
⊢ i✝³ • A ∩ i✝¹ • B ⊆ f i✝³ i✝¹ • (A⁻¹ * A ∩ (B⁻¹ * B))

Tactic:
exact hf ..

Result:
no goals

Proof state:
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))
⊢ A ^ m ∩ B ^ n ⊆ ↑F₁ ^ (m - 1) * A ∩ (↑F₂ ^ (n - 1) * B)

Tactic:
gcongr <;> apply pow_subset_pow_mul_of_sq_subset_mul <;> norm_cast <;> omega

Result:
no goals

Proof state:
case intro.intro.intro.intro
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
⊢ CovBySMul G (K ^ (m - 1) * L ^ (n - 1)) (A ^ m ∩ B ^ n) (A ^ 2 ∩ B ^ 2)

Tactic:
have := hA.one_le

Result:
case intro.intro.intro.intro
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
⊢ CovBySMul G (K ^ (m - 1) * L ^ (n - 1)) (A ^ m ∩ B ^ n) (A ^ 2 ∩ B ^ 2)

Proof state:
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:
gcongr <;> exact mod_cast Finset.card_pow_le

Result:
no goals