awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
h :
  ∀ (x : Fin (n + 1)),
    Membership.mem (γ := Set (Fin (n + 1))) (Iio (↑(k + 1) : Fin (n + 1))) x ↔
      Membership.mem (γ := Set (Fin (n + 1))) (Iic (↑k : Fin (n + 1))) x
⊢ Eq (α := Set (Fin (n + 1))) (Iio (↑(k + 1) : Fin (n + 1))) (Iic (↑k : Fin (n + 1)))

Tactic:
ext x
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
h : ∀ (x : ℕ), x ∈ Iio (k + 1) ↔ x ∈ Iic k
⊢ Iio (k + 1) = Iic k

Tactic:
ext x
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
x : Fin (n + 1)
h : (↑x : ℕ) < (↑(HAdd.hAdd (α := Fin (n + 1)) (↑k : Fin (n + 1)) 1) : ℕ) ↔ (↑x : ℕ) ≤ k
⊢ Membership.mem (γ := Set (Fin (n + 1))) (Iio (↑(k + 1) : Fin (n + 1))) x ↔
    Membership.mem (γ := Set (Fin (n + 1))) (Iic (↑k : Fin (n + 1))) x

Tactic:
simp only [Nat.cast_add, Nat.cast_one, mem_Iio, lt_def, mem_Iic, le_iff_val_le_val,
      val_natCast, aux hm hkmn', Nat.mod_eq_of_lt]

Premises used: Set.mem_Iio, Fin.val_natCast, _private.0.Fin.aux, Nat.mod_eq_of_lt, Nat.cast_add, Fin.lt_def, Set.mem_Iic, Nat.cast_one, Fin.le_iff_val_le_val
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
x : Fin (n + 1)
h : (↑x : ℕ) < (↑(↑(k + 1) : Fin (n + 1)) : ℕ) ↔ (↑x : ℕ) ≤ k
⊢ (↑x : ℕ) < (↑(HAdd.hAdd (α := Fin (n + 1)) (↑k : Fin (n + 1)) 1) : ℕ) ↔ (↑x : ℕ) ≤ k

Tactic:
simp_rw [← Nat.cast_add_one]

Premises used: Nat.cast_add_one
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
x : Fin (n + 1)
h : (↑x : ℕ) < k + 1 ↔ (↑x : ℕ) ≤ k
h₁ h₂ : (↑x : ℕ) ≤ k ↔ (↑x : ℕ) ≤ k
⊢ (↑x : ℕ) < (↑(↑(k + 1) : Fin (n + 1)) : ℕ) ↔ (↑x : ℕ) ≤ k

Tactic:
rw [Fin.val_cast_of_lt (aux hm hkmn), Nat.lt_succ_iff]

Premises used: _private.0.Fin.aux, Nat.lt_succ_iff, Fin.val_cast_of_lt
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
x : ℕ
⊢ x ∈ Iio (k + 1) ↔ x ∈ Iic k

Tactic:
simp [Nat.lt_succ_iff]

Premises used: Nat.lt_succ_iff
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B C : Finset G
rw : #(A / C) * #B ≤ #((A / B) ×ˢ (C / B)) * 1
⊢ #(A / C) * #B ≤ #(A / B) * #(C / B)

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

Premises used: SProd.sprod, Finset.card_product, HDiv.hDiv, Finset.card, mul_one
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B C : Finset G
⊢ #(A / C) * #B ≤ #((A / B) ×ˢ (C / B)) * 1

Tactic:
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 ?_

Premises used: Iff.mpr, Finset.card_mul_le_card_mul, Finset.card_le_one_iff
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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)
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
⊢ #(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 ?_

Premises used: Iff.mpr, Finset.card_mul_le_card_mul, Finset.card_le_one_iff
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B C : Finset G
x : G
hx : x ∈ A / C
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))
⊢ #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)

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

Premises used: Finset.mem_div, Iff.mp, rfl
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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))

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

