awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.FiniteExtension (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_4
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i_1 : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i_1 : L) (1 : L)
k : K
y : L
hk : ¬k = 0
i : ι
left : Membership.mem (γ := Finset ι) univ i
hi :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)) =
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)
j : ι
left_1 : Membership.mem (γ := Finset ι) univ j
hj :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K)
        ((((B.repr : (a : L) → ι →₀ K) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) : ι →₀ K) :
              (a : ι) → K)
            i :
          K)) =
    Norm.norm.{u_1} (E := K)
      ((((B.repr : (a : L) → ι →₀ K) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) : ι →₀ K) :
            (a : ι) → K)
          j :
        K)
hj' :
  Norm.norm.{u_1} (E := K)
      ((((B.repr : (a : L) → ι →₀ K) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) : ι →₀ K) :
            (a : ι) → K)
          i :
        K) ≤
    sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K)
        ((((B.repr : (a : L) → ι →₀ K) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) : ι →₀ K) :
              (a : ι) → K)
            i :
          K)
hj₁ :
  (sup' univ ⋯ fun (x : ι) ↦
      ‖k‖ * Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) x : K)) =
    ‖k‖ * Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) j : K)
⊢ B.norm y ≤ Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) j : K)
have hj'₁ : (‖k‖ *
    sup' univ sorry fun (i : ι) ↦
      Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)) ≤
  sup' univ sorry fun (x : ι) ↦
    ‖k‖ * Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) x : K)
Tactic: simp only [repr_smul', norm_mul, ← hi] at hj hj'
Cleared hypotheses: hj, hj'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.FiniteExtension (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_4
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i_1 : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i_1 : L) (1 : L)
k : K
y : L
hk : ¬k = 0
i : ι
left : Membership.mem (γ := Finset ι) univ i
hi :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)) =
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)
j : ι
left_1 : Membership.mem (γ := Finset ι) univ j
hj :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K)
        ((((B.repr : (a : L) → ι →₀ K) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) : ι →₀ K) :
              (a : ι) → K)
            i :
          K)) =
    Norm.norm.{u_1} (E := K)
      ((((B.repr : (a : L) → ι →₀ K) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) : ι →₀ K) :
            (a : ι) → K)
          j :
        K)
⊢ B.norm (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) = ‖k‖ * B.norm y
have hij : Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K) =
  Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) j : K)
Tactic: have hij : ‖B.repr y i‖ = ‖B.repr y j‖ := by
      rw [← hi]
      apply le_antisymm _ (norm_repr_le_norm B j)
      have hj' := Finset.le_sup' (fun i ↦ ‖B.repr ((algebraMap K L) k * y) i‖) (mem_univ i)
      simp only [repr_smul', norm_mul, ← hi] at hj hj'
      exact (mul_le_mul_iff_right₀ (lt_of_le_of_ne (norm_nonneg _)
        (Ne.symm (norm_ne_zero_iff.mpr hk)))).mp (hj ▸ hj')
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.FiniteExtension (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_4
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i_1 : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i_1 : L) (1 : L)
k : K
y : L
hk : ¬k = 0
i : ι
left : Membership.mem (γ := Finset ι) univ i
hi :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)) =
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)
j : ι
left_1 : Membership.mem (γ := Finset ι) univ j
hj :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K)
        ((((B.repr : (a : L) → ι →₀ K) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) : ι →₀ K) :
              (a : ι) → K)
            i :
          K)) =
    Norm.norm.{u_1} (E := K)
      ((((B.repr : (a : L) → ι →₀ K) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) : ι →₀ K) :
            (a : ι) → K)
          j :
        K)
hij :
  Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K) =
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) j : K)
⊢ B.norm (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) = ‖k‖ * B.norm y
have neg : Norm.norm.{u_1} (E := K)
    ((((B.repr : (a : L) → ι →₀ K) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) : ι →₀ K) :
          (a : ι) → K)
        j :
      K) =
  ‖k‖ *
    sup' univ sorry fun (i : ι) ↦ Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)
