awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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
⊢ (↑(#(A⁻¹ * A * A⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have 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
Tactic: nlinarith [small_neg_pos_neg_mul hA]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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
⊢ (↑(#(A⁻¹ * A⁻¹ * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have nlinarith : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A⁻¹ * A⁻¹ * A)) : ℝ) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
Tactic: nlinarith [small_neg_neg_pos_mul hA]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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
⊢ (↑(#(A⁻¹ * A⁻¹ * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have nlinarith₁ : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A⁻¹ * A⁻¹ * A)) : ℝ) → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: nlinarith [small_neg_neg_pos_mul hA]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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
⊢ (↑(#(A⁻¹ * A⁻¹ * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have nlinarith₂ : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A⁻¹ * A⁻¹ * A)) : ℝ) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 3 = 1
Tactic: nlinarith [small_neg_neg_pos_mul hA]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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
⊢ (↑(#(A⁻¹ * A⁻¹ * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have 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
Tactic: nlinarith [small_neg_neg_pos_mul hA]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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
⊢ (↑(#(A⁻¹ * A⁻¹ * A⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have inr : ∀ (hA : (↑(#(A * (A * A))) : ℝ) ≤ K * (↑(#A) : ℝ)), (↑(#(A * (A * A))) : ℝ) ≤ K * (K * K) * (↑(#A) : ℝ)
Tactic: simp [*, pow_succ', ← mul_inv_rev] at hA ⊢
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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) : ℝ)
⊢ (↑(#(A * (A * A))) : ℝ) ≤ K * (K * K) * (↑(#A) : ℝ)
have 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
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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
have inl : ∀ (hε : Eq (α := ℤ) |1| 1), HPow.hPow (β := ℤ) A 1 = A
Tactic: obtain rfl | rfl := eq_or_eq_neg_of_abs_eq hε
Cleared hypotheses: ε, hε
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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
⊢ A ^ ε = A
have inr : ∀ (hε : Eq (α := ℤ) |(-1)| 1), HPow.hPow (β := ℤ) A (-1) = A
Tactic: obtain rfl | rfl := eq_or_eq_neg_of_abs_eq hε
Cleared hypotheses: ε, hε
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (hypothesis)
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
⊢ (↑(#(A ^ m)) : ℝ) ≤ K ^ (m - 2) * (↑(#A) : ℝ)
have this : ∀ (ε : ℤ) (hε : |ε| = 1), A ^ ε = A
Tactic: have (ε : ℤ) (hε : |ε| = 1) : A ^ ε = A := by
    obtain rfl | rfl := eq_or_eq_neg_of_abs_eq hε <;> simp [hAsymm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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
⊢ (↑(#(A ^ m)) : ℝ) ≤ K ^ (m - 2) * (↑(#A) : ℝ)
have fun : Eq (α := ℝ) (↑(#(A ^ m)) : ℝ)
  (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin m) ↦ HPow.hPow (β := ℤ) A 1) (finRange m)))) : ℝ)
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)
-- 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
⊢ (A.erase 0).subsetSum = A.subsetSum
have refine : ∀ (x : M) (hx : x ∈ A.subsetSum), x ∈ (A.erase 0).subsetSum
Tactic: refine le_antisymm (subsetSum_mono (erase_subset _ _)) fun x hx => ?_
-- 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
x : M
hx : x ∈ A.subsetSum
⊢ x ∈ (A.erase 0).subsetSum
have obtain : ∀ (B : Finset M) (hB : B ⊆ A) (hx : ∑ b ∈ B, b ∈ A.subsetSum), ∑ b ∈ B, b ∈ (A.erase 0).subsetSum
Tactic: obtain ⟨B, hB, rfl⟩ := mem_subsetSum_iff.mp hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SubsetSum (goal)
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 ∈ B, b ∈ (A.erase 0).subsetSum
have refine : B.erase 0 ⊆ A.erase 0
Tactic: refine mem_subsetSum_iff.mpr ⟨B.erase 0, ?_, sum_erase _ (by simp)⟩
-- 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
a : M
a_notin_A : a ∉ A
⊢ a +ᵥ A.subsetSum ⊆ (insert a A).subsetSum
have simp_rw : ∀ ⦃x : M⦄, (∃ (y : M), (∃ B ⊆ A, ∑ b ∈ B, b = y) ∧ a +ᵥ y = x) → ∃ B ⊆ insert a A, ∑ b ∈ B, b = x
Tactic: simp_rw [subset_iff, mem_vadd_finset, mem_subsetSum_iff]
-- 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
a : M
a_notin_A : a ∉ A
B : Finset M
hB : B ⊆ A
⊢ ∑ b ∈ insert a B, b = HVAdd.hVAdd (β := M) a (∑ b ∈ B, b)
have rw : a + ∑ x ∈ B, x = HVAdd.hVAdd (β := M) a (∑ b ∈ B, b)
Tactic: rw [sum_insert (fun h => a_notin_A (hB h))]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SubsetSum (hypothesis)
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)
have this : ∀ x ∈ A.subsetSum, 0 ≤ x
Tactic: have := nonneg_of_mem_subsetSum (fun y hy ↦ (hA y hy).le)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SubsetSum (hypothesis)
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
⊢ #A + #A.subsetSum < #(insert a A).subsetSum
have disjoint : 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'⟩
-- 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
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
have grw : 0 ∈ A.subsetSum ∧ A ⊆ A.subsetSum
Tactic: grw [insert_subset_iff, ← subset_insert]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SubsetSum (hypothesis)
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)
⊢ #A + #A.subsetSum < #(insert a A).subsetSum
have insert_subset : 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⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SubsetSum (hypothesis)
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
have vadd_subset : 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
-- 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
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.subsetSum < #A + 1 + #A.subsetSum
have bc : #A < #A + 1
Tactic: gcongr
-- 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
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 + 1 + #A.subsetSum = #(insert 0 A) + #A.subsetSum
have rw : #A + 1 + #A.subsetSum = #A + 1 + #A.subsetSum
Tactic: rw [card_insert_of_notMem fun h => (hA 0 h).false]
-- 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
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 +ᵥ A.subsetSum) = #(insert 0 A ∪ (a +ᵥ A.subsetSum))
have rw : #(insert 0 A) + #(a +ᵥ A.subsetSum) = #(insert 0 A) + #(a +ᵥ A.subsetSum)
Tactic: rw [card_union_of_disjoint disjoint]
-- 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
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 +ᵥ A.subsetSum)) ≤ #(insert a A).subsetSum
have grw : #(insert a A).subsetSum ≤ #(insert a A).subsetSum
Tactic: grw [union_subset insert_subset vadd_subset]
-- 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
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.subsetSum < #(insert a A).subsetSum
have calc : #A + #A.subsetSum < #A + 1 + #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]
-- 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
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
⊢ #A + #A.subsetSum < #(insert a A).subsetSum
have calc₁ : #A + 1 + #A.subsetSum = #(insert 0 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]
-- 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
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
⊢ #A + #A.subsetSum < #(insert a A).subsetSum
have calc₂ : #(insert 0 A) + #A.subsetSum = #(insert 0 A) + #(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]
-- 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
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)
⊢ #A + #A.subsetSum < #(insert a A).subsetSum
have calc₃ : #(insert 0 A) + #(a +ᵥ A.subsetSum) = #(insert 0 A ∪ (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]
-- 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
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))
⊢ #A + #A.subsetSum < #(insert a A).subsetSum
have calc₄ : #(insert 0 A ∪ (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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SubsetSum (hypothesis)
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
⊢ (#(insert a A) + 1).choose 2 < #(insert a A).subsetSum
have A_pos' : ∀ x ∈ A, 0 < x
Tactic: have A_pos' : ∀ x ∈ A, 0 < x := fun x hx => A_pos x (mem_insert_of_mem hx)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SubsetSum (goal)
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
⊢ (#(insert a A) + 1).choose 2 < #(insert a A).subsetSum
have insert : #A + #A.subsetSum < #(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')]
-- 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 + 1).choose 2 < #A.subsetSum
have empty : ∀ (A_pos : ∀ (x : M), Membership.mem (γ := Finset M) ∅ x → 0 < x),
  (card.{u_1} (α := M) ∅ + 1).choose 2 < card.{u_1} (α := M) (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