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
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 ^ m ∩ B ^ n ⊆
    (↑(Finset.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1))) : Set G) • (HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2)
have 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
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]
-- 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₁ : 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 ^ m ∩ B ^ n ⊆
    (↑(Finset.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1))) : Set G) • (HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2)
have 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)))
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]
-- 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₁ : 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 ^ 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 ∈ 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: 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]
-- 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: classical
  obtain ⟨F₁, hF₁, hAF₁⟩ := hA.sq_covBySMul
  obtain ⟨F₂, hF₂, hBF₂⟩ := hB.sq_covBySMul
  have := hA.one_le
  choose f hf using exists_smul_inter_smul_subset_smul_inv_mul_inter_inv_mul A B
  refine ⟨.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1)), ?_, ?_⟩
  · 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
  · 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]
-- 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
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)
have obtain₁ : ∀ (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)
Tactic: classical
  obtain ⟨F₁, hF₁, hAF₁⟩ := hA.sq_covBySMul
  obtain ⟨F₂, hF₂, hBF₂⟩ := hB.sq_covBySMul
  have := hA.one_le
  choose f hf using exists_smul_inter_smul_subset_smul_inv_mul_inter_inv_mul A B
  refine ⟨.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1)), ?_, ?_⟩
  · 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
  · 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]
-- 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
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)
obtain₁ :
  ∀ (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)
⊢ 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) (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)
Tactic: classical
  obtain ⟨F₁, hF₁, hAF₁⟩ := hA.sq_covBySMul
  obtain ⟨F₂, hF₂, hBF₂⟩ := hB.sq_covBySMul
  have := hA.one_le
  choose f hf using exists_smul_inter_smul_subset_smul_inv_mul_inter_inv_mul A B
  refine ⟨.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1)), ?_, ?_⟩
  · 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
  · 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]
-- 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
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)
obtain₁ :
  ∀ (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)
obtain₂ :
  ∀ (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)
⊢ 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) (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: classical
  obtain ⟨F₁, hF₁, hAF₁⟩ := hA.sq_covBySMul
  obtain ⟨F₂, hF₂, hBF₂⟩ := hB.sq_covBySMul
  have := hA.one_le
  choose f hf using exists_smul_inter_smul_subset_smul_inv_mul_inter_inv_mul A B
  refine ⟨.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1)), ?_, ?_⟩
  · 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
  · 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]
