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_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i : L) (1 : L)
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
c : ι × ι
left : Membership.mem (γ := Finset (ι × ι)) univ c
hc :
  (sup' univ ⋯ fun (i : ι × ι) ↦
      B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) i.1 : L) ((B : (a : ι) → L) i.2 : L))) =
    B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L))
h :
  ∃ (_ : 0 < B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L))),
    ∀ (x y : L),
      B.norm (x * y) ≤
        B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L)) * B.norm x *
          B.norm y
⊢ ∃ (c : ℝ) (_ : 0 < c), ∀ (x y : L), B.norm (x * y) ≤ c * B.norm x * B.norm y

Tactic:
use B.norm (B c.1 * B c.2)

Premises used: HMul.hMul, Module.Basis.norm, Prod.fst, Prod.snd, 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_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i : L) (1 : L)
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
c : ι × ι
left : Membership.mem (γ := Finset (ι × ι)) univ c
hc :
  (sup' univ ⋯ fun (i : ι × ι) ↦
      B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) i.1 : L) ((B : (a : ι) → L) i.2 : L))) =
    B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L))
h :
  ∀ (x y : L),
    B.norm (x * y) ≤
      B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L)) * B.norm x * B.norm y
h₁ : 0 < B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L))
⊢ ∃ (_ : 0 < B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L))),
    ∀ (x y : L),
      B.norm (x * y) ≤
        B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L)) * B.norm x *
          B.norm y

Tactic:
constructor
-- 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_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i : L) (1 : L)
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
c : ι × ι
left : Membership.mem (γ := Finset (ι × ι)) univ c
hc :
  (sup' univ ⋯ fun (i : ι × ι) ↦
      B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) i.1 : L) ((B : (a : ι) → L) i.2 : L))) =
    B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L))
x y : L
h :
  ∀ (ixy : ι),
    Membership.mem (γ := Finset ι) univ ixy →
      ∀
        (hixy_def :
          (sup' univ ⋯ fun (i : ι) ↦
              Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x * y) : ι →₀ K) : (a : ι) → K) i : K)) =
            Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x * y) : ι →₀ K) : (a : ι) → K) ixy : K)),
        B.norm (x * y) ≤
          B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L)) * B.norm x *
            B.norm y
⊢ B.norm (x * y) ≤
    B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L)) * B.norm x * B.norm y

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

Premises used: Norm.norm, HMul.hMul, 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_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i : L) (1 : L)
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
c : ι × ι
left : Membership.mem (γ := Finset (ι × ι)) univ c
hc :
  (sup' univ ⋯ fun (i : ι × ι) ↦
      B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) i.1 : L) ((B : (a : ι) → L) i.2 : L))) =
    B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L))
x y : L
ixy : ι
left_1 : Membership.mem (γ := Finset ι) univ ixy
hixy_def :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x * y) : ι →₀ K) : (a : ι) → K) i : K)) =
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x * y) : ι →₀ K) : (a : ι) → K) ixy : K)
rw :
  Norm.norm.{u_1} (E := K)
    ((((B.repr : (a : L) → ι →₀ K)
              (HMul.hMul (α := L)
                (∑ i : ι,
                  HSMul.hSMul.{u_1, u_2, u_2} (α := K) (β := L)
                    ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K) ((B : (a : ι) → L) i : L))
                (∑ i : ι,
                  HSMul.hSMul.{u_1, u_2, u_2} (α := K) (β := L)
                    ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K) ((B : (a : ι) → L) i : L))) :
            ι →₀ K) :
          (a : ι) → K)
        ixy :
      K)
| sup' univ ⋯ fun (i : ι) ↦
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x * y) : ι →₀ K) : (a : ι) → K) i : K)

Tactic:
rw [hixy_def, ← Basis.sum_repr B x, ← Basis.sum_repr B y]

Premises used: Module.Basis.sum_repr
-- 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_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i : L) (1 : L)
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
c : ι × ι
left : Membership.mem (γ := Finset (ι × ι)) univ c
hc :
  (sup' univ ⋯ fun (i : ι × ι) ↦
      B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) i.1 : L) ((B : (a : ι) → L) i.2 : L))) =
    B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L))
