awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.VectorBundle.Riemannian
Goal:
B : Type u_1
inst : TopologicalSpace B
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : B → Type u_3
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → NormedAddCommGroup (E x)
inst_5 : (x : B) → InnerProductSpace ℝ (E x)
inst_6 : FiberBundle F E
inst_7 : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x y : B
hy :
  norm (E := E x →L[ℝ] E y)
      (comp.{0, 0, 0, u_3, u_2, u_3} (R₂ := ℝ) (σ₁₂ := RingHom.id ℝ) (σ₂₃ := RingHom.id ℝ) (M₂ := F)
          (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) y)
          (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x) :
        E x →L[ℝ] E y) <
    2
A :
  Eq (α := F →L[ℝ] F)
    ((Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x :
        ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F) ∘SL
      (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) x :
        ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x)))
    (ContinuousLinearMap.id ℝ F)
this :
  Eq (α := ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E y))
    (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) y :
      ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E y))
    (comp (σ₂₃ := RingHom.id ℝ) (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) y)
        (ContinuousLinearMap.id ℝ F) :
      ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E y))
h₁ :
  norm (E := E x →L[ℝ] E y)
        (comp.{0, 0, 0, u_3, u_2, u_3} (R₂ := ℝ) (σ₁₂ := RingHom.id ℝ) (σ₂₃ := RingHom.id ℝ) (M₂ := F)
            (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) y)
            (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x) :
          E x →L[ℝ] E y) *
      norm (E := ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x))
        (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) x :
          ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x)) <
    2 *
      (1 +
        norm (E := ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x))
          (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) x :
            ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x)))
⊢ norm (E := ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E y))
      (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) y :
        ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E y)) <
    2 *
      (1 +
        norm (E := ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x))
          (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) x :
            ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x)))

Tactic:
grw [this, ← A, ← comp_assoc, opNorm_comp_le]

Premises used: ContinuousLinearMap.opNorm_comp_le, ContinuousLinearMap.comp_assoc
-- Module: Mathlib.Topology.VectorBundle.Riemannian
Goal:
B : Type u_1
inst : TopologicalSpace B
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : B → Type u_3
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → NormedAddCommGroup (E x)
inst_5 : (x : B) → InnerProductSpace ℝ (E x)
inst_6 : FiberBundle F E
inst_7 : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x y : B
hy :
  norm (E := E x →L[ℝ] E y)
      (comp.{0, 0, 0, u_3, u_2, u_3} (R₂ := ℝ) (σ₁₂ := RingHom.id ℝ) (σ₂₃ := RingHom.id ℝ) (M₂ := F)
          (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) y)
          (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x) :
        E x →L[ℝ] E y) <
    2
A :
  Eq (α := F →L[ℝ] F)
    ((Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x :
        ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F) ∘SL
      (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) x :
        ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x)))
    (ContinuousLinearMap.id ℝ F)
this :
  Eq (α := ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E y))
    (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) y :
      ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E y))
    (comp (σ₂₃ := RingHom.id ℝ) (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) y)
        (ContinuousLinearMap.id ℝ F) :
      ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E y))
h₁ :
  norm (E := ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x))
      (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) x :
        ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x)) <
    1 +
      norm (E := ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x))
        (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) x :
          ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x))
⊢ norm (E := E x →L[ℝ] E y)
        (comp.{0, 0, 0, u_3, u_2, u_3} (R₂ := ℝ) (σ₁₂ := RingHom.id ℝ) (σ₂₃ := RingHom.id ℝ) (M₂ := F)
            (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) y)
            (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x) :
          E x →L[ℝ] E y) *
      norm (E := ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x))
        (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) x :
          ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x)) <
    2 *
      (1 +
        norm (E := ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x))
          (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) x :
            ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x)))

Tactic:
gcongr
-- Module: Mathlib.Topology.VectorBundle.Riemannian
Goal:
B : Type u_1
inst : TopologicalSpace B
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : B → Type u_3
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → NormedAddCommGroup (E x)
inst_5 : (x : B) → InnerProductSpace ℝ (E x)
inst_6 : FiberBundle F E
inst_7 : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x y : B
hy :
  norm (E := E x →L[ℝ] E y)
      (comp.{0, 0, 0, u_3, u_2, u_3} (R₂ := ℝ) (σ₁₂ := RingHom.id ℝ) (σ₂₃ := RingHom.id ℝ) (M₂ := F)
          (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) y)
          (Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x) :
        E x →L[ℝ] E y) <
    2
