-- Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean
theorem mul_aux (hA : A.Nonempty) (hAB : A ⊆ B)
    (h : ∀ A' ∈ B.powerset.erase ∅, (#(A * C) : ℚ≥0) / #A ≤ #(A' * C) / #A') :
    ∀ A' ⊆ A, #(A * C) * #A' ≤ #(A' * C) * #A

Proof state:
case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hA : A.Nonempty
hAB : A ⊆ B
h : ∀ A' ∈ B.powerset.erase ∅, ↑(#(A * C)) / ↑(#A) ≤ ↑(#(A' * C)) / ↑(#A')
A' : Finset G
hAA' : A' ⊆ A
hA' : A'.Nonempty
⊢ #(A * C) * #A' ≤ #(A' * C) * #A

Tactic:
have hA₀ : (0 : ℚ≥0) < #A := cast_pos.2 hA.card_pos

Result:
case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hA : A.Nonempty
hAB : A ⊆ B
h : ∀ A' ∈ B.powerset.erase ∅, ↑(#(A * C)) / ↑(#A) ≤ ↑(#(A' * C)) / ↑(#A')
A' : Finset G
hAA' : A' ⊆ A
hA' : A'.Nonempty
hA₀ : 0 < ↑(#A)
⊢ #(A * C) * #A' ≤ #(A' * C) * #A

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hA : A.Nonempty
hAB : A ⊆ B
h : ∀ A' ∈ B.powerset.erase ∅, ↑(#(A * C)) / ↑(#A) ≤ ↑(#(A' * C)) / ↑(#A')
A' : Finset G
hAA' : A' ⊆ A
⊢ #(A * C) * #A' ≤ #(A' * C) * #A

Tactic:
obtain rfl | hA' := A'.eq_empty_or_nonempty

Result:
case inl
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hA : A.Nonempty
hAB : A ⊆ B
h : ∀ A' ∈ B.powerset.erase ∅, ↑(#(A * C)) / ↑(#A) ≤ ↑(#(A' * C)) / ↑(#A')
hAA' : ∅ ⊆ A
⊢ #(A * C) * #∅ ≤ #(∅ * C) * #A

case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hA : A.Nonempty
hAB : A ⊆ B
h : ∀ A' ∈ B.powerset.erase ∅, ↑(#(A * C)) / ↑(#A) ≤ ↑(#(A' * C)) / ↑(#A')
A' : Finset G
hAA' : A' ⊆ A
hA' : A'.Nonempty
⊢ #(A * C) * #A' ≤ #(A' * C) * #A

Proof state:
case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hA : A.Nonempty
hAB : A ⊆ B
h : ∀ A' ∈ B.powerset.erase ∅, ↑(#(A * C)) / ↑(#A) ≤ ↑(#(A' * C)) / ↑(#A')
A' : Finset G
hAA' : A' ⊆ A
hA' : A'.Nonempty
hA₀ : 0 < ↑(#A)
hA₀' : 0 < ↑(#A')
⊢ #(A * C) * #A' ≤ #(A' * C) * #A

Tactic:
exact mod_cast
  (div_le_div_iff₀ hA₀ hA₀').1
    (h _ <| mem_erase_of_ne_of_mem hA'.ne_empty <| mem_powerset.2 <| hAA'.trans hAB)

Result:
no goals

Proof state:
case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hA : A.Nonempty
hAB : A ⊆ B
h : ∀ A' ∈ B.powerset.erase ∅, ↑(#(A * C)) / ↑(#A) ≤ ↑(#(A' * C)) / ↑(#A')
A' : Finset G
hAA' : A' ⊆ A
hA' : A'.Nonempty
hA₀ : 0 < ↑(#A)
⊢ #(A * C) * #A' ≤ #(A' * C) * #A

Tactic:
have hA₀' : (0 : ℚ≥0) < #A' := cast_pos.2 hA'.card_pos

Result:
case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hA : A.Nonempty
hAB : A ⊆ B
h : ∀ A' ∈ B.powerset.erase ∅, ↑(#(A * C)) / ↑(#A) ≤ ↑(#(A' * C)) / ↑(#A')
A' : Finset G
hAA' : A' ⊆ A
hA' : A'.Nonempty
hA₀ : 0 < ↑(#A)
hA₀' : 0 < ↑(#A')
⊢ #(A * C) * #A' ≤ #(A' * C) * #A

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hA : A.Nonempty
hAB : A ⊆ B
h : ∀ A' ∈ B.powerset.erase ∅, ↑(#(A * C)) / ↑(#A) ≤ ↑(#(A' * C)) / ↑(#A')
⊢ ∀ A' ⊆ A, #(A * C) * #A' ≤ #(A' * C) * #A

Tactic:
rintro A' hAA'

Result:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hA : A.Nonempty
hAB : A ⊆ B
h : ∀ A' ∈ B.powerset.erase ∅, ↑(#(A * C)) / ↑(#A) ≤ ↑(#(A' * C)) / ↑(#A')
A' : Finset G
hAA' : A' ⊆ A
⊢ #(A * C) * #A' ≤ #(A' * C) * #A

Proof state:
case inl
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hA : A.Nonempty
hAB : A ⊆ B
h : ∀ A' ∈ B.powerset.erase ∅, ↑(#(A * C)) / ↑(#A) ≤ ↑(#(A' * C)) / ↑(#A')
hAA' : ∅ ⊆ A
⊢ #(A * C) * #∅ ≤ #(∅ * C) * #A

Tactic:
simp

Result:
no goals