-- Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean
theorem ruzsa_triangle_inequality_div_div_div (A B C : Finset G) :
    #(A / C) * #B ≤ #(A / B) * #(C / B)

Proof state:
case refine_1
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
x : G
hx : x ∈ A / C
⊢ #B ≤
    #(bipartiteAbove
        (fun b x =>
          match x with
          | (a, c) => a / c = b)
        ((A / B) ×ˢ (C / B)) x)

Tactic:
obtain ⟨a, ha, c, hc, rfl⟩ := mem_div.1 hx

Result:
case refine_1.intro.intro.intro.intro
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
a : G
ha : a ∈ A
c : G
hc : c ∈ C
hx : a / c ∈ A / C
⊢ #B ≤
    #(bipartiteAbove
        (fun b x =>
          match x with
          | (a, c) => a / c = b)
        ((A / B) ×ˢ (C / B)) (a / c))

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
⊢ #(A / C) * #B ≤ #(A / B) * #(C / B)

Tactic:
rw [← card_product (A / B), ← mul_one #((A / B) ×ˢ (C / B))]

Result:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
⊢ #(A / C) * #B ≤ #((A / B) ×ˢ (C / B)) * 1

Proof state:
case refine_2
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
x : G × G
x✝ : x ∈ (A / B) ×ˢ (C / B)
a✝ b✝ : G
hu :
  a✝ ∈
    bipartiteBelow
      (fun b x =>
        match x with
        | (a, c) => a / c = b)
      (A / C) x
hv :
  b✝ ∈
    bipartiteBelow
      (fun b x =>
        match x with
        | (a, c) => a / c = b)
      (A / C) x
⊢ x.1 / x.2 = b✝

Tactic:
exact ((mem_bipartiteBelow _).1 hv).2

Result:
no goals

Proof state:
case refine_1.intro.intro.intro.intro.refine_1
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
a : G
ha : a ∈ A
c : G
hc : c ∈ C
hx : a / c ∈ A / C
b : G
hb : b ∈ B
⊢ (fun b => (a / b, c / b)) b ∈ (A / B) ×ˢ (C / B) ∧
    match (fun b => (a / b, c / b)) b with
    | (a_1, c_1) => a_1 / c_1 = a / c

Tactic:
exact ⟨mk_mem_product (div_mem_div ha hb) (div_mem_div hc hb), div_div_div_cancel_right ..⟩

Result:
no goals

Proof state:
case refine_1.intro.intro.intro.intro
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
a : G
ha : a ∈ A
c : G
hc : c ∈ C
hx : a / c ∈ A / C
⊢ #B ≤
    #(bipartiteAbove
        (fun b x =>
          match x with
          | (a, c) => a / c = b)
        ((A / B) ×ˢ (C / B)) (a / c))

Tactic:
refine card_le_card_of_injOn (fun b ↦ (a / b, c / b)) (fun b hb ↦ ?_) fun b₁ _ b₂ _ h ↦ ?_

Result:
case refine_1.intro.intro.intro.intro.refine_1
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
a : G
ha : a ∈ A
c : G
hc : c ∈ C
hx : a / c ∈ A / C
b : G
hb : b ∈ B
⊢ (fun b => (a / b, c / b)) b ∈
    bipartiteAbove
      (fun b x =>
        match x with
        | (a, c) => a / c = b)
      ((A / B) ×ˢ (C / B)) (a / c)

case refine_1.intro.intro.intro.intro.refine_2
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
a : G
ha : a ∈ A
c : G
hc : c ∈ C
hx : a / c ∈ A / C
b₁ : G
x✝¹ : b₁ ∈ ↑B
b₂ : G
x✝ : b₂ ∈ ↑B
h : (fun b => (a / b, c / b)) b₁ = (fun b => (a / b, c / b)) b₂
⊢ b₁ = b₂

Proof state:
case refine_1.intro.intro.intro.intro.refine_1
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
a : G
ha : a ∈ A
c : G
hc : c ∈ C
hx : a / c ∈ A / C
b : G
hb : b ∈ B
⊢ (fun b => (a / b, c / b)) b ∈
    bipartiteAbove
      (fun b x =>
        match x with
        | (a, c) => a / c = b)
      ((A / B) ×ˢ (C / B)) (a / c)

Tactic:
rw [mem_bipartiteAbove]

Result:
case refine_1.intro.intro.intro.intro.refine_1
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
a : G
ha : a ∈ A
c : G
hc : c ∈ C
hx : a / c ∈ A / C
b : G
hb : b ∈ B
⊢ (fun b => (a / b, c / b)) b ∈ (A / B) ×ˢ (C / B) ∧
    match (fun b => (a / b, c / b)) b with
    | (a_1, c_1) => a_1 / c_1 = a / c

Proof state:
case refine_1.intro.intro.intro.intro.refine_2
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
a : G
ha : a ∈ A
c : G
hc : c ∈ C
hx : a / c ∈ A / C
b₁ : G
x✝¹ : b₁ ∈ ↑B
b₂ : G
x✝ : b₂ ∈ ↑B
h : (fun b => (a / b, c / b)) b₁ = (fun b => (a / b, c / b)) b₂
⊢ b₁ = b₂

Tactic:
exact div_right_injective (Prod.ext_iff.1 h).1

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
⊢ #(A / C) * #B ≤ #((A / B) ×ˢ (C / B)) * 1

Tactic:
refine card_mul_le_card_mul (fun b (a, c) ↦ a / c = b) (fun x hx ↦ ?_)
  fun x _ ↦ card_le_one_iff.2 fun hu hv ↦
    ((mem_bipartiteBelow _).1 hu).2.symm.trans ?_

Result:
case refine_1
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
x : G
hx : x ∈ A / C
⊢ #B ≤
    #(bipartiteAbove
        (fun b x =>
          match x with
          | (a, c) => a / c = b)
        ((A / B) ×ˢ (C / B)) x)

case refine_2
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
x : G × G
x✝ : x ∈ (A / B) ×ˢ (C / B)
a✝ b✝ : G
hu :
  a✝ ∈
    bipartiteBelow
      (fun b x =>
        match x with
        | (a, c) => a / c = b)
      (A / C) x
hv :
  b✝ ∈
    bipartiteBelow
      (fun b x =>
        match x with
        | (a, c) => a / c = b)
      (A / C) x
⊢ x.1 / x.2 = b✝