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
p_1 q_1 : Seminorm 𝕜 E
x_1 : E
p q : Seminorm 𝕜 E
x_2 : E
x : ℝ
hx : 0 < x
rwa : HAdd.hAdd (α := ℝ) (β := ℝ) (0 : ℝ) ((q : (a : E) → ℝ) (HSub.hSub (α := E) 0 0) : ℝ) < x
rwa₁ : HAdd.hAdd (α := ℝ) (β := ℝ) (0 : ℝ) ((q : (a : E) → ℝ) 0 : ℝ) < x
rwa₂ : HAdd.hAdd (α := ℝ) 0 0 < x
rwa₃ rwa₄ rwa₅ rwa₆ : 0 < x
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) 0 : ℝ) ((q : (a : E) → ℝ) (HSub.hSub (α := E) 0 0) : ℝ) < x

Tactic:
rwa [map_zero, sub_zero, map_zero, add_zero]

Premises used: sub_zero, map_zero, add_zero
-- 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
⊢ Eq (α := ℝ) (⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (0 - u) : ℝ)) 0

Tactic:
refine
            ciInf_eq_of_forall_ge_of_forall_gt_exists_lt
              (fun i => by positivity)
              fun x hx => ⟨0, by rwa [map_zero, sub_zero, map_zero, add_zero]⟩

Premises used: ciInf_eq_of_forall_ge_of_forall_gt_exists_lt, Exists.intro, OfNat.ofNat
-- 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
ha : a ≠ 0
inr :
  Eq (α := ℝ) (⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (a • x - u) : ℝ))
    (⨅ (i : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • i) : ℝ) ((q : (a : E) → ℝ) (a • x - a • i) : ℝ))
⊢ ⨅ (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:
simp_rw [Real.mul_iInf_of_nonneg (norm_nonneg a), mul_add, ← map_smul_eq_mul p, ←
          map_smul_eq_mul q, smul_sub]

Premises used: Real.mul_iInf_of_nonneg, smul_sub, SeminormClass.map_smul_eq_mul, mul_add, norm_nonneg
-- 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
ha : a ≠ 0
⊢ Eq (α := ℝ) (⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (a • x - u) : ℝ))
    (⨅ (i : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • i) : ℝ) ((q : (a : E) → ℝ) (a • x - a • i) : ℝ))

Tactic:
Function.Surjective.iInf_congr ((a⁻¹ • ·) : E → E)
            (fun u => ⟨a • u, inv_smul_smul₀ ha u⟩) fun u => ?_

Premises used: inv_smul_smul₀, Inv.inv, Exists.intro, Function.Surjective.iInf_congr, HSMul.hSMul
-- 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
ha : a ≠ 0
inr :
  ∀ (u : E),
    HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (HSMul.hSMul (β := E) a ((fun (x : E) ↦ a⁻¹ • x) u)) : ℝ)
        ((q : (a : E) → ℝ) (a • x - HSMul.hSMul (β := E) a ((fun (x : E) ↦ a⁻¹ • x) u)) : ℝ) =
      HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (a • x - u) : ℝ)
⊢ Eq (α := ℝ) (⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (a • x - u) : ℝ))
    (⨅ (i : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • i) : ℝ) ((q : (a : E) → ℝ) (a • x - a • i) : ℝ))

Tactic:
refine
          Function.Surjective.iInf_congr ((a⁻¹ • ·) : E → E)
            (fun u => ⟨a • u, inv_smul_smul₀ ha u⟩) fun u => ?_

Premises used: inv_smul_smul₀, Inv.inv, Exists.intro, Function.Surjective.iInf_congr, HSMul.hSMul
-- 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
ha : a ≠ 0
u : E
inr inr₁ :
  HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (a • x - u) : ℝ) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (a • x - u) : ℝ)
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (HSMul.hSMul (β := E) a ((fun (x : E) ↦ a⁻¹ • x) u)) : ℝ)
      ((q : (a : E) → ℝ) (a • x - HSMul.hSMul (β := E) a ((fun (x : E) ↦ a⁻¹ • x) u)) : ℝ) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (a • x - u) : ℝ)

