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
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‖

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))
-- 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' := ⋯ }
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) → ℝ)

Tactic:
⟨F, isPowMul_smoothingFun f hf_1, hF_ext, isNonarchimedean_smoothingFun f hf_1 hf_na⟩

Premises used: isPowMul_smoothingFun, And.intro, Exists.intro, isNonarchimedean_smoothingFun
-- Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension
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
⊢ Eq (α := ℝ)
    ((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) → ℝ))
            ⋯ :
          (a : L) → ℝ)
        ((σ : (a : L) → L) 0 : L) :
      ℝ)
    (0 : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension
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
⊢ (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) → ℝ))
          ⋯ :
        (a : L) → ℝ)
      ((σ : (a : L) → L) (x + y) : L) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ)
      ((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) → ℝ))
              ⋯ :
            (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) → ℝ))
              ⋯ :
            (a : L) → ℝ)
          ((σ : (a : L) → L) y : L) :
        ℝ)

Tactic:
simp [map_add σ, map_add_le_add]

Premises used: map_add, SubadditiveHomClass.map_add_le_add
-- Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension
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
⊢ Eq (α := ℝ)
    ((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) → ℝ))
            ⋯ :
          (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) → ℝ))
            ⋯ :
          (a : L) → ℝ)
        ((σ : (a : L) → L) x : L) :
      ℝ)

Tactic:
simp [map_neg σ, map_neg_eq_map]

Premises used: AddGroupSeminormClass.map_neg_eq_map, map_neg
-- Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension
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
⊢ (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) → ℝ))
          ⋯ :
        (a : L) → ℝ)
      ((σ : (a : L) → L) (x * y) : L) ≤
    HMul.hMul (α := ℝ) (β := ℝ)
      ((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) → ℝ))
              ⋯ :
            (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) → ℝ))
              ⋯ :
            (a : L) → ℝ)
          ((σ : (a : L) → L) y : L) :
        ℝ)

Tactic:
simp [map_mul σ, map_mul_le_mul]

Premises used: map_mul, SubmultiplicativeHomClass.map_mul_le_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension
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
y : 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) → ℝ))
          ⋯ :
        (a : L) → ℝ)
      ((σ : (a : L) → L) (x • y) : L) =
    HMul.hMul (β := ℝ) ‖x‖
      ((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) → ℝ))
              ⋯ :
            (a : L) → ℝ)
          ((σ : (a : L) → L) y : L) :
        ℝ)

Tactic:
simp [map_smul σ, map_smul_eq_mul]

Premises used: SeminormClass.map_smul_eq_mul, map_smul
-- Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension
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
⊢ Eq (α := ℝ) ((algNormOfAlgEquiv σ : (a : L) → ℝ) x : ℝ)
    ((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) → ℝ))
            ⋯ :
          (a : L) → ℝ)
        ((σ : (a : L) → L) x : L) :
      ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension
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
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) → ℝ))
          ⋯ :
        (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) → ℝ))
              ⋯ :
            (a : L) → ℝ)
          ((σ : (a : L) → L) x : L) :
        ℝ)
      n
⊢ (algNormOfAlgEquiv σ : (a : L) → ℝ) (x ^ n) = HPow.hPow (α := ℝ) ((algNormOfAlgEquiv σ : (a : L) → ℝ) x : ℝ) n

Tactic:
simp only [algNormOfAlgEquiv_apply, map_pow σ x n]

Premises used: map_pow, IsUltrametricDist.algNormOfAlgEquiv_apply
-- Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension
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
⊢ (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) → ℝ))
          ⋯ :
        (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) → ℝ))
              ⋯ :
            (a : L) → ℝ)
          ((σ : (a : L) → L) x : L) :
        ℝ)
      n

Tactic:
(Classical.choose_spec (exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional
    h_fin hu.isNonarchimedean_norm)).1 _ hn

Premises used: IsUltrametricDist.isNonarchimedean_norm, exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional, Classical.choose_spec, And.left
-- Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension
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
⊢ (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) → ℝ))
          ⋯ :
        (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) → ℝ))
              ⋯ :
            (a : L) → ℝ)
          ((σ : (a : L) → L) x : L) :
        ℝ)
      n

Tactic:
exact (Classical.choose_spec (exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional
    h_fin hu.isNonarchimedean_norm)).1 _ hn

