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 C : Finset G
refine_1 :
  ∀ (x : G) (hx : x ∈ A / C),
    #B ≤
      #(bipartiteAbove
          (fun (b : G) (x : G × G) ↦
            match (motive := G × G → Prop) x with
            | (a, c) => a / c = b)
          ((A / B) ×ˢ (C / B)) x)
⊢ #(A / C) * #B ≤ #((A / B) ×ˢ (C / B)) * 1
have refine_2 : ∀ x ∈ (A / B) ×ˢ (C / B),
  ∀ {a b : G}
    (hu :
      a ∈
        bipartiteBelow
          (fun (b : G) (x : G × G) ↦
            match (motive := G × G → Prop) x with
            | (a, c) => a / c = b)
          (A / C) x)
    (hv :
      b ∈
        bipartiteBelow
          (fun (b : G) (x : G × G) ↦
            match (motive := G × G → Prop) x with
            | (a, c) => a / c = b)
          (A / C) x),
    x.1 / x.2 = b
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 ?_
-- 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
x : G
hx : x ∈ A / C
⊢ #B ≤
    #(bipartiteAbove
        (fun (b : G) (x : G × G) ↦
          match (motive := G × G → Prop) x with
          | (a, c) => a / c = b)
        ((A / B) ×ˢ (C / B)) x)
have refine_1 : ∀ (a : G) (ha : a ∈ A) (c : G) (hc : c ∈ C) (hx : a / c ∈ A / C),
  #B ≤
    #(bipartiteAbove
        (fun (b : G) (x : G × G) ↦
          match (motive := G × G → Prop) x with
          | (a, c) => a / c = b)
        ((A / B) ×ˢ (C / B)) (a / c))
Tactic: obtain ⟨a, ha, c, hc, rfl⟩ := mem_div.1 hx
Cleared hypotheses: x, hx
-- 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
a : G
ha : a ∈ A
c : G
hc : c ∈ C
hx : a / c ∈ A / C
⊢ #B ≤
    #(bipartiteAbove
        (fun (b : G) (x : G × G) ↦
          match (motive := G × G → Prop) x with
          | (a, c) => a / c = b)
        ((A / B) ×ˢ (C / B)) (a / c))
have refine_1 : ∀ (b : G) (hb : b ∈ (↑B : Set G)),
  (fun (b : G) ↦ (a / b, c / b)) b ∈
    (↑(bipartiteAbove
          (fun (b : G) (x : G × G) ↦
            match (motive := G × G → Prop) x with
            | (a, c) => a / c = b)
          ((A / B) ×ˢ (C / B)) (a / c)) :
      Set (G × G))
Tactic: refine card_le_card_of_injOn (fun b ↦ (a / b, c / b)) (fun b hb ↦ ?_) fun b₁ _ b₂ _ h ↦ ?_
-- 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
a : G
ha : a ∈ A
c : G
hc : c ∈ C
hx : a / c ∈ A / C
refine_1 :
  ∀ (b : G) (hb : b ∈ (↑B : Set G)),
    (fun (b : G) ↦ (a / b, c / b)) b ∈
      (↑(bipartiteAbove
            (fun (b : G) (x : G × G) ↦
              match (motive := G × G → Prop) x with
              | (a, c) => a / c = b)
            ((A / B) ×ˢ (C / B)) (a / c)) :
        Set (G × G))
⊢ #B ≤
    #(bipartiteAbove
        (fun (b : G) (x : G × G) ↦
          match (motive := G × G → Prop) x with
          | (a, c) => a / c = b)
        ((A / B) ×ˢ (C / B)) (a / c))
have refine_1₁ : ∀ b₁ ∈ (↑B : Set G),
  ∀ b₂ ∈ (↑B : Set G),
    ∀ (h : Eq.{u_1 + 1} (α := G × G) ((fun (b : G) ↦ (a / b, c / b)) b₁) ((fun (b : G) ↦ (a / b, c / b)) b₂)), b₁ = b₂
