internlm/Lean-Github huggingface dataset:
Theorem: skip_le_succ
Proof state before:
case a
n k j : Nat
hyp : j < n
⊢ j < n
Tactic:
exact hyp
Proof state after:
no goals
Theorem: skip_preimage_lt
Proof state before:
i j k n : Nat
kw : k < n + 1
jw : j < n + 1
eqn : skip k i = j
ineq : i + 1 ≤ skip k i
⊢ i < n
Tactic:
have lem1 : i <  j :=
by
  rw [← eqn]
  exact ineq
Proof state after:
i j k n : Nat
kw : k < n + 1
jw : j < n + 1
eqn : skip k i = j
ineq : i + 1 ≤ skip k i
lem1 : i < j
⊢ i < n
Theorem: skip_preimage_lt
Proof state before:
i j k n : Nat
kw : k < n + 1
jw : j < n + 1
eqn : skip k i = j
ineq : i + 1 ≤ skip k i
lem1 : i < j
⊢ i < n
Tactic:
apply Nat.lt_of_lt_of_le lem1
Proof state after:
i j k n : Nat
kw : k < n + 1
jw : j < n + 1
eqn : skip k i = j
ineq : i + 1 ≤ skip k i
lem1 : i < j
⊢ j ≤ n
Theorem: skip_preimage_lt
Proof state before:
i j k n : Nat
kw : k < n + 1
jw : j < n + 1
eqn : skip k i = j
ineq : i + 1 ≤ skip k i
lem1 : i < j
⊢ j ≤ n
Tactic:
apply Nat.le_of_succ_le_succ
Proof state after:
case a
i j k n : Nat
kw : k < n + 1
jw : j < n + 1
eqn : skip k i = j
ineq : i + 1 ≤ skip k i
lem1 : i < j
⊢ succ j ≤ succ n
Theorem: skip_preimage_lt
Proof state before:
case a
i j k n : Nat
kw : k < n + 1
jw : j < n + 1
eqn : skip k i = j
ineq : i + 1 ≤ skip k i
lem1 : i < j
⊢ succ j ≤ succ n
Tactic:
apply jw
Proof state after:
no goals
Theorem: skip_preimage_lt
Proof state before:
i j k n : Nat
kw : k < n + 1
jw : j < n + 1
eqn : skip k i = j
ineq : i + 1 ≤ skip k i
⊢ i < j
Tactic:
rw [← eqn]
Proof state after:
i j k n : Nat
kw : k < n + 1
jw : j < n + 1
eqn : skip k i = j
ineq : i + 1 ≤ skip k i
⊢ i < skip k i
Theorem: skip_preimage_lt
Proof state before:
i j k n : Nat
kw : k < n + 1
jw : j < n + 1
eqn : skip k i = j
ineq : i + 1 ≤ skip k i
⊢ i < skip k i
Tactic:
exact ineq
Proof state after:
no goals
Theorem: skip_preimage_lt
Proof state before:
i j k n : Nat
kw : k < n + 1
jw : j < n + 1
eqn : skip k i = j
ineqn : i < k
⊢ i < n
Tactic:
apply Nat.lt_of_lt_of_le ineqn
Proof state after:
i j k n : Nat
kw : k < n + 1
jw : j < n + 1
eqn : skip k i = j
ineqn : i < k
⊢ k ≤ n
Theorem: skip_preimage_lt
Proof state before:
i j k n : Nat
kw : k < n + 1
jw : j < n + 1
eqn : skip k i = j
ineqn : i < k
⊢ k ≤ n
Tactic:
apply Nat.le_of_succ_le_succ
Proof state after:
case a
i j k n : Nat
kw : k < n + 1
jw : j < n + 1
eqn : skip k i = j
ineqn : i < k
⊢ succ k ≤ succ n
Theorem: skip_preimage_lt
Proof state before:
case a
i j k n : Nat
kw : k < n + 1
jw : j < n + 1
eqn : skip k i = j
ineqn : i < k
⊢ succ k ≤ succ n
Tactic:
apply kw
Proof state after:
no goals
Theorem: skip_injective
Proof state before:
n j1 j2 : Nat
hyp : skip n j1 = skip n j2
p1 : j1 < n
eq1 : skip n j1 = j1 := skip_below_eq p1
p2 : j2 < n
eq2 : skip n j2 = j2 := skip_below_eq p2
⊢ j1 = j2
Tactic:
rw [← eq1]
Proof state after:
n j1 j2 : Nat
hyp : skip n j1 = skip n j2
p1 : j1 < n
eq1 : skip n j1 = j1 := skip_below_eq p1
p2 : j2 < n
eq2 : skip n j2 = j2 := skip_below_eq p2
⊢ skip n j1 = j2
Theorem: skip_injective
Proof state before:
n j1 j2 : Nat
hyp : skip n j1 = skip n j2
p1 : j1 < n
eq1 : skip n j1 = j1 := skip_below_eq p1
p2 : j2 < n
eq2 : skip n j2 = j2 := skip_below_eq p2
⊢ skip n j1 = j2
Tactic:
rw [← eq2]
Proof state after:
n j1 j2 : Nat
hyp : skip n j1 = skip n j2
p1 : j1 < n
eq1 : skip n j1 = j1 := skip_below_eq p1
p2 : j2 < n
eq2 : skip n j2 = j2 := skip_below_eq p2
⊢ skip n j1 = skip n j2
Theorem: skip_injective
Proof state before:
n j1 j2 : Nat
hyp : skip n j1 = skip n j2
p1 : j1 < n
eq1 : skip n j1 = j1 := skip_below_eq p1
p2 : j2 < n
eq2 : skip n j2 = j2 := skip_below_eq p2
⊢ skip n j1 = skip n j2
Tactic:
exact hyp
Proof state after:
no goals
Theorem: skip_injective
Proof state before:
n j1 j2 : Nat
hyp : skip n j1 = skip n j2
p1 : j1 ≥ n
eq1 : skip n j1 = succ j1 := skip_above_eq n j1 p1
p2 : j2 ≥ n
eq2 : skip n j2 = succ j2 := skip_above_eq n j2 p2
⊢ succ j1 = succ j2
Tactic:
rw [← eq1]
Proof state after:
n j1 j2 : Nat
hyp : skip n j1 = skip n j2
p1 : j1 ≥ n
eq1 : skip n j1 = succ j1 := skip_above_eq n j1 p1
p2 : j2 ≥ n
eq2 : skip n j2 = succ j2 := skip_above_eq n j2 p2
⊢ skip n j1 = succ j2
Theorem: skip_injective
Proof state before:
n j1 j2 : Nat
hyp : skip n j1 = skip n j2
p1 : j1 ≥ n
eq1 : skip n j1 = succ j1 := skip_above_eq n j1 p1
p2 : j2 ≥ n
eq2 : skip n j2 = succ j2 := skip_above_eq n j2 p2
⊢ skip n j1 = succ j2
Tactic:
rw [← eq2]
Proof state after:
n j1 j2 : Nat
hyp : skip n j1 = skip n j2
p1 : j1 ≥ n
eq1 : skip n j1 = succ j1 := skip_above_eq n j1 p1
p2 : j2 ≥ n
eq2 : skip n j2 = succ j2 := skip_above_eq n j2 p2
⊢ skip n j1 = skip n j2
Theorem: skip_injective
Proof state before:
n j1 j2 : Nat
hyp : skip n j1 = skip n j2
p1 : j1 ≥ n
eq1 : skip n j1 = succ j1 := skip_above_eq n j1 p1
p2 : j2 ≥ n
eq2 : skip n j2 = succ j2 := skip_above_eq n j2 p2
⊢ skip n j1 = skip n j2
Tactic:
exact hyp
Proof state after:
no goals
Theorem: skip_injective
Proof state before:
n j1 j2 : Nat
hyp : skip n j1 = skip n j2
p1 : j1 ≥ n
eq1 : skip n j1 = succ j1 := skip_above_eq n j1 p1
p2 : j2 ≥ n
eq2 : skip n j2 = succ j2 := skip_above_eq n j2 p2
eq3 : succ j1 = succ j2 :=
  Eq.mpr (id (congrArg (fun _a => _a = succ j2) (Eq.symm eq1)))
    (Eq.mpr (id (congrArg (fun _a => skip n j1 = _a) (Eq.symm eq2))) hyp)
