-- Mathlib/Combinatorics/Additive/RuzsaCovering.lean
/-- **Ruzsa's covering lemma** for sets. See also `Finset.ruzsa_covering_mul`. -/
@[to_additive "**Ruzsa's covering lemma** for sets. See also `Finset.ruzsa_covering_add`."]
lemma ruzsa_covering_mul (hA : A.Finite) (hB : B.Finite) (hB₀ : B.Nonempty)
    (hK : Nat.card (A * B) ≤ K * Nat.card B) :
    ∃ F ⊆ A, Nat.card F ≤ K ∧ A ⊆ F * (B / B) ∧ F.Finite

Proof state:
case intro.intro
G : Type u_1
inst✝ : Group G
K : ℝ
A B : Finset G
hB₀ : (↑B).Nonempty
hK : ↑(Nat.card ↑(↑A * ↑B)) ≤ K * ↑(Nat.card ↑↑B)
⊢ ∃ F ⊆ ↑A, ↑(Nat.card ↑F) ≤ K ∧ ↑A ⊆ F * (↑B / ↑B) ∧ F.Finite

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

Result:
case intro.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
K : ℝ
A B : Finset G
hB₀ : (↑B).Nonempty
hK : ↑(Nat.card ↑(↑A * ↑B)) ≤ K * ↑(Nat.card ↑↑B)
F : Finset G
hFA : F ⊆ A
hF : ↑F.card ≤ K
hAF : A ⊆ F * (B / B)
⊢ ∃ F ⊆ ↑A, ↑(Nat.card ↑F) ≤ K ∧ ↑A ⊆ F * (↑B / ↑B) ∧ F.Finite

Proof state:
G : Type u_1
inst✝ : Group G
K : ℝ
A B : Finset G
hB₀ : (↑B).Nonempty
hK : ↑(Nat.card ↑(↑A * ↑B)) ≤ K * ↑(Nat.card ↑↑B)
⊢ ↑(?m.28860 * B).card ≤ ?m.28858 * ↑B.card

Tactic:
simpa [← Finset.coe_mul] using hK

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
K : ℝ
A B : Finset G
hB₀ : (↑B).Nonempty
hK : ↑(Nat.card ↑(↑A * ↑B)) ≤ K * ↑(Nat.card ↑↑B)
F : Finset G
hFA : F ⊆ A
hF : ↑F.card ≤ K
hAF : A ⊆ F * (B / B)
⊢ ↑F ⊆ ↑A ∧ ↑(Nat.card ↑↑F) ≤ K ∧ ↑A ⊆ ↑F * (↑B / ↑B) ∧ (↑F).Finite

Tactic:
norm_cast

Result:
G : Type u_1
inst✝ : Group G
K : ℝ
A B : Finset G
hB₀ : (↑B).Nonempty
hK : ↑(Nat.card ↑(↑A * ↑B)) ≤ K * ↑(Nat.card ↑↑B)
F : Finset G
hFA : F ⊆ A
hF : ↑F.card ≤ K
hAF : A ⊆ F * (B / B)
⊢ F ⊆ A ∧ ↑(Nat.card { x // x ∈ F }) ≤ K ∧ A ⊆ F * (B / B) ∧ (↑F).Finite

Proof state:
case intro.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
K : ℝ
A B : Finset G
hB₀ : (↑B).Nonempty
hK : ↑(Nat.card ↑(↑A * ↑B)) ≤ K * ↑(Nat.card ↑↑B)
F : Finset G
hFA : F ⊆ A
hF : ↑F.card ≤ K
hAF : A ⊆ F * (B / B)
⊢ ∃ F ⊆ ↑A, ↑(Nat.card ↑F) ≤ K ∧ ↑A ⊆ F * (↑B / ↑B) ∧ F.Finite

Tactic:
exact ⟨F, by norm_cast; simp [*]⟩

Result:
no goals

Proof state:
case intro
G : Type u_1
inst✝ : Group G
K : ℝ
B : Set G
hB : B.Finite
hB₀ : B.Nonempty
A : Finset G
hK : ↑(Nat.card ↑(↑A * B)) ≤ K * ↑(Nat.card ↑B)
⊢ ∃ F ⊆ ↑A, ↑(Nat.card ↑F) ≤ K ∧ ↑A ⊆ F * (B / B) ∧ F.Finite

Tactic:
lift B to Finset G using hB

Result:
case intro.intro
G : Type u_1
inst✝ : Group G
K : ℝ
A B : Finset G
hB₀ : (↑B).Nonempty
hK : ↑(Nat.card ↑(↑A * ↑B)) ≤ K * ↑(Nat.card ↑↑B)
⊢ ∃ F ⊆ ↑A, ↑(Nat.card ↑F) ≤ K ∧ ↑A ⊆ F * (↑B / ↑B) ∧ F.Finite

Proof state:
G : Type u_1
inst✝ : Group G
K : ℝ
A B : Finset G
hB₀ : (↑B).Nonempty
hK : ↑(Nat.card ↑(↑A * ↑B)) ≤ K * ↑(Nat.card ↑↑B)
F : Finset G
hFA : F ⊆ A
hF : ↑F.card ≤ K
hAF : A ⊆ F * (B / B)
⊢ F ⊆ A ∧ ↑(Nat.card { x // x ∈ F }) ≤ K ∧ A ⊆ F * (B / B) ∧ (↑F).Finite

Tactic:
simp [*]

Result:
no goals

Proof state:
case intro.intro
G : Type u_1
inst✝ : Group G
K : ℝ
A B : Finset G
hB₀ : (↑B).Nonempty
hK : ↑(Nat.card ↑(↑A * ↑B)) ≤ K * ↑(Nat.card ↑↑B)
⊢ ∃ F ⊆ ↑A, ↑(Nat.card ↑F) ≤ K ∧ ↑A ⊆ F * (↑B / ↑B) ∧ 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 [*]⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
K : ℝ
A B : Set G
hA : A.Finite
hB : B.Finite
hB₀ : B.Nonempty
hK : ↑(Nat.card ↑(A * B)) ≤ K * ↑(Nat.card ↑B)
⊢ ∃ F ⊆ A, ↑(Nat.card ↑F) ≤ K ∧ A ⊆ F * (B / B) ∧ F.Finite

Tactic:
lift A to Finset G using hA

Result:
case intro
G : Type u_1
inst✝ : Group G
K : ℝ
B : Set G
hB : B.Finite
hB₀ : B.Nonempty
A : Finset G
hK : ↑(Nat.card ↑(↑A * B)) ≤ K * ↑(Nat.card ↑B)
⊢ ∃ F ⊆ ↑A, ↑(Nat.card ↑F) ≤ K ∧ ↑A ⊆ F * (B / B) ∧ F.Finite