awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
inst : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
set set₁ : Set.Finite.{u_1} (α := σ →₀ ℕ) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d ≤ n}
set₂ :
  let fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) :=
    @Finset.antidiagonal _ instAddMonoid _ ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n));
  ∀
    (hfg :
      fg =
        @Finset.antidiagonal _ instAddMonoid _
          ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n))),
    Set.Finite.{u_1} (α := σ →₀ ℕ) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d ≤ n}
⊢ Set.Finite.{u_1} (α := σ →₀ ℕ) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d ≤ n}
have set₃ : let fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) :=
  @Finset.antidiagonal _ instAddMonoid _ ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n));
∀
  (hfg :
    fg =
      @Finset.antidiagonal _ instAddMonoid _
        ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n))),
  {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d ≤ n} ⊆
    (↑(Finset.image (fun (uv : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ uv.1) fg) : Set (σ →₀ ℕ))
Tactic: classical
  set fg := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n)) with hfg
  suffices {d : σ →₀ ℕ | weight w d ≤ n} ⊆ ↑(fg.image fun uv => uv.fst) by
    exact Set.Finite.subset (Finset.finite_toSet _) this
  intro d hd
  rw [hfg]
  simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe,
    Finset.mem_antidiagonal, Prod.exists, exists_and_right, exists_eq_right]
  use Finsupp.equivFunOnFinite.symm (Function.const σ n) - d
  ext x
  dsimp at hd
  grw [← le_weight _ (hw x)] at hd
  simp [*]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
inst : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
set set₁ : Set.Finite.{u_1} (α := σ →₀ ℕ) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d ≤ n}
set₂ :
  let fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) :=
    @Finset.antidiagonal _ instAddMonoid _ ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n));
  ∀
    (hfg :
      fg =
        @Finset.antidiagonal _ instAddMonoid _
          ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n))),
    Set.Finite.{u_1} (α := σ →₀ ℕ) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d ≤ n}
set₃ :
  let fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) :=
    @Finset.antidiagonal _ instAddMonoid _ ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n));
  ∀
    (hfg :
      fg =
        @Finset.antidiagonal _ instAddMonoid _
          ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n))),
    {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d ≤ n} ⊆
      (↑(Finset.image (fun (uv : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ uv.1) fg) : Set (σ →₀ ℕ))
⊢ Set.Finite.{u_1} (α := σ →₀ ℕ) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d ≤ n}
have set₄ : let fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) :=
  @Finset.antidiagonal _ instAddMonoid _ ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n));
∀
  (hfg :
    fg =
      @Finset.antidiagonal _ instAddMonoid _
        ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n)))
  ⦃d : σ →₀ ℕ⦄ (hd : Membership.mem (γ := Set (σ →₀ ℕ)) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d ≤ n} d),
  d ∈ (↑(Finset.image (fun (uv : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ uv.1) fg) : Set (σ →₀ ℕ))
Tactic: classical
  set fg := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n)) with hfg
  suffices {d : σ →₀ ℕ | weight w d ≤ n} ⊆ ↑(fg.image fun uv => uv.fst) by
    exact Set.Finite.subset (Finset.finite_toSet _) this
  intro d hd
  rw [hfg]
  simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe,
    Finset.mem_antidiagonal, Prod.exists, exists_and_right, exists_eq_right]
  use Finsupp.equivFunOnFinite.symm (Function.const σ n) - d
  ext x
  dsimp at hd
  grw [← le_weight _ (hw x)] at hd
  simp [*]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
R : Type u_4
inst : AddCommMonoid R
inst_1 : Fintype σ
f : σ →₀ R
⊢ Eq.{u_4 + 1} (α := R) ((degree : (a : σ →₀ R) → R) f : R) (∑ i : σ, (f : (a : σ) → R) i : R)
have h : f.support ⊆ Finset.univ
Tactic: rw [degree_apply, Finset.sum_subset]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
R : Type u_4
inst : AddCommMonoid R
inst_1 : Fintype σ
f : σ →₀ R
h : f.support ⊆ Finset.univ
⊢ Eq.{u_4 + 1} (α := R) ((degree : (a : σ →₀ R) → R) f : R) (∑ i : σ, (f : (a : σ) → R) i : R)
have hf : ∀ (x : σ),
  Membership.mem (γ := Finset σ) Finset.univ x → x ∉ f.support → Eq.{u_4 + 1} (α := R) ((f : (a : σ) → R) x : R) (0 : R)