A :
  Eq (α := F →L[ℝ] F)
    ((Trivialization.continuousLinearMapAt ℝ (E := E) (trivializationAt F E x) x :
        ContinuousLinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F) ∘SL
      (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) x :
        ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x)))
    (ContinuousLinearMap.id ℝ F)
this :
  Eq (α := ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E y))
    (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) y :
      ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E y))
    (comp (σ₂₃ := RingHom.id ℝ) (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) y)
        (ContinuousLinearMap.id ℝ F) :
      ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E y))
linarith :
  1 +
        norm (E := ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x))
          (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) x :
            ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x)) ≤
      norm (E := ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x))
        (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) x :
          ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x)) →
    -1 +
        (1 +
            norm (E := ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x))
              (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) x :
                ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x)) -
          norm (E := ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x))
            (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) x :
              ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x))) =
      0
⊢ norm (E := ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x))
      (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) x :
        ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x)) <
    1 +
      norm (E := ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x))
        (Trivialization.symmL ℝ (E := E) (trivializationAt F E x) x :
          ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) F (E x))

Tactic:
linarith
-- Module: Mathlib.Topology.VectorBundle.Riemannian
Goal:
B_1 : Type u_1
inst : TopologicalSpace B_1
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace ℝ F_1
E_1 : B_1 → Type u_3
inst_3 : TopologicalSpace (TotalSpace F_1 E_1)
inst_4 : (x : B_1) → NormedAddCommGroup (E_1 x)
inst_5 : (x : B_1) → InnerProductSpace ℝ (E_1 x)
inst_6 : FiberBundle F_1 E_1
inst_7 : VectorBundle ℝ F_1 E_1
B : Type u_4
inst_8 : TopologicalSpace B
F : Type u_5
inst_9 : NormedAddCommGroup F
inst_10 : NormedSpace ℝ F
E : B → Type u_6
inst_11 : TopologicalSpace (TotalSpace F E)
inst_12 : (b : B) → TopologicalSpace (E b)
inst_13 : (b : B) → AddCommGroup (E b)
inst_14 : (b : B) → Module ℝ (E b)
inst_15 : ∀ (b : B), IsTopologicalAddGroup.{u_6} (E b)
inst_16 : ∀ (b : B), ContinuousConstSMul.{0, u_6} ℝ (E b)
inst_17 : FiberBundle F E
inst_18 : VectorBundle ℝ F E
g : RiemannianMetric E
b : B
v : E b
inl :
  LE.le (α := ℝ) (0 : ℝ)
    ((RCLike.re : (a : ℝ) → ℝ)
        ((((g.inner (E := E) b : (a : E b) → E b →L[ℝ] ℝ) 0 : E b →L[ℝ] ℝ) : (a : E b) → ℝ) 0 : ℝ) :
      ℝ)
inr :
  ∀ (hv : v ≠ 0),
    LE.le (α := ℝ) (0 : ℝ)
      ((RCLike.re : (a : ℝ) → ℝ)
          ((((g.inner (E := E) b : (a : E b) → E b →L[ℝ] ℝ) v : E b →L[ℝ] ℝ) : (a : E b) → ℝ) v : ℝ) :
        ℝ)
⊢ LE.le (α := ℝ) (0 : ℝ)
    ((RCLike.re : (a : ℝ) → ℝ)
        ((((g.inner (E := E) b : (a : E b) → E b →L[ℝ] ℝ) v : E b →L[ℝ] ℝ) : (a : E b) → ℝ) v : ℝ) :
      ℝ)

