Theorem: mderiv_comp_eq_zero_iff (Ray/AnalyticManifold/OneDimension.lean)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
⊢ f.comp g = 0 ↔ f = 0 ∨ g = 0
Tactic:
rcases exists_ne (0 : TangentSpace I x) with ⟨t, t0⟩
State after:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
⊢ f.comp g = 0 ↔ f = 0 ∨ g = 0

State before:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
⊢ f.comp g = 0 ↔ f = 0 ∨ g = 0
Tactic:
constructor
State after:
case intro.mp
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
⊢ f.comp g = 0 → f = 0 ∨ g = 0

case intro.mpr
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
⊢ f = 0 ∨ g = 0 → f.comp g = 0

State before:
case intro.mp
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
⊢ f.comp g = 0 → f = 0 ∨ g = 0
Tactic:
intro h
State after:
case intro.mp
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f.comp g = 0
⊢ f = 0 ∨ g = 0

State before:
case intro.mp
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f.comp g = 0
⊢ f = 0 ∨ g = 0
Tactic:
simp only [← mderiv_eq_zero_iff' t0, ContinuousLinearMap.comp_apply] at h
State after:
case intro.mp
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
⊢ f = 0 ∨ g = 0

State before:
case intro.mp
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
⊢ f = 0 ∨ g = 0
Tactic:
by_cases g0 : g t = 0
State after:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : g t = 0
⊢ f = 0 ∨ g = 0

case neg
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : ¬g t = 0
⊢ f = 0 ∨ g = 0

State before:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : g t = 0
⊢ f = 0 ∨ g = 0

case neg
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : ¬g t = 0
⊢ f = 0 ∨ g = 0
Tactic:
right
State after:
case pos.h
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : g t = 0
⊢ g = 0

case neg
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : ¬g t = 0
⊢ f = 0 ∨ g = 0

State before:
case pos.h
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : g t = 0
⊢ g = 0

case neg
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : ¬g t = 0
⊢ f = 0 ∨ g = 0
Tactic:
rw [mderiv_eq_zero_iff' t0] at g0
State after:
case pos.h
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : g = 0
⊢ g = 0

case neg
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : ¬g t = 0
⊢ f = 0 ∨ g = 0

State before:
case pos.h
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : g = 0
⊢ g = 0

case neg
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : ¬g t = 0
⊢ f = 0 ∨ g = 0
Tactic:
exact g0
State after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : ¬g t = 0
⊢ f = 0 ∨ g = 0

State before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : ¬g t = 0
⊢ f = 0 ∨ g = 0
Tactic:
left
State after:
case neg.h
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : ¬g t = 0
⊢ f = 0

State before:
case neg.h
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : ¬g t = 0
⊢ f = 0
Tactic:
rwa [← mderiv_eq_zero_iff' g0]
State after:
no goals

State before:
case intro.mpr
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
⊢ f = 0 ∨ g = 0 → f.comp g = 0
Tactic:
intro h
State after:
case intro.mpr
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f = 0 ∨ g = 0
⊢ f.comp g = 0

State before:
case intro.mpr
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f = 0 ∨ g = 0
⊢ f.comp g = 0
Tactic:
cases' h with h h
State after:
case intro.mpr.inl
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f = 0
⊢ f.comp g = 0

case intro.mpr.inr
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : g = 0
⊢ f.comp g = 0

State before:
case intro.mpr.inl
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f = 0
⊢ f.comp g = 0

case intro.mpr.inr
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : g = 0
⊢ f.comp g = 0
Tactic:
simp only [h, g.zero_comp]
State after:
case intro.mpr.inr
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : g = 0
⊢ f.comp g = 0

State before:
case intro.mpr.inr
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : g = 0
⊢ f.comp g = 0
Tactic:
simp only [h, f.comp_zero]
State after:
no goals