Premises used: Finset.card_le_card_of_injOn, HDiv.hDiv, Prod.mk
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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))
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₂
⊢ #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:
refine card_le_card_of_injOn (fun b ↦ (a / b, c / b)) (fun b hb ↦ ?_) fun b₁ _ b₂ _ h ↦ ?_

Premises used: Finset.card_le_card_of_injOn, HDiv.hDiv, Prod.mk
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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)
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
⊢ (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:
rw [mem_coe, mem_bipartiteAbove]

Premises used: Finset.mem_bipartiteAbove, Finset.mem_coe
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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 ∈ (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:
⟨mk_mem_product (div_mem_div ha hb) (div_mem_div hc hb), div_div_div_cancel_right ..⟩

Premises used: Finset.mk_mem_product, div_div_div_cancel_right, And.intro, Finset.div_mem_div
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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 ∈ (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:
exact ⟨mk_mem_product (div_mem_div ha hb) (div_mem_div hc hb), div_div_div_cancel_right ..⟩
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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
h_1 : b₁ ∈ (↑B : Set G)
b₂ : G
h_2 : 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:
div_right_injective (Prod.ext_iff.1 h).1

Premises used: Prod.ext_iff, div_right_injective, And.left, Iff.mp
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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
h_1 : b₁ ∈ (↑B : Set G)
b₂ : G
h_2 : 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:
exact div_right_injective (Prod.ext_iff.1 h).1

Premises used: Prod.ext_iff, div_right_injective, And.left, Iff.mp
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B C : Finset G
x : G × G
h : 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:
((mem_bipartiteBelow _).1 hv).2

Premises used: And.right, Finset.mem_bipartiteBelow, Iff.mp
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B C : Finset G
x : G × G
h : 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:
exact ((mem_bipartiteBelow _).1 hv).2

Premises used: And.right, Finset.mem_bipartiteBelow, Iff.mp
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B C : Finset G
⊢ #(A * C⁻¹) * #B ≤ #(A * B⁻¹) * #(C * B⁻¹)

Tactic:
simpa [div_eq_mul_inv] using ruzsa_triangle_inequality_div_div_div A B C

Premises used: div_eq_mul_inv, Finset.ruzsa_triangle_inequality_div_div_div
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B C : Finset G
⊢ #B * #(A⁻¹ * C) ≤ #(B⁻¹ * A) * #(B⁻¹ * C)

Tactic:
simpa [mul_comm, div_eq_mul_inv, ← map_op_mul, ← map_op_inv] using
    ruzsa_triangle_inequality_div_div_div (G := Gᵐᵒᵖ) (C.map opEquiv.toEmbedding)
      (B.map opEquiv.toEmbedding) (A.map opEquiv.toEmbedding)

Premises used: Finset.map_op_inv, MulOpposite.opEquiv, Finset.map, div_eq_mul_inv, Finset.map_op_mul, Equiv.toEmbedding, mul_comm, Finset.ruzsa_triangle_inequality_div_div_div
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B C : Finset G
⊢ #(A / C) * #B ≤ #(A * B) * #(C * B)

Tactic:
simpa using ruzsa_triangle_inequality_div_div_div A B⁻¹ C

Premises used: Inv.inv, Finset.ruzsa_triangle_inequality_div_div_div
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B C : Finset G
⊢ #(A * C⁻¹) * #B ≤ #(A * B) * #(C * B)

Tactic:
simpa using ruzsa_triangle_inequality_mulInv_mulInv_mulInv A B⁻¹ C

Premises used: Inv.inv, Finset.ruzsa_triangle_inequality_mulInv_mulInv_mulInv
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B C : Finset G
⊢ #B * #(A⁻¹ * C) ≤ #(B * A) * #(B * C)

Tactic:
simpa using ruzsa_triangle_inequality_invMul_invMul_invMul A B⁻¹ C

Premises used: Finset.ruzsa_triangle_inequality_invMul_invMul_invMul, Inv.inv
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B C : Finset G
⊢ #B * #(A * C) ≤ #(B / A) * #(B * C)

Tactic:
simpa [div_eq_mul_inv] using ruzsa_triangle_inequality_invMul_mul_mul A⁻¹ B C

Premises used: Finset.ruzsa_triangle_inequality_invMul_mul_mul, div_eq_mul_inv, Inv.inv
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B C : Finset G
⊢ #B * #(A * C) ≤ #(B * A⁻¹) * #(B * C)

Tactic:
simpa [div_eq_mul_inv] using ruzsa_triangle_inequality_mul_div_mul A B C

Premises used: Finset.ruzsa_triangle_inequality_mul_div_mul, div_eq_mul_inv
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B C : Finset G
⊢ #(A * C) * #B ≤ #(A * B) * #(C⁻¹ * B)

Tactic:
simpa using ruzsa_triangle_inequality_mulInv_mul_mul A B C⁻¹

Premises used: Finset.ruzsa_triangle_inequality_mulInv_mul_mul, Inv.inv
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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
⊢ #(∅ * A * B) * #A ≤ #(A * B) * #(∅ * A)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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)
⊢ let A' := A ∩ ({x}⁻¹ * C * A);
  A' = A ∩ ({x}⁻¹ * C * A)

Tactic:
set A' := A ∩ ({x}⁻¹ * C * A) with hA'

Premises used: HMul.hMul, Inv.inv
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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 :
  let C' := Insert.insert x C;
  ∀ (hC' : C' = Insert.insert x C), #(C' * A * B) * #A ≤ #(A * B) * #(C' * A)
⊢ #(Insert.insert x C * A * B) * #A ≤ #(A * B) * #(Insert.insert x C * A)

Tactic:
set C' := insert x C with hC'

Premises used: Insert.insert
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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)
rw₃ rw₄ : {x} * A ∩ (C * A) = {x} * A ∩ (C * A)
⊢ {x} * A' = {x} * A ∩ (C * A)

Tactic:
rw [hA', mul_assoc, singleton_mul_inter, (isUnit_singleton x).mul_inv_cancel_left]

Premises used: mul_assoc, Finset.singleton_mul_inter, Finset.isUnit_singleton, IsUnit.mul_inv_cancel_left
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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
⊢ {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]
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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)
rw : C * A * B ∪ {x} * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
⊢ C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)

Tactic:
rw [hC', insert_eq, union_comm, union_mul, union_mul]

Premises used: Finset.union_mul, Finset.insert_eq, Finset.union_comm
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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)

Tactic:
(sup_sdiff_eq_sup ?_).symm

Premises used: sup_sdiff_eq_sup, Eq.symm
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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)
refine : {x} * A' * B ≤ C * A * B
⊢ C * A * B ∪ {x} * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)

