awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.SubsetSum
Goal:
M : Type u_1
inst : DecidableEq M
inst_1 : AddCommMonoid M
A : Finset M
a : M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
hA : ∀ x ∈ A, 0 < x
hAa : ∀ x ∈ A, x < a
ha : 0 < a
disjoint : Disjoint (insert 0 A) (a +ᵥ A.subsetSum)
insert_subset : insert 0 A ⊆ (insert a A).subsetSum
vadd_subset : a +ᵥ A.subsetSum ⊆ (insert a A).subsetSum
grw grw₁ : #(insert a A).subsetSum ≤ #(insert a A).subsetSum
⊢ #(insert 0 A ∪ (a +ᵥ A.subsetSum)) ≤ #(insert a A).subsetSum

Tactic:
grw [union_subset insert_subset vadd_subset]

Premises used: Finset.union_subset
-- Module: Mathlib.Combinatorics.Additive.SubsetSum
Goal:
M : Type u_1
inst : DecidableEq M
inst_1 : AddCommMonoid M
A : Finset M
a : M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
hA : ∀ x ∈ A, 0 < x
hAa : ∀ x ∈ A, x < a
ha : 0 < a
disjoint : Disjoint (insert 0 A) (a +ᵥ A.subsetSum)
insert_subset : insert 0 A ⊆ (insert a A).subsetSum
vadd_subset : a +ᵥ A.subsetSum ⊆ (insert a A).subsetSum
calc : #A + #A.subsetSum < #A + 1 + #A.subsetSum
calc₁ : #A + 1 + #A.subsetSum = #(insert 0 A) + #A.subsetSum
calc₂ : #(insert 0 A) + #A.subsetSum = #(insert 0 A) + #(a +ᵥ A.subsetSum)
calc₃ : #(insert 0 A) + #(a +ᵥ A.subsetSum) = #(insert 0 A ∪ (a +ᵥ A.subsetSum))
calc₄ : #(insert 0 A ∪ (a +ᵥ A.subsetSum)) ≤ #(insert a A).subsetSum
⊢ #A + #A.subsetSum < #(insert a A).subsetSum

Tactic:
calc #A + #A.subsetSum
    _ < #A + 1 + #A.subsetSum := by gcongr; exact Nat.lt_add_one _
    _ = #(insert 0 A) + #A.subsetSum := by rw [card_insert_of_notMem fun h => (hA 0 h).false]
    _ = #(insert 0 A) + #(a +ᵥ A.subsetSum) := by simp [vadd_finset_def, card_image_of_injOn]
    _ = #((insert 0 A) ∪ (a +ᵥ A.subsetSum)) := by rw [card_union_of_disjoint disjoint]
    _ ≤ #(insert a A).subsetSum := by grw [union_subset insert_subset vadd_subset]

