-- Mathlib/Analysis/Convex/Gauge.lean
theorem gauge_smul_of_nonneg [MulActionWithZero α E] [IsScalarTower α ℝ (Set E)] {s : Set E} {a : α}
    (ha : 0 ≤ a) (x : E) : gauge s (a • x) = a • gauge s x

Proof state:
case inr.e_a.h
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
α : Type u_3
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
⊢ r ∈ {r | r ∈ Ioi 0 ∧ r⁻¹ • a • x ∈ s} ↔ r ∈ a • {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ s}

Tactic:
simp_rw [Set.mem_smul_set, Set.mem_sep_iff]

Result:
case inr.e_a.h
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
α : Type u_3
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
⊢ r ∈ Ioi 0 ∧ r⁻¹ • a • x ∈ s ↔ ∃ y, (y ∈ Ioi 0 ∧ y⁻¹ • x ∈ s) ∧ a • y = r

Proof state:
case inr.e_a
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
α : Type u_3
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
⊢ {r | r ∈ Ioi 0 ∧ r⁻¹ • a • x ∈ s} = a • {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ s}

Tactic:
ext r

Result:
case inr.e_a.h
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
α : Type u_3
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
⊢ r ∈ {r | r ∈ Ioi 0 ∧ r⁻¹ • a • x ∈ s} ↔ r ∈ a • {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ s}

Proof state:
case inr
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
α : Type u_3
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • a • x ∈ s} = sInf (a • {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ s})

Tactic:
congr 1

Result:
case inr.e_a
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
α : Type u_3
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
⊢ {r | r ∈ Ioi 0 ∧ r⁻¹ • a • x ∈ s} = a • {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ s}

Proof state:
case inr.e_a.h.mp.intro
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
α : Type u_3
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hx : a • x ∈ r • s
hr : 0 < r
this : 0 < a⁻¹ • r
⊢ (a⁻¹ • r)⁻¹ • x ∈ s

Tactic:
rwa [← mem_smul_set_iff_inv_smul_mem₀ this.ne', smul_assoc,
  mem_smul_set_iff_inv_smul_mem₀ (inv_ne_zero ha'.ne'), inv_inv]

Result:
no goals

Proof state:
case inr.e_a.h.mpr.intro.intro.intro
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
α : Type u_3
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : 0 < r
hx : x ∈ r • s
⊢ 0 < a • r ∧ (a • r)⁻¹ • a • x ∈ s

Tactic:
have := smul_pos ha' hr

Result:
case inr.e_a.h.mpr.intro.intro.intro
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
α : Type u_3
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : 0 < r
hx : x ∈ r • s
this : 0 < a • r
⊢ 0 < a • r ∧ (a • r)⁻¹ • a • x ∈ s

Proof state:
case inr.e_a.h.mp.intro
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
α : Type u_3
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hx : a • x ∈ r • s
hr : 0 < r
⊢ ∃ y, (0 < y ∧ y⁻¹ • x ∈ s) ∧ a • y = r

Tactic:
have := smul_pos (inv_pos.2 ha') hr

Result:
case inr.e_a.h.mp.intro
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
α : Type u_3
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hx : a • x ∈ r • s
hr : 0 < r
this : 0 < a⁻¹ • r
⊢ ∃ y, (0 < y ∧ y⁻¹ • x ∈ s) ∧ a • y = r

Proof state:
case inr.e_a.h.mp
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
α : Type u_3
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
⊢ r ∈ Ioi 0 ∧ r⁻¹ • a • x ∈ s → ∃ y, (y ∈ Ioi 0 ∧ y⁻¹ • x ∈ s) ∧ a • y = r

Tactic:
rintro ⟨hr, hx⟩

Result:
case inr.e_a.h.mp.intro
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
α : Type u_3
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : r ∈ Ioi 0
hx : r⁻¹ • a • x ∈ s
⊢ ∃ y, (y ∈ Ioi 0 ∧ y⁻¹ • x ∈ s) ∧ a • y = r

Proof state:
case inr.e_a.h.mpr.intro.intro.intro
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
α : Type u_3
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : 0 < r
hx : x ∈ r • s
this : 0 < a • r
⊢ 0 < a • r ∧ (a • r)⁻¹ • a • x ∈ s

Tactic:
refine ⟨this, ?_⟩

Result:
case inr.e_a.h.mpr.intro.intro.intro
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
α : Type u_3
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : 0 < r
hx : x ∈ r • s
this : 0 < a • r
⊢ (a • r)⁻¹ • a • x ∈ s

Proof state:
case inl
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
α : Type u_3
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
x : E
ha : 0 ≤ 0
⊢ gauge s (0 • x) = 0 • gauge s x

Tactic:
rw [zero_smul, gauge_zero, zero_smul]

Result:
no goals

Proof state:
case inr.e_a.h.mpr.intro.intro.intro
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
α : Type u_3
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : 0 < r
hx : x ∈ r • s
this : 0 < a • r
⊢ (a • r)⁻¹ • a • x ∈ s

Tactic:
rw [← mem_smul_set_iff_inv_smul_mem₀ this.ne', smul_assoc]

Result:
case inr.e_a.h.mpr.intro.intro.intro
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
α : Type u_3
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : 0 < r
hx : x ∈ r • s
this : 0 < a • r
⊢ a • x ∈ a • r • s

Proof state:
case inr.e_a.h.mpr.intro.intro.intro
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
α : Type u_3
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : 0 < r
hx : x ∈ r • s
this : 0 < a • r
⊢ a • x ∈ a • r • s

Tactic:
exact smul_mem_smul_set hx

Result:
no goals