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

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 : TangentBundle I H
y : ModelProd H E
⊢ ∀ (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✝ : TangentBundle I H
y : ModelProd H E
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 : ℕ∞
⊢ ContMDiff I.tangent (I.prod 𝓘(𝕜, E)) ↑n ⇑(tangentBundleModelSpaceHomeomorph I)

Tactic:
apply contMDiff_iff.2 ⟨Homeomorph.continuous _, fun x y ↦ ?_⟩

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 : TangentBundle I H
y : ModelProd H E
⊢ ContDiffOn 𝕜 (↑n)
    (↑(extChartAt (I.prod 𝓘(𝕜, E)) y) ∘ ⇑(tangentBundleModelSpaceHomeomorph I) ∘ ↑(extChartAt I.tangent x).symm)
    ((extChartAt I.tangent x).target ∩
      ↑(extChartAt I.tangent x).symm ⁻¹'
        (⇑(tangentBundleModelSpaceHomeomorph I) ⁻¹' (extChartAt (I.prod 𝓘(𝕜, E)) y).source))

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 : TangentBundle I H
y : ModelProd H E
⊢ ContDiffOn 𝕜 (↑n)
    (↑(extChartAt (I.prod 𝓘(𝕜, E)) y) ∘ ⇑(tangentBundleModelSpaceHomeomorph I) ∘ ↑(extChartAt I.tangent x).symm)
    ((extChartAt I.tangent x).target ∩
      ↑(extChartAt I.tangent x).symm ⁻¹'
        (⇑(tangentBundleModelSpaceHomeomorph I) ⁻¹' (extChartAt (I.prod 𝓘(𝕜, E)) 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 : TangentBundle I H
y : ModelProd H E
⊢ ∀
    x_1 ∈
      (extChartAt I.tangent x).target ∩
        ↑(extChartAt I.tangent x).symm ⁻¹'
          (⇑(tangentBundleModelSpaceHomeomorph I) ⁻¹' (extChartAt (I.prod 𝓘(𝕜, E)) y).source),
    (↑(extChartAt (I.prod 𝓘(𝕜, E)) y) ∘ ⇑(tangentBundleModelSpaceHomeomorph I) ∘ ↑(extChartAt I.tangent 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✝ : TangentBundle I H
y : ModelProd H E
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:
no goals

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 : TangentBundle I H
y : ModelProd H E
⊢ ∀
    x_1 ∈
      (extChartAt I.tangent x).target ∩
        ↑(extChartAt I.tangent x).symm ⁻¹'
          (⇑(tangentBundleModelSpaceHomeomorph I) ⁻¹' (extChartAt (I.prod 𝓘(𝕜, E)) y).source),
    (↑(extChartAt (I.prod 𝓘(𝕜, E)) y) ∘ ⇑(tangentBundleModelSpaceHomeomorph I) ∘ ↑(extChartAt I.tangent 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 : TangentBundle I H
y : ModelProd H E
⊢ ∀ (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