Premises used: Finset.subsetSum, Insert.insert, HVAdd.hVAdd, Union.union, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Additive.SubsetSum
Goal:
M : Type u_1
inst : DecidableEq M
inst_1 : AddCommMonoid M
A : Finset M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
A_pos : ∀ (x : M), Membership.mem (γ := Finset M) ∅ x → 0 < x
⊢ (card.{u_1} (α := M) ∅ + 1).choose 2 < card.{u_1} (α := M) (subsetSum ∅)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.SubsetSum
Goal:
M : Type u_1
inst : DecidableEq M
inst_1 : AddCommMonoid M
A_1 : Finset M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
a : M
A : Finset M
A_lt_a : ∀ x ∈ A, x < a
ih : ∀ (A_pos : ∀ x ∈ A, 0 < x), (#A + 1).choose 2 < #A.subsetSum
A_pos : ∀ x ∈ insert a A, 0 < x
⊢ ∀ x ∈ A, 0 < x

Tactic:
have A_pos' : ∀ x ∈ A, 0 < x := fun x hx => A_pos x (mem_insert_of_mem hx)
-- Module: Mathlib.Combinatorics.Additive.SubsetSum
Goal:
M : Type u_1
inst : DecidableEq M
inst_1 : AddCommMonoid M
A_1 : Finset M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
a : M
A : Finset M
A_lt_a : ∀ x ∈ A, x < a
ih : ∀ (A_pos : ∀ x ∈ A, 0 < x), (#A + 1).choose 2 < #A.subsetSum
A_pos : ∀ x ∈ insert a A, 0 < x
A_pos' : ∀ x ∈ A, 0 < x
⊢ LT.lt (α := ℕ) 0 2

Tactic:
lia
-- Module: Mathlib.Combinatorics.Additive.SubsetSum
Goal:
M : Type u_1
inst : DecidableEq M
inst_1 : AddCommMonoid M
A_1 : Finset M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
a : M
A : Finset M
A_lt_a : ∀ x ∈ A, x < a
ih : ∀ (A_pos : ∀ x ∈ A, 0 < x), (#A + 1).choose 2 < #A.subsetSum
A_pos : ∀ x ∈ Insert.insert a A, 0 < x
A_pos' : ∀ x ∈ A, 0 < x
insert : #A + #A.subsetSum < #(Insert.insert a A).subsetSum
⊢ (#(Insert.insert a A) + 1).choose 2 < #(Insert.insert a A).subsetSum

Tactic:
grw [card_insert_of_notMem fun ha => (A_lt_a a ha).false, Nat.choose_succ_left _ _ (by lia),
      Nat.choose_one_right, add_right_comm, add_assoc, Nat.add_one_le_iff.2 (ih A_pos')]

Premises used: Iff.mpr, add_assoc, Nat.choose_succ_left, add_right_comm, Finset.card_insert_of_notMem, Nat.choose_one_right, Nat.add_one_le_iff, LT.lt.false
-- Module: Mathlib.Combinatorics.Additive.SubsetSum
Goal:
M : Type u_1
inst : DecidableEq M
inst_1 : AddCommMonoid M
A_1 : Finset M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
a : M
A : Finset M
A_lt_a : ∀ x ∈ A, x < a
ih : ∀ (A_pos : ∀ x ∈ A, 0 < x), (#A + 1).choose 2 < #A.subsetSum
A_pos : ∀ x ∈ insert a A, 0 < x
A_pos' : ∀ x ∈ A, 0 < x
⊢ #A + #A.subsetSum < #(insert a A).subsetSum

Tactic:
card_add_card_subsetSum_lt_card_subsetSum_insert_max A_pos' A_lt_a <| A_pos a <|
      mem_insert_self a A

Premises used: Finset.mem_insert_self, Finset.card_add_card_subsetSum_lt_card_subsetSum_insert_max
-- Module: Mathlib.Combinatorics.Additive.SubsetSum
Goal:
M : Type u_1
inst : DecidableEq M
inst_1 : AddCommMonoid M
A_1 : Finset M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
a : M
A : Finset M
A_lt_a : ∀ x ∈ A, x < a
ih : ∀ (A_pos : ∀ x ∈ A, 0 < x), (#A + 1).choose 2 < #A.subsetSum
A_pos : ∀ x ∈ insert a A, 0 < x
A_pos' : ∀ x ∈ A, 0 < x
⊢ #A + #A.subsetSum < #(insert a A).subsetSum

Tactic:
exact card_add_card_subsetSum_lt_card_subsetSum_insert_max A_pos' A_lt_a <| A_pos a <|
      mem_insert_self a A

Premises used: Finset.mem_insert_self, Finset.card_add_card_subsetSum_lt_card_subsetSum_insert_max
-- Module: Mathlib.Combinatorics.Additive.SubsetSum
Goal:
M : Type u_1
inst : DecidableEq M
inst_1 : AddCommMonoid M
A : Finset M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
A_pos : ∀ x ∈ A, 0 < x
empty :
  ∀ (A_pos : ∀ (x : M), Membership.mem (γ := Finset M) ∅ x → 0 < x),
    (card.{u_1} (α := M) ∅ + 1).choose 2 < card.{u_1} (α := M) (subsetSum ∅)
insert :
  ∀ (a : M) (A : Finset M) (A_lt_a : ∀ x ∈ A, x < a) (ih : ∀ (A_pos : ∀ x ∈ A, 0 < x), (#A + 1).choose 2 < #A.subsetSum)
    (A_pos : ∀ x ∈ Insert.insert a A, 0 < x), (#(Insert.insert a A) + 1).choose 2 < #(Insert.insert a A).subsetSum
⊢ (#A + 1).choose 2 < #A.subsetSum

Tactic:
induction A using induction_on_max with
  | empty => simp
  | insert a A A_lt_a ih =>
    have A_pos' : ∀ x ∈ A, 0 < x := fun x hx => A_pos x (mem_insert_of_mem hx)
    grw [card_insert_of_notMem fun ha => (A_lt_a a ha).false, Nat.choose_succ_left _ _ (by lia),
      Nat.choose_one_right, add_right_comm, add_assoc, Nat.add_one_le_iff.2 (ih A_pos')]
    exact card_add_card_subsetSum_lt_card_subsetSum_insert_max A_pos' A_lt_a <| A_pos a <|
      mem_insert_self a A

Premises used: add_assoc, Nat.choose_succ_left, Insert.insert, add_right_comm, Nat.choose_one_right
-- Module: Mathlib.Combinatorics.Additive.SubsetSum
Goal:
M : Type u_1
inst : DecidableEq M
inst_1 : AddCommMonoid M
A : Finset M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
A_pos : ∀ x ∈ A, 0 ≤ x
grw : (#(A.erase 0) + 1).choose 2 ≤ (#(A.erase 0) + 1).choose 2
grw₁ : M
grw₂ : (#(A.erase 0) + 1).choose 2 ≤ (#(A.erase 0) + 1).choose 2
grw₃ : M
⊢ (#A).choose 2 ≤ (#(A.erase 0) + 1).choose 2

Tactic:
grw [tsub_le_iff_right.1 <| pred_card_le_card_erase]

Premises used: tsub_le_iff_right, Finset.pred_card_le_card_erase, Iff.mp
-- Module: Mathlib.Combinatorics.Additive.SubsetSum
Goal:
M : Type u_1
inst : DecidableEq M
inst_1 : AddCommMonoid M
A : Finset M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
A_pos : ∀ x ∈ A, 0 ≤ x
⊢ (#(A.erase 0) + 1).choose 2 < #(A.erase 0).subsetSum

Tactic:
card_succ_choose_two_lt_card_subsetSum_of_pos fun x hx =>
          (A_pos x (mem_of_mem_erase hx)).lt_of_ne (ne_of_mem_erase hx).symm

Premises used: Finset.ne_of_mem_erase, Finset.card_succ_choose_two_lt_card_subsetSum_of_pos, Ne.symm, LE.le.lt_of_ne, Finset.mem_of_mem_erase
-- Module: Mathlib.Combinatorics.Additive.SubsetSum
Goal:
M : Type u_1
inst : DecidableEq M
inst_1 : AddCommMonoid M
A : Finset M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
A_pos : ∀ x ∈ A, 0 ≤ x
rw rw₁ : #A.subsetSum = #A.subsetSum
⊢ #(A.erase 0).subsetSum = #A.subsetSum

Tactic:
rw [subsetSum_erase_zero]

Premises used: Finset.subsetSum_erase_zero
-- Module: Mathlib.Combinatorics.Additive.SubsetSum
Goal:
M : Type u_1
inst : DecidableEq M
inst_1 : AddCommMonoid M
A : Finset M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
A_pos : ∀ x ∈ A, 0 ≤ x
calc : (#A).choose 2 ≤ (#(A.erase 0) + 1).choose 2
calc₁ : #(A.erase 0).subsetSum = #A.subsetSum
⊢ (#A).choose 2 < #A.subsetSum

Tactic:
calc (#A).choose 2
    _ ≤ (#(A.erase 0) + 1).choose 2 := by grw [tsub_le_iff_right.1 <| pred_card_le_card_erase]
    _ < #(A.erase 0).subsetSum :=
        card_succ_choose_two_lt_card_subsetSum_of_pos fun x hx =>
          (A_pos x (mem_of_mem_erase hx)).lt_of_ne (ne_of_mem_erase hx).symm
    _ = #A.subsetSum := by rw [subsetSum_erase_zero]

Premises used: Nat.choose, Finset.subsetSum, Finset.ne_of_mem_erase, Finset.card_succ_choose_two_lt_card_subsetSum_of_pos, Ne.symm, LE.le.lt_of_ne, HAdd.hAdd, Finset.mem_of_mem_erase, Finset.card, OfNat.ofNat, Finset.erase
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
a_1 : G
hA : #(A * A) ≤ #A
ha_1 : a_1 ∈ A
a : G
ha : a ∈ A
⊢ #(A * A) ≤ #(a •> A)

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
a : G
hA : #(A * A) ≤ #A
ha : a ∈ A
⊢ ∀ {a : G} (ha : a ∈ A), a •> A = A * A

Tactic:
have smul_A {a} (ha : a ∈ A) : a •> A = A * A :=
    eq_of_subset_of_card_le (smul_finset_subset_mul ha) (by simpa)
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
a_1 : G
hA : #(A * A) ≤ #A
ha_1 : a_1 ∈ A
smul_A : ∀ {a : G} (ha : a ∈ A), a •> A = A * A
a : G
ha : a ∈ A
⊢ #(A * A) ≤ #(A <• a)

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
a : G
hA : #(A * A) ≤ #A
ha : a ∈ A
smul_A : ∀ {a : G} (ha : a ∈ A), a •> A = A * A
⊢ ∀ {a : G} (ha : a ∈ A), A <• a = A * A

Tactic:
have A_smul {a} (ha : a ∈ A) : A <• a = A * A :=
    eq_of_subset_of_card_le (op_smul_finset_subset_mul ha) (by simpa)
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
a_1 : G
hA : #(A * A) ≤ #A
ha_1 : a_1 ∈ A
smul_A : ∀ {a : G} (ha : a ∈ A), a •> A = A * A
A_smul : ∀ {a : G} (ha : a ∈ A), A <• a = A * A
a : G
ha : a ∈ A
rw : A * A = A <• a
rw₁ rw₂ : A * A = A * A
⊢ a •> A = A <• a

Tactic:
rw [smul_A ha, A_smul ha]
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
a : G
hA : #(A * A) ≤ #A
ha : a ∈ A
smul_A : ∀ {a : G} (ha : a ∈ A), a •> A = A * A
A_smul : ∀ {a : G} (ha : a ∈ A), A <• a = A * A
⊢ ∀ {a : G} (ha : a ∈ A), a •> A = A <• a

Tactic:
have smul_A_eq_A_smul {a} (ha : a ∈ A) : a •> A = A <• a := by rw [smul_A ha, A_smul ha]
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
a_1 : G
hA : #(A * A) ≤ #A
ha_1 : a_1 ∈ A
smul_A : ∀ {a : G} (ha : a ∈ A), a •> A = A * A
A_smul : ∀ {a : G} (ha : a ∈ A), A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G} (ha : a ∈ A), a •> A = A <• a
x a : G
ha : a ∈ A
rw : a •> (x * a) ∈ a •> A ↔ a * x ∈ A
rw₁ : a •> (x * a) ∈ A <• a ↔ a * x ∈ A
rw₂ : a •> (x <• a) ∈ A <• a ↔ a * x ∈ A
rw₃ : a •> x <• a ∈ A <• a ↔ a * x ∈ A
rw₄ : a •> x ∈ A ↔ a * x ∈ A
rw₅ rw₆ : a * x ∈ A ↔ a * x ∈ A
⊢ x * a ∈ A ↔ a * x ∈ A

Tactic:
rw [← smul_mem_smul_finset_iff a, smul_A_eq_A_smul ha, ← op_smul_eq_mul, smul_comm,
      smul_mem_smul_finset_iff, smul_eq_mul]

Premises used: Finset.smul_mem_smul_finset_iff, op_smul_eq_mul, smul_eq_mul, SMulCommClass.smul_comm
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
a : G
hA : #(A * A) ≤ #A
ha : a ∈ A
smul_A : ∀ {a : G} (ha : a ∈ A), a •> A = A * A
A_smul : ∀ {a : G} (ha : a ∈ A), A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G} (ha : a ∈ A), a •> A = A <• a
⊢ ∀ {x a : G} (ha : a ∈ A), x * a ∈ A ↔ a * x ∈ A

Tactic:
have mul_mem_A_comm {x a} (ha : a ∈ A) : x * a ∈ A ↔ a * x ∈ A := by
    rw [← smul_mem_smul_finset_iff a, smul_A_eq_A_smul ha, ← op_smul_eq_mul, smul_comm,
      smul_mem_smul_finset_iff, smul_eq_mul]
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
a_1 : G
hA : #(A * A) ≤ #A
ha_1 : a_1 ∈ A
smul_A : ∀ {a : G} (ha : a ∈ A), a •> A = A * A
A_smul : ∀ {a : G} (ha : a ∈ A), A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G} (ha : a ∈ A), a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G} (ha : a ∈ A), x * a ∈ A ↔ a * x ∈ A
H : Subgroup G := stabilizer G A
a : G
ha : a ∈ A
h : ∀ (x : G), x ∈ a⁻¹ •> (↑A : Set G) ↔ x ∈ (↑H : Set G)
⊢ a⁻¹ •> (↑A : Set G) = (↑H : Set G)

Tactic:
ext x
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
a_1 : G
hA : #(A * A) ≤ #A
ha_1 : a_1 ∈ A
smul_A : ∀ {a : G} (ha : a ∈ A), a •> A = A * A
A_smul : ∀ {a : G} (ha : a ∈ A), A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G} (ha : a ∈ A), a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G} (ha : a ∈ A), x * a ∈ A ↔ a * x ∈ A
H : Subgroup G := stabilizer G A
a : G
ha : a ∈ A
x : G
h : a * x ∈ (↑A : Set G) ↔ x ∈ (↑H : Set G)
⊢ x ∈ a⁻¹ •> (↑A : Set G) ↔ x ∈ (↑H : Set G)

Tactic:
rw [Set.mem_inv_smul_set_iff, smul_eq_mul]

Premises used: Set.mem_inv_smul_set_iff, smul_eq_mul
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
a_1 : G
hA : #(A * A) ≤ #A
ha_1 : a_1 ∈ A
smul_A : ∀ {a : G} (ha : a ∈ A), a •> A = A * A
A_smul : ∀ {a : G} (ha : a ∈ A), A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G} (ha : a ∈ A), a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G} (ha : a ∈ A), x * a ∈ A ↔ a * x ∈ A
H : Subgroup G := stabilizer G A
a : G
ha : a ∈ A
x : G
⊢ a * x ∈ (↑A : Set G) ↔ x ∈ (↑H : Set G)

Tactic:
⟨fun hx ↦ ?_, fun hx ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
a_1 : G
hA : #(A * A) ≤ #A
ha_1 : a_1 ∈ A
smul_A : ∀ {a : G} (ha : a ∈ A), a •> A = A * A
A_smul : ∀ {a : G} (ha : a ∈ A), A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G} (ha : a ∈ A), a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G} (ha : a ∈ A), x * a ∈ A ↔ a * x ∈ A
H : Subgroup G := stabilizer G A
a : G
ha : a ∈ A
x : G
h : ∀ (hx : a * x ∈ (↑A : Set G)), x ∈ (↑H : Set G)
h₁ : ∀ (hx : x ∈ (↑H : Set G)), a * x ∈ (↑A : Set G)
⊢ a * x ∈ (↑A : Set G) ↔ x ∈ (↑H : Set G)

Tactic:
refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
a_1 : G
hA : #(A * A) ≤ #A
ha_1 : a_1 ∈ A
smul_A : ∀ {a : G} (ha : a ∈ A), a •> A = A * A
A_smul : ∀ {a : G} (ha : a ∈ A), A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G} (ha : a ∈ A), a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G} (ha : a ∈ A), x * a ∈ A ↔ a * x ∈ A
H : Subgroup G := stabilizer G A
a : G
ha : a ∈ A
x : G
hx : a * x ∈ (↑A : Set G)
⊢ x ∈ (↑H : Set G)

Tactic:
simpa [← smul_A ha, mul_smul] using smul_A hx

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
a_1 : G
hA : #(A * A) ≤ #A
ha_1 : a_1 ∈ A
smul_A : ∀ {a : G} (ha : a ∈ A), a •> A = A * A
A_smul : ∀ {a : G} (ha : a ∈ A), A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G} (ha : a ∈ A), a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G} (ha : a ∈ A), x * a ∈ A ↔ a * x ∈ A
H : Subgroup G := stabilizer G A
a : G
ha : a ∈ A
x : G
hx : x ∈ (↑H : Set G)
h : x * a ∈ A
h₁ : x •> a ∈ A
h₂ : a ∈ x⁻¹ •> A
h₃ h₄ h₅ h₆ : a ∈ A
⊢ a * x ∈ A

Tactic:
rwa [← mul_mem_A_comm ha, ← smul_eq_mul, ← mem_inv_smul_finset_iff, inv_mem hx]

Premises used: Finset.mem_inv_smul_finset_iff, InvMemClass.inv_mem, smul_eq_mul
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
a : G
hA : #(A * A) ≤ #A
ha : a ∈ A
smul_A : ∀ {a : G} (ha : a ∈ A), a •> A = A * A
A_smul : ∀ {a : G} (ha : a ∈ A), A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G} (ha : a ∈ A), a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G} (ha : a ∈ A), x * a ∈ A ↔ a * x ∈ A
H : Subgroup G := stabilizer G A
⊢ ∀ {a : G} (ha : a ∈ A), a⁻¹ •> (↑A : Set G) = (↑H : Set G)

Tactic:
have inv_smul_A {a} (ha : a ∈ A) : a⁻¹ • (A : Set G) = H := by
    ext x
    rw [Set.mem_inv_smul_set_iff, smul_eq_mul]
    refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
    · simpa [← smul_A ha, mul_smul] using smul_A hx
    · norm_cast
      rwa [← mul_mem_A_comm ha, ← smul_eq_mul, ← mem_inv_smul_finset_iff, inv_mem hx]
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
a : G
hA : #(A * A) ≤ #A
ha : a ∈ A
smul_A : ∀ {a : G} (ha : a ∈ A), a •> A = A * A
A_smul : ∀ {a : G} (ha : a ∈ A), A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G} (ha : a ∈ A), a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G} (ha : a ∈ A), x * a ∈ A ↔ a * x ∈ A
H : Subgroup G := stabilizer G A
inv_smul_A : ∀ {a : G} (ha : a ∈ A), a⁻¹ •> (↑A : Set G) = (↑H : Set G)
⊢ a •> (↑(stabilizer G A) : Set G) = (↑A : Set G) ∧ (↑(stabilizer G A) : Set G) <• a = (↑A : Set G)

Tactic:
⟨?_, ?_⟩

Premises used: And.intro
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
a : G
hA : #(A * A) ≤ #A
ha : a ∈ A
smul_A : ∀ {a : G} (ha : a ∈ A), a •> A = A * A
A_smul : ∀ {a : G} (ha : a ∈ A), A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G} (ha : a ∈ A), a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G} (ha : a ∈ A), x * a ∈ A ↔ a * x ∈ A
H : Subgroup G := stabilizer G A
inv_smul_A : ∀ {a : G} (ha : a ∈ A), a⁻¹ •> (↑A : Set G) = (↑H : Set G)
refine_1 : a •> (↑(stabilizer G A) : Set G) = (↑A : Set G)
refine_2 : (↑(stabilizer G A) : Set G) <• a = (↑A : Set G)
⊢ a •> (↑(stabilizer G A) : Set G) = (↑A : Set G) ∧ (↑(stabilizer G A) : Set G) <• a = (↑A : Set G)

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
a : G
hA : #(A * A) ≤ #A
ha : a ∈ A
smul_A : ∀ {a : G} (ha : a ∈ A), a •> A = A * A
A_smul : ∀ {a : G} (ha : a ∈ A), A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G} (ha : a ∈ A), a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G} (ha : a ∈ A), x * a ∈ A ↔ a * x ∈ A
H : Subgroup G := stabilizer G A
inv_smul_A : ∀ {a : G} (ha : a ∈ A), a⁻¹ •> (↑A : Set G) = (↑H : Set G)
refine_1 : a •> a⁻¹ •> (↑A : Set G) = (↑A : Set G)
refine_1₁ refine_1₂ : (↑A : Set G) = (↑A : Set G)
⊢ a •> (↑(stabilizer G A) : Set G) = (↑A : Set G)

