awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
f : E → ℝ
map_zero : f 0 = 0
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
r : 𝕜
x : E
h : ¬r = 0
smul_le : f (r⁻¹ • r • x) ≤ ‖r‖⁻¹ * f (r • x)
h₁ : x = r⁻¹ • r • x
⊢ f x ≤ ‖r‖⁻¹ * f (r • x)

Tactic:
convert! smul_le
-- 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
f : E → ℝ
map_zero : f 0 = 0
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
r : 𝕜
x : E
h : ¬r = 0
smul_le : f (r⁻¹ • r • x) ≤ ‖r‖⁻¹ * f (r • x)
⊢ x = r⁻¹ • r • x

Tactic:
simp [h]
-- 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 : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
f g : Seminorm 𝕜 E
h :
  Eq.{max (u_7 + 1) 1} (α := (a : E) → ℝ) ((fun (f : Seminorm 𝕜 E) ↦ f.toFun) f) ((fun (f : Seminorm 𝕜 E) ↦ f.toFun) g)
rcases :
  ∀ (toFun : E → ℝ) (map_zero' : toFun 0 = 0) (add_le' : ∀ (r s : E), toFun (r + s) ≤ toFun r + toFun s)
    (neg' : ∀ (r : E), toFun (-r) = toFun r)
    (smul' :
      ∀ (a : 𝕜) (x : E),
        { toFun := toFun, map_zero' := map_zero', add_le' := add_le', neg' := neg' : AddGroupSeminorm E }.toFun
            (a • x) =
          ‖a‖ *
            { toFun := toFun, map_zero' := map_zero', add_le' := add_le', neg' := neg' : AddGroupSeminorm E }.toFun x)
    (h :
      Eq.{max (u_7 + 1) 1} (α := (a : E) → ℝ)
        ((fun (f : Seminorm 𝕜 E) ↦ f.toFun)
          { toFun := toFun, map_zero' := map_zero', add_le' := add_le', neg' := neg', smul' := smul' })
        ((fun (f : Seminorm 𝕜 E) ↦ f.toFun) g)),
    { toFun := toFun, map_zero' := map_zero', add_le' := add_le', neg' := neg', smul' := smul' : Seminorm 𝕜 E } = g
⊢ f = g

Tactic:
rcases f with ⟨⟨_⟩⟩
-- 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 : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
g : Seminorm 𝕜 E
toFun : E → ℝ
map_zero' : toFun 0 = 0
add_le' : ∀ (r s : E), toFun (r + s) ≤ toFun r + toFun s
neg' : ∀ (r : E), toFun (-r) = toFun r
smul' :
  ∀ (a : 𝕜) (x : E),
    { toFun := toFun, map_zero' := map_zero', add_le' := add_le', neg' := neg' : AddGroupSeminorm E }.toFun (a • x) =
      ‖a‖ * { toFun := toFun, map_zero' := map_zero', add_le' := add_le', neg' := neg' : AddGroupSeminorm E }.toFun x
h :
  Eq.{max (u_7 + 1) 1} (α := (a : E) → ℝ)
    ((fun (f : Seminorm 𝕜 E) ↦ f.toFun)
      { toFun := toFun, map_zero' := map_zero', add_le' := add_le', neg' := neg', smul' := smul' })
    ((fun (f : Seminorm 𝕜 E) ↦ f.toFun) g)
rcases :
  ∀ (toFun_1 : E → ℝ) (map_zero'_1 : toFun_1 0 = 0) (add_le'_1 : ∀ (r s : E), toFun_1 (r + s) ≤ toFun_1 r + toFun_1 s)
    (neg'_1 : ∀ (r : E), toFun_1 (-r) = toFun_1 r)
    (smul'_1 :
      ∀ (a : 𝕜) (x : E),
        { toFun := toFun_1, map_zero' := map_zero'_1, add_le' := add_le'_1, neg' := neg'_1 : AddGroupSeminorm E }.toFun
            (a • x) =
          ‖a‖ *
            { toFun := toFun_1, map_zero' := map_zero'_1, add_le' := add_le'_1, neg' := neg'_1 :
                  AddGroupSeminorm E }.toFun
              x)
    (h :
      Eq.{max (u_7 + 1) 1} (α := (a : E) → ℝ)
        ((fun (f : Seminorm 𝕜 E) ↦ f.toFun)
          { toFun := toFun, map_zero' := map_zero', add_le' := add_le', neg' := neg', smul' := smul' })
        ((fun (f : Seminorm 𝕜 E) ↦ f.toFun)
          { toFun := toFun_1, map_zero' := map_zero'_1, add_le' := add_le'_1, neg' := neg'_1, smul' := smul'_1 })),
    { toFun := toFun, map_zero' := map_zero', add_le' := add_le', neg' := neg', smul' := smul' : Seminorm 𝕜 E } =
      { toFun := toFun_1, map_zero' := map_zero'_1, add_le' := add_le'_1, neg' := neg'_1, smul' := smul'_1 }
⊢ { toFun := toFun, map_zero' := map_zero', add_le' := add_le', neg' := neg', smul' := smul' : Seminorm 𝕜 E } = g

Tactic:
rcases g with ⟨⟨_⟩⟩
-- 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 : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
toFun : E → ℝ
map_zero' : toFun 0 = 0
add_le' : ∀ (r s : E), toFun (r + s) ≤ toFun r + toFun s
neg' : ∀ (r : E), toFun (-r) = toFun r
smul' :
  ∀ (a : 𝕜) (x : E),
    { toFun := toFun, map_zero' := map_zero', add_le' := add_le', neg' := neg' : AddGroupSeminorm E }.toFun (a • x) =
      ‖a‖ * { toFun := toFun, map_zero' := map_zero', add_le' := add_le', neg' := neg' : AddGroupSeminorm E }.toFun x
toFun_1 : E → ℝ
map_zero'_1 : toFun_1 0 = 0
add_le'_1 : ∀ (r s : E), toFun_1 (r + s) ≤ toFun_1 r + toFun_1 s
neg'_1 : ∀ (r : E), toFun_1 (-r) = toFun_1 r
smul'_1 :
  ∀ (a : 𝕜) (x : E),
    { toFun := toFun_1, map_zero' := map_zero'_1, add_le' := add_le'_1, neg' := neg'_1 : AddGroupSeminorm E }.toFun
        (a • x) =
      ‖a‖ *
        { toFun := toFun_1, map_zero' := map_zero'_1, add_le' := add_le'_1, neg' := neg'_1 : AddGroupSeminorm E }.toFun
          x
h :
  Eq.{max (u_7 + 1) 1} (α := (a : E) → ℝ)
    ((fun (f : Seminorm 𝕜 E) ↦ f.toFun)
      { toFun := toFun, map_zero' := map_zero', add_le' := add_le', neg' := neg', smul' := smul' })
    ((fun (f : Seminorm 𝕜 E) ↦ f.toFun)
      { toFun := toFun_1, map_zero' := map_zero'_1, add_le' := add_le'_1, neg' := neg'_1, smul' := smul'_1 })
⊢ { toFun := toFun, map_zero' := map_zero', add_le' := add_le', neg' := neg', smul' := smul' : Seminorm 𝕜 E } =
    { toFun := toFun_1, map_zero' := map_zero'_1, add_le' := add_le'_1, neg' := neg'_1, smul' := smul'_1 }

Tactic:
congr
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
p q : Seminorm 𝕜 E
h : ∀ (x : E), Eq (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((q : (a : E) → ℝ) x : ℝ)
⊢ p = q

Tactic:
DFunLike.ext p q h

Premises used: DFunLike.ext
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
⊢ Eq.{u_7 + 1} (α := (a : E) → ℝ) (⇑0 : (a : E) → ℝ) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
x : E
⊢ Eq (α := ℝ) ((0 : (a : E) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
rfl

Premises used: 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 : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
p_1 : Seminorm 𝕜 E
x : E
r_1 : ℝ
inst_3 : SMul R ℝ
inst_4 : SMul R ℝ≥0
inst_5 : IsScalarTower R ℝ≥0 ℝ
r : R
p : Seminorm 𝕜 E
x_1 : 𝕜
x_2 : E
simp :
  HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) (x_1 • x_2) : ℝ) =
    ‖x_1‖ * HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) x_2 : ℝ)
⊢ HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) (x_1 • x_2) : ℝ) =
    ‖x_1‖ * HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) x_2 : ℝ)

