awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
x : E
rw :
  (∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : 𝕜) (_ : x ∈ i • s), ‖i‖ₑ < b) ↔
    ∀ (i : ℝ≥0∞),
      0 < i →
        ∃ (x_1 : 𝕜),
          Membership.mem (γ := Set 𝕜) {y : 𝕜 | Membership.mem (γ := SetRel 𝕜 𝕜) {p : 𝕜 × 𝕜 | edist p.1 p.2 < i} (y, 0)}
              x_1 ∧
            x ∈ x_1 • s
⊢ (∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : 𝕜) (_ : x ∈ i • s), ‖i‖ₑ < b) ↔ ∃ᶠ (c : 𝕜) in 𝓝 0, x ∈ c • s

Tactic:
rw [(nhds_basis_uniformity uniformity_basis_edist).frequently_iff]

Premises used: uniformity_basis_edist, Filter.HasBasis.frequently_iff, nhds_basis_uniformity
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
x : E
⊢ (∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : 𝕜) (_ : x ∈ i • s), ‖i‖ₑ < b) ↔
    ∀ (i : ℝ≥0∞),
      0 < i →
        ∃ (x_1 : 𝕜),
          Membership.mem (γ := Set 𝕜) {y : 𝕜 | Membership.mem (γ := SetRel 𝕜 𝕜) {p : 𝕜 × 𝕜 | edist p.1 p.2 < i} (y, 0)}
              x_1 ∧
            x ∈ x_1 • s

Tactic:
simp [and_comm]

Premises used: and_comm
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
x : E
inst_3 : NeBot (α := 𝕜) (𝓝[≠] 0)
rw : ∃ᶠ (c : 𝕜) in 𝓝 0, x ∈ HSMul.hSMul (β := Set E) c univ
⊢ egauge 𝕜 univ x = 0

Tactic:
rw [egauge_eq_zero_iff]

Premises used: egauge_eq_zero_iff
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
x : E
inst_3 : NeBot (α := 𝕜) (𝓝[≠] 0)
⊢ ∃ᶠ (c : 𝕜) in 𝓝 0, x ∈ HSMul.hSMul (β := Set E) c univ

Tactic:
(frequently_iff_neBot.2 ‹_›).mono fun c hc ↦ ?_

Premises used: Iff.mpr, Filter.Frequently.mono, Filter.frequently_iff_neBot
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
x : E
inst_3 : NeBot (α := 𝕜) (𝓝[≠] 0)
refine : ∀ (c : 𝕜) (hc : c ∉ {0}), x ∈ HSMul.hSMul (β := Set E) c univ
⊢ ∃ᶠ (c : 𝕜) in 𝓝 0, x ∈ HSMul.hSMul (β := Set E) c univ

Tactic:
refine (frequently_iff_neBot.2 ‹_›).mono fun c hc ↦ ?_

Premises used: Iff.mpr, Filter.Frequently.mono, Filter.frequently_iff_neBot
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
x : E
inst_3 : NeBot (α := 𝕜) (𝓝[≠] 0)
c : 𝕜
hc : c ∉ {0}
⊢ x ∈ HSMul.hSMul (β := Set E) c univ

Tactic:
simp_all [smul_set_univ₀]

Premises used: Set.smul_set_univ₀
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
hs : s.Nonempty
⊢ 0 ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s

Tactic:
simp [zero_smul_set hs]

Premises used: Set.zero_smul_set
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
hs : s.Nonempty
⊢ 0 ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s

Tactic:
have : 0 ∈ (0 : 𝕜) • s := by simp [zero_smul_set hs]
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
hs : s.Nonempty
this : 0 ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s
⊢ egauge 𝕜 s 0 = 0

Tactic:
simpa using egauge_le_of_mem_smul this

Premises used: egauge_le_of_mem_smul
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
⊢ egauge.{u_1, u_2} 𝕜 (E := E) 0 0 = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
x : E
h : x ∈ s
⊢ x ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 s

Tactic:
rw [← one_smul 𝕜 s] at h

Premises used: one_smul
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
x : E
h : x ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 s
⊢ egauge 𝕜 s x ≤ 1

