awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
S : Type u_2
inst : SeminormedCommRing R
inst_1 : Ring S
inst_2 : Algebra R S
f : MulAlgebraNorm R S
a : R
⊢ (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = ‖a‖

Tactic:
extends_norm' _ _

Premises used: MulAlgebraNorm.extends_norm'
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
S : Type u_2
inst : SeminormedCommRing R
inst_1 : Ring S
inst_2 : Algebra R S
f : MulAlgebraNorm R S
a : R
⊢ (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = ‖a‖

Tactic:
exact extends_norm' _ _

Premises used: MulAlgebraNorm.extends_norm'
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
S : Type u_2
inst : SeminormedCommRing R
inst_1 : Ring S
inst_2 : Algebra R S
f : MulAlgebraNorm R S
⊢ Eq (α := (a : S) → ℝ) (⇑f.toAlgebraNorm : (a : S) → ℝ) (⇑f : (a : S) → ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : NormedField L
inst_2 : NormedAlgebra K L
r : K
x : L
simp :
  (MulRingNorm.toMulRingSeminorm (NormedField.toMulRingNorm L) : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) r : L) =
      ‖r‖ ∨
    x = 0
⊢ AddGroupSeminorm.toFun
      (MulRingSeminorm.toAddGroupSeminorm (MulRingNorm.toMulRingSeminorm (NormedField.toMulRingNorm L))) (r • x) =
    ‖r‖ *
      AddGroupSeminorm.toFun
        (MulRingSeminorm.toAddGroupSeminorm (MulRingNorm.toMulRingSeminorm (NormedField.toMulRingNorm L))) x

Tactic:
simp only [Algebra.smul_def, AddGroupSeminorm.toFun_eq_coe, MulRingSeminorm.toFun_eq_coe,
      map_mul, mul_eq_mul_right_iff, map_eq_zero]

Premises used: AddGroupSeminorm.toFun_eq_coe, mul_eq_mul_right_iff, map_eq_zero, map_mul, MulRingSeminorm.toFun_eq_coe, Algebra.smul_def
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : NormedField L
inst_2 : NormedAlgebra K L
r : K
x : L
⊢ (MulRingNorm.toMulRingSeminorm (NormedField.toMulRingNorm L) : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) r : L) =
      ‖r‖ ∨
    x = 0

Tactic:
Or.inl <| norm_algebraMap' L r

Premises used: Or.inl, norm_algebraMap'
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : NormedField L
inst_2 : NormedAlgebra K L
r : K
x : L
⊢ (MulRingNorm.toMulRingSeminorm (NormedField.toMulRingNorm L) : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) r : L) =
      ‖r‖ ∨
    x = 0

Tactic:
exact Or.inl <| norm_algebraMap' L r

Premises used: Or.inl, norm_algebraMap'
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : NormedField L
inst_2 : NormedAlgebra K L
x : L
⊢ (toMulAlgebraNorm K L : (a : L) → ℝ) x = ‖x‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
A : Type u_2
inst : Ring A
f : MulRingNorm A
x : A
n : ℕ
hn : 1 ≤ n
zero :
  ∀ (hn : LE.le (α := ℕ) 1 0),
    (f : (a : A) → ℝ) (HPow.hPow (β := ℕ) x 0) = HPow.hPow (α := ℝ) (β := ℕ) ((f : (a : A) → ℝ) x : ℝ) 0
succ :
  ∀ (n : ℕ) (hn : 1 ≤ n + 1), (f : (a : A) → ℝ) (x ^ (n + 1)) = HPow.hPow (α := ℝ) ((f : (a : A) → ℝ) x : ℝ) (n + 1)
⊢ (f : (a : A) → ℝ) (x ^ n) = HPow.hPow (α := ℝ) ((f : (a : A) → ℝ) x : ℝ) n