Tactic:
rcases eq_or_ne v 0 with rfl | hv

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Topology.VectorBundle.Riemannian
Goal:
B_1 : Type u_1
inst : TopologicalSpace B_1
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace ℝ F_1
E_1 : B_1 → Type u_3
inst_3 : TopologicalSpace (TotalSpace F_1 E_1)
inst_4 : (x : B_1) → NormedAddCommGroup (E_1 x)
inst_5 : (x : B_1) → InnerProductSpace ℝ (E_1 x)
inst_6 : FiberBundle F_1 E_1
inst_7 : VectorBundle ℝ F_1 E_1
B : Type u_4
inst_8 : TopologicalSpace B
F : Type u_5
inst_9 : NormedAddCommGroup F
inst_10 : NormedSpace ℝ F
E : B → Type u_6
inst_11 : TopologicalSpace (TotalSpace F E)
inst_12 : (b : B) → TopologicalSpace (E b)
inst_13 : (b : B) → AddCommGroup (E b)
inst_14 : (b : B) → Module ℝ (E b)
inst_15 : ∀ (b : B), IsTopologicalAddGroup.{u_6} (E b)
inst_16 : ∀ (b : B), ContinuousConstSMul.{0, u_6} ℝ (E b)
inst_17 : FiberBundle F E
inst_18 : VectorBundle ℝ F E
g : RiemannianMetric E
b : B
⊢ LE.le (α := ℝ) (0 : ℝ)
    ((RCLike.re : (a : ℝ) → ℝ)
        ((((g.inner (E := E) b : (a : E b) → E b →L[ℝ] ℝ) 0 : E b →L[ℝ] ℝ) : (a : E b) → ℝ) 0 : ℝ) :
      ℝ)

Tactic:
simp
-- Module: Mathlib.Topology.VectorBundle.Riemannian
Goal:
B_1 : Type u_1
inst : TopologicalSpace B_1
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace ℝ F_1
E_1 : B_1 → Type u_3
inst_3 : TopologicalSpace (TotalSpace F_1 E_1)
inst_4 : (x : B_1) → NormedAddCommGroup (E_1 x)
inst_5 : (x : B_1) → InnerProductSpace ℝ (E_1 x)
inst_6 : FiberBundle F_1 E_1
inst_7 : VectorBundle ℝ F_1 E_1
B : Type u_4
inst_8 : TopologicalSpace B
F : Type u_5
inst_9 : NormedAddCommGroup F
inst_10 : NormedSpace ℝ F
E : B → Type u_6
inst_11 : TopologicalSpace (TotalSpace F E)
inst_12 : (b : B) → TopologicalSpace (E b)
inst_13 : (b : B) → AddCommGroup (E b)
inst_14 : (b : B) → Module ℝ (E b)
inst_15 : ∀ (b : B), IsTopologicalAddGroup.{u_6} (E b)
inst_16 : ∀ (b : B), ContinuousConstSMul.{0, u_6} ℝ (E b)
inst_17 : FiberBundle F E
inst_18 : VectorBundle ℝ F E
g : RiemannianMetric E
b : B
v : E b
hv : v ≠ 0
⊢ LE.le (α := ℝ) (0 : ℝ)
    ((RCLike.re : (a : ℝ) → ℝ)
        ((((g.inner (E := E) b : (a : E b) → E b →L[ℝ] ℝ) v : E b →L[ℝ] ℝ) : (a : E b) → ℝ) v : ℝ) :
      ℝ)

Tactic:
simpa using (g.pos b v hv).le

Premises used: LT.lt.le, Bundle.RiemannianMetric.pos
-- Module: Mathlib.Topology.VectorBundle.Riemannian
Goal:
B_1 : Type u_1
inst : TopologicalSpace B_1
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace ℝ F_1
E_1 : B_1 → Type u_3
inst_3 : TopologicalSpace (TotalSpace F_1 E_1)
inst_4 : (x : B_1) → NormedAddCommGroup (E_1 x)
inst_5 : (x : B_1) → InnerProductSpace ℝ (E_1 x)
inst_6 : FiberBundle F_1 E_1
inst_7 : VectorBundle ℝ F_1 E_1
B : Type u_4
inst_8 : TopologicalSpace B
F : Type u_5
inst_9 : NormedAddCommGroup F
inst_10 : NormedSpace ℝ F
E : B → Type u_6
inst_11 : TopologicalSpace (TotalSpace F E)
inst_12 : (b : B) → TopologicalSpace (E b)
inst_13 : (b : B) → AddCommGroup (E b)
inst_14 : (b : B) → Module ℝ (E b)
inst_15 : ∀ (b : B), IsTopologicalAddGroup.{u_6} (E b)
inst_16 : ∀ (b : B), ContinuousConstSMul.{0, u_6} ℝ (E b)
inst_17 : FiberBundle F E
inst_18 : VectorBundle ℝ F E
g : RiemannianMetric E
b : B
v w x : E b
⊢ (((g.inner (E := E) b : (a : E b) → E b →L[ℝ] ℝ) (v + w) : E b →L[ℝ] ℝ) : (a : E b) → ℝ) x =
    HAdd.hAdd (α := ℝ) (β := ℝ)
      ((((g.inner (E := E) b : (a : E b) → E b →L[ℝ] ℝ) v : E b →L[ℝ] ℝ) : (a : E b) → ℝ) x : ℝ)
      ((((g.inner (E := E) b : (a : E b) → E b →L[ℝ] ℝ) w : E b →L[ℝ] ℝ) : (a : E b) → ℝ) x : ℝ)

