awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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) : ℝ)
⊢ Eq (α := ℝ) (↑(#(HPow.hPow (β := ℕ) A 4 * A)) : ℝ) (↑(#(HPow.hPow (β := ℕ) A 5)) : ℝ)
have rw : Eq (α := ℝ) (↑(#(A ^ HAdd.hAdd (α := ℕ) 4 1)) : ℝ) (↑(#(HPow.hPow (β := ℕ) A 5)) : ℝ)
Tactic: rw [← pow_succ]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (hypothesis)
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) : ℝ)
⊢ CovBySMul G (HPow.hPow (β := ℕ) K 3) (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑A : Set G) 2) 2)
    (HPow.hPow (β := ℕ) (↑A : Set G) 2)
have hA₂ : (↑(#(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
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (hypothesis)
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) : ℝ)
⊢ CovBySMul G (HPow.hPow (β := ℕ) K 3) (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑A : Set G) 2) 2)
    (HPow.hPow (β := ℕ) (↑A : Set G) 2)
have hA₀ : A.Nonempty
Tactic: have hA₀ : A.Nonempty := ⟨1, hA₁⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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
⊢ CovBySMul G (HPow.hPow (β := ℕ) K 3) (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑A : Set G) 2) 2)
    (HPow.hPow (β := ℕ) (↑A : Set G) 2)
