awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
x : E
a : ι
s : Finset ι
ha : a ∉ s
ih : (s.sup p : (a : E) → ℝ) x = (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
cons :
  (p a ⊔ s.sup p : (a : E) → ℝ) x = (↑((Finset.cons a s ha).sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
cons₁ :
  (p a ⊔ s.sup p : (a : E) → ℝ) x =
    (↑(max (NNReal.mk ((p a : (a : E) → ℝ) x) ⋯) (s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯)) : ℝ)
cons₂ :
  ((⇑(p a) : (a : E) → ℝ) ⊔ (⇑(s.sup p) : (a : E) → ℝ)) x =
    (↑(max (NNReal.mk ((p a : (a : E) → ℝ) x) ⋯) (s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯)) : ℝ)
cons₃ :
  max ((p a : (a : E) → ℝ) x) ((s.sup p : (a : E) → ℝ) x) =
    (↑(max (NNReal.mk ((p a : (a : E) → ℝ) x) ⋯) (s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯)) : ℝ)
cons₄ :
  max ((p a : (a : E) → ℝ) x) ((s.sup p : (a : E) → ℝ) x) =
    max (↑(NNReal.mk ((p a : (a : E) → ℝ) x) ⋯) : ℝ) (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
cons₅ :
  Eq (α := ℝ) (max ((p a : (a : E) → ℝ) x) ((s.sup p : (a : E) → ℝ) x) : ℝ)
    (max ((p a : (a : E) → ℝ) x) (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ) : ℝ)
cons₆ cons₇ :
  Eq (α := ℝ) (max ((p a : (a : E) → ℝ) x) (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ) : ℝ)
    (max ((p a : (a : E) → ℝ) x) (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ) : ℝ)
⊢ ((Finset.cons a s ha).sup p : (a : E) → ℝ) x =
    (↑((Finset.cons a s ha).sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)

Tactic:
rw [Finset.sup_cons, Finset.sup_cons, coe_sup, Pi.sup_apply, NNReal.coe_max, NNReal.coe_mk, ih]

Premises used: Seminorm.coe_sup, NNReal.coe_mk, Pi.sup_apply, Finset.sup_cons, NNReal.coe_max
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
empty : (Finset.sup ∅ p : (a : E) → ℝ) x = (↑(Finset.sup ∅ fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
cons :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
    (ih : (s.sup p : (a : E) → ℝ) x = (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)),
    ((Finset.cons a s ha).sup p : (a : E) → ℝ) x =
      (↑((Finset.cons a s ha).sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
⊢ (s.sup p : (a : E) → ℝ) x = (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)

Tactic:
induction s using Finset.cons_induction_on with
  | empty =>
    rw [Finset.sup_empty, Finset.sup_empty, coe_bot, _root_.bot_eq_zero, Pi.zero_apply]
    norm_cast
  | cons a s ha ih =>
    rw [Finset.sup_cons, Finset.sup_cons, coe_sup, Pi.sup_apply, NNReal.coe_max, NNReal.coe_mk, ih]

Premises used: Pi.zero_apply, Seminorm.coe_sup, Finset.sup_empty, NNReal.coe_mk, Seminorm.coe_bot, Pi.sup_apply, Finset.sup_cons, bot_eq_zero, NNReal.coe_max
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
hs : s.Nonempty
x : E
rcases :
  ∀ (i : ι) (hi : i ∈ s)
    (hix :
      Eq (α := { r : ℝ // 0 ≤ r })
        (s.sup fun (i : ι) ↦ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ((p i : (a : E) → ℝ) x) ⋯ : { r : ℝ // 0 ≤ r })
        (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ((p i : (a : E) → ℝ) x) ⋯ : { r : ℝ // 0 ≤ r })),
    ∃ i ∈ s, Eq (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) ((p i : (a : E) → ℝ) x : ℝ)
⊢ ∃ i ∈ s, Eq (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) ((p i : (a : E) → ℝ) x : ℝ)

Tactic:
rcases Finset.exists_mem_eq_sup s hs (fun i ↦ (⟨p i x, apply_nonneg _ _⟩ : ℝ≥0)) with ⟨i, hi, hix⟩

Premises used: Subtype.mk, Finset.exists_mem_eq_sup, NonnegHomClass.apply_nonneg, DFunLike.coe
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
hs : s.Nonempty
x : E
i : ι
hi : i ∈ s
hix :
  Eq (α := { r : ℝ // 0 ≤ r })
    (s.sup fun (i : ι) ↦ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ((p i : (a : E) → ℝ) x) ⋯ : { r : ℝ // 0 ≤ r })
    (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ((p i : (a : E) → ℝ) x) ⋯ : { r : ℝ // 0 ≤ r })
rw : ∃ i ∈ s, (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ) = (p i : (a : E) → ℝ) x
⊢ ∃ i ∈ s, Eq (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) ((p i : (a : E) → ℝ) x : ℝ)

Tactic:
rw [finset_sup_apply]

Premises used: Seminorm.finset_sup_apply
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
hs : s.Nonempty
x : E
i : ι
hi : i ∈ s
hix :
  Eq (α := { r : ℝ // 0 ≤ r })
    (s.sup fun (i : ι) ↦ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ((p i : (a : E) → ℝ) x) ⋯ : { r : ℝ // 0 ≤ r })
    (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ((p i : (a : E) → ℝ) x) ⋯ : { r : ℝ // 0 ≤ r })
⊢ ∃ i ∈ s, (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ) = (p i : (a : E) → ℝ) x

Tactic:
⟨i, hi, congr_arg _ hix⟩

Premises used: congr_arg, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
hs : s.Nonempty
x : E
i : ι
hi : i ∈ s
hix :
  Eq (α := { r : ℝ // 0 ≤ r })
    (s.sup fun (i : ι) ↦ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ((p i : (a : E) → ℝ) x) ⋯ : { r : ℝ // 0 ≤ r })
    (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ((p i : (a : E) → ℝ) x) ⋯ : { r : ℝ // 0 ≤ r })
⊢ ∃ i ∈ s, (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ) = (p i : (a : E) → ℝ) x

Tactic:
exact ⟨i, hi, congr_arg _ hix⟩
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
inl :
  Eq (α := ℝ) ((Finset.sup ∅ p : (a : E) → ℝ) x : ℝ) (0 : ℝ) ∨
    ∃ (i : ι),
      Membership.mem (γ := Finset ι) ∅ i ∧
        Eq (α := ℝ) ((Finset.sup ∅ p : (a : E) → ℝ) x : ℝ) ((p i : (a : E) → ℝ) x : ℝ)
inr :
  ∀ (hs : s.Nonempty),
    Eq (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) (0 : ℝ) ∨
      ∃ i ∈ s, Eq (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) ((p i : (a : E) → ℝ) x : ℝ)
⊢ Eq (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) (0 : ℝ) ∨
    ∃ i ∈ s, Eq (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) ((p i : (a : E) → ℝ) x : ℝ)

Tactic:
rcases Finset.eq_empty_or_nonempty s with (rfl | hs)

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
x : E
inl : Eq (α := ℝ) ((Finset.sup ∅ p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) ((Finset.sup ∅ p : (a : E) → ℝ) x : ℝ) (0 : ℝ) ∨
    ∃ (i : ι),
      Membership.mem (γ := Finset ι) ∅ i ∧
        Eq (α := ℝ) ((Finset.sup ∅ p : (a : E) → ℝ) x : ℝ) ((p i : (a : E) → ℝ) x : ℝ)

Tactic:
left
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
x : E
⊢ Eq (α := ℝ) ((Finset.sup ∅ p : (a : E) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
hs : s.Nonempty
inr : ∃ i ∈ s, Eq (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) ((p i : (a : E) → ℝ) x : ℝ)
⊢ Eq (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) (0 : ℝ) ∨
    ∃ i ∈ s, Eq (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) ((p i : (a : E) → ℝ) x : ℝ)

Tactic:
right
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
hs : s.Nonempty
⊢ ∃ i ∈ s, Eq (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) ((p i : (a : E) → ℝ) x : ℝ)

Tactic:
exists_apply_eq_finset_sup p hs x

Premises used: Seminorm.exists_apply_eq_finset_sup
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
hs : s.Nonempty
⊢ ∃ i ∈ s, Eq (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) ((p i : (a : E) → ℝ) x : ℝ)

Tactic:
exact exists_apply_eq_finset_sup p hs x

Premises used: Seminorm.exists_apply_eq_finset_sup
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
C : ℝ≥0
h : ∀ (x : E), Eq (α := ℝ) ((s.sup (C • p) : (a : E) → ℝ) x : ℝ) ((C • s.sup p : (a : E) → ℝ) x : ℝ)
⊢ s.sup (C • p) = C • s.sup p

Tactic:
ext x
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
C : ℝ≥0
x : E
h :
  (↑(s.sup fun (i : ι) ↦ NNReal.mk (((C • p) i : (a : E) → ℝ) x) ⋯) : ℝ) =
    C • (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
⊢ Eq (α := ℝ) ((s.sup (C • p) : (a : E) → ℝ) x : ℝ) ((C • s.sup p : (a : E) → ℝ) x : ℝ)

Tactic:
rw [smul_apply, finset_sup_apply, finset_sup_apply]

Premises used: Seminorm.finset_sup_apply, Seminorm.smul_apply
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
C : ℝ≥0
x : E
h :
  C • (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ) =
    (↑(s.sup fun (i : ι) ↦ NNReal.mk (((C • p) i : (a : E) → ℝ) x) ⋯) : ℝ)
⊢ (↑(s.sup fun (i : ι) ↦ NNReal.mk (((C • p) i : (a : E) → ℝ) x) ⋯) : ℝ) =
    C • (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)

Tactic:
symm
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
C : ℝ≥0
x : E
⊢ C • (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ) =
    (↑(s.sup fun (i : ι) ↦ NNReal.mk (((C • p) i : (a : E) → ℝ) x) ⋯) : ℝ)

Tactic:
congr_arg ((↑) : ℝ≥0 → ℝ) (NNReal.mul_finset_sup C s (fun i ↦ ⟨p i x, apply_nonneg _ _⟩))

Premises used: NNReal.mk, NNReal.mul_finset_sup, Subtype.mk, congr_arg, NonnegHomClass.apply_nonneg, DFunLike.coe, NNReal.toReal
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
C : ℝ≥0
x : E
⊢ C • (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ) =
    (↑(s.sup fun (i : ι) ↦ NNReal.mk (((C • p) i : (a : E) → ℝ) x) ⋯) : ℝ)

Tactic:
exact congr_arg ((↑) : ℝ≥0 → ℝ) (NNReal.mul_finset_sup C s (fun i ↦ ⟨p i x, apply_nonneg _ _⟩))

Premises used: NNReal.mul_finset_sup, Subtype.mk, congr_arg, NonnegHomClass.apply_nonneg, DFunLike.coe, NNReal.toReal
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
⊢ s.sup p ≤ ∑ i ∈ s, p i

Tactic:
Finset.sup_le_iff.mpr ?_

Premises used: Iff.mpr, Finset.sup_le_iff
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
refine : ∀ b ∈ s, p b ≤ ∑ i ∈ s, p i
⊢ s.sup p ≤ ∑ i ∈ s, p i

Tactic:
refine Finset.sup_le_iff.mpr ?_

Premises used: Iff.mpr, Finset.sup_le_iff
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
i : ι
hi : i ∈ s
rw : LE.le.{u_7} (α := Seminorm 𝕜 E) 0 (∑ x ∈ s \ {i}, p x)
⊢ p i ≤ ∑ i ∈ s, p i

Tactic:
rw [Finset.sum_eq_sum_diff_singleton_add hi, le_add_iff_nonneg_left]

Premises used: Finset.sum_eq_sum_diff_singleton_add, le_add_iff_nonneg_left
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
i : ι
hi : i ∈ s
⊢ LE.le.{u_7} (α := Seminorm 𝕜 E) 0 (∑ x ∈ s \ {i}, p x)

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
i : ι
hi : i ∈ s
⊢ LE.le.{u_7} (α := Seminorm 𝕜 E) 0 (∑ x ∈ s \ {i}, p x)

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
refine refine₁ : ∀ (i : ι) (hi : i ∈ s), p i ≤ ∑ i ∈ s, p i
refine₂ : ∀ (i : ι) (hi : i ∈ s), LE.le.{u_7} (α := Seminorm 𝕜 E) 0 (∑ x ∈ s \ {i}, p x)
⊢ s.sup p ≤ ∑ i ∈ s, p i

Tactic:
classical
  refine Finset.sup_le_iff.mpr ?_
  intro i hi
  rw [Finset.sum_eq_sum_diff_singleton_add hi, le_add_iff_nonneg_left]
  exact bot_le

Premises used: Iff.mpr, Finset.sup_le_iff, bot_le, le_add_iff_nonneg_left
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ
ha : 0 ≤ a
h : ∀ i ∈ s, (p i : (a : E) → ℝ) x ≤ a
⊢ 0 ≤ a

Tactic:
ha
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ
ha : 0 ≤ a
h : ∀ i ∈ s, (p i : (a : E) → ℝ) x ≤ a
lift : ∀ (a : ℝ≥0) (h : ∀ i ∈ s, (p i : (a : E) → ℝ) x ≤ (↑a : ℝ)), (s.sup p : (a : E) → ℝ) x ≤ (↑a : ℝ)
⊢ (s.sup p : (a : E) → ℝ) x ≤ a

Tactic:
lift a to ℝ≥0 using ha
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ≥0
h : ∀ i ∈ s, (p i : (a : E) → ℝ) x ≤ (↑a : ℝ)
rw : (s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) ≤ a
⊢ (s.sup p : (a : E) → ℝ) x ≤ (↑a : ℝ)

Tactic:
rw [finset_sup_apply, NNReal.coe_le_coe]

Premises used: Seminorm.finset_sup_apply, NNReal.coe_le_coe
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ≥0
h : ∀ i ∈ s, (p i : (a : E) → ℝ) x ≤ (↑a : ℝ)
⊢ (s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) ≤ a

Tactic:
Finset.sup_le h

Premises used: Finset.sup_le
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ≥0
h : ∀ i ∈ s, (p i : (a : E) → ℝ) x ≤ (↑a : ℝ)
⊢ (s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) ≤ a

Tactic:
exact Finset.sup_le h
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
i : ι
hi : i ∈ s
⊢ LE.le (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ)

Tactic:
(Finset.le_sup hi : p i ≤ s.sup p) x

Premises used: Finset.le_sup
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ
ha : 0 < a
h : ∀ i ∈ s, (p i : (a : E) → ℝ) x < a
⊢ 0 ≤ a

Tactic:
ha.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ
ha : 0 < a
h : ∀ i ∈ s, (p i : (a : E) → ℝ) x < a
lift :
  ∀ (a : ℝ≥0) (ha : 0 < (↑a : ℝ)) (h : ∀ i ∈ s, (p i : (a : E) → ℝ) x < (↑a : ℝ)), (s.sup p : (a : E) → ℝ) x < (↑a : ℝ)
⊢ (s.sup p : (a : E) → ℝ) x < a

Tactic:
lift a to ℝ≥0 using ha.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ≥0
ha : 0 < (↑a : ℝ)
h : ∀ i ∈ s, (p i : (a : E) → ℝ) x < (↑a : ℝ)
rw : ∀ b ∈ s, NNReal.mk ((p b : (a : E) → ℝ) x) ⋯ < a
rw₁ : ⊥ < a
⊢ (s.sup p : (a : E) → ℝ) x < (↑a : ℝ)

Tactic:
rw [finset_sup_apply, NNReal.coe_lt_coe, Finset.sup_lt_iff]

Premises used: Seminorm.finset_sup_apply, Finset.sup_lt_iff, NNReal.coe_lt_coe
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ≥0
ha : 0 < (↑a : ℝ)
h : ∀ i ∈ s, (p i : (a : E) → ℝ) x < (↑a : ℝ)
⊢ ∀ b ∈ s, NNReal.mk ((p b : (a : E) → ℝ) x) ⋯ < a

Tactic:
h

Premises used: NNReal.toReal
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ≥0
ha : 0 < (↑a : ℝ)
h : ∀ i ∈ s, (p i : (a : E) → ℝ) x < (↑a : ℝ)
⊢ ∀ b ∈ s, NNReal.mk ((p b : (a : E) → ℝ) x) ⋯ < a

Tactic:
exact h
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ≥0
ha : 0 < (↑a : ℝ)
h : ∀ i ∈ s, (p i : (a : E) → ℝ) x < (↑a : ℝ)
⊢ ⊥ < a

Tactic:
NNReal.coe_pos.mpr ha

Premises used: Iff.mpr, NNReal.coe_pos, NNReal.toReal
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ≥0
ha : 0 < (↑a : ℝ)
h : ∀ i ∈ s, (p i : (a : E) → ℝ) x < (↑a : ℝ)
⊢ ⊥ < a

Tactic:
exact NNReal.coe_pos.mpr ha

Premises used: Iff.mpr, NNReal.coe_pos
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
x y : E
⊢ ‖HSub.hSub (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((p : (a : E) → ℝ) y : ℝ)‖ ≤ (p : (a : E) → ℝ) (x - y)

Tactic:
abs_sub_map_le_sub p x y

Premises used: abs_sub_map_le_sub
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst : SeminormedRing 𝕜
inst_1 : SeminormedCommRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup E₂
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜₂ E₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
c : 𝕜₂
x : E
rw : Eq (α := ℝ) ((p : (a : E₂) → ℝ) ((c • f : (a : E) → E₂) x : E₂) : ℝ) ((‖c‖₊ • p.comp f : (a : E) → ℝ) x : ℝ)
rw₁ : (p : (a : E₂) → ℝ) ((c • f : (a : E) → E₂) x : E₂) = HSMul.hSMul (β := ℝ) ‖c‖₊ ((p.comp f : (a : E) → ℝ) x : ℝ)
rw₂ :
  (p : (a : E₂) → ℝ) (HSMul.hSMul (β := E₂) c ((f : (a : E) → E₂) x : E₂)) =
    HSMul.hSMul (β := ℝ) ‖c‖₊ ((p.comp f : (a : E) → ℝ) x : ℝ)
rw₃ :
  HMul.hMul (β := ℝ) ‖c‖ ((p : (a : E₂) → ℝ) ((f : (a : E) → E₂) x : E₂) : ℝ) =
    HSMul.hSMul (β := ℝ) ‖c‖₊ ((p.comp f : (a : E) → ℝ) x : ℝ)
rw₄ :
  HMul.hMul (β := ℝ) ‖c‖ ((p : (a : E₂) → ℝ) ((f : (a : E) → E₂) x : E₂) : ℝ) =
    HSMul.hSMul (β := ℝ) (↑‖c‖₊ : ℝ) ((p.comp f : (a : E) → ℝ) x : ℝ)
rw₅ :
  HMul.hMul (β := ℝ) ‖c‖ ((p : (a : E₂) → ℝ) ((f : (a : E) → E₂) x : E₂) : ℝ) =
    HSMul.hSMul (β := ℝ) ‖c‖ ((p.comp f : (a : E) → ℝ) x : ℝ)
rw₆ :
  HMul.hMul (β := ℝ) ‖c‖ ((p : (a : E₂) → ℝ) ((f : (a : E) → E₂) x : E₂) : ℝ) =
    HMul.hMul (β := ℝ) ‖c‖ ((p.comp f : (a : E) → ℝ) x : ℝ)
rw₇ rw₈ :
  HMul.hMul (β := ℝ) ‖c‖ ((p : (a : E₂) → ℝ) ((f : (a : E) → E₂) x : E₂) : ℝ) =
    HMul.hMul (β := ℝ) ‖c‖ ((p : (a : E₂) → ℝ) ((f : (a : E) → E₂) x : E₂) : ℝ)
⊢ Eq (α := ℝ) ((p.comp (c • f) : (a : E) → ℝ) x : ℝ) ((‖c‖₊ • p.comp f : (a : E) → ℝ) x : ℝ)

Tactic:
rw [comp_apply, smul_apply, LinearMap.smul_apply, map_smul_eq_mul, NNReal.smul_def, coe_nnnorm,
      smul_eq_mul, comp_apply]

Premises used: LinearMap.smul_apply, Seminorm.comp_apply, NNReal.smul_def, SeminormClass.map_smul_eq_mul, coe_nnnorm, Seminorm.smul_apply, smul_eq_mul
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst : SeminormedRing 𝕜
inst_1 : SeminormedCommRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup E₂
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜₂ E₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
c : 𝕜₂
x : E
⊢ (p.comp (c • f) : (a : E) → ℝ) x = HMul.hMul (β := ℝ) ‖c‖ ((p : (a : E₂) → ℝ) ((f : (a : E) → E₂) x : E₂) : ℝ)

Tactic:
map_smul_eq_mul p _ _

Premises used: SeminormClass.map_smul_eq_mul
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p q : Seminorm 𝕜 E
x_1 x : E
⊢ 0 ≤ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((q : (a : E) → ℝ) (x_1 - x) : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.Seminorm
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p_1 q_1 : Seminorm 𝕜 E
x_1 : E
p q : Seminorm 𝕜 E
a : 𝕜
x : E
inl :
  ⨅ (u : E),
      HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ)
        ((q : (a : E) → ℝ) (HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) 0 x - u) : ℝ) =
    norm.{u_3} (E := 𝕜) 0 *
      ⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)
inr :
  ∀ (ha : a ≠ 0),
    ⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (a • x - u) : ℝ) =
      ‖a‖ * ⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)
⊢ ⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (a • x - u) : ℝ) =
    ‖a‖ * ⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)

Tactic:
obtain rfl | ha := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p_1 q_1 : Seminorm 𝕜 E
x_1 : E
p q : Seminorm 𝕜 E
x : E
inl : Eq (α := ℝ) (⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (0 - u) : ℝ)) 0
⊢ ⨅ (u : E),
      HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ)
        ((q : (a : E) → ℝ) (HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) 0 x - u) : ℝ) =
    norm.{u_3} (E := 𝕜) 0 *
      ⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)

Tactic:
rw [norm_zero, zero_mul, zero_smul]

Premises used: MulZeroClass.zero_mul, norm_zero, zero_smul
-- Module: Mathlib.Analysis.Seminorm
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p_1 q_1 : Seminorm 𝕜 E
x_1 : E
p q : Seminorm 𝕜 E
x i : E
⊢ 0 ≤ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) i : ℝ) ((q : (a : E) → ℝ) (0 - i) : ℝ)

Tactic:
positivity