α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
⊢ card (A / C) * card B ≤ card ((A / B) ×ˢ (B / C)) * 1
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
⊢ card (A / C) * card B ≤ card (A / B) * card (B / C)
rw [← card_product (A / B), ← mul_one ((A / B) ×ˢ (B / C)).card]
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
x : α
hx : x ∈ A / C
⊢ card B ≤ card (bipartiteAbove (fun b ac => ac.fst * ac.snd = b) ((A / B) ×ˢ (B / C)) x)
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
⊢ card (A / C) * card B ≤ card ((A / B) ×ˢ (B / C)) * 1
refine' card_mul_le_card_mul (fun b ac ↦ ac.1 * ac.2 = b) (fun x hx ↦ _)
  fun x _ ↦ card_le_one_iff.2 fun hu hv ↦
    ((mem_bipartiteBelow _).1 hu).2.symm.trans ((mem_bipartiteBelow _).1 hv).2
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
a c : α
ha : a ∈ A
hc : c ∈ C
hx : a / c ∈ A / C
⊢ card B ≤ card (bipartiteAbove (fun b ac => ac.fst * ac.snd = b) ((A / B) ×ˢ (B / C)) (a / c))
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
x : α
hx : x ∈ A / C
⊢ card B ≤ card (bipartiteAbove (fun b ac => ac.fst * ac.snd = b) ((A / B) ×ˢ (B / C)) x)
obtain ⟨a, c, ha, hc, rfl⟩ := mem_div.1 hx
case intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
a c : α
ha : a ∈ A
hc : c ∈ C
hx : a / c ∈ A / C
b : α
hb : b ∈ B
⊢ (fun b => (a / b, b / c)) b ∈ bipartiteAbove (fun b ac => ac.fst * ac.snd = b) ((A / B) ×ˢ (B / C)) (a / c)

case intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
a c : α
ha : a ∈ A
hc : c ∈ C
hx : a / c ∈ A / C
b₁ : α
x✝¹ : b₁ ∈ B
b₂ : α
x✝ : b₂ ∈ B
h : (fun b => (a / b, b / c)) b₁ = (fun b => (a / b, b / c)) b₂
⊢ b₁ = b₂
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
a c : α
ha : a ∈ A
hc : c ∈ C
hx : a / c ∈ A / C
⊢ card B ≤ card (bipartiteAbove (fun b ac => ac.fst * ac.snd = b) ((A / B) ×ˢ (B / C)) (a / c))
refine' card_le_card_of_inj_on (fun b ↦ (a / b, b / c)) (fun b hb ↦ _) fun b₁ _ b₂ _ h ↦ _
case intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
a c : α
ha : a ∈ A
hc : c ∈ C
hx : a / c ∈ A / C
b : α
hb : b ∈ B
⊢ (fun b => (a / b, b / c)) b ∈ (A / B) ×ˢ (B / C) ∧
    ((fun b => (a / b, b / c)) b).fst * ((fun b => (a / b, b / c)) b).snd = a / c
case intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
a c : α
ha : a ∈ A
hc : c ∈ C
hx : a / c ∈ A / C
b : α
hb : b ∈ B
⊢ (fun b => (a / b, b / c)) b ∈ bipartiteAbove (fun b ac => ac.fst * ac.snd = b) ((A / B) ×ˢ (B / C)) (a / c)
rw [mem_bipartiteAbove]
no goals
case intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
a c : α
ha : a ∈ A
hc : c ∈ C
hx : a / c ∈ A / C
b : α
hb : b ∈ B
⊢ (fun b => (a / b, b / c)) b ∈ (A / B) ×ˢ (B / C) ∧
    ((fun b => (a / b, b / c)) b).fst * ((fun b => (a / b, b / c)) b).snd = a / c
exact ⟨mk_mem_product (div_mem_div ha hb) (div_mem_div hb hc), div_mul_div_cancel' _ _ _⟩
no goals
case intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
a c : α
ha : a ∈ A
hc : c ∈ C
hx : a / c ∈ A / C
b₁ : α
x✝¹ : b₁ ∈ B
b₂ : α
x✝ : b₂ ∈ B
h : (fun b => (a / b, b / c)) b₁ = (fun b => (a / b, b / c)) b₂
⊢ b₁ = b₂
exact div_right_injective (Prod.ext_iff.1 h).1