case inl
X : Type ?u.12625
α : Type u_2
α' : Type ?u.12631
β : Type u_1
γ : Type ?u.12637
δ : Type ?u.12640
M : Type ?u.12643
E : Type ?u.12646
R : Type ?u.12649
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace α'
inst✝³ : One β
inst✝² : One γ
inst✝¹ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
inst✝ : TopologicalSpace β
h : HasCompactMulSupport f
hf : Continuous f
h2 : range f = f '' mulTSupport f
⊢ IsCompact (f '' mulTSupport f)

case inr
X : Type ?u.12625
α : Type u_2
α' : Type ?u.12631
β : Type u_1
γ : Type ?u.12637
δ : Type ?u.12640
M : Type ?u.12643
E : Type ?u.12646
R : Type ?u.12649
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace α'
inst✝³ : One β
inst✝² : One γ
inst✝¹ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
inst✝ : TopologicalSpace β
h : HasCompactMulSupport f
hf : Continuous f
h2 : range f = insert 1 (f '' mulTSupport f)
⊢ IsCompact (insert 1 (f '' mulTSupport f))
X : Type ?u.12625
α : Type u_2
α' : Type ?u.12631
β : Type u_1
γ : Type ?u.12637
δ : Type ?u.12640
M : Type ?u.12643
E : Type ?u.12646
R : Type ?u.12649
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace α'
inst✝³ : One β
inst✝² : One γ
inst✝¹ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
inst✝ : TopologicalSpace β
h : HasCompactMulSupport f
hf : Continuous f
⊢ IsCompact (range f)
cases' range_eq_image_mulTSupport_or f with h2 h2 <;> rw [h2]
no goals
case inl
X : Type ?u.12625
α : Type u_2
α' : Type ?u.12631
β : Type u_1
γ : Type ?u.12637
δ : Type ?u.12640
M : Type ?u.12643
E : Type ?u.12646
R : Type ?u.12649
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace α'
inst✝³ : One β
inst✝² : One γ
inst✝¹ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
inst✝ : TopologicalSpace β
h : HasCompactMulSupport f
hf : Continuous f
h2 : range f = f '' mulTSupport f
⊢ IsCompact (f '' mulTSupport f)

case inr
X : Type ?u.12625
α : Type u_2
α' : Type ?u.12631
β : Type u_1
γ : Type ?u.12637
δ : Type ?u.12640
M : Type ?u.12643
E : Type ?u.12646
R : Type ?u.12649
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace α'
inst✝³ : One β
inst✝² : One γ
inst✝¹ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
inst✝ : TopologicalSpace β
h : HasCompactMulSupport f
hf : Continuous f
h2 : range f = insert 1 (f '' mulTSupport f)
⊢ IsCompact (insert 1 (f '' mulTSupport f))
exacts [h.image hf, (h.image hf).insert 1]