Tactic: simp only [norm, hj]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.FiniteExtension (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_4
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i_1 : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i_1 : L) (1 : L)
k : K
y : L
hk : ¬k = 0
i : ι
left : Membership.mem (γ := Finset ι) univ i
hi :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)) =
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)
j : ι
left_1 : Membership.mem (γ := Finset ι) univ j
hj :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K)
        ((((B.repr : (a : L) → ι →₀ K) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) : ι →₀ K) :
              (a : ι) → K)
            i :
          K)) =
    Norm.norm.{u_1} (E := K)
      ((((B.repr : (a : L) → ι →₀ K) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) : ι →₀ K) :
            (a : ι) → K)
          j :
        K)
hij :
  Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K) =
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) j : K)
⊢ Norm.norm.{u_1} (E := K)
      ((((B.repr : (a : L) → ι →₀ K) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) : ι →₀ K) :
            (a : ι) → K)
          j :
        K) =
    ‖k‖ *
      sup' univ ⋯ fun (i : ι) ↦
        Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)
have neg : ‖HMul.hMul (β := K) k ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) j : K)‖ =
  ‖k‖ *
    sup' univ sorry fun (i : ι) ↦ Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)
Tactic: rw [repr_smul', norm_mul, hi, hij]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.FiniteExtension (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_4
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i_1 : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i_1 : L) (1 : L)
k : K
y : L
hk : ¬k = 0
i : ι
left : Membership.mem (γ := Finset ι) univ i
hi :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)) =
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)
j : ι
left_1 : Membership.mem (γ := Finset ι) univ j
hj :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K)
        ((((B.repr : (a : L) → ι →₀ K) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) : ι →₀ K) :
              (a : ι) → K)
            i :
          K)) =
    Norm.norm.{u_1} (E := K)
      ((((B.repr : (a : L) → ι →₀ K) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) : ι →₀ K) :
            (a : ι) → K)
          j :
        K)
hij :
  Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K) =
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) j : K)
neg :
  ‖HMul.hMul (β := K) k ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) j : K)‖ =
    ‖k‖ *
      sup' univ ⋯ fun (i : ι) ↦
        Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)
⊢ Norm.norm.{u_1} (E := K)
      ((((B.repr : (a : L) → ι →₀ K) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) : ι →₀ K) :
            (a : ι) → K)
          j :
        K) =
    ‖k‖ *
      sup' univ ⋯ fun (i : ι) ↦
        Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)
have neg₁ : ‖k‖ * Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) j : K) =
  ‖k‖ *
    sup' univ sorry fun (i : ι) ↦ Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)
Tactic: rw [repr_smul', norm_mul, hi, hij]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.FiniteExtension (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_4
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i_1 : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i_1 : L) (1 : L)
k : K
y : L
hk : ¬k = 0
i : ι
left : Membership.mem (γ := Finset ι) univ i
hi :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)) =
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)
j : ι
left_1 : Membership.mem (γ := Finset ι) univ j
hj :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K)
        ((((B.repr : (a : L) → ι →₀ K) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) : ι →₀ K) :
              (a : ι) → K)
            i :
          K)) =
    Norm.norm.{u_1} (E := K)
      ((((B.repr : (a : L) → ι →₀ K) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) : ι →₀ K) :
            (a : ι) → K)
          j :
        K)
hij :
  Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K) =
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) j : K)
neg :
  ‖HMul.hMul (β := K) k ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) j : K)‖ =
    ‖k‖ *
      sup' univ ⋯ fun (i : ι) ↦
        Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)
neg₁ :
  ‖k‖ * Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) j : K) =
    ‖k‖ *
      sup' univ ⋯ fun (i : ι) ↦
        Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)
⊢ Norm.norm.{u_1} (E := K)
      ((((B.repr : (a : L) → ι →₀ K) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) : ι →₀ K) :
            (a : ι) → K)
          j :
        K) =
    ‖k‖ *
      sup' univ ⋯ fun (i : ι) ↦
        Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)
have neg₂ : ‖k‖ * Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) j : K) =
  ‖k‖ * Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)
Tactic: rw [repr_smul', norm_mul, hi, hij]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.FiniteExtension (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_4
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i_1 : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i_1 : L) (1 : L)
k : K
y : L
hk : ¬k = 0
i : ι
left : Membership.mem (γ := Finset ι) univ i
hi :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)) =
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)
j : ι
left_1 : Membership.mem (γ := Finset ι) univ j
hj :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K)
        ((((B.repr : (a : L) → ι →₀ K) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) : ι →₀ K) :
              (a : ι) → K)
            i :
          K)) =
    Norm.norm.{u_1} (E := K)
      ((((B.repr : (a : L) → ι →₀ K) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) : ι →₀ K) :
            (a : ι) → K)
          j :
        K)
