awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
p : σ →₀ ℕ
hp : Eq (α := ℕ) (p.sum fun (a : σ) (k : ℕ) ↦ k) 1
refine_2 :
  ∀ (a : σ) (hp : Eq (α := ℕ) (sum (single a 1) fun (a : σ) (k : ℕ) ↦ k) 1),
    Membership.mem (γ := Set (σ →₀ ℕ)) (Set.range fun (a : σ) ↦ single a 1) (single a 1)
⊢ Membership.mem (γ := Set (σ →₀ ℕ)) (Set.range fun (a : σ) ↦ single a 1) p

Tactic:
obtain ⟨a, rfl⟩ := (Finsupp.sum_eq_one_iff _).mp hp

Premises used: Iff.mp, Finsupp.sum_eq_one_iff, rfl
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
a : σ
hp : Eq (α := ℕ) (sum (single a 1) fun (a : σ) (k : ℕ) ↦ k) 1
w : σ
h : Eq (α := σ →₀ ℕ) ((fun (a : σ) ↦ (single a 1 : σ →₀ ℕ)) a) (single a 1)
⊢ Membership.mem (γ := Set (σ →₀ ℕ)) (Set.range fun (a : σ) ↦ single a 1) (single a 1)

Tactic:
use a
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
M : Type u_2
τ : Type u_5
f : σ → τ
inst : AddCommMonoid M
x : σ →₀ M
simp : Eq.{u_2 + 1} (α := M) (∑ x_1 ∈ x.support, (x : (a : σ) → M) x_1 : M) ((degree : (a : σ →₀ M) → M) x : M)
⊢ Eq.{u_2 + 1} (α := M) ((degree : (a : τ →₀ M) → M) (mapDomain f x) : M) ((degree : (a : σ →₀ M) → M) x : M)

Tactic:
simp [mapDomain, sum]

Premises used: Finsupp.mapDomain, Finsupp.sum
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
M : Type u_2
τ : Type u_5
f : σ → τ
inst : AddCommMonoid M
x : σ →₀ M
⊢ Eq.{u_2 + 1} (α := M) (∑ x_1 ∈ x.support, (x : (a : σ) → M) x_1 : M) ((degree : (a : σ →₀ M) → M) x : M)

Tactic:
dsimp [degree_apply]

