awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
this : HPow.hPow (β := ℕ) K 2 ≤ HPow.hPow (β := ℕ) K 3
hδ₀ : δ 0 = 1
hδ₁ : δ 1 = -1
hδ₂ : δ 2 = -1
nlinarith : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A * A⁻¹ * A⁻¹)) : ℝ) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
nlinarith₁ : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A * A⁻¹ * A⁻¹)) : ℝ) → HMul.hMul (α := ℝ) 1 1 = 1
nlinarith₂ : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A * A⁻¹ * A⁻¹)) : ℝ) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 3 = 1
nlinarith₃ : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A * A⁻¹ * A⁻¹)) : ℝ) → HMul.hMul (α := ℝ) 1 1 = 1
nlinarith₄ :
  HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A * A⁻¹ * A⁻¹)) : ℝ) →
    1 * HPow.hPow (β := ℕ) (1 * K) 3 * HMul.hMul (α := ℝ) 1 (↑(#A) : ℝ) -
            HMul.hMul (α := ℝ) 1 (↑(#(A * A⁻¹ * A⁻¹)) : ℝ) +
          (HMul.hMul (α := ℝ) 1 (↑(#(A * A⁻¹ * A⁻¹)) : ℝ) -
            1 * HPow.hPow (β := ℕ) (1 * K) 2 * HMul.hMul (α := ℝ) 1 (↑(#A) : ℝ)) +
        (0 - HSub.hSub (α := ℝ) 0 (↑(#A) : ℝ) * (HPow.hPow (β := ℕ) K 2 - HPow.hPow (β := ℕ) K 3)) =
      0
⊢ (↑(#(A * A⁻¹ * A⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)

Tactic:
nlinarith [small_pos_neg_neg_mul hA]

Premises used: _private.0.Finset.small_pos_neg_neg_mul
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
this : HPow.hPow (β := ℕ) K 2 ≤ HPow.hPow (β := ℕ) K 3
hδ₀ : δ 0 = -1
hδ₁ : δ 1 = 1
hδ₂ : δ 2 = 1
nlinarith : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A⁻¹ * A * A)) : ℝ) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
nlinarith₁ : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A⁻¹ * A * A)) : ℝ) → HMul.hMul (α := ℝ) 1 1 = 1
nlinarith₂ : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A⁻¹ * A * A)) : ℝ) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 3 = 1
nlinarith₃ : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A⁻¹ * A * A)) : ℝ) → HMul.hMul (α := ℝ) 1 1 = 1
nlinarith₄ :
  HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A⁻¹ * A * A)) : ℝ) →
    1 * HPow.hPow (β := ℕ) (1 * K) 3 * HMul.hMul (α := ℝ) 1 (↑(#A) : ℝ) - HMul.hMul (α := ℝ) 1 (↑(#(A⁻¹ * A * A)) : ℝ) +
          (HMul.hMul (α := ℝ) 1 (↑(#(A⁻¹ * A * A)) : ℝ) -
            1 * HPow.hPow (β := ℕ) (1 * K) 2 * HMul.hMul (α := ℝ) 1 (↑(#A) : ℝ)) +
        (0 - HSub.hSub (α := ℝ) 0 (↑(#A) : ℝ) * (HPow.hPow (β := ℕ) K 2 - HPow.hPow (β := ℕ) K 3)) =
      0
⊢ (↑(#(A⁻¹ * A * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)

Tactic:
nlinarith [small_neg_pos_pos_mul hA]

Premises used: _private.0.Finset.small_neg_pos_pos_mul
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
this : HPow.hPow (β := ℕ) K 2 ≤ HPow.hPow (β := ℕ) K 3
hδ₀ : δ 0 = -1
hδ₁ : δ 1 = 1
hδ₂ : δ 2 = -1
nlinarith : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A⁻¹ * A * A⁻¹)) : ℝ) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 3 = 1
nlinarith₁ : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A⁻¹ * A * A⁻¹)) : ℝ) → HMul.hMul (α := ℝ) 1 1 = 1
nlinarith₂ : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A⁻¹ * A * A⁻¹)) : ℝ) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 3 = 1
nlinarith₃ : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A⁻¹ * A * A⁻¹)) : ℝ) → HMul.hMul (α := ℝ) 1 1 = 1
nlinarith₄ :
  HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A⁻¹ * A * A⁻¹)) : ℝ) →
    1 * HPow.hPow (β := ℕ) (1 * K) 3 * HMul.hMul (α := ℝ) 1 (↑(#A) : ℝ) -
          HMul.hMul (α := ℝ) 1 (↑(#(A⁻¹ * A * A⁻¹)) : ℝ) +
        (HMul.hMul (α := ℝ) 1 (↑(#(A⁻¹ * A * A⁻¹)) : ℝ) -
          1 * HPow.hPow (β := ℕ) (1 * K) 3 * HMul.hMul (α := ℝ) 1 (↑(#A) : ℝ)) =
      0
⊢ (↑(#(A⁻¹ * A * A⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)

Tactic:
nlinarith [small_neg_pos_neg_mul hA]

Premises used: _private.0.Finset.small_neg_pos_neg_mul
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
this : HPow.hPow (β := ℕ) K 2 ≤ HPow.hPow (β := ℕ) K 3
hδ₀ : δ 0 = -1
hδ₁ : δ 1 = -1
hδ₂ : δ 2 = 1
nlinarith : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A⁻¹ * A⁻¹ * A)) : ℝ) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
nlinarith₁ : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A⁻¹ * A⁻¹ * A)) : ℝ) → HMul.hMul (α := ℝ) 1 1 = 1
nlinarith₂ : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A⁻¹ * A⁻¹ * A)) : ℝ) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 3 = 1
nlinarith₃ : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A⁻¹ * A⁻¹ * A)) : ℝ) → HMul.hMul (α := ℝ) 1 1 = 1
nlinarith₄ :
  HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A⁻¹ * A⁻¹ * A)) : ℝ) →
    1 * HPow.hPow (β := ℕ) (1 * K) 3 * HMul.hMul (α := ℝ) 1 (↑(#A) : ℝ) -
            HMul.hMul (α := ℝ) 1 (↑(#(A⁻¹ * A⁻¹ * A)) : ℝ) +
          (HMul.hMul (α := ℝ) 1 (↑(#(A⁻¹ * A⁻¹ * A)) : ℝ) -
            1 * HPow.hPow (β := ℕ) (1 * K) 2 * HMul.hMul (α := ℝ) 1 (↑(#A) : ℝ)) +
        (0 - HSub.hSub (α := ℝ) 0 (↑(#A) : ℝ) * (HPow.hPow (β := ℕ) K 2 - HPow.hPow (β := ℕ) K 3)) =
      0
⊢ (↑(#(A⁻¹ * A⁻¹ * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)

Tactic:
nlinarith [small_neg_neg_pos_mul hA]

Premises used: _private.0.Finset.small_neg_neg_pos_mul
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
this : HPow.hPow (β := ℕ) K 2 ≤ HPow.hPow (β := ℕ) K 3
hδ₀ : δ 0 = -1
hδ₁ : δ 1 = -1
hδ₂ : δ 2 = -1
inr : ∀ (hA : (↑(#(A * (A * A))) : ℝ) ≤ K * (↑(#A) : ℝ)), (↑(#(A * (A * A))) : ℝ) ≤ K * (K * K) * (↑(#A) : ℝ)
⊢ (↑(#(A⁻¹ * A⁻¹ * A⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)

Tactic:
simp [*, pow_succ', ← mul_inv_rev] at hA ⊢

Premises used: mul_inv_rev, pow_succ'
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
this : HPow.hPow (β := ℕ) K 2 ≤ HPow.hPow (β := ℕ) K 3
hδ₀ : δ 0 = -1
hδ₁ : δ 1 = -1
hδ₂ : δ 2 = -1
hA : (↑(#(A * (A * A))) : ℝ) ≤ K * (↑(#A) : ℝ)
nlinarith :
  K * (K * K) * (↑(#A) : ℝ) < (↑(#(A * (A * A))) : ℝ) →
    (↑(#(A * (A * A))) : ℝ) - K * (↑(#A) : ℝ) + (K * (K * K) * (↑(#A) : ℝ) - (↑(#(A * (A * A))) : ℝ)) +
            (0 - HSub.hSub (α := ℝ) 0 (↑(#(A * (A * A))) : ℝ) * (1 - K)) +
          (0 - HSub.hSub (α := ℝ) 0 (↑(#A) : ℝ) * (HPow.hPow (β := ℕ) K 2 - HPow.hPow (β := ℕ) K 3)) +
        (0 - (1 - K) * ((↑(#(A * (A * A))) : ℝ) - K * (↑(#A) : ℝ))) =
      0
⊢ (↑(#(A * (A * A))) : ℝ) ≤ K * (K * K) * (↑(#A) : ℝ)

Tactic:
nlinarith
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
hAsymm : A⁻¹ = A
ε : ℤ
hε : |ε| = 1
inl : ∀ (hε : Eq (α := ℤ) |1| 1), HPow.hPow (β := ℤ) A 1 = A
inr : ∀ (hε : Eq (α := ℤ) |(-1)| 1), HPow.hPow (β := ℤ) A (-1) = A
⊢ A ^ ε = A

Tactic:
obtain rfl | rfl := eq_or_eq_neg_of_abs_eq hε

Premises used: eq_or_eq_neg_of_abs_eq, rfl
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
hAsymm : A⁻¹ = A
hε : Eq (α := ℤ) |1| 1
⊢ HPow.hPow (β := ℤ) A 1 = A

Tactic:
simp [hAsymm]
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
hAsymm : A⁻¹ = A
hε : Eq (α := ℤ) |(-1)| 1
⊢ HPow.hPow (β := ℤ) A (-1) = A

Tactic:
simp [hAsymm]
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
hAsymm : A⁻¹ = A
⊢ ∀ (ε : ℤ) (hε : |ε| = 1), A ^ ε = A

Tactic:
have (ε : ℤ) (hε : |ε| = 1) : A ^ ε = A := by
    obtain rfl | rfl := eq_or_eq_neg_of_abs_eq hε <;> simp [hAsymm]
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
hAsymm : A⁻¹ = A
this : ∀ (ε : ℤ) (hε : |ε| = 1), A ^ ε = A
⊢ Eq (α := ℝ) (↑(#(A ^ m)) : ℝ)
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin m) ↦ HPow.hPow (β := ℤ) A 1) (finRange m)))) : ℝ)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
hAsymm : A⁻¹ = A
this : ∀ (ε : ℤ) (hε : |ε| = 1), A ^ ε = A
δ : Fin 3 → ℤ
hδ : ∀ (i : Fin 3), |δ i| = 1
⊢ (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ δ i) (finRange 3)))) : ℝ) ≤ K * (↑(#A) : ℝ)

Tactic:
simpa [this _ (hδ _), pow_succ'] using hA

Premises used: pow_succ'
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
hAsymm : A⁻¹ = A
this : ∀ (ε : ℤ) (hε : |ε| = 1), A ^ ε = A
⊢ ∀ (i : Fin m), Eq (α := ℤ) |1| 1

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
hAsymm : A⁻¹ = A
this : ∀ (ε : ℤ) (hε : |ε| = 1), A ^ ε = A
fun :
  Eq (α := ℝ) (↑(#(A ^ m)) : ℝ)
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin m) ↦ HPow.hPow (β := ℤ) A 1) (finRange m)))) : ℝ)
⊢ (↑(#(A ^ m)) : ℝ) ≤ K ^ (m - 2) * (↑(#A) : ℝ)

Tactic:
calc
    (#(A ^ m) : ℝ) = #((finRange m).map fun i ↦ A ^ 1).prod := by simp
    _ ≤ K ^ (m - 2) * #A :=
      inductive_claim_mul hm (fun δ hδ ↦ by simpa [this _ (hδ _), pow_succ'] using hA) _ (by simp)

Premises used: List.map, HSub.hSub, Nat.cast, _private.0.Finset.inductive_claim_mul, HPow.hPow, Finset.card, OfNat.ofNat, List.finRange, List.prod
-- Module: Mathlib.Combinatorics.Additive.SubsetSum
Goal:
M : Type u_1
inst : DecidableEq M
inst_1 : AddCommMonoid M
A : Finset M
a : M
⊢ a ∈ A.subsetSum ↔ ∃ B ⊆ A, ∑ b ∈ B, b = a

Tactic:
simp [subsetSum]

Premises used: Finset.subsetSum
-- Module: Mathlib.Combinatorics.Additive.SubsetSum
Goal:
M : Type u_1
inst : DecidableEq M
inst_1 : AddCommMonoid M
A : Finset M
⊢ 0 ∈ A.subsetSum

Tactic:
mem_subsetSum_iff.mpr ⟨∅, empty_subset _, sum_empty⟩

Premises used: Iff.mpr, Finset.mem_subsetSum_iff, And.intro, Exists.intro, Finset.empty_subset, Finset.sum_empty, EmptyCollection.emptyCollection
-- Module: Mathlib.Combinatorics.Additive.SubsetSum
Goal:
M : Type u_1
inst : DecidableEq M
inst_1 : AddCommMonoid M
A : Finset M
⊢ 0 ∈ A.subsetSum

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.SubsetSum
Goal:
M : Type u_1
inst : DecidableEq M
inst_1 : AddCommMonoid M
A : Finset M
a : M
ha : a ∈ A
⊢ {a} ⊆ A ∧ ∑ b ∈ {a}, b = a

Tactic:
simp [ha]
-- Module: Mathlib.Combinatorics.Additive.SubsetSum
Goal:
M : Type u_1
inst : DecidableEq M
inst_1 : AddCommMonoid M
A B : Finset M
hAB : A ⊆ B
⊢ A.subsetSum ⊆ B.subsetSum

Tactic:
image_mono _ <| powerset_mono.mpr hAB

Premises used: Iff.mpr, Set.Mem, setOf, Finset.powerset_mono, Finset.image_mono
-- Module: Mathlib.Combinatorics.Additive.SubsetSum
Goal:
M : Type u_1
inst : DecidableEq M
inst_1 : AddCommMonoid M
A : Finset M
⊢ (A.erase 0).subsetSum = A.subsetSum

Tactic:
le_antisymm (subsetSum_mono (erase_subset _ _)) fun x hx => ?_

Premises used: le_antisymm, Finset.subsetSum_mono, Finset.erase_subset
-- Module: Mathlib.Combinatorics.Additive.SubsetSum
Goal:
M : Type u_1
inst : DecidableEq M
inst_1 : AddCommMonoid M
A : Finset M
refine : ∀ (x : M) (hx : x ∈ A.subsetSum), x ∈ (A.erase 0).subsetSum
⊢ (A.erase 0).subsetSum = A.subsetSum

Tactic:
refine le_antisymm (subsetSum_mono (erase_subset _ _)) fun x hx => ?_

Premises used: le_antisymm
-- Module: Mathlib.Combinatorics.Additive.SubsetSum
Goal:
M : Type u_1
inst : DecidableEq M
inst_1 : AddCommMonoid M
A : Finset M
x : M
hx : x ∈ A.subsetSum
obtain : ∀ (B : Finset M) (hB : B ⊆ A) (hx : ∑ b ∈ B, b ∈ A.subsetSum), ∑ b ∈ B, b ∈ (A.erase 0).subsetSum
⊢ x ∈ (A.erase 0).subsetSum

Tactic:
obtain ⟨B, hB, rfl⟩ := mem_subsetSum_iff.mp hx

Premises used: Finset.mem_subsetSum_iff, Iff.mp, rfl
-- Module: Mathlib.Combinatorics.Additive.SubsetSum
Goal:
M : Type u_1
inst : DecidableEq M
inst_1 : AddCommMonoid M
A B : Finset M
hB : B ⊆ A
hx : ∑ b ∈ B, b ∈ A.subsetSum
⊢ Eq.{u_1 + 1} (α := M) 0 0

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.SubsetSum
Goal:
M : Type u_1
inst : DecidableEq M
inst_1 : AddCommMonoid M
A B : Finset M
hB : B ⊆ A
hx : ∑ b ∈ B, b ∈ A.subsetSum
refine : B.erase 0 ⊆ A.erase 0
⊢ ∑ b ∈ B, b ∈ (A.erase 0).subsetSum

Tactic:
refine mem_subsetSum_iff.mpr ⟨B.erase 0, ?_, sum_erase _ (by simp)⟩

Premises used: Iff.mpr, Finset.mem_subsetSum_iff, And.intro, Exists.intro, Finset.sum_erase, OfNat.ofNat, Finset.erase
-- Module: Mathlib.Combinatorics.Additive.SubsetSum
Goal:
M : Type u_1
inst : DecidableEq M
inst_1 : AddCommMonoid M
A B : Finset M
hB : B ⊆ A
hx : ∑ b ∈ B, b ∈ A.subsetSum
⊢ B.erase 0 ⊆ A.erase 0

Tactic:
fun i hi => mem_erase.mpr ⟨(mem_erase.mp hi).1, hB (mem_of_mem_erase hi)⟩

Premises used: Iff.mpr, Finset.mem_erase, And.left, Finset.mem_of_mem_erase, And.intro, Iff.mp
-- Module: Mathlib.Combinatorics.Additive.SubsetSum
Goal:
M : Type u_1
inst : DecidableEq M
inst_1 : AddCommMonoid M
A B : Finset M
hB : B ⊆ A
hx : ∑ b ∈ B, b ∈ A.subsetSum
⊢ B.erase 0 ⊆ A.erase 0

Tactic:
exact fun i hi => mem_erase.mpr ⟨(mem_erase.mp hi).1, hB (mem_of_mem_erase hi)⟩

Premises used: Iff.mpr, Finset.mem_erase, And.left, Finset.mem_of_mem_erase, And.intro, Iff.mp
-- Module: Mathlib.Combinatorics.Additive.SubsetSum
Goal:
M : Type u_1
inst : DecidableEq M
inst_1 : AddCommMonoid M
A : Finset M
a : M
a_notin_A : a ∉ A
simp_rw : ∀ ⦃x : M⦄, (∃ (y : M), (∃ B ⊆ A, ∑ b ∈ B, b = y) ∧ a +ᵥ y = x) → ∃ B ⊆ insert a A, ∑ b ∈ B, b = x
⊢ a +ᵥ A.subsetSum ⊆ (insert a A).subsetSum

Tactic:
simp_rw [subset_iff, mem_vadd_finset, mem_subsetSum_iff]

Premises used: Finset.mem_subsetSum_iff, Finset.mem_vadd_finset, Finset.subset_iff
-- Module: Mathlib.Combinatorics.Additive.SubsetSum
Goal:
M : Type u_1
inst : DecidableEq M
inst_1 : AddCommMonoid M
A : Finset M
a : M
a_notin_A : a ∉ A
B : Finset M
hB : B ⊆ A
⊢ insert a B ⊆ insert a A

Tactic:
aesop
-- Module: Mathlib.Combinatorics.Additive.SubsetSum
Goal:
M : Type u_1
inst : DecidableEq M
inst_1 : AddCommMonoid M
A : Finset M
a : M
a_notin_A : a ∉ A
B : Finset M
hB : B ⊆ A
rw : a + ∑ x ∈ B, x = HVAdd.hVAdd (β := M) a (∑ b ∈ B, b)
⊢ ∑ b ∈ insert a B, b = HVAdd.hVAdd (β := M) a (∑ b ∈ B, b)

Tactic:
rw [sum_insert (fun h => a_notin_A (hB h))]

Premises used: Finset.sum_insert
-- Module: Mathlib.Combinatorics.Additive.SubsetSum
Goal:
M : Type u_1
inst : DecidableEq M
inst_1 : AddCommMonoid M
A : Finset M
a : M
a_notin_A : a ∉ A
B : Finset M
hB : B ⊆ A
⊢ a + ∑ x ∈ B, x = HVAdd.hVAdd (β := M) a (∑ b ∈ B, b)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.SubsetSum
Goal:
M : Type u_1
inst : DecidableEq M
inst_1 : AddCommMonoid M
A : Finset M
a : M
a_notin_A : a ∉ A
B : Finset M
hB : B ⊆ A
⊢ ∃ B_1 ⊆ insert a A, ∑ b ∈ B_1, b = HVAdd.hVAdd (β := M) a (∑ b ∈ B, b)

Tactic:
exact ⟨insert a B, by aesop, by rw [sum_insert (fun h => a_notin_A (hB h))]; simp⟩
-- 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_nonneg : ∀ x ∈ A, 0 ≤ x
⊢ ∀ x ∈ A.subsetSum, 0 ≤ x

Tactic:
simpa [mem_subsetSum_iff] using fun B hB ↦ Finset.sum_nonneg fun x hx ↦ A_nonneg _ <| hB hx

Premises used: Finset.mem_subsetSum_iff, Finset.sum_nonneg
-- 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
⊢ ∀ x ∈ A.subsetSum, 0 ≤ x

Tactic:
have := nonneg_of_mem_subsetSum (fun y hy ↦ (hA y hy).le)
-- 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
this : ∀ x ∈ A.subsetSum, 0 ≤ x
⊢ Disjoint (insert 0 A) (a +ᵥ A.subsetSum)

Tactic:
simpa [disjoint_left, mem_insert, mem_vadd_finset] using
      ⟨fun x hx => (add_pos_of_pos_of_nonneg ha <| this _ hx).ne',
        fun x hx y hy ↦ (lt_add_of_lt_of_nonneg (hAa x hx) <| this _ hy).ne'⟩

Premises used: Finset.mem_insert, Finset.mem_vadd_finset, Finset.disjoint_left
-- 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 (insert 0 A) (a +ᵥ A.subsetSum)

Tactic:
have disjoint : Disjoint (insert 0 A) (a +ᵥ A.subsetSum) := by
    have := nonneg_of_mem_subsetSum (fun y hy ↦ (hA y hy).le)
    simpa [disjoint_left, mem_insert, mem_vadd_finset] using
      ⟨fun x hx => (add_pos_of_pos_of_nonneg ha <| this _ hx).ne',
        fun x hx y hy ↦ (lt_add_of_lt_of_nonneg (hAa x hx) <| this _ hy).ne'⟩
-- 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)
grw : 0 ∈ A.subsetSum ∧ A ⊆ A.subsetSum
⊢ insert 0 A ⊆ (insert a A).subsetSum

Tactic:
grw [insert_subset_iff, ← subset_insert]

Premises used: Finset.insert_subset_iff, Finset.subset_insert
-- 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)
⊢ 0 ∈ A.subsetSum ∧ A ⊆ A.subsetSum

Tactic:
⟨zero_mem_subsetSum, subset_subsetSum⟩

Premises used: Finset.zero_mem_subsetSum, Finset.subset_subsetSum, And.intro
-- 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)
⊢ 0 ∈ A.subsetSum ∧ A ⊆ A.subsetSum

Tactic:
exact ⟨zero_mem_subsetSum, subset_subsetSum⟩
-- 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 0 A ⊆ (insert a A).subsetSum

Tactic:
have insert_subset : insert 0 A ⊆ (insert a A).subsetSum := by
    grw [insert_subset_iff, ← subset_insert]; exact ⟨zero_mem_subsetSum, subset_subsetSum⟩
-- 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
⊢ a +ᵥ A.subsetSum ⊆ (insert a A).subsetSum

Tactic:
have vadd_subset : a +ᵥ A.subsetSum ⊆ (insert a A).subsetSum :=
    vadd_finset_subsetSum_subset_subsetSum_insert fun ha => (hAa a ha).false
-- 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
bc : #A < #A + 1
⊢ #A + #A.subsetSum < #A + 1 + #A.subsetSum

Tactic:
gcongr
-- 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
⊢ #A < #A + 1

Tactic:
Nat.lt_add_one _

Premises used: Nat.lt_add_one
-- 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
⊢ #A < #A + 1

Tactic:
exact Nat.lt_add_one _

Premises used: Nat.lt_add_one
-- 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
rw rw₁ : #A + 1 + #A.subsetSum = #A + 1 + #A.subsetSum
⊢ #A + 1 + #A.subsetSum = #(insert 0 A) + #A.subsetSum

Tactic:
rw [card_insert_of_notMem fun h => (hA 0 h).false]

Premises used: Finset.card_insert_of_notMem, LT.lt.false, OfNat.ofNat
-- 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
⊢ #(insert 0 A) + #A.subsetSum = #(insert 0 A) + #(a +ᵥ A.subsetSum)

Tactic:
simp [vadd_finset_def, card_image_of_injOn]

Premises used: Finset.vadd_finset_def, Finset.card_image_of_injOn
-- 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
rw rw₁ : #(insert 0 A) + #(a +ᵥ A.subsetSum) = #(insert 0 A) + #(a +ᵥ A.subsetSum)
⊢ #(insert 0 A) + #(a +ᵥ A.subsetSum) = #(insert 0 A ∪ (a +ᵥ A.subsetSum))

Tactic:
rw [card_union_of_disjoint disjoint]

Premises used: Finset.card_union_of_disjoint