Theorem: MvPowerSeries.continuous_C (DividedPowers/ForMathlib/MvPowerSeries/Topology.lean)

State before:
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
⊢ Continuous ⇑(C σ α)
Tactic:
apply continuous_of_continuousAt_zero
State after:
case hf
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
⊢ ContinuousAt (⇑(C σ α)) 0

State before:
case hf
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
⊢ ContinuousAt (⇑(C σ α)) 0
Tactic:
rw [continuousAt_pi]
State after:
case hf
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
⊢ ∀ (i : σ →₀ ℕ), ContinuousAt (fun y => (C σ α) y i) 0

State before:
case hf
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
⊢ ∀ (i : σ →₀ ℕ), ContinuousAt (fun y => (C σ α) y i) 0
Tactic:
intro d
State after:
case hf
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
⊢ ContinuousAt (fun y => (C σ α) y d) 0

State before:
case hf
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
⊢ ContinuousAt (fun y => (C σ α) y d) 0
Tactic:
change ContinuousAt (fun y => coeff α d ((C σ α) y)) 0
State after:
case hf
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
⊢ ContinuousAt (fun y => (coeff α d) ((C σ α) y)) 0

State before:
case hf
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
⊢ ContinuousAt (fun y => (coeff α d) ((C σ α) y)) 0
Tactic:
by_cases hd : d = 0
State after:
case pos
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
hd : d = 0
⊢ ContinuousAt (fun y => (coeff α d) ((C σ α) y)) 0

case neg
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
hd : ¬d = 0
⊢ ContinuousAt (fun y => (coeff α d) ((C σ α) y)) 0

State before:
case pos
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
hd : d = 0
⊢ ContinuousAt (fun y => (coeff α d) ((C σ α) y)) 0
Tactic:
convert continuousAt_id
State after:
case h.e'_5.h
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
hd : d = 0
x✝ : α
⊢ (coeff α d) ((C σ α) x✝) = id x✝

State before:
case h.e'_5.h
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
hd : d = 0
x✝ : α
⊢ (coeff α d) ((C σ α) x✝) = id x✝
Tactic:
rw [hd, coeff_zero_C, id_eq]
State after:
no goals

State before:
case neg
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
hd : ¬d = 0
⊢ ContinuousAt (fun y => (coeff α d) ((C σ α) y)) 0
Tactic:
convert continuousAt_const
State after:
case h.e'_5.h
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
hd : ¬d = 0
x✝ : α
⊢ (coeff α d) ((C σ α) x✝) = ?neg.convert_6✝

case neg.convert_6
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
hd : ¬d = 0
⊢ α

State before:
case h.e'_5.h
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
hd : ¬d = 0
x✝ : α
⊢ (coeff α d) ((C σ α) x✝) = ?neg.convert_6✝

case neg.convert_6
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
hd : ¬d = 0
⊢ α
Tactic:
rw [coeff_C, if_neg hd]
State after:
no goals