awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SubsetSum (goal)
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 ∅)
⊢ (#A + 1).choose 2 < #A.subsetSum
have 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 a A, 0 < x), (#(insert a A) + 1).choose 2 < #(insert a 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
Cleared hypotheses: A_pos
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SubsetSum (goal)
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).choose 2 ≤ (#(A.erase 0) + 1).choose 2
have grw : (#(A.erase 0) + 1).choose 2 ≤ (#(A.erase 0) + 1).choose 2
Tactic: grw [tsub_le_iff_right.1 <| pred_card_le_card_erase]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SubsetSum (goal)
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
⊢ (#A).choose 2 ≤ (#(A.erase 0) + 1).choose 2
have grw₁ : M
Tactic: grw [tsub_le_iff_right.1 <| pred_card_le_card_erase]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SubsetSum (goal)
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).subsetSum = #A.subsetSum
have rw : #A.subsetSum = #A.subsetSum
Tactic: rw [subsetSum_erase_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SubsetSum (goal)
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).choose 2 < #A.subsetSum
have calc : (#A).choose 2 ≤ (#(A.erase 0) + 1).choose 2
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SubsetSum (goal)
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
⊢ (#A).choose 2 < #A.subsetSum
have calc₁ : #(A.erase 0).subsetSum = #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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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) ∧ (↑(stabilizer G A) : Set G) <• a = (↑A : Set G)
have smul_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)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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 •> (↑(stabilizer G A) : Set G) = (↑A : Set G) ∧ (↑(stabilizer G A) : Set G) <• a = (↑A : Set G)
have A_smul : ∀ {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)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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
⊢ a •> A = A <• a
have rw : A * A = A <• a
Tactic: rw [smul_A ha, A_smul ha]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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
⊢ a •> A = A <• a
have rw₁ : A * A = A * A
Tactic: rw [smul_A ha, A_smul ha]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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 •> (↑(stabilizer G A) : Set G) = (↑A : Set G) ∧ (↑(stabilizer G A) : Set G) <• a = (↑A : Set G)
have smul_A_eq_A_smul : ∀ {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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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
⊢ x * a ∈ A ↔ a * x ∈ A
have rw : a •> (x * a) ∈ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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
⊢ x * a ∈ A ↔ a * x ∈ A
have rw₁ : a •> (x * a) ∈ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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
⊢ x * a ∈ A ↔ a * x ∈ A
have rw₂ : a •> (x <• a) ∈ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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
⊢ x * a ∈ A ↔ a * x ∈ A
have rw₃ : a •> x <• a ∈ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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
⊢ x * a ∈ A ↔ a * x ∈ A
have rw₄ : a •> x ∈ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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
⊢ x * a ∈ A ↔ a * x ∈ A
have rw₅ : a * x ∈ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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
⊢ a •> (↑(stabilizer G A) : Set G) = (↑A : Set G) ∧ (↑(stabilizer G A) : Set G) <• a = (↑A : Set G)
have mul_mem_A_comm : ∀ {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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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
⊢ a⁻¹ •> (↑A : Set G) = (↑H : Set G)
have h : ∀ (x : G), x ∈ a⁻¹ •> (↑A : Set G) ↔ x ∈ (↑H : Set G)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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
⊢ x ∈ a⁻¹ •> (↑A : Set G) ↔ x ∈ (↑H : Set G)
have h : a * x ∈ (↑A : Set G) ↔ x ∈ (↑H : Set G)
Tactic: rw [Set.mem_inv_smul_set_iff, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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)
have h : ∀ (hx : a * x ∈ (↑A : Set G)), x ∈ (↑H : Set G)
Tactic: refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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)
⊢ a * x ∈ (↑A : Set G) ↔ x ∈ (↑H : Set G)
have h₁ : ∀ (hx : x ∈ (↑H : Set G)), a * x ∈ (↑A : Set G)
Tactic: refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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)
⊢ a * x ∈ A
have h : x * a ∈ A
Tactic: rwa [← mul_mem_A_comm ha, ← smul_eq_mul, ← mem_inv_smul_finset_iff, inv_mem hx]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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
⊢ a * x ∈ A
have h₁ : x •> a ∈ A
Tactic: rwa [← mul_mem_A_comm ha, ← smul_eq_mul, ← mem_inv_smul_finset_iff, inv_mem hx]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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
⊢ a * x ∈ A
have h₂ : a ∈ x⁻¹ •> A
Tactic: rwa [← mul_mem_A_comm ha, ← smul_eq_mul, ← mem_inv_smul_finset_iff, inv_mem hx]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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 •> (↑(stabilizer G A) : Set G) = (↑A : Set G) ∧ (↑(stabilizer G A) : Set G) <• a = (↑A : Set G)
have inv_smul_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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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)
have refine_1 : a •> (↑(stabilizer G A) : Set G) = (↑A : Set G)
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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)
⊢ a •> (↑(stabilizer G A) : Set G) = (↑A : Set G) ∧ (↑(stabilizer G A) : Set G) <• a = (↑A : Set G)
have refine_2 : (↑(stabilizer G A) : Set G) <• a = (↑A : Set G)
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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)
have refine_1 : a •> a⁻¹ •> (↑A : Set G) = (↑A : Set G)
Tactic: rw [← inv_smul_A ha, smul_inv_smul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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)
⊢ a •> (↑(stabilizer G A) : Set G) = (↑A : Set G)
have refine_1₁ : (↑A : Set G) = (↑A : Set G)
Tactic: rw [← inv_smul_A ha, smul_inv_smul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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)
⊢ (↑(stabilizer G A) : Set G) <• a = (↑A : Set G)
have refine_2 : a⁻¹ •> ((↑A : Set G) <• a) = (↑A : Set G)
Tactic: rw [← inv_smul_A ha, smul_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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⁻¹ •> ((↑A : Set G) <• a) = (↑A : Set G)
have refine_2 : a⁻¹ •> (A <• a) = A
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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⁻¹ •> (A <• a) = A
have refine_2 : a⁻¹ •> a •> A = A
Tactic: rw [← smul_A_eq_A_smul ha, inv_smul_smul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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 <• a) = A
have refine_2₁ : A = A
Tactic: rw [← smul_A_eq_A_smul ha, inv_smul_smul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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)
have a₁ : a •> A ∪ b •> A ⊆ B * A
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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
have a₁ : a •> A ⊆ B * A ∧ b •> A ⊆ B * A
Tactic: rw [union_subset_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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
⊢ 2 * #A ≤ #(a •> A ∩ b •> A) + #(B * A)
have this : #(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⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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) + #(B * A)
have grw : 2 * #A ≤ #(a •> A) + #(b •> A)
Tactic: grw [← this, card_inter_add_card_union]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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
⊢ (2 - K) * (↑(#A) : ℝ) ≤ (↑(#(a •> A ∩ b •> A)) : ℝ)
have this : 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
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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
this : HMul.hMul (α := ℝ) 2 (↑(#A) : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑(#(a •> A ∩ b •> A)) : ℝ) (↑(#(B * A)) : ℝ)
⊢ (2 - K) * (↑(#A) : ℝ) ≤ (↑(#(a •> A ∩ b •> A)) : ℝ)
have linarith : (↑(#(a •> A ∩ b •> A)) : ℝ) < (2 - K) * (↑(#A) : ℝ) →
  (↑(#(B * A)) : ℝ) - K * (↑(#A) : ℝ) +
        (HMul.hMul (α := ℝ) 2 (↑(#A) : ℝ) - HAdd.hAdd (α := ℝ) (↑(#(a •> A ∩ b •> A)) : ℝ) (↑(#(B * A)) : ℝ)) +
      ((↑(#(a •> A ∩ b •> A)) : ℝ) - (2 - K) * (↑(#A) : ℝ)) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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
⊢ (2 - K) * (↑(#A) : ℝ) < (↑(#(a •> A ∩ b •> A)) : ℝ)
have this : 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