Tactic:
simp
-- Module: Mathlib.Topology.VectorBundle.Riemannian
Goal:
B_1 : Type u_1
inst : TopologicalSpace B_1
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace ℝ F_1
E_1 : B_1 → Type u_3
inst_3 : TopologicalSpace (TotalSpace F_1 E_1)
inst_4 : (x : B_1) → NormedAddCommGroup (E_1 x)
inst_5 : (x : B_1) → InnerProductSpace ℝ (E_1 x)
inst_6 : FiberBundle F_1 E_1
inst_7 : VectorBundle ℝ F_1 E_1
B : Type u_4
inst_8 : TopologicalSpace B
F : Type u_5
inst_9 : NormedAddCommGroup F
inst_10 : NormedSpace ℝ F
E : B → Type u_6
inst_11 : TopologicalSpace (TotalSpace F E)
inst_12 : (b : B) → TopologicalSpace (E b)
inst_13 : (b : B) → AddCommGroup (E b)
inst_14 : (b : B) → Module ℝ (E b)
inst_15 : ∀ (b : B), IsTopologicalAddGroup.{u_6} (E b)
inst_16 : ∀ (b : B), ContinuousConstSMul.{0, u_6} ℝ (E b)
inst_17 : FiberBundle F E
inst_18 : VectorBundle ℝ F E
g : RiemannianMetric E
b : B
c v : E b
⊢ ∀ (r : ℝ),
    (((g.inner (E := E) b : (a : E b) → E b →L[ℝ] ℝ) (r • c) : E b →L[ℝ] ℝ) : (a : E b) → ℝ) v =
      HMul.hMul (α := ℝ) (β := ℝ) ((starRingEnd ℝ : (a : ℝ) → ℝ) r : ℝ)
        ((((g.inner (E := E) b : (a : E b) → E b →L[ℝ] ℝ) c : E b →L[ℝ] ℝ) : (a : E b) → ℝ) v : ℝ)

Tactic:
simp
-- Module: Mathlib.Topology.VectorBundle.Riemannian
Goal:
B_1 : Type u_1
inst : TopologicalSpace B_1
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace ℝ F_1
E_1 : B_1 → Type u_3
inst_3 : TopologicalSpace (TotalSpace F_1 E_1)
inst_4 : (x : B_1) → NormedAddCommGroup (E_1 x)
inst_5 : (x : B_1) → InnerProductSpace ℝ (E_1 x)
inst_6 : FiberBundle F_1 E_1
inst_7 : VectorBundle ℝ F_1 E_1
B : Type u_4
inst_8 : TopologicalSpace B
F : Type u_5
inst_9 : NormedAddCommGroup F
inst_10 : NormedSpace ℝ F
E : B → Type u_6
inst_11 : TopologicalSpace (TotalSpace F E)
inst_12 : (b : B) → TopologicalSpace (E b)
inst_13 : (b : B) → AddCommGroup (E b)
inst_14 : (b : B) → Module ℝ (E b)
inst_15 : ∀ (b : B), IsTopologicalAddGroup.{u_6} (E b)
inst_16 : ∀ (b : B), ContinuousConstSMul.{0, u_6} ℝ (E b)
inst_17 : FiberBundle F E
inst_18 : VectorBundle ℝ F E
g : RiemannianMetric E
b : B
v : E b
h : Eq (α := ℝ) ((((g.inner (E := E) b : (a : E b) → E b →L[ℝ] ℝ) v : E b →L[ℝ] ℝ) : (a : E b) → ℝ) v : ℝ) (0 : ℝ)
contrapose! :
  ∀ (h : v ≠ 0),
    Ne (α := ℝ) ((((g.inner (E := E) b : (a : E b) → E b →L[ℝ] ℝ) v : E b →L[ℝ] ℝ) : (a : E b) → ℝ) v : ℝ) (0 : ℝ)