-- 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
⊢ (A ^ m ∩ B ^ n)⁻¹ = A ^ m ∩ B ^ n
have simp_rw : (A ^ m)⁻¹ ∩ (B ^ n)⁻¹ = A ^ m ∩ B ^ n
Tactic: simp_rw [inter_inv, ← inv_pow, hA.inv_eq_self, hB.inv_eq_self]
-- 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
simp_rw : (A ^ m)⁻¹ ∩ (B ^ n)⁻¹ = A ^ m ∩ B ^ n
⊢ (A ^ m ∩ B ^ n)⁻¹ = A ^ m ∩ B ^ n
have simp_rw₁ : A⁻¹ ^ m ∩ B⁻¹ ^ n = A ^ m ∩ B ^ n
Tactic: simp_rw [inter_inv, ← inv_pow, hA.inv_eq_self, hB.inv_eq_self]
-- 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
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
have simp_rw₂ : A ^ m ∩ B⁻¹ ^ n = A ^ m ∩ B ^ n
Tactic: simp_rw [inter_inv, ← inv_pow, hA.inv_eq_self, hB.inv_eq_self]
-- 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
⊢ HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2 ⊆ A ^ m ∩ B ^ n
have h₁ : 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
h₁ : 1 ∈ A
⊢ HPow.hPow (β := ℕ) A 2 ∩ HPow.hPow (β := ℕ) B 2 ⊆ A ^ m ∩ B ^ n
have h₂ : 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
⊢ CovBySMul G (K ^ (2 * m - 1) * L ^ (2 * n - 1)) (HPow.hPow (β := ℕ) (A ^ m ∩ B ^ n) 2) (A ^ m ∩ B ^ n)
have refine : HPow.hPow (β := ℕ) (A ^ m ∩ B ^ n) 2 ⊆ A ^ (2 * m) ∩ B ^ (2 * 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])
-- 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
⊢ HPow.hPow (β := ℕ) (A ^ m ∩ B ^ n) 2 ⊆ A ^ (2 * m) ∩ B ^ (2 * n)
have m₁ : HPow.hPow (β := ℕ) (A ^ m) 2 ∩ HPow.hPow (β := ℕ) (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']
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
Goal:
G : Type u_1
inst : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
this : A * A ⊆ A
x : G
hx : x ∈ A
⊢ x⁻¹ ∈ A
have rwa : x⁻¹ ∈ A⁻¹
Tactic: rwa [← hA.inv_eq_self, inv_mem_inv]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
Goal:
G : Type u_1
inst : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
⊢ ∃ (H : Subgroup G), (↑H : Set G) = A
have suffices : A * A ⊆ 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⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
Goal:
G : Type u_1
inst : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
⊢ ∃ (x : G), A * A ⊆ x • A
have obtain : ∀ (K : Finset G) (hK : LE.le (α := ℝ) (↑(#K) : ℝ) 1) (hKA : HPow.hPow (β := ℕ) A 2 ⊆ (↑K : Set G) • A),
  ∃ (x : G), A * A ⊆ x • A
Tactic: obtain ⟨K, hK, hKA⟩ := hA.sq_covBySMul
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (hypothesis)
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), A * A ⊆ x • A
have hK₁ : ∃ (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
Cleared hypotheses: hK
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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}
⊢ ∃ (x : G), A * A ⊆ x • A
have inl : ∀ (x : G) (hKA : HPow.hPow (β := ℕ) A 2 ⊆ (↑∅ : Set G) • A), ∃ (x : G), A * A ⊆ x • A
Tactic: obtain ⟨x, rfl | rfl⟩ := hK
Cleared hypotheses: K, hKA, hK
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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
⊢ ∃ (x : G), A * A ⊆ x • A
have inr : ∀ (x : G) (hKA : HPow.hPow (β := ℕ) A 2 ⊆ (↑{x} : Set G) • A), ∃ (x : G), A * A ⊆ x • A
Tactic: obtain ⟨x, rfl | rfl⟩ := hK
Cleared hypotheses: K, hKA, hK
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (hypothesis)
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
⊢ ∃ (x : G), A * A ⊆ x • A
have hKA₁ : A * A ⊆ x • A
Tactic: rw [Finset.coe_singleton, singleton_smul, sq] at hKA
Cleared hypotheses: hKA
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
Goal:
G : Type u_1
inst : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
⊢ A * A ⊆ A
have obtain : ∀ (x : G) (hx : A * A ⊆ x • 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
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (hypothesis)
Goal:
G : Type u_1
inst : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
⊢ A * A ⊆ A
have hx' : x⁻¹ • (A * A) ⊆ A
Tactic: have hx' : x⁻¹ • (A * A) ⊆ A := by rwa [← subset_smul_set_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (hypothesis)
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
⊢ A * A ⊆ A
have hx_inv : 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))
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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
have rw : x * x ∈ A⁻¹
Tactic: rw [← hA.inv_eq_self]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (hypothesis)
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
⊢ A * A ⊆ A
have hx_sq : 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))
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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
⊢ A * A ⊆ A
have calc₁ : x • A = x⁻¹ • (x * x) • 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'
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
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
have refine : ∀ (n : ℕ),
  Set.WellFoundedOn.{u_2} (α := Finset α × Finset α)
    ({x : Finset α × Finset α | x.1.Nonempty ∧ x.2.Nonempty} ∩
      Set.preimage (β := ℕ) (fun (x : Finset α × Finset α) ↦ #(x.1 * x.2)) {n})
    ((fun (x1 x2 : ℕ) ↦ x1 > x2) on fun (x : Finset α × Finset α) ↦ #x.1 + #x.2)
Tactic: refine wellFounded_lt.onFun.wellFoundedOn.prod_lex_of_wellFoundedOn_fiber fun n ↦
    Set.WellFoundedOn.prod_lex_of_wellFoundedOn_fiber ?_ fun n ↦
      wellFounded_lt.onFun.wellFoundedOn
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (hypothesis)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ min (minOrder α) (↑(#s + #t - 1) : ℕ∞) ≤ (↑(#(s * t)) : ℕ∞)
have hx : let x := (s, t);
x = (s, t)
Tactic: set x := (s, t) with hx
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
x : Finset α × Finset α := (s, t)
hx : x = (s, t)
⊢ min (minOrder α) (↑(#s + #t - 1) : ℕ∞) ≤ (↑(#(s * t)) : ℕ∞)
have clear_value : ∀ (x : Finset α × Finset α) (hx : x = (s, t)), min (minOrder α) (↑(#s + #t - 1) : ℕ∞) ≤ (↑(#(s * t)) : ℕ∞)
Tactic: clear_value x
Cleared hypotheses: x, hx