internlm/Lean-Github huggingface dataset:
Theorem: termCmmap_norm
Proof state before:
case pos
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
nk : n < k
tn : ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (fstCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖fstCmmap 𝕜 𝕜 𝕜‖ * ‖t‖
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (fstCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖
Tactic:
rw [fstCmmap_norm] at tn
Proof state after:
case pos
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
nk : n < k
tn : ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (fstCmmap 𝕜 𝕜 𝕜) t‖ ≤ 1 * ‖t‖
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (fstCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖
Theorem: termCmmap_norm
Proof state before:
case pos
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
nk : n < k
tn : ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (fstCmmap 𝕜 𝕜 𝕜) t‖ ≤ 1 * ‖t‖
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (fstCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖
Tactic:
simp at tn
Proof state after:
case pos
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
nk : n < k
tn : ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (fstCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖t‖
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (fstCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖
Theorem: termCmmap_norm
Proof state before:
case pos
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
nk : n < k
tn : ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (fstCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖t‖
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (fstCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖
Tactic:
exact _root_.trans tn nh
Proof state after:
no goals
Theorem: termCmmap_norm
Proof state before:
case neg
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
tn :
  ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) t‖ ≤
    ‖if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜‖ * ‖t‖
nk : ¬n < k
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖
Tactic:
simp [nk] at tn ⊢
Proof state after:
case neg
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
nk : ¬n < k
tn : ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖sndCmmap 𝕜 𝕜 𝕜‖ * ‖t‖
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖
Theorem: termCmmap_norm
Proof state before:
case neg
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
nk : ¬n < k
tn : ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖sndCmmap 𝕜 𝕜 𝕜‖ * ‖t‖
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖
Tactic:
rw [sndCmmap_norm] at tn
Proof state after:
case neg
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
nk : ¬n < k
tn : ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ 1 * ‖t‖
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖
Theorem: termCmmap_norm
Proof state before:
case neg
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
nk : ¬n < k
tn : ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ 1 * ‖t‖
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖
Tactic:
simp at tn
Proof state after:
case neg
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
nk : ¬n < k
tn : ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖t‖
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖
Theorem: termCmmap_norm
Proof state before:
case neg
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
nk : ¬n < k
tn : ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖t‖
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖
Tactic:
exact _root_.trans tn nh
Proof state after:
no goals
Theorem: ContinuousLinearMap.apply_eq_zero_of_eq_zero
Proof state before:
n : ℕ
𝕜✝ : Type
inst✝⁷ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝⁶ : Semiring R
𝕜 X Y : Type
inst✝⁵ : NormedField 𝕜
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup X
inst✝² : Module 𝕜 X
inst✝¹ : NormedAddCommGroup Y
inst✝ : Module 𝕜 Y
f : X →L[𝕜] Y
x : X
h : x = 0
⊢ f x = 0
Tactic:
rw [h, ContinuousLinearMap.map_zero]
Proof state after:
no goals
Theorem: ContinuousLinearMap.smulRight_ne_zero
Proof state before:
n : ℕ
𝕜 : Type
inst✝¹¹ : NontriviallyNormedField 𝕜
R✝ A✝ B✝ E : Type
inst✝¹⁰ : Semiring R✝
R A B : Type
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : AddCommMonoid A
inst✝⁶ : TopologicalSpace R
inst✝⁵ : Module R A
inst✝⁴ : TopologicalSpace B
inst✝³ : AddCommMonoid B
inst✝² : Module R B
inst✝¹ : ContinuousSMul R B
inst✝ : NoZeroSMulDivisors R B
c : A →L[R] R
f : B
c0 : c ≠ 0
f0 : f ≠ 0
⊢ c.smulRight f ≠ 0
Tactic:
rcases ContinuousLinearMap.exists_ne_zero c0 with ⟨x,cx⟩
Proof state after:
case intro
n : ℕ
𝕜 : Type
inst✝¹¹ : NontriviallyNormedField 𝕜
R✝ A✝ B✝ E : Type
inst✝¹⁰ : Semiring R✝
R A B : Type
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : AddCommMonoid A
inst✝⁶ : TopologicalSpace R
inst✝⁵ : Module R A
inst✝⁴ : TopologicalSpace B
inst✝³ : AddCommMonoid B
inst✝² : Module R B
inst✝¹ : ContinuousSMul R B
inst✝ : NoZeroSMulDivisors R B
c : A →L[R] R
f : B
c0 : c ≠ 0
f0 : f ≠ 0
x : A
cx : c x ≠ 0
⊢ c.smulRight f ≠ 0
Theorem: ContinuousLinearMap.smulRight_ne_zero
Proof state before:
case intro
n : ℕ
𝕜 : Type
inst✝¹¹ : NontriviallyNormedField 𝕜
R✝ A✝ B✝ E : Type
inst✝¹⁰ : Semiring R✝
R A B : Type
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : AddCommMonoid A
inst✝⁶ : TopologicalSpace R
inst✝⁵ : Module R A
inst✝⁴ : TopologicalSpace B
inst✝³ : AddCommMonoid B
inst✝² : Module R B
inst✝¹ : ContinuousSMul R B
inst✝ : NoZeroSMulDivisors R B
c : A →L[R] R
f : B
c0 : c ≠ 0
f0 : f ≠ 0
x : A
cx : c x ≠ 0
⊢ c.smulRight f ≠ 0
Tactic:
simp only [Ne, ContinuousLinearMap.ext_iff, not_forall, ContinuousLinearMap.zero_apply,
  ContinuousLinearMap.smulRight_apply, smul_eq_zero, not_or]
Proof state after:
case intro
n : ℕ
𝕜 : Type
inst✝¹¹ : NontriviallyNormedField 𝕜
R✝ A✝ B✝ E : Type
inst✝¹⁰ : Semiring R✝
R A B : Type
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : AddCommMonoid A
inst✝⁶ : TopologicalSpace R
inst✝⁵ : Module R A
inst✝⁴ : TopologicalSpace B
inst✝³ : AddCommMonoid B
inst✝² : Module R B
inst✝¹ : ContinuousSMul R B
inst✝ : NoZeroSMulDivisors R B
c : A →L[R] R
f : B
c0 : c ≠ 0
f0 : f ≠ 0
x : A
cx : c x ≠ 0
⊢ ∃ x, ¬c x = 0 ∧ ¬f = 0
Theorem: ContinuousLinearMap.smulRight_ne_zero
Proof state before:
case intro
n : ℕ
𝕜 : Type
inst✝¹¹ : NontriviallyNormedField 𝕜
R✝ A✝ B✝ E : Type
inst✝¹⁰ : Semiring R✝
R A B : Type
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : AddCommMonoid A
inst✝⁶ : TopologicalSpace R
inst✝⁵ : Module R A
inst✝⁴ : TopologicalSpace B
inst✝³ : AddCommMonoid B
inst✝² : Module R B
inst✝¹ : ContinuousSMul R B
inst✝ : NoZeroSMulDivisors R B
c : A →L[R] R
f : B
c0 : c ≠ 0
f0 : f ≠ 0
x : A
cx : c x ≠ 0
⊢ ∃ x, ¬c x = 0 ∧ ¬f = 0
Tactic:
use x
Proof state after:
no goals
Theorem: ContinuousLinearMap.one_ne_zero
Proof state before:
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R✝ A✝ B E : Type
inst✝⁵ : Semiring R✝
R A : Type
inst✝⁴ : Ring R
inst✝³ : TopologicalSpace A
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Nontrivial A
⊢ 1 ≠ 0
Tactic:
simp only [Ne, ContinuousLinearMap.ext_iff, not_forall, ContinuousLinearMap.zero_apply,
  ContinuousLinearMap.one_apply]
Proof state after:
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R✝ A✝ B E : Type
inst✝⁵ : Semiring R✝
R A : Type
inst✝⁴ : Ring R
inst✝³ : TopologicalSpace A
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Nontrivial A
⊢ ∃ x, ¬x = 0
Theorem: ContinuousLinearMap.one_ne_zero
Proof state before:
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R✝ A✝ B E : Type
inst✝⁵ : Semiring R✝
R A : Type
inst✝⁴ : Ring R
inst✝³ : TopologicalSpace A
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Nontrivial A
⊢ ∃ x, ¬x = 0
Tactic:
apply exists_ne
Proof state after:
no goals
Theorem: tangentSpace_norm_eq_complex_norm
Proof 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
z : S
x : TangentSpace I z
⊢ ‖x‖ = Complex.abs x
Tactic:
rw [← Complex.norm_eq_abs]
Proof state after:
no goals
Theorem: mderiv_eq_zero_iff
Proof 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
z : S
w : T
f : TangentSpace I z →L[ℂ] TangentSpace I w
u : TangentSpace I z
⊢ f u = 0 ↔ f = 0 ∨ u = 0
Tactic:
constructor
Proof state after:
case 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
z : S
w : T
f : TangentSpace I z →L[ℂ] TangentSpace I w
u : TangentSpace I z
⊢ f u = 0 → f = 0 ∨ u = 0

case 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
z : S
w : T
f : TangentSpace I z →L[ℂ] TangentSpace I w
u : TangentSpace I z
⊢ f = 0 ∨ u = 0 → f u = 0
Theorem: mderiv_eq_zero_iff
Proof state before:
case 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
z : S
w : T
f : TangentSpace I z →L[ℂ] TangentSpace I w
u : TangentSpace I z
⊢ f u = 0 → f = 0 ∨ u = 0
Tactic:
rw [or_iff_not_imp_right]
Proof state after:
case 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
z : S
w : T
f : TangentSpace I z →L[ℂ] TangentSpace I w
u : TangentSpace I z
⊢ f u = 0 → ¬u = 0 → f = 0
Theorem: mderiv_eq_zero_iff
Proof state before:
case 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
z : S
w : T
f : TangentSpace I z →L[ℂ] TangentSpace I w
u : TangentSpace I z
⊢ f u = 0 → ¬u = 0 → f = 0
Tactic:
intro f0 u0
Proof state after:
case 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
z : S
w : T
f : TangentSpace I z →L[ℂ] TangentSpace I w
u : TangentSpace I z
f0 : f u = 0
u0 : ¬u = 0
⊢ f = 0
Theorem: mderiv_eq_zero_iff
Proof state before:
case 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
z : S
w : T
f : TangentSpace I z →L[ℂ] TangentSpace I w
u : TangentSpace I z
f0 : f u = 0
u0 : ¬u = 0
⊢ f = 0
Tactic:
apply ContinuousLinearMap.ext
Proof state after:
case mp.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
z : S
w : T
f : TangentSpace I z →L[ℂ] TangentSpace I w
u : TangentSpace I z
f0 : f u = 0
u0 : ¬u = 0
⊢ ∀ (x : TangentSpace I z), f x = 0 x
Theorem: mderiv_eq_zero_iff
Proof state before:
case mp.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
z : S
w : T
f : TangentSpace I z →L[ℂ] TangentSpace I w
u : TangentSpace I z
f0 : f u = 0
u0 : ¬u = 0
⊢ ∀ (x : TangentSpace I z), f x = 0 x
Tactic:
intro v
Proof state after:
case mp.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
z : S
w : T
f : TangentSpace I z →L[ℂ] TangentSpace I w
u : TangentSpace I z
f0 : f u = 0
u0 : ¬u = 0
v : TangentSpace I z
⊢ f v = 0 v
Theorem: mderiv_eq_zero_iff
Proof state before:
case mp.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
z : S
w : T
f : TangentSpace I z →L[ℂ] TangentSpace I w
u : TangentSpace I z
f0 : f u = 0
u0 : ¬u = 0
v : TangentSpace I z
⊢ f v = 0 v
Tactic:
simp only [TangentSpace] at f u v u0
Proof state after:
case mp.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
z : S
w : T
f : ℂ →L[ℂ] ℂ
u : ℂ
f0 : f u = 0
u0 : ¬u = 0
v : ℂ
⊢ f v = 0 v
Theorem: mderiv_eq_zero_iff
Proof state before:
case mp.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
z : S
w : T
f : ℂ →L[ℂ] ℂ
u : ℂ
f0 : f u = 0
u0 : ¬u = 0
v : ℂ
⊢ f v = 0 v
Tactic:
have e : v = (v * u⁻¹) • u := by simp only [smul_eq_mul, mul_assoc, inv_mul_cancel u0, mul_one]
Proof state after:
case mp.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
z : S
w : T
f : ℂ →L[ℂ] ℂ
u : ℂ
f0 : f u = 0
u0 : ¬u = 0
v : ℂ
e : v = (v * u⁻¹) • u
⊢ f v = 0 v
Theorem: mderiv_eq_zero_iff
Proof state before:
case mp.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
z : S
w : T
f : ℂ →L[ℂ] ℂ
u : ℂ
f0 : f u = 0
u0 : ¬u = 0
v : ℂ
e : v = (v * u⁻¹) • u
⊢ f v = 0 v
Tactic:
rw [ContinuousLinearMap.zero_apply, e]
Proof state after:
case mp.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
z : S
w : T
f : ℂ →L[ℂ] ℂ
u : ℂ
f0 : f u = 0
u0 : ¬u = 0
v : ℂ
e : v = (v * u⁻¹) • u
⊢ f ((v * u⁻¹) • u) = 0
Theorem: mderiv_eq_zero_iff
Proof state before:
case mp.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
z : S
w : T
f : ℂ →L[ℂ] ℂ
u : ℂ
f0 : f u = 0
u0 : ¬u = 0
v : ℂ
e : v = (v * u⁻¹) • u
⊢ f ((v * u⁻¹) • u) = 0
Tactic:
refine Eq.trans (f.map_smul _ _) ?_
Proof state after:
case mp.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
z : S
w : T
f : ℂ →L[ℂ] ℂ
u : ℂ
f0 : f u = 0
u0 : ¬u = 0
v : ℂ
e : v = (v * u⁻¹) • u
⊢ (v * u⁻¹) • f u = 0
Theorem: mderiv_eq_zero_iff
Proof state before:
case mp.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
z : S
w : T
f : ℂ →L[ℂ] ℂ
u : ℂ
f0 : f u = 0
u0 : ¬u = 0
v : ℂ
e : v = (v * u⁻¹) • u
⊢ (v * u⁻¹) • f u = 0
Tactic:
rw [smul_eq_zero]
Proof state after:
case mp.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
z : S
w : T
f : ℂ →L[ℂ] ℂ
u : ℂ
f0 : f u = 0
u0 : ¬u = 0
v : ℂ
e : v = (v * u⁻¹) • u
⊢ v * u⁻¹ = 0 ∨ f u = 0
Theorem: mderiv_eq_zero_iff
Proof state before:
case mp.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
z : S
w : T
f : ℂ →L[ℂ] ℂ
u : ℂ
f0 : f u = 0
u0 : ¬u = 0
v : ℂ
e : v = (v * u⁻¹) • u
⊢ v * u⁻¹ = 0 ∨ f u = 0
Tactic:
right
Proof state after:
case mp.h.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
z : S
w : T
f : ℂ →L[ℂ] ℂ
u : ℂ
f0 : f u = 0
u0 : ¬u = 0
v : ℂ
e : v = (v * u⁻¹) • u
⊢ f u = 0
Theorem: mderiv_eq_zero_iff
Proof state before:
case mp.h.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
z : S
w : T
f : ℂ →L[ℂ] ℂ
u : ℂ
f0 : f u = 0
u0 : ¬u = 0
v : ℂ
e : v = (v * u⁻¹) • u
⊢ f u = 0
Tactic:
exact f0
Proof state after:
no goals
Theorem: mderiv_eq_zero_iff
Proof 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
z : S
w : T
f : ℂ →L[ℂ] ℂ
u : ℂ
f0 : f u = 0
u0 : ¬u = 0
v : ℂ
⊢ v = (v * u⁻¹) • u
Tactic:
simp only [smul_eq_mul, mul_assoc, inv_mul_cancel u0, mul_one]
Proof state after:
no goals
Theorem: mderiv_eq_zero_iff
Proof state before:
case 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
z : S
w : T
f : TangentSpace I z →L[ℂ] TangentSpace I w
u : TangentSpace I z
⊢ f = 0 ∨ u = 0 → f u = 0
Tactic:
intro h
Proof state after:
case 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
z : S
w : T
f : TangentSpace I z →L[ℂ] TangentSpace I w
u : TangentSpace I z
h : f = 0 ∨ u = 0
⊢ f u = 0
Theorem: mderiv_eq_zero_iff
Proof state before:
case 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
z : S
w : T
f : TangentSpace I z →L[ℂ] TangentSpace I w
u : TangentSpace I z
h : f = 0 ∨ u = 0
⊢ f u = 0
Tactic:
cases' h with h h
Proof state after:
case 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
z : S
w : T
f : TangentSpace I z →L[ℂ] TangentSpace I w
u : TangentSpace I z
h : f = 0
⊢ f u = 0

case 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
z : S
w : T
f : TangentSpace I z →L[ℂ] TangentSpace I w
u : TangentSpace I z
h : u = 0
⊢ f u = 0