Tactic:
simpa using egauge_le_of_mem_smul h

Premises used: egauge_le_of_mem_smul
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
x : E
inst_3 : NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → x ∈ c • s → r ≤ ‖c‖ₑ
rw : ∀ (c : 𝕜), x ∈ c • s → r ≤ ‖c‖ₑ
⊢ r ≤ egauge 𝕜 s x

Tactic:
rw [le_egauge_iff]

Premises used: le_egauge_iff
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
x : E
inst_3 : NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → x ∈ c • s → r ≤ ‖c‖ₑ
c : 𝕜
hc : x ∈ c • s
inl : ∀ (hc₀ : c ≠ 0), r ≤ ‖c‖ₑ
inr : ∀ (hc : x ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s), r ≤ enorm.{u_1} (E := 𝕜) 0
⊢ r ≤ ‖c‖ₑ

Tactic:
rcases ne_or_eq c 0 with hc₀ | rfl

Premises used: ne_or_eq, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
x : E
inst_3 : NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → x ∈ c • s → r ≤ ‖c‖ₑ
c : 𝕜
hc : x ∈ c • s
hc₀ : c ≠ 0
⊢ r ≤ ‖c‖ₑ

Tactic:
h c hc₀ hc
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
x : E
inst_3 : NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → x ∈ c • s → r ≤ ‖c‖ₑ
c : 𝕜
hc : x ∈ c • s
hc₀ : c ≠ 0
⊢ r ≤ ‖c‖ₑ

Tactic:
exact h c hc₀ hc
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
x : E
inst_3 : NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → x ∈ c • s → r ≤ ‖c‖ₑ
hc : x ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s
⊢ x = 0

Tactic:
grw [zero_smul_set_subset, Set.mem_zero] at hc

Premises used: Set.mem_zero, Set.zero_smul_set_subset
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
x : E
inst_3 : NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → x ∈ c • s → r ≤ ‖c‖ₑ
hc : x = 0
⊢ x = 0

Tactic:
hc
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
x : E
inst_3 : NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → x ∈ c • s → r ≤ ‖c‖ₑ
hc : x = 0
⊢ x = 0

Tactic:
exact hc
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
x : E
inst_3 : NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → x ∈ c • s → r ≤ ‖c‖ₑ
hc : x ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s
⊢ ∀ (c : 𝕜), c ≠ 0 → 0 ∈ c • s → r ≤ ‖c‖ₑ

Tactic:
obtain rfl : x = 0 := by
    grw [zero_smul_set_subset, Set.mem_zero] at hc
    exact hc

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
x : E
inst_3 : NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → x ∈ c • s → r ≤ ‖c‖ₑ
hc : x ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s
h₁ : ∀ (c : 𝕜), c ≠ 0 → 0 ∈ c • s → r ≤ ‖c‖ₑ
⊢ 0 ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s

Tactic:
obtain rfl : x = 0 := by
    grw [zero_smul_set_subset, Set.mem_zero] at hc
    exact hc

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → 0 ∈ c • s → r ≤ ‖c‖ₑ
hc : 0 ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s
inr : ∀ (c : ℝ≥0∞), enorm.{u_1} (E := 𝕜) 0 < c → r < c
⊢ r ≤ enorm.{u_1} (E := 𝕜) 0

Tactic:
apply le_of_forall_gt

Premises used: le_of_forall_gt
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → 0 ∈ c • s → r ≤ ‖c‖ₑ
hc : 0 ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s
b : ℝ≥0∞
hb : enorm.{u_1} (E := 𝕜) 0 < b
⊢ 0 < b

Tactic:
simpa using hb
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → 0 ∈ c • s → r ≤ ‖c‖ₑ
hc : 0 ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s
b : ℝ≥0∞
hb : enorm.{u_1} (E := 𝕜) 0 < b
inr : ∀ (c : 𝕜) (hc₀ : Membership.mem (γ := Set 𝕜) {0}ᶜ c) (hcb : Membership.mem (γ := Set 𝕜) (eball 0 b) c), r < b
⊢ r < b

