internlm/Lean-Github huggingface dataset:
Theorem: MvPowerSeries.StronglySummable.hasProd_of_one_add
Proof state before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
hf : StronglySummable f
this : UniformAddGroup (MvPowerSeries σ α)
V : Set (MvPowerSeries σ α)
hV : V ∈ nhds ⋯.prod
V₀ : Set (MvPowerSeries σ α) := Add.add ⋯.prod ⁻¹' V
hV'₀ : V = Add.add (-⋯.prod) ⁻¹' V₀
⊢ V₀ ∈ nhds 0
Tactic:
apply continuousAt_def.mp (Continuous.continuousAt (continuous_add_left _))
Proof state after:
case a
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
hf : StronglySummable f
this : UniformAddGroup (MvPowerSeries σ α)
V : Set (MvPowerSeries σ α)
hV : V ∈ nhds ⋯.prod
V₀ : Set (MvPowerSeries σ α) := Add.add ⋯.prod ⁻¹' V
hV'₀ : V = Add.add (-⋯.prod) ⁻¹' V₀
⊢ V ∈ nhds (⋯.prod + 0)
Theorem: MvPowerSeries.StronglySummable.hasProd_of_one_add
Proof state before:
case a
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
hf : StronglySummable f
this : UniformAddGroup (MvPowerSeries σ α)
V : Set (MvPowerSeries σ α)
hV : V ∈ nhds ⋯.prod
V₀ : Set (MvPowerSeries σ α) := Add.add ⋯.prod ⁻¹' V
hV'₀ : V = Add.add (-⋯.prod) ⁻¹' V₀
⊢ V ∈ nhds (⋯.prod + 0)
Tactic:
rw [add_zero]
Proof state after:
case a
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
hf : StronglySummable f
this : UniformAddGroup (MvPowerSeries σ α)
V : Set (MvPowerSeries σ α)
hV : V ∈ nhds ⋯.prod
V₀ : Set (MvPowerSeries σ α) := Add.add ⋯.prod ⁻¹' V
hV'₀ : V = Add.add (-⋯.prod) ⁻¹' V₀
⊢ V ∈ nhds ⋯.prod
Theorem: MvPowerSeries.StronglySummable.hasProd_of_one_add
Proof state before:
case a
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
hf : StronglySummable f
this : UniformAddGroup (MvPowerSeries σ α)
V : Set (MvPowerSeries σ α)
hV : V ∈ nhds ⋯.prod
V₀ : Set (MvPowerSeries σ α) := Add.add ⋯.prod ⁻¹' V
hV'₀ : V = Add.add (-⋯.prod) ⁻¹' V₀
⊢ V ∈ nhds ⋯.prod
Tactic:
exact hV
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.hasProd_of_one_add
Proof state before:
case h.e'_4
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
hf : StronglySummable f
this : UniformAddGroup (MvPowerSeries σ α)
V : Set (MvPowerSeries σ α)
hV : V ∈ nhds ⋯.prod
V₀ : Set (MvPowerSeries σ α) := Add.add ⋯.prod ⁻¹' V
hV'₀ : V = Add.add (-⋯.prod) ⁻¹' V₀
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
htV₀ : D.pi t ⊆ V₀
J : Finset ι
hIJ : hf.unionOfSupportOfCoeffLe (hD.toFinset.sup id) ⊆ J
d : σ →₀ ℕ
hd : d ∈ D
⊢ hf.unionOfSupportOfCoeffLe d ⊆ J
Tactic:
intro i hi
Proof state after:
case h.e'_4
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
hf : StronglySummable f
this : UniformAddGroup (MvPowerSeries σ α)
V : Set (MvPowerSeries σ α)
hV : V ∈ nhds ⋯.prod
V₀ : Set (MvPowerSeries σ α) := Add.add ⋯.prod ⁻¹' V
hV'₀ : V = Add.add (-⋯.prod) ⁻¹' V₀
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
htV₀ : D.pi t ⊆ V₀
J : Finset ι
hIJ : hf.unionOfSupportOfCoeffLe (hD.toFinset.sup id) ⊆ J
d : σ →₀ ℕ
hd : d ∈ D
i : ι
hi : i ∈ hf.unionOfSupportOfCoeffLe d
⊢ i ∈ J
Theorem: MvPowerSeries.StronglySummable.hasProd_of_one_add
Proof state before:
case h.e'_4
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
hf : StronglySummable f
this : UniformAddGroup (MvPowerSeries σ α)
V : Set (MvPowerSeries σ α)
hV : V ∈ nhds ⋯.prod
V₀ : Set (MvPowerSeries σ α) := Add.add ⋯.prod ⁻¹' V
hV'₀ : V = Add.add (-⋯.prod) ⁻¹' V₀
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
htV₀ : D.pi t ⊆ V₀
J : Finset ι
hIJ : hf.unionOfSupportOfCoeffLe (hD.toFinset.sup id) ⊆ J
d : σ →₀ ℕ
hd : d ∈ D
i : ι
hi : i ∈ hf.unionOfSupportOfCoeffLe d
⊢ i ∈ J
Tactic:
apply hIJ
Proof state after:
case h.e'_4.a
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
hf : StronglySummable f
this : UniformAddGroup (MvPowerSeries σ α)
V : Set (MvPowerSeries σ α)
hV : V ∈ nhds ⋯.prod
V₀ : Set (MvPowerSeries σ α) := Add.add ⋯.prod ⁻¹' V
hV'₀ : V = Add.add (-⋯.prod) ⁻¹' V₀
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
htV₀ : D.pi t ⊆ V₀
J : Finset ι
hIJ : hf.unionOfSupportOfCoeffLe (hD.toFinset.sup id) ⊆ J
d : σ →₀ ℕ
hd : d ∈ D
i : ι
hi : i ∈ hf.unionOfSupportOfCoeffLe d
⊢ i ∈ hf.unionOfSupportOfCoeffLe (hD.toFinset.sup id)
Theorem: MvPowerSeries.StronglySummable.hasProd_of_one_add
Proof state before:
case h.e'_4.a
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
hf : StronglySummable f
this : UniformAddGroup (MvPowerSeries σ α)
V : Set (MvPowerSeries σ α)
hV : V ∈ nhds ⋯.prod
V₀ : Set (MvPowerSeries σ α) := Add.add ⋯.prod ⁻¹' V
hV'₀ : V = Add.add (-⋯.prod) ⁻¹' V₀
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
htV₀ : D.pi t ⊆ V₀
J : Finset ι
hIJ : hf.unionOfSupportOfCoeffLe (hD.toFinset.sup id) ⊆ J
d : σ →₀ ℕ
hd : d ∈ D
i : ι
hi : i ∈ hf.unionOfSupportOfCoeffLe d
⊢ i ∈ hf.unionOfSupportOfCoeffLe (hD.toFinset.sup id)
Tactic:
revert hi
Proof state after:
case h.e'_4.a
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
hf : StronglySummable f
this : UniformAddGroup (MvPowerSeries σ α)
V : Set (MvPowerSeries σ α)
hV : V ∈ nhds ⋯.prod
V₀ : Set (MvPowerSeries σ α) := Add.add ⋯.prod ⁻¹' V
hV'₀ : V = Add.add (-⋯.prod) ⁻¹' V₀
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
htV₀ : D.pi t ⊆ V₀
J : Finset ι
hIJ : hf.unionOfSupportOfCoeffLe (hD.toFinset.sup id) ⊆ J
d : σ →₀ ℕ
hd : d ∈ D
i : ι
⊢ i ∈ hf.unionOfSupportOfCoeffLe d → i ∈ hf.unionOfSupportOfCoeffLe (hD.toFinset.sup id)
Theorem: MvPowerSeries.StronglySummable.hasProd_of_one_add
Proof state before:
case h.e'_4.a
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
hf : StronglySummable f
this : UniformAddGroup (MvPowerSeries σ α)
V : Set (MvPowerSeries σ α)
hV : V ∈ nhds ⋯.prod
V₀ : Set (MvPowerSeries σ α) := Add.add ⋯.prod ⁻¹' V
hV'₀ : V = Add.add (-⋯.prod) ⁻¹' V₀
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
htV₀ : D.pi t ⊆ V₀
J : Finset ι
hIJ : hf.unionOfSupportOfCoeffLe (hD.toFinset.sup id) ⊆ J
d : σ →₀ ℕ
hd : d ∈ D
i : ι
⊢ i ∈ hf.unionOfSupportOfCoeffLe d → i ∈ hf.unionOfSupportOfCoeffLe (hD.toFinset.sup id)
Tactic:
contrapose
Proof state after:
case h.e'_4.a
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
hf : StronglySummable f
this : UniformAddGroup (MvPowerSeries σ α)
V : Set (MvPowerSeries σ α)
hV : V ∈ nhds ⋯.prod
V₀ : Set (MvPowerSeries σ α) := Add.add ⋯.prod ⁻¹' V
hV'₀ : V = Add.add (-⋯.prod) ⁻¹' V₀
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
htV₀ : D.pi t ⊆ V₀
J : Finset ι
hIJ : hf.unionOfSupportOfCoeffLe (hD.toFinset.sup id) ⊆ J
d : σ →₀ ℕ
hd : d ∈ D
i : ι
⊢ i ∉ hf.unionOfSupportOfCoeffLe (hD.toFinset.sup id) → i ∉ hf.unionOfSupportOfCoeffLe d
Theorem: MvPowerSeries.StronglySummable.hasProd_of_one_add
Proof state before:
case h.e'_4.a
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
hf : StronglySummable f
this : UniformAddGroup (MvPowerSeries σ α)
V : Set (MvPowerSeries σ α)
hV : V ∈ nhds ⋯.prod
V₀ : Set (MvPowerSeries σ α) := Add.add ⋯.prod ⁻¹' V
hV'₀ : V = Add.add (-⋯.prod) ⁻¹' V₀
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
htV₀ : D.pi t ⊆ V₀
J : Finset ι
hIJ : hf.unionOfSupportOfCoeffLe (hD.toFinset.sup id) ⊆ J
d : σ →₀ ℕ
hd : d ∈ D
i : ι
⊢ i ∉ hf.unionOfSupportOfCoeffLe (hD.toFinset.sup id) → i ∉ hf.unionOfSupportOfCoeffLe d
Tactic:
simp only [StronglySummable.not_mem_unionOfSupportOfCoeffLe_iff]
Proof state after:
case h.e'_4.a
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
hf : StronglySummable f
this : UniformAddGroup (MvPowerSeries σ α)
V : Set (MvPowerSeries σ α)
hV : V ∈ nhds ⋯.prod
V₀ : Set (MvPowerSeries σ α) := Add.add ⋯.prod ⁻¹' V
hV'₀ : V = Add.add (-⋯.prod) ⁻¹' V₀
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
htV₀ : D.pi t ⊆ V₀
J : Finset ι
hIJ : hf.unionOfSupportOfCoeffLe (hD.toFinset.sup id) ⊆ J
d : σ →₀ ℕ
hd : d ∈ D
i : ι
⊢ (∀ e ≤ hD.toFinset.sup id, (coeff α e) (f i) = 0) → ∀ e ≤ d, (coeff α e) (f i) = 0
Theorem: MvPowerSeries.StronglySummable.hasProd_of_one_add
Proof state before:
case h.e'_4.a
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
hf : StronglySummable f
this : UniformAddGroup (MvPowerSeries σ α)
V : Set (MvPowerSeries σ α)
hV : V ∈ nhds ⋯.prod
V₀ : Set (MvPowerSeries σ α) := Add.add ⋯.prod ⁻¹' V
hV'₀ : V = Add.add (-⋯.prod) ⁻¹' V₀
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
htV₀ : D.pi t ⊆ V₀
J : Finset ι
hIJ : hf.unionOfSupportOfCoeffLe (hD.toFinset.sup id) ⊆ J
d : σ →₀ ℕ
hd : d ∈ D
i : ι
⊢ (∀ e ≤ hD.toFinset.sup id, (coeff α e) (f i) = 0) → ∀ e ≤ d, (coeff α e) (f i) = 0
Tactic:
intro h e hed
Proof state after:
case h.e'_4.a
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
hf : StronglySummable f
this : UniformAddGroup (MvPowerSeries σ α)
V : Set (MvPowerSeries σ α)
hV : V ∈ nhds ⋯.prod
V₀ : Set (MvPowerSeries σ α) := Add.add ⋯.prod ⁻¹' V
hV'₀ : V = Add.add (-⋯.prod) ⁻¹' V₀
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
htV₀ : D.pi t ⊆ V₀
J : Finset ι
hIJ : hf.unionOfSupportOfCoeffLe (hD.toFinset.sup id) ⊆ J
d : σ →₀ ℕ
hd : d ∈ D
i : ι
h : ∀ e ≤ hD.toFinset.sup id, (coeff α e) (f i) = 0
e : σ →₀ ℕ
hed : e ≤ d
⊢ (coeff α e) (f i) = 0
Theorem: MvPowerSeries.StronglySummable.hasProd_of_one_add
Proof state before:
case h.e'_4.a
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
hf : StronglySummable f
this : UniformAddGroup (MvPowerSeries σ α)
V : Set (MvPowerSeries σ α)
hV : V ∈ nhds ⋯.prod
V₀ : Set (MvPowerSeries σ α) := Add.add ⋯.prod ⁻¹' V
hV'₀ : V = Add.add (-⋯.prod) ⁻¹' V₀
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
htV₀ : D.pi t ⊆ V₀
J : Finset ι
hIJ : hf.unionOfSupportOfCoeffLe (hD.toFinset.sup id) ⊆ J
d : σ →₀ ℕ
hd : d ∈ D
i : ι
h : ∀ e ≤ hD.toFinset.sup id, (coeff α e) (f i) = 0
e : σ →₀ ℕ
hed : e ≤ d
⊢ (coeff α e) (f i) = 0
Tactic:
refine' h e (le_trans hed _)
Proof state after:
case h.e'_4.a
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
hf : StronglySummable f
this : UniformAddGroup (MvPowerSeries σ α)
V : Set (MvPowerSeries σ α)
hV : V ∈ nhds ⋯.prod
V₀ : Set (MvPowerSeries σ α) := Add.add ⋯.prod ⁻¹' V
hV'₀ : V = Add.add (-⋯.prod) ⁻¹' V₀
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
htV₀ : D.pi t ⊆ V₀
J : Finset ι
hIJ : hf.unionOfSupportOfCoeffLe (hD.toFinset.sup id) ⊆ J
d : σ →₀ ℕ
hd : d ∈ D
i : ι
h : ∀ e ≤ hD.toFinset.sup id, (coeff α e) (f i) = 0
e : σ →₀ ℕ
hed : e ≤ d
⊢ d ≤ hD.toFinset.sup id
Theorem: MvPowerSeries.StronglySummable.hasProd_of_one_add
Proof state before:
case h.e'_4.a
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
hf : StronglySummable f
this : UniformAddGroup (MvPowerSeries σ α)
V : Set (MvPowerSeries σ α)
hV : V ∈ nhds ⋯.prod
V₀ : Set (MvPowerSeries σ α) := Add.add ⋯.prod ⁻¹' V
hV'₀ : V = Add.add (-⋯.prod) ⁻¹' V₀
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
htV₀ : D.pi t ⊆ V₀
J : Finset ι
hIJ : hf.unionOfSupportOfCoeffLe (hD.toFinset.sup id) ⊆ J
d : σ →₀ ℕ
hd : d ∈ D
i : ι
h : ∀ e ≤ hD.toFinset.sup id, (coeff α e) (f i) = 0
e : σ →₀ ℕ
hed : e ≤ d
⊢ d ≤ hD.toFinset.sup id
Tactic:
apply Finset.le_sup ((Set.Finite.mem_toFinset hD).mpr hd)
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.multipliable_of_one_add
Proof state before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι✝ : Type u_3
f✝ : ι✝ → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
ι : Type u_4
f : ι → MvPowerSeries σ α
hf : StronglySummable f
⊢ Multipliable fun i => 1 + f i
Tactic:
classical exact hf.hasProd_of_one_add.multipliable
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.multipliable_of_one_add
Proof state before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι✝ : Type u_3
f✝ : ι✝ → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
ι : Type u_4
f : ι → MvPowerSeries σ α
hf : StronglySummable f
⊢ Multipliable fun i => 1 + f i
Tactic:
exact hf.hasProd_of_one_add.multipliable
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.tprod_eq_of_one_add
Proof state before:
σ : Type u_1
α : Type u_2
inst✝⁴ : DecidableEq σ
ι✝ : Type u_3
f✝ : ι✝ → MvPowerSeries σ α
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : T2Space α
ι : Type u_4
f : ι → MvPowerSeries σ α
hf : StronglySummable f
⊢ ∏' (i : ι), (1 + f i) = tsum (partialProduct f)
Tactic:
haveI : T2Space (MvPowerSeries σ α) := t2Space σ α
Proof state after:
σ : Type u_1
α : Type u_2
inst✝⁴ : DecidableEq σ
ι✝ : Type u_3
f✝ : ι✝ → MvPowerSeries σ α
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : T2Space α
ι : Type u_4
f : ι → MvPowerSeries σ α
hf : StronglySummable f
this : T2Space (MvPowerSeries σ α)
⊢ ∏' (i : ι), (1 + f i) = tsum (partialProduct f)
Theorem: MvPowerSeries.StronglySummable.tprod_eq_of_one_add
Proof state before:
σ : Type u_1
α : Type u_2
inst✝⁴ : DecidableEq σ
ι✝ : Type u_3
f✝ : ι✝ → MvPowerSeries σ α
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : T2Space α
ι : Type u_4
f : ι → MvPowerSeries σ α
hf : StronglySummable f
this : T2Space (MvPowerSeries σ α)
⊢ ∏' (i : ι), (1 + f i) = tsum (partialProduct f)
Tactic:
rw [hf.hasProd_of_one_add.tprod_eq, StronglyMultipliable.prod_eq, sum_eq_tsum]
Proof state after:
no goals
Theorem: rewriting_4_fold_sums
Proof state before:
α : Type u_1
inst✝ : CommSemiring α
m n u v : ℕ
h : m + n = u + v
f : ℕ × ℕ → α
g : (ℕ × ℕ) × ℕ × ℕ → α
hgf : g = fun x => f (x.1.1, x.1.2)
hf : ∀ (x : ℕ × ℕ), u < x.1 ∨ v < x.2 → f x = 0
⊢ (Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) (Finset.antidiagonal m ×ˢ Finset.antidiagonal n)).sum
      g =
    (Finset.antidiagonal m).sum f