Tactic:
cases n
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
A : Type u_2
inst : Ring A
f : MulRingNorm A
x : A
hn : LE.le (α := ℕ) 1 0
⊢ (f : (a : A) → ℝ) (HPow.hPow (β := ℕ) x 0) = HPow.hPow (α := ℝ) (β := ℕ) ((f : (a : A) → ℝ) x : ℝ) 0

Tactic:
lia
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
A : Type u_2
inst : Ring A
f : MulRingNorm A
x : A
n : ℕ
hn : 1 ≤ n + 1
succ succ₁ : HPow.hPow (α := ℝ) ((f : (a : A) → ℝ) x : ℝ) (n + 1) = HPow.hPow (α := ℝ) ((f : (a : A) → ℝ) x : ℝ) (n + 1)
⊢ (f : (a : A) → ℝ) (x ^ (n + 1)) = HPow.hPow (α := ℝ) ((f : (a : A) → ℝ) x : ℝ) (n + 1)

Tactic:
rw [map_pow]

Premises used: map_pow
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
x : L
i : ι
⊢ Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K) ≤ B.norm x

Tactic:
Finset.le_sup' (fun i : ι ↦ ‖B.repr x i‖) (mem_univ i)

Premises used: Finset.mem_univ, Norm.norm, Module.Basis.norm, Module.Basis.repr, Finset.le_sup', DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
⊢ B.norm 0 = 0

Tactic:
simp [norm, map_zero, norm_zero]

Premises used: norm_zero, Module.Basis.norm, map_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
x : L
⊢ B.norm (-x) = B.norm x

Tactic:
simp [norm, map_neg, Pi.neg_apply, _root_.norm_neg]

Premises used: Module.Basis.norm, map_neg, norm_neg, Pi.neg_apply
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
x : L
⊢ 0 ≤ B.norm x

Tactic:
simp only [norm, le_sup'_iff, mem_univ, norm_nonneg, and_self, exists_const]

Premises used: Finset.mem_univ, Finset.le_sup'_iff, and_self, Module.Basis.norm, exists_const, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i : L) (1 : L)
x : K
simp : (sup' univ ⋯ fun (x_1 : ι) ↦ ‖if i = x_1 then x else 0‖) = ‖x‖
⊢ B.norm ((algebraMap K L : (a : K) → L) x) = ‖x‖

Tactic:
simp only [norm, repr_algebraMap hBi, Finsupp.single_apply]

Premises used: Module.Basis.repr_algebraMap, Module.Basis.norm, Finsupp.single_apply
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i : L) (1 : L)
x : K
a : (sup' univ ⋯ fun (x_1 : ι) ↦ ‖if i = x_1 then x else 0‖) ≤ ‖x‖
a₁ : ‖x‖ ≤ sup' univ ⋯ fun (x_1 : ι) ↦ ‖if i = x_1 then x else 0‖
⊢ (sup' univ ⋯ fun (x_1 : ι) ↦ ‖if i = x_1 then x else 0‖) = ‖x‖

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i : L) (1 : L)
x : K
⊢ (sup' univ ⋯ fun (x_1 : ι) ↦ ‖if i = x_1 then x else 0‖) ≤ ‖x‖

Tactic:
aesop
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i : L) (1 : L)
x : K
⊢ ‖x‖ ≤ ‖if i = i then x else 0‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i : L) (1 : L)
x : K
⊢ ‖x‖ ≤ sup' univ ⋯ fun (x_1 : ι) ↦ ‖if i = x_1 then x else 0‖

Tactic:
exact le_sup'_of_le _ (mem_univ i) (by simp)

Premises used: Finset.mem_univ, Finset.le_sup'_of_le
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i : L) (1 : L)
x : K
simp : (sup' univ ⋯ fun (x_1 : ι) ↦ ‖if i = x_1 then x else 0‖) = ‖x‖
a : (sup' univ ⋯ fun (x_1 : ι) ↦ ‖if i = x_1 then x else 0‖) ≤ ‖x‖
a₁ a₂ : ‖x‖ ≤ sup' univ ⋯ fun (x_1 : ι) ↦ ‖if i = x_1 then x else 0‖
⊢ B.norm ((algebraMap K L : (a : K) → L) x) = ‖x‖

Tactic:
classical
  simp only [norm, repr_algebraMap hBi, Finsupp.single_apply]
  apply le_antisymm
  · aesop
  · exact le_sup'_of_le _ (mem_univ i) (by simp)

Premises used: Finset.mem_univ, Finset.le_sup'_of_le, Module.Basis.repr_algebraMap, Module.Basis.norm, le_antisymm, Finsupp.single_apply
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
x y : L
obtain :
  ∀ (ixy : ι),
    Membership.mem (γ := Finset ι) univ ixy →
      ∀
        (hixy :
          (sup' univ ⋯ fun (i : ι) ↦
              Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) i : K)) =
            Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K)),
        B.norm (x + y) ≤ max (B.norm x) (B.norm y)
