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‖
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 (α := ℝ) ((F' : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
have h1₁ : 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]
-- 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
hF'_ext : ∀ (k : K), (F' : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) = ‖k‖
⊢ ∃ (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 : Eq (α := ℝ) ((F' : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
Tactic: have hF'_1 : F' 1 = 1 := by
    have h1 : (1 : L) = (algebraMap K L) 1 := by rw [map_one]
    simp only [h1, hF'_ext (1 : K), norm_one]
-- 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‖
hF'_1 : Eq (α := ℝ) ((F' : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
⊢ Ne (α := ℝ) ((F' : (a : L) → ℝ) 1 : ℝ) ((0 : (a : L) → ℝ) 1 : ℝ)
have rw : Ne (α := ℝ) (1 : ℝ) ((0 : (a : L) → ℝ) 1 : ℝ)
Tactic: rw [hF'_1]
-- 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
hF'_ext : ∀ (k : K), (F' : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) = ‖k‖
hF'_1 : Eq (α := ℝ) ((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'_0 : F' ≠ 0
Tactic: have hF'_0 : F' ≠ 0 := DFunLike.ne_iff.mpr ⟨(1 : L), by rw [hF'_1]; exact one_ne_zero⟩
-- 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
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
⊢ (F'.toRingNorm hF'_0).toFun (k • y) = ‖k‖ * (F'.toRingNorm hF'_0).toFun y
have 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 : ℝ)
Tactic: have hk : ∀ y : L, f (algebraMap K L k * y) = f (algebraMap K L k) * f y :=
          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‖
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)
have 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) : ℝ)
Tactic: rw [← hf_ext k, eq_comm, smoothingSeminorm_apply_of_map_mul_eq_mul f hf_1 hf_na hk]
-- 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‖
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) : ℝ)
⊢ ‖k‖ = (smoothingSeminorm f hf_1 hf_na : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L)
have 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) : ℝ)
Tactic: rw [← hf_ext k, eq_comm, smoothingSeminorm_apply_of_map_mul_eq_mul f hf_1 hf_na hk]
-- 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‖
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) : ℝ)
⊢ ‖k‖ = (smoothingSeminorm f hf_1 hf_na : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L)
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 k, eq_comm, smoothingSeminorm_apply_of_map_mul_eq_mul f hf_1 hf_na hk]
-- 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
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 : ℝ)
⊢ (F'.toRingNorm hF'_0).toFun (k • y) = ‖k‖ * (F'.toRingNorm hF'_0).toFun y
have hfk : ‖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]