awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
n_1 : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s s' : ι → (x : M) → V x
u u' : Set M
x : M
n : ℕ∞ω
inst_13 : VectorBundle 𝕜 F V
inst_14 : FiniteDimensional 𝕜 F
hs : IsLocalFrameOn I F (V := V) n s u
hx : x ∈ u
⊢ Fintype ι
have this : FiniteDimensional.{u_1, u_6} 𝕜 (V x)
Tactic: have : FiniteDimensional 𝕜 (V x) := by
    let phi := (trivializationAt F V x).linearEquivAt 𝕜 x
      (FiberBundle.mem_baseSet_trivializationAt' x)
    exact Finite.equiv phi.symm
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
inst_13 : Finite ι
hs : IsLocalFrameOn I F (V := V) n s u
hx : x ∈ u
t t' : (x : M) → V x
h :
  ∀ (i : ι),
    Eq.{u_1 + 1} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
      ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t' x) : 𝕜)
this : Fintype ι := Fintype.ofFinite ι
⊢ t x = t' x
have t₁ : Eq.{u_6 + 1} (α := V x)
  (∑ i : ι, HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜) (s i x))
  (∑ i : ι, HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t' x) : 𝕜) (s i x))
Tactic: calc
    t x = ∑ i, hs.coeff i x (t x) • (s i x) := hs.coeff_sum_eq t hx
    _ = ∑ i, hs.coeff i x (t' x) • (s i x) := by simp [h]
    _ = t' x := (hs.coeff_sum_eq t' hx).symm
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
t t' : (x : M) → V x
hs : IsLocalFrameOn I F (V := V) n s u
htt' : t x = t' x
i : ι
⊢ Eq.{u_1 + 1} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
    ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t' x) : 𝕜)
have pos : ∀ (hxe : x ∈ u),
  Eq.{u_1 + 1} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
    ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t' x) : 𝕜)
Tactic: by_cases hxe : x ∈ u
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
t t' : (x : M) → V x
hs : IsLocalFrameOn I F (V := V) n s u
htt' : t x = t' x
i : ι
pos :
  ∀ (hxe : x ∈ u),
    Eq.{u_1 + 1} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
      ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t' x) : 𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
    ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t' x) : 𝕜)
have neg : ∀ (hxe : x ∉ u),
  Eq.{u_1 + 1} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
    ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t' x) : 𝕜)
Tactic: by_cases hxe : x ∈ u
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s s' : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
hs : IsLocalFrameOn I F (V := V) n s u
hs' : IsLocalFrameOn I F (V := V) n s' u
hss' : ∀ (i : ι), s i x = s' i x
t : (x : M) → V x
i : ι
⊢ Eq.{u_1 + 1} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
    ((hs'.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
have pos : ∀ (hxe : x ∈ u),
  Eq.{u_1 + 1} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
    ((hs'.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
Tactic: by_cases hxe : x ∈ u
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s s' : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
hs : IsLocalFrameOn I F (V := V) n s u
hs' : IsLocalFrameOn I F (V := V) n s' u
hss' : ∀ (i : ι), s i x = s' i x
t : (x : M) → V x
i : ι
pos :
  ∀ (hxe : x ∈ u),
    Eq.{u_1 + 1} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
      ((hs'.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
    ((hs'.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
have neg : ∀ (hxe : x ∉ u),
  Eq.{u_1 + 1} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
    ((hs'.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
Tactic: by_cases hxe : x ∈ u
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s s' : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
hs : IsLocalFrameOn I F (V := V) n s u
hs' : IsLocalFrameOn I F (V := V) n s' u
hss' : ∀ (i : ι), s i x = s' i x
t : (x : M) → V x
i : ι
hxe : x ∈ u
⊢ Eq.{u_1 + 1} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
    ((hs'.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
have pos : Eq.{u_1 + 1} (α := 𝕜)
  (((((hs.toBasisAt (V := V) (u := u) sorry).repr : (a : V x) → ι →₀ 𝕜) (t x) : ι →₀ 𝕜) : (a : ι) → 𝕜) i : 𝕜)
  (((((hs'.toBasisAt (V := V) (u := u) sorry).repr : (a : V x) → ι →₀ 𝕜) (t x) : ι →₀ 𝕜) : (a : ι) → 𝕜) i : 𝕜)
Tactic: simp [coeff, hxe]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
t : (x : M) → V x
hs : IsLocalFrameOn I F (V := V) n s u
inst_13 : VectorBundle 𝕜 F V
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    ContMDiffOn I 𝓘(𝕜, 𝕜) (M' := 𝕜) n
      ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
              (hs.coeff (V := V) (u := u) i) :
            ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
          (a : (x : M) → V x) → M → 𝕜)
        t)
      u
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) u
have inl : ∀ (hs : IsLocalFrameOn I F (V := V) n s ∅)
  (h :
    ∀ (i : ι),
      ContMDiffOn.{u_1, u_2, u_3, u_4, u_1, u_1, u_1} I (M := M) 𝓘(𝕜, 𝕜) (M' := 𝕜) n
        ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
                (hs.coeff (V := V) (u := ∅) i) :
              ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
            (a : (x : M) → V x) → M → 𝕜)
          t)
        ∅),
  ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) ∅
Tactic: rcases u.eq_empty_or_nonempty with rfl | ⟨x, hx⟩
Cleared hypotheses: u, hs, h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
t : (x : M) → V x
hs : IsLocalFrameOn I F (V := V) n s u
inst_13 : VectorBundle 𝕜 F V
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    ContMDiffOn I 𝓘(𝕜, 𝕜) (M' := 𝕜) n
      ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
              (hs.coeff (V := V) (u := u) i) :
            ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
          (a : (x : M) → V x) → M → 𝕜)
        t)
      u
inl :
  ∀ (hs : IsLocalFrameOn I F (V := V) n s ∅)
    (h :
      ∀ (i : ι),
        ContMDiffOn.{u_1, u_2, u_3, u_4, u_1, u_1, u_1} I (M := M) 𝓘(𝕜, 𝕜) (M' := 𝕜) n
          ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
                  (hs.coeff (V := V) (u := ∅) i) :
                ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
              (a : (x : M) → V x) → M → 𝕜)
            t)
          ∅),
    ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) ∅
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) u
have inr : ∀ (x : M) (hx : x ∈ u), ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) u
Tactic: rcases u.eq_empty_or_nonempty with rfl | ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
t : (x : M) → V x
hs : IsLocalFrameOn I F (V := V) n s u
inst_13 : VectorBundle 𝕜 F V
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    ContMDiffOn I 𝓘(𝕜, 𝕜) (M' := 𝕜) n
      ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
              (hs.coeff (V := V) (u := u) i) :
            ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
          (a : (x : M) → V x) → M → 𝕜)
        t)
      u
x : M
hx : x ∈ u
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) u
have inr : ∀ (this : Fintype ι), ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) u
Tactic: have := fintypeOfFiniteDimensional hs hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
t : (x : M) → V x
hs : IsLocalFrameOn I F (V := V) n s u
inst_13 : VectorBundle 𝕜 F V
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    ContMDiffOn I 𝓘(𝕜, 𝕜) (M' := 𝕜) n
      ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
              (hs.coeff (V := V) (u := u) i) :
            ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
          (a : (x : M) → V x) → M → 𝕜)
        t)
      u
x : M
hx : x ∈ u
this : Fintype ι
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) u
have this₁ : ∀ (i : ι),
  ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n
    (fun (x : M) ↦
      ⟨x,
        HSMul.hSMul (α := M → 𝕜)
          ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
                    (hs.coeff (V := V) (u := u) i) :
                  ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
                (a : (x : M) → V x) → M → 𝕜)
              t :
            M → 𝕜)
          (s i) x⟩)
    u
Tactic: have this (i) : CMDiff[u] n (T% ((LinearMap.piApply (hs.coeff i)) t • s i)) :=
    (h i).smul_section (hs.contMDiffOn i)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
t : (x : M) → V x
hs : IsLocalFrameOn I F (V := V) n s u
inst_13 : VectorBundle 𝕜 F V
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    ContMDiffOn I 𝓘(𝕜, 𝕜) (M' := 𝕜) n
      ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
              (hs.coeff (V := V) (u := u) i) :
            ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
          (a : (x : M) → V x) → M → 𝕜)
        t)
      u
x : M
hx : x ∈ u
this_1 : Fintype ι
this :
  ∀ (i : ι),
    ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n
      (fun (x : M) ↦
        ⟨x,
          HSMul.hSMul (α := M → 𝕜)
            ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
                      (hs.coeff (V := V) (u := u) i) :
                    ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
                  (a : (x : M) → V x) → M → 𝕜)
                t :
              M → 𝕜)
            (s i) x⟩)
      u
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) u
have almost : ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n
  (fun (x : M) ↦
    ⟨x,
      ∑ i : ι,
        HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜)
          ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
                    (hs.coeff (V := V) (u := u) i) :
                  ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
                (a : (x : M) → V x) → M → 𝕜)
              t x :
            𝕜)
          (s i x)⟩)
  u