Tactic:
have hq :∀ x ∈ Finset.filter
  (fun x : (ℕ × ℕ) × ℕ × ℕ => x.fst.fst + x.snd.fst = u ∧ x.fst.snd + x.snd.snd = v)
    (Finset.antidiagonal m ×ˢ Finset.antidiagonal n),
  x.fst ∈ Finset.antidiagonal m := by
  intro x; simp; intro h'; simp [h']
Proof state after:
α : Type u_1
inst✝ : CommSemiring α
m n u v : ℕ
h : m + n = u + v
f : ℕ × ℕ → α
g : (ℕ × ℕ) × ℕ × ℕ → α
hgf : g = fun x => f (x.1.1, x.1.2)
hf : ∀ (x : ℕ × ℕ), u < x.1 ∨ v < x.2 → f x = 0
hq :
  ∀ x ∈ Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) (Finset.antidiagonal m ×ˢ Finset.antidiagonal n),
    x.1 ∈ Finset.antidiagonal m
⊢ (Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) (Finset.antidiagonal m ×ˢ Finset.antidiagonal n)).sum
      g =
    (Finset.antidiagonal m).sum f
Theorem: rewriting_4_fold_sums
Proof state before:
α : Type u_1
inst✝ : CommSemiring α
m n u v : ℕ
h : m + n = u + v
f : ℕ × ℕ → α
g : (ℕ × ℕ) × ℕ × ℕ → α
hgf : g = fun x => f (x.1.1, x.1.2)
hf : ∀ (x : ℕ × ℕ), u < x.1 ∨ v < x.2 → f x = 0
hq :
  ∀ x ∈ Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) (Finset.antidiagonal m ×ˢ Finset.antidiagonal n),
    x.1 ∈ Finset.antidiagonal m
