awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace 𝕜
ι : Type u_1
inst_4 : Finite ι
i₀ : ι
ι' : Type (max 0 u_1) := { x : ι // x ≠ i₀ }
⊢ IsOpen[Pi.topologicalSpace]
    {p : ι → E | LinearIndependent.{u_1, u, v} 𝕜 (M := E) fun (i : { x : ι // x ≠ i₀ }) ↦ p (↑i : ι) -ᵥ p i₀}
have inr : ∀ (val : Fintype ι),
  IsOpen[Pi.topologicalSpace]
    {p : ι → E | LinearIndependent.{u_1, u, v} 𝕜 (M := E) fun (i : { x : ι // x ≠ i₀ }) ↦ p (↑i : ι) -ᵥ p i₀}
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace 𝕜
ι : Type u_1
inst_4 : Finite ι
i₀ : ι
ι' : Type (max 0 u_1) := { x : ι // x ≠ i₀ }
val : Fintype ι
⊢ IsOpen[Pi.topologicalSpace]
    {p : ι → E | LinearIndependent.{u_1, u, v} 𝕜 (M := E) fun (i : { x : ι // x ≠ i₀ }) ↦ p (↑i : ι) -ᵥ p i₀}
have inr : ∀ (this : Fintype ι'),
  IsOpen[Pi.topologicalSpace]
    {p : ι → E | LinearIndependent.{u_1, u, v} 𝕜 (M := E) fun (i : { x : ι // x ≠ i₀ }) ↦ p (↑i : ι) -ᵥ p i₀}
Tactic: haveI : Fintype ι' := Subtype.fintype _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace 𝕜
ι : Type u_1
inst_4 : Finite ι
i₀ : ι
ι' : Type (max 0 u_1) := { x : ι // x ≠ i₀ }
val : Fintype ι
this : Fintype ι'
⊢ IsOpen[Pi.topologicalSpace]
    {p : ι → E | LinearIndependent.{u_1, u, v} 𝕜 (M := E) fun (i : { x : ι // x ≠ i₀ }) ↦ p (↑i : ι) -ᵥ p i₀}
have inr : IsOpen[Pi.topologicalSpace]
  (preimage (β := (i : ι') → E) (fun (p : ι → E) (i : ι') ↦ p (↑i : ι) -ᵥ p i₀) {p : ι' → E | LinearIndependent 𝕜 p})
Tactic: convert_to
      IsOpen ((fun (p : ι → E) (i : ι') ↦ p i -ᵥ p i₀) ⁻¹' {p : ι' → E | LinearIndependent 𝕜 p})
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace 𝕜
ι : Type u_1
inst_4 : Finite ι
⊢ IsOpen[Pi.topologicalSpace] {p : ι → E | AffineIndependent 𝕜 p}
have inl : ∀ (h : IsEmpty ι), IsOpen[Pi.topologicalSpace] {p : ι → E | AffineIndependent 𝕜 p}
Tactic: classical
  rcases isEmpty_or_nonempty ι with h | ⟨⟨i₀⟩⟩
  · exact isOpen_discrete _
  · simp_rw [affineIndependent_iff_linearIndependent_vsub 𝕜 _ i₀]
    let ι' := { x // x ≠ i₀ }
    cases nonempty_fintype ι
    haveI : Fintype ι' := Subtype.fintype _
    convert_to
      IsOpen ((fun (p : ι → E) (i : ι') ↦ p i -ᵥ p i₀) ⁻¹' {p : ι' → E | LinearIndependent 𝕜 p})
    exact isOpen_setOf_linearIndependent.preimage (by fun_prop)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace 𝕜
ι : Type u_1
inst_4 : Finite ι
inl : ∀ (h : IsEmpty ι), IsOpen[Pi.topologicalSpace] {p : ι → E | AffineIndependent 𝕜 p}
⊢ IsOpen[Pi.topologicalSpace] {p : ι → E | AffineIndependent 𝕜 p}
have inr : ∀ (i₀ : ι), IsOpen[Pi.topologicalSpace] {p : ι → E | AffineIndependent 𝕜 p}
Tactic: classical
  rcases isEmpty_or_nonempty ι with h | ⟨⟨i₀⟩⟩
  · exact isOpen_discrete _
  · simp_rw [affineIndependent_iff_linearIndependent_vsub 𝕜 _ i₀]
    let ι' := { x // x ≠ i₀ }
    cases nonempty_fintype ι
    haveI : Fintype ι' := Subtype.fintype _
    convert_to
      IsOpen ((fun (p : ι → E) (i : ι') ↦ p i -ᵥ p i₀) ⁻¹' {p : ι' → E | LinearIndependent 𝕜 p})
    exact isOpen_setOf_linearIndependent.preimage (by fun_prop)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
ι : Type u_1
inst_6 : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := (↑v.equivFunL : E →L[𝕜] ι → 𝕜)
⊢ nnnorm.{w} (E := F) ((u : (a : E) → F) e : F) =
    nnnorm.{w} (E := F)
      ((u : (a : E) → F)
          (∑ i : ι,
            HSMul.hSMul.{u, v, v} (α := 𝕜) (β := E) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
              ((v : (a : ι) → E) i : E)) :
        F)
have rw : nnnorm.{w} (E := F) ((u : (a : E) → F) e : F) = nnnorm.{w} (E := F) ((u : (a : E) → F) e : F)
Tactic: rw [v.sum_equivFun]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
ι : Type u_1
inst_6 : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := (↑v.equivFunL : E →L[𝕜] ι → 𝕜)
⊢ LE.le (α := ℝ≥0)
    (∑ i : ι,
      nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) *
        nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F))
    (∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) * M)
have h : ∀ (i : ι),
  Membership.mem (γ := Finset ι) Finset.univ i →
    nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
ι : Type u_1
inst_6 : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := (↑v.equivFunL : E →L[𝕜] ι → 𝕜)
⊢ ∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) * M =
    (∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)) * M
have rw : Eq (α := ℝ≥0) (∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) * M)
  (∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) * M)
Tactic: rw [Finset.sum_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
ι : Type u_1
inst_6 : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := (↑v.equivFunL : E →L[𝕜] ι → 𝕜)
⊢ (∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)) * M ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) * M
have bc : ∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
ι : Type u_1
inst_6 : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := (↑v.equivFunL : E →L[𝕜] ι → 𝕜)
⊢ nnnorm.{w} (E := F) ((u : (a : E) → F) e : F) ≤ Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊
have e₁ : nnnorm.{w} (E := F) ((u : (a : E) → F) e : F) =
  nnnorm.{w} (E := F)
    ((u : (a : E) → F)
        (∑ i : ι,
          HSMul.hSMul.{u, v, v} (α := 𝕜) (β := E) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) ((v : (a : ι) → E) i : E)) :
      F)
Tactic: calc
      ‖u e‖₊ = ‖u (∑ i, v.equivFun e i • v i)‖₊ := by rw [v.sum_equivFun]
      _ = ‖∑ i, v.equivFun e i • (u <| v i)‖₊ := by simp only [equivFun_apply, map_sum, map_smul]
      _ ≤ ∑ i, ‖v.equivFun e i • (u <| v i)‖₊ := nnnorm_sum_le _ _
      _ = ∑ i, ‖v.equivFun e i‖₊ * ‖u (v i)‖₊ := by simp only [nnnorm_smul]
      _ ≤ ∑ i, ‖v.equivFun e i‖₊ * M := by gcongr; apply hu
      _ = (∑ i, ‖v.equivFun e i‖₊) * M := by rw [Finset.sum_mul]
      _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) * M := by
        gcongr
        calc
          ∑ i, ‖v.equivFun e i‖₊ ≤ Fintype.card ι • ‖φ e‖₊ := Pi.sum_nnnorm_apply_le_nnnorm _
          _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) := nsmul_le_nsmul_right (φ.le_opNNNorm e) _
      _ = Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊ := by simp only [smul_mul_assoc, mul_right_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
ι : Type u_1
inst_6 : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := (↑v.equivFunL : E →L[𝕜] ι → 𝕜)
e₁ :
  nnnorm.{w} (E := F) ((u : (a : E) → F) e : F) =
    nnnorm.{w} (E := F)
      ((u : (a : E) → F)
          (∑ i : ι,
            HSMul.hSMul.{u, v, v} (α := 𝕜) (β := E) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
              ((v : (a : ι) → E) i : E)) :
        F)
⊢ nnnorm.{w} (E := F) ((u : (a : E) → F) e : F) ≤ Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊
have e₂ : nnnorm.{w} (E := F)
    ((u : (a : E) → F)
        (∑ i : ι,
          HSMul.hSMul.{u, v, v} (α := 𝕜) (β := E) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) ((v : (a : ι) → E) i : E)) :
      F) =
  nnnorm.{w} (E := F)
    (∑ i : ι,
      HSMul.hSMul.{u, w, w} (α := 𝕜) (β := F) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
        ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F))
Tactic: calc
      ‖u e‖₊ = ‖u (∑ i, v.equivFun e i • v i)‖₊ := by rw [v.sum_equivFun]
      _ = ‖∑ i, v.equivFun e i • (u <| v i)‖₊ := by simp only [equivFun_apply, map_sum, map_smul]
      _ ≤ ∑ i, ‖v.equivFun e i • (u <| v i)‖₊ := nnnorm_sum_le _ _
      _ = ∑ i, ‖v.equivFun e i‖₊ * ‖u (v i)‖₊ := by simp only [nnnorm_smul]
      _ ≤ ∑ i, ‖v.equivFun e i‖₊ * M := by gcongr; apply hu
      _ = (∑ i, ‖v.equivFun e i‖₊) * M := by rw [Finset.sum_mul]
      _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) * M := by
        gcongr
        calc
          ∑ i, ‖v.equivFun e i‖₊ ≤ Fintype.card ι • ‖φ e‖₊ := Pi.sum_nnnorm_apply_le_nnnorm _
          _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) := nsmul_le_nsmul_right (φ.le_opNNNorm e) _
      _ = Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊ := by simp only [smul_mul_assoc, mul_right_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
ι : Type u_1
inst_6 : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := (↑v.equivFunL : E →L[𝕜] ι → 𝕜)
e₁ :
  nnnorm.{w} (E := F) ((u : (a : E) → F) e : F) =
    nnnorm.{w} (E := F)
      ((u : (a : E) → F)
          (∑ i : ι,
            HSMul.hSMul.{u, v, v} (α := 𝕜) (β := E) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
              ((v : (a : ι) → E) i : E)) :
        F)
e₂ :
  nnnorm.{w} (E := F)
      ((u : (a : E) → F)
          (∑ i : ι,
            HSMul.hSMul.{u, v, v} (α := 𝕜) (β := E) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
              ((v : (a : ι) → E) i : E)) :
        F) =
    nnnorm.{w} (E := F)
      (∑ i : ι,
        HSMul.hSMul.{u, w, w} (α := 𝕜) (β := F) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
          ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F))
⊢ nnnorm.{w} (E := F) ((u : (a : E) → F) e : F) ≤ Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊
have e₃ : Eq (α := ℝ≥0)
  (∑ i : ι,
    ‖HSMul.hSMul.{u, w, w} (α := 𝕜) (β := F) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
        ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F)‖₊)
  (∑ i : ι,
    nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) *
      nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F))
Tactic: calc
      ‖u e‖₊ = ‖u (∑ i, v.equivFun e i • v i)‖₊ := by rw [v.sum_equivFun]
      _ = ‖∑ i, v.equivFun e i • (u <| v i)‖₊ := by simp only [equivFun_apply, map_sum, map_smul]
      _ ≤ ∑ i, ‖v.equivFun e i • (u <| v i)‖₊ := nnnorm_sum_le _ _
      _ = ∑ i, ‖v.equivFun e i‖₊ * ‖u (v i)‖₊ := by simp only [nnnorm_smul]
      _ ≤ ∑ i, ‖v.equivFun e i‖₊ * M := by gcongr; apply hu
      _ = (∑ i, ‖v.equivFun e i‖₊) * M := by rw [Finset.sum_mul]
      _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) * M := by
        gcongr
        calc
          ∑ i, ‖v.equivFun e i‖₊ ≤ Fintype.card ι • ‖φ e‖₊ := Pi.sum_nnnorm_apply_le_nnnorm _
          _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) := nsmul_le_nsmul_right (φ.le_opNNNorm e) _
      _ = Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊ := by simp only [smul_mul_assoc, mul_right_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
ι : Type u_1
inst_6 : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := (↑v.equivFunL : E →L[𝕜] ι → 𝕜)
e₁ :
  nnnorm.{w} (E := F) ((u : (a : E) → F) e : F) =
    nnnorm.{w} (E := F)
      ((u : (a : E) → F)
          (∑ i : ι,
            HSMul.hSMul.{u, v, v} (α := 𝕜) (β := E) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
              ((v : (a : ι) → E) i : E)) :
        F)
e₂ :
  nnnorm.{w} (E := F)
      ((u : (a : E) → F)
          (∑ i : ι,
            HSMul.hSMul.{u, v, v} (α := 𝕜) (β := E) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
              ((v : (a : ι) → E) i : E)) :
        F) =
    nnnorm.{w} (E := F)
      (∑ i : ι,
        HSMul.hSMul.{u, w, w} (α := 𝕜) (β := F) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
          ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F))
e₃ :
  Eq (α := ℝ≥0)
    (∑ i : ι,
      ‖HSMul.hSMul.{u, w, w} (α := 𝕜) (β := F) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
          ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F)‖₊)
    (∑ i : ι,
      nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) *
        nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F))
⊢ nnnorm.{w} (E := F) ((u : (a : E) → F) e : F) ≤ Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊
have e₄ : LE.le (α := ℝ≥0)
  (∑ i : ι,
    nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) *
      nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F))
  (∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) * M)
Tactic: calc
      ‖u e‖₊ = ‖u (∑ i, v.equivFun e i • v i)‖₊ := by rw [v.sum_equivFun]
      _ = ‖∑ i, v.equivFun e i • (u <| v i)‖₊ := by simp only [equivFun_apply, map_sum, map_smul]
      _ ≤ ∑ i, ‖v.equivFun e i • (u <| v i)‖₊ := nnnorm_sum_le _ _
      _ = ∑ i, ‖v.equivFun e i‖₊ * ‖u (v i)‖₊ := by simp only [nnnorm_smul]
      _ ≤ ∑ i, ‖v.equivFun e i‖₊ * M := by gcongr; apply hu
      _ = (∑ i, ‖v.equivFun e i‖₊) * M := by rw [Finset.sum_mul]
      _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) * M := by
        gcongr
        calc
          ∑ i, ‖v.equivFun e i‖₊ ≤ Fintype.card ι • ‖φ e‖₊ := Pi.sum_nnnorm_apply_le_nnnorm _
          _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) := nsmul_le_nsmul_right (φ.le_opNNNorm e) _
      _ = Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊ := by simp only [smul_mul_assoc, mul_right_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
ι : Type u_1
inst_6 : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := (↑v.equivFunL : E →L[𝕜] ι → 𝕜)
e₁ :
  nnnorm.{w} (E := F) ((u : (a : E) → F) e : F) =
    nnnorm.{w} (E := F)
      ((u : (a : E) → F)
          (∑ i : ι,
            HSMul.hSMul.{u, v, v} (α := 𝕜) (β := E) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
              ((v : (a : ι) → E) i : E)) :
        F)
e₂ :
  nnnorm.{w} (E := F)
      ((u : (a : E) → F)
          (∑ i : ι,
            HSMul.hSMul.{u, v, v} (α := 𝕜) (β := E) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
              ((v : (a : ι) → E) i : E)) :
        F) =
    nnnorm.{w} (E := F)
      (∑ i : ι,
        HSMul.hSMul.{u, w, w} (α := 𝕜) (β := F) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
          ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F))
e₃ :
  Eq (α := ℝ≥0)
    (∑ i : ι,
      ‖HSMul.hSMul.{u, w, w} (α := 𝕜) (β := F) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
          ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F)‖₊)
    (∑ i : ι,
      nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) *
        nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F))
