Theorem: MvPowerSeries.StronglySummable.hasProd_of_one_add (DividedPowers/ForMathlib/MvPowerSeries/StronglySummable/Topology.lean)

State before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
hf : StronglySummable f
⊢ HasProd (fun i => 1 + f i) ⋯.prod
Tactic:
haveI := uniformAddGroup σ α
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 σ α)
⊢ HasProd (fun i => 1 + f i) ⋯.prod

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 σ α)
⊢ HasProd (fun i => 1 + f i) ⋯.prod
Tactic:
intro V hV
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 ∈ Filter.map (fun s => ∏ b ∈ s, (fun i => 1 + f i) b) Filter.atTop

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 ∈ Filter.map (fun s => ∏ b ∈ s, (fun i => 1 + f i) b) Filter.atTop
Tactic:
simp only [Filter.mem_map, Filter.mem_atTop_sets, ge_iff_le, Finset.le_eq_subset,
  Set.mem_preimage]
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
⊢ ∃ a, ∀ (b : Finset ι), a ⊆ b → ∏ x ∈ b, (1 + f x) ∈ V

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
⊢ ∃ a, ∀ (b : Finset ι), a ⊆ b → ∏ x ∈ b, (1 + f x) ∈ V
Tactic:
let V₀ := Add.add hf.toStronglyMultipliable.prod ⁻¹' V
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
⊢ ∃ a, ∀ (b : Finset ι), a ⊆ b → ∏ x ∈ b, (1 + f x) ∈ V

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]
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

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
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

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₀
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

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₀
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

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)
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

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
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

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]
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₀

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₀
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

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
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

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
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

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
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

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]
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

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
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

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)
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

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]
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

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
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

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]
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

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
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

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]
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

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
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

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]
State after:
no goals

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 _))
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)

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]
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

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
State after:
no goals

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
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

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
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)

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
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)

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
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

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]
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

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
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

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 _)
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

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)
State after:
no goals