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 : 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)
⊢ (F'.toRingNorm hF'_0).toFun (k • y) = ‖k‖ * (F'.toRingNorm hF'_0).toFun y
have simp : ((smoothingSeminorm f hf_1 hf_na).toRingNorm sorry).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 sorry).toFun y)
Tactic: simp only [hfk, 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
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 (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)
have erw : ((smoothingSeminorm f hf_1 hf_na).toRingNorm sorry).toFun (k • y) =
  (smoothingSeminorm f hf_1 hf_na : (a : L) → ℝ) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y)
Tactic: erw [← smoothingSeminorm_of_mul f hf_1 hf_na hk 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 : 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 (k • y) =
    (smoothingSeminorm f hf_1 hf_na : (a : L) → ℝ) (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y)
have rw : ((smoothingSeminorm f hf_1 hf_na).toRingNorm sorry).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: rw [Algebra.smul_def]
-- 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
F : AlgebraNorm K L :=
  let __src := F'.toRingNorm hF'_0;
  { toRingNorm := __src, smul' := ⋯ }
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
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' := ⋯ }
⊢ ∃ (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
    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.InvariantExtension (goal)
Goal:
K : Type u_1
inst : NormedField K
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
h_fin : FiniteDimensional K L
hu : IsUltrametricDist K
σ : L ≃ₐ[K] L
x : L
n : ℕ
hn : 1 ≤ n
⊢ (algNormOfAlgEquiv σ : (a : L) → ℝ) (x ^ n) = HPow.hPow (α := ℝ) ((algNormOfAlgEquiv σ : (a : L) → ℝ) x : ℝ) n
have simp : (Classical.choose (p := fun (x : AlgebraNorm K L) ↦
        IsPowMul (R := L) (⇑x : (a : L) → ℝ) ∧
          (∀ (x_1 : K), (x : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x_1 : L) = ‖x_1‖) ∧
            IsNonarchimedean (R := ℝ) (α := L) (⇑x : (a : L) → ℝ))
        sorry :
      (a : L) → ℝ)
    (HPow.hPow (α := L) ((σ : (a : L) → L) x : L) n) =
  HPow.hPow (α := ℝ)
    ((Classical.choose (p := fun (x : AlgebraNorm K L) ↦
            IsPowMul (R := L) (⇑x : (a : L) → ℝ) ∧
              (∀ (x_1 : K), (x : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x_1 : L) = ‖x_1‖) ∧
                IsNonarchimedean (R := ℝ) (α := L) (⇑x : (a : L) → ℝ))
            sorry :
          (a : L) → ℝ)
        ((σ : (a : L) → L) x : L) :
      ℝ)
    n
Tactic: simp only [algNormOfAlgEquiv_apply, map_pow σ x n]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.InvariantExtension (goal)
Goal:
K : Type u_1
inst : NormedField K
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
h_fin : FiniteDimensional K L
hu : IsUltrametricDist K
σ : L ≃ₐ[K] L
x y : L
⊢ LE.le (α := ℝ) ((algNormOfAlgEquiv σ : (a : L) → ℝ) (x + y) : ℝ)
    (max ((algNormOfAlgEquiv σ : (a : L) → ℝ) x) ((algNormOfAlgEquiv σ : (a : L) → ℝ) y) : ℝ)
have simp : LE.le (α := ℝ)
  ((Classical.choose (p := fun (x : AlgebraNorm K L) ↦
          IsPowMul (R := L) (⇑x : (a : L) → ℝ) ∧
            (∀ (x_1 : K), (x : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x_1 : L) = ‖x_1‖) ∧
              IsNonarchimedean (R := ℝ) (α := L) (⇑x : (a : L) → ℝ))
          sorry :
        (a : L) → ℝ)
      (HAdd.hAdd (α := L) (β := L) ((σ : (a : L) → L) x : L) ((σ : (a : L) → L) y : L)) :
    ℝ)
  (max
      ((Classical.choose (p := fun (x : AlgebraNorm K L) ↦
            IsPowMul (R := L) (⇑x : (a : L) → ℝ) ∧
              (∀ (x_1 : K), (x : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x_1 : L) = ‖x_1‖) ∧
                IsNonarchimedean (R := ℝ) (α := L) (⇑x : (a : L) → ℝ))
            sorry :
          (a : L) → ℝ)
        ((σ : (a : L) → L) x : L))
      ((Classical.choose (p := fun (x : AlgebraNorm K L) ↦
            IsPowMul (R := L) (⇑x : (a : L) → ℝ) ∧
              (∀ (x_1 : K), (x : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x_1 : L) = ‖x_1‖) ∧
                IsNonarchimedean (R := ℝ) (α := L) (⇑x : (a : L) → ℝ))
            sorry :
          (a : L) → ℝ)
        ((σ : (a : L) → L) y : L)) :
    ℝ)
Tactic: simp only [algNormOfAlgEquiv_apply, map_add σ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.InvariantExtension (goal)
Goal:
K : Type u_1
inst : NormedField K
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
h_fin : FiniteDimensional K L
hu : IsUltrametricDist K
σ : L ≃ₐ[K] L
x : K
⊢ (algNormOfAlgEquiv σ : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
have simp : (Classical.choose (p := fun (x : AlgebraNorm K L) ↦
        IsPowMul (R := L) (⇑x : (a : L) → ℝ) ∧
          (∀ (x_1 : K), (x : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x_1 : L) = ‖x_1‖) ∧
            IsNonarchimedean (R := ℝ) (α := L) (⇑x : (a : L) → ℝ))
        sorry :
      (a : L) → ℝ)
    ((algebraMap K L : (a : K) → L) x : L) =
  ‖x‖
Tactic: simp only [algNormOfAlgEquiv_apply, AlgEquiv.commutes]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.InvariantExtension (goal)
Goal:
K : Type u_1
inst : NormedField K
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
h_fin : FiniteDimensional K L
hu : IsUltrametricDist K
x : L
⊢ Eq (α := ℝ) (⨆ (σ : L ≃ₐ[K] L), (algNormOfAlgEquiv σ : (a : L) → ℝ) x) 0 → x = 0
have contrapose! : x ≠ 0 → Ne (α := ℝ) (⨆ (σ : L ≃ₐ[K] L), (algNormOfAlgEquiv σ : (a : L) → ℝ) x) 0
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.InvariantExtension (goal)
Goal:
K : Type u_1
inst : NormedField K
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
h_fin : FiniteDimensional K L
hu : IsUltrametricDist K
x : L
n : ℕ
hn : 1 ≤ n
⊢ (invariantExtension K L : (a : L) → ℝ) (x ^ n) = HPow.hPow (α := ℝ) ((invariantExtension K L : (a : L) → ℝ) x : ℝ) n
have rw : Eq (α := ℝ) (⨆ (σ : L ≃ₐ[K] L), (algNormOfAlgEquiv σ : (a : L) → ℝ) (x ^ n))
  (⨆ (i : L ≃ₐ[K] L), HPow.hPow (α := ℝ) ((algNormOfAlgEquiv i : (a : L) → ℝ) x : ℝ) n)
Tactic: rw [invariantExtension_apply, invariantExtension_apply, Real.iSup_pow
    (fun σ ↦ apply_nonneg (algNormOfAlgEquiv σ) x)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (goal)
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
β : Type u_3
inst_3 : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
hf : RingHom.IsBoundedWrt (⇑nα : (a : α) → ℝ) nβ f
x : α
⊢ nβ ((f : (a : α) → β) x) ≤ (nα : (a : α) → ℝ) x
have obtain : ∀ (C : ℝ) (hC0 : 0 < C) (hC : ∀ (x : α), nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) C ((nα : (a : α) → ℝ) x : ℝ)),
  nβ ((f : (a : α) → β) x) ≤ (nα : (a : α) → ℝ) x
Tactic: obtain ⟨C, hC0, hC⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (goal)
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
β : Type u_3
inst_3 : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) C ((nα : (a : α) → ℝ) x : ℝ)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ))
    atTop (𝓝 ((nα : (a : α) → ℝ) x) : Filter ℝ)
have nth_rewrite : Tendsto (fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ)) atTop
  (𝓝 (HMul.hMul (α := ℝ) (β := ℝ) (1 : ℝ) ((nα : (a : α) → ℝ) x : ℝ)))
Tactic: nth_rewrite 2 [← one_mul (nα x)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (hypothesis)
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
β : Type u_3
inst_3 : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) C ((nα : (a : α) → ℝ) x : ℝ)
⊢ nβ ((f : (a : α) → β) x) ≤ (nα : (a : α) → ℝ) x
have hlim : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ)) atTop
  (𝓝 ((nα : (a : α) → ℝ) x) : Filter ℝ)