e₄ :
  LE.le (α := ℝ≥0)
    (∑ i : ι,
      nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) *
        nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F))
    (∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) * M)
⊢ nnnorm.{w} (E := F) ((u : (a : E) → F) e : F) ≤ Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊
have e₅ : ∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) * M =
  (∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)) * M
Tactic: calc
      ‖u e‖₊ = ‖u (∑ i, v.equivFun e i • v i)‖₊ := by rw [v.sum_equivFun]
      _ = ‖∑ i, v.equivFun e i • (u <| v i)‖₊ := by simp only [equivFun_apply, map_sum, map_smul]
      _ ≤ ∑ i, ‖v.equivFun e i • (u <| v i)‖₊ := nnnorm_sum_le _ _
      _ = ∑ i, ‖v.equivFun e i‖₊ * ‖u (v i)‖₊ := by simp only [nnnorm_smul]
      _ ≤ ∑ i, ‖v.equivFun e i‖₊ * M := by gcongr; apply hu
      _ = (∑ i, ‖v.equivFun e i‖₊) * M := by rw [Finset.sum_mul]
      _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) * M := by
        gcongr
        calc
          ∑ i, ‖v.equivFun e i‖₊ ≤ Fintype.card ι • ‖φ e‖₊ := Pi.sum_nnnorm_apply_le_nnnorm _
          _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) := nsmul_le_nsmul_right (φ.le_opNNNorm e) _
      _ = Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊ := by simp only [smul_mul_assoc, mul_right_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
ι : Type u_1
inst_6 : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := (↑v.equivFunL : E →L[𝕜] ι → 𝕜)
e₁ :
  nnnorm.{w} (E := F) ((u : (a : E) → F) e : F) =
    nnnorm.{w} (E := F)
      ((u : (a : E) → F)
          (∑ i : ι,
            HSMul.hSMul.{u, v, v} (α := 𝕜) (β := E) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
              ((v : (a : ι) → E) i : E)) :
        F)
e₂ :
  nnnorm.{w} (E := F)
      ((u : (a : E) → F)
          (∑ i : ι,
            HSMul.hSMul.{u, v, v} (α := 𝕜) (β := E) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
              ((v : (a : ι) → E) i : E)) :
        F) =
    nnnorm.{w} (E := F)
      (∑ i : ι,
        HSMul.hSMul.{u, w, w} (α := 𝕜) (β := F) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
          ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F))
