awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (goal)
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 : B
⊢ ∃ C > 0,
    ∀ᶠ (y : B) in 𝓝 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)) <
        C
have refine : ∀ᶠ (y : B) in 𝓝 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: refine ⟨2 * (1 + ‖(trivializationAt F E x).symmL ℝ x‖), by positivity, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (goal)
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 : B
⊢ ∀ᶠ (y : B) in 𝓝 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)))
have h₁ : ∀ (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),
  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: filter_upwards [eventually_norm_symmL_trivializationAt_comp_self_lt F E x one_lt_two] with y hy
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (goal)
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
⊢ 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)
have h₁ : ∀ (v : F),
  Eq (α := 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)) :
          (a : F) → F)
        v :
      F)
    ((ContinuousLinearMap.id ℝ F : (a : F) → F) v : F)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (hypothesis)
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
v : F
⊢ Eq (α := 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)) :
          (a : F) → F)
        v :
      F)
    ((ContinuousLinearMap.id ℝ F : (a : F) → F) v : F)
have h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
Tactic: have h'x : x ∈ (trivializationAt F E x).baseSet := FiberBundle.mem_baseSet_trivializationAt' x
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (goal)
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
v : F
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
⊢ Eq (α := 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)) :
          (a : F) → F)
        v :
      F)
    ((ContinuousLinearMap.id ℝ F : (a : F) → F) v : F)
have h₁ : ((Trivialization.linearMapAt ℝ (E := E) (trivializationAt F E x) x :
        LinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F) :
      (a : E x) → F)
    (Trivialization.symm (E := E) (trivializationAt F E x) x v) =
  v
Tactic: simp only [coe_comp', Trivialization.continuousLinearMapAt_apply, Trivialization.symmL_apply,
      Function.comp_apply, coe_id', id_eq]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (goal)
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
v : F
h'x : x ∈ Trivialization.baseSet (trivializationAt F E x)
⊢ ((Trivialization.linearMapAt ℝ (E := E) (trivializationAt F E x) x :
          LinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F) :
        (a : E x) → F)
      (Trivialization.symm (E := E) (trivializationAt F E x) x v) =
    v
have h₁ : Eq (α := (a : E x) → F)
  (⇑(Trivialization.linearMapAt ℝ (E := E) (trivializationAt F E x) x :
        LinearMap.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F) :
    (a : E x) → F)
  (⇑(Trivialization.continuousLinearEquivAt ℝ (E := E) (trivializationAt F E x) x h'x :
        ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (E x) F) :
    (a : E x) → F)
Tactic: convert! ((trivializationAt F E x).continuousLinearEquivAt ℝ _ h'x).apply_symm_apply v
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (hypothesis)
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
⊢ 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)))
have 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)
Tactic: have A : ((trivializationAt F E x).continuousLinearMapAt ℝ x) ∘L
      ((trivializationAt F E x).symmL ℝ x) = ContinuousLinearMap.id _ _ := by
    ext v
    have h'x : x ∈ (trivializationAt F E x).baseSet := FiberBundle.mem_baseSet_trivializationAt' x
    simp only [coe_comp', Trivialization.continuousLinearMapAt_apply, Trivialization.symmL_apply,
      Function.comp_apply, coe_id', id_eq]
    convert! ((trivializationAt F E x).continuousLinearEquivAt ℝ _ h'x).apply_symm_apply v
    simp [Trivialization.coe_continuousLinearEquivAt_eq _ h'x]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (hypothesis)
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)
⊢ 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)))
have 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))
Tactic: have : (trivializationAt F E x).symmL ℝ y =
     ((trivializationAt F E x).symmL ℝ y) ∘L (ContinuousLinearMap.id _ _) := by simp
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (goal)
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))
⊢ 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)))
have 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)))
Tactic: grw [this, ← A, ← comp_assoc, opNorm_comp_le]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (goal)
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))
⊢ 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)))
have 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))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (goal)
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))
⊢ 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))
have 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Riemannian (goal)
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
⊢ 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 : ℝ) :
      ℝ)
have 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 : ℝ) :
    ℝ)
Tactic: rcases eq_or_ne v 0 with rfl | hv
Cleared hypotheses: v