⊢ (Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) (Finset.antidiagonal m ×ˢ Finset.antidiagonal n)).sum
      g =
    (Finset.antidiagonal m).sum f
Tactic:
rw [← Finset.sum_fiberwise_of_maps_to hq]
Proof state after:
α : Type u_1
inst✝ : CommSemiring α
m n u v : ℕ
h : m + n = u + v
f : ℕ × ℕ → α
g : (ℕ × ℕ) × ℕ × ℕ → α
hgf : g = fun x => f (x.1.1, x.1.2)
hf : ∀ (x : ℕ × ℕ), u < x.1 ∨ v < x.2 → f x = 0
hq :
  ∀ x ∈ Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) (Finset.antidiagonal m ×ˢ Finset.antidiagonal n),
    x.1 ∈ Finset.antidiagonal m
⊢ ∑ j ∈ Finset.antidiagonal m,
      ∑
        i ∈
          Finset.filter (fun i => i.1 = j)
            (Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v)
              (Finset.antidiagonal m ×ˢ Finset.antidiagonal n)),
        g i =
    (Finset.antidiagonal m).sum f
Theorem: rewriting_4_fold_sums
Proof state before:
α : Type u_1
inst✝ : CommSemiring α
m n u v : ℕ
h : m + n = u + v
f : ℕ × ℕ → α
g : (ℕ × ℕ) × ℕ × ℕ → α
hgf : g = fun x => f (x.1.1, x.1.2)
hf : ∀ (x : ℕ × ℕ), u < x.1 ∨ v < x.2 → f x = 0
hq :
  ∀ x ∈ Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) (Finset.antidiagonal m ×ˢ Finset.antidiagonal n),
    x.1 ∈ Finset.antidiagonal m