⊢ B.norm (x + y) ≤ max (B.norm x) (B.norm y)

Tactic:
obtain ⟨ixy, _, hixy⟩ := exists_mem_eq_sup' univ_nonempty (fun i ↦ ‖(B.repr (x + y)) i‖)

Premises used: Norm.norm, Finset.univ_nonempty, Module.Basis.repr, HAdd.hAdd, Finset.exists_mem_eq_sup', DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
x y : L
ixy : ι
left : Membership.mem (γ := Finset ι) univ ixy
hixy :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) i : K)) =
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K)
rw :
  ‖HAdd.hAdd (α := K) (β := K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) ixy : K)
        ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) ixy : K)‖ ≤
    max (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) ixy : K))
      (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) ixy : K))
⊢ Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
    max (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) ixy : K))
      (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) ixy : K))

Tactic:
rw [map_add, Finsupp.coe_add, Pi.add_apply]

Premises used: map_add, Pi.add_apply, Finsupp.coe_add
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
x y : L
ixy : ι
left : Membership.mem (γ := Finset ι) univ ixy
hixy :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) i : K)) =
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K)
⊢ ‖HAdd.hAdd (α := K) (β := K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) ixy : K)
        ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) ixy : K)‖ ≤
    max (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) ixy : K))
      (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) ixy : K))

Tactic:
hna _ _
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
x y : L
ixy : ι
left : Membership.mem (γ := Finset ι) univ ixy
hixy :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) i : K)) =
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K)
⊢ ‖HAdd.hAdd (α := K) (β := K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) ixy : K)
        ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) ixy : K)‖ ≤
    max (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) ixy : K))
      (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) ixy : K))

Tactic:
exact hna _ _
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
x y : L
ixy : ι
left : Membership.mem (γ := Finset ι) univ ixy
hixy :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) i : K)) =
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K)
⊢ Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
    max (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) ixy : K))
      (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) ixy : K))

Tactic:
have hxy : ‖B.repr (x + y) ixy‖ ≤ max ‖B.repr x ixy‖ ‖B.repr y ixy‖ := by
    rw [map_add, Finsupp.coe_add, Pi.add_apply]; exact hna _ _
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
x y : L
ixy : ι
left : Membership.mem (γ := Finset ι) univ ixy
hixy :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) i : K)) =
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K)
hxy :
  Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
    max (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) ixy : K))
      (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) ixy : K))
rw :
  Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
    max (B.norm x) (B.norm y)
⊢ B.norm (x + y) ≤ max (B.norm x) (B.norm y)

Tactic:
rw [Basis.norm, hixy]

Premises used: Module.Basis.norm
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
x y : L
ixy : ι
left : Membership.mem (γ := Finset ι) univ ixy
hixy :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) i : K)) =
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K)
hxy :
  Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
    max (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) ixy : K))
      (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) ixy : K))
inl :
  ∀
    (hx :
      Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
        Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) ixy : K)),
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
      max (B.norm x) (B.norm y)
inr :
  ∀
    (hy :
      Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
        Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) ixy : K)),
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
      max (B.norm x) (B.norm y)
⊢ Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
    max (B.norm x) (B.norm y)