⊢ j1 = j2
Tactic:
injection eq3
Proof state after:
no goals
Theorem: skip_no_fixedpoints
Proof state before:
k j : Nat
c : j < k
eqn : skip k j = j := skip_below_eq c
hyp : skip k j = k
⊢ k ≤ j
Tactic:
rw [←hyp]
Proof state after:
k j : Nat
c : j < k
eqn : skip k j = j := skip_below_eq c
hyp : skip k j = k
⊢ skip k j ≤ j
Theorem: skip_no_fixedpoints
Proof state before:
k j : Nat
c : j < k
eqn : skip k j = j := skip_below_eq c
hyp : skip k j = k
⊢ skip k j ≤ j
Tactic:
rw [eqn]
Proof state after:
k j : Nat
c : j < k
eqn : skip k j = j := skip_below_eq c
hyp : skip k j = k
⊢ j ≤ j
Theorem: skip_no_fixedpoints
Proof state before:
k j : Nat
c : j < k
eqn : skip k j = j := skip_below_eq c
hyp : skip k j = k
⊢ j ≤ j
Tactic:
apply Nat.le_refl
Proof state after:
no goals
Theorem: skip_no_fixedpoints
Proof state before:
k j : Nat
c : ¬j < k
eqn : skip k j = j + 1 := skip_not_below_eq k j c
hyp : skip k j = k
⊢ j + 1 = k
Tactic:
rw [←hyp]
Proof state after:
k j : Nat
c : ¬j < k
eqn : skip k j = j + 1 := skip_not_below_eq k j c
hyp : skip k j = k
⊢ j + 1 = skip k j
Theorem: skip_no_fixedpoints
Proof state before:
k j : Nat
c : ¬j < k
eqn : skip k j = j + 1 := skip_not_below_eq k j c
hyp : skip k j = k
⊢ j + 1 = skip k j
Tactic:
rw [eqn]
Proof state after:
no goals
Theorem: skip_no_fixedpoints
Proof state before:
k j : Nat
c : ¬j < k
eqn : skip k j = j + 1 := skip_not_below_eq k j c
hyp : skip k j = k
lemEq : j + 1 = k :=
  Eq.mpr (id (congrArg (fun _a => j + 1 = _a) (Eq.symm hyp)))
    (Eq.mpr (id (congrArg (fun _a => j + 1 = _a) eqn)) (Eq.refl (j + 1)))