Tactic:
rw [smul_inv_smul₀ ha]

Premises used: smul_inv_smul₀
-- 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 : E
⊢ Eq (α := ℝ) ((p ⊓ q : (a : E) → ℝ) x : ℝ)
    (⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ) : ℝ)

Tactic:
rfl

Premises used: iInf, 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
simp : LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((p : (a : E) → ℝ) x : ℝ)
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((q : (a : E) → ℝ) (x - x) : ℝ) ≤
    (fun (f : Seminorm 𝕜 E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ)) p x

Tactic:
simp only [sub_self, map_zero, add_zero]

Premises used: sub_self, map_zero, add_zero
-- 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
⊢ LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((p : (a : E) → ℝ) x : ℝ)

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 : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p_1 q_1 : Seminorm 𝕜 E
x_1 : E
p q : Seminorm 𝕜 E
x : E
simp : LE.le (α := ℝ) ((q : (a : E) → ℝ) x : ℝ) ((q : (a : E) → ℝ) x : ℝ)
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) 0 : ℝ) ((q : (a : E) → ℝ) (x - 0) : ℝ) ≤
    (fun (f : Seminorm 𝕜 E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ)) q x

Tactic:
simp only [map_zero, zero_add, sub_zero]

Premises used: sub_zero, map_zero, zero_add
-- 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
⊢ LE.le (α := ℝ) ((q : (a : E) → ℝ) x : ℝ) ((q : (a : E) → ℝ) x : ℝ)

Tactic:
rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
R : Type u_1
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SMul R ℝ
inst_4 : SMul R ℝ≥0
inst_5 : IsScalarTower R ℝ≥0 ℝ
r : R
p q : Seminorm 𝕜 E
h : ∀ (x : E), Eq (α := ℝ) ((r • (p ⊓ q) : (a : E) → ℝ) x : ℝ) ((r • p ⊓ r • q : (a : E) → ℝ) x : ℝ)
⊢ r • (p ⊓ q) = r • p ⊓ r • q

Tactic:
ext
-- Module: Mathlib.Analysis.Seminorm
Goal:
R : Type u_1
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SMul R ℝ
inst_4 : SMul R ℝ≥0
inst_5 : IsScalarTower R ℝ≥0 ℝ
r : R
p q : Seminorm 𝕜 E
x : E
h : HSMul.hSMul (β := ℝ) r ((p ⊓ q : (a : E) → ℝ) x : ℝ) = (r • p ⊓ r • q : (a : E) → ℝ) x
h₁ :
  HSMul.hSMul (β := ℝ) r
      (⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)) =
    ⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((r • p : (a : E) → ℝ) u : ℝ) ((r • q : (a : E) → ℝ) (x - u) : ℝ)
h₂ :
  HSMul.hSMul (β := ℝ) r
      (⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)) =
    ⨅ (u : E), HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) u : ℝ) + HSMul.hSMul (β := ℝ) r ((q : (a : E) → ℝ) (x - u) : ℝ)
h₃ :
  HSMul.hSMul (β := ℝ) (HSMul.hSMul (β := ℝ≥0) r 1)
      (⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)) =
    ⨅ (u : E),
      HSMul.hSMul (β := ℝ) (HSMul.hSMul (β := ℝ≥0) r 1) ((p : (a : E) → ℝ) u : ℝ) +
        HSMul.hSMul (β := ℝ) (HSMul.hSMul (β := ℝ≥0) r 1) ((q : (a : E) → ℝ) (x - u) : ℝ)
h₄ :
  HSMul.hSMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ)
      (⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)) =
    ⨅ (u : E),
      HSMul.hSMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) u : ℝ) +
        HSMul.hSMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)
h₅ :
  (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) *
      ⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ) =
    ⨅ (u : E),
      HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) u : ℝ) +
        HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)