⊢ ∑ j ∈ Finset.antidiagonal m,
      ∑
        i ∈
          Finset.filter (fun i => i.1 = j)
            (Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v)
              (Finset.antidiagonal m ×ˢ Finset.antidiagonal n)),
        g i =
    (Finset.antidiagonal m).sum f
Tactic:
apply Finset.sum_congr rfl
Proof state after:
α : Type u_1
inst✝ : CommSemiring α
m n u v : ℕ
h : m + n = u + v
f : ℕ × ℕ → α
g : (ℕ × ℕ) × ℕ × ℕ → α
hgf : g = fun x => f (x.1.1, x.1.2)
hf : ∀ (x : ℕ × ℕ), u < x.1 ∨ v < x.2 → f x = 0
hq :
  ∀ x ∈ Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) (Finset.antidiagonal m ×ˢ Finset.antidiagonal n),
    x.1 ∈ Finset.antidiagonal m
⊢ ∀ x ∈ Finset.antidiagonal m,
    ∑
        i ∈
          Finset.filter (fun i => i.1 = x)
            (Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v)
              (Finset.antidiagonal m ×ˢ Finset.antidiagonal n)),
        g i =
      f x
Theorem: rewriting_4_fold_sums
Proof state before:
α : Type u_1
inst✝ : CommSemiring α
m n u v : ℕ
h : m + n = u + v
f : ℕ × ℕ → α
g : (ℕ × ℕ) × ℕ × ℕ → α
hgf : g = fun x => f (x.1.1, x.1.2)
hf : ∀ (x : ℕ × ℕ), u < x.1 ∨ v < x.2 → f x = 0
hq :
  ∀ x ∈ Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) (Finset.antidiagonal m ×ˢ Finset.antidiagonal n),
    x.1 ∈ Finset.antidiagonal m