Tactic:
refine (sup_sdiff_eq_sup ?_).symm

Premises used: sup_sdiff_eq_sup, Eq.symm
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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)
rw : {x} * A ∩ (C * A) * B ≤ C * A * B
⊢ {x} * A' * B ≤ C * A * B

Tactic:
rw [h₀]
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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)
bc : {x} * A ∩ (C * A) ≤ C * A
⊢ {x} * A ∩ (C * A) * B ≤ C * A * B

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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) ≤ C * A

Tactic:
inter_subset_right

Premises used: Finset.inter_subset_right
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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) ≤ C * A

Tactic:
exact inter_subset_right

Premises used: Finset.inter_subset_right
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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)

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
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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)
a : A' ⊆ A
⊢ {x} * A' * B ⊆ {x} * A * B

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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)
⊢ A' ⊆ A

Tactic:
inter_subset_left

Premises used: Set.Mem, setOf, Finset.inter_subset_left
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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)
⊢ A' ⊆ A

Tactic:
exact inter_subset_left

Premises used: Finset.inter_subset_left
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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

Tactic:
have h₂ : {x} * A' * B ⊆ {x} * A * B := by gcongr; exact inter_subset_left
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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) ≤ #(C * A * B) + #(A * B) - #(A' * B)
⊢ #(C' * A * B) * #A ≤ (#(C * A * B) + #(A * B) - #(A' * B)) * #A

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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) ≤ #(C * A * B) + #(A * B) - #(A' * B)

Tactic:
rw [h₁]