Theorem: MvPowerSeries.finite_of_weight_le (DividedPowers/ForMathlib/MvPowerSeries/Order.lean)

State before:
σ : Type u_1
α : Type ?u.4528
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
inst✝ : Finite σ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
⊢ {f | (weight w) f ≤ n}.Finite
Tactic:
classical
set fg := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n)) with hfg
suffices {f : σ →₀ ℕ | weight w f ≤ n} ⊆ ↑(fg.image fun uv => uv.fst) by
  apply Set.Finite.subset _ this
  apply Finset.finite_toSet
intro f hf
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) - f
ext x
simp only [Finsupp.coe_add, Finsupp.coe_tsub, Pi.add_apply, Pi.sub_apply,
  Finsupp.equivFunOnFinite_symm_apply_toFun, Function.const_apply]
rw [add_comm]
apply Nat.sub_add_cancel
apply le_trans (le_weight w x (hw x) f)
simpa only [Set.mem_setOf_eq] using hf
State after:
no goals

State before:
σ : Type u_1
α : Type ?u.4528
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
inst✝ : Finite σ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
⊢ {f | (weight w) f ≤ n}.Finite
Tactic:
set fg := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n)) with hfg
State after:
σ : Type u_1
α : Type ?u.4528
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
inst✝ : Finite σ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
⊢ {f | (weight w) f ≤ n}.Finite

State before:
σ : Type u_1
α : Type ?u.4528
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
inst✝ : Finite σ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
⊢ {f | (weight w) f ≤ n}.Finite
Tactic:
suffices {f : σ →₀ ℕ | weight w f ≤ n} ⊆ ↑(fg.image fun uv => uv.fst) by
  apply Set.Finite.subset _ this
  apply Finset.finite_toSet
State after:
σ : Type u_1
α : Type ?u.4528
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
inst✝ : Finite σ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
⊢ {f | (weight w) f ≤ n} ⊆ ↑(Finset.image (fun uv => uv.1) fg)

State before:
σ : Type u_1
α : Type ?u.4528
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
inst✝ : Finite σ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
⊢ {f | (weight w) f ≤ n} ⊆ ↑(Finset.image (fun uv => uv.1) fg)
Tactic:
intro f hf
State after:
σ : Type u_1
α : Type ?u.4528
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : Finite σ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
f : σ →₀ ℕ
hf : f ∈ {f | (weight w) f ≤ n}
⊢ f ∈ ↑(Finset.image (fun uv => uv.1) fg)

State before:
σ : Type u_1
α : Type ?u.4528
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : Finite σ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
f : σ →₀ ℕ
hf : f ∈ {f | (weight w) f ≤ n}
⊢ f ∈ ↑(Finset.image (fun uv => uv.1) fg)
Tactic:
rw [hfg]
State after:
σ : Type u_1
α : Type ?u.4528
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : Finite σ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
f : σ →₀ ℕ
hf : f ∈ {f | (weight w) f ≤ n}
⊢ f ∈ ↑(Finset.image (fun uv => uv.1) (Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))))

State before:
σ : Type u_1
α : Type ?u.4528
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : Finite σ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
f : σ →₀ ℕ
hf : f ∈ {f | (weight w) f ≤ n}
⊢ f ∈ ↑(Finset.image (fun uv => uv.1) (Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))))
Tactic:
simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe,
  Finset.mem_antidiagonal, Prod.exists, exists_and_right, exists_eq_right]
State after:
σ : Type u_1
α : Type ?u.4528
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : Finite σ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
f : σ →₀ ℕ
hf : f ∈ {f | (weight w) f ≤ n}
⊢ ∃ x, f + x = Finsupp.equivFunOnFinite.symm (Function.const σ n)

State before:
σ : Type u_1
α : Type ?u.4528
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : Finite σ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
f : σ →₀ ℕ
hf : f ∈ {f | (weight w) f ≤ n}
⊢ ∃ x, f + x = Finsupp.equivFunOnFinite.symm (Function.const σ n)
Tactic:
use Finsupp.equivFunOnFinite.symm (Function.const σ n) - f
State after:
case h
σ : Type u_1
α : Type ?u.4528
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : Finite σ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
f : σ →₀ ℕ
hf : f ∈ {f | (weight w) f ≤ n}
⊢ f + (Finsupp.equivFunOnFinite.symm (Function.const σ n) - f) = Finsupp.equivFunOnFinite.symm (Function.const σ n)