Tactic: have almost : CMDiff[u] n (T% (fun x ↦ ∑ i, ((LinearMap.piApply (hs.coeff i)) t) x • s i x)) :=
    .sum_section fun i _ ↦ this i
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
t : (x : M) → V x
hs : IsLocalFrameOn I F (V := V) n s u
inst_13 : VectorBundle 𝕜 F V
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    ContMDiffOn I 𝓘(𝕜, 𝕜) (M' := 𝕜) n
      ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
              (hs.coeff (V := V) (u := u) i) :
            ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
          (a : (x : M) → V x) → M → 𝕜)
        t)
      u
x : M
hx : x ∈ u
this_1 : Fintype ι
this :
  ∀ (i : ι),
    ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n
      (fun (x : M) ↦
        ⟨x,
          HSMul.hSMul (α := M → 𝕜)
            ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
                      (hs.coeff (V := V) (u := u) i) :
                    ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
                  (a : (x : M) → V x) → M → 𝕜)
                t :
              M → 𝕜)
            (s i) x⟩)
      u
almost :
  ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n
    (fun (x : M) ↦
      ⟨x,
        ∑ i : ι,
          HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜)
            ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
                      (hs.coeff (V := V) (u := u) i) :
                    ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
                  (a : (x : M) → V x) → M → 𝕜)
                t x :
              𝕜)
            (s i x)⟩)
    u
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) u
have inr : ∀ y ∈ u,
  ⟨y, t y⟩ =
    ⟨y,
      ∑ i : ι,
        HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜)
          ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
                    (hs.coeff (V := V) (u := u) i) :
                  ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
                (a : (x : M) → V x) → M → 𝕜)
              t y :
            𝕜)
          (s i y)⟩
