-- Mathlib/Geometry/Manifold/PartitionOfUnity.lean
theorem exists_msmooth_support_eq_eq_one_iff
    {s t : Set M} (hs : IsOpen s) (ht : IsClosed t) (h : t ⊆ s) :
    ∃ f : M → ℝ, ContMDiff I 𝓘(ℝ) ∞ f ∧ range f ⊆ Icc 0 1 ∧ support f = s
      ∧ (∀ 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 : IsOpen s
ht : IsClosed t
h : t ⊆ s
⊢ ∃ f, ContMDiff I 𝓘(ℝ, ℝ) ∞ f ∧ range f ⊆ Icc 0 1 ∧ support f = s ∧ ∀ (x : M), x ∈ t ↔ f x = 1

Tactic:
rcases hs.exists_msmooth_support_eq I with ⟨f, f_supp, f_diff, f_pos⟩

Result:
case 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 : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ f
f_pos : ∀ (x : M), 0 ≤ f x
⊢ ∃ f, ContMDiff I 𝓘(ℝ, ℝ) ∞ f ∧ range f ⊆ Icc 0 1 ∧ support f = s ∧ ∀ (x : M), x ∈ t ↔ f x = 1

Proof state:
case intro.intro.intro.intro.intro.intro.refine_2
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 : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
⊢ (range fun x => f x / (f x + g x)) ⊆ Icc 0 1

Tactic:
refine range_subset_iff.2 (fun x ↦ ⟨div_nonneg (f_pos x) (A x).le, ?_⟩)

Result:
case intro.intro.intro.intro.intro.intro.refine_2
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 : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
x : M
⊢ f x / (f x + g x) ≤ 1

Proof state:
case intro.intro.intro.intro.intro.intro.refine_3
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 : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
B : (support fun x => f x + g x) = univ
⊢ (support fun x => f x / (f x + g x)) = s

Tactic:
simp only [support_div, f_supp, B, inter_univ]

Result:
no goals

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 : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
xs : x ∉ support f
⊢ 0 < g x

Tactic:
classical
apply lt_of_le_of_ne (g_pos x) (Ne.symm ?_)
rw [← mem_support, g_supp]
contrapose! xs
simp? at xs says simp only [mem_compl_iff, Decidable.not_not] at xs
exact h.trans f_supp.symm.subset xs

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.refine_4
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 : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
x : M
⊢ x ∈ t ↔ (fun x => f x / (f x + g x)) x = 1

Tactic:
simp [div_eq_one_iff_eq (A x).ne', self_eq_add_right, ← nmem_support, g_supp]

Result:
no goals

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 : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
⊢ 0 < f x + g x

Tactic:
by_cases xs : x ∈ support f

Result:
case pos
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 : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
xs : x ∈ support f
⊢ 0 < f x + g x

case neg
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 : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
xs : x ∉ support f
⊢ 0 < f x + g x