⊢ v = 0

Tactic:
contrapose! h
-- Module: Mathlib.Topology.VectorBundle.Riemannian
Goal:
B_1 : Type u_1
inst : TopologicalSpace B_1
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace ℝ F_1
E_1 : B_1 → Type u_3
inst_3 : TopologicalSpace (TotalSpace F_1 E_1)
inst_4 : (x : B_1) → NormedAddCommGroup (E_1 x)
inst_5 : (x : B_1) → InnerProductSpace ℝ (E_1 x)
inst_6 : FiberBundle F_1 E_1
inst_7 : VectorBundle ℝ F_1 E_1
B : Type u_4
inst_8 : TopologicalSpace B
F : Type u_5
inst_9 : NormedAddCommGroup F
inst_10 : NormedSpace ℝ F
E : B → Type u_6
inst_11 : TopologicalSpace (TotalSpace F E)
inst_12 : (b : B) → TopologicalSpace (E b)
inst_13 : (b : B) → AddCommGroup (E b)
inst_14 : (b : B) → Module ℝ (E b)
inst_15 : ∀ (b : B), IsTopologicalAddGroup.{u_6} (E b)
inst_16 : ∀ (b : B), ContinuousConstSMul.{0, u_6} ℝ (E b)
inst_17 : FiberBundle F E
inst_18 : VectorBundle ℝ F E
g : RiemannianMetric E
b : B
v : E b
h : v ≠ 0
⊢ Ne (α := ℝ) ((((g.inner (E := E) b : (a : E b) → E b →L[ℝ] ℝ) v : E b →L[ℝ] ℝ) : (a : E b) → ℝ) v : ℝ) (0 : ℝ)

Tactic:
(g.pos b v h).ne'

Premises used: LT.lt.ne', Bundle.RiemannianMetric.pos
-- Module: Mathlib.Topology.VectorBundle.Riemannian
Goal:
B_1 : Type u_1
inst : TopologicalSpace B_1
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace ℝ F_1
E_1 : B_1 → Type u_3
inst_3 : TopologicalSpace (TotalSpace F_1 E_1)
inst_4 : (x : B_1) → NormedAddCommGroup (E_1 x)
inst_5 : (x : B_1) → InnerProductSpace ℝ (E_1 x)
inst_6 : FiberBundle F_1 E_1
inst_7 : VectorBundle ℝ F_1 E_1
B : Type u_4
inst_8 : TopologicalSpace B
F : Type u_5
inst_9 : NormedAddCommGroup F
inst_10 : NormedSpace ℝ F
E : B → Type u_6
inst_11 : TopologicalSpace (TotalSpace F E)
inst_12 : (b : B) → TopologicalSpace (E b)
inst_13 : (b : B) → AddCommGroup (E b)
inst_14 : (b : B) → Module ℝ (E b)
inst_15 : ∀ (b : B), IsTopologicalAddGroup.{u_6} (E b)
inst_16 : ∀ (b : B), ContinuousConstSMul.{0, u_6} ℝ (E b)
inst_17 : FiberBundle F E
inst_18 : VectorBundle ℝ F E
g : RiemannianMetric E
b : B
v : E b
h : v ≠ 0
⊢ Ne (α := ℝ) ((((g.inner (E := E) b : (a : E b) → E b →L[ℝ] ℝ) v : E b →L[ℝ] ℝ) : (a : E b) → ℝ) v : ℝ) (0 : ℝ)

Tactic:
exact (g.pos b v h).ne'