e₃ :
  Eq (α := ℝ≥0)
    (∑ i : ι,
      ‖HSMul.hSMul.{u, w, w} (α := 𝕜) (β := F) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
          ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F)‖₊)
    (∑ i : ι,
      nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) *
        nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F))
e₄ :
  LE.le (α := ℝ≥0)
    (∑ i : ι,
      nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) *
        nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F))
    (∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) * M)
e₅ :
  ∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) * M =
    (∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)) * M
⊢ nnnorm.{w} (E := F) ((u : (a : E) → F) e : F) ≤ Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊
have e₆ : (∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)) * M ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) * M
Tactic: calc
      ‖u e‖₊ = ‖u (∑ i, v.equivFun e i • v i)‖₊ := by rw [v.sum_equivFun]
      _ = ‖∑ i, v.equivFun e i • (u <| v i)‖₊ := by simp only [equivFun_apply, map_sum, map_smul]
      _ ≤ ∑ i, ‖v.equivFun e i • (u <| v i)‖₊ := nnnorm_sum_le _ _
      _ = ∑ i, ‖v.equivFun e i‖₊ * ‖u (v i)‖₊ := by simp only [nnnorm_smul]
      _ ≤ ∑ i, ‖v.equivFun e i‖₊ * M := by gcongr; apply hu
      _ = (∑ i, ‖v.equivFun e i‖₊) * M := by rw [Finset.sum_mul]
      _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) * M := by
        gcongr
        calc
          ∑ i, ‖v.equivFun e i‖₊ ≤ Fintype.card ι • ‖φ e‖₊ := Pi.sum_nnnorm_apply_le_nnnorm _
          _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) := nsmul_le_nsmul_right (φ.le_opNNNorm e) _
      _ = Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊ := by simp only [smul_mul_assoc, mul_right_comm]