Tactic:
simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul]

Premises used: NNReal, NNReal.smul_def, smul_one_smul, smul_eq_mul
-- 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 : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
p_1 : Seminorm 𝕜 E
x : E
r_1 : ℝ
inst_3 : SMul R ℝ
inst_4 : SMul R ℝ≥0
inst_5 : IsScalarTower R ℝ≥0 ℝ
r : R
p : Seminorm 𝕜 E
x_1 : 𝕜
x_2 : E
rw :
  (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) * HMul.hMul (β := ℝ) ‖x_1‖ ((p : (a : E) → ℝ) x_2 : ℝ) =
    ‖x_1‖ * HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) x_2 : ℝ)
rw₁ rw₂ :
  ‖x_1‖ * HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) x_2 : ℝ) =
    ‖x_1‖ * HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) x_2 : ℝ)
⊢ HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) (x_1 • x_2) : ℝ) =
    ‖x_1‖ * HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) x_2 : ℝ)

Tactic:
rw [map_smul_eq_mul, mul_left_comm]

Premises used: mul_left_comm, SeminormClass.map_smul_eq_mul
-- Module: Mathlib.Analysis.Seminorm
Goal:
R : Type u_1
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
inst_3 : SMul R ℝ
inst_4 : SMul R ℝ≥0
inst_5 : IsScalarTower R ℝ≥0 ℝ
r : R
p : Seminorm 𝕜 E
⊢ (⇑(r • p) : (a : E) → ℝ) = HSMul.hSMul (β := (a : E) → ℝ) r (⇑p : (a : E) → ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
R : Type u_1
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
inst_3 : SMul R ℝ
inst_4 : SMul R ℝ≥0
inst_5 : IsScalarTower R ℝ≥0 ℝ
r : R
p : Seminorm 𝕜 E
x : E
⊢ (r • p : (a : E) → ℝ) x = HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) x : ℝ)