Tactic: apply almost.congr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
t : (x : M) → V x
hs : IsLocalFrameOn I F (V := V) n s u
inst_13 : VectorBundle 𝕜 F V
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    ContMDiffAt I 𝓘(𝕜, 𝕜) (M' := 𝕜) n
      ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
              (hs.coeff (V := V) (u := u) i) :
            ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
          (a : (x : M) → V x) → M → 𝕜)
        t)
      x
hu : u ∈ 𝓝 x
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) x
have have : ∀ (this : Fintype ι), ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) x
Tactic: have := fintypeOfFiniteDimensional hs (mem_of_mem_nhds hu)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
t : (x : M) → V x
hs : IsLocalFrameOn I F (V := V) n s u
inst_13 : VectorBundle 𝕜 F V
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    ContMDiffAt I 𝓘(𝕜, 𝕜) (M' := 𝕜) n
      ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
              (hs.coeff (V := V) (u := u) i) :
            ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
          (a : (x : M) → V x) → M → 𝕜)
        t)
      x
hu : u ∈ 𝓝 x
this : Fintype ι
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) x
have almost : ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n
  (fun (x : M) ↦
    ⟨x,
      ∑ i : ι,
        HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜)
          ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
                    (hs.coeff (V := V) (u := u) i) :
                  ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
                (a : (x : M) → V x) → M → 𝕜)
              t x :
            𝕜)
          (s i x)⟩)
  x
Tactic: have almost : CMDiffAt n (T% (fun x ↦ ∑ i, ((LinearMap.piApply (hs.coeff i)) t) x • s i x)) x :=
    .sum_section (fun i _ ↦ (h i).smul_section <| (hs.contMDiffOn i).contMDiffAt hu)