State before:
case h
σ : Type u_1
α : Type ?u.4528
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : Finite σ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
f : σ →₀ ℕ
hf : f ∈ {f | (weight w) f ≤ n}
⊢ f + (Finsupp.equivFunOnFinite.symm (Function.const σ n) - f) = Finsupp.equivFunOnFinite.symm (Function.const σ n)
Tactic:
ext x
State after:
case h.h
σ : Type u_1
α : Type ?u.4528
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : Finite σ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
f : σ →₀ ℕ
hf : f ∈ {f | (weight w) f ≤ n}
x : σ
⊢ (f + (Finsupp.equivFunOnFinite.symm (Function.const σ n) - f)) x =
    (Finsupp.equivFunOnFinite.symm (Function.const σ n)) x

State before:
case h.h
σ : Type u_1
α : Type ?u.4528
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : Finite σ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
f : σ →₀ ℕ
hf : f ∈ {f | (weight w) f ≤ n}
x : σ
⊢ (f + (Finsupp.equivFunOnFinite.symm (Function.const σ n) - f)) x =
    (Finsupp.equivFunOnFinite.symm (Function.const σ n)) x
Tactic:
simp only [Finsupp.coe_add, Finsupp.coe_tsub, Pi.add_apply, Pi.sub_apply,
  Finsupp.equivFunOnFinite_symm_apply_toFun, Function.const_apply]
State after:
case h.h
σ : Type u_1
α : Type ?u.4528
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : Finite σ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
f : σ →₀ ℕ
hf : f ∈ {f | (weight w) f ≤ n}
x : σ
⊢ f x + (n - f x) = n

State before:
case h.h
σ : Type u_1
α : Type ?u.4528
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : Finite σ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
f : σ →₀ ℕ
hf : f ∈ {f | (weight w) f ≤ n}
x : σ
⊢ f x + (n - f x) = n
Tactic:
rw [add_comm]
State after:
case h.h
σ : Type u_1
α : Type ?u.4528
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : Finite σ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
f : σ →₀ ℕ
hf : f ∈ {f | (weight w) f ≤ n}
x : σ
⊢ n - f x + f x = n

State before:
case h.h
σ : Type u_1
α : Type ?u.4528
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : Finite σ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
f : σ →₀ ℕ
hf : f ∈ {f | (weight w) f ≤ n}
x : σ
⊢ n - f x + f x = n
Tactic:
apply Nat.sub_add_cancel
State after:
case h.h.h
σ : Type u_1
α : Type ?u.4528
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : Finite σ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
f : σ →₀ ℕ
hf : f ∈ {f | (weight w) f ≤ n}
x : σ
⊢ f x ≤ n

State before:
case h.h.h
σ : Type u_1
α : Type ?u.4528
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : Finite σ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
f : σ →₀ ℕ
hf : f ∈ {f | (weight w) f ≤ n}
x : σ
⊢ f x ≤ n
Tactic:
apply le_trans (le_weight w x (hw x) f)
State after:
case h.h.h
σ : Type u_1
α : Type ?u.4528
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : Finite σ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
f : σ →₀ ℕ
hf : f ∈ {f | (weight w) f ≤ n}
x : σ
⊢ (weight w) f ≤ n

State before:
case h.h.h
σ : Type u_1
α : Type ?u.4528
inst✝¹ : Semiring α
w : σ → ℕ
f✝ : MvPowerSeries σ α
inst✝ : Finite σ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
f : σ →₀ ℕ
hf : f ∈ {f | (weight w) f ≤ n}
x : σ
⊢ (weight w) f ≤ n
Tactic:
simpa only [Set.mem_setOf_eq] using hf
State after:
no goals

State before:
σ : Type u_1
α : Type ?u.4528
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
inst✝ : Finite σ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
this : {f | (weight w) f ≤ n} ⊆ ↑(Finset.image (fun uv => uv.1) fg)
⊢ {f | (weight w) f ≤ n}.Finite
Tactic:
apply Set.Finite.subset _ this
State after:
σ : Type u_1
α : Type ?u.4528
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
inst✝ : Finite σ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
this : {f | (weight w) f ≤ n} ⊆ ↑(Finset.image (fun uv => uv.1) fg)
⊢ (↑(Finset.image (fun uv => uv.1) fg)).Finite

State before:
σ : Type u_1
α : Type ?u.4528
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
inst✝ : Finite σ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n))
this : {f | (weight w) f ≤ n} ⊆ ↑(Finset.image (fun uv => uv.1) fg)
⊢ (↑(Finset.image (fun uv => uv.1) fg)).Finite
Tactic:
apply Finset.finite_toSet
State after:
no goals