⊢ ∀ x ∈ Finset.antidiagonal m,
    ∑
        i ∈
          Finset.filter (fun i => i.1 = x)
            (Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v)
              (Finset.antidiagonal m ×ˢ Finset.antidiagonal n)),
        g i =
      f x
Tactic:
rintro ⟨i, j⟩ hij
Proof state after:
case mk
α : Type u_1
inst✝ : CommSemiring α
m n u v : ℕ
h : m + n = u + v
f : ℕ × ℕ → α
g : (ℕ × ℕ) × ℕ × ℕ → α
hgf : g = fun x => f (x.1.1, x.1.2)
hf : ∀ (x : ℕ × ℕ), u < x.1 ∨ v < x.2 → f x = 0
hq :
  ∀ x ∈ Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) (Finset.antidiagonal m ×ˢ Finset.antidiagonal n),
    x.1 ∈ Finset.antidiagonal m
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal m
⊢ ∑
      i ∈
        Finset.filter (fun i_1 => i_1.1 = (i, j))
          (Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v)
            (Finset.antidiagonal m ×ˢ Finset.antidiagonal n)),
      g i =
    f (i, j)
Theorem: rewriting_4_fold_sums
Proof state before:
case mk
α : Type u_1
inst✝ : CommSemiring α
m n u v : ℕ
h : m + n = u + v
f : ℕ × ℕ → α
g : (ℕ × ℕ) × ℕ × ℕ → α
hgf : g = fun x => f (x.1.1, x.1.2)
hf : ∀ (x : ℕ × ℕ), u < x.1 ∨ v < x.2 → f x = 0
hq :
  ∀ x ∈ Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) (Finset.antidiagonal m ×ˢ Finset.antidiagonal n),
    x.1 ∈ Finset.antidiagonal m
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal m
⊢ ∑
      i ∈
        Finset.filter (fun i_1 => i_1.1 = (i, j))
          (Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v)
            (Finset.antidiagonal m ×ˢ Finset.antidiagonal n)),
      g i =
    f (i, j)
