case h
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
R : Type u_1
inst✝³ : Zero R
inst✝² : SMulWithZero R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : NoZeroSMulDivisors R ℝ≥0∞
c : R
hc : c ≠ 0
s : α
⊢ (c • extend m) s = extend (fun s h => c • m s h) s
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
R : Type u_1
inst✝³ : Zero R
inst✝² : SMulWithZero R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : NoZeroSMulDivisors R ℝ≥0∞
c : R
hc : c ≠ 0
⊢ c • extend m = extend fun s h => c • m s h
ext1 s
case h
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
R : Type u_1
inst✝³ : Zero R
inst✝² : SMulWithZero R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : NoZeroSMulDivisors R ℝ≥0∞
c : R
hc : c ≠ 0
s : α
⊢ (c • ⨅ (h : P s), m s h) = ⨅ (h : P s), c • m s h
case h
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
R : Type u_1
inst✝³ : Zero R
inst✝² : SMulWithZero R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : NoZeroSMulDivisors R ℝ≥0∞
c : R
hc : c ≠ 0
s : α
⊢ (c • extend m) s = extend (fun s h => c • m s h) s
dsimp [extend]
case pos
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
R : Type u_1
inst✝³ : Zero R
inst✝² : SMulWithZero R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : NoZeroSMulDivisors R ℝ≥0∞
c : R
hc : c ≠ 0
s : α
h : P s
⊢ (c • ⨅ (h : P s), m s h) = ⨅ (h : P s), c • m s h

case neg
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
R : Type u_1
inst✝³ : Zero R
inst✝² : SMulWithZero R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : NoZeroSMulDivisors R ℝ≥0∞
c : R
hc : c ≠ 0
s : α
h : ¬P s
⊢ (c • ⨅ (h : P s), m s h) = ⨅ (h : P s), c • m s h
case h
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
R : Type u_1
inst✝³ : Zero R
inst✝² : SMulWithZero R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : NoZeroSMulDivisors R ℝ≥0∞
c : R
hc : c ≠ 0
s : α
⊢ (c • ⨅ (h : P s), m s h) = ⨅ (h : P s), c • m s h
by_cases h : P s
no goals
case pos
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
R : Type u_1
inst✝³ : Zero R
inst✝² : SMulWithZero R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : NoZeroSMulDivisors R ℝ≥0∞
c : R
hc : c ≠ 0
s : α
h : P s
⊢ (c • ⨅ (h : P s), m s h) = ⨅ (h : P s), c • m s h
simp [h]
no goals
case neg
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
R : Type u_1
inst✝³ : Zero R
inst✝² : SMulWithZero R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : NoZeroSMulDivisors R ℝ≥0∞
c : R
hc : c ≠ 0
s : α
h : ¬P s
⊢ (c • ⨅ (h : P s), m s h) = ⨅ (h : P s), c • m s h
simp [h, ENNReal.smul_top, hc]