Tactic: rw [degree_apply, Finset.sum_subset]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
R : Type u_5
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
s : σ
f : σ →₀ R
⊢ LE.le.{u_5} (α := R) ((f : (a : σ) → R) s : R) ((degree : (a : σ →₀ R) → R) f : R)
have pos : ∀ (h : s ∈ f.support), LE.le.{u_5} (α := R) ((f : (a : σ) → R) s : R) ((degree : (a : σ →₀ R) → R) f : R)
Tactic: by_cases h : s ∈ f.support
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
R : Type u_5
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
s : σ
f : σ →₀ R
pos : ∀ (h : s ∈ f.support), LE.le.{u_5} (α := R) ((f : (a : σ) → R) s : R) ((degree : (a : σ →₀ R) → R) f : R)
⊢ LE.le.{u_5} (α := R) ((f : (a : σ) → R) s : R) ((degree : (a : σ →₀ R) → R) f : R)
have neg : ∀ (h : s ∉ f.support), LE.le.{u_5} (α := R) ((f : (a : σ) → R) s : R) ((degree : (a : σ →₀ R) → R) f : R)
Tactic: by_cases h : s ∈ f.support
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (hypothesis)
Goal:
σ : Type u_1
R : Type u_5
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
s : σ
f : σ →₀ R
h : s ∉ f.support
⊢ LE.le.{u_5} (α := R) ((f : (a : σ) → R) s : R) ((degree : (a : σ →₀ R) → R) f : R)
have h₁ : Eq.{u_5 + 1} (α := R) ((f : (a : σ) → R) s : R) (0 : R)
Tactic: simp only [notMem_support_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
R : Type u_5
inst : Semiring R
⊢ Eq (α := (σ →₀ R) →+ R) degree (weight fun (x : σ) ↦ 1)
have H : ∀ (d : σ) (x : R),
  Eq (α := R) ((AddMonoidHom.comp degree (singleAddHom d) : (a : R) → R) x : R)
    ((AddMonoidHom.comp (N := σ →₀ R) (weight fun (x : σ) ↦ 1) (singleAddHom d) : (a : R) → R) x : R)
Tactic: ext d
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
inst : Finite σ
n : ℕ
⊢ Set.Finite.{u_1} (α := σ →₀ ℕ) {f : σ →₀ ℕ | (degree : (a : σ →₀ ℕ) → ℕ) f ≤ n}
have simp_rw : Set.Finite.{u_1} (α := σ →₀ ℕ) {f : σ →₀ ℕ | (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) f ≤ n}
Tactic: simp_rw [degree_eq_weight_one]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
inst : Finite σ
n : ℕ
⊢ Set.Finite.{u_1} (α := σ →₀ ℕ) {f : σ →₀ ℕ | (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) f ≤ n}
have refine : ∀ (x : σ), Ne (α := ℕ) (Function.const σ 1 x) 0
Tactic: refine finite_of_nat_weight_le (Function.const σ 1) ?_ n
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
⊢ Eq.{max (u_1 + 1) 1} (α := Set (σ →₀ ℕ)) (Set.range fun (a : σ) ↦ single a 1)
    {d : σ →₀ ℕ | Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)}
have refine_1 : Subset.{u_1} (α := Set (σ →₀ ℕ)) (Set.range fun (a : σ) ↦ single a 1)
  {d : σ →₀ ℕ | Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)}
Tactic: refine subset_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
refine_1 :
  Subset.{u_1} (α := Set (σ →₀ ℕ)) (Set.range fun (a : σ) ↦ single a 1)
    {d : σ →₀ ℕ | Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)}