x y : L
ixy : ι
left_1 : Membership.mem (γ := Finset ι) univ ixy
hixy_def :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x * y) : ι →₀ K) : (a : ι) → K) i : K)) =
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x * y) : ι →₀ K) : (a : ι) → K) ixy : K)
simp :
  Norm.norm.{u_1} (E := K)
    ((((B.repr : (a : L) → ι →₀ K)
              (HMul.hMul (α := L)
                (∑ i : ι,
                  HSMul.hSMul.{u_1, u_2, u_2} (α := K) (β := L)
                    ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K) ((B : (a : ι) → L) i : L))
                (∑ i : ι,
                  HSMul.hSMul.{u_1, u_2, u_2} (α := K) (β := L)
                    ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K) ((B : (a : ι) → L) i : L))) :
            ι →₀ K) :
          (a : ι) → K)
        ixy :
      K)
| B.norm (x * y)

Tactic:
simp only [Basis.norm]; rw [hixy_def, ← Basis.sum_repr B x, ← Basis.sum_repr B y]

Premises used: Module.Basis.norm, Module.Basis.sum_repr
-- 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_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i : L) (1 : L)
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
c : ι × ι
left : Membership.mem (γ := Finset (ι × ι)) univ c
hc :
  (sup' univ ⋯ fun (i : ι × ι) ↦
      B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) i.1 : L) ((B : (a : ι) → L) i.2 : L))) =
    B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L))
x y : L
ixy : ι
left_1 : Membership.mem (γ := Finset ι) univ ixy
hixy_def :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x * y) : ι →₀ K) : (a : ι) → K) i : K)) =
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x * y) : ι →₀ K) : (a : ι) → K) ixy : K)
h :
  Norm.norm.{u_1} (E := K)
      ((((B.repr : (a : L) → ι →₀ K)
                (HMul.hMul (α := L)
                  (∑ i : ι,
                    HSMul.hSMul.{u_1, u_2, u_2} (α := K) (β := L)
                      ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K) ((B : (a : ι) → L) i : L))
                  (∑ i : ι,
                    HSMul.hSMul.{u_1, u_2, u_2} (α := K) (β := L)
                      ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K) ((B : (a : ι) → L) i : L))) :
              ι →₀ K) :
            (a : ι) → K)
          ixy :
        K) ≤
    B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L)) * B.norm x * B.norm y
⊢ B.norm (x * y) ≤
    B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L)) * B.norm x * B.norm y

Tactic:
conv_lhs => simp only [Basis.norm]; rw [hixy_def, ← Basis.sum_repr B x, ← Basis.sum_repr B y]

Premises used: Module.Basis.norm, Module.Basis.sum_repr
-- 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_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i : L) (1 : L)
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
c : ι × ι
left : Membership.mem (γ := Finset (ι × ι)) univ c
hc :
  (sup' univ ⋯ fun (i : ι × ι) ↦
      B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) i.1 : L) ((B : (a : ι) → L) i.2 : L))) =
    B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L))
x y : L
ixy : ι
left_1 : Membership.mem (γ := Finset ι) univ ixy
hixy_def :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x * y) : ι →₀ K) : (a : ι) → K) i : K)) =
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x * y) : ι →₀ K) : (a : ι) → K) ixy : K)
h :
  Norm.norm.{u_1} (E := K)
      ((∑ i : ι,
              (B.repr : (a : L) → ι →₀ K)
                (HSMul.hSMul.{u_1, u_2, u_2} (α := K) (β := L)
                    ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K) ((B : (a : ι) → L) i : L) *
                  ∑ i : ι,
                    HSMul.hSMul.{u_1, u_2, u_2} (α := K) (β := L)
                      ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K) ((B : (a : ι) → L) i : L)) :
            (a : ι) → K)
          ixy :
        K) ≤
    B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L)) * B.norm x * B.norm y
⊢ Norm.norm.{u_1} (E := K)
      ((((B.repr : (a : L) → ι →₀ K)
                (HMul.hMul (α := L)
                  (∑ i : ι,
                    HSMul.hSMul.{u_1, u_2, u_2} (α := K) (β := L)
                      ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K) ((B : (a : ι) → L) i : L))
                  (∑ i : ι,
                    HSMul.hSMul.{u_1, u_2, u_2} (α := K) (β := L)
                      ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K) ((B : (a : ι) → L) i : L))) :
              ι →₀ K) :
            (a : ι) → K)
          ixy :
        K) ≤
    B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L)) * B.norm x * B.norm y

Tactic:
rw [sum_mul, map_finsetSum]