Tactic:
rw [← inv_smul_A ha, smul_inv_smul]

Premises used: smul_inv_smul
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
a : G
hA : #(A * A) ≤ #A
ha : a ∈ A
smul_A : ∀ {a : G} (ha : a ∈ A), a •> A = A * A
A_smul : ∀ {a : G} (ha : a ∈ A), A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G} (ha : a ∈ A), a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G} (ha : a ∈ A), x * a ∈ A ↔ a * x ∈ A
H : Subgroup G := stabilizer G A
inv_smul_A : ∀ {a : G} (ha : a ∈ A), a⁻¹ •> (↑A : Set G) = (↑H : Set G)
refine_2 : a⁻¹ •> ((↑A : Set G) <• a) = (↑A : Set G)
⊢ (↑(stabilizer G A) : Set G) <• a = (↑A : Set G)

Tactic:
rw [← inv_smul_A ha, smul_comm]

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
a : G
hA : #(A * A) ≤ #A
ha : a ∈ A
smul_A : ∀ {a : G} (ha : a ∈ A), a •> A = A * A
A_smul : ∀ {a : G} (ha : a ∈ A), A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G} (ha : a ∈ A), a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G} (ha : a ∈ A), x * a ∈ A ↔ a * x ∈ A
H : Subgroup G := stabilizer G A
inv_smul_A : ∀ {a : G} (ha : a ∈ A), a⁻¹ •> (↑A : Set G) = (↑H : Set G)
refine_2 : a⁻¹ •> (A <• a) = A
⊢ a⁻¹ •> ((↑A : Set G) <• a) = (↑A : Set G)

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
a : G
hA : #(A * A) ≤ #A
ha : a ∈ A
smul_A : ∀ {a : G} (ha : a ∈ A), a •> A = A * A
A_smul : ∀ {a : G} (ha : a ∈ A), A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G} (ha : a ∈ A), a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G} (ha : a ∈ A), x * a ∈ A ↔ a * x ∈ A
H : Subgroup G := stabilizer G A
inv_smul_A : ∀ {a : G} (ha : a ∈ A), a⁻¹ •> (↑A : Set G) = (↑H : Set G)
refine_2 : a⁻¹ •> a •> A = A
refine_2₁ refine_2₂ : A = A
⊢ a⁻¹ •> (A <• a) = A