Premises used: Finsupp.degree_apply
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
M : Type u_2
τ : Type u_5
f : σ → τ
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : CanonicallyOrderedAdd M
x : τ →₀ M
hf : Set.InjOn f (f ⁻¹' (↑x.support : Set τ))
⊢ LE.le.{u_2} (α := M) ((degree : (a : σ →₀ M) → M) (comapDomain f x hf) : M) ((degree : (a : τ →₀ M) → M) x : M)

Tactic:
simpa [degree, comapDomain, Finset.sum_preimage' f x.support hf x] using
    Finset.sum_le_sum_of_subset (Finset.filter_subset ..)

Premises used: Finsupp.support, Finset.filter_subset, Finsupp.degree, Finset.sum_preimage', Finset.sum_le_sum_of_subset, Finsupp.comapDomain, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
M : Type u_2
τ : Type u_5
f : σ → τ
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : CanonicallyOrderedAdd M
x : τ →₀ M
hf : Set.InjOn f (f ⁻¹' (↑x.support : Set τ))
⊢ LE.le.{u_2} (α := M) ((degree : (a : σ →₀ M) → M) (comapDomain f x hf) : M) ((degree : (a : τ →₀ M) → M) x : M)

Tactic:
classical
  simpa [degree, comapDomain, Finset.sum_preimage' f x.support hf x] using
    Finset.sum_le_sum_of_subset (Finset.filter_subset ..)

Premises used: Finset.filter_subset, Finsupp.degree, Finset.sum_le_sum_of_subset, Finsupp.comapDomain
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
R : Type u_5
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
⊢ Monotone (α := σ →₀ R) (β := R) (⇑degree : (a : σ →₀ R) → R)

Tactic:
fun _ _ e ↦
    (Finset.sum_le_sum_of_subset (support_mono e)).trans (Finset.sum_le_sum fun _ _ ↦ e _)

Premises used: Multiset.sum, Multiset.foldr, Monotone, Finset.sum_le_sum_of_subset, Finsupp.support_mono, Finset.sum_le_sum, LE.le.trans, Finset.sum
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_5
f : σ →₀ ℕ
hn : LE.le (α := ℕ) (0 : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) f : ℕ)
⊢ ∃ g ≤ f, Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) (0 : ℕ)

Tactic:
simp [degree_eq_zero_iff]

Premises used: Finsupp.degree_eq_zero_iff
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_5
f : σ →₀ ℕ
n : ℕ
IH : ∀ (hn : n ≤ (degree : (a : σ →₀ ℕ) → ℕ) f), ∃ g ≤ f, (degree : (a : σ →₀ ℕ) → ℕ) g = n
hn : n + 1 ≤ (degree : (a : σ →₀ ℕ) → ℕ) f
⊢ n ≤ (degree : (a : σ →₀ ℕ) → ℕ) f

Tactic:
lia
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_5
f : σ →₀ ℕ
n : ℕ
IH : ∀ (hn : n ≤ (degree : (a : σ →₀ ℕ) → ℕ) f), ∃ g ≤ f, (degree : (a : σ →₀ ℕ) → ℕ) g = n
hn : n + 1 ≤ (degree : (a : σ →₀ ℕ) → ℕ) f
succ :
  ∀ (g : σ →₀ ℕ) (hgf : g ≤ f)
    (IH :
      ∀ (hn : LE.le (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) f : ℕ)),
        ∃ g_1 ≤ f, Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g_1 : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ))
    (hn : HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) (1 : ℕ) ≤ (degree : (a : σ →₀ ℕ) → ℕ) f),
    ∃ g_1 ≤ f, (degree : (a : σ →₀ ℕ) → ℕ) g_1 = HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) (1 : ℕ)
⊢ ∃ g ≤ f, (degree : (a : σ →₀ ℕ) → ℕ) g = n + 1

Tactic:
obtain ⟨g, hgf, rfl⟩ := IH (by lia)

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_5
f g : σ →₀ ℕ
hgf : g ≤ f
IH :
  ∀ (hn : LE.le (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) f : ℕ)),
    ∃ g_1 ≤ f, Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g_1 : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ)
hn : HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) (1 : ℕ) ≤ (degree : (a : σ →₀ ℕ) → ℕ) f
succ :
  ∀ (f : σ →₀ ℕ) (hgf : g ≤ g + f)
    (IH :
      ∀ (hn : LE.le (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) (g + f) : ℕ)),
        ∃ g_1 ≤ g + f, Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g_1 : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ))
    (hn :
      HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) (1 : ℕ) ≤ (degree : (a : σ →₀ ℕ) → ℕ) (g + f)),
    ∃ g_1 ≤ g + f,
      (degree : (a : σ →₀ ℕ) → ℕ) g_1 = HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) (1 : ℕ)
⊢ ∃ g_1 ≤ f, (degree : (a : σ →₀ ℕ) → ℕ) g_1 = HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) (1 : ℕ)

Tactic:
obtain ⟨f, rfl⟩ := le_iff_exists_add.mp hgf

Premises used: le_iff_exists_add, Iff.mp, rfl
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_5
g f : σ →₀ ℕ
hgf : g ≤ g + f
IH :
  ∀ (hn : LE.le (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) (g + f) : ℕ)),
    ∃ g_1 ≤ g + f, Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g_1 : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ)
hn : HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) (1 : ℕ) ≤ (degree : (a : σ →₀ ℕ) → ℕ) (g + f)
⊢ f.support.Nonempty

Tactic:
aesop
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_5
g f : σ →₀ ℕ
hgf : g ≤ g + f
IH :
  ∀ (hn : LE.le (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) (g + f) : ℕ)),
    ∃ g_1 ≤ g + f, Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g_1 : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ)