Tactic: have hlim : Tendsto (fun n : ℕ => C ^ (1 / (n : ℝ)) * nα x) atTop (𝓝 (nα x)) := by
    nth_rewrite 2 [← one_mul (nα x)]
    exact ((rpow_zero C ▸ ContinuousAt.tendsto (continuousAt_const_rpow (ne_of_gt hC0))).comp
      (tendsto_const_div_atTop_nhds_zero_nat 1)).mul tendsto_const_nhds
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (goal)
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
β : Type u_3
inst_3 : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) C ((nα : (a : α) → ℝ) x : ℝ)
hlim :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ))
    atTop (𝓝 ((nα : (a : α) → ℝ) x) : Filter ℝ)
⊢ nβ ((f : (a : α) → β) x) ≤ (nα : (a : α) → ℝ) x
have apply : ∀ᶠ (c : ℕ) in atTop,
  nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑c : ℝ)) ((nα : (a : α) → ℝ) x : ℝ)
Tactic: apply ge_of_tendsto hlim
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (goal)
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
β : Type u_3
inst_3 : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) C ((nα : (a : α) → ℝ) x : ℝ)
hlim :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ))
    atTop (𝓝 ((nα : (a : α) → ℝ) x) : Filter ℝ)
⊢ ∀ᶠ (c : ℕ) in atTop,
    nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑c : ℝ)) ((nα : (a : α) → ℝ) x : ℝ)