Premises used: map_finsetSum, Finset.sum_mul
-- 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_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i : L) (1 : L)
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
c : ι × ι
left : Membership.mem (γ := Finset (ι × ι)) univ c
hc :
  (sup' univ ⋯ fun (i : ι × ι) ↦
      B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) i.1 : L) ((B : (a : ι) → L) i.2 : L))) =
    B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L))
x y : L
ixy : ι
left_1 : Membership.mem (γ := Finset ι) univ ixy
hixy_def :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x * y) : ι →₀ K) : (a : ι) → K) i : K)) =
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x * y) : ι →₀ K) : (a : ι) → K) ixy : K)
h :
  Norm.norm.{u_1} (E := K)
      ((∑ x_1 : ι,
              HSMul.hSMul (α := K) (β := ι →₀ K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) x_1 : K)
                (∑ x : ι,
                  HSMul.hSMul (α := K) (β := ι →₀ K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) x : K)
                    ((B.repr : (a : L) → ι →₀ K)
                        (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) x_1 : L) ((B : (a : ι) → L) x : L)) :
                      ι →₀ K)) :
            (a : ι) → K)
          ixy :
        K) ≤
    B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L)) * B.norm x * B.norm y
⊢ Norm.norm.{u_1} (E := K)
      ((∑ i : ι,
              (B.repr : (a : L) → ι →₀ K)
                (HSMul.hSMul.{u_1, u_2, u_2} (α := K) (β := L)
                    ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K) ((B : (a : ι) → L) i : L) *
                  ∑ i : ι,
                    HSMul.hSMul.{u_1, u_2, u_2} (α := K) (β := L)
                      ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) i : K) ((B : (a : ι) → L) i : L)) :
            (a : ι) → K)
          ixy :
        K) ≤
    B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L)) * B.norm x * B.norm y

Tactic:
simp_rw [smul_mul_assoc, map_smul, mul_sum, map_finsetSum, mul_smul_comm, map_smul]

Premises used: Finset.mul_sum, map_finsetSum, smul_mul_assoc, mul_smul_comm, map_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_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i : L) (1 : L)
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
c : ι × ι
left : Membership.mem (γ := Finset (ι × ι)) univ c
hc :
  (sup' univ ⋯ fun (i : ι × ι) ↦
      B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) i.1 : L) ((B : (a : ι) → L) i.2 : L))) =
    B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L))
x y : L
ixy : ι
left_1 : Membership.mem (γ := Finset ι) univ ixy
hixy_def :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x * y) : ι →₀ K) : (a : ι) → K) i : K)) =
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x * y) : ι →₀ K) : (a : ι) → K) ixy : K)
⊢ IsNonarchimedean (R := ℝ) (α := K) (⇑(NormedField.toMulRingNorm K) : (a : K) → ℝ)

Tactic:
have hna' : IsNonarchimedean (NormedField.toMulRingNorm K) := hna
-- 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_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i : L) (1 : L)
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
c : ι × ι
left : Membership.mem (γ := Finset (ι × ι)) univ c
hc :
  (sup' univ ⋯ fun (i : ι × ι) ↦
      B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) i.1 : L) ((B : (a : ι) → L) i.2 : L))) =
    B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L))
rw rw₁ : Eq.{u_2 + 1} (α := L) 1 1
⊢ Eq.{u_2 + 1} (α := L) (1 : L) ((algebraMap K L : (a : K) → L) 1 : L)

Tactic:
rw [map_one]

Premises used: map_one
-- 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_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i : L) (1 : L)
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
c : ι × ι
left : Membership.mem (γ := Finset (ι × ι)) univ c
hc :
  (sup' univ ⋯ fun (i : ι × ι) ↦
      B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) i.1 : L) ((B : (a : ι) → L) i.2 : L))) =
    B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L))
⊢ Eq.{u_2 + 1} (α := L) (1 : L) ((algebraMap K L : (a : K) → L) 1 : L)

Tactic:
have h1 : (1 : L) = (algebraMap K L) 1 := by rw [map_one]
-- 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_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i : L) (1 : L)
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
c : ι × ι
left : Membership.mem (γ := Finset (ι × ι)) univ c
hc :
  (sup' univ ⋯ fun (i : ι × ι) ↦
      B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) i.1 : L) ((B : (a : ι) → L) i.2 : L))) =
    B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L))
h1 : Eq.{u_2 + 1} (α := L) (1 : L) ((algebraMap K L : (a : K) → L) 1 : L)
rw : 0 < Norm.norm.{u_1} (E := K) 1
⊢ 0 < B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) i : L) ((B : (a : ι) → L) i : L))

