awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
h : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
rw : #(A * B) * (#(C * A) + #A) - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) = #(A * B) * #(C' * A)
⊢ #(A * B) * #(C * A) + #(A * B) * #A - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) = #(A * B) * #(C' * A)
have rw₁ : #(A * B) * (#(C * A) + #A - #(A ∩ ({x}⁻¹ * C * A))) = #(A * B) * #(C' * A)
Tactic: rw [← mul_add, ← mul_tsub, ← hA', hC', insert_eq, union_mul, ← card_singleton_mul x A,
          ← card_singleton_mul x A', add_comm #_, h₀,
          eq_tsub_of_add_eq (card_union_add_card_inter _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
h : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
rw : #(A * B) * (#(C * A) + #A) - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) = #(A * B) * #(C' * A)
rw₁ : #(A * B) * (#(C * A) + #A - #(A ∩ ({x}⁻¹ * C * A))) = #(A * B) * #(C' * A)
rw₂ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #(C' * A)
rw₃ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #(insert x C * A)
⊢ #(A * B) * #(C * A) + #(A * B) * #A - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) = #(A * B) * #(C' * A)
have rw₄ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #(({x} ∪ C) * A)
Tactic: rw [← mul_add, ← mul_tsub, ← hA', hC', insert_eq, union_mul, ← card_singleton_mul x A,
          ← card_singleton_mul x A', add_comm #_, h₀,
          eq_tsub_of_add_eq (card_union_add_card_inter _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
h : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
rw : #(A * B) * (#(C * A) + #A) - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) = #(A * B) * #(C' * A)
rw₁ : #(A * B) * (#(C * A) + #A - #(A ∩ ({x}⁻¹ * C * A))) = #(A * B) * #(C' * A)
rw₂ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #(C' * A)
rw₃ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #(insert x C * A)
rw₄ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #(({x} ∪ C) * A)
⊢ #(A * B) * #(C * A) + #(A * B) * #A - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) = #(A * B) * #(C' * A)
have rw₅ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #({x} * A ∪ C * A)
Tactic: rw [← mul_add, ← mul_tsub, ← hA', hC', insert_eq, union_mul, ← card_singleton_mul x A,
          ← card_singleton_mul x A', add_comm #_, h₀,
          eq_tsub_of_add_eq (card_union_add_card_inter _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
h : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
rw : #(A * B) * (#(C * A) + #A) - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) = #(A * B) * #(C' * A)
rw₁ : #(A * B) * (#(C * A) + #A - #(A ∩ ({x}⁻¹ * C * A))) = #(A * B) * #(C' * A)
rw₂ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #(C' * A)
rw₃ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #(insert x C * A)
rw₄ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #(({x} ∪ C) * A)
rw₅ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #({x} * A ∪ C * A)
⊢ #(A * B) * #(C * A) + #(A * B) * #A - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) = #(A * B) * #(C' * A)
have rw₆ : #(A * B) * (#(C * A) + #({x} * A) - #A') = #(A * B) * #({x} * A ∪ C * A)
Tactic: rw [← mul_add, ← mul_tsub, ← hA', hC', insert_eq, union_mul, ← card_singleton_mul x A,
          ← card_singleton_mul x A', add_comm #_, h₀,
          eq_tsub_of_add_eq (card_union_add_card_inter _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
h : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
rw : #(A * B) * (#(C * A) + #A) - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) = #(A * B) * #(C' * A)
rw₁ : #(A * B) * (#(C * A) + #A - #(A ∩ ({x}⁻¹ * C * A))) = #(A * B) * #(C' * A)
rw₂ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #(C' * A)
rw₃ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #(insert x C * A)
rw₄ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #(({x} ∪ C) * A)
rw₅ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #({x} * A ∪ C * A)
rw₆ : #(A * B) * (#(C * A) + #({x} * A) - #A') = #(A * B) * #({x} * A ∪ C * A)
⊢ #(A * B) * #(C * A) + #(A * B) * #A - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) = #(A * B) * #(C' * A)
have rw₇ : #(A * B) * (#(C * A) + #({x} * A) - #({x} * A')) = #(A * B) * #({x} * A ∪ C * A)
Tactic: rw [← mul_add, ← mul_tsub, ← hA', hC', insert_eq, union_mul, ← card_singleton_mul x A,
          ← card_singleton_mul x A', add_comm #_, h₀,
          eq_tsub_of_add_eq (card_union_add_card_inter _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
h : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
rw : #(A * B) * (#(C * A) + #A) - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) = #(A * B) * #(C' * A)
rw₁ : #(A * B) * (#(C * A) + #A - #(A ∩ ({x}⁻¹ * C * A))) = #(A * B) * #(C' * A)
rw₂ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #(C' * A)
rw₃ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #(insert x C * A)
rw₄ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #(({x} ∪ C) * A)
rw₅ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #({x} * A ∪ C * A)
rw₆ : #(A * B) * (#(C * A) + #({x} * A) - #A') = #(A * B) * #({x} * A ∪ C * A)
rw₇ : #(A * B) * (#(C * A) + #({x} * A) - #({x} * A')) = #(A * B) * #({x} * A ∪ C * A)
⊢ #(A * B) * #(C * A) + #(A * B) * #A - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) = #(A * B) * #(C' * A)
have rw₈ : #(A * B) * (#({x} * A) + #(C * A) - #({x} * A')) = #(A * B) * #({x} * A ∪ C * A)
Tactic: rw [← mul_add, ← mul_tsub, ← hA', hC', insert_eq, union_mul, ← card_singleton_mul x A,
          ← card_singleton_mul x A', add_comm #_, h₀,
          eq_tsub_of_add_eq (card_union_add_card_inter _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
h : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
rw : #(A * B) * (#(C * A) + #A) - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) = #(A * B) * #(C' * A)
rw₁ : #(A * B) * (#(C * A) + #A - #(A ∩ ({x}⁻¹ * C * A))) = #(A * B) * #(C' * A)
rw₂ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #(C' * A)
rw₃ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #(insert x C * A)
rw₄ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #(({x} ∪ C) * A)
rw₅ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #({x} * A ∪ C * A)
rw₆ : #(A * B) * (#(C * A) + #({x} * A) - #A') = #(A * B) * #({x} * A ∪ C * A)
rw₇ : #(A * B) * (#(C * A) + #({x} * A) - #({x} * A')) = #(A * B) * #({x} * A ∪ C * A)
rw₈ : #(A * B) * (#({x} * A) + #(C * A) - #({x} * A')) = #(A * B) * #({x} * A ∪ C * A)
⊢ #(A * B) * #(C * A) + #(A * B) * #A - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) = #(A * B) * #(C' * A)
have rw₉ : #(A * B) * (#({x} * A) + #(C * A) - #({x} * A ∩ (C * A))) = #(A * B) * #({x} * A ∪ C * A)
Tactic: rw [← mul_add, ← mul_tsub, ← hA', hC', insert_eq, union_mul, ← card_singleton_mul x A,
          ← card_singleton_mul x A', add_comm #_, h₀,
          eq_tsub_of_add_eq (card_union_add_card_inter _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
h : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
rw : #(A * B) * (#(C * A) + #A) - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) = #(A * B) * #(C' * A)
rw₁ : #(A * B) * (#(C * A) + #A - #(A ∩ ({x}⁻¹ * C * A))) = #(A * B) * #(C' * A)
rw₂ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #(C' * A)
rw₃ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #(insert x C * A)
rw₄ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #(({x} ∪ C) * A)
rw₅ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #({x} * A ∪ C * A)
rw₆ : #(A * B) * (#(C * A) + #({x} * A) - #A') = #(A * B) * #({x} * A ∪ C * A)
rw₇ : #(A * B) * (#(C * A) + #({x} * A) - #({x} * A')) = #(A * B) * #({x} * A ∪ C * A)
rw₈ : #(A * B) * (#({x} * A) + #(C * A) - #({x} * A')) = #(A * B) * #({x} * A ∪ C * A)
rw₉ : #(A * B) * (#({x} * A) + #(C * A) - #({x} * A ∩ (C * A))) = #(A * B) * #({x} * A ∪ C * A)
⊢ #(A * B) * #(C * A) + #(A * B) * #A - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) = #(A * B) * #(C' * A)
have rw₁₀ : #(A * B) * (#({x} * A) + #(C * A) - #({x} * A ∩ (C * A))) = #(A * B) * (#({x} * A) + #(C * A) - #({x} * A ∩ (C * A)))
Tactic: rw [← mul_add, ← mul_tsub, ← hA', hC', insert_eq, union_mul, ← card_singleton_mul x A,
          ← card_singleton_mul x A', add_comm #_, h₀,
          eq_tsub_of_add_eq (card_union_add_card_inter _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
h : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
⊢ #(C' * A * B) * #A ≤ #(A * B) * #(C' * A)
have A₁ : #(C' * A * B) * #A ≤ (#(C * A * B) + #(A * B) - #(A' * B)) * #A
Tactic: calc
      #(C' * A * B) * #A
      _ ≤ (#(C * A * B) + #(A * B) - #(A' * B)) * #A := by
        gcongr
        rw [h₁]
        refine (card_union_le _ _).trans_eq ?_
        rw [card_sdiff_of_subset h₂, ← add_tsub_assoc_of_le (card_le_card h₂), mul_assoc {_},
          mul_assoc {_}, card_singleton_mul, card_singleton_mul]
      _ = #(C * A * B) * #A + #(A * B) * #A - #(A' * B) * #A := by rw [tsub_mul, add_mul]
      _ ≤ #(A * B) * #(C * A) + #(A * B) * #A - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) := by
        gcongr ?_ + _ - ?_; exact hA _ inter_subset_left
      _ = #(A * B) * #(C' * A) := by
        rw [← mul_add, ← mul_tsub, ← hA', hC', insert_eq, union_mul, ← card_singleton_mul x A,
          ← card_singleton_mul x A', add_comm #_, h₀,
          eq_tsub_of_add_eq (card_union_add_card_inter _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
h : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
A₁ : #(C' * A * B) * #A ≤ (#(C * A * B) + #(A * B) - #(A' * B)) * #A
⊢ #(C' * A * B) * #A ≤ #(A * B) * #(C' * A)
have A₂ : (#(C * A * B) + #(A * B) - #(A' * B)) * #A = #(C * A * B) * #A + #(A * B) * #A - #(A' * B) * #A
Tactic: calc
      #(C' * A * B) * #A
      _ ≤ (#(C * A * B) + #(A * B) - #(A' * B)) * #A := by
        gcongr
        rw [h₁]
        refine (card_union_le _ _).trans_eq ?_
        rw [card_sdiff_of_subset h₂, ← add_tsub_assoc_of_le (card_le_card h₂), mul_assoc {_},
          mul_assoc {_}, card_singleton_mul, card_singleton_mul]
      _ = #(C * A * B) * #A + #(A * B) * #A - #(A' * B) * #A := by rw [tsub_mul, add_mul]
      _ ≤ #(A * B) * #(C * A) + #(A * B) * #A - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) := by
        gcongr ?_ + _ - ?_; exact hA _ inter_subset_left
      _ = #(A * B) * #(C' * A) := by
        rw [← mul_add, ← mul_tsub, ← hA', hC', insert_eq, union_mul, ← card_singleton_mul x A,
          ← card_singleton_mul x A', add_comm #_, h₀,
          eq_tsub_of_add_eq (card_union_add_card_inter _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
h : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
A₁ : #(C' * A * B) * #A ≤ (#(C * A * B) + #(A * B) - #(A' * B)) * #A
A₂ : (#(C * A * B) + #(A * B) - #(A' * B)) * #A = #(C * A * B) * #A + #(A * B) * #A - #(A' * B) * #A
⊢ #(C' * A * B) * #A ≤ #(A * B) * #(C' * A)
have A₃ : #(C * A * B) * #A + #(A * B) * #A - #(A' * B) * #A ≤
  #(A * B) * #(C * A) + #(A * B) * #A - #(A * B) * #(A ∩ ({x}⁻¹ * C * A))
Tactic: calc
      #(C' * A * B) * #A
      _ ≤ (#(C * A * B) + #(A * B) - #(A' * B)) * #A := by
        gcongr
        rw [h₁]
        refine (card_union_le _ _).trans_eq ?_
        rw [card_sdiff_of_subset h₂, ← add_tsub_assoc_of_le (card_le_card h₂), mul_assoc {_},
          mul_assoc {_}, card_singleton_mul, card_singleton_mul]
      _ = #(C * A * B) * #A + #(A * B) * #A - #(A' * B) * #A := by rw [tsub_mul, add_mul]
      _ ≤ #(A * B) * #(C * A) + #(A * B) * #A - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) := by
        gcongr ?_ + _ - ?_; exact hA _ inter_subset_left
      _ = #(A * B) * #(C' * A) := by
        rw [← mul_add, ← mul_tsub, ← hA', hC', insert_eq, union_mul, ← card_singleton_mul x A,
          ← card_singleton_mul x A', add_comm #_, h₀,
          eq_tsub_of_add_eq (card_union_add_card_inter _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
h : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
A₁ : #(C' * A * B) * #A ≤ (#(C * A * B) + #(A * B) - #(A' * B)) * #A
A₂ : (#(C * A * B) + #(A * B) - #(A' * B)) * #A = #(C * A * B) * #A + #(A * B) * #A - #(A' * B) * #A
A₃ :
  #(C * A * B) * #A + #(A * B) * #A - #(A' * B) * #A ≤
    #(A * B) * #(C * A) + #(A * B) * #A - #(A * B) * #(A ∩ ({x}⁻¹ * C * A))
⊢ #(C' * A * B) * #A ≤ #(A * B) * #(C' * A)
have A₄ : #(A * B) * #(C * A) + #(A * B) * #A - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) = #(A * B) * #(C' * A)
Tactic: calc
      #(C' * A * B) * #A
      _ ≤ (#(C * A * B) + #(A * B) - #(A' * B)) * #A := by
        gcongr
        rw [h₁]
        refine (card_union_le _ _).trans_eq ?_
        rw [card_sdiff_of_subset h₂, ← add_tsub_assoc_of_le (card_le_card h₂), mul_assoc {_},
          mul_assoc {_}, card_singleton_mul, card_singleton_mul]
      _ = #(C * A * B) * #A + #(A * B) * #A - #(A' * B) * #A := by rw [tsub_mul, add_mul]
      _ ≤ #(A * B) * #(C * A) + #(A * B) * #A - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) := by
        gcongr ?_ + _ - ?_; exact hA _ inter_subset_left
      _ = #(A * B) * #(C' * A) := by
        rw [← mul_add, ← mul_tsub, ← hA', hC', insert_eq, union_mul, ← card_singleton_mul x A,
          ← card_singleton_mul x A', add_comm #_, h₀,
          eq_tsub_of_add_eq (card_union_add_card_inter _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B C : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
⊢ #(C * A * B) * #A ≤ #(A * B) * #(C * A)
have empty : #(∅ * A * B) * #A ≤ #(A * B) * #(∅ * A)
Tactic: induction C using Finset.induction_on with
  | empty => simp
  | insert x C _ ih =>
    set A' := A ∩ ({x}⁻¹ * C * A) with hA'
    set C' := insert x C with hC'
    have h₀ : {x} * A' = {x} * A ∩ (C * A) := by
      rw [hA', mul_assoc, singleton_mul_inter, (isUnit_singleton x).mul_inv_cancel_left]
    have h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B) := by
      rw [hC', insert_eq, union_comm, union_mul, union_mul]
      refine (sup_sdiff_eq_sup ?_).symm
      rw [h₀]
      gcongr
      exact inter_subset_right
    have h₂ : {x} * A' * B ⊆ {x} * A * B := by gcongr; exact inter_subset_left
    calc
      #(C' * A * B) * #A
      _ ≤ (#(C * A * B) + #(A * B) - #(A' * B)) * #A := by
        gcongr
        rw [h₁]
        refine (card_union_le _ _).trans_eq ?_
        rw [card_sdiff_of_subset h₂, ← add_tsub_assoc_of_le (card_le_card h₂), mul_assoc {_},
          mul_assoc {_}, card_singleton_mul, card_singleton_mul]
      _ = #(C * A * B) * #A + #(A * B) * #A - #(A' * B) * #A := by rw [tsub_mul, add_mul]
      _ ≤ #(A * B) * #(C * A) + #(A * B) * #A - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) := by
        gcongr ?_ + _ - ?_; exact hA _ inter_subset_left
      _ = #(A * B) * #(C' * A) := by
        rw [← mul_add, ← mul_tsub, ← hA', hC', insert_eq, union_mul, ← card_singleton_mul x A,
          ← card_singleton_mul x A', add_comm #_, h₀,
          eq_tsub_of_add_eq (card_union_add_card_inter _ _)]
Cleared hypotheses: C
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B C : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
empty : #(∅ * A * B) * #A ≤ #(A * B) * #(∅ * A)
⊢ #(C * A * B) * #A ≤ #(A * B) * #(C * A)
have insert : ∀ (x : G) (C : Finset G),
  x ∉ C → ∀ (ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)), #(insert x C * A * B) * #A ≤ #(A * B) * #(insert x C * A)
Tactic: induction C using Finset.induction_on with
  | empty => simp
  | insert x C _ ih =>
    set A' := A ∩ ({x}⁻¹ * C * A) with hA'
    set C' := insert x C with hC'
    have h₀ : {x} * A' = {x} * A ∩ (C * A) := by
      rw [hA', mul_assoc, singleton_mul_inter, (isUnit_singleton x).mul_inv_cancel_left]
    have h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B) := by
      rw [hC', insert_eq, union_comm, union_mul, union_mul]
      refine (sup_sdiff_eq_sup ?_).symm
      rw [h₀]
      gcongr
      exact inter_subset_right
    have h₂ : {x} * A' * B ⊆ {x} * A * B := by gcongr; exact inter_subset_left
    calc
      #(C' * A * B) * #A
      _ ≤ (#(C * A * B) + #(A * B) - #(A' * B)) * #A := by
        gcongr
        rw [h₁]
        refine (card_union_le _ _).trans_eq ?_
        rw [card_sdiff_of_subset h₂, ← add_tsub_assoc_of_le (card_le_card h₂), mul_assoc {_},
          mul_assoc {_}, card_singleton_mul, card_singleton_mul]
      _ = #(C * A * B) * #A + #(A * B) * #A - #(A' * B) * #A := by rw [tsub_mul, add_mul]
      _ ≤ #(A * B) * #(C * A) + #(A * B) * #A - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) := by
        gcongr ?_ + _ - ?_; exact hA _ inter_subset_left
      _ = #(A * B) * #(C' * A) := by
        rw [← mul_add, ← mul_tsub, ← hA', hC', insert_eq, union_mul, ← card_singleton_mul x A,
          ← card_singleton_mul x A', add_comm #_, h₀,
          eq_tsub_of_add_eq (card_union_add_card_inter _ _)]
Cleared hypotheses: C
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B C : Finset G
hA : A.Nonempty
hAB : A ⊆ B
h :
  ∀ A' ∈ B.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(A * C)) : ℚ≥0) (↑(#A) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A' * C)) : ℚ≥0) (↑(#A') : ℚ≥0)
A' : Finset G
hAA' : A' ⊆ A
⊢ #(A * C) * #A' ≤ #(A' * C) * #A
have inl : ∀ (hAA' : ∅ ⊆ A), #(A * C) * card.{u_1} (α := G) ∅ ≤ #(∅ * C) * #A
Tactic: obtain rfl | hA' := A'.eq_empty_or_nonempty
Cleared hypotheses: A', hAA'
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B C : Finset G
hA : A.Nonempty
hAB : A ⊆ B
h :
  ∀ A' ∈ B.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(A * C)) : ℚ≥0) (↑(#A) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A' * C)) : ℚ≥0) (↑(#A') : ℚ≥0)
A' : Finset G
hAA' : A' ⊆ A
inl : ∀ (hAA' : ∅ ⊆ A), #(A * C) * card.{u_1} (α := G) ∅ ≤ #(∅ * C) * #A
⊢ #(A * C) * #A' ≤ #(A' * C) * #A
have inr : ∀ (hA' : A'.Nonempty), #(A * C) * #A' ≤ #(A' * C) * #A
Tactic: obtain rfl | hA' := A'.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (hypothesis)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B C : Finset G
hA : A.Nonempty
hAB : A ⊆ B
h :
  ∀ A' ∈ B.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(A * C)) : ℚ≥0) (↑(#A) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A' * C)) : ℚ≥0) (↑(#A') : ℚ≥0)
A' : Finset G
hAA' : A' ⊆ A
hA' : A'.Nonempty
⊢ #(A * C) * #A' ≤ #(A' * C) * #A
have hA₀ : LT.lt (α := ℚ≥0) 0 (↑(#A) : ℚ≥0)
Tactic: have hA₀ : (0 : ℚ≥0) < #A := cast_pos.2 hA.card_pos
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (hypothesis)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B C : Finset G
hA : A.Nonempty
hAB : A ⊆ B
h :
  ∀ A' ∈ B.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(A * C)) : ℚ≥0) (↑(#A) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A' * C)) : ℚ≥0) (↑(#A') : ℚ≥0)
A' : Finset G
hAA' : A' ⊆ A
hA' : A'.Nonempty
hA₀ : LT.lt (α := ℚ≥0) 0 (↑(#A) : ℚ≥0)
⊢ #(A * C) * #A' ≤ #(A' * C) * #A
have hA₀' : LT.lt (α := ℚ≥0) 0 (↑(#A') : ℚ≥0)
Tactic: have hA₀' : (0 : ℚ≥0) < #A' := cast_pos.2 hA'.card_pos
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B C : Finset G
⊢ #(A * C) * #B ≤ #(A * B) * #(B * C)
have inl : #(A * C) * card.{u_1} (α := G) ∅ ≤ #(A * ∅) * #(∅ * C)
Tactic: obtain rfl | hB := B.eq_empty_or_nonempty
Cleared hypotheses: B
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B C : Finset G
inl : #(A * C) * card.{u_1} (α := G) ∅ ≤ #(A * ∅) * #(∅ * C)
⊢ #(A * C) * #B ≤ #(A * B) * #(B * C)
have inr : ∀ (hB : B.Nonempty), #(A * C) * #B ≤ #(A * B) * #(B * C)
Tactic: obtain rfl | hB := B.eq_empty_or_nonempty