-- Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
theorem contMDiff_tangentBundleModelSpaceHomeomorph_symm {n : ℕ∞} :
    ContMDiff (I.prod 𝓘(𝕜, E)) I.tangent n
    ((tangentBundleModelSpaceHomeomorph I).symm : ModelProd H E → TangentBundle I H)

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞
x : ModelProd H E
y : TangentBundle I H
⊢ ∀ (a b : E) (x : H),
    ↑I x = a →
      ↑I
            ({ toFun := fun x => (x.proj, x.snd), invFun := fun x => { proj := x.1, snd := x.2 }, left_inv := ⋯,
                  right_inv := ⋯ }
                { proj := (↑(I.prod (PartialEquiv.refl E)).symm (a, b)).1,
                  snd := (↑(I.prod (PartialEquiv.refl E)).symm (a, b)).2 }).1 =
          a ∧
        ({ toFun := fun x => (x.proj, x.snd), invFun := fun x => { proj := x.1, snd := x.2 }, left_inv := ⋯,
                right_inv := ⋯ }
              { proj := (↑(I.prod (PartialEquiv.refl E)).symm (a, b)).1,
                snd := (↑(I.prod (PartialEquiv.refl E)).symm (a, b)).2 }).2 =
          b

Tactic:
rintro a b x rfl

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞
x✝ : ModelProd H E
y : TangentBundle I H
b : E
x : H
⊢ ↑I
        ({ toFun := fun x => (x.proj, x.snd), invFun := fun x => { proj := x.1, snd := x.2 }, left_inv := ⋯,
              right_inv := ⋯ }
            { proj := (↑(I.prod (PartialEquiv.refl E)).symm (↑I x, b)).1,
              snd := (↑(I.prod (PartialEquiv.refl E)).symm (↑I x, b)).2 }).1 =
      ↑I x ∧
    ({ toFun := fun x => (x.proj, x.snd), invFun := fun x => { proj := x.1, snd := x.2 }, left_inv := ⋯,
            right_inv := ⋯ }
          { proj := (↑(I.prod (PartialEquiv.refl E)).symm (↑I x, b)).1,
            snd := (↑(I.prod (PartialEquiv.refl E)).symm (↑I x, b)).2 }).2 =
      b

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞
x✝ : ModelProd H E
y : TangentBundle I H
b : E
x : H
⊢ ↑I
        ({ toFun := fun x => (x.proj, x.snd), invFun := fun x => { proj := x.1, snd := x.2 }, left_inv := ⋯,
              right_inv := ⋯ }
            { proj := (↑(I.prod (PartialEquiv.refl E)).symm (↑I x, b)).1,
              snd := (↑(I.prod (PartialEquiv.refl E)).symm (↑I x, b)).2 }).1 =
      ↑I x ∧
    ({ toFun := fun x => (x.proj, x.snd), invFun := fun x => { proj := x.1, snd := x.2 }, left_inv := ⋯,
            right_inv := ⋯ }
          { proj := (↑(I.prod (PartialEquiv.refl E)).symm (↑I x, b)).1,
            snd := (↑(I.prod (PartialEquiv.refl E)).symm (↑I x, b)).2 }).2 =
      b

Tactic:
simp [PartialEquiv.prod]

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞
x✝ : ModelProd H E
y : TangentBundle I H
b : E
x : H
⊢ ↑I
        ({ toFun := fun x => (x.proj, x.snd), invFun := fun x => { proj := x.1, snd := x.2 }, left_inv := ⋯,
              right_inv := ⋯ }
            { proj := x, snd := b }).1 =
      ↑I x ∧
    ({ toFun := fun x => (x.proj, x.snd), invFun := fun x => { proj := x.1, snd := x.2 }, left_inv := ⋯,
            right_inv := ⋯ }
          { proj := x, snd := b }).2 =
      b

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞
x : ModelProd H E
y : TangentBundle I H
⊢ ∀
    x_1 ∈
      (extChartAt (I.prod 𝓘(𝕜, E)) x).target ∩
        ↑(extChartAt (I.prod 𝓘(𝕜, E)) x).symm ⁻¹'
          (⇑(tangentBundleModelSpaceHomeomorph I).symm ⁻¹' (extChartAt I.tangent y).source),
    (↑(extChartAt I.tangent y) ∘ ⇑(tangentBundleModelSpaceHomeomorph I).symm ∘ ↑(extChartAt (I.prod 𝓘(𝕜, E)) x).symm)
        x_1 =
      _root_.id x_1

Tactic:
simp only [mfld_simps, mem_range, TotalSpace.toProd, Equiv.coe_fn_symm_mk, forall_exists_index,
  Prod.forall, Prod.mk.injEq]

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞
x : ModelProd H E
y : TangentBundle I H
⊢ ∀ (a b : E) (x : H),
    ↑I x = a →
      ↑I
            ({ toFun := fun x => (x.proj, x.snd), invFun := fun x => { proj := x.1, snd := x.2 }, left_inv := ⋯,
                  right_inv := ⋯ }
                { proj := (↑(I.prod (PartialEquiv.refl E)).symm (a, b)).1,
                  snd := (↑(I.prod (PartialEquiv.refl E)).symm (a, b)).2 }).1 =
          a ∧
        ({ toFun := fun x => (x.proj, x.snd), invFun := fun x => { proj := x.1, snd := x.2 }, left_inv := ⋯,
                right_inv := ⋯ }
              { proj := (↑(I.prod (PartialEquiv.refl E)).symm (a, b)).1,
                snd := (↑(I.prod (PartialEquiv.refl E)).symm (a, b)).2 }).2 =
          b

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞
x : ModelProd H E
y : TangentBundle I H
⊢ ContDiffOn 𝕜 (↑n)
    (↑(extChartAt I.tangent y) ∘ ⇑(tangentBundleModelSpaceHomeomorph I).symm ∘ ↑(extChartAt (I.prod 𝓘(𝕜, E)) x).symm)
    ((extChartAt (I.prod 𝓘(𝕜, E)) x).target ∩
      ↑(extChartAt (I.prod 𝓘(𝕜, E)) x).symm ⁻¹'
        (⇑(tangentBundleModelSpaceHomeomorph I).symm ⁻¹' (extChartAt I.tangent y).source))

Tactic:
apply contDiffOn_id.congr

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞
x : ModelProd H E
y : TangentBundle I H
⊢ ∀
    x_1 ∈
      (extChartAt (I.prod 𝓘(𝕜, E)) x).target ∩
        ↑(extChartAt (I.prod 𝓘(𝕜, E)) x).symm ⁻¹'
          (⇑(tangentBundleModelSpaceHomeomorph I).symm ⁻¹' (extChartAt I.tangent y).source),
    (↑(extChartAt I.tangent y) ∘ ⇑(tangentBundleModelSpaceHomeomorph I).symm ∘ ↑(extChartAt (I.prod 𝓘(𝕜, E)) x).symm)
        x_1 =
      _root_.id x_1

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞
x✝ : ModelProd H E
y : TangentBundle I H
b : E
x : H
⊢ ↑I
        ({ toFun := fun x => (x.proj, x.snd), invFun := fun x => { proj := x.1, snd := x.2 }, left_inv := ⋯,
              right_inv := ⋯ }
            { proj := x, snd := b }).1 =
      ↑I x ∧
    ({ toFun := fun x => (x.proj, x.snd), invFun := fun x => { proj := x.1, snd := x.2 }, left_inv := ⋯,
            right_inv := ⋯ }
          { proj := x, snd := b }).2 =
      b

Tactic:
exact ⟨rfl, rfl⟩

Result:
no goals