-- Mathlib/Combinatorics/Additive/RuzsaCovering.lean
theorem ruzsa_covering_mul (hB : B.Nonempty) (hK : #(A * B) ≤ K * #B) :
    ∃ F ⊆ A, #F ≤ K ∧ A ⊆ F * (B / B)

Proof state:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x => x • B)
C : Finset (Finset G) := filter (fun F => (↑F).PairwiseDisjoint fun x => x • B) A.powerset
F : Finset G
hFmax : ∀ x ∈ C, ¬F < x
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x => x • B
⊢ ↑(#F) * ↑(#B) = ↑(#(F * B))

Tactic:
rw [card_mul_iff.2 <| pairwiseDisjoint_smul_iff.1 hF, Nat.cast_mul]

Result:
no goals

Proof state:
case pos
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x => x • B)
C : Finset (Finset G) := filter (fun F => (↑F).PairwiseDisjoint fun x => x • B) A.powerset
F : Finset G
hFmax : ∀ x ∈ C, ¬F < x
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x => x • B
a : G
ha : a ∈ A
hau : a ∈ F
⊢ a ∈ F * (B / B)

Tactic:
exact subset_mul_left _ hB.one_mem_div hau

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x => x • B)
C : Finset (Finset G) := filter (fun F => (↑F).PairwiseDisjoint fun x => x • B) A.powerset
F : Finset G
hFmax : ∀ x ∈ C, ¬F < x
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x => 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

Result:
no goals

Proof state:
case neg
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x => x • B)
C : Finset (Finset G) := filter (fun F => (↑F).PairwiseDisjoint fun x => x • B) A.powerset
F : Finset G
hFmax : ∀ x ∈ C, ¬F < x
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x => x • B
a : G
ha : a ∈ A
hau : a ∉ F
H : ∃ b ∈ F, ¬Disjoint (a • B) (b • B)
⊢ a ∈ F * (B / B)

Tactic:
simp_rw [not_disjoint_iff, ← inv_smul_mem_iff] at H

Result:
case neg
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x => x • B)
C : Finset (Finset G) := filter (fun F => (↑F).PairwiseDisjoint fun x => x • B) A.powerset
F : Finset G
hFmax : ∀ x ∈ C, ¬F < x
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x => x • B
a : G
ha : a ∈ A
hau : a ∉ F
H : ∃ b ∈ F, ∃ a_1, a⁻¹ • a_1 ∈ B ∧ b⁻¹ • a_1 ∈ B
⊢ a ∈ F * (B / B)

Proof state:
case intro.intro
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x => x • B)
C : Finset (Finset G) := filter (fun F => (↑F).PairwiseDisjoint fun x => x • B) A.powerset
F : Finset G
hF : F ∈ C
hFmax : ∀ x ∈ C, ¬F < x
⊢ ∃ F ⊆ A, ↑(#F) ≤ K ∧ A ⊆ F * (B / B)

Tactic:
rw [mem_filter, mem_powerset] at hF

Result:
case intro.intro
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x => x • B)
C : Finset (Finset G) := filter (fun F => (↑F).PairwiseDisjoint fun x => x • B) A.powerset
F : Finset G
hF : F ⊆ A ∧ (↑F).PairwiseDisjoint fun x => x • B
hFmax : ∀ x ∈ C, ¬F < x
⊢ ∃ F ⊆ A, ↑(#F) ≤ K ∧ A ⊆ F * (B / B)

Proof state:
case intro.intro.intro
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x => x • B)
C : Finset (Finset G) := filter (fun F => (↑F).PairwiseDisjoint fun x => x • B) A.powerset
F : Finset G
hFmax : ∀ x ∈ C, ¬F < x
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x => x • B
⊢ ∃ F ⊆ A, ↑(#F) ≤ K ∧ A ⊆ F * (B / B)

Tactic:
refine ⟨F, hFA, le_of_mul_le_mul_right ?_ (by positivity : (0 : ℝ) < #B), fun a ha ↦ ?_⟩

Result:
case intro.intro.intro.refine_1
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x => x • B)
C : Finset (Finset G) := filter (fun F => (↑F).PairwiseDisjoint fun x => x • B) A.powerset
F : Finset G
hFmax : ∀ x ∈ C, ¬F < x
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x => x • B
⊢ ↑(#F) * ↑(#B) ≤ K * ↑(#B)

case intro.intro.intro.refine_2
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x => x • B)
C : Finset (Finset G) := filter (fun F => (↑F).PairwiseDisjoint fun x => x • B) A.powerset
F : Finset G
hFmax : ∀ x ∈ C, ¬F < x
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x => x • B
a : G
ha : a ∈ A
⊢ a ∈ F * (B / B)

Proof state:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x => x • B)
C : Finset (Finset G) := filter (fun F => (↑F).PairwiseDisjoint fun x => x • B) A.powerset
⊢ (↑∅).PairwiseDisjoint fun x => x • B

Tactic:
rw [coe_empty]

Result:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x => x • B)
C : Finset (Finset G) := filter (fun F => (↑F).PairwiseDisjoint fun x => x • B) A.powerset
⊢ ∅.PairwiseDisjoint fun x => x • B

Proof state:
case neg
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x => x • B)
C : Finset (Finset G) := filter (fun F => (↑F).PairwiseDisjoint fun x => x • B) A.powerset
F : Finset G
hFmax : ∀ x ∈ C, ¬F < x
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x => x • B
a : G
ha : a ∈ A
hau : a ∉ F
H : ¬∀ b ∈ F, Disjoint (a • B) (b • B)
⊢ a ∈ F * (B / B)

Tactic:
push_neg at H

Result:
case neg
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x => x • B)
C : Finset (Finset G) := filter (fun F => (↑F).PairwiseDisjoint fun x => x • B) A.powerset
F : Finset G
hFmax : ∀ x ∈ C, ¬F < x
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x => x • B
a : G
ha : a ∈ A
hau : a ∉ F
H : ∃ b ∈ F, ¬Disjoint (a • B) (b • B)
⊢ a ∈ F * (B / B)

Proof state:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x => x • B)
C : Finset (Finset G) := filter (fun F => (↑F).PairwiseDisjoint fun x => x • B) A.powerset
F : Finset G
hFmax : ∀ x ∈ C, ¬F < x
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x => x • B
⊢ ↑(#(F * B)) ≤ ↑(#(A * B))

Tactic:
gcongr

Result:
no goals

Proof state:
case intro.intro
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x => x • B)
C : Finset (Finset G) := filter (fun F => (↑F).PairwiseDisjoint fun x => x • B) A.powerset
F : Finset G
hF : F ⊆ A ∧ (↑F).PairwiseDisjoint fun x => x • B
hFmax : ∀ x ∈ C, ¬F < x
⊢ ∃ F ⊆ A, ↑(#F) ≤ K ∧ A ⊆ F * (B / B)

Tactic:
obtain ⟨hFA, hF⟩ := hF

Result:
case intro.intro.intro
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x => x • B)
C : Finset (Finset G) := filter (fun F => (↑F).PairwiseDisjoint fun x => x • B) A.powerset
F : Finset G
hFmax : ∀ x ∈ C, ¬F < x
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x => x • B
⊢ ∃ F ⊆ A, ↑(#F) ≤ K ∧ A ⊆ F * (B / B)