awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
rw : HMul.hMul (α := ℝ) (↑(#F) : ℝ) (↑(#B) : ℝ) = (↑(#(F * B)) : ℝ)
rw₁ : LE.le (α := ℝ) (↑(#(F * B)) : ℝ) (↑(#(A * B)) : ℝ)
⊢ HMul.hMul (α := ℝ) (↑(#F) : ℝ) (↑(#B) : ℝ) ≤ K * (↑(#B) : ℝ)

Tactic:
calc
      (#F * #B : ℝ) = #(F * B) := by
        rw [card_mul_iff.2 <| pairwiseDisjoint_smul_iff.1 hF, Nat.cast_mul]
      _ ≤ #(A * B) := by gcongr
      _ ≤ K * #B := hK

Premises used: HMul.hMul, Nat.cast, Finset.card
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
a : G
ha : a ∈ A
pos : ∀ (hau : a ∈ F), a ∈ F * (B / B)
neg : ∀ (hau : a ∉ F), a ∈ F * (B / B)
⊢ a ∈ F * (B / B)

Tactic:
by_cases hau : a ∈ F
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
a : G
ha : a ∈ A
hau : a ∈ F
⊢ a ∈ F * (B / B)

Tactic:
subset_mul_left _ hB.one_mem_div hau

Premises used: Finset.Nonempty.one_mem_div, Finset.subset_mul_left
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
a : G
ha : a ∈ A
hau : a ∈ F
⊢ a ∈ F * (B / B)

Tactic:
exact subset_mul_left _ hB.one_mem_div hau

Premises used: Finset.Nonempty.one_mem_div, Finset.subset_mul_left
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
a : G
ha : a ∈ A
hau : a ∉ F
pos : ∀ (H : ∀ b ∈ F, Disjoint (a • B) (b • B)), a ∈ F * (B / B)
neg : ∀ (H : ∃ b ∈ F, ¬Disjoint (a • B) (b • B)), a ∈ F * (B / B)
⊢ a ∈ F * (B / B)

Tactic:
by_cases! H : ∀ b ∈ F, Disjoint (a • B) (b • B)
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
a : G
ha : a ∈ A
hau : a ∉ F
H : ∀ b ∈ F, Disjoint (a • B) (b • B)
⊢ a ∈ F * (B / B)

Tactic:
(hFmax.not_gt ?_ <| ssubset_insert hau).elim

Premises used: False.elim, Finset.ssubset_insert, Maximal.not_gt
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
a : G
ha : a ∈ A
hau : a ∉ F
H : ∀ b ∈ F, Disjoint (a • B) (b • B)
pos : insert a F ⊆ A ∧ (↑(insert a F) : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
⊢ a ∈ F * (B / B)

Tactic:
refine (hFmax.not_gt ?_ <| ssubset_insert hau).elim

Premises used: False.elim, Finset.ssubset_insert, Maximal.not_gt
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
a : G
ha : a ∈ A
hau : a ∉ F
H : ∀ b ∈ F, Disjoint (a • B) (b • B)
pos : (a ∈ A ∧ F ⊆ A) ∧ (insert a (↑F : Set G)).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
⊢ insert a F ⊆ A ∧ (↑(insert a F) : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B

Tactic:
rw [insert_subset_iff, coe_insert]

Premises used: Finset.insert_subset_iff, Finset.coe_insert
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
a : G
ha : a ∈ A
hau : a ∉ F
H : ∀ b ∈ F, Disjoint (a • B) (b • B)
⊢ (a ∈ A ∧ F ⊆ A) ∧ (insert a (↑F : Set G)).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B

Tactic:
⟨⟨ha, hFA⟩, hF.insert fun _ hb _ ↦ H _ hb⟩

Premises used: Set.PairwiseDisjoint.insert, And.intro
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
a : G
ha : a ∈ A
hau : a ∉ F
H : ∀ b ∈ F, Disjoint (a • B) (b • B)
⊢ (a ∈ A ∧ F ⊆ A) ∧ (insert a (↑F : Set G)).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B

Tactic:
exact ⟨⟨ha, hFA⟩, hF.insert fun _ hb _ ↦ H _ hb⟩
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
a : G
ha : a ∈ A
hau : a ∉ F
H : ∃ b ∈ F, ¬Disjoint (a • B) (b • B)
⊢ ∃ b ∈ F, ∃ (a_1 : G), a⁻¹ • a_1 ∈ B ∧ b⁻¹ • a_1 ∈ B

Tactic:
simp_rw [not_disjoint_iff, ← inv_smul_mem_iff] at H

Premises used: Finset.inv_smul_mem_iff, Finset.not_disjoint_iff
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
a : G
ha : a ∈ A
hau : a ∉ F
H : ∃ b ∈ F, ∃ (a_1 : G), a⁻¹ • a_1 ∈ B ∧ b⁻¹ • a_1 ∈ B
neg : ∀ (b : G) (hb : b ∈ F) (c : G) (hc₁ : a⁻¹ • c ∈ B) (hc₂ : b⁻¹ • c ∈ B), a ∈ F * (B / B)
⊢ a ∈ F * (B / B)

Tactic:
obtain ⟨b, hb, c, hc₁, hc₂⟩ := H
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
a : G
ha : a ∈ A
hau : a ∉ F
b : G
hb : b ∈ F
c : G
hc₁ : a⁻¹ • c ∈ B
hc₂ : b⁻¹ • c ∈ B
⊢ b⁻¹ • c / a⁻¹ • c = b⁻¹ * a

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
a : G
ha : a ∈ A
hau : a ∉ F
b : G
hb : b ∈ F
c : G
hc₁ : a⁻¹ • c ∈ B
hc₂ : b⁻¹ • c ∈ B
⊢ b * (b⁻¹ * a) = a

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
a : G
ha : a ∈ A
hau : a ∉ F
b : G
hb : b ∈ F
c : G
hc₁ : a⁻¹ • c ∈ B
hc₂ : b⁻¹ • c ∈ B
⊢ a ∈ F * (B / B)

Tactic:
exact mem_mul.2 ⟨b, hb, b⁻¹ * a, mem_div.2 ⟨_, hc₂, _, hc₁, by simp⟩, by simp⟩

Premises used: Iff.mpr, HMul.hMul, Finset.mem_div, Inv.inv, And.intro, Exists.intro, Finset.mem_mul
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
A B : Set G
hA : A.Finite
hB : B.Finite
hB₀ : B.Nonempty
hK : (↑(Nat.card.{u_1} (↑(A * B) : Type u_1)) : ℝ) ≤ K * (↑(Nat.card.{u_1} (↑B : Type u_1)) : ℝ)
⊢ A.Finite

Tactic:
hA
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
A B : Set G
hA : A.Finite
hB : B.Finite
hB₀ : B.Nonempty
hK : (↑(Nat.card.{u_1} (↑(A * B) : Type u_1)) : ℝ) ≤ K * (↑(Nat.card.{u_1} (↑B : Type u_1)) : ℝ)
lift :
  ∀ (A : Finset G)
    (hK : (↑(Nat.card.{u_1} (↑((↑A : Set G) * B) : Type u_1)) : ℝ) ≤ K * (↑(Nat.card.{u_1} (↑B : Type u_1)) : ℝ)),
    ∃ F ⊆ (↑A : Set G), (↑(Nat.card.{u_1} (↑F : Type u_1)) : ℝ) ≤ K ∧ (↑A : Set G) ⊆ F * (B / B) ∧ F.Finite
⊢ ∃ F ⊆ A, (↑(Nat.card.{u_1} (↑F : Type u_1)) : ℝ) ≤ K ∧ A ⊆ F * (B / B) ∧ F.Finite

Tactic:
lift A to Finset G using hA

Premises used: Finset
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
B : Set G
hB : B.Finite
hB₀ : B.Nonempty
A : Finset G
hK : (↑(Nat.card.{u_1} (↑((↑A : Set G) * B) : Type u_1)) : ℝ) ≤ K * (↑(Nat.card.{u_1} (↑B : Type u_1)) : ℝ)
⊢ B.Finite

Tactic:
hB
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
B : Set G
hB : B.Finite
hB₀ : B.Nonempty
A : Finset G
hK : (↑(Nat.card.{u_1} (↑((↑A : Set G) * B) : Type u_1)) : ℝ) ≤ K * (↑(Nat.card.{u_1} (↑B : Type u_1)) : ℝ)
lift :
  ∀ (B : Finset G) (hB₀ : (↑B : Set G).Nonempty)
    (hK :
      (↑(Nat.card.{u_1} (↑((↑A : Set G) * (↑B : Set G)) : Type u_1)) : ℝ) ≤
        K * (↑(Nat.card.{u_1} (↑(↑B : Set G) : Type u_1)) : ℝ)),
    ∃ F ⊆ (↑A : Set G),
      (↑(Nat.card.{u_1} (↑F : Type u_1)) : ℝ) ≤ K ∧ (↑A : Set G) ⊆ F * ((↑B : Set G) / (↑B : Set G)) ∧ F.Finite
⊢ ∃ F ⊆ (↑A : Set G), (↑(Nat.card.{u_1} (↑F : Type u_1)) : ℝ) ≤ K ∧ (↑A : Set G) ⊆ F * (B / B) ∧ F.Finite

Tactic:
lift B to Finset G using hB

Premises used: Finset
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
A B : Finset G
hB₀ : (↑B : Set G).Nonempty
hK :
  (↑(Nat.card.{u_1} (↑((↑A : Set G) * (↑B : Set G)) : Type u_1)) : ℝ) ≤
    K * (↑(Nat.card.{u_1} (↑(↑B : Set G) : Type u_1)) : ℝ)
⊢ (↑(A * B).card : ℝ) ≤ K * (↑B.card : ℝ)

Tactic:
simpa [← Finset.coe_mul] using hK

Premises used: Finset.coe_mul
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
A B : Finset G
hB₀ : (↑B : Set G).Nonempty
hK :
  (↑(Nat.card.{u_1} (↑((↑A : Set G) * (↑B : Set G)) : Type u_1)) : ℝ) ≤
    K * (↑(Nat.card.{u_1} (↑(↑B : Set G) : Type u_1)) : ℝ)
obtain :
  ∀ (F : Finset G) (hFA : F ⊆ A) (hF : (↑F.card : ℝ) ≤ K) (hAF : A ⊆ F * (B / B)),
    ∃ F ⊆ (↑A : Set G),
      (↑(Nat.card.{u_1} (↑F : Type u_1)) : ℝ) ≤ K ∧ (↑A : Set G) ⊆ F * ((↑B : Set G) / (↑B : Set G)) ∧ F.Finite
⊢ ∃ F ⊆ (↑A : Set G),
    (↑(Nat.card.{u_1} (↑F : Type u_1)) : ℝ) ≤ K ∧ (↑A : Set G) ⊆ F * ((↑B : Set G) / (↑B : Set G)) ∧ F.Finite

Tactic:
obtain ⟨F, hFA, hF, hAF⟩ := Finset.ruzsa_covering_mul hB₀ (by simpa [← Finset.coe_mul] using hK)

Premises used: Finset.ruzsa_covering_mul
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
A B : Finset G
hB₀ : (↑B : Set G).Nonempty
hK :
  (↑(Nat.card.{u_1} (↑((↑A : Set G) * (↑B : Set G)) : Type u_1)) : ℝ) ≤
    K * (↑(Nat.card.{u_1} (↑(↑B : Set G) : Type u_1)) : ℝ)
F : Finset G
hFA : F ⊆ A
hF : (↑F.card : ℝ) ≤ K
hAF : A ⊆ F * (B / B)
norm_cast : F ≤ A ∧ (↑(Nat.card.{u_1} ↥F) : ℝ) ≤ K ∧ A ≤ F * (B / B) ∧ (↑F : Set G).Finite
⊢ (↑F : Set G) ⊆ (↑A : Set G) ∧
    (↑(Nat.card.{u_1} (↑(↑F : Set G) : Type u_1)) : ℝ) ≤ K ∧
      (↑A : Set G) ⊆ (↑F : Set G) * ((↑B : Set G) / (↑B : Set G)) ∧ (↑F : Set G).Finite

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
A B : Finset G
hB₀ : (↑B : Set G).Nonempty
hK :
  (↑(Nat.card.{u_1} (↑((↑A : Set G) * (↑B : Set G)) : Type u_1)) : ℝ) ≤
    K * (↑(Nat.card.{u_1} (↑(↑B : Set G) : Type u_1)) : ℝ)
F : Finset G
hFA : F ⊆ A
hF : (↑F.card : ℝ) ≤ K
hAF : A ⊆ F * (B / B)
⊢ F ≤ A ∧ (↑(Nat.card.{u_1} ↥F) : ℝ) ≤ K ∧ A ≤ F * (B / B) ∧ (↑F : Set G).Finite

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
A B : Finset G
hB₀ : (↑B : Set G).Nonempty
hK :
  (↑(Nat.card.{u_1} (↑((↑A : Set G) * (↑B : Set G)) : Type u_1)) : ℝ) ≤
    K * (↑(Nat.card.{u_1} (↑(↑B : Set G) : Type u_1)) : ℝ)
F : Finset G
hFA : F ⊆ A
hF : (↑F.card : ℝ) ≤ K
hAF : A ⊆ F * (B / B)
⊢ ∃ F ⊆ (↑A : Set G),
    (↑(Nat.card.{u_1} (↑F : Type u_1)) : ℝ) ≤ K ∧ (↑A : Set G) ⊆ F * ((↑B : Set G) / (↑B : Set G)) ∧ F.Finite

Tactic:
exact ⟨F, by norm_cast; simp [*]⟩
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
A B : Finset G
hB₀ : (↑B : Set G).Nonempty
hK :
  (↑(Nat.card.{u_1} (↑((↑A : Set G) * (↑B : Set G)) : Type u_1)) : ℝ) ≤
    K * (↑(Nat.card.{u_1} (↑(↑B : Set G) : Type u_1)) : ℝ)
obtain :
  ∀ (F : Finset G) (hFA : F ⊆ A) (hF : (↑F.card : ℝ) ≤ K) (hAF : A ⊆ F * (B / B)),
    ∃ F ⊆ (↑A : Set G),
      (↑(Nat.card.{u_1} (↑F : Type u_1)) : ℝ) ≤ K ∧ (↑A : Set G) ⊆ F * ((↑B : Set G) / (↑B : Set G)) ∧ F.Finite
⊢ ∃ F ⊆ (↑A : Set G),
    (↑(Nat.card.{u_1} (↑F : Type u_1)) : ℝ) ≤ K ∧ (↑A : Set G) ⊆ F * ((↑B : Set G) / (↑B : Set G)) ∧ F.Finite

Tactic:
classical
  obtain ⟨F, hFA, hF, hAF⟩ := Finset.ruzsa_covering_mul hB₀ (by simpa [← Finset.coe_mul] using hK)
  exact ⟨F, by norm_cast; simp [*]⟩
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
k : ℝ
m : ℕ
h :
  ∀ (ε : Fin 3 → ℤ),
    (∀ (i : Fin 3), |ε i| = 1) →
      (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ ε i) (finRange 3)))) : ℝ) ≤ k * (↑(#A) : ℝ)
ε : Fin 3 → ℤ
hε : ∀ (i : Fin 3), |ε i| = 1
⊢ (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ ε i) (finRange 3)))) : ℝ) ≤
    k ^ HSub.hSub (α := ℕ) 3 2 * (↑(#A) : ℝ)

Tactic:
simpa using h ε hε
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
k : ℝ
m_1 : ℕ
h :
  ∀ (ε : Fin 3 → ℤ),
    (∀ (i : Fin 3), |ε i| = 1) →
      (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ ε i) (finRange 3)))) : ℝ) ≤ k * (↑(#A) : ℝ)
m : ℕ
hm : 3 ≤ m
ih :
  ∀ (ε : Fin m → ℤ) (hε : ∀ (i : Fin m), |ε i| = 1),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin m) ↦ A ^ ε i) (finRange m)))) : ℝ) ≤ k ^ (m - 2) * (↑(#A) : ℝ)
ε : Fin (m + 1) → ℤ
hε : ∀ (i : Fin (m + 1)), |ε i| = 1
succ :
  ∀ (hm : LE.le (α := ℕ) 3 0)
    (ih :
      ∀ (ε : Fin 0 → ℤ) (hε : ∀ (i : Fin 0), |ε i| = 1),
        (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 0) ↦ A ^ ε i) (finRange 0)))) : ℝ) ≤
          k ^ HSub.hSub (α := ℕ) 0 2 * (↑(#A) : ℝ))
    (ε : Fin (HAdd.hAdd (α := ℕ) 0 1) → ℤ) (hε : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)), |ε i| = 1),
    (↑(card.{u_1} (α := G)
            (prod (List.map (fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ A ^ ε i) (finRange (HAdd.hAdd (α := ℕ) 0 1))))) :
        ℝ) ≤
      k ^ (HAdd.hAdd (α := ℕ) 0 1 - 2) * (↑(#A) : ℝ)
succ₁ :
  ∀ (m : ℕ) (hm : 3 ≤ m + 1)
    (ih :
      ∀ (ε : Fin (m + 1) → ℤ) (hε : ∀ (i : Fin (m + 1)), |ε i| = 1),
        (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1)) ↦ A ^ ε i) (finRange (m + 1))))) : ℝ) ≤
          k ^ (m + 1 - 2) * (↑(#A) : ℝ))
    (ε : Fin (m + 1 + 1) → ℤ) (hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1 + 1)) ↦ A ^ ε i) (finRange (m + 1 + 1))))) : ℝ) ≤
      k ^ (m + 1 + 1 - 2) * (↑(#A) : ℝ)
⊢ (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1)) ↦ A ^ ε i) (finRange (m + 1))))) : ℝ) ≤
    k ^ (m + 1 - 2) * (↑(#A) : ℝ)

Tactic:
obtain _ | m := m
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
k : ℝ
m : ℕ
h :
  ∀ (ε : Fin 3 → ℤ),
    (∀ (i : Fin 3), |ε i| = 1) →
      (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ ε i) (finRange 3)))) : ℝ) ≤ k * (↑(#A) : ℝ)
hm : LE.le (α := ℕ) 3 0
ih :
  ∀ (ε : Fin 0 → ℤ) (hε : ∀ (i : Fin 0), |ε i| = 1),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 0) ↦ A ^ ε i) (finRange 0)))) : ℝ) ≤
      k ^ HSub.hSub (α := ℕ) 0 2 * (↑(#A) : ℝ)
ε : Fin (HAdd.hAdd (α := ℕ) 0 1) → ℤ
hε : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)), |ε i| = 1
⊢ (↑(card.{u_1} (α := G)
          (prod (List.map (fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ A ^ ε i) (finRange (HAdd.hAdd (α := ℕ) 0 1))))) :
      ℝ) ≤
    k ^ (HAdd.hAdd (α := ℕ) 0 1 - 2) * (↑(#A) : ℝ)

Tactic:
simp at hm
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
k : ℝ
m_1 : ℕ
h :
  ∀ (ε : Fin 3 → ℤ),
    (∀ (i : Fin 3), |ε i| = 1) →
      (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ ε i) (finRange 3)))) : ℝ) ≤ k * (↑(#A) : ℝ)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ) (hε : ∀ (i : Fin (m + 1)), |ε i| = 1),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1)) ↦ A ^ ε i) (finRange (m + 1))))) : ℝ) ≤
      k ^ (m + 1 - 2) * (↑(#A) : ℝ)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
⊢ 2 ≤ m

Tactic:
simp at hm
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
k : ℝ
m_1 : ℕ
h :
  ∀ (ε : Fin 3 → ℤ),
    (∀ (i : Fin 3), |ε i| = 1) →
      (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ ε i) (finRange 3)))) : ℝ) ≤ k * (↑(#A) : ℝ)
m : ℕ
ih :
  ∀ (ε : Fin (m + 1) → ℤ) (hε : ∀ (i : Fin (m + 1)), |ε i| = 1),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1)) ↦ A ^ ε i) (finRange (m + 1))))) : ℝ) ≤
      k ^ (m + 1 - 2) * (↑(#A) : ℝ)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm : 2 ≤ m
⊢ m ≠ 0

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
k : ℝ
m_1 : ℕ
h :
  ∀ (ε : Fin 3 → ℤ),
    (∀ (i : Fin 3), |ε i| = 1) →
      (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ ε i) (finRange 3)))) : ℝ) ≤ k * (↑(#A) : ℝ)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ) (hε : ∀ (i : Fin (m + 1)), |ε i| = 1),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1)) ↦ A ^ ε i) (finRange (m + 1))))) : ℝ) ≤
      k ^ (m + 1 - 2) * (↑(#A) : ℝ)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
⊢ m ≠ 0

Tactic:
have hm₀ : m ≠ 0 := by simp at hm; positivity
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
k : ℝ
m_1 : ℕ
h_1 :
  ∀ (ε : Fin 3 → ℤ),
    (∀ (i : Fin 3), |ε i| = 1) →
      (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ ε i) (finRange 3)))) : ℝ) ≤ k * (↑(#A) : ℝ)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ) (hε : ∀ (i : Fin (m + 1)), |ε i| = 1),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1)) ↦ A ^ ε i) (finRange (m + 1))))) : ℝ) ≤
      k ^ (m + 1 - 2) * (↑(#A) : ℝ)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
i : Fin (m + 1 + 1)
h : ε i = 0
⊢ False

Tactic:
simpa [h] using hε i