Tactic:
rw [← smul_A_eq_A_smul ha, inv_smul_smul]

Premises used: inv_smul_smul
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
a : G
hA : #(A * A) ≤ #A
ha : a ∈ A
⊢ a •> (↑(stabilizer G A) : Set G) = (↑A : Set G)

Tactic:
(smul_stabilizer_of_no_doubling_aux hA ha).1

Premises used: _private.0.Finset.smul_stabilizer_of_no_doubling_aux, And.left
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
a : G
hA : #(A * A) ≤ #A
ha : a ∈ A
⊢ (↑(stabilizer G A) : Set G) <• a = (↑A : Set G)

Tactic:
(smul_stabilizer_of_no_doubling_aux hA ha).2

Premises used: _private.0.Finset.smul_stabilizer_of_no_doubling_aux, And.right
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
a b : G
ha : a ∈ B
hb : b ∈ B
a₁ : a •> A ∪ b •> A ⊆ B * A
⊢ #(a •> A ∪ b •> A) ≤ #(B * A)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
a b : G
ha : a ∈ B
hb : b ∈ B
a₁ : a •> A ⊆ B * A ∧ b •> A ⊆ B * A
⊢ a •> A ∪ b •> A ⊆ B * A

Tactic:
rw [union_subset_iff]

Premises used: Finset.union_subset_iff
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
a b : G
ha : a ∈ B
hb : b ∈ B
⊢ a •> A ⊆ B * A ∧ b •> A ⊆ B * A