⊢ j < k
Tactic:
rw [←lemEq]
Proof state after:
k j : Nat
c : ¬j < k
eqn : skip k j = j + 1 := skip_not_below_eq k j c
hyp : skip k j = k
lemEq : j + 1 = k :=
  Eq.mpr (id (congrArg (fun _a => j + 1 = _a) (Eq.symm hyp)))
    (Eq.mpr (id (congrArg (fun _a => j + 1 = _a) eqn)) (Eq.refl (j + 1)))
⊢ j < j + 1
Theorem: skip_no_fixedpoints
Proof state before:
k j : Nat
c : ¬j < k
eqn : skip k j = j + 1 := skip_not_below_eq k j c
hyp : skip k j = k
lemEq : j + 1 = k :=
  Eq.mpr (id (congrArg (fun _a => j + 1 = _a) (Eq.symm hyp)))
    (Eq.mpr (id (congrArg (fun _a => j + 1 = _a) eqn)) (Eq.refl (j + 1)))
⊢ j < j + 1
Tactic:
apply Nat.lt_succ_self
Proof state after:
no goals
Theorem: MvPowerSeries.exists_coeff_ne_zero_iff_ne_zero
Proof state before:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
f : MvPowerSeries σ α
⊢ (∃ d, (coeff α d) f ≠ 0) ↔ f ≠ 0
Tactic:
simp only [ext_iff, ne_eq, coeff_zero, not_forall]
Proof state after:
no goals
Theorem: MvPowerSeries.weight_apply
Proof state before:
σ : Type u_1
α : Type ?u.2439
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ (weight w) d = d.sum fun x => Mul.mul (w x)
Tactic:
simp only [weight]
Proof state after:
σ : Type u_1
α : Type ?u.2439
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ { toFun := fun d => d.sum fun x y => w x * y, map_zero' := ⋯, map_add' := ⋯ } d = d.sum fun x => Mul.mul (w x)
Theorem: MvPowerSeries.weight_apply
Proof state before:
σ : Type u_1
α : Type ?u.2439
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ { toFun := fun d => d.sum fun x y => w x * y, map_zero' := ⋯, map_add' := ⋯ } d = d.sum fun x => Mul.mul (w x)
Tactic:
rfl
Proof state after:
no goals
Theorem: MvPowerSeries.le_weight
Proof state before:
σ : Type u_1
α : Type ?u.2913
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
x : σ
hx : w x ≠ 0
d : σ →₀ ℕ
⊢ d x ≤ (weight w) d
Tactic:
simp only [weight_apply, Finsupp.sum]
Proof state after:
σ : Type u_1
α : Type ?u.2913
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
x : σ
hx : w x ≠ 0
d : σ →₀ ℕ
⊢ d x ≤ ∑ x ∈ d.support, Mul.mul (w x) (d x)
Theorem: MvPowerSeries.le_weight
Proof state before:
σ : Type u_1
α : Type ?u.2913
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
x : σ
hx : w x ≠ 0
d : σ →₀ ℕ
⊢ d x ≤ ∑ x ∈ d.support, Mul.mul (w x) (d x)
Tactic:
by_cases hxd : x ∈ d.support
Proof state after:
case pos
σ : Type u_1
α : Type ?u.2913
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
x : σ
hx : w x ≠ 0
d : σ →₀ ℕ
hxd : x ∈ d.support
⊢ d x ≤ ∑ x ∈ d.support, Mul.mul (w x) (d x)