Tactic:
rcases Filter.nonempty_of_mem <|
    inter_mem_nhdsWithin {(0 : 𝕜)}ᶜ (Metric.eball_mem_nhds 0 (by simpa using hb))
    with ⟨c, hc₀, hcb⟩

Premises used: inter_mem_nhdsWithin, Compl.compl, Filter.nonempty_of_mem, Metric.eball_mem_nhds, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → 0 ∈ c • s → r ≤ ‖c‖ₑ
hc : 0 ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s
b : ℝ≥0∞
hb : enorm.{u_1} (E := 𝕜) 0 < b
c : 𝕜
hc₀ : Membership.mem (γ := Set 𝕜) {0}ᶜ c
hcb : Membership.mem (γ := Set 𝕜) (eball 0 b) c
⊢ c ≠ 0

Tactic:
simpa using hc₀
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → 0 ∈ c • s → r ≤ ‖c‖ₑ
hc : 0 ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s
b : ℝ≥0∞
hb : enorm.{u_1} (E := 𝕜) 0 < b
c : 𝕜
hc₀ : Membership.mem (γ := Set 𝕜) {0}ᶜ c
hcb : Membership.mem (γ := Set 𝕜) (eball 0 b) c
⊢ Eq.{u_2 + 1} (α := E) ((fun (x : E) ↦ c • x) 0) 0

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → 0 ∈ c • s → r ≤ ‖c‖ₑ
hc : 0 ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s
b : ℝ≥0∞
hb : enorm.{u_1} (E := 𝕜) 0 < b
c : 𝕜
hc₀ : Membership.mem (γ := Set 𝕜) {0}ᶜ c
hcb : Membership.mem (γ := Set 𝕜) (eball 0 b) c
⊢ ‖c‖ₑ < b

Tactic:
simpa using hcb
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → 0 ∈ c • s → r ≤ ‖c‖ₑ
hc : 0 ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s
b : ℝ≥0∞
hb : enorm.{u_1} (E := 𝕜) 0 < b
c : 𝕜
hc₀ : Membership.mem (γ := Set 𝕜) {0}ᶜ c
hcb : Membership.mem (γ := Set 𝕜) (eball 0 b) c
⊢ r < b

Tactic:
exact (h c (by simpa using hc₀) ⟨_, hs₀, by simp⟩).trans_lt (by simpa using hcb)

Premises used: And.intro, Exists.intro, LE.le.trans_lt
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
x : E
simp_rw : ∀ (c_1 : 𝕜), x ∈ (c_1 * c) • s → egauge 𝕜 s x / ‖c‖ₑ ≤ ‖c_1‖ₑ
⊢ egauge 𝕜 s x / ‖c‖ₑ ≤ egauge 𝕜 (c • s) x

Tactic:
simp_rw [le_egauge_iff, smul_smul]

Premises used: smul_smul, le_egauge_iff
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
a : 𝕜
x : E
hx : x ∈ s
h : egauge 𝕜 s ((fun (x : E) ↦ (a * c) • x) x) ≤ ‖a‖ₑ * ‖c‖ₑ
⊢ egauge 𝕜 s ((fun (x : E) ↦ (a * c) • x) x) / ‖c‖ₑ ≤ ‖a‖ₑ

Tactic:
apply ENNReal.div_le_of_le_mul

Premises used: ENNReal.div_le_of_le_mul
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
a : 𝕜
x : E
hx : x ∈ s
h : egauge 𝕜 s ((fun (x : E) ↦ (a * c) • x) x) ≤ ‖a * c‖ₑ
⊢ egauge 𝕜 s ((fun (x : E) ↦ (a * c) • x) x) ≤ ‖a‖ₑ * ‖c‖ₑ

Tactic:
rw [← enorm_mul]

Premises used: enorm_mul
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
a : 𝕜
x : E
hx : x ∈ s
⊢ egauge 𝕜 s ((fun (x : E) ↦ (a * c) • x) x) ≤ ‖a * c‖ₑ

Tactic:
egauge_le_of_mem_smul <| smul_mem_smul_set hx