Tactic:
rw [hBi, mul_one, h1, Basis.norm_extends hBi]

Premises used: mul_one, Module.Basis.norm_extends
-- 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_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i : L) (1 : L)
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
c : ι × ι
left : Membership.mem (γ := Finset (ι × ι)) univ c
hc :
  (sup' univ ⋯ fun (i : ι × ι) ↦
      B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) i.1 : L) ((B : (a : ι) → L) i.2 : L))) =
    B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L))
h1 : Eq.{u_2 + 1} (α := L) (1 : L) ((algebraMap K L : (a : K) → L) 1 : L)
⊢ 0 < Norm.norm.{u_1} (E := K) 1

Tactic:
simp [norm_one, zero_lt_one]

Premises used: NormOneClass.norm_one, zero_lt_one
-- 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_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i : L) (1 : L)
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
c : ι × ι
left : Membership.mem (γ := Finset (ι × ι)) univ c
hc :
  (sup' univ ⋯ fun (i : ι × ι) ↦
      B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) i.1 : L) ((B : (a : ι) → L) i.2 : L))) =
    B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L))
⊢ 0 < B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) i : L) ((B : (a : ι) → L) i : L))

Tactic:
have h_pos : (0 : ℝ) < B.norm (B i * B i) := by
      have h1 : (1 : L) = (algebraMap K L) 1 := by rw [map_one]
      rw [hBi, mul_one, h1, Basis.norm_extends hBi]
      simp [norm_one, zero_lt_one]
-- 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_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i : L) (1 : L)
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
c : ι × ι
left : Membership.mem (γ := Finset (ι × ι)) univ c
hc :
  (sup' univ ⋯ fun (i : ι × ι) ↦
      B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) i.1 : L) ((B : (a : ι) → L) i.2 : L))) =
    B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L))
h_pos : 0 < B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) i : L) ((B : (a : ι) → L) i : L))
⊢ 0 < B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L))

Tactic:
lt_of_lt_of_le h_pos
      (hc ▸ Finset.le_sup' (fun i : ι × ι ↦ B.norm (B i.1 * B i.2)) (mem_univ (i, i)))

Premises used: Finset.mem_univ, HMul.hMul, Module.Basis.norm, Eq.rec, Prod.mk, Prod.fst, Finset.le_sup', Prod.snd, DFunLike.coe, lt_of_lt_of_le
-- 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_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i : L) (1 : L)
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
c : ι × ι
left : Membership.mem (γ := Finset (ι × ι)) univ c
hc :
  (sup' univ ⋯ fun (i : ι × ι) ↦
      B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) i.1 : L) ((B : (a : ι) → L) i.2 : L))) =
    B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L))
h_pos : 0 < B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) i : L) ((B : (a : ι) → L) i : L))
⊢ 0 < B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L))

Tactic:
exact lt_of_lt_of_le h_pos
      (hc ▸ Finset.le_sup' (fun i : ι × ι ↦ B.norm (B i.1 * B i.2)) (mem_univ (i, i)))

Premises used: lt_of_lt_of_le
-- 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
pos :
  ∀ (hk : k = 0),
    B.norm (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) =
      B.norm ((algebraMap K L : (a : K) → L) k) * B.norm y
neg :
  ∀ (hk : ¬k = 0),
    B.norm (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) =
      B.norm ((algebraMap K L : (a : K) → L) k) * B.norm y
⊢ B.norm (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) =
    B.norm ((algebraMap K L : (a : K) → L) k) * B.norm y

Tactic:
by_cases hk : k = 0
-- 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
pos :
  B.norm (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) 0 : L) y) =
    B.norm ((algebraMap K L : (a : K) → L) 0) * B.norm y
pos₁ : B.norm (0 * y) = B.norm 0 * B.norm y
pos₂ : B.norm 0 = B.norm 0 * B.norm y
pos₃ : 0 = 0 * B.norm y
pos₄ pos₅ : Eq (α := ℝ) 0 0
⊢ B.norm (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) =
    B.norm ((algebraMap K L : (a : K) → L) k) * B.norm y

Tactic:
rw [hk, map_zero, zero_mul, B.norm_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, map_zero, Module.Basis.norm_zero
-- 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 : 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) =
    B.norm ((algebraMap K L : (a : K) → L) k) * B.norm y

Tactic:
rw [norm_extends hBi]

Premises used: Module.Basis.norm_extends