-- Mathlib/Geometry/Manifold/WhitneyEmbedding.lean
theorem embeddingPiTangent_injOn : InjOn f.embeddingPiTangent s

Proof state:
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
a✝ : y ∈ s
h : f.embeddingPiTangent x = f.embeddingPiTangent y
⊢ x = y

Tactic:
simp only [embeddingPiTangent_coe, funext_iff] at h

Result:
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
a✝ : y ∈ s
h :
  ∀ (x_1 : ι),
    (↑(f.toFun x_1) x • ↑(extChartAt I (f.c x_1)) x, ↑(f.toFun x_1) x) =
      (↑(f.toFun x_1) y • ↑(extChartAt I (f.c x_1)) y, ↑(f.toFun x_1) y)
⊢ x = y

Proof state:
case intro
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
a✝ : y ∈ s
h :
  ∀ (x_1 : ι),
    (↑(f.toFun x_1) x • ↑(extChartAt I (f.c x_1)) x, ↑(f.toFun x_1) x) =
      (↑(f.toFun x_1) y • ↑(extChartAt I (f.c x_1)) y, ↑(f.toFun x_1) y)
h₁ :
  ↑(f.toFun (f.ind x hx)) x • ↑(extChartAt I (f.c (f.ind x hx))) x =
    ↑(f.toFun (f.ind x hx)) y • ↑(extChartAt I (f.c (f.ind x hx))) y
h₂ : 1 = ↑(f.toFun (f.ind x hx)) y
⊢ x = y

Tactic:
rw [← h₂, f.apply_ind x hx, one_smul, one_smul] at h₁

Result:
case intro
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
a✝ : y ∈ s
h :
  ∀ (x_1 : ι),
    (↑(f.toFun x_1) x • ↑(extChartAt I (f.c x_1)) x, ↑(f.toFun x_1) x) =
      (↑(f.toFun x_1) y • ↑(extChartAt I (f.c x_1)) y, ↑(f.toFun x_1) y)
h₁ : ↑(extChartAt I (f.c (f.ind x hx))) x = ↑(extChartAt I (f.c (f.ind x hx))) y
h₂ : 1 = ↑(f.toFun (f.ind x hx)) y
⊢ x = y

Proof state:
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
⊢ InjOn (⇑f.embeddingPiTangent) s

Tactic:
intro x hx y _ h

Result:
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
a✝ : y ∈ s
h : f.embeddingPiTangent x = f.embeddingPiTangent y
⊢ x = y

Proof state:
case intro
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
a✝ : y ∈ s
h :
  ∀ (x_1 : ι),
    (↑(f.toFun x_1) x • ↑(extChartAt I (f.c x_1)) x, ↑(f.toFun x_1) x) =
      (↑(f.toFun x_1) y • ↑(extChartAt I (f.c x_1)) y, ↑(f.toFun x_1) y)
h₁ : ↑(extChartAt I (f.c (f.ind x hx))) x = ↑(extChartAt I (f.c (f.ind x hx))) y
h₂ : 1 = ↑(f.toFun (f.ind x hx)) y
this : y ∈ (extChartAt I (f.c (f.ind x hx))).source
⊢ x = y

Tactic:
exact (extChartAt I (f.c _)).injOn (f.mem_extChartAt_ind_source x hx) this h₁

Result:
no goals

Proof state:
case intro
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
a✝ : y ∈ s
h :
  ∀ (x_1 : ι),
    (↑(f.toFun x_1) x • ↑(extChartAt I (f.c x_1)) x, ↑(f.toFun x_1) x) =
      (↑(f.toFun x_1) y • ↑(extChartAt I (f.c x_1)) y, ↑(f.toFun x_1) y)
h₁ : ↑(extChartAt I (f.c (f.ind x hx))) x = ↑(extChartAt I (f.c (f.ind x hx))) y
h₂ : 1 = ↑(f.toFun (f.ind x hx)) y
⊢ x = y

Tactic:
have := f.mem_extChartAt_source_of_eq_one h₂.symm

Result:
case intro
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
a✝ : y ∈ s
h :
  ∀ (x_1 : ι),
    (↑(f.toFun x_1) x • ↑(extChartAt I (f.c x_1)) x, ↑(f.toFun x_1) x) =
      (↑(f.toFun x_1) y • ↑(extChartAt I (f.c x_1)) y, ↑(f.toFun x_1) y)
h₁ : ↑(extChartAt I (f.c (f.ind x hx))) x = ↑(extChartAt I (f.c (f.ind x hx))) y
h₂ : 1 = ↑(f.toFun (f.ind x hx)) y
this : y ∈ (extChartAt I (f.c (f.ind x hx))).source
⊢ x = y

Proof state:
case intro
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
a✝ : y ∈ s
h :
  ∀ (x_1 : ι),
    (↑(f.toFun x_1) x • ↑(extChartAt I (f.c x_1)) x, ↑(f.toFun x_1) x) =
      (↑(f.toFun x_1) y • ↑(extChartAt I (f.c x_1)) y, ↑(f.toFun x_1) y)
h₁ :
  ↑(f.toFun (f.ind x hx)) x • ↑(extChartAt I (f.c (f.ind x hx))) x =
    ↑(f.toFun (f.ind x hx)) y • ↑(extChartAt I (f.c (f.ind x hx))) y
h₂ : ↑(f.toFun (f.ind x hx)) x = ↑(f.toFun (f.ind x hx)) y
⊢ x = y

Tactic:
rw [f.apply_ind x hx] at h₂

Result:
case intro
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
a✝ : y ∈ s
h :
  ∀ (x_1 : ι),
    (↑(f.toFun x_1) x • ↑(extChartAt I (f.c x_1)) x, ↑(f.toFun x_1) x) =
      (↑(f.toFun x_1) y • ↑(extChartAt I (f.c x_1)) y, ↑(f.toFun x_1) y)
h₁ :
  ↑(f.toFun (f.ind x hx)) x • ↑(extChartAt I (f.c (f.ind x hx))) x =
    ↑(f.toFun (f.ind x hx)) y • ↑(extChartAt I (f.c (f.ind x hx))) y
h₂ : 1 = ↑(f.toFun (f.ind x hx)) y
⊢ x = y