⊢ Eq.{max (u_1 + 1) 1} (α := Set (σ →₀ ℕ)) (Set.range fun (a : σ) ↦ single a 1)
    {d : σ →₀ ℕ | Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)}
have refine_2 : Subset.{u_1} (α := Set (σ →₀ ℕ)) {d : σ →₀ ℕ | Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)}
  (Set.range fun (a : σ) ↦ single a 1)
Tactic: refine subset_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
p : σ →₀ ℕ
⊢ Membership.mem (γ := Set (σ →₀ ℕ)) {d : σ →₀ ℕ | Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)} p →
    Membership.mem (γ := Set (σ →₀ ℕ)) (Set.range fun (a : σ) ↦ single a 1) p
have refine_2 : ∀ (hp : Eq (α := ℕ) (p.sum fun (a : σ) (k : ℕ) ↦ k) 1),
  Membership.mem (γ := Set (σ →₀ ℕ)) (Set.range fun (a : σ) ↦ single a 1) p
Tactic: (hp : p.sum (fun a k ↦ k) = 1)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
p : σ →₀ ℕ
hp : Eq (α := ℕ) (p.sum fun (a : σ) (k : ℕ) ↦ k) 1
⊢ Membership.mem (γ := Set (σ →₀ ℕ)) (Set.range fun (a : σ) ↦ single a 1) p
have 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)
Tactic: obtain ⟨a, rfl⟩ := (Finsupp.sum_eq_one_iff _).mp hp
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
a : σ
hp : Eq (α := ℕ) (sum (single a 1) fun (a : σ) (k : ℕ) ↦ k) 1
w : σ
⊢ Membership.mem (γ := Set (σ →₀ ℕ)) (Set.range fun (a : σ) ↦ single a 1) (single a 1)
have h : Eq (α := σ →₀ ℕ) ((fun (a : σ) ↦ (single a 1 : σ →₀ ℕ)) a) (single a 1)
Tactic: use a
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
M : Type u_2
τ : Type u_5
f : σ → τ
inst : AddCommMonoid M
x : σ →₀ M
⊢ Eq.{u_2 + 1} (α := M) ((degree : (a : τ →₀ M) → M) (mapDomain f x) : M) ((degree : (a : σ →₀ M) → M) x : M)
have simp : Eq.{u_2 + 1} (α := M) (∑ x_1 ∈ x.support, (x : (a : σ) → M) x_1 : M) ((degree : (a : σ →₀ M) → M) x : M)
Tactic: simp [mapDomain, sum]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_5
f : σ →₀ ℕ
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
have 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 : ℕ)
Tactic: obtain ⟨g, hgf, rfl⟩ := IH (by lia)
Cleared hypotheses: n, IH, hn
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
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
⊢ ∃ g_1 ≤ f, (degree : (a : σ →₀ ℕ) → ℕ) g_1 = HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) (1 : ℕ)
have 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 : ℕ)
Tactic: obtain ⟨f, rfl⟩ := le_iff_exists_add.mp hgf
Cleared hypotheses: f, hgf, IH, hn
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
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)
⊢ ∃ g_1 ≤ g + f,
    (degree : (a : σ →₀ ℕ) → ℕ) g_1 = HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) (1 : ℕ)
have succ : ∀ (i : σ) (hi : i ∈ f.support),
  ∃ g_1 ≤ g + f,
    (degree : (a : σ →₀ ℕ) → ℕ) g_1 = HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) (1 : ℕ)
Tactic: obtain ⟨i, hi⟩ : f.support.Nonempty := by aesop
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
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
⊢ single i 1 ≤ f
have simp : LE.le (α := ℕ) (1 : ℕ) ((f : (a : σ) → ℕ) i : ℕ)
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_5
f : σ →₀ ℕ
n : ℕ
hn : n ≤ (degree : (a : σ →₀ ℕ) → ℕ) f
⊢ ∃ g ≤ f, (degree : (a : σ →₀ ℕ) → ℕ) g = n
have zero : ∀ (hn : LE.le (α := ℕ) (0 : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) f : ℕ)),
  ∃ g ≤ f, Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) g : ℕ) (0 : ℕ)
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⟩
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
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 : ℕ)
⊢ ∃ g ≤ f, (degree : (a : σ →₀ ℕ) → ℕ) g = n
have 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
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⟩
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_5
s t : Set ℕ
⊢ (⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' (s + t) =
    HAdd.hAdd (α := Set (σ →₀ ℕ)) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' s) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' t)