Tactic:
simp only [Finset.mem_antidiagonal] at hij
Proof state after:
case mk
α : Type u_1
inst✝ : CommSemiring α
m n u v : ℕ
h : m + n = u + v
f : ℕ × ℕ → α
g : (ℕ × ℕ) × ℕ × ℕ → α
hgf : g = fun x => f (x.1.1, x.1.2)
hf : ∀ (x : ℕ × ℕ), u < x.1 ∨ v < x.2 → f x = 0
hq :
  ∀ x ∈ Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) (Finset.antidiagonal m ×ˢ Finset.antidiagonal n),
    x.1 ∈ Finset.antidiagonal m
i j : ℕ
hij : i + j = m
⊢ ∑
      i ∈
        Finset.filter (fun i_1 => i_1.1 = (i, j))
          (Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v)
            (Finset.antidiagonal m ×ˢ Finset.antidiagonal n)),
      g i =
    f (i, j)
Theorem: rewriting_4_fold_sums
Proof state before:
case mk
α : Type u_1
inst✝ : CommSemiring α
m n u v : ℕ
h : m + n = u + v
f : ℕ × ℕ → α
g : (ℕ × ℕ) × ℕ × ℕ → α
hgf : g = fun x => f (x.1.1, x.1.2)
hf : ∀ (x : ℕ × ℕ), u < x.1 ∨ v < x.2 → f x = 0
hq :
  ∀ x ∈ Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) (Finset.antidiagonal m ×ˢ Finset.antidiagonal n),
    x.1 ∈ Finset.antidiagonal m
i j : ℕ
hij : i + j = m
⊢ ∑
      i ∈
        Finset.filter (fun i_1 => i_1.1 = (i, j))
          (Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v)
            (Finset.antidiagonal m ×ˢ Finset.antidiagonal n)),
      g i =
    f (i, j)
Tactic:
rw [Finset.sum_filter]
Proof state after:
case mk
α : Type u_1
inst✝ : CommSemiring α
m n u v : ℕ
h : m + n = u + v
f : ℕ × ℕ → α
g : (ℕ × ℕ) × ℕ × ℕ → α
hgf : g = fun x => f (x.1.1, x.1.2)
hf : ∀ (x : ℕ × ℕ), u < x.1 ∨ v < x.2 → f x = 0
hq :
  ∀ x ∈ Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) (Finset.antidiagonal m ×ˢ Finset.antidiagonal n),
    x.1 ∈ Finset.antidiagonal m
i j : ℕ
hij : i + j = m
⊢ (∑
      a ∈
        Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) (Finset.antidiagonal m ×ˢ Finset.antidiagonal n),
      if a.1 = (i, j) then g a else 0) =
    f (i, j)