Premises used: IsUltrametricDist.isNonarchimedean_norm, exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional, Classical.choose_spec, And.left
-- Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension
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
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) → ℝ))
            ⋯ :
          (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) → ℝ))
              ⋯ :
            (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) → ℝ))
              ⋯ :
            (a : L) → ℝ)
          ((σ : (a : L) → L) y : L)) :
      ℝ)
⊢ LE.le (α := ℝ) ((algNormOfAlgEquiv σ : (a : L) → ℝ) (x + y) : ℝ)
    (max ((algNormOfAlgEquiv σ : (a : L) → ℝ) x) ((algNormOfAlgEquiv σ : (a : L) → ℝ) y) : ℝ)

Tactic:
simp only [algNormOfAlgEquiv_apply, map_add σ]

Premises used: map_add, IsUltrametricDist.algNormOfAlgEquiv_apply
-- Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension
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 (α := ℝ)
    ((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) → ℝ))
            ⋯ :
          (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) → ℝ))
              ⋯ :
            (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) → ℝ))
              ⋯ :
            (a : L) → ℝ)
          ((σ : (a : L) → L) y : L)) :
      ℝ)

Tactic:
(Classical.choose_spec (exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional
    h_fin hu.isNonarchimedean_norm)).2.2 _ _

Premises used: IsUltrametricDist.isNonarchimedean_norm, exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional, Classical.choose_spec, And.right
-- Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension
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 (α := ℝ)
    ((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) → ℝ))
            ⋯ :
          (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) → ℝ))
              ⋯ :
            (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) → ℝ))
              ⋯ :
            (a : L) → ℝ)
          ((σ : (a : L) → L) y : L)) :
      ℝ)

Tactic:
exact (Classical.choose_spec (exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional
    h_fin hu.isNonarchimedean_norm)).2.2 _ _

Premises used: IsUltrametricDist.isNonarchimedean_norm, exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional, Classical.choose_spec, And.right
-- Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension
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
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) → ℝ))
          ⋯ :
        (a : L) → ℝ)
      ((algebraMap K L : (a : K) → L) x : L) =
    ‖x‖
⊢ (algNormOfAlgEquiv σ : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖

Tactic:
simp only [algNormOfAlgEquiv_apply, AlgEquiv.commutes]

Premises used: AlgEquiv.commutes, IsUltrametricDist.algNormOfAlgEquiv_apply
-- Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension
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
⊢ (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) → ℝ))
          ⋯ :
        (a : L) → ℝ)
      ((algebraMap K L : (a : K) → L) x : L) =
    ‖x‖

Tactic:
(Classical.choose_spec (exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional
    h_fin hu.isNonarchimedean_norm)).2.1 _

Premises used: IsUltrametricDist.isNonarchimedean_norm, exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional, Classical.choose_spec, And.right, And.left
-- Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension
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
⊢ (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) → ℝ))
          ⋯ :
        (a : L) → ℝ)
      ((algebraMap K L : (a : K) → L) x : L) =
    ‖x‖

Tactic:
exact (Classical.choose_spec (exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional
    h_fin hu.isNonarchimedean_norm)).2.1 _

Premises used: IsUltrametricDist.isNonarchimedean_norm, exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional, Classical.choose_spec, And.right, And.left
-- Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension
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
⊢ Eq (α := ℝ) (⨆ (σ : L ≃ₐ[K] L), (algNormOfAlgEquiv σ : (a : L) → ℝ) 0) 0

Tactic:
simp only [map_zero, ciSup_const]

Premises used: map_zero, ciSup_const
-- Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension
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))
    (⨆ (σ : L ≃ₐ[K] L), (algNormOfAlgEquiv σ : (a : L) → ℝ) x)

Tactic:
simp only [map_neg_eq_map]

Premises used: AddGroupSeminormClass.map_neg_eq_map
-- Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension
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
contrapose! : x ≠ 0 → Ne (α := ℝ) (⨆ (σ : L ≃ₐ[K] L), (algNormOfAlgEquiv σ : (a : L) → ℝ) x) 0
⊢ Eq (α := ℝ) (⨆ (σ : L ≃ₐ[K] L), (algNormOfAlgEquiv σ : (a : L) → ℝ) x) 0 → x = 0

Tactic:
contrapose!