hn : HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) (1 : ℕ) ≤ (degree : (a : σ →₀ ℕ) → ℕ) (g + f)
succ :
  ∀ (i : σ) (hi : i ∈ f.support),
    ∃ g_1 ≤ g + f,
      (degree : (a : σ →₀ ℕ) → ℕ) g_1 = HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) (1 : ℕ)
⊢ ∃ g_1 ≤ g + f,
    (degree : (a : σ →₀ ℕ) → ℕ) g_1 = HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) (1 : ℕ)

Tactic:
obtain ⟨i, hi⟩ : f.support.Nonempty := by aesop

Premises used: Finsupp.support, Finset.Nonempty
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_5
g f : σ →₀ ℕ
hgf : g ≤ g + f
IH :
  ∀ (hn : LE.le (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) (g + f) : ℕ)),
    ∃ g_1 ≤ g + f, Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g_1 : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ)
hn : HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) (1 : ℕ) ≤ (degree : (a : σ →₀ ℕ) → ℕ) (g + f)
i : σ
hi : i ∈ f.support
simp : LE.le (α := ℕ) (1 : ℕ) ((f : (a : σ) → ℕ) i : ℕ)
⊢ single i 1 ≤ f

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_5
g f : σ →₀ ℕ
hgf : g ≤ g + f
IH :
  ∀ (hn : LE.le (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) (g + f) : ℕ)),
    ∃ g_1 ≤ g + f, Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g_1 : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ)
hn : HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) (1 : ℕ) ≤ (degree : (a : σ →₀ ℕ) → ℕ) (g + f)
i : σ
hi : i ∈ f.support
⊢ LE.le (α := ℕ) (1 : ℕ) ((f : (a : σ) → ℕ) i : ℕ)

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_5
g f : σ →₀ ℕ
hgf : g ≤ g + f
IH :
  ∀ (hn : LE.le (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) (g + f) : ℕ)),
    ∃ g_1 ≤ g + f, Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g_1 : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ)
hn : HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) (1 : ℕ) ≤ (degree : (a : σ →₀ ℕ) → ℕ) (g + f)
i : σ
hi : i ∈ f.support
⊢ (degree : (a : σ →₀ ℕ) → ℕ) (g + single i 1) = HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) (1 : ℕ)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_5
g f : σ →₀ ℕ
hgf : g ≤ g + f
IH :
  ∀ (hn : LE.le (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) (g + f) : ℕ)),
    ∃ g_1 ≤ g + f, Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g_1 : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ)
hn : HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) (1 : ℕ) ≤ (degree : (a : σ →₀ ℕ) → ℕ) (g + f)
i : σ
hi : i ∈ f.support
⊢ ∃ g_1 ≤ g + f,
    (degree : (a : σ →₀ ℕ) → ℕ) g_1 = HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) (1 : ℕ)

Tactic:
exact ⟨g + .single i 1, add_le_add_right (by simp; grind) _, by simp⟩
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_5
f : σ →₀ ℕ
n : ℕ
hn : n ≤ (degree : (a : σ →₀ ℕ) → ℕ) f
zero :
  ∀ (hn : LE.le (α := ℕ) (0 : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) f : ℕ)),
    ∃ g ≤ f, Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) (0 : ℕ)
succ :
  ∀ (n : ℕ) (IH : ∀ (hn : n ≤ (degree : (a : σ →₀ ℕ) → ℕ) f), ∃ g ≤ f, (degree : (a : σ →₀ ℕ) → ℕ) g = n)
    (hn : n + 1 ≤ (degree : (a : σ →₀ ℕ) → ℕ) f), ∃ g ≤ f, (degree : (a : σ →₀ ℕ) → ℕ) g = n + 1
⊢ ∃ g ≤ f, (degree : (a : σ →₀ ℕ) → ℕ) g = n

Tactic:
induction n with
  | zero => simp [degree_eq_zero_iff]
  | succ n IH =>
    obtain ⟨g, hgf, rfl⟩ := IH (by lia)
    obtain ⟨f, rfl⟩ := le_iff_exists_add.mp hgf
    obtain ⟨i, hi⟩ : f.support.Nonempty := by aesop
    exact ⟨g + .single i 1, add_le_add_right (by simp; grind) _, by simp⟩