have 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)
Tactic: obtain ⟨F, -, hF, hAF⟩ := ruzsa_covering_mul hA₀ hA
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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 : Set G) 2) 2 ⊆ (↑F : Set G) • HPow.hPow (β := ℕ) (↑A : Set G) 2
have norm_cast : HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) A 2) 2 ≤ F • HPow.hPow (β := ℕ) A 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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
⊢ CovBySMul G (K ^ (m - 1) * L ^ (n - 1)) (A ^ m ∩ B ^ n) (HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2)
have 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)
Tactic: obtain ⟨F₁, hF₁, hAF₁⟩ := hA.sq_covBySMul
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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
⊢ CovBySMul G (K ^ (m - 1) * L ^ (n - 1)) (A ^ m ∩ B ^ n) (HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2)
have 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)
Tactic: obtain ⟨F₂, hF₂, hBF₂⟩ := hB.sq_covBySMul
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (hypothesis)
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
⊢ CovBySMul G (K ^ (m - 1) * L ^ (n - 1)) (A ^ m ∩ B ^ n) (HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2)
have this : 1 ≤ K
Tactic: have := hA.one_le
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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
⊢ CovBySMul G (K ^ (m - 1) * L ^ (n - 1)) (A ^ m ∩ B ^ n) (HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2)
have 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)
Tactic: choose f hf using exists_smul_inter_smul_subset_smul_inv_mul_inter_inv_mul A B
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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)
have refine_1 : (↑(#(Finset.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1)))) : ℝ) ≤ K ^ (m - 1) * L ^ (n - 1)
Tactic: refine ⟨.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1)), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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)
⊢ CovBySMul G (K ^ (m - 1) * L ^ (n - 1)) (A ^ m ∩ B ^ n) (HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2)
have 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)
Tactic: refine ⟨.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1)), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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))
⊢ HMul.hMul (α := ℝ) (↑(#(F₁ ^ (m - 1))) : ℝ) (↑(#(F₂ ^ (n - 1))) : ℝ) ≤
    HPow.hPow (α := ℝ) (↑(#F₁) : ℝ) (m - 1) * HPow.hPow (α := ℝ) (↑(#F₂) : ℝ) (n - 1)
have h₁ : (↑(#(F₁ ^ (m - 1))) : ℝ) ≤ HPow.hPow (α := ℝ) (↑(#F₁) : ℝ) (m - 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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)
⊢ HMul.hMul (α := ℝ) (↑(#(F₁ ^ (m - 1))) : ℝ) (↑(#(F₂ ^ (n - 1))) : ℝ) ≤
    HPow.hPow (α := ℝ) (↑(#F₁) : ℝ) (m - 1) * HPow.hPow (α := ℝ) (↑(#F₂) : ℝ) (n - 1)
have h₂ : (↑(#(F₂ ^ (n - 1))) : ℝ) ≤ HPow.hPow (α := ℝ) (↑(#F₂) : ℝ) (n - 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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 (α := ℝ) (↑(#F₁) : ℝ) (m - 1) * HPow.hPow (α := ℝ) (↑(#F₂) : ℝ) (n - 1) ≤ K ^ (m - 1) * L ^ (n - 1)
have c0 : 0 ≤ HPow.hPow (α := ℝ) (↑(#F₂) : ℝ) (n - 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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)
⊢ HPow.hPow (α := ℝ) (↑(#F₁) : ℝ) (m - 1) * HPow.hPow (α := ℝ) (↑(#F₂) : ℝ) (n - 1) ≤ K ^ (m - 1) * L ^ (n - 1)
have b0 : 0 ≤ K ^ (m - 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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)
⊢ HPow.hPow (α := ℝ) (↑(#F₁) : ℝ) (m - 1) * HPow.hPow (α := ℝ) (↑(#F₂) : ℝ) (n - 1) ≤ K ^ (m - 1) * L ^ (n - 1)
have h₁ : LE.le (α := ℝ) 0 (↑(#F₁) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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₁) : ℝ)
⊢ HPow.hPow (α := ℝ) (↑(#F₁) : ℝ) (m - 1) * HPow.hPow (α := ℝ) (↑(#F₂) : ℝ) (n - 1) ≤ K ^ (m - 1) * L ^ (n - 1)
have h₂ : LE.le (α := ℝ) 0 (↑(#F₂) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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)))) : ℝ) ≤ K ^ (m - 1) * L ^ (n - 1)
have f₁ : HMul.hMul (α := ℝ) (↑(#(F₁ ^ (m - 1))) : ℝ) (↑(#(F₂ ^ (n - 1))) : ℝ) ≤
  HPow.hPow (α := ℝ) (↑(#F₁) : ℝ) (m - 1) * HPow.hPow (α := ℝ) (↑(#F₂) : ℝ) (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
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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)
⊢ (↑(#(Finset.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1)))) : ℝ) ≤ K ^ (m - 1) * L ^ (n - 1)
have f₂ : HPow.hPow (α := ℝ) (↑(#F₁) : ℝ) (m - 1) * HPow.hPow (α := ℝ) (↑(#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
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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 ^ m ∩ B ^ n ⊆ (↑F₁ : Set G) ^ (m - 1) * A ∩ ((↑F₂ : Set G) ^ (n - 1) * B)
have h₁ : A ^ m ⊆ (↑F₁ : Set G) ^ (m - 1) * A
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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
⊢ A ^ m ∩ B ^ n ⊆ (↑F₁ : Set G) ^ (m - 1) * A ∩ ((↑F₂ : Set G) ^ (n - 1) * B)
have h₂ : B ^ n ⊆ (↑F₂ : Set G) ^ (n - 1) * B
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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 ^ m ⊆ (↑F₁ : Set G) ^ (m - 1) * A
have h₁ : HPow.hPow (β := ℕ) A 2 ⊆ (↑F₁ : Set G) * A
Tactic: apply pow_subset_pow_mul_of_sq_subset_mul
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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
⊢ A ^ m ⊆ (↑F₁ : Set G) ^ (m - 1) * A
have h₂ : m ≠ 0
Tactic: apply pow_subset_pow_mul_of_sq_subset_mul
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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))
⊢ B ^ n ⊆ (↑F₂ : Set G) ^ (n - 1) * B
have h₂ : HPow.hPow (β := ℕ) B 2 ⊆ (↑F₂ : Set G) * B
Tactic: apply pow_subset_pow_mul_of_sq_subset_mul
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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
⊢ B ^ n ⊆ (↑F₂ : Set G) ^ (n - 1) * B
have h₃ : n ≠ 0
Tactic: apply pow_subset_pow_mul_of_sq_subset_mul
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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₁ : Set G) ^ (m - 1) * A ∩ ((↑F₂ : Set G) ^ (n - 1) * B) = ⋃ a ∈ F₁ ^ (m - 1), ⋃ b ∈ F₂ ^ (n - 1), a • A ∩ b • B
have 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)
Tactic: simp_rw [← smul_eq_mul, ← iUnion_smul_set, iUnion₂_inter_iUnion₂]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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) (⋃ 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)
have 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)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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))
⊢ 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)))
have h : ∀ i ∈ F₁ ^ (m - 1), ∀ i_2 ∈ F₂ ^ (n - 1), i • A ∩ i_2 • B ⊆ f i i_2 • (A⁻¹ * A ∩ (B⁻¹ * B))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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 ∈ 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)
have 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)
Tactic: simp_rw [hA.inv_eq_self, hB.inv_eq_self, ← sq]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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 ∈ 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)
have 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))
Tactic: rw [Finset.coe_image₂, ← smul_eq_mul, ← iUnion_smul_set, biUnion_image2]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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 ^ m ∩ B ^ n ⊆
    (↑(Finset.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1))) : Set G) • (HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2)
have A₁ : A ^ m ∩ B ^ n ⊆ (↑F₁ : Set G) ^ (m - 1) * A ∩ ((↑F₂ : Set G) ^ (n - 1) * B)
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]