Tactic: refine card_le_card_of_injOn (fun b ↦ (a / b, c / b)) (fun b hb ↦ ?_) fun b₁ _ b₂ _ h ↦ ?_
-- 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
a : G
ha : a ∈ A
c : G
hc : c ∈ C
hx : a / c ∈ A / C
b : G
hb : b ∈ (↑B : Set G)
⊢ (fun (b : G) ↦ (a / b, c / b)) b ∈
    (↑(bipartiteAbove
          (fun (b : G) (x : G × G) ↦
            match (motive := G × G → Prop) x with
            | (a, c) => a / c = b)
          ((A / B) ×ˢ (C / B)) (a / c)) :
      Set (G × G))
have refine_1 : (fun (b : G) ↦ (a / b, c / b)) b ∈ (A / B) ×ˢ (C / B) ∧
  match (motive := G × G → Prop) (fun (b : G) ↦ (a / b, c / b)) b with
  | (a_1, c_1) => a_1 / c_1 = a / c
Tactic: rw [mem_coe, mem_bipartiteAbove]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (hypothesis)
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)
⊢ #(insert x C * A * B) * #A ≤ #(A * B) * #(insert x C * A)
have hA' : let A' := A ∩ ({x}⁻¹ * C * A);
A' = A ∩ ({x}⁻¹ * C * A)
Tactic: set A' := A ∩ ({x}⁻¹ * C * A) with hA'
-- 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)
⊢ #(insert x C * A * B) * #A ≤ #(A * B) * #(insert x C * A)
have insert : let C' := insert x C;
∀ (hC' : C' = insert x C), #(C' * A * B) * #A ≤ #(A * B) * #(C' * A)
Tactic: set C' := insert x C with hC'
-- 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
rw : {x} * (A ∩ ({x}⁻¹ * C * A)) = {x} * A ∩ (C * A)
⊢ {x} * A' = {x} * A ∩ (C * A)
have rw₁ : {x} * (A ∩ ({x}⁻¹ * (C * A))) = {x} * A ∩ (C * A)
Tactic: rw [hA', mul_assoc, singleton_mul_inter, (isUnit_singleton x).mul_inv_cancel_left]
-- 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
rw : {x} * (A ∩ ({x}⁻¹ * C * A)) = {x} * A ∩ (C * A)
rw₁ : {x} * (A ∩ ({x}⁻¹ * (C * A))) = {x} * A ∩ (C * A)
⊢ {x} * A' = {x} * A ∩ (C * A)
have rw₂ : {x} * A ∩ ({x} * ({x}⁻¹ * (C * A))) = {x} * A ∩ (C * A)
Tactic: rw [hA', mul_assoc, singleton_mul_inter, (isUnit_singleton x).mul_inv_cancel_left]
-- 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
rw : {x} * (A ∩ ({x}⁻¹ * C * A)) = {x} * A ∩ (C * A)
rw₁ : {x} * (A ∩ ({x}⁻¹ * (C * A))) = {x} * A ∩ (C * A)
rw₂ : {x} * A ∩ ({x} * ({x}⁻¹ * (C * A))) = {x} * A ∩ (C * A)
⊢ {x} * A' = {x} * A ∩ (C * A)
have rw₃ : {x} * A ∩ (C * A) = {x} * A ∩ (C * A)
Tactic: rw [hA', mul_assoc, singleton_mul_inter, (isUnit_singleton x).mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (hypothesis)
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
⊢ #(C' * A * B) * #A ≤ #(A * B) * #(C' * A)
have h₀ : {x} * A' = {x} * A ∩ (C * A)
Tactic: have h₀ : {x} * A' = {x} * A ∩ (C * A) := by
      rw [hA', mul_assoc, singleton_mul_inter, (isUnit_singleton x).mul_inv_cancel_left]
-- 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)
⊢ C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
have rw : C * A * B ∪ {x} * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
Tactic: rw [hC', insert_eq, union_comm, union_mul, union_mul]
-- 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)
⊢ C * A * B ∪ {x} * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
have refine : {x} * A' * B ≤ C * A * B
Tactic: refine (sup_sdiff_eq_sup ?_).symm
-- 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)
⊢ {x} * A' * B ≤ C * A * B
have rw : {x} * A ∩ (C * A) * B ≤ C * A * B
Tactic: rw [h₀]
-- 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)
⊢ {x} * A ∩ (C * A) * B ≤ C * A * B
have bc : {x} * A ∩ (C * A) ≤ C * A
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (hypothesis)
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)
⊢ #(C' * A * B) * #A ≤ #(A * B) * #(C' * A)
have h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
Tactic: 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
-- 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)
⊢ {x} * A' * B ⊆ {x} * A * B
have a : A' ⊆ A
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (hypothesis)
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)
⊢ #(C' * A * B) * #A ≤ #(A * B) * #(C' * A)
have h₂ : {x} * A' * B ⊆ {x} * A * B
Tactic: have h₂ : {x} * A' * B ⊆ {x} * A * B := by gcongr; exact inter_subset_left
-- 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 ≤ (#(C * A * B) + #(A * B) - #(A' * B)) * #A
have bc : #(C' * A * B) ≤ #(C * A * B) + #(A * B) - #(A' * B)
Tactic: gcongr
-- 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) ≤ #(C * A * B) + #(A * B) - #(A' * B)
have bc : #(C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)) ≤ #(C * A * B) + #(A * B) - #(A' * B)
Tactic: rw [h₁]
-- 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 ∪ ({x} * A * B) \ ({x} * A' * B)) ≤ #(C * A * B) + #(A * B) - #(A' * B)
have bc : #(C * A * B) + #(({x} * A * B) \ ({x} * A' * B)) = #(C * A * B) + #(A * B) - #(A' * B)
Tactic: refine (card_union_le _ _).trans_eq ?_
-- 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) + #(({x} * A * B) \ ({x} * A' * B)) = #(C * A * B) + #(A * B) - #(A' * B)
have bc : #(C * A * B) + (#({x} * A * B) - #({x} * A' * B)) = #(C * A * B) + #(A * B) - #(A' * B)
Tactic: 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]
-- 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
bc : #(C * A * B) + (#({x} * A * B) - #({x} * A' * B)) = #(C * A * B) + #(A * B) - #(A' * B)
⊢ #(C * A * B) + #(({x} * A * B) \ ({x} * A' * B)) = #(C * A * B) + #(A * B) - #(A' * B)
have bc₁ : #(C * A * B) + #({x} * A * B) - #({x} * A' * B) = #(C * A * B) + #(A * B) - #(A' * B)
Tactic: 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]
-- 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
bc : #(C * A * B) + (#({x} * A * B) - #({x} * A' * B)) = #(C * A * B) + #(A * B) - #(A' * B)
bc₁ : #(C * A * B) + #({x} * A * B) - #({x} * A' * B) = #(C * A * B) + #(A * B) - #(A' * B)
⊢ #(C * A * B) + #(({x} * A * B) \ ({x} * A' * B)) = #(C * A * B) + #(A * B) - #(A' * B)
have bc₂ : #(C * A * B) + #({x} * (A * B)) - #({x} * A' * B) = #(C * A * B) + #(A * B) - #(A' * B)
Tactic: 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]
-- 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
bc : #(C * A * B) + (#({x} * A * B) - #({x} * A' * B)) = #(C * A * B) + #(A * B) - #(A' * B)
bc₁ : #(C * A * B) + #({x} * A * B) - #({x} * A' * B) = #(C * A * B) + #(A * B) - #(A' * B)
bc₂ : #(C * A * B) + #({x} * (A * B)) - #({x} * A' * B) = #(C * A * B) + #(A * B) - #(A' * B)
⊢ #(C * A * B) + #(({x} * A * B) \ ({x} * A' * B)) = #(C * A * B) + #(A * B) - #(A' * B)
have bc₃ : #(C * A * B) + #({x} * (A * B)) - #({x} * (A' * B)) = #(C * A * B) + #(A * B) - #(A' * B)
Tactic: 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]
-- 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
bc : #(C * A * B) + (#({x} * A * B) - #({x} * A' * B)) = #(C * A * B) + #(A * B) - #(A' * B)
bc₁ : #(C * A * B) + #({x} * A * B) - #({x} * A' * B) = #(C * A * B) + #(A * B) - #(A' * B)
bc₂ : #(C * A * B) + #({x} * (A * B)) - #({x} * A' * B) = #(C * A * B) + #(A * B) - #(A' * B)
bc₃ : #(C * A * B) + #({x} * (A * B)) - #({x} * (A' * B)) = #(C * A * B) + #(A * B) - #(A' * B)
⊢ #(C * A * B) + #(({x} * A * B) \ ({x} * A' * B)) = #(C * A * B) + #(A * B) - #(A' * B)
have bc₄ : #(C * A * B) + #(A * B) - #({x} * (A' * B)) = #(C * A * B) + #(A * B) - #(A' * B)
Tactic: 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]
-- 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
bc : #(C * A * B) + (#({x} * A * B) - #({x} * A' * B)) = #(C * A * B) + #(A * B) - #(A' * B)
bc₁ : #(C * A * B) + #({x} * A * B) - #({x} * A' * B) = #(C * A * B) + #(A * B) - #(A' * B)
bc₂ : #(C * A * B) + #({x} * (A * B)) - #({x} * A' * B) = #(C * A * B) + #(A * B) - #(A' * B)
bc₃ : #(C * A * B) + #({x} * (A * B)) - #({x} * (A' * B)) = #(C * A * B) + #(A * B) - #(A' * B)
bc₄ : #(C * A * B) + #(A * B) - #({x} * (A' * B)) = #(C * A * B) + #(A * B) - #(A' * B)
⊢ #(C * A * B) + #(({x} * A * B) \ ({x} * A' * B)) = #(C * A * B) + #(A * B) - #(A' * B)
have bc₅ : #(C * A * B) + #(A * B) - #(A' * B) = #(C * A * B) + #(A * B) - #(A' * B)
Tactic: 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]
-- 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 * B) - #(A' * B)) * #A = #(C * A * B) * #A + #(A * B) * #A - #(A' * B) * #A
have rw : (#(C * A * B) + #(A * B)) * #A - #(A' * B) * #A = #(C * A * B) * #A + #(A * B) * #A - #(A' * B) * #A
Tactic: rw [tsub_mul, add_mul]
-- 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 : (#(C * A * B) + #(A * B)) * #A - #(A' * B) * #A = #(C * A * B) * #A + #(A * B) * #A - #(A' * B) * #A
⊢ (#(C * A * B) + #(A * B) - #(A' * B)) * #A = #(C * A * B) * #A + #(A * B) * #A - #(A' * B) * #A
have rw₁ : #(C * A * B) * #A + #(A * B) * #A - #(A' * B) * #A = #(C * A * B) * #A + #(A * B) * #A - #(A' * B) * #A
Tactic: rw [tsub_mul, add_mul]
-- 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) * #A - #(A' * B) * #A ≤
    #(A * B) * #(C * A) + #(A * B) * #A - #(A * B) * #(A ∩ ({x}⁻¹ * C * A))
have hcd : #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) ≤ #(A' * B) * #A
Tactic: gcongr ?_ + _ - ?_
-- 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 * B) * #(C * A) + #(A * B) * #A - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) = #(A * B) * #(C' * A)
have rw : #(A * B) * (#(C * A) + #A) - #(A * B) * #(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 _ _)]