h₆ :
  Eq (α := ℝ)
    (⨅ (i : E),
      (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) *
        HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) i : ℝ) ((q : (a : E) → ℝ) (x - i) : ℝ))
    (⨅ (u : E),
      HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) u : ℝ) +
        HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ))
⊢ Eq (α := ℝ) ((r • (p ⊓ q) : (a : E) → ℝ) x : ℝ) ((r • p ⊓ r • q : (a : E) → ℝ) x : ℝ)

Tactic:
simp_rw [smul_apply, inf_apply, smul_apply, ← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def,
    smul_eq_mul, Real.mul_iInf_of_nonneg (NNReal.coe_nonneg _), mul_add]

Premises used: NNReal, Real.mul_iInf_of_nonneg, NNReal.smul_def, Seminorm.inf_apply, smul_one_smul, NNReal.coe_nonneg, Seminorm.smul_apply, mul_add, 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 : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p q : Seminorm 𝕜 E
x : E
s : Set (Seminorm 𝕜 E)
h : BddAbove (α := E → ℝ) (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)
rw : Eq (α := ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) 0) (⨆ (x : (↑s : Type u_7)), 0)
⊢ Eq (α := ℝ) ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) 0) 0

Tactic:
rw [iSup_apply, ← @Real.iSup_const_zero s]

Premises used: Real.iSup_const_zero, iSup_apply
-- 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 q : Seminorm 𝕜 E
x : E
s : Set (Seminorm 𝕜 E)
h : BddAbove (α := E → ℝ) (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)
h₁ : ∀ (x : (↑s : Type u_7)), Eq (α := ℝ) (((↑x : Seminorm 𝕜 E) : (a : E) → ℝ) 0 : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) 0) (⨆ (x : (↑s : Type u_7)), 0)

Tactic:
congr!
-- 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 q : Seminorm 𝕜 E
x : E
s : Set (Seminorm 𝕜 E)
h : BddAbove (α := E → ℝ) (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)
i : (↑s : Type u_7)
⊢ Eq (α := ℝ) (((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) 0 : ℝ) (0 : ℝ)

Tactic:
map_zero i.1

Premises used: map_zero, Subtype.val
-- 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 q : Seminorm 𝕜 E
x : E
s : Set (Seminorm 𝕜 E)
h : BddAbove (α := E → ℝ) (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)
i : (↑s : Type u_7)
⊢ Eq (α := ℝ) (((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) 0 : ℝ) (0 : ℝ)

Tactic:
exact map_zero i.1

Premises used: map_zero, Subtype.val
-- 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 q : Seminorm 𝕜 E
x_1 : E
s : Set (Seminorm 𝕜 E)
h : BddAbove (α := E → ℝ) (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)
x y : E
rcases :
  ∀ (q : E → ℝ) (hq : Membership.mem (γ := Set (E → ℝ)) (upperBounds (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)) q),
    (⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) (x + y) ≤
      HAdd.hAdd (α := ℝ) ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) x)
        ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) y)
⊢ (⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) (x + y) ≤
    HAdd.hAdd (α := ℝ) ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) x)
      ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) y)

Tactic:
rcases h with ⟨q, hq⟩
-- 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 q_1 : Seminorm 𝕜 E
x_1 : E
s : Set (Seminorm 𝕜 E)
x y : E
q : E → ℝ
hq : Membership.mem (γ := Set (E → ℝ)) (upperBounds (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)) q
inl :
  ∀
    (hq :
      Membership.mem (γ := Set (E → ℝ))
        (upperBounds (image (α := Seminorm 𝕜 E) (DFunLike.coe (β := fun (x : E) ↦ ℝ)) ∅)) q),
    (⨆ (p : (↑∅ : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) (x + y) ≤
      HAdd.hAdd (α := ℝ) ((⨆ (p : (↑∅ : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) x)
        ((⨆ (p : (↑∅ : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) y)
inr :
  ∀ (h : s.Nonempty),
    (⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) (x + y) ≤
      HAdd.hAdd (α := ℝ) ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) x)
        ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) y)
⊢ (⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) (x + y) ≤
    HAdd.hAdd (α := ℝ) ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) x)
      ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) y)