have refine : (⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' (s + t) ⊆
  HAdd.hAdd (α := Set (σ →₀ ℕ)) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' s) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' t)
Tactic: refine (Set.preimage_add_preimage_subset ..).antisymm' ?_
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_5
s t : Set ℕ
f : σ →₀ ℕ
m : ℕ
hm : m ∈ s
n : ℕ
hn : n ∈ t
e : m + n = (degree : (a : σ →₀ ℕ) → ℕ) f
⊢ f ∈ HAdd.hAdd (α := Set (σ →₀ ℕ)) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' s) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' t)
have 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)
Tactic: obtain ⟨g, hgf, rfl⟩ := exists_le_degree_eq f m (by grind)
Cleared hypotheses: m, hm, e
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
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
⊢ f ∈ HAdd.hAdd (α := Set (σ →₀ ℕ)) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' s) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' t)
have 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)
Tactic: obtain ⟨f, rfl⟩ := le_iff_exists_add.mp hgf
Cleared hypotheses: f, hgf, e
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_5
s : Set ℕ
n : ℕ
hn : n ≠ 0
⊢ (⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' (n • s) = HSMul.hSMul (β := Set (σ →₀ ℕ)) n ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' s)
have zero : ∀ (hn : Ne (α := ℕ) 0 0),
  (⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' HSMul.hSMul (α := ℕ) 0 s =
    HSMul.hSMul (α := ℕ) (β := Set (σ →₀ ℕ)) 0 ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' s)
Tactic: obtain (_ | n) := n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
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)
⊢ (⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' (n • s) = HSMul.hSMul (β := Set (σ →₀ ℕ)) n ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' s)
have succ : ∀ (n : ℕ) (hn : n + 1 ≠ 0),
  (⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' ((n + 1) • s) =
    HSMul.hSMul (β := Set (σ →₀ ℕ)) (n + 1) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' s)
Tactic: obtain (_ | n) := n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_5
s : Set ℕ
n : ℕ
hn : n + 1 ≠ 0
⊢ (⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' ((n + 1) • s) =
    HSMul.hSMul (β := Set (σ →₀ ℕ)) (n + 1) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' s)
have succ : ∀ (hn : HAdd.hAdd (α := ℕ) 0 1 ≠ 0),
  (⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' (HAdd.hAdd (α := ℕ) 0 1 • s) =
    HSMul.hSMul (β := Set (σ →₀ ℕ)) (HAdd.hAdd (α := ℕ) 0 1) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' s)
Tactic: induction n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
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)
⊢ (⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' ((n + 1) • s) =
    HSMul.hSMul (β := Set (σ →₀ ℕ)) (n + 1) ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' s)
have 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)
Tactic: induction n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
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}
⊢ HSMul.hSMul (β := Set (α →₀ ℕ)) (n + 1) ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n + 1 ∧ (↑x.support : Set α) ⊆ s}
have 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}
Tactic: rw [succ_nsmul, ih]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
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}
have 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}
Tactic: refine subset_antisymm ?_ fun f ⟨f_deg, f_supp⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
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}
⊢ 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}
have 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)
Tactic: refine subset_antisymm ?_ fun f ⟨f_deg, f_supp⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
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}
have 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
Tactic: simp [Set.subset_def, Set.mem_add, @forall_comm (α →₀ ℕ)]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
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 ∈
    HAdd.hAdd (α := Set (α →₀ ℕ)) {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
      ((fun (x : α) ↦ single x 1) '' s)
have 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)
Tactic: obtain ⟨i, hi⟩ : f.support.Nonempty := by aesop