Premises used: egauge_le_of_mem_smul, Set.smul_mem_smul_set
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
a : 𝕜
x : E
hx : x ∈ s
⊢ egauge 𝕜 s ((fun (x : E) ↦ (a * c) • x) x) ≤ ‖a * c‖ₑ

Tactic:
exact egauge_le_of_mem_smul <| smul_mem_smul_set hx

Premises used: egauge_le_of_mem_smul, Set.smul_mem_smul_set
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ egauge 𝕜 (c • s) x = egauge 𝕜 s x / ‖c‖ₑ

Tactic:
le_antisymm ?_ (le_egauge_smul_left _ _ _)

Premises used: le_egauge_smul_left, le_antisymm
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
refine : egauge 𝕜 (c • s) x ≤ egauge 𝕜 s x / ‖c‖ₑ
⊢ egauge 𝕜 (c • s) x = egauge 𝕜 s x / ‖c‖ₑ

Tactic:
refine le_antisymm ?_ (le_egauge_smul_left _ _ _)

Premises used: le_egauge_smul_left, le_antisymm
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ ‖c‖ₑ ≠ 0 ∨ egauge 𝕜 s x ≠ 0

Tactic:
simp [*]
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ ‖c‖ₑ ≠ ∞ ∨ egauge 𝕜 s x ≠ ∞

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
rw : egauge 𝕜 (c • s) x * ‖c‖ₑ ≤ egauge 𝕜 s x
⊢ egauge 𝕜 (c • s) x ≤ egauge 𝕜 s x / ‖c‖ₑ

Tactic:
rw [ENNReal.le_div_iff_mul_le (by simp [*]) (by simp)]

Premises used: ENNReal.le_div_iff_mul_le
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ c ≠ 0

Tactic:
simpa
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
rw : egauge 𝕜 (c • s) x * ‖c‖ₑ = egauge 𝕜 (c • s) x / ‖c‖ₑ⁻¹
rw₁ : egauge 𝕜 (c • s) x * ‖c‖ₑ = egauge 𝕜 (c • s) x * ‖c‖ₑ⁻¹⁻¹
rw₂ rw₃ : egauge 𝕜 (c • s) x * ‖c‖ₑ = egauge 𝕜 (c • s) x * ‖c‖ₑ
⊢ egauge 𝕜 (c • s) x * ‖c‖ₑ = egauge 𝕜 (c • s) x / ‖c⁻¹‖ₑ

Tactic:
rw [enorm_inv (by simpa), div_eq_mul_inv, inv_inv]

Premises used: div_eq_mul_inv, inv_inv, enorm_inv
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ egauge 𝕜 (c • s) x / ‖c⁻¹‖ₑ ≤ egauge 𝕜 (c⁻¹ • c • s) x

Tactic:
le_egauge_smul_left _ _ _

Premises used: le_egauge_smul_left
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
rw rw₁ : egauge 𝕜 s x = egauge 𝕜 s x
⊢ egauge 𝕜 (c⁻¹ • c • s) x = egauge 𝕜 s x

Tactic:
rw [inv_smul_smul₀ hc]

Premises used: inv_smul_smul₀
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
egauge : _root_.egauge 𝕜 (c • s) x * ‖c‖ₑ = _root_.egauge 𝕜 (c • s) x / ‖c⁻¹‖ₑ
egauge₁ : _root_.egauge 𝕜 (c⁻¹ • c • s) x = _root_.egauge 𝕜 s x
⊢ _root_.egauge 𝕜 (c • s) x * ‖c‖ₑ ≤ _root_.egauge 𝕜 s x

Tactic:
calc
    egauge 𝕜 (c • s) x * ‖c‖ₑ = egauge 𝕜 (c • s) x / ‖c⁻¹‖ₑ := by
      rw [enorm_inv (by simpa), div_eq_mul_inv, inv_inv]
    _ ≤ egauge 𝕜 (c⁻¹ • c • s) x := le_egauge_smul_left _ _ _
    _ = egauge 𝕜 s x := by rw [inv_smul_smul₀ hc]

