awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
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 : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i : L) (1 : L)
k : K
y : L
hk : ¬k = 0
neg :
  ∀ (i : ι),
    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)),
        B.norm (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) = ‖k‖ * B.norm y
⊢ B.norm (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) = ‖k‖ * B.norm y

Tactic:
obtain ⟨i, _, hi⟩ := exists_mem_eq_sup' univ_nonempty (fun i ↦ ‖B.repr y i‖)

Premises used: Norm.norm, Finset.univ_nonempty, Module.Basis.repr, Finset.exists_mem_eq_sup', DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
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)
neg :
  ∀ (j : ι),
    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
⊢ B.norm (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) = ‖k‖ * B.norm y

Tactic:
obtain ⟨j, _, hj⟩ := exists_mem_eq_sup' univ_nonempty
      (fun i ↦ ‖B.repr ((algebraMap K L) k * y) i‖)

Premises used: Norm.norm, HMul.hMul, Algebra.algebraMap, Finset.univ_nonempty, Module.Basis.repr, Finset.exists_mem_eq_sup', DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
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)
rw :
  (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) j : 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) y : ι →₀ K) : (a : ι) → K) j : K)

Tactic:
rw [← hi]
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
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)
apply : B.norm y ≤ Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) j : 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) y : ι →₀ K) : (a : ι) → K) j : K)

Tactic:
apply le_antisymm _ (norm_repr_le_norm B j)

Premises used: le_antisymm, Module.Basis.norm_repr_le_norm
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
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)
⊢ 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)

Tactic:
have hj' := Finset.le_sup' (fun i ↦ ‖B.repr ((algebraMap K L) k * y) i‖) (mem_univ i)
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
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)
⊢ (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)

Tactic:
simp only [repr_smul', norm_mul, ← hi] at hj hj'

Premises used: norm_mul, Module.Basis.repr_smul'
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
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)
⊢ (‖k‖ *
      sup' univ ⋯ fun (i : ι) ↦
        Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)) ≤
    sup' univ ⋯ 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'

Premises used: norm_mul, Module.Basis.repr_smul'
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
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 (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)
hj' :
  (‖k‖ *
      sup' univ ⋯ fun (i : ι) ↦
        Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)) ≤
    sup' univ ⋯ fun (x : ι) ↦
      ‖k‖ * Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) x : K)
⊢ B.norm y ≤ Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) j : K)

Tactic:
(mul_le_mul_iff_right₀ (lt_of_le_of_ne (norm_nonneg _)
        (Ne.symm (norm_ne_zero_iff.mpr hk)))).mp (hj ▸ hj')

Premises used: Iff.mpr, Eq.rec, Ne.symm, norm_ne_zero_iff, Iff.mp, norm_nonneg, lt_of_le_of_ne, mul_le_mul_iff_right₀
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
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 (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)
hj' :
  (‖k‖ *
      sup' univ ⋯ fun (i : ι) ↦
        Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K)) ≤
    sup' univ ⋯ fun (x : ι) ↦
      ‖k‖ * Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) x : K)
⊢ B.norm y ≤ Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) j : K)

Tactic:
exact (mul_le_mul_iff_right₀ (lt_of_le_of_ne (norm_nonneg _)
        (Ne.symm (norm_ne_zero_iff.mpr hk)))).mp (hj ▸ hj')

Premises used: Iff.mpr, Ne.symm, norm_ne_zero_iff, Iff.mp, norm_nonneg, lt_of_le_of_ne, mul_le_mul_iff_right₀
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
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)
⊢ 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')
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
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 :
  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)
⊢ B.norm (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) = ‖k‖ * B.norm y

Tactic:
simp only [norm, hj]

Premises used: Module.Basis.norm
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
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)
neg₃ 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)
⊢ 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)

Tactic:
rw [repr_smul', norm_mul, hi, hij]

Premises used: norm_mul, Module.Basis.repr_smul'
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
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
⊢ LinearIndepOn (ι := L) K id {1}

Tactic:
have h1 : LinearIndepOn K id ({1} : Set L) := .singleton one_ne_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
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
⊢ Nonempty ι

Tactic:
haveI hem : Nonempty ι := B.index_nonempty
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
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 ι
⊢ 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

Tactic:
have h1L : (1 : L) ∈ LinearIndepOn.extend h1 _ :=
    Basis.subset_extend _ (Set.mem_singleton (1 : L))
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
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
⊢ 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)

Tactic:
have hB1 : B ⟨1, h1L⟩ = (1 : L) := by rw [Basis.coe_extend, Subtype.coe_mk]
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
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
⊢ g 0 = 0

Tactic:
have hg0 : g 0 = 0 := B.norm_zero