Tactic:
rcases le_max_iff.mp hxy with (hx | hy)

Premises used: Iff.mp, le_max_iff
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
x y : L
ixy : ι
left : Membership.mem (γ := Finset ι) univ ixy
hixy :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) i : K)) =
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K)
hxy :
  Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
    max (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) ixy : K))
      (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) ixy : K))
hx :
  Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) ixy : K)
⊢ Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
    max (B.norm x) (B.norm y)

Tactic:
le_max_of_le_left (le_trans hx (norm_repr_le_norm B ixy))

Premises used: le_max_of_le_left, Module.Basis.norm_repr_le_norm, le_trans
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
x y : L
ixy : ι
left : Membership.mem (γ := Finset ι) univ ixy
hixy :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) i : K)) =
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K)
hxy :
  Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
    max (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) ixy : K))
      (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) ixy : K))
hx :
  Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) ixy : K)
⊢ Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
    max (B.norm x) (B.norm y)

Tactic:
exact le_max_of_le_left (le_trans hx (norm_repr_le_norm B ixy))

Premises used: le_max_of_le_left, Module.Basis.norm_repr_le_norm, le_trans
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
x y : L
ixy : ι
left : Membership.mem (γ := Finset ι) univ ixy
hixy :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) i : K)) =
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K)
hxy :
  Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
    max (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) ixy : K))
      (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) ixy : K))
hy :
  Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) ixy : K)
⊢ Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
    max (B.norm x) (B.norm y)

Tactic:
le_max_of_le_right (le_trans hy (norm_repr_le_norm B ixy))

Premises used: le_max_of_le_right, Module.Basis.norm_repr_le_norm, le_trans
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
x y : L
ixy : ι
left : Membership.mem (γ := Finset ι) univ ixy
hixy :
  (sup' univ ⋯ fun (i : ι) ↦
      Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) i : K)) =
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K)
hxy :
  Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
    max (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) ixy : K))
      (Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) ixy : K))
hy :
  Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
    Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) y : ι →₀ K) : (a : ι) → K) ixy : K)
⊢ Norm.norm.{u_1} (E := K) ((((B.repr : (a : L) → ι →₀ K) (x + y) : ι →₀ K) : (a : ι) → K) ixy : K) ≤
    max (B.norm x) (B.norm y)

Tactic:
exact le_max_of_le_right (le_trans hy (norm_repr_le_norm B ixy))

Premises used: le_max_of_le_right, Module.Basis.norm_repr_le_norm, le_trans
-- Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : Ring L
inst_2 : Algebra K L
ι : Type u_3
inst_3 : Fintype ι
inst_4 : Nonempty ι
B : Basis ι K L
i : ι
hBi : Eq.{u_2 + 1} (α := L) ((B : (a : ι) → L) i : L) (1 : L)
hna : IsNonarchimedean.{0, u_1} (α := K) Norm.norm
obtain :
  ∀ (c : ι × ι),
    Membership.mem (γ := Finset (ι × ι)) univ c →
      ∀
        (hc :
          (sup' univ ⋯ fun (i : ι × ι) ↦
              B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) i.1 : L) ((B : (a : ι) → L) i.2 : L))) =
            B.norm (HMul.hMul (α := L) (β := L) ((B : (a : ι) → L) c.1 : L) ((B : (a : ι) → L) c.2 : L))),
        ∃ (c : ℝ) (_ : 0 < c), ∀ (x y : L), B.norm (x * y) ≤ c * B.norm x * B.norm y
⊢ ∃ (c : ℝ) (_ : 0 < c), ∀ (x y : L), B.norm (x * y) ≤ c * B.norm x * B.norm y

Tactic:
obtain ⟨c, _, hc⟩ := exists_mem_eq_sup' univ_nonempty (fun i : ι × ι ↦ B.norm (B i.1 * B i.2))

Premises used: HMul.hMul, Finset.univ_nonempty, Module.Basis.norm, Prod.fst, Finset.exists_mem_eq_sup', Prod.snd, DFunLike.coe