-- Mathlib/Geometry/Manifold/PartitionOfUnity.lean
theorem exists_msmooth_zero_iff_one_iff_of_isClosed {s t : Set M}
    (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) :
    ∃ f : M → ℝ, ContMDiff I 𝓘(ℝ) ∞ f ∧ range f ⊆ Icc 0 1 ∧ (∀ x, x ∈ s ↔ f x = 0)
      ∧ (∀ x, x ∈ t ↔ f x = 1)

Proof state:
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
s t : Set M
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
⊢ ∃ f, ContMDiff I 𝓘(ℝ, ℝ) ∞ f ∧ range f ⊆ Icc 0 1 ∧ (∀ (x : M), x ∈ s ↔ f x = 0) ∧ ∀ (x : M), x ∈ t ↔ f x = 1

Tactic:
rcases exists_msmooth_support_eq_eq_one_iff I hs.isOpen_compl ht hd.subset_compl_left with
  ⟨f, f_diff, f_range, fs, ft⟩

Result:
case intro.intro.intro.intro
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
s t : Set M
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
f : M → ℝ
f_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ f
f_range : range f ⊆ Icc 0 1
fs : support f = sᶜ
ft : ∀ (x : M), x ∈ t ↔ f x = 1
⊢ ∃ f, ContMDiff I 𝓘(ℝ, ℝ) ∞ f ∧ range f ⊆ Icc 0 1 ∧ (∀ (x : M), x ∈ s ↔ f x = 0) ∧ ∀ (x : M), x ∈ t ↔ f x = 1

Proof state:
case intro.intro.intro.intro
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
s t : Set M
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
f : M → ℝ
f_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ f
f_range : range f ⊆ Icc 0 1
fs : support f = sᶜ
ft : ∀ (x : M), x ∈ t ↔ f x = 1
⊢ ∀ (x : M), x ∈ s ↔ f x = 0

Tactic:
simp [← nmem_support, fs]

Result:
no goals

Proof state:
case intro.intro.intro.intro
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
s t : Set M
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
f : M → ℝ
f_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ f
f_range : range f ⊆ Icc 0 1
fs : support f = sᶜ
ft : ∀ (x : M), x ∈ t ↔ f x = 1
⊢ ∃ f, ContMDiff I 𝓘(ℝ, ℝ) ∞ f ∧ range f ⊆ Icc 0 1 ∧ (∀ (x : M), x ∈ s ↔ f x = 0) ∧ ∀ (x : M), x ∈ t ↔ f x = 1

Tactic:
refine ⟨f, f_diff, f_range, ?_, ft⟩

Result:
case intro.intro.intro.intro
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
s t : Set M
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
f : M → ℝ
f_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ f
f_range : range f ⊆ Icc 0 1
fs : support f = sᶜ
ft : ∀ (x : M), x ∈ t ↔ f x = 1
⊢ ∀ (x : M), x ∈ s ↔ f x = 0