-- Mathlib/Geometry/Manifold/IsManifold/Basic.lean
/-- Any change of coordinates with empty source belongs to `contDiffGroupoid`. -/
lemma ContDiffGroupoid.mem_of_source_eq_empty (f : PartialHomeomorph H H)
    (hf : f.source = ∅) : f ∈ contDiffGroupoid n I

Proof state:
case right
n : WithTop ℕ∞
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : PartialHomeomorph H H
hf : f.source = ∅
x : E
hx : x ∈ ↑I.symm ⁻¹' f.target
right✝ : x ∈ range ↑I
⊢ ContDiffWithinAt 𝕜 n (↑I ∘ ↑f.symm ∘ ↑I.symm) (↑I.symm ⁻¹' f.target ∩ range ↑I) x

Tactic:
have : f.target = ∅ := by simp [← f.image_source_eq_target, hf]

Result:
case right
n : WithTop ℕ∞
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : PartialHomeomorph H H
hf : f.source = ∅
x : E
hx : x ∈ ↑I.symm ⁻¹' f.target
right✝ : x ∈ range ↑I
this : f.target = ∅
⊢ ContDiffWithinAt 𝕜 n (↑I ∘ ↑f.symm ∘ ↑I.symm) (↑I.symm ⁻¹' f.target ∩ range ↑I) x

Proof state:
n : WithTop ℕ∞
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : PartialHomeomorph H H
hf : f.source = ∅
x : E
hx : x ∈ ↑I.symm ⁻¹' f.target
right✝ : x ∈ range ↑I
⊢ f.target = ∅

Tactic:
simp [← f.image_source_eq_target, hf]

Result:
no goals

Proof state:
case left
n : WithTop ℕ∞
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : PartialHomeomorph H H
hf : f.source = ∅
⊢ (contDiffPregroupoid n I).property (↑f) f.source

Tactic:
intro x ⟨hx, _⟩

Result:
case left
n : WithTop ℕ∞
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : PartialHomeomorph H H
hf : f.source = ∅
x : E
hx : x ∈ ↑I.symm ⁻¹' f.source
right✝ : x ∈ range ↑I
⊢ ContDiffWithinAt 𝕜 n (↑I ∘ ↑f ∘ ↑I.symm) (↑I.symm ⁻¹' f.source ∩ range ↑I) x

Proof state:
n : WithTop ℕ∞
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : PartialHomeomorph H H
hf : f.source = ∅
⊢ f ∈ contDiffGroupoid n I

Tactic:
constructor

Result:
case left
n : WithTop ℕ∞
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : PartialHomeomorph H H
hf : f.source = ∅
⊢ (contDiffPregroupoid n I).property (↑f) f.source

case right
n : WithTop ℕ∞
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : PartialHomeomorph H H
hf : f.source = ∅
⊢ (contDiffPregroupoid n I).property (↑f.symm) f.target

Proof state:
case left
n : WithTop ℕ∞
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : PartialHomeomorph H H
hf : f.source = ∅
x : E
hx : ↑I.symm x ∈ f.source
right✝ : x ∈ range ↑I
⊢ ContDiffWithinAt 𝕜 n (↑I ∘ ↑f ∘ ↑I.symm) (↑I.symm ⁻¹' f.source ∩ range ↑I) x

Tactic:
simp_all only [mem_empty_iff_false]

Result:
no goals

Proof state:
case right
n : WithTop ℕ∞
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : PartialHomeomorph H H
hf : f.source = ∅
x : E
hx : x ∈ ↑I.symm ⁻¹' f.target
right✝ : x ∈ range ↑I
this : f.target = ∅
⊢ ContDiffWithinAt 𝕜 n (↑I ∘ ↑f.symm ∘ ↑I.symm) (↑I.symm ⁻¹' f.target ∩ range ↑I) x

Tactic:
simp_all [hx]

Result:
no goals

Proof state:
case right
n : WithTop ℕ∞
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : PartialHomeomorph H H
hf : f.source = ∅
⊢ (contDiffPregroupoid n I).property (↑f.symm) f.target

Tactic:
intro x ⟨hx, _⟩

Result:
case right
n : WithTop ℕ∞
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : PartialHomeomorph H H
hf : f.source = ∅
x : E
hx : x ∈ ↑I.symm ⁻¹' f.target
right✝ : x ∈ range ↑I
⊢ ContDiffWithinAt 𝕜 n (↑I ∘ ↑f.symm ∘ ↑I.symm) (↑I.symm ⁻¹' f.target ∩ range ↑I) x

Proof state:
case left
n : WithTop ℕ∞
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : PartialHomeomorph H H
hf : f.source = ∅
x : E
hx : x ∈ ↑I.symm ⁻¹' f.source
right✝ : x ∈ range ↑I
⊢ ContDiffWithinAt 𝕜 n (↑I ∘ ↑f ∘ ↑I.symm) (↑I.symm ⁻¹' f.source ∩ range ↑I) x

Tactic:
rw [mem_preimage] at hx

Result:
case left
n : WithTop ℕ∞
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : PartialHomeomorph H H
hf : f.source = ∅
x : E
hx : ↑I.symm x ∈ f.source
right✝ : x ∈ range ↑I
⊢ ContDiffWithinAt 𝕜 n (↑I ∘ ↑f ∘ ↑I.symm) (↑I.symm ⁻¹' f.source ∩ range ↑I) x