-- Mathlib/Geometry/Manifold/PartitionOfUnity.lean
lemma IsOpen.exists_msmooth_support_eq_aux {s : Set H} (hs : IsOpen s) :
    ∃ f : H → ℝ, f.support = s ∧ ContMDiff I 𝓘(ℝ) ∞ f ∧ Set.range f ⊆ Set.Icc 0 1

Proof state:
case intro.intro.intro
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
H : Type uH
inst✝¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝ : FiniteDimensional ℝ E
s : Set H
hs : IsOpen s
h's : IsOpen (↑I.symm ⁻¹' s)
f : E → ℝ
f_supp : support f = ↑I.symm ⁻¹' s
f_diff : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
⊢ ∃ f, support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) ∞ f ∧ range f ⊆ Icc 0 1

Tactic:
refine ⟨f ∘ I, ?_, ?_, ?_⟩

Result:
case intro.intro.intro.refine_1
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
H : Type uH
inst✝¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝ : FiniteDimensional ℝ E
s : Set H
hs : IsOpen s
h's : IsOpen (↑I.symm ⁻¹' s)
f : E → ℝ
f_supp : support f = ↑I.symm ⁻¹' s
f_diff : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
⊢ support (f ∘ ↑I) = s

case intro.intro.intro.refine_2
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
H : Type uH
inst✝¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝ : FiniteDimensional ℝ E
s : Set H
hs : IsOpen s
h's : IsOpen (↑I.symm ⁻¹' s)
f : E → ℝ
f_supp : support f = ↑I.symm ⁻¹' s
f_diff : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
⊢ ContMDiff I 𝓘(ℝ, ℝ) ∞ (f ∘ ↑I)

case intro.intro.intro.refine_3
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
H : Type uH
inst✝¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝ : FiniteDimensional ℝ E
s : Set H
hs : IsOpen s
h's : IsOpen (↑I.symm ⁻¹' s)
f : E → ℝ
f_supp : support f = ↑I.symm ⁻¹' s
f_diff : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
⊢ range (f ∘ ↑I) ⊆ Icc 0 1

Proof state:
case intro.intro.intro.refine_2
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
H : Type uH
inst✝¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝ : FiniteDimensional ℝ E
s : Set H
hs : IsOpen s
h's : IsOpen (↑I.symm ⁻¹' s)
f : E → ℝ
f_supp : support f = ↑I.symm ⁻¹' s
f_diff : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
⊢ ContMDiff I 𝓘(ℝ, ℝ) ∞ (f ∘ ↑I)

Tactic:
exact f_diff.comp_contMDiff contMDiff_model

Result:
no goals

Proof state:
case intro.intro.intro.refine_1
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
H : Type uH
inst✝¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝ : FiniteDimensional ℝ E
s : Set H
hs : IsOpen s
h's : IsOpen (↑I.symm ⁻¹' s)
f : E → ℝ
f_supp : support f = ↑I.symm ⁻¹' s
f_diff : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
⊢ support (f ∘ ↑I) = s

Tactic:
rw [support_comp_eq_preimage, f_supp, ← preimage_comp]

Result:
case intro.intro.intro.refine_1
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
H : Type uH
inst✝¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝ : FiniteDimensional ℝ E
s : Set H
hs : IsOpen s
h's : IsOpen (↑I.symm ⁻¹' s)
f : E → ℝ
f_supp : support f = ↑I.symm ⁻¹' s
f_diff : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
⊢ ↑I.symm ∘ ↑I ⁻¹' s = s

Proof state:
case intro.intro.intro.refine_1
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
H : Type uH
inst✝¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝ : FiniteDimensional ℝ E
s : Set H
hs : IsOpen s
h's : IsOpen (↑I.symm ⁻¹' s)
f : E → ℝ
f_supp : support f = ↑I.symm ⁻¹' s
f_diff : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
⊢ ↑I.symm ∘ ↑I ⁻¹' s = s

Tactic:
simp only [ModelWithCorners.symm_comp_self, preimage_id_eq, id_eq]

Result:
no goals

Proof state:
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
H : Type uH
inst✝¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝ : FiniteDimensional ℝ E
s : Set H
hs : IsOpen s
h's : IsOpen (↑I.symm ⁻¹' s)
⊢ ∃ f, support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) ∞ f ∧ range f ⊆ Icc 0 1

Tactic:
rcases h's.exists_smooth_support_eq with ⟨f, f_supp, f_diff, f_range⟩

Result:
case intro.intro.intro
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
H : Type uH
inst✝¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝ : FiniteDimensional ℝ E
s : Set H
hs : IsOpen s
h's : IsOpen (↑I.symm ⁻¹' s)
f : E → ℝ
f_supp : support f = ↑I.symm ⁻¹' s
f_diff : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
⊢ ∃ f, support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) ∞ f ∧ range f ⊆ Icc 0 1

Proof state:
case intro.intro.intro.refine_3
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
H : Type uH
inst✝¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝ : FiniteDimensional ℝ E
s : Set H
hs : IsOpen s
h's : IsOpen (↑I.symm ⁻¹' s)
f : E → ℝ
f_supp : support f = ↑I.symm ⁻¹' s
f_diff : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
⊢ range (f ∘ ↑I) ⊆ Icc 0 1

Tactic:
exact Subset.trans (range_comp_subset_range _ _) f_range

Result:
no goals

Proof state:
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
H : Type uH
inst✝¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝ : FiniteDimensional ℝ E
s : Set H
hs : IsOpen s
⊢ ∃ f, support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) ∞ f ∧ range f ⊆ Icc 0 1

Tactic:
have h's : IsOpen (I.symm ⁻¹' s) := I.continuous_symm.isOpen_preimage _ hs

Result:
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
H : Type uH
inst✝¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝ : FiniteDimensional ℝ E
s : Set H
hs : IsOpen s
h's : IsOpen (↑I.symm ⁻¹' s)
⊢ ∃ f, support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) ∞ f ∧ range f ⊆ Icc 0 1