-- 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₄ :
  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 (σ →₀ ℕ))
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)
            (@Finset.antidiagonal _ instAddMonoid _
                ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n)) :
              Finset ((σ →₀ ℕ) × (σ →₀ ℕ)))) :
        Set (σ →₀ ℕ))
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),
    ∃ (x : σ →₀ ℕ), d + x = (Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n)
h :
  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 + HSub.hSub (α := σ →₀ ℕ) ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n) : σ →₀ ℕ) d =
      (Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n)
h₁ :
  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) (x : σ),
    Eq (α := ℕ)
      ((d +
              HSub.hSub (α := σ →₀ ℕ)
                ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n) : σ →₀ ℕ) d :
            (a : σ) → ℕ)
          x :
        ℕ)
      ((((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n) : σ →₀ ℕ) : (a : σ) → ℕ) x : ℕ)
h₂ :
  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 : (weight w : (a : σ →₀ ℕ) → ℕ) d ≤ n) (x : σ),
    Eq (α := ℕ)
      ((d +
              HSub.hSub (α := σ →₀ ℕ)
                ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n) : σ →₀ ℕ) d :
            (a : σ) → ℕ)
          x :
        ℕ)
      ((((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n) : σ →₀ ℕ) : (a : σ) → ℕ) x : ℕ)
⊢ Set.Finite.{u_1} (α := σ →₀ ℕ) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d ≤ n}
have h₃ : 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 : σ →₀ ℕ⦄ (x : σ) (hd : (d : (a : σ) → ℕ) x ≤ n),
  Eq (α := ℕ)
    ((d +
            HSub.hSub (α := σ →₀ ℕ) ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n) : σ →₀ ℕ)
              d :
          (a : σ) → ℕ)
        x :
      ℕ)
    ((((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n) : σ →₀ ℕ) : (a : σ) → ℕ) x : ℕ)
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 [*]