have simp : ∃ (a : ℕ),
  ∀ (b : ℕ),
    a ≤ b → nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑b : ℝ)) ((nα : (a : α) → ℝ) x : ℝ)
Tactic: simp only [eventually_atTop, ge_iff_le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (goal)
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
β : Type u_3
inst_3 : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) C ((nα : (a : α) → ℝ) x : ℝ)
hlim :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ))
    atTop (𝓝 ((nα : (a : α) → ℝ) x) : Filter ℝ)
⊢ ∃ (a : ℕ),
    ∀ (b : ℕ),
      a ≤ b →
        nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑b : ℝ)) ((nα : (a : α) → ℝ) x : ℝ)
have h : ∀ (b : ℕ),
  1 ≤ b → nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑b : ℝ)) ((nα : (a : α) → ℝ) x : ℝ)
Tactic: use 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (hypothesis)
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
β : Type u_3
inst_3 : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) C ((nα : (a : α) → ℝ) x : ℝ)
hlim :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ))
    atTop (𝓝 ((nα : (a : α) → ℝ) x) : Filter ℝ)
n : ℕ
hn : 1 ≤ n
⊢ (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ^ n = C
have hn0 : Ne (α := ℝ) (↑n : ℝ) 0
Tactic: have hn0 : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (ne_of_gt hn)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (goal)
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
β : Type u_3
inst_3 : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) C ((nα : (a : α) → ℝ) x : ℝ)
hlim :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ))
    atTop (𝓝 ((nα : (a : α) → ℝ) x) : Filter ℝ)
n : ℕ
hn : 1 ≤ n
hn0 : Ne (α := ℝ) (↑n : ℝ) 0
⊢ (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ^ n = C
have rw : HPow.hPow (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) (↑n : ℝ) = C
Tactic: rw [← rpow_natCast, ← rpow_mul hC0.le, one_div, inv_mul_cancel₀ hn0, rpow_one]