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 : 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
hg_ext : ∀ (x : K), g ((algebraMap K L : (a : K) → L) x) = ‖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_na : IsNonarchimedean g
Tactic: have hg_na : IsNonarchimedean g := Basis.norm_isNonarchimedean hna
-- 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
hg_ext : ∀ (x : K), g ((algebraMap K L : (a : K) → L) x) = ‖x‖
hg_na : IsNonarchimedean g
⊢ ∃ (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_add : ∀ (a b : L), g (a + b) ≤ g a + g b
Tactic: have hg_add : ∀ a b : L, g (a + b) ≤ g a + g b :=
    fun _ _ ↦ IsNonarchimedean.add_le hg_nonneg hg_na
-- 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
hg_ext : ∀ (x : K), g ((algebraMap K L : (a : K) → L) x) = ‖x‖
hg_na : IsNonarchimedean g
hg_add : ∀ (a b : L), g (a + b) ≤ g a + g 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 hg_neg : ∀ (a : L), g (-a) = g a
Tactic: have hg_neg : ∀ a : L, g (-a) = g a := B.norm_neg
-- 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
hg_nonneg : ∀ (x : L), 0 ≤ g x
hg_ext : ∀ (x : K), g ((algebraMap K L : (a : K) → L) x) = ‖x‖
hg_na : IsNonarchimedean g
hg_add : ∀ (a b : L), g (a + b) ≤ g a + g b
hg_neg : ∀ (a : L), g (-a) = g a
⊢ ∃ (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 obtain : ∀ (w : ℝ),
  0 < w →
    ∀ (hg_bdd : ∀ (x y : L), B.norm (x * y) ≤ w * B.norm x * B.norm y),
      ∃ (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) → ℝ)
Tactic: obtain ⟨_, _, hg_bdd⟩ := Basis.norm_mul_le_const_mul_norm hB1 hna
-- 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
hg_ext : ∀ (x : K), g ((algebraMap K L : (a : K) → L) x) = ‖x‖
hg_na : IsNonarchimedean g
hg_add : ∀ (a b : L), g (a + b) ≤ g a + g b
hg_neg : ∀ (a : L), g (-a) = g a
w : ℝ
w_1 : 0 < w
hg_bdd : ∀ (x y : L), B.norm (x * y) ≤ w * B.norm x * B.norm y
⊢ ∃ (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_mul : ∀ (k : K) (y : L),
  g (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) = g ((algebraMap K L : (a : K) → L) k) * g y
Tactic: have hg_mul : ∀ (k : K) (y : L), g ((algebraMap K L) k * y) = g ((algebraMap K L) k) * g y :=
    fun k y ↦ Basis.norm_smul hB1 k y
-- 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
hg_ext : ∀ (x : K), g ((algebraMap K L : (a : K) → L) x) = ‖x‖
hg_na : IsNonarchimedean g
hg_add : ∀ (a b : L), g (a + b) ≤ g a + g b
hg_neg : ∀ (a : L), g (-a) = g a
w : ℝ
w_1 : 0 < w
hg_bdd : ∀ (x y : L), B.norm (x * y) ≤ w * B.norm x * B.norm y
hg_mul :
  ∀ (k : K) (y : L),
    g (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) = g ((algebraMap K L : (a : K) → L) k) * g y
f : RingSeminorm L := seminormFromBounded hg0 hg_nonneg hg_bdd hg_add hg_neg
⊢ ∃ (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 hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
Tactic: have hf_na : IsNonarchimedean f := seminormFromBounded_isNonarchimedean hg_nonneg hg_bdd hg_na
-- 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
hg_ext : ∀ (x : K), g ((algebraMap K L : (a : K) → L) x) = ‖x‖
hg_na : IsNonarchimedean g
hg_add : ∀ (a b : L), g (a + b) ≤ g a + g b
hg_neg : ∀ (a : L), g (-a) = g a
w : ℝ
w_1 : 0 < w
hg_bdd : ∀ (x y : L), B.norm (x * y) ≤ w * B.norm x * B.norm y
hg_mul :
  ∀ (k : K) (y : L),
    g (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) = g ((algebraMap K L : (a : K) → L) k) * g y
f : RingSeminorm L := seminormFromBounded hg0 hg_nonneg hg_bdd hg_add hg_neg
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
⊢ ∃ (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 hf_1 : LE.le (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
Tactic: have hf_1 : f 1 ≤ 1 := seminormFromBounded_one_le hg_nonneg hg_bdd
-- 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
hg_ext : ∀ (x : K), g ((algebraMap K L : (a : K) → L) x) = ‖x‖
hg_na : IsNonarchimedean g
hg_add : ∀ (a b : L), g (a + b) ≤ g a + g b
hg_neg : ∀ (a : L), g (-a) = g a
w : ℝ
w_1 : 0 < w
hg_bdd : ∀ (x y : L), B.norm (x * y) ≤ w * B.norm x * B.norm y
hg_mul :
  ∀ (k : K) (y : L),
    g (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) = g ((algebraMap K L : (a : K) → L) k) * g y
f : RingSeminorm L := seminormFromBounded hg0 hg_nonneg hg_bdd hg_add hg_neg
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf_1 : LE.le (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (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 hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
Tactic: have hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ‖x‖ :=
    fun k ↦ hg_ext k ▸ seminormFromBounded_of_mul_apply hg_nonneg hg_bdd (hg_mul k)
-- 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
hg_ext : ∀ (x : K), g ((algebraMap K L : (a : K) → L) x) = ‖x‖
hg_na : IsNonarchimedean g
hg_add : ∀ (a b : L), g (a + b) ≤ g a + g b
hg_neg : ∀ (a : L), g (-a) = g a
w : ℝ
w_1 : 0 < w
hg_bdd : ∀ (x y : L), B.norm (x * y) ≤ w * B.norm x * B.norm y
hg_mul :
  ∀ (k : K) (y : L),
    g (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) = g ((algebraMap K L : (a : K) → L) k) * g y
f : RingSeminorm L := seminormFromBounded hg0 hg_nonneg hg_bdd hg_add hg_neg
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf_1 : LE.le (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖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 hF' : let F' := smoothingSeminorm f hf_1 hf_na;
F' = smoothingSeminorm f hf_1 hf_na
Tactic: set F' := smoothingSeminorm f hf_1 hf_na with hF'
-- 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
hg_nonneg : ∀ (x : L), 0 ≤ g x
hg_ext : ∀ (x : K), g ((algebraMap K L : (a : K) → L) x) = ‖x‖
hg_na : IsNonarchimedean g
hg_add : ∀ (a b : L), g (a + b) ≤ g a + g b
hg_neg : ∀ (a : L), g (-a) = g a
w : ℝ
w_1 : 0 < w
hg_bdd : ∀ (x y : L), B.norm (x * y) ≤ w * B.norm x * B.norm y
hg_mul :
  ∀ (k : K) (y : L),
    g (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) = g ((algebraMap K L : (a : K) → L) k) * g y
f : RingSeminorm L := seminormFromBounded hg0 hg_nonneg hg_bdd hg_add hg_neg
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf_1 : LE.le (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
F' : RingSeminorm L := smoothingSeminorm f hf_1 hf_na
hF' : F' = smoothingSeminorm f hf_1 hf_na
k : K
⊢ (F' : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) = ‖k‖
have rw : Eq (α := ℝ) ((F' : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) : ℝ)
  ((f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) : ℝ)
Tactic: rw [← hf_ext _]
-- 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
hg_ext : ∀ (x : K), g ((algebraMap K L : (a : K) → L) x) = ‖x‖
hg_na : IsNonarchimedean g
hg_add : ∀ (a b : L), g (a + b) ≤ g a + g b
hg_neg : ∀ (a : L), g (-a) = g a
w : ℝ
w_1 : 0 < w
hg_bdd : ∀ (x y : L), B.norm (x * y) ≤ w * B.norm x * B.norm y
hg_mul :
  ∀ (k : K) (y : L),
    g (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) = g ((algebraMap K L : (a : K) → L) k) * g y
f : RingSeminorm L := seminormFromBounded hg0 hg_nonneg hg_bdd hg_add hg_neg
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf_1 : LE.le (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
F' : RingSeminorm L := smoothingSeminorm f hf_1 hf_na
hF' : F' = smoothingSeminorm f hf_1 hf_na
⊢ ∃ (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 hF'_ext : ∀ (k : K), (F' : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) = ‖k‖
Tactic: have hF'_ext : ∀ k : K, F' ((algebraMap K L) k) = ‖k‖ := by
    intro k
    rw [← hf_ext _]
    exact smoothingSeminorm_apply_of_map_mul_eq_mul f hf_1 hf_na
      (seminormFromBounded_of_mul_is_mul hg_nonneg hg_bdd (hg_mul k))
-- 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
hg_nonneg : ∀ (x : L), 0 ≤ g x
hg_ext : ∀ (x : K), g ((algebraMap K L : (a : K) → L) x) = ‖x‖
hg_na : IsNonarchimedean g
hg_add : ∀ (a b : L), g (a + b) ≤ g a + g b
hg_neg : ∀ (a : L), g (-a) = g a
w : ℝ
w_1 : 0 < w
hg_bdd : ∀ (x y : L), B.norm (x * y) ≤ w * B.norm x * B.norm y
hg_mul :
  ∀ (k : K) (y : L),
    g (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) = g ((algebraMap K L : (a : K) → L) k) * g y
f : RingSeminorm L := seminormFromBounded hg0 hg_nonneg hg_bdd hg_add hg_neg
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf_1 : LE.le (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
F' : RingSeminorm L := smoothingSeminorm f hf_1 hf_na
hF' : F' = smoothingSeminorm f hf_1 hf_na
hF'_ext : ∀ (k : K), (F' : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) = ‖k‖
⊢ Eq.{u_2 + 1} (α := L) (1 : L) ((algebraMap K L : (a : K) → L) 1 : L)
have rw : Eq.{u_2 + 1} (α := L) 1 1
Tactic: rw [map_one]