Premises used: le_egauge_smul_left, Inv.inv, HSMul.hSMul, egauge
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
x : E
rw : ∀ (c_1 : 𝕜), c • x ∈ c_1 • s → ‖c‖ₑ * egauge 𝕜 s x ≤ ‖c_1‖ₑ
⊢ ‖c‖ₑ * egauge 𝕜 s x ≤ egauge 𝕜 s (c • x)

Tactic:
rw [le_egauge_iff]

Premises used: le_egauge_iff
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
x : E
a : 𝕜
y : E
hy : y ∈ s
hxy : (fun (x : E) ↦ a • x) y = c • x
inl :
  ∀ (hxy : (fun (x : E) ↦ a • x) y = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x),
    enorm.{u_1} (E := 𝕜) 0 * egauge 𝕜 s x ≤ ‖a‖ₑ
inr : ∀ (hc : c ≠ 0), ‖c‖ₑ * egauge 𝕜 s x ≤ ‖a‖ₑ
⊢ ‖c‖ₑ * egauge 𝕜 s x ≤ ‖a‖ₑ

Tactic:
rcases eq_or_ne c 0 with rfl | hc

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
x : E
a : 𝕜
y : E
hy : y ∈ s
hxy : (fun (x : E) ↦ a • x) y = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x
⊢ enorm.{u_1} (E := 𝕜) 0 * egauge 𝕜 s x ≤ ‖a‖ₑ

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
x : E
a : 𝕜
y : E
hy : y ∈ s
hxy : (fun (x : E) ↦ a • x) y = c • x
hc : c ≠ 0
⊢ ‖c‖ₑ * egauge 𝕜 s x ≤ ‖a‖ₑ

Tactic:
ENNReal.mul_le_of_le_div' <| le_trans ?_ ENNReal.coe_div_le

Premises used: ENNReal.mul_le_of_le_div', ENNReal.coe_div_le, le_trans
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
x : E
a : 𝕜
y : E
hy : y ∈ s
hxy : (fun (x : E) ↦ a • x) y = c • x
hc : c ≠ 0
inr : egauge 𝕜 s x ≤ (↑(‖a‖₊ / ‖c‖₊) : ℝ≥0∞)
⊢ ‖c‖ₑ * egauge 𝕜 s x ≤ ‖a‖ₑ

Tactic:
refine ENNReal.mul_le_of_le_div' <| le_trans ?_ ENNReal.coe_div_le

Premises used: ENNReal.mul_le_of_le_div', ENNReal.coe_div_le, le_trans
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
x : E
a : 𝕜
y : E
hy : y ∈ s
hxy : (fun (x : E) ↦ a • x) y = c • x
hc : c ≠ 0
inr : egauge 𝕜 s x ≤ (↑‖c⁻¹ * a‖₊ : ℝ≥0∞)
⊢ egauge 𝕜 s x ≤ (↑(‖a‖₊ / ‖c‖₊) : ℝ≥0∞)

Tactic:
rw [div_eq_inv_mul, ← nnnorm_inv, ← nnnorm_mul]

Premises used: nnnorm_inv, nnnorm_mul, div_eq_inv_mul
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
x : E
a : 𝕜
y : E
hy : y ∈ s
hxy : (fun (x : E) ↦ a • x) y = c • x
hc : c ≠ 0
⊢ egauge 𝕜 s x ≤ (↑‖c⁻¹ * a‖₊ : ℝ≥0∞)

Tactic:
egauge_le_of_mem_smul ⟨y, hy, ?_⟩

Premises used: egauge_le_of_mem_smul, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
x : E
a : 𝕜
y : E
hy : y ∈ s
hxy : (fun (x : E) ↦ a • x) y = c • x
hc : c ≠ 0
inr : (fun (x : E) ↦ (c⁻¹ * a) • x) y = x
⊢ egauge 𝕜 s x ≤ (↑‖c⁻¹ * a‖₊ : ℝ≥0∞)

Tactic:
refine egauge_le_of_mem_smul ⟨y, hy, ?_⟩

Premises used: egauge_le_of_mem_smul, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
x : E
a : 𝕜
y : E
hy : y ∈ s
hxy : (fun (x : E) ↦ a • x) y = c • x
hc : c ≠ 0
⊢ (fun (x : E) ↦ (c⁻¹ * a) • x) y = x

