Theorem: SciLean.norm₂.arg_x.ContCDiff_rule (SciLean/Core/FunctionPropositions/ContCDiff.lean)

State before:
K✝ : Type ?u.40925
inst✝¹⁴ : RCLike K✝
n : ℕ∞
X✝¹ : Type ?u.40933
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.40946
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.40957
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.40968
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.40977
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.40993
inst✝⁸ : RCLike K
X✝ : Type ?u.40999
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.41012
inst✝⁶ : Vec K Y✝
Z : Type ?u.41023
inst✝⁵ : Vec K Z
ι : Type ?u.41034
inst✝⁴ : IndexType ι
E : ι → Type ?u.41043
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : ContCDiff R n f
hx : ∀ (x : X), f x ≠ 0
⊢ ContCDiff R n fun x => ‖f x‖₂[R]
Tactic:
intro x
State after:
K✝ : Type ?u.40925
inst✝¹⁴ : RCLike K✝
n : ℕ∞
X✝¹ : Type ?u.40933
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.40946
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.40957
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.40968
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.40977
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.40993
inst✝⁸ : RCLike K
X✝ : Type ?u.40999
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.41012
inst✝⁶ : Vec K Y✝
Z : Type ?u.41023
inst✝⁵ : Vec K Z
ι : Type ?u.41034
inst✝⁴ : IndexType ι
E : ι → Type ?u.41043
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : ContCDiff R n f
hx : ∀ (x : X), f x ≠ 0
x : X
⊢ ContCDiffAt R n (fun x => ‖f x‖₂[R]) x

State before:
K✝ : Type ?u.40925
inst✝¹⁴ : RCLike K✝
n : ℕ∞
X✝¹ : Type ?u.40933
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.40946
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.40957
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.40968
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.40977
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.40993
inst✝⁸ : RCLike K
X✝ : Type ?u.40999
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.41012
inst✝⁶ : Vec K Y✝
Z : Type ?u.41023
inst✝⁵ : Vec K Z
ι : Type ?u.41034
inst✝⁴ : IndexType ι
E : ι → Type ?u.41043
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : ContCDiff R n f
hx : ∀ (x : X), f x ≠ 0
x : X
⊢ ContCDiffAt R n (fun x => ‖f x‖₂[R]) x
Tactic:
fun_prop (disch:=aesop)
State after:
no goals

State before:
case funProp.discharger
K✝ : Type ?u.40925
inst✝¹⁴ : RCLike K✝
n : ℕ∞
X✝¹ : Type ?u.40933
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.40946
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.40957
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.40968
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.40977
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.40993
inst✝⁸ : RCLike K
X✝ : Type ?u.40999
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.41012
inst✝⁶ : Vec K Y✝
Z : Type ?u.41023
inst✝⁵ : Vec K Z
ι : Type ?u.41034
inst✝⁴ : IndexType ι
E : ι → Type ?u.41043
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : ContCDiff R n f
hx : ∀ (x : X), f x ≠ 0
x : X
⊢ f x ≠ 0
Tactic:
aesop
State after:
no goals