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 : 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‖
hF'_1 : Eq (α := ℝ) ((F' : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
hF'_0 : F' ≠ 0
k : K
y : L
hk :
  ∀ (y : L),
    (f : (a : L) → ℝ) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) =
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) : ℝ)
        ((f : (a : L) → ℝ) y : ℝ)
rw :
  Eq (α := ℝ) ((f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) : ℝ)
    ((smoothingSeminorm f hf_1 hf_na : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) : ℝ)
rw₁ :
  Eq (α := ℝ) ((smoothingSeminorm f hf_1 hf_na : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) : ℝ)
    ((f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) : ℝ)
rw₂ rw₃ :
  Eq (α := ℝ) ((f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) : ℝ)
    ((f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) : ℝ)
⊢ ‖k‖ = (smoothingSeminorm f hf_1 hf_na : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L)

Tactic:
rw [← hf_ext k, eq_comm, smoothingSeminorm_apply_of_map_mul_eq_mul f hf_1 hf_na hk]

Premises used: eq_comm, smoothingSeminorm_apply_of_map_mul_eq_mul
-- 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
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‖
hF'_1 : Eq (α := ℝ) ((F' : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
hF'_0 : F' ≠ 0
k : K
y : L
hk :
  ∀ (y : L),
    (f : (a : L) → ℝ) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) =
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) : ℝ)
        ((f : (a : L) → ℝ) y : ℝ)
⊢ ‖k‖ = (smoothingSeminorm f hf_1 hf_na : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L)

Tactic:
have hfk : ‖k‖ = (smoothingSeminorm f hf_1 hf_na) ((algebraMap K L) k) := by
          rw [← hf_ext k, eq_comm, smoothingSeminorm_apply_of_map_mul_eq_mul f hf_1 hf_na hk]
-- 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
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‖
hF'_1 : Eq (α := ℝ) ((F' : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
hF'_0 : F' ≠ 0
k : K
y : L
hk :
  ∀ (y : L),
    (f : (a : L) → ℝ) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) =
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) : ℝ)
        ((f : (a : L) → ℝ) y : ℝ)
hfk : ‖k‖ = (smoothingSeminorm f hf_1 hf_na : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L)
simp :
  ((smoothingSeminorm f hf_1 hf_na).toRingNorm ⋯).toFun (k • y) =
    HMul.hMul (α := ℝ) ((smoothingSeminorm f hf_1 hf_na : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) : ℝ)
      (((smoothingSeminorm f hf_1 hf_na).toRingNorm ⋯).toFun y)
⊢ (F'.toRingNorm hF'_0).toFun (k • y) = ‖k‖ * (F'.toRingNorm hF'_0).toFun y

Tactic:
simp only [hfk, hF']
-- 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
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‖
hF'_1 : Eq (α := ℝ) ((F' : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
hF'_0 : F' ≠ 0
k : K
y : L
hk :
  ∀ (y : L),
    (f : (a : L) → ℝ) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) =
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) : ℝ)
        ((f : (a : L) → ℝ) y : ℝ)
hfk : ‖k‖ = (smoothingSeminorm f hf_1 hf_na : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L)
erw :
  ((smoothingSeminorm f hf_1 hf_na).toRingNorm ⋯).toFun (k • y) =
    (smoothingSeminorm f hf_1 hf_na : (a : L) → ℝ) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y)
⊢ ((smoothingSeminorm f hf_1 hf_na).toRingNorm ⋯).toFun (k • y) =
    HMul.hMul (α := ℝ) ((smoothingSeminorm f hf_1 hf_na : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) : ℝ)
      (((smoothingSeminorm f hf_1 hf_na).toRingNorm ⋯).toFun y)

Tactic:
erw [← smoothingSeminorm_of_mul f hf_1 hf_na hk y]

Premises used: smoothingSeminorm_of_mul
-- 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
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‖
hF'_1 : Eq (α := ℝ) ((F' : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
hF'_0 : F' ≠ 0
k : K
y : L
hk :
  ∀ (y : L),
    (f : (a : L) → ℝ) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) =
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) : ℝ)
        ((f : (a : L) → ℝ) y : ℝ)
hfk : ‖k‖ = (smoothingSeminorm f hf_1 hf_na : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L)
rw :
  ((smoothingSeminorm f hf_1 hf_na).toRingNorm ⋯).toFun (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) =
    (smoothingSeminorm f hf_1 hf_na : (a : L) → ℝ) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y)
⊢ ((smoothingSeminorm f hf_1 hf_na).toRingNorm ⋯).toFun (k • y) =
    (smoothingSeminorm f hf_1 hf_na : (a : L) → ℝ) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y)

Tactic:
rw [Algebra.smul_def]

Premises used: Algebra.smul_def
-- 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
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‖
hF'_1 : Eq (α := ℝ) ((F' : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
hF'_0 : F' ≠ 0
k : K
y : L
hk :
  ∀ (y : L),
    (f : (a : L) → ℝ) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) =
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) : ℝ)
        ((f : (a : L) → ℝ) y : ℝ)
hfk : ‖k‖ = (smoothingSeminorm f hf_1 hf_na : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L)
⊢ ((smoothingSeminorm f hf_1 hf_na).toRingNorm ⋯).toFun (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) =
    (smoothingSeminorm f hf_1 hf_na : (a : L) → ℝ) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y)

Tactic:
rfl
-- 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
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‖
hF'_1 : Eq (α := ℝ) ((F' : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
hF'_0 : F' ≠ 0
F : AlgebraNorm K L :=
  let __src := F'.toRingNorm hF'_0;
  { toRingNorm := __src, smul' := ⋯ }
k : K
rw :
  Eq (α := ℝ) ((F : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) : ℝ)
    ((f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) : ℝ)
⊢ (F : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) = ‖k‖

Tactic:
rw [← hf_ext]
-- 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
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‖
hF'_1 : Eq (α := ℝ) ((F' : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
hF'_0 : F' ≠ 0
F : AlgebraNorm K L :=
  let __src := F'.toRingNorm hF'_0;
  { toRingNorm := __src, smul' := ⋯ }
k : K
⊢ Eq (α := ℝ) ((F : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) : ℝ)
    ((f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) : ℝ)

Tactic:
smoothingSeminorm_apply_of_map_mul_eq_mul f hf_1 hf_na
      (seminormFromBounded_of_mul_is_mul hg_nonneg hg_bdd (hg_mul k))

Premises used: seminormFromBounded_of_mul_is_mul, smoothingSeminorm_apply_of_map_mul_eq_mul
-- 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
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‖
hF'_1 : Eq (α := ℝ) ((F' : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
hF'_0 : F' ≠ 0
F : AlgebraNorm K L :=
  let __src := F'.toRingNorm hF'_0;
  { toRingNorm := __src, smul' := ⋯ }
k : K
⊢ Eq (α := ℝ) ((F : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) : ℝ)
    ((f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) : ℝ)

Tactic:
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))

Premises used: seminormFromBounded_of_mul_is_mul, smoothingSeminorm_apply_of_map_mul_eq_mul