Tactic:
obtain rfl | h := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, 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 q_1 : Seminorm 𝕜 E
x_1 x y : E
q : E → ℝ
hq :
  Membership.mem (γ := Set (E → ℝ)) (upperBounds (image (α := Seminorm 𝕜 E) (DFunLike.coe (β := fun (x : E) ↦ ℝ)) ∅)) q
⊢ (⨆ (p : (↑∅ : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) (x + y) ≤
    HAdd.hAdd (α := ℝ) ((⨆ (p : (↑∅ : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) x)
      ((⨆ (p : (↑∅ : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) y)

Tactic:
simp [Real.iSup_of_isEmpty]

Premises used: Real.iSup_of_isEmpty
-- 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 q_1 : Seminorm 𝕜 E
x_1 : E
s : Set (Seminorm 𝕜 E)
x y : E
q : E → ℝ
hq : Membership.mem (γ := Set (E → ℝ)) (upperBounds (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)) q
h : s.Nonempty
⊢ Nonempty.{u_7 + 1} (↑s : Type u_7)

Tactic:
haveI : Nonempty ↑s := h.coe_sort
-- 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 q_1 : Seminorm 𝕜 E
x_1 : E
s : Set (Seminorm 𝕜 E)
x y : E
q : E → ℝ
hq : Membership.mem (γ := Set (E → ℝ)) (upperBounds (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)) q
h : s.Nonempty
this : Nonempty.{u_7 + 1} (↑s : Type u_7)
inr :
  ⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (x + y) ≤
    HAdd.hAdd (α := ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x)
      (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) y)
⊢ (⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) (x + y) ≤
    HAdd.hAdd (α := ℝ) ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) x)
      ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) y)

Tactic:
simp only [iSup_apply]

Premises used: iSup_apply
-- 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 q_1 : Seminorm 𝕜 E
x_1 : E
s : Set (Seminorm 𝕜 E)
x y : E
q : E → ℝ
hq : Membership.mem (γ := Set (E → ℝ)) (upperBounds (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)) q
h : s.Nonempty
this : Nonempty.{u_7 + 1} (↑s : Type u_7)
⊢ ⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (x + y) ≤
    HAdd.hAdd (α := ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x)
      (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) y)

