-- 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:
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
H : ∀ b ∈ F, Disjoint (a • B) (b • B)
⊢ (a ∈ A ∧ F ⊆ A) ∧ (insert a ↑F).PairwiseDisjoint fun x => x • B

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

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
⊢ a ∈ F * (B / B)

Tactic:
by_cases H : ∀ b ∈ F, Disjoint (a • B) (b • B)

Result:
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
H : ∀ b ∈ F, Disjoint (a • B) (b • B)
⊢ a ∈ F * (B / B)

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:
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)

Tactic:
obtain ⟨b, hb, c, hc₁, hc₂⟩ := H

Result:
case neg.intro.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
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)

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

Tactic:
by_cases hau : a ∈ F

Result:
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)

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
⊢ 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 ⊆ A, ↑(#F) ≤ K ∧ A ⊆ F * (B / B)

Tactic:
obtain ⟨F, hF, hFmax⟩ := C.exists_maximal <| filter_nonempty_iff.2
  ⟨∅, empty_mem_powerset _, by rw [coe_empty]; exact Set.pairwiseDisjoint_empty⟩

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 ∈ C
hFmax : ∀ x ∈ C, ¬F < x
⊢ ∃ F ⊆ A, ↑(#F) ≤ K ∧ A ⊆ F * (B / B)

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

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

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
⊢ ∅.PairwiseDisjoint fun x => x • B

Tactic:
exact Set.pairwiseDisjoint_empty

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
H : ∀ b ∈ F, Disjoint (a • B) (b • B)
⊢ a ∈ F * (B / B)

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

Result:
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
H : ∀ b ∈ F, Disjoint (a • B) (b • B)
⊢ insert a F ∈ C

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 * (b⁻¹ * a) = a

Tactic:
simp

Result:
no goals