Premises used: LT.lt.ne', Bundle.RiemannianMetric.pos
-- Module: Mathlib.Topology.VectorBundle.Riemannian
Goal:
B_1 : Type u_1
inst : TopologicalSpace B_1
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace ℝ F_1
E_1 : B_1 → Type u_3
inst_3 : TopologicalSpace (TotalSpace F_1 E_1)
inst_4 : (x : B_1) → NormedAddCommGroup (E_1 x)
inst_5 : (x : B_1) → InnerProductSpace ℝ (E_1 x)
inst_6 : FiberBundle F_1 E_1
inst_7 : VectorBundle ℝ F_1 E_1
B : Type u_4
inst_8 : TopologicalSpace B
F : Type u_5
inst_9 : NormedAddCommGroup F
inst_10 : NormedSpace ℝ F
E : B → Type u_6
inst_11 : TopologicalSpace (TotalSpace F E)
inst_12 : (b : B) → TopologicalSpace (E b)
inst_13 : (b : B) → AddCommGroup (E b)
inst_14 : (b : B) → Module ℝ (E b)
inst_15 : ∀ (b : B), IsTopologicalAddGroup.{u_6} (E b)
inst_16 : ∀ (b : B), ContinuousConstSMul.{0, u_6} ℝ (E b)
inst_17 : FiberBundle F E
inst_18 : VectorBundle ℝ F E
g : ContinuousRiemannianMetric F E
b : B
e : ContinuousLinearEquiv.{0, 0, u_6, u_5} (RingHom.id ℝ) (E b) F :=
  Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E b) b ⋯
m : ContinuousLinearEquiv.{0, 0, u_6, u_5} (RingHom.id ℝ) (E b →L[ℝ] E b →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) :=
  e.arrowCongr (e.arrowCongr (ContinuousLinearEquiv.refl ℝ ℝ))
v : E b
⊢ Eq (α := ℝ) ((((g.inner (E := E) b : (a : E b) → E b →L[ℝ] ℝ) v : E b →L[ℝ] ℝ) : (a : E b) → ℝ) v : ℝ)
    (((fun (w : F) ↦
            (((((m : (a : E b →L[ℝ] E b →L[ℝ] ℝ) → F →L[ℝ] F →L[ℝ] ℝ) (g.inner (E := E) b) : F →L[ℝ] F →L[ℝ] ℝ) :
                      (a : F) → F →L[ℝ] ℝ)
                    w :
                  F →L[ℝ] ℝ) :
                (a : F) → ℝ)
              w) ∘
          (⇑e : (a : E b) → F))
        v :
      ℝ)

Tactic:
simp [m]
-- Module: Mathlib.Topology.VectorBundle.Riemannian
Goal:
B_1 : Type u_1
inst : TopologicalSpace B_1
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace ℝ F_1
E_1 : B_1 → Type u_3
inst_3 : TopologicalSpace (TotalSpace F_1 E_1)
inst_4 : (x : B_1) → NormedAddCommGroup (E_1 x)
inst_5 : (x : B_1) → InnerProductSpace ℝ (E_1 x)
inst_6 : FiberBundle F_1 E_1
inst_7 : VectorBundle ℝ F_1 E_1
B : Type u_4
inst_8 : TopologicalSpace B
F : Type u_5
inst_9 : NormedAddCommGroup F
inst_10 : NormedSpace ℝ F
E : B → Type u_6
inst_11 : TopologicalSpace (TotalSpace F E)
inst_12 : (b : B) → TopologicalSpace (E b)
inst_13 : (b : B) → AddCommGroup (E b)
inst_14 : (b : B) → Module ℝ (E b)
inst_15 : ∀ (b : B), IsTopologicalAddGroup.{u_6} (E b)
inst_16 : ∀ (b : B), ContinuousConstSMul.{0, u_6} ℝ (E b)
inst_17 : FiberBundle F E
inst_18 : VectorBundle ℝ F E
g : ContinuousRiemannianMetric F E
b : B
e : ContinuousLinearEquiv.{0, 0, u_6, u_5} (RingHom.id ℝ) (E b) F :=
  Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E b) b ⋯
m : ContinuousLinearEquiv.{0, 0, u_6, u_5} (RingHom.id ℝ) (E b →L[ℝ] E b →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) :=
  e.arrowCongr (e.arrowCongr (ContinuousLinearEquiv.refl ℝ ℝ))