Tactic:
rfl

Premises used: 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 : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
p_1 : Seminorm 𝕜 E
x_1 : E
r : ℝ
p q : Seminorm 𝕜 E
a : 𝕜
x : E
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • x) : ℝ) ((q : (a : E) → ℝ) (a • x) : ℝ) =
    ‖a‖ * HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((q : (a : E) → ℝ) x : ℝ)

Tactic:
simp only [map_smul_eq_mul, map_smul_eq_mul, mul_add]

Premises used: SeminormClass.map_smul_eq_mul, mul_add
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
p q : Seminorm 𝕜 E
⊢ (⇑(p + q) : (a : E) → ℝ) = HAdd.hAdd (α := (a : E) → ℝ) (⇑p : (a : E) → ℝ) (⇑q : (a : E) → ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
p q : Seminorm 𝕜 E
x : E
⊢ (p + q : (a : E) → ℝ) x = HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((q : (a : E) → ℝ) x : ℝ)

Tactic:
rfl

Premises used: 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 : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
x_1 : Seminorm 𝕜 E
x_2 : ℕ
⊢ (⇑(x_2 • x_1) : (a : E) → ℝ) = HSMul.hSMul (β := (a : E) → ℝ) x_2 (⇑x_1 : (a : E) → ℝ)

Tactic:
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 : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
⊢ IsOrderedCancelAddMonoid.{u_7} (Seminorm 𝕜 E)

Tactic:
Function.Injective.isOrderedCancelAddMonoid DFunLike.coe coe_add .rfl

Premises used: Iff.rfl, Seminorm.coe_add, Function.Injective.isOrderedCancelAddMonoid, DFunLike.coe
-- 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 : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
inst_3 : Monoid R
inst_4 : MulAction R ℝ
inst_5 : SMul R ℝ≥0
inst_6 : IsScalarTower R ℝ≥0 ℝ
c : R
x_1 : Seminorm 𝕜 E
⊢ (⇑(c • x_1) : (a : E) → ℝ) = HSMul.hSMul (β := (a : E) → ℝ) c (⇑x_1 : (a : E) → ℝ)

Tactic:
rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
⊢ Function.Injective (α := Seminorm 𝕜 E) (β := E → ℝ) (⇑(coeFnAddMonoidHom 𝕜 E) : (a : Seminorm 𝕜 E) → E → ℝ)

Tactic:
show @Function.Injective (Seminorm 𝕜 E) (E → ℝ) (↑) from DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- 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 : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
inst_3 : Monoid R
inst_4 : DistribMulAction R ℝ
inst_5 : SMul R ℝ≥0
inst_6 : IsScalarTower R ℝ≥0 ℝ
c : R
x_1 : Seminorm 𝕜 E
⊢ (coeFnAddMonoidHom 𝕜 E : (a : Seminorm 𝕜 E) → E → ℝ) (c • x_1) =
    HSMul.hSMul (β := E → ℝ) c ((coeFnAddMonoidHom 𝕜 E : (a : Seminorm 𝕜 E) → E → ℝ) x_1 : E → ℝ)

Tactic:
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 : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
inst_3 : Semiring R
inst_4 : Module R ℝ
inst_5 : SMul R ℝ≥0
inst_6 : IsScalarTower R ℝ≥0 ℝ
c : R
x_1 : Seminorm 𝕜 E
⊢ (coeFnAddMonoidHom 𝕜 E : (a : Seminorm 𝕜 E) → E → ℝ) (c • x_1) =
    HSMul.hSMul (β := E → ℝ) c ((coeFnAddMonoidHom 𝕜 E : (a : Seminorm 𝕜 E) → E → ℝ) x_1 : E → ℝ)

Tactic:
rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
p q : Seminorm 𝕜 E
⊢ Eq (α := (a : E) → ℝ) (⇑(p ⊔ q) : (a : E) → ℝ) ((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
p q : Seminorm 𝕜 E
x : E
⊢ Eq (α := ℝ) ((p ⊔ q : (a : E) → ℝ) x : ℝ) (max ((p : (a : E) → ℝ) x) ((q : (a : E) → ℝ) x) : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
R : Type u_1
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
inst_3 : SMul R ℝ
inst_4 : SMul R ℝ≥0
inst_5 : IsScalarTower R ℝ≥0 ℝ
r : R
p q : Seminorm 𝕜 E
x y : ℝ
⊢ r • max x y = max (r • x) (r • y)

Tactic:
simpa only [← smul_eq_mul, ← NNReal.smul_def, smul_one_smul ℝ≥0 r (_ : ℝ)] using
      mul_max_of_nonneg x y (r • (1 : ℝ≥0) : ℝ≥0).coe_nonneg

Premises used: NNReal, mul_max_of_nonneg, NNReal.smul_def, smul_one_smul, NNReal.coe_nonneg, HSMul.hSMul, smul_eq_mul, OfNat.ofNat
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
p q : Seminorm 𝕜 E
⊢ LE.le (α := (a : E) → ℝ) (⇑p : (a : E) → ℝ) (⇑q : (a : E) → ℝ) ↔ p ≤ q

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
p q : Seminorm 𝕜 E
⊢ LT.lt (α := (a : E) → ℝ) (⇑p : (a : E) → ℝ) (⇑q : (a : E) → ℝ) ↔ p < q

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
p q : Seminorm 𝕜 E
⊢ p ≤ q ↔ ∀ (x : E), LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((q : (a : E) → ℝ) x : ℝ)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
p q : Seminorm 𝕜 E
⊢ p < q ↔ p ≤ q ∧ ∃ (x : E), LT.lt (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((q : (a : E) → ℝ) x : ℝ)

Tactic:
@Pi.lt_def _ _ _ p q

Premises used: Pi.lt_def
-- 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 : SeminormedRing 𝕜
inst_1 : SeminormedRing 𝕜₂
inst_2 : SeminormedRing 𝕜₃
σ₁₂ : 𝕜 →+* 𝕜₂
inst_3 : RingHomIsometric σ₁₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst_4 : RingHomIsometric σ₂₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_5 : RingHomIsometric σ₁₃
inst_6 : AddCommGroup E
inst_7 : AddCommGroup E₂
inst_8 : AddCommGroup E₃
inst_9 : Module 𝕜 E
inst_10 : Module 𝕜₂ E₂
inst_11 : Module 𝕜₃ E₃
inst_12 : SMul R ℝ
inst_13 : SMul R ℝ≥0
inst_14 : IsScalarTower R ℝ≥0 ℝ
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
x : 𝕜
x_1 : E
⊢ (p : (a : E₂) → ℝ) ((f : (a : E) → E₂) (x • x_1) : E₂) =
    HMul.hMul (β := ℝ) ‖x‖ ((p : (a : E₂) → ℝ) ((f : (a : E) → E₂) x_1 : E₂) : ℝ)

Tactic:
simp only [map_smulₛₗ _, map_smul_eq_mul, RingHomIsometric.norm_map]

Premises used: MulActionSemiHomClass.map_smulₛₗ, RingHomIsometric.norm_map, SeminormClass.map_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 : SeminormedRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
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₂
⊢ Eq (α := (a : E) → ℝ) (⇑(p.comp f) : (a : E) → ℝ) (Function.comp (β := E₂) (⇑p : (a : E₂) → ℝ) (⇑f : (a : E) → E₂))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst : SeminormedRing 𝕜
inst_1 : SeminormedRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
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₂
x : E
⊢ Eq (α := ℝ) ((p.comp f : (a : E) → ℝ) x : ℝ) ((p : (a : E₂) → ℝ) ((f : (a : E) → E₂) x : E₂) : ℝ)

Tactic:
rfl

Premises used: rfl
-- 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
⊢ p.comp LinearMap.id = p

Tactic:
ext fun _ => rfl

Premises used: Seminorm.ext, rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst : SeminormedRing 𝕜
inst_1 : SeminormedRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup E₂
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜₂ E₂
p : Seminorm 𝕜₂ E₂
⊢ Eq.{u_7 + 1} (α := Seminorm 𝕜 E) (p.comp (σ₁₂ := σ₁₂) 0) 0

Tactic:
ext fun _ => map_zero p

Premises used: map_zero, Seminorm.ext
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst : SeminormedRing 𝕜
inst_1 : SeminormedRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup E₂
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
⊢ comp 0 f = 0

Tactic:
ext fun _ => rfl

Premises used: Seminorm.ext, rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
inst : SeminormedRing 𝕜
inst_1 : SeminormedRing 𝕜₂
inst_2 : SeminormedRing 𝕜₃
σ₁₂ : 𝕜 →+* 𝕜₂
inst_3 : RingHomIsometric σ₁₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst_4 : RingHomIsometric σ₂₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_5 : RingHomIsometric σ₁₃
inst_6 : AddCommGroup E
inst_7 : AddCommGroup E₂
inst_8 : AddCommGroup E₃
inst_9 : Module 𝕜 E
inst_10 : Module 𝕜₂ E₂
inst_11 : Module 𝕜₃ E₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p : Seminorm 𝕜₃ E₃
g : E₂ →ₛₗ[σ₂₃] E₃
f : E →ₛₗ[σ₁₂] E₂
⊢ p.comp (g ∘ₛₗ f) = (p.comp g).comp f

Tactic:
ext fun _ => rfl

Premises used: Seminorm.ext, rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst : SeminormedRing 𝕜
inst_1 : SeminormedRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup E₂
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜₂ E₂
p q : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
⊢ (p + q).comp f = p.comp f + q.comp f

Tactic:
ext fun _ => rfl

Premises used: Seminorm.ext, rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst : SeminormedRing 𝕜
inst_1 : SeminormedRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup E₂
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜₂ E₂
p : Seminorm 𝕜₂ E₂
f g : E →ₛₗ[σ₁₂] E₂
⊢ p.comp (f + g) ≤ p.comp f + p.comp g

Tactic:
fun _ => map_add_le_add p _ _

Premises used: SubadditiveHomClass.map_add_le_add, DFunLike.coe
-- Module: Mathlib.Analysis.Seminorm
Goal:
R : Type u_1
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst : SeminormedRing 𝕜
inst_1 : SeminormedRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup E₂
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜₂ E₂
inst_7 : SMul R ℝ
inst_8 : SMul R ℝ≥0
inst_9 : IsScalarTower R ℝ≥0 ℝ
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
c : R
⊢ (c • p).comp f = c • p.comp f

Tactic:
ext fun _ => rfl

Premises used: Seminorm.ext, rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst : SeminormedRing 𝕜
inst_1 : SeminormedRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup E₂
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜₂ E₂
p q : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
hp : p ≤ q
⊢ p.comp f ≤ q.comp f

Tactic:
fun _ => hp _

Premises used: DFunLike.coe
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
⊢ Eq.{u_7 + 1} (α := (a : E) → ℝ) (⇑⊥ : (a : E) → ℝ) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
⊢ Eq.{u_7 + 1} (α := Seminorm 𝕜 E) ⊥ 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p q : Seminorm 𝕜 E
a b : ℝ≥0
hpq : p ≤ q
hab : a ≤ b
x : E
⊢ LE.le (α := ℝ) ((a • p : (a : E) → ℝ) x : ℝ) ((b • q : (a : E) → ℝ) x : ℝ)

Tactic:
mul_le_mul hab (hpq x) (apply_nonneg p x) (NNReal.coe_nonneg b)

Premises used: mul_le_mul, NNReal.coe_nonneg, NonnegHomClass.apply_nonneg
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p q : Seminorm 𝕜 E
a b : ℝ≥0
hpq : p ≤ q
hab : a ≤ b
x : E
⊢ LE.le (α := ℝ) ((a • p : (a : E) → ℝ) x : ℝ) ((b • q : (a : E) → ℝ) x : ℝ)

Tactic:
exact mul_le_mul hab (hpq x) (apply_nonneg p x) (NNReal.coe_nonneg b)

Premises used: mul_le_mul, NNReal.coe_nonneg
-- 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
empty empty₁ empty₂ empty₃ : Eq (α := ℕ) 0 0
⊢ 0 = (↑0 : ℝ)

Tactic:
norm_cast