awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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)
x : K
simp : (sup' univ ⋯ fun (x_1 : ι) ↦ ‖if i = x_1 then x else 0‖) = ‖x‖
⊢ B.norm ((algebraMap K L : (a : K) → L) x) = ‖x‖
have a : (sup' univ sorry fun (x_1 : ι) ↦ ‖if i = x_1 then x else 0‖) ≤ ‖x‖
Tactic: classical
  simp only [norm, repr_algebraMap hBi, Finsupp.single_apply]
  apply le_antisymm
  · aesop
  · exact le_sup'_of_le _ (mem_univ i) (by simp)
-- 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_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)
x : K
simp : (sup' univ ⋯ fun (x_1 : ι) ↦ ‖if i = x_1 then x else 0‖) = ‖x‖
a : (sup' univ ⋯ fun (x_1 : ι) ↦ ‖if i = x_1 then x else 0‖) ≤ ‖x‖
⊢ B.norm ((algebraMap K L : (a : K) → L) x) = ‖x‖
have a₁ : ‖x‖ ≤ sup' univ sorry fun (x_1 : ι) ↦ ‖if i = x_1 then x else 0‖
Tactic: classical
  simp only [norm, repr_algebraMap hBi, Finsupp.single_apply]
  apply le_antisymm
  · aesop
  · exact le_sup'_of_le _ (mem_univ i) (by simp)
-- 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_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
x y : L
⊢ B.norm (x + y) ≤ max (B.norm x) (B.norm y)
have obtain : ∀ (ixy : ι),
  Membership.mem (γ := Finset ι) univ ixy →
    ∀
      (hixy :
        (sup' univ sorry 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) ≤ max (B.norm x) (B.norm y)
Tactic: obtain ⟨ixy, _, hixy⟩ := exists_mem_eq_sup' univ_nonempty (fun i ↦ ‖(B.repr (x + y)) i‖)
-- 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_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
x y : L
ixy : ι
left : Membership.mem (γ := Finset ι) univ ixy
hixy :
  (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)
⊢ Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
    max (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) ixy : K))
      (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) ixy : K))
have rw : ‖HAdd.hAdd (α := K) (β := K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) ixy : K)
      ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) ixy : K)‖ ≤
  max (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) ixy : K))
    (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) ixy : K))
Tactic: rw [map_add, Finsupp.coe_add, Pi.add_apply]
-- 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_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
x y : L
ixy : ι
left : Membership.mem (γ := Finset ι) univ ixy
hixy :
  (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) ≤ max (B.norm x) (B.norm y)
have hxy : Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
  max (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) ixy : K))
    (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) ixy : K))
Tactic: have hxy : ‖B.repr (x + y) ixy‖ ≤ max ‖B.repr x ixy‖ ‖B.repr y ixy‖ := by
    rw [map_add, Finsupp.coe_add, Pi.add_apply]; exact hna _ _
-- 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_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
x y : L
ixy : ι
left : Membership.mem (γ := Finset ι) univ ixy
hixy :
  (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)
hxy :
  Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
    max (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) ixy : K))
      (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) ixy : K))
⊢ B.norm (x + y) ≤ max (B.norm x) (B.norm y)
have rw : Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
  max (B.norm x) (B.norm y)
Tactic: rw [Basis.norm, hixy]
-- 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_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
x y : L
ixy : ι
left : Membership.mem (γ := Finset ι) univ ixy
hixy :
  (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)
hxy :
  Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
    max (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) ixy : K))
      (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) ixy : K))
⊢ Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
    max (B.norm x) (B.norm y)
have inl : ∀
  (hx :
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
      Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) ixy : K)),
  Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
    max (B.norm x) (B.norm y)
Tactic: rcases le_max_iff.mp hxy with (hx | hy)
-- 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_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
x y : L
ixy : ι
left : Membership.mem (γ := Finset ι) univ ixy
hixy :
  (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)
hxy :
  Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
    max (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) ixy : K))
      (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) ixy : K))
inl :
  ∀
    (hx :
      Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
        Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) ixy : K)),
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
      max (B.norm x) (B.norm y)
⊢ Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
    max (B.norm x) (B.norm y)
have inr : ∀
  (hy :
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
      Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) ixy : K)),
  Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
    max (B.norm x) (B.norm y)
Tactic: rcases le_max_iff.mp hxy with (hx | hy)
-- 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_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 : ℝ) (_ : 0 < c), ∀ (x y : L), B.norm (x * y) ≤ c * B.norm x * B.norm y
have obtain : ∀ (c : ι × ι),
  Membership.mem (γ := Finset (ι × ι)) univ c →
    ∀
      (hc :
        (sup' univ sorry 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))),
      ∃ (c : ℝ) (_ : 0 < c), ∀ (x y : L), B.norm (x * y) ≤ c * B.norm x * B.norm y
Tactic: obtain ⟨c, _, hc⟩ := exists_mem_eq_sup' univ_nonempty (fun i : ι × ι ↦ B.norm (B i.1 * B i.2))
-- 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_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))
⊢ ∃ (c : ℝ) (_ : 0 < c), ∀ (x y : L), B.norm (x * y) ≤ c * B.norm x * B.norm y
have 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
Tactic: use B.norm (B c.1 * B c.2)
-- 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_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) 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
have 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
Tactic: constructor
-- 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_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
⊢ ∃ (_ : 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
have h₁ : 0 < B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L))
Tactic: constructor
-- 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_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
⊢ 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
have h : ∀ (ixy : ι),
  Membership.mem (γ := Finset ι) univ ixy →
    ∀
      (hixy_def :
        (sup' univ sorry 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
Tactic: obtain ⟨ixy, _, hixy_def⟩ := exists_mem_eq_sup' univ_nonempty (fun i ↦ ‖(B.repr (x * y)) i‖)
-- 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_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)
| sup' univ ⋯ fun (i : ι) ↦
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x * y) : ι →₀ K) : (a : ι) → K) i : K)
have 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)
Tactic: rw [hixy_def, ← Basis.sum_repr B x, ← Basis.sum_repr B y]
-- 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_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)
| B.norm (x * y)
have 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)
Tactic: simp only [Basis.norm]; rw [hixy_def, ← Basis.sum_repr B x, ← Basis.sum_repr B y]
-- 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_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)
⊢ 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
have 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
Tactic: conv_lhs => simp only [Basis.norm]; rw [hixy_def, ← Basis.sum_repr B x, ← Basis.sum_repr B y]
-- 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_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)
⊢ 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
have 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
Tactic: rw [sum_mul, map_finsetSum]