Tactic:
simp only [mul_smul, hxy, inv_smul_smul₀ hc]

Premises used: inv_smul_smul₀, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
h : c = 0 → s.Nonempty
x : E
⊢ egauge 𝕜 s (c • x) = ‖c‖ₑ * egauge 𝕜 s x

Tactic:
le_antisymm ?_ (le_egauge_smul_right c s x)

Premises used: le_egauge_smul_right, le_antisymm
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
h : c = 0 → s.Nonempty
x : E
refine : egauge 𝕜 s (c • x) ≤ ‖c‖ₑ * egauge 𝕜 s x
⊢ egauge 𝕜 s (c • x) = ‖c‖ₑ * egauge 𝕜 s x

Tactic:
refine le_antisymm ?_ (le_egauge_smul_right c s x)

Premises used: le_egauge_smul_right, le_antisymm
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
h : c = 0 → s.Nonempty
x : E
inl :
  ∀ (h : Eq.{u_1 + 1} (α := 𝕜) 0 0 → s.Nonempty),
    egauge 𝕜 s (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x) ≤ enorm.{u_1} (E := 𝕜) 0 * egauge 𝕜 s x
inr : ∀ (hc : c ≠ 0), egauge 𝕜 s (c • x) ≤ ‖c‖ₑ * egauge 𝕜 s x
⊢ egauge 𝕜 s (c • x) ≤ ‖c‖ₑ * egauge 𝕜 s x

Tactic:
rcases eq_or_ne c 0 with rfl | hc

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
x : E
h : Eq.{u_1 + 1} (α := 𝕜) 0 0 → s.Nonempty
⊢ egauge 𝕜 s (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x) ≤ enorm.{u_1} (E := 𝕜) 0 * egauge 𝕜 s x

Tactic:
simp [egauge_zero_right _ (h rfl)]

Premises used: egauge_zero_right, rfl
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
h : c = 0 → s.Nonempty
x : E
hc : c ≠ 0
⊢ ‖c‖ₑ ≠ 0

Tactic:
simpa
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
h : c = 0 → s.Nonempty
x : E
hc : c ≠ 0
⊢ c ≠ 0

Tactic:
simpa
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
h : c = 0 → s.Nonempty
x : E
hc : c ≠ 0
inr : ‖c⁻¹‖ₑ * egauge 𝕜 s (c • x) ≤ egauge 𝕜 s x
⊢ egauge 𝕜 s (c • x) ≤ ‖c‖ₑ * egauge 𝕜 s x

Tactic:
rw [mul_comm, ← ENNReal.div_le_iff_le_mul (.inl <| by simpa) (.inl enorm_ne_top),
      ENNReal.div_eq_inv_mul, ← enorm_inv (by simpa)]

Premises used: ENNReal.div_le_iff_le_mul, mul_comm, Or.inl, enorm_inv, enorm_ne_top, ENNReal.div_eq_inv_mul
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
h : c = 0 → s.Nonempty
x : E
hc : c ≠ 0
⊢ ‖c⁻¹‖ₑ * egauge 𝕜 s (c • x) ≤ egauge 𝕜 s x

Tactic:
(le_egauge_smul_right _ _ _).trans_eq ?_

Premises used: LE.le.trans_eq, le_egauge_smul_right
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
h : c = 0 → s.Nonempty
x : E
hc : c ≠ 0
inr : egauge 𝕜 s (c⁻¹ • c • x) = egauge 𝕜 s x
⊢ ‖c⁻¹‖ₑ * egauge 𝕜 s (c • x) ≤ egauge 𝕜 s x

Tactic:
refine (le_egauge_smul_right _ _ _).trans_eq ?_

Premises used: LE.le.trans_eq, le_egauge_smul_right
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
h : c = 0 → s.Nonempty
x : E
hc : c ≠ 0
inr inr₁ : egauge 𝕜 s x = egauge 𝕜 s x
⊢ egauge 𝕜 s (c⁻¹ • c • x) = egauge 𝕜 s x

Tactic:
rw [inv_smul_smul₀ hc]

Premises used: inv_smul_smul₀