case neg
σ : Type u_1
α : Type ?u.2913
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
x : σ
hx : w x ≠ 0
d : σ →₀ ℕ
hxd : x ∉ d.support
⊢ d x ≤ ∑ x ∈ d.support, Mul.mul (w x) (d x)
Theorem: MvPowerSeries.le_weight
Proof state before:
case neg
σ : Type u_1
α : Type ?u.2913
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
x : σ
hx : w x ≠ 0
d : σ →₀ ℕ
hxd : x ∉ d.support
⊢ d x ≤ ∑ x ∈ d.support, Mul.mul (w x) (d x)
Tactic:
simp only [Finsupp.mem_support_iff, Classical.not_not] at hxd
Proof state after:
case neg
σ : Type u_1
α : Type ?u.2913
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
x : σ
hx : w x ≠ 0
d : σ →₀ ℕ
hxd : d x = 0
⊢ d x ≤ ∑ x ∈ d.support, Mul.mul (w x) (d x)
Theorem: MvPowerSeries.le_weight
Proof state before:
case neg
σ : Type u_1
α : Type ?u.2913
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
x : σ
hx : w x ≠ 0
d : σ →₀ ℕ
hxd : d x = 0
⊢ d x ≤ ∑ x ∈ d.support, Mul.mul (w x) (d x)
Tactic:
rw [hxd]
Proof state after:
case neg
σ : Type u_1
α : Type ?u.2913
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
x : σ
hx : w x ≠ 0
d : σ →₀ ℕ
hxd : d x = 0
⊢ 0 ≤ ∑ x ∈ d.support, Mul.mul (w x) (d x)
Theorem: MvPowerSeries.le_weight
Proof state before:
case neg
σ : Type u_1
α : Type ?u.2913
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
x : σ
hx : w x ≠ 0
d : σ →₀ ℕ
hxd : d x = 0
⊢ 0 ≤ ∑ x ∈ d.support, Mul.mul (w x) (d x)
Tactic:
apply zero_le
Proof state after:
no goals
Theorem: MvPowerSeries.le_weight
Proof state before:
case pos
σ : Type u_1
α : Type ?u.2913
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
x : σ
hx : w x ≠ 0
d : σ →₀ ℕ
hxd : x ∈ d.support
⊢ d x ≤ ∑ x ∈ d.support, Mul.mul (w x) (d x)
Tactic:
rw [Finset.sum_eq_add_sum_diff_singleton hxd]
Proof state after:
case pos
σ : Type u_1
α : Type ?u.2913
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
x : σ
hx : w x ≠ 0
d : σ →₀ ℕ
hxd : x ∈ d.support
⊢ d x ≤ Mul.mul (w x) (d x) + ∑ x ∈ d.support \ {x}, Mul.mul (w x) (d x)
Theorem: MvPowerSeries.le_weight
Proof state before:
case pos
σ : Type u_1
α : Type ?u.2913
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
x : σ
hx : w x ≠ 0
d : σ →₀ ℕ
hxd : x ∈ d.support
⊢ d x ≤ Mul.mul (w x) (d x) + ∑ x ∈ d.support \ {x}, Mul.mul (w x) (d x)
Tactic:
refine' le_trans _ (Nat.le_add_right _ _)
Proof state after:
case pos
σ : Type u_1
α : Type ?u.2913
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
x : σ
hx : w x ≠ 0
d : σ →₀ ℕ
hxd : x ∈ d.support
⊢ d x ≤ Mul.mul (w x) (d x)
Theorem: MvPowerSeries.le_weight
Proof state before:
case pos
σ : Type u_1
α : Type ?u.2913
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
x : σ
hx : w x ≠ 0
d : σ →₀ ℕ
hxd : x ∈ d.support
⊢ d x ≤ Mul.mul (w x) (d x)
Tactic:
exact Nat.le_mul_of_pos_left _ (Nat.pos_of_ne_zero hx)
Proof state after:
no goals
Theorem: MvPowerSeries.finite_of_weight_le
Proof 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
Proof state after:
no goals
Theorem: MvPowerSeries.finite_of_weight_le
Proof 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
Proof 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
Theorem: MvPowerSeries.finite_of_weight_le
Proof 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
Proof 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)
Theorem: MvPowerSeries.finite_of_weight_le
Proof 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
Proof 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)
Theorem: MvPowerSeries.finite_of_weight_le
Proof 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]
Proof 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))))
Theorem: MvPowerSeries.finite_of_weight_le
Proof 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]
Proof 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)
Theorem: MvPowerSeries.finite_of_weight_le
Proof 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
Proof 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)
Theorem: MvPowerSeries.finite_of_weight_le
Proof 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
Proof 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
Theorem: MvPowerSeries.finite_of_weight_le
Proof 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]
Proof 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
Theorem: MvPowerSeries.finite_of_weight_le
Proof 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]
Proof 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
Theorem: MvPowerSeries.finite_of_weight_le
Proof 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
Proof 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
Theorem: MvPowerSeries.finite_of_weight_le
Proof 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)
Proof 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
Theorem: MvPowerSeries.finite_of_weight_le
Proof 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
Proof state after:
no goals