⊢ ∀ (v : E b),
    Eq (α := ℝ) ((((g.inner (E := E) b : (a : E b) → E b →L[ℝ] ℝ) v : E b →L[ℝ] ℝ) : (a : E b) → ℝ) v : ℝ)
      (((fun (w : F) ↦
              (((((m : (a : E b →L[ℝ] E b →L[ℝ] ℝ) → F →L[ℝ] F →L[ℝ] ℝ) (g.inner (E := E) b) : F →L[ℝ] F →L[ℝ] ℝ) :
                        (a : F) → F →L[ℝ] ℝ)
                      w :
                    F →L[ℝ] ℝ) :
                  (a : F) → ℝ)
                w) ∘
            (⇑e : (a : E b) → F))
          v :
        ℝ)

Tactic:
have A (v : E b) : g.inner b v v = ((fun w ↦ m (g.inner b) w w) ∘ e) v := by simp [m]
-- Module: Mathlib.Topology.VectorBundle.Riemannian
Goal:
B_1 : Type u_1
inst : TopologicalSpace B_1
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace ℝ F_1
E_1 : B_1 → Type u_3
inst_3 : TopologicalSpace (TotalSpace F_1 E_1)
inst_4 : (x : B_1) → NormedAddCommGroup (E_1 x)
inst_5 : (x : B_1) → InnerProductSpace ℝ (E_1 x)
inst_6 : FiberBundle F_1 E_1
inst_7 : VectorBundle ℝ F_1 E_1
B : Type u_4
inst_8 : TopologicalSpace B
F : Type u_5
inst_9 : NormedAddCommGroup F
inst_10 : NormedSpace ℝ F
E : B → Type u_6
inst_11 : TopologicalSpace (TotalSpace F E)
inst_12 : (b : B) → TopologicalSpace (E b)
inst_13 : (b : B) → AddCommGroup (E b)
inst_14 : (b : B) → Module ℝ (E b)
inst_15 : ∀ (b : B), IsTopologicalAddGroup.{u_6} (E b)
inst_16 : ∀ (b : B), ContinuousConstSMul.{0, u_6} ℝ (E b)
inst_17 : FiberBundle F E
inst_18 : VectorBundle ℝ F E
g : ContinuousRiemannianMetric F E
b : B
e : ContinuousLinearEquiv.{0, 0, u_6, u_5} (RingHom.id ℝ) (E b) F :=
  Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E b) b ⋯
m : ContinuousLinearEquiv.{0, 0, u_6, u_5} (RingHom.id ℝ) (E b →L[ℝ] E b →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) :=
  e.arrowCongr (e.arrowCongr (ContinuousLinearEquiv.refl ℝ ℝ))
A :
  ∀ (v : E b),
    Eq (α := ℝ) ((((g.inner (E := E) b : (a : E b) → E b →L[ℝ] ℝ) v : E b →L[ℝ] ℝ) : (a : E b) → ℝ) v : ℝ)
      (((fun (w : F) ↦
              (((((m : (a : E b →L[ℝ] E b →L[ℝ] ℝ) → F →L[ℝ] F →L[ℝ] ℝ) (g.inner (E := E) b) : F →L[ℝ] F →L[ℝ] ℝ) :
                        (a : F) → F →L[ℝ] ℝ)
                      w :
                    F →L[ℝ] ℝ) :
                  (a : F) → ℝ)
                w) ∘
            (⇑e : (a : E b) → F))
          v :
        ℝ)
simp :
  ContinuousAt (Y := ℝ)
    (fun (v : E b) ↦
      ((fun (w : F) ↦
            (((((m : (a : E b →L[ℝ] E b →L[ℝ] ℝ) → F →L[ℝ] F →L[ℝ] ℝ) (g.inner (E := E) b) : F →L[ℝ] F →L[ℝ] ℝ) :
                      (a : F) → F →L[ℝ] ℝ)
                    w :
                  F →L[ℝ] ℝ) :
                (a : F) → ℝ)
              w) ∘
          (⇑e : (a : E b) → F))
        v)
    0
⊢ ContinuousAt (Y := ℝ)
    (fun (v : E b) ↦ (((g.inner (E := E) b : (a : E b) → E b →L[ℝ] ℝ) v : E b →L[ℝ] ℝ) : (a : E b) → ℝ) v) 0

Tactic:
simp only [A]