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
⊢ ∃ a, ∀ (b : Finset ι), a ⊆ b → ∏ x ∈ b, (1 + f x) ∈ V
Tactic:
have hV'₀ : V = Add.add (-hf.toStronglyMultipliable.prod) ⁻¹' V₀ := by
  rw [← Set.preimage_comp, eq_comm]
  convert Set.preimage_id
  rw [Function.funext_iff]
  intro f
  simp only [comp_apply, id_eq]
  change _ + (_ + f) = f
  simp_rw [← add_assoc, add_right_neg, zero_add]
Proof state after:
σ : 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₀
⊢ ∃ a, ∀ (b : Finset ι), a ⊆ b → ∏ x ∈ b, (1 + f x) ∈ V
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₀
⊢ ∃ a, ∀ (b : Finset ι), a ⊆ b → ∏ x ∈ b, (1 + f x) ∈ V
Tactic:
have hV₀ : V₀ ∈ nhds (0 : MvPowerSeries σ α) := by
  apply continuousAt_def.mp (Continuous.continuousAt (continuous_add_left _))
  rw [add_zero]
  exact hV
Proof state after:
σ : 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₀
hV₀ : V₀ ∈ nhds 0
⊢ ∃ a, ∀ (b : Finset ι), a ⊆ b → ∏ x ∈ b, (1 + f x) ∈ V
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₀
hV₀ : V₀ ∈ nhds 0
⊢ ∃ a, ∀ (b : Finset ι), a ⊆ b → ∏ x ∈ b, (1 + f x) ∈ V
Tactic:
rw [nhds_pi, Filter.mem_pi] at hV₀
Proof state after:
σ : 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₀
hV₀ : ∃ I, I.Finite ∧ ∃ t, (∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)) ∧ I.pi t ⊆ V₀
⊢ ∃ a, ∀ (b : Finset ι), a ⊆ b → ∏ x ∈ b, (1 + f x) ∈ V
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₀
hV₀ : ∃ I, I.Finite ∧ ∃ t, (∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)) ∧ I.pi t ⊆ V₀
⊢ ∃ a, ∀ (b : Finset ι), a ⊆ b → ∏ x ∈ b, (1 + f x) ∈ V
Tactic:
obtain ⟨D, hD, t, ht, htV₀⟩ := hV₀
Proof state after:
case intro.intro.intro.intro
σ : 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₀
⊢ ∃ a, ∀ (b : Finset ι), a ⊆ b → ∏ x ∈ b, (1 + f x) ∈ V
Theorem: MvPowerSeries.StronglySummable.hasProd_of_one_add
Proof state before:
case intro.intro.intro.intro
σ : 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₀
⊢ ∃ a, ∀ (b : Finset ι), a ⊆ b → ∏ x ∈ b, (1 + f x) ∈ V
Tactic:
use hf.unionOfSupportOfCoeffLe (hD.toFinset.sup id)
Proof state after:
case h
σ : 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₀
⊢ ∀ (b : Finset ι), hf.unionOfSupportOfCoeffLe (hD.toFinset.sup id) ⊆ b → ∏ x ∈ b, (1 + f x) ∈ V
Theorem: MvPowerSeries.StronglySummable.hasProd_of_one_add
Proof state before:
case h
σ : 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₀
⊢ ∀ (b : Finset ι), hf.unionOfSupportOfCoeffLe (hD.toFinset.sup id) ⊆ b → ∏ x ∈ b, (1 + f x) ∈ V
Tactic:
intro J hIJ
Proof state after:
case h
σ : 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
⊢ ∏ x ∈ J, (1 + f x) ∈ V
Theorem: MvPowerSeries.StronglySummable.hasProd_of_one_add
Proof state before:
case h
σ : 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
⊢ ∏ x ∈ J, (1 + f x) ∈ V
Tactic:
rw [hV'₀, Set.mem_preimage]
Proof state after:
case h
σ : 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
⊢ Add.add (-⋯.prod) (∏ x ∈ J, (1 + f x)) ∈ V₀
Theorem: MvPowerSeries.StronglySummable.hasProd_of_one_add
Proof state before:
case h
σ : 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
⊢ Add.add (-⋯.prod) (∏ x ∈ J, (1 + f x)) ∈ V₀
Tactic:
apply htV₀
Proof state after:
case h.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
⊢ Add.add (-⋯.prod) (∏ x ∈ J, (1 + f x)) ∈ D.pi t
Theorem: MvPowerSeries.StronglySummable.hasProd_of_one_add
Proof state before:
case h.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
⊢ Add.add (-⋯.prod) (∏ x ∈ J, (1 + f x)) ∈ D.pi t
Tactic:
intro d hd
Proof state after:
case h.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
⊢ Add.add (-⋯.prod) (∏ x ∈ J, (1 + f x)) d ∈ t d
Theorem: MvPowerSeries.StronglySummable.hasProd_of_one_add
Proof state before:
case h.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
⊢ Add.add (-⋯.prod) (∏ x ∈ J, (1 + f x)) d ∈ t d
Tactic:
convert mem_of_mem_nhds (ht d) using 1
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
⊢ Add.add (-⋯.prod) (∏ x ∈ J, (1 + f x)) d = 0 d
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
⊢ Add.add (-⋯.prod) (∏ x ∈ J, (1 + f x)) d = 0 d
Tactic:
change (-_ + _) = 0
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
⊢ -⋯.prod d + (∏ x ∈ J, (1 + f x)) d = 0
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
⊢ -⋯.prod d + (∏ x ∈ J, (1 + f x)) d = 0
Tactic:
rw [neg_add_eq_sub, sub_eq_zero]
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
⊢ (∏ x ∈ J, (1 + f x)) d = ⋯.prod d
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
⊢ (∏ x ∈ J, (1 + f x)) d = ⋯.prod d
Tactic:
symm
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
⊢ ⋯.prod d = (∏ x ∈ J, (1 + f x)) d
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
⊢ ⋯.prod d = (∏ x ∈ J, (1 + f x)) d
Tactic:
apply StronglyMultipliable.coeff_prod_apply_eq_finset_prod hf (J := J)
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
⊢ hf.unionOfSupportOfCoeffLe d ⊆ J
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
⊢ V = Add.add (-⋯.prod) ⁻¹' V₀
Tactic:
rw [← Set.preimage_comp, eq_comm]
Proof state after:
σ : 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
⊢ Add.add ⋯.prod ∘ Add.add (-⋯.prod) ⁻¹' V = V
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
⊢ Add.add ⋯.prod ∘ Add.add (-⋯.prod) ⁻¹' V = V
Tactic:
convert Set.preimage_id
Proof state after:
case h.e'_2.h.e'_3
σ : 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
⊢ Add.add ⋯.prod ∘ Add.add (-⋯.prod) = id
Theorem: MvPowerSeries.StronglySummable.hasProd_of_one_add
Proof state before:
case h.e'_2.h.e'_3
σ : 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
⊢ Add.add ⋯.prod ∘ Add.add (-⋯.prod) = id
Tactic:
rw [Function.funext_iff]
Proof state after:
case h.e'_2.h.e'_3
σ : 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
⊢ ∀ (a : MvPowerSeries σ α), (Add.add ⋯.prod ∘ Add.add (-⋯.prod)) a = id a
Theorem: MvPowerSeries.StronglySummable.hasProd_of_one_add
Proof state before:
case h.e'_2.h.e'_3
σ : 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
⊢ ∀ (a : MvPowerSeries σ α), (Add.add ⋯.prod ∘ Add.add (-⋯.prod)) a = id a
Tactic:
intro f
Proof state after:
case h.e'_2.h.e'_3
σ : 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
f : MvPowerSeries σ α
⊢ (Add.add ⋯.prod ∘ Add.add (-⋯.prod)) f = id f
Theorem: MvPowerSeries.StronglySummable.hasProd_of_one_add
Proof state before:
case h.e'_2.h.e'_3
σ : 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
f : MvPowerSeries σ α
⊢ (Add.add ⋯.prod ∘ Add.add (-⋯.prod)) f = id f
Tactic:
simp only [comp_apply, id_eq]
Proof state after:
case h.e'_2.h.e'_3
σ : 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
f : MvPowerSeries σ α
⊢ Add.add ⋯.prod (Add.add (-⋯.prod) f) = f
Theorem: MvPowerSeries.StronglySummable.hasProd_of_one_add
Proof state before:
case h.e'_2.h.e'_3
σ : 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
f : MvPowerSeries σ α
⊢ Add.add ⋯.prod (Add.add (-⋯.prod) f) = f
Tactic:
change _ + (_ + f) = f
Proof state after:
case h.e'_2.h.e'_3
σ : 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
f : MvPowerSeries σ α
⊢ ⋯.prod + (-⋯.prod + f) = f
Theorem: MvPowerSeries.StronglySummable.hasProd_of_one_add
Proof state before:
case h.e'_2.h.e'_3
σ : 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
f : MvPowerSeries σ α
⊢ ⋯.prod + (-⋯.prod + f) = f
Tactic:
simp_rw [← add_assoc, add_right_neg, zero_add]
Proof state after:
no goals