Premises used: Finsupp.support, Finset.Nonempty, Finsupp.degree_eq_zero_iff, rfl
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_5
s t : Set ℕ
⊢ (⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' (s + t) =
    HAdd.hAdd (α := Set (σ →₀ ℕ)) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' s) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' t)

Tactic:
(Set.preimage_add_preimage_subset ..).antisymm' ?_

Premises used: Set.preimage_add_preimage_subset, HasSubset.Subset.antisymm'
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_5
s t : Set ℕ
refine :
  (⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' (s + t) ⊆
    HAdd.hAdd (α := Set (σ →₀ ℕ)) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' s) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' t)
⊢ (⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' (s + t) =
    HAdd.hAdd (α := Set (σ →₀ ℕ)) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' s) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' t)

Tactic:
refine (Set.preimage_add_preimage_subset ..).antisymm' ?_

Premises used: Set.preimage_add_preimage_subset, HasSubset.Subset.antisymm'
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_5
s t : Set ℕ
f : σ →₀ ℕ
m : ℕ
hm : m ∈ s
n : ℕ
hn : n ∈ t
e : m + n = (degree : (a : σ →₀ ℕ) → ℕ) f
⊢ m ≤ (degree : (a : σ →₀ ℕ) → ℕ) f

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_5
s t : Set ℕ
f : σ →₀ ℕ
m : ℕ
hm : m ∈ s
n : ℕ
hn : n ∈ t
e : m + n = (degree : (a : σ →₀ ℕ) → ℕ) f
obtain :
  ∀ (g : σ →₀ ℕ) (hgf : g ≤ f) (hm : Membership.mem (α := ℕ) s ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ))
    (e : HAdd.hAdd (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) n = (degree : (a : σ →₀ ℕ) → ℕ) f),
    f ∈ HAdd.hAdd (α := Set (σ →₀ ℕ)) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' s) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' t)
⊢ f ∈ HAdd.hAdd (α := Set (σ →₀ ℕ)) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' s) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' t)

Tactic:
obtain ⟨g, hgf, rfl⟩ := exists_le_degree_eq f m (by grind)

Premises used: Finsupp.exists_le_degree_eq, rfl
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_5
s t : Set ℕ
f : σ →₀ ℕ
n : ℕ
hn : n ∈ t
g : σ →₀ ℕ
hgf : g ≤ f
hm : Membership.mem (α := ℕ) s ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ)
e : HAdd.hAdd (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) n = (degree : (a : σ →₀ ℕ) → ℕ) f
obtain :
  ∀ (f : σ →₀ ℕ) (hgf : g ≤ g + f)
    (e : HAdd.hAdd (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) n = (degree : (a : σ →₀ ℕ) → ℕ) (g + f)),
    g + f ∈ HAdd.hAdd (α := Set (σ →₀ ℕ)) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' s) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' t)
⊢ f ∈ HAdd.hAdd (α := Set (σ →₀ ℕ)) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' s) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' t)

Tactic:
obtain ⟨f, rfl⟩ := le_iff_exists_add.mp hgf

Premises used: le_iff_exists_add, Iff.mp, rfl
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_5
s t : Set ℕ
n : ℕ
hn : n ∈ t
g : σ →₀ ℕ
hm : Membership.mem (α := ℕ) s ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ)
f : σ →₀ ℕ
hgf : g ≤ g + f
e : HAdd.hAdd (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) n = (degree : (a : σ →₀ ℕ) → ℕ) (g + f)
⊢ Membership.mem (γ := Set (σ →₀ ℕ)) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' t) f

Tactic:
simp_all
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_5
s t : Set ℕ
n : ℕ
hn : n ∈ t
g : σ →₀ ℕ
hm : Membership.mem (α := ℕ) s ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ)
f : σ →₀ ℕ
hgf : g ≤ g + f
e : HAdd.hAdd (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) n = (degree : (a : σ →₀ ℕ) → ℕ) (g + f)
⊢ g + f ∈ HAdd.hAdd (α := Set (σ →₀ ℕ)) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' s) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' t)

