Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: case inl.inr
x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M✝ : Type u_3
inst✝² : TopologicalSpace M✝
inst✝¹ : ChartedSpace H M✝
x y : ℝ
inst✝ : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ n
    (have this := fun z ↦ toLp 2 fun i ↦ -z.ofLp i + (y - x);
    this)
⊢ ContDiffOn ℝ n (↑(𝓡∂ 1) ∘ ↑((IccLeftChart x y).symm ≫ₕ IccRightChart x y) ∘ ↑(𝓡∂ 1).symm)
    (↑(𝓡∂ 1).symm ⁻¹' ((IccLeftChart x y).symm ≫ₕ IccRightChart x y).source ∩ range ↑(𝓡∂ 1))

pp: case inr.inl
x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M✝ : Type u_3
inst✝² : TopologicalSpace M✝
inst✝¹ : ChartedSpace H M✝
x y : ℝ
inst✝ : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ n
    (have this := fun z ↦ toLp 2 fun i ↦ -z.ofLp i + (y - x);
    this)
⊢ ContDiffOn ℝ n (↑(𝓡∂ 1) ∘ ↑((IccRightChart x y).symm ≫ₕ IccLeftChart x y) ∘ ↑(𝓡∂ 1).symm)
    (↑(𝓡∂ 1).symm ⁻¹' ((IccRightChart x y).symm ≫ₕ IccLeftChart x y).source ∩ range ↑(𝓡∂ 1))

pp: case inr.inr
x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M✝ : Type u_3
inst✝² : TopologicalSpace M✝
inst✝¹ : ChartedSpace H M✝
x y : ℝ
inst✝ : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ n
    (have this := fun z ↦ toLp 2 fun i ↦ -z.ofLp i + (y - x);
    this)
⊢ ContDiffOn ℝ n (↑(𝓡∂ 1) ∘ ↑((IccRightChart x y).symm ≫ₕ IccRightChart x y) ∘ ↑(𝓡∂ 1).symm)
    (↑(𝓡∂ 1).symm ⁻¹' ((IccRightChart x y).symm ≫ₕ IccRightChart x y).source ∩ range ↑(𝓡∂ 1))

Tactic:
· -- `e = left chart`, `e' = right chart`
    apply M.contDiffOn.congr
    rintro _ ⟨⟨hz₁, hz₂⟩, ⟨⟨z, hz₀⟩, rfl⟩⟩
    simp only [modelWithCornersEuclideanHalfSpace, IccLeftChart, IccRightChart, update_self,
      max_eq_left, hz₀, lt_sub_iff_add_lt, mfld_simps] at hz₁ hz₂
    rw [min_eq_left hz₁.le, lt_add_iff_pos_left] at hz₂
    ext i
    rw [Subsingleton.elim i 0]
    simp only [modelWithCornersEuclideanHalfSpace, IccLeftChart, IccRightChart, *,
      max_eq_left, min_eq_left hz₁.le, update_self, mfld_simps]
    abel

Goal state after:
case inr.inl
x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M✝ : Type u_3
inst✝² : TopologicalSpace M✝
inst✝¹ : ChartedSpace H M✝
x y : ℝ
inst✝ : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ n
    (have this := fun z ↦ toLp 2 fun i ↦ -z.ofLp i + (y - x);
    this)
⊢ ContDiffOn ℝ n (↑(𝓡∂ 1) ∘ ↑((IccRightChart x y).symm ≫ₕ IccLeftChart x y) ∘ ↑(𝓡∂ 1).symm)
    (↑(𝓡∂ 1).symm ⁻¹' ((IccRightChart x y).symm ≫ₕ IccLeftChart x y).source ∩ range ↑(𝓡∂ 1))

case inr.inr
x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M✝ : Type u_3
inst✝² : TopologicalSpace M✝
inst✝¹ : ChartedSpace H M✝
x y : ℝ
inst✝ : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ n
    (have this := fun z ↦ toLp 2 fun i ↦ -z.ofLp i + (y - x);
    this)
⊢ ContDiffOn ℝ n (↑(𝓡∂ 1) ∘ ↑((IccRightChart x y).symm ≫ₕ IccRightChart x y) ∘ ↑(𝓡∂ 1).symm)
    (↑(𝓡∂ 1).symm ⁻¹' ((IccRightChart x y).symm ≫ₕ IccRightChart x y).source ∩ range ↑(𝓡∂ 1))