Tactic:
⟨smul_finset_subset_mul ha, smul_finset_subset_mul hb⟩

Premises used: And.intro, Finset.smul_finset_subset_mul
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
a b : G
ha : a ∈ B
hb : b ∈ B
⊢ a •> A ⊆ B * A ∧ b •> A ⊆ B * A

Tactic:
exact ⟨smul_finset_subset_mul ha, smul_finset_subset_mul hb⟩
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
a b : G
ha : a ∈ B
hb : b ∈ B
⊢ #(a •> A ∪ b •> A) ≤ #(B * A)

Tactic:
have : #((a • A) ∪ (b • A)) ≤ #(B * A) := by
    gcongr
    rw [union_subset_iff]
    exact ⟨smul_finset_subset_mul ha, smul_finset_subset_mul hb⟩
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
a b : G
ha : a ∈ B
hb : b ∈ B
this : #(a •> A ∪ b •> A) ≤ #(B * A)
grw : 2 * #A ≤ #(a •> A) + #(b •> A)
⊢ 2 * #A ≤ #(a •> A ∩ b •> A) + #(B * A)

Tactic:
grw [← this, card_inter_add_card_union]

Premises used: Finset.card_inter_add_card_union
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
a b : G
ha : a ∈ B
hb : b ∈ B
this : #(a •> A ∪ b •> A) ≤ #(B * A)
⊢ 2 * #A ≤ #(a •> A) + #(b •> A)

Tactic:
simp [card_smul_finset, two_mul]

Premises used: two_mul, Finset.card_smul_finset
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A B : Finset G
a b : G
hA : (↑(#(B * A)) : ℝ) ≤ K * (↑(#A) : ℝ)
ha : a ∈ B
hb : b ∈ B
⊢ HMul.hMul (α := ℝ) 2 (↑(#A) : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑(#(a •> A ∩ b •> A)) : ℝ) (↑(#(B * A)) : ℝ)

Tactic:
have : 2 * (#A : ℝ) ≤ #(a •> A ∩ b •> A) + #(B * A) := mod_cast big_intersection ha hb