Tactic:
exact Set.add_mem_add hm (by simp_all)

Premises used: Set.add_mem_add
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_5
s : Set ℕ
n : ℕ
hn : n ≠ 0
zero :
  ∀ (hn : Ne (α := ℕ) 0 0),
    (⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' HSMul.hSMul (α := ℕ) 0 s =
      HSMul.hSMul (α := ℕ) (β := Set (σ →₀ ℕ)) 0 ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' s)
succ :
  ∀ (n : ℕ) (hn : n + 1 ≠ 0),
    (⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' ((n + 1) • s) =
      HSMul.hSMul (β := Set (σ →₀ ℕ)) (n + 1) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' s)
⊢ (⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' (n • s) = HSMul.hSMul (β := Set (σ →₀ ℕ)) n ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' s)

Tactic:
obtain (_ | n) := n
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_5
s : Set ℕ
hn : Ne (α := ℕ) 0 0
⊢ (⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' HSMul.hSMul (α := ℕ) 0 s =
    HSMul.hSMul (α := ℕ) (β := Set (σ →₀ ℕ)) 0 ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' s)

Tactic:
contradiction
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_5
s : Set ℕ
n : ℕ
hn : n + 1 ≠ 0
succ :
  ∀ (hn : HAdd.hAdd (α := ℕ) 0 1 ≠ 0),
    (⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' (HAdd.hAdd (α := ℕ) 0 1 • s) =
      HSMul.hSMul (β := Set (σ →₀ ℕ)) (HAdd.hAdd (α := ℕ) 0 1) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' s)
succ₁ :
  ∀ (n : ℕ),
    (∀ (hn : n + 1 ≠ 0),
        (⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' ((n + 1) • s) =
          HSMul.hSMul (β := Set (σ →₀ ℕ)) (n + 1) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' s)) →
      ∀ (hn : n + 1 + 1 ≠ 0),
        (⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' ((n + 1 + 1) • s) =
          HSMul.hSMul (β := Set (σ →₀ ℕ)) (n + 1 + 1) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' s)
⊢ (⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' ((n + 1) • s) =
    HSMul.hSMul (β := Set (σ →₀ ℕ)) (n + 1) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' s)

Tactic:
induction n
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_5
s : Set ℕ
hn : HAdd.hAdd (α := ℕ) 0 1 ≠ 0
⊢ (⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' (HAdd.hAdd (α := ℕ) 0 1 • s) =
    HSMul.hSMul (β := Set (σ →₀ ℕ)) (HAdd.hAdd (α := ℕ) 0 1) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' s)

Tactic:
simp_all [succ_nsmul, degree_preimage_add]

Premises used: Finsupp.degree_preimage_add, succ_nsmul
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_5
s : Set ℕ
n : ℕ
h :
  ∀ (hn : n + 1 ≠ 0),
    (⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' ((n + 1) • s) =
      HSMul.hSMul (β := Set (σ →₀ ℕ)) (n + 1) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' s)
hn : n + 1 + 1 ≠ 0
⊢ (⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' ((n + 1 + 1) • s) =
    HSMul.hSMul (β := Set (σ →₀ ℕ)) (n + 1 + 1) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' s)

Tactic:
simp_all [succ_nsmul, degree_preimage_add]

Premises used: Finsupp.degree_preimage_add, succ_nsmul
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
α : Type u_5
s : Set α
⊢ HSMul.hSMul (α := ℕ) (β := Set (α →₀ ℕ)) 0 ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) x : ℕ) (0 : ℕ) ∧ (↑x.support : Set α) ⊆ s}

Tactic:
aesop (add simp degree_eq_zero_iff)

Premises used: Finsupp.degree_eq_zero_iff
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
α : Type u_5
s : Set α
n : ℕ
ih :
  HSMul.hSMul (β := Set (α →₀ ℕ)) n ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
succ :
  HAdd.hAdd (α := Set (α →₀ ℕ)) {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
      ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n + 1 ∧ (↑x.support : Set α) ⊆ s}
⊢ HSMul.hSMul (β := Set (α →₀ ℕ)) (n + 1) ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n + 1 ∧ (↑x.support : Set α) ⊆ s}

Tactic:
rw [succ_nsmul, ih]

Premises used: succ_nsmul
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
α : Type u_5
s : Set α
n : ℕ
ih :
  HSMul.hSMul (β := Set (α →₀ ℕ)) n ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
⊢ HAdd.hAdd (α := Set (α →₀ ℕ)) {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
      ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n + 1 ∧ (↑x.support : Set α) ⊆ s}

Tactic:
subset_antisymm ?_ fun f ⟨f_deg, f_supp⟩ ↦ ?_

Premises used: subset_antisymm
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
α : Type u_5
s : Set α
n : ℕ
ih :
  HSMul.hSMul (β := Set (α →₀ ℕ)) n ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
succ :
  HAdd.hAdd (α := Set (α →₀ ℕ)) {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
      ((fun (x : α) ↦ single x 1) '' s) ⊆
    {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n + 1 ∧ (↑x.support : Set α) ⊆ s}
succ₁ :
  ∀ (f : α →₀ ℕ),
    Membership.mem (γ := Set (α →₀ ℕ)) {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n + 1 ∧ (↑x.support : Set α) ⊆ s}
        f →
      ∀ (f_deg : (degree : (a : α →₀ ℕ) → ℕ) f = n + 1) (f_supp : (↑f.support : Set α) ⊆ s),
        f ∈
          HAdd.hAdd (α := Set (α →₀ ℕ)) {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
            ((fun (x : α) ↦ single x 1) '' s)
⊢ HAdd.hAdd (α := Set (α →₀ ℕ)) {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
      ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n + 1 ∧ (↑x.support : Set α) ⊆ s}

Tactic:
refine subset_antisymm ?_ fun f ⟨f_deg, f_supp⟩ ↦ ?_

Premises used: subset_antisymm
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
α : Type u_5
s : Set α
n : ℕ
ih :
  HSMul.hSMul (β := Set (α →₀ ℕ)) n ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
succ :
  ∀ (b : α →₀ ℕ) (b_1 : (degree : (a : α →₀ ℕ) → ℕ) b = n)
    (b_2 : ∀ (x : α), ¬Eq (α := ℕ) ((b : (a : α) → ℕ) x : ℕ) (0 : ℕ) → x ∈ s),
    ∀ a ∈ s,
      (degree : (a : α →₀ ℕ) → ℕ) b = n ∧
        ∀ (x : α),
          (Eq (α := ℕ) ((b : (a : α) → ℕ) x : ℕ) (0 : ℕ) → ¬Eq (α := ℕ) ((single a 1 : (a : α) → ℕ) x : ℕ) (0 : ℕ)) →
            x ∈ s
⊢ HAdd.hAdd (α := Set (α →₀ ℕ)) {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
      ((fun (x : α) ↦ single x 1) '' s) ⊆
    {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n + 1 ∧ (↑x.support : Set α) ⊆ s}

Tactic:
simp [Set.subset_def, Set.mem_add, @forall_comm (α →₀ ℕ)]

Premises used: Set.subset_def, forall_comm, Set.mem_add
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
α : Type u_5
s : Set α
n : ℕ
ih :
  HSMul.hSMul (β := Set (α →₀ ℕ)) n ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
⊢ ∀ (b : α →₀ ℕ) (b_1 : (degree : (a : α →₀ ℕ) → ℕ) b = n)
    (b_2 : ∀ (x : α), ¬Eq (α := ℕ) ((b : (a : α) → ℕ) x : ℕ) (0 : ℕ) → x ∈ s),
    ∀ a ∈ s,
      (degree : (a : α →₀ ℕ) → ℕ) b = n ∧
        ∀ (x : α),
          (Eq (α := ℕ) ((b : (a : α) → ℕ) x : ℕ) (0 : ℕ) → ¬Eq (α := ℕ) ((single a 1 : (a : α) → ℕ) x : ℕ) (0 : ℕ)) →
            x ∈ s

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
α : Type u_5
s : Set α
n : ℕ
ih :
  HSMul.hSMul (β := Set (α →₀ ℕ)) n ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
f : α →₀ ℕ
h : Membership.mem (γ := Set (α →₀ ℕ)) {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n + 1 ∧ (↑x.support : Set α) ⊆ s} f
f_deg : (degree : (a : α →₀ ℕ) → ℕ) f = n + 1
f_supp : (↑f.support : Set α) ⊆ s
⊢ f.support.Nonempty

Tactic:
aesop
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
α : Type u_5
s : Set α
n : ℕ
ih :
  HSMul.hSMul (β := Set (α →₀ ℕ)) n ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
f : α →₀ ℕ
h : Membership.mem (γ := Set (α →₀ ℕ)) {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n + 1 ∧ (↑x.support : Set α) ⊆ s} f
f_deg : (degree : (a : α →₀ ℕ) → ℕ) f = n + 1
f_supp : (↑f.support : Set α) ⊆ s
succ :
  ∀ (i : α) (hi : i ∈ f.support),
    f ∈
      HAdd.hAdd (α := Set (α →₀ ℕ)) {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
        ((fun (x : α) ↦ single x 1) '' s)
⊢ f ∈
    HAdd.hAdd (α := Set (α →₀ ℕ)) {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
      ((fun (x : α) ↦ single x 1) '' s)

Tactic:
obtain ⟨i, hi⟩ : f.support.Nonempty := by aesop

Premises used: Finsupp.support, Finset.Nonempty
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
α : Type u_5
s : Set α
n : ℕ
ih :
  HSMul.hSMul (β := Set (α →₀ ℕ)) n ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
f : α →₀ ℕ
h : Membership.mem (γ := Set (α →₀ ℕ)) {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n + 1 ∧ (↑x.support : Set α) ⊆ s} f
f_deg : (degree : (a : α →₀ ℕ) → ℕ) f = n + 1
f_supp : (↑f.support : Set α) ⊆ s
i : α
hi : i ∈ f.support
⊢ single i 1 ≤ f

Tactic:
simpa [Nat.one_le_iff_ne_zero] using hi

Premises used: Nat.one_le_iff_ne_zero
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
α : Type u_5
s : Set α
n : ℕ
ih :
  HSMul.hSMul (β := Set (α →₀ ℕ)) n ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
f : α →₀ ℕ
h : Membership.mem (γ := Set (α →₀ ℕ)) {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n + 1 ∧ (↑x.support : Set α) ⊆ s} f
f_deg : (degree : (a : α →₀ ℕ) → ℕ) f = n + 1
f_supp : (↑f.support : Set α) ⊆ s
i : α
hi : i ∈ f.support
succ :
  ∀ (x : α →₀ ℕ) (hx : f = x + single i 1),
    f ∈
      HAdd.hAdd (α := Set (α →₀ ℕ)) {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
        ((fun (x : α) ↦ single x 1) '' s)
⊢ f ∈
    HAdd.hAdd (α := Set (α →₀ ℕ)) {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
      ((fun (x : α) ↦ single x 1) '' s)

Tactic:
obtain ⟨x, hx⟩ := le_iff_exists_add'.mp
      (show single i 1 ≤ f by simpa [Nat.one_le_iff_ne_zero] using hi)

Premises used: Iff.mp, le_iff_exists_add'
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
α : Type u_5
s : Set α
n : ℕ
ih :
  HSMul.hSMul (β := Set (α →₀ ℕ)) n ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
f : α →₀ ℕ
h : Membership.mem (γ := Set (α →₀ ℕ)) {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n + 1 ∧ (↑x.support : Set α) ⊆ s} f
f_deg : (degree : (a : α →₀ ℕ) → ℕ) f = n + 1
f_supp : (↑f.support : Set α) ⊆ s
i : α
hi : i ∈ f.support
x : α →₀ ℕ
hx : f = x + single i 1
⊢ Membership.mem (γ := Set (α →₀ ℕ)) {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s} x

Tactic:
aesop (add simp Set.subset_def)

Premises used: Set.subset_def