Tactic:
ciSup_le fun i =>
            ((i : Seminorm 𝕜 E).add_le' x y).trans <| add_le_add
              -- Porting note: `f` is provided to force `Subtype.val` to appear.
              -- A type ascription on `_` would have also worked, but would have been more verbose.
              (le_ciSup (f := fun i => (Subtype.val i : Seminorm 𝕜 E).toFun x) ⟨q x, ?_⟩ i)
              (le_ciSup (f := fun i => (Subtype.val i : Seminorm 𝕜 E).toFun y) ⟨q y, ?_⟩ i)

Premises used: add_le_add, Seminorm.toAddGroupSeminorm, AddGroupSeminorm.add_le', le_ciSup, Exists.intro, LE.le.trans, Subtype.val, ciSup_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
p q_1 : Seminorm 𝕜 E
x_1 : E
s : Set (Seminorm 𝕜 E)
x y : E
q : E → ℝ
hq : Membership.mem (γ := Set (E → ℝ)) (upperBounds (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)) q
h : s.Nonempty
this : Nonempty.{u_7 + 1} (↑s : Type u_7)
inr :
  ∀ (i : (↑s : Type u_7)),
    Membership.mem (γ := Set ℝ)
      (upperBounds (range fun (i : { x : Seminorm 𝕜 E // x ∈ s }) ↦ (↑i : Seminorm 𝕜 E).toFun x)) (q x)
inr₁ :
  ∀ (i : (↑s : Type u_7)),
    Membership.mem (γ := Set ℝ)
      (upperBounds (range fun (i : { x : Seminorm 𝕜 E // x ∈ s }) ↦ (↑i : Seminorm 𝕜 E).toFun y)) (q y)
⊢ ⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (x + y) ≤
    HAdd.hAdd (α := ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x)
      (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) y)

Tactic:
refine ciSup_le fun i =>
            ((i : Seminorm 𝕜 E).add_le' x y).trans <| add_le_add
              -- Porting note: `f` is provided to force `Subtype.val` to appear.
              -- A type ascription on `_` would have also worked, but would have been more verbose.
              (le_ciSup (f := fun i => (Subtype.val i : Seminorm 𝕜 E).toFun x) ⟨q x, ?_⟩ i)
              (le_ciSup (f := fun i => (Subtype.val i : Seminorm 𝕜 E).toFun y) ⟨q y, ?_⟩ i)

Premises used: add_le_add, Seminorm.toAddGroupSeminorm, AddGroupSeminorm.add_le', LE.le.trans, ciSup_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
p q_1 : Seminorm 𝕜 E
x_1 : E
s : Set (Seminorm 𝕜 E)
x y : E
q : E → ℝ
hq : Membership.mem (γ := Set (E → ℝ)) (upperBounds (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)) q
h : s.Nonempty
this : Nonempty.{u_7 + 1} (↑s : Type u_7)
i : (↑s : Type u_7)
inr : ∀ (i : { x : Seminorm 𝕜 E // x ∈ s }), (↑i : Seminorm 𝕜 E).toFun x ≤ q x
⊢ Membership.mem (γ := Set ℝ)
    (upperBounds (range fun (i : { x : Seminorm 𝕜 E // x ∈ s }) ↦ (↑i : Seminorm 𝕜 E).toFun x)) (q x)

Tactic:
rw [mem_upperBounds, forall_mem_range]

Premises used: Set.forall_mem_range, mem_upperBounds
-- 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 q_1 : Seminorm 𝕜 E
x_1 : E
s : Set (Seminorm 𝕜 E)
x y : E
q : E → ℝ
hq : Membership.mem (γ := Set (E → ℝ)) (upperBounds (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)) q
h : s.Nonempty
this : Nonempty.{u_7 + 1} (↑s : Type u_7)
i : (↑s : Type u_7)
inr : ∀ (i : { x : Seminorm 𝕜 E // x ∈ s }), (↑i : Seminorm 𝕜 E).toFun y ≤ q y
⊢ Membership.mem (γ := Set ℝ)
    (upperBounds (range fun (i : { x : Seminorm 𝕜 E // x ∈ s }) ↦ (↑i : Seminorm 𝕜 E).toFun y)) (q y)

Tactic:
rw [mem_upperBounds, forall_mem_range]

Premises used: Set.forall_mem_range, mem_upperBounds
-- 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 q_1 : Seminorm 𝕜 E
x_1 : E
s : Set (Seminorm 𝕜 E)
x y : E
q : E → ℝ
hq : Membership.mem (γ := Set (E → ℝ)) (upperBounds (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)) q
h : s.Nonempty
this : Nonempty.{u_7 + 1} (↑s : Type u_7)
i : (↑s : Type u_7)
⊢ ∀ (i : { x : Seminorm 𝕜 E // x ∈ s }), (↑i : Seminorm 𝕜 E).toFun x ≤ q x

Tactic:
fun j => hq (mem_image_of_mem _ j.2) _

Premises used: Set.mem_image_of_mem, DFunLike.coe, Subtype.property
-- 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 q_1 : Seminorm 𝕜 E
x_1 : E
s : Set (Seminorm 𝕜 E)
x y : E
q : E → ℝ
hq : Membership.mem (γ := Set (E → ℝ)) (upperBounds (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)) q
h : s.Nonempty
this : Nonempty.{u_7 + 1} (↑s : Type u_7)
i : (↑s : Type u_7)
⊢ ∀ (i : { x : Seminorm 𝕜 E // x ∈ s }), (↑i : Seminorm 𝕜 E).toFun x ≤ q x

Tactic:
exact fun j => hq (mem_image_of_mem _ j.2) _

Premises used: Set.mem_image_of_mem, DFunLike.coe