hij :
  Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K) =
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) j : K)
neg :
  ‖HMul.hMul (β := K) k ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) j : K)‖ =
    ‖k‖ *
      sup' univ ⋯ fun (i : ι) ↦
        Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)
neg₁ :
  ‖k‖ * Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) j : K) =
    ‖k‖ *
      sup' univ ⋯ fun (i : ι) ↦
        Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)
neg₂ :
  ‖k‖ * Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) j : K) =
    ‖k‖ * Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)
⊢ Norm.norm.{u_1} (E := K)
      ((((B.repr : (a : L) → ι →₀ K) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) : ι →₀ K) :
            (a : ι) → K)
          j :
        K) =
    ‖k‖ *
      sup' univ ⋯ fun (i : ι) ↦
        Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)
have neg₃ : ‖k‖ * Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) j : K) =
  ‖k‖ * Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) j : K)
Tactic: rw [repr_smul', norm_mul, hi, hij]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.FiniteExtension (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Field L
inst_2 : Algebra K L
hfd : FiniteDimensional K L
hna : IsNonarchimedean.{0, u_1} (α := K) norm
⊢ ∃ (f : AlgebraNorm K L),
    IsPowMul (R := L) (⇑f : (a : L) → ℝ) ∧
      (∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖) ∧
        IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
have h1 : LinearIndepOn (ι := L) K id {1}
Tactic: have h1 : LinearIndepOn K id ({1} : Set L) := .singleton one_ne_zero
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.FiniteExtension (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Field L
inst_2 : Algebra K L
hfd : FiniteDimensional K L
hna : IsNonarchimedean.{0, u_1} (α := K) norm
h1 : LinearIndepOn (ι := L) K id {1}
ι : Type u_2 :=
  { x : L //
    Membership.mem (γ := Set L)
      (LinearIndepOn.extend.{u_2, u_2, u_1} (K := K) (V := L) (v := id) (s := {1}) (t := Set.univ) h1 ⋯) x }
B : Basis ι K L := Basis.extend (s := {1}) h1
hfin : Fintype ι := FiniteDimensional.fintypeBasisIndex.{u_1, u_2, u_2} (K := K) (V := L) B
⊢ ∃ (f : AlgebraNorm K L),
    IsPowMul (R := L) (⇑f : (a : L) → ℝ) ∧
      (∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖) ∧
        IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
have hem : Nonempty ι
Tactic: haveI hem : Nonempty ι := B.index_nonempty
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.FiniteExtension (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Field L
inst_2 : Algebra K L
hfd : FiniteDimensional K L
hna : IsNonarchimedean.{0, u_1} (α := K) norm
h1 : LinearIndepOn (ι := L) K id {1}
ι : Type u_2 :=
  { x : L //
    Membership.mem (γ := Set L)
      (LinearIndepOn.extend.{u_2, u_2, u_1} (K := K) (V := L) (v := id) (s := {1}) (t := Set.univ) h1 ⋯) x }
B : Basis ι K L := Basis.extend (s := {1}) h1
hfin : Fintype ι := FiniteDimensional.fintypeBasisIndex.{u_1, u_2, u_2} (K := K) (V := L) B
hem : Nonempty ι
⊢ ∃ (f : AlgebraNorm K L),
    IsPowMul (R := L) (⇑f : (a : L) → ℝ) ∧
      (∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖) ∧
        IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
have h1L : Membership.mem (γ := Set L)
  (LinearIndepOn.extend.{u_2, u_2, u_1} (K := K) (V := L) (v := id) (s := {1}) (t := Set.univ) h1 sorry) 1
Tactic: have h1L : (1 : L) ∈ LinearIndepOn.extend h1 _ :=
    Basis.subset_extend _ (Set.mem_singleton (1 : L))
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.FiniteExtension (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Field L
inst_2 : Algebra K L
hfd : FiniteDimensional K L
hna : IsNonarchimedean.{0, u_1} (α := K) norm
h1 : LinearIndepOn (ι := L) K id {1}
ι : Type u_2 :=
  { x : L //
    Membership.mem (γ := Set L)
      (LinearIndepOn.extend.{u_2, u_2, u_1} (K := K) (V := L) (v := id) (s := {1}) (t := Set.univ) h1 ⋯) x }
B : Basis ι K L := Basis.extend (s := {1}) h1
hfin : Fintype ι := FiniteDimensional.fintypeBasisIndex.{u_1, u_2, u_2} (K := K) (V := L) B
hem : Nonempty ι
h1L :
  Membership.mem (γ := Set L)
    (LinearIndepOn.extend.{u_2, u_2, u_1} (K := K) (V := L) (v := id) (s := {1}) (t := Set.univ) h1 ⋯) 1
⊢ ∃ (f : AlgebraNorm K L),
    IsPowMul (R := L) (⇑f : (a : L) → ℝ) ∧
      (∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖) ∧
        IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
have hB1 : Eq (α := L)
  ((B : (a : ι) → L)
      (Subtype.mk (p := fun (x : L) ↦
        Membership.mem (γ := Set L)
          (LinearIndepOn.extend.{u_2, u_2, u_1} (K := K) (V := L) (v := id) (s := {1}) (t := Set.univ) h1 sorry) x)
        1 h1L) :
    L)
  (1 : L)
Tactic: have hB1 : B ⟨1, h1L⟩ = (1 : L) := by rw [Basis.coe_extend, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.FiniteExtension (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Field L
inst_2 : Algebra K L
hfd : FiniteDimensional K L
hna : IsNonarchimedean.{0, u_1} (α := K) norm
h1 : LinearIndepOn (ι := L) K id {1}
ι : Type u_2 :=
  { x : L //
    Membership.mem (γ := Set L)
      (LinearIndepOn.extend.{u_2, u_2, u_1} (K := K) (V := L) (v := id) (s := {1}) (t := Set.univ) h1 ⋯) x }
B : Basis ι K L := Basis.extend (s := {1}) h1
hfin : Fintype ι := FiniteDimensional.fintypeBasisIndex.{u_1, u_2, u_2} (K := K) (V := L) B
hem : Nonempty ι
h1L :
  Membership.mem (γ := Set L)
    (LinearIndepOn.extend.{u_2, u_2, u_1} (K := K) (V := L) (v := id) (s := {1}) (t := Set.univ) h1 ⋯) 1
hB1 :
  Eq (α := L)
    ((B : (a : ι) → L)
        (Subtype.mk (p := fun (x : L) ↦
          Membership.mem (γ := Set L)
            (LinearIndepOn.extend.{u_2, u_2, u_1} (K := K) (V := L) (v := id) (s := {1}) (t := Set.univ) h1 ⋯) x)
          1 h1L) :
      L)
    (1 : L)
g : L → ℝ := B.norm
⊢ ∃ (f : AlgebraNorm K L),
    IsPowMul (R := L) (⇑f : (a : L) → ℝ) ∧
      (∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖) ∧
        IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
have hg0 : g 0 = 0
Tactic: have hg0 : g 0 = 0 := B.norm_zero
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.FiniteExtension (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Field L
inst_2 : Algebra K L
hfd : FiniteDimensional K L
hna : IsNonarchimedean.{0, u_1} (α := K) norm
h1 : LinearIndepOn (ι := L) K id {1}
ι : Type u_2 :=
  { x : L //
    Membership.mem (γ := Set L)
      (LinearIndepOn.extend.{u_2, u_2, u_1} (K := K) (V := L) (v := id) (s := {1}) (t := Set.univ) h1 ⋯) x }
B : Basis ι K L := Basis.extend (s := {1}) h1
hfin : Fintype ι := FiniteDimensional.fintypeBasisIndex.{u_1, u_2, u_2} (K := K) (V := L) B
hem : Nonempty ι
h1L :
  Membership.mem (γ := Set L)
    (LinearIndepOn.extend.{u_2, u_2, u_1} (K := K) (V := L) (v := id) (s := {1}) (t := Set.univ) h1 ⋯) 1
hB1 :
  Eq (α := L)
    ((B : (a : ι) → L)
        (Subtype.mk (p := fun (x : L) ↦
          Membership.mem (γ := Set L)
            (LinearIndepOn.extend.{u_2, u_2, u_1} (K := K) (V := L) (v := id) (s := {1}) (t := Set.univ) h1 ⋯) x)
          1 h1L) :
      L)
    (1 : L)
g : L → ℝ := B.norm
hg0 : g 0 = 0
x : L
⊢ 0 ≤ g x
have simp : LE.le (α := ℝ) 0
  (sup' univ sorry fun (i : ι) ↦ norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K))
Tactic: simp only [g, Basis.norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.FiniteExtension (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Field L
inst_2 : Algebra K L
hfd : FiniteDimensional K L
hna : IsNonarchimedean.{0, u_1} (α := K) norm
h1 : LinearIndepOn (ι := L) K id {1}
ι : Type u_2 :=
  { x : L //
    Membership.mem (γ := Set L)
      (LinearIndepOn.extend.{u_2, u_2, u_1} (K := K) (V := L) (v := id) (s := {1}) (t := Set.univ) h1 ⋯) x }
B : Basis ι K L := Basis.extend (s := {1}) h1
hfin : Fintype ι := FiniteDimensional.fintypeBasisIndex.{u_1, u_2, u_2} (K := K) (V := L) B
hem : Nonempty ι
h1L :
  Membership.mem (γ := Set L)
    (LinearIndepOn.extend.{u_2, u_2, u_1} (K := K) (V := L) (v := id) (s := {1}) (t := Set.univ) h1 ⋯) 1
hB1 :
  Eq (α := L)
    ((B : (a : ι) → L)
        (Subtype.mk (p := fun (x : L) ↦
          Membership.mem (γ := Set L)
            (LinearIndepOn.extend.{u_2, u_2, u_1} (K := K) (V := L) (v := id) (s := {1}) (t := Set.univ) h1 ⋯) x)
          1 h1L) :
      L)
    (1 : L)
g : L → ℝ := B.norm
hg0 : g 0 = 0
⊢ ∃ (f : AlgebraNorm K L),
    IsPowMul (R := L) (⇑f : (a : L) → ℝ) ∧
      (∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖) ∧
        IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
have hg_nonneg : ∀ (x : L), 0 ≤ g x
Tactic: have hg_nonneg : ∀ x : L, 0 ≤ g x := fun x ↦ by simp only [g, Basis.norm]; simp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.FiniteExtension (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Field L
inst_2 : Algebra K L
hfd : FiniteDimensional K L
hna : IsNonarchimedean.{0, u_1} (α := K) norm
h1 : LinearIndepOn (ι := L) K id {1}
ι : Type u_2 :=
  { x : L //
    Membership.mem (γ := Set L)
      (LinearIndepOn.extend.{u_2, u_2, u_1} (K := K) (V := L) (v := id) (s := {1}) (t := Set.univ) h1 ⋯) x }
B : Basis ι K L := Basis.extend (s := {1}) h1
hfin : Fintype ι := FiniteDimensional.fintypeBasisIndex.{u_1, u_2, u_2} (K := K) (V := L) B
hem : Nonempty ι
h1L :
  Membership.mem (γ := Set L)
    (LinearIndepOn.extend.{u_2, u_2, u_1} (K := K) (V := L) (v := id) (s := {1}) (t := Set.univ) h1 ⋯) 1
hB1 :
  Eq (α := L)
    ((B : (a : ι) → L)
        (Subtype.mk (p := fun (x : L) ↦
          Membership.mem (γ := Set L)
            (LinearIndepOn.extend.{u_2, u_2, u_1} (K := K) (V := L) (v := id) (s := {1}) (t := Set.univ) h1 ⋯) x)
          1 h1L) :
      L)
    (1 : L)
g : L → ℝ := B.norm
hg0 : g 0 = 0
hg_nonneg : ∀ (x : L), 0 ≤ g x
⊢ ∃ (f : AlgebraNorm K L),
    IsPowMul (R := L) (⇑f : (a : L) → ℝ) ∧
      (∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖) ∧
        IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
have hg_ext : ∀ (x : K), g ((algebraMap K L : (a : K) → L) x) = ‖x‖
Tactic: have hg_ext : ∀ (x : K), g ((algebraMap K L) x) = ‖x‖ := Basis.norm_extends hB1