awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
u : OpenPartialHomeomorph H H
h : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (StructureGroupoid.members ⊤) u
⊢ MapsTo (↑I.symm : E → H) ((↑I.symm : E → H) ⁻¹' u.target ∩ range (↑I : H → E)) u.symm.source

Tactic:
(mapsTo_preimage _ _).mono_left inter_subset_left

Premises used: Set.inter_subset_left, Set.mapsTo_preimage, Set.MapsTo.mono_left
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
u : OpenPartialHomeomorph H H
h : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (StructureGroupoid.members ⊤) u
⊢ MapsTo (↑I.symm : E → H) ((↑I.symm : E → H) ⁻¹' u.target ∩ range (↑I : H → E)) u.symm.source

Tactic:
exact (mapsTo_preimage _ _).mono_left inter_subset_left

Premises used: Set.inter_subset_left, Set.mapsTo_preimage, Set.MapsTo.mono_left
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : OpenPartialHomeomorph H H
hf : f.source = ∅
left : (contDiffPregroupoid n I).property (↑f : H → H) f.source
right : (contDiffPregroupoid n I).property (↑f.symm : H → H) f.target
⊢ f ∈ contDiffGroupoid n I

Tactic:
constructor
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : OpenPartialHomeomorph H H
hf : f.source = ∅
x : E
left :
  ∀ (hx : x ∈ (↑I.symm : E → H) ⁻¹' f.source),
    x ∈ range (↑I : H → E) →
      ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑f : H → H) ∘ (↑I.symm : E → H))
        ((↑I.symm : E → H) ⁻¹' f.source ∩ range (↑I : H → E)) x
⊢ x ∈ (↑I.symm : E → H) ⁻¹' f.source ∩ range (↑I : H → E) →
    ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑f : H → H) ∘ (↑I.symm : E → H))
      ((↑I.symm : E → H) ⁻¹' f.source ∩ range (↑I : H → E)) x

Tactic:
⟨hx, _⟩
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : OpenPartialHomeomorph H H
hf : f.source = ∅
x : E
hx : x ∈ (↑I.symm : E → H) ⁻¹' f.source
right : x ∈ range (↑I : H → E)
⊢ (↑I.symm : E → H) x ∈ f.source

Tactic:
rw [mem_preimage] at hx

Premises used: Set.mem_preimage
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : OpenPartialHomeomorph H H
hf : f.source = ∅
x : E
hx : x ∈ (↑I.symm : E → H) ⁻¹' f.source
right : x ∈ range (↑I : H → E)
hx₁ : (↑I.symm : E → H) x ∈ f.source
⊢ x ∈ range (↑I : H → E)

Tactic:
rw [mem_preimage] at hx

Premises used: Set.mem_preimage
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : OpenPartialHomeomorph H H
hf : f.source = ∅
x : E
hx : (↑I.symm : E → H) x ∈ f.source
right : x ∈ range (↑I : H → E)
⊢ ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑f : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' f.source ∩ range (↑I : H → E)) x

Tactic:
simp_all only [mem_empty_iff_false]

Premises used: Set.mem_empty_iff_false
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : OpenPartialHomeomorph H H
hf : f.source = ∅
x : E
right :
  ∀ (hx : x ∈ (↑I.symm : E → H) ⁻¹' f.target),
    x ∈ range (↑I : H → E) →
      ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑f.symm : H → H) ∘ (↑I.symm : E → H))
        ((↑I.symm : E → H) ⁻¹' f.target ∩ range (↑I : H → E)) x
⊢ x ∈ (↑I.symm : E → H) ⁻¹' f.target ∩ range (↑I : H → E) →
    ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑f.symm : H → H) ∘ (↑I.symm : E → H))
      ((↑I.symm : E → H) ⁻¹' f.target ∩ range (↑I : H → E)) x

Tactic:
⟨hx, _⟩
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : OpenPartialHomeomorph H H
hf : f.source = ∅
x : E
hx : x ∈ (↑I.symm : E → H) ⁻¹' f.target
right : x ∈ range (↑I : H → E)
⊢ f.target = ∅

Tactic:
simp [← f.image_source_eq_target, hf]

Premises used: OpenPartialHomeomorph.image_source_eq_target
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : OpenPartialHomeomorph H H
hf : f.source = ∅
x : E
hx : x ∈ (↑I.symm : E → H) ⁻¹' f.target
right : x ∈ range (↑I : H → E)
⊢ f.target = ∅

Tactic:
have : f.target = ∅ := by simp [← f.image_source_eq_target, hf]
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : OpenPartialHomeomorph H H
hf : f.source = ∅
x : E
hx : x ∈ (↑I.symm : E → H) ⁻¹' f.target
right : x ∈ range (↑I : H → E)
this : f.target = ∅
⊢ ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑f.symm : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' f.target ∩ range (↑I : H → E)) x

Tactic:
simp_all
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : OpenPartialHomeomorph H H
hf : f.source = ∅
rw : f ∈ contDiffGroupoid 0 I
⊢ Membership.mem (γ := StructureGroupoid H) (continuousGroupoid H) f

Tactic:
rw [← contDiffGroupoid_zero_eq (I := I)]

Premises used: contDiffGroupoid_zero_eq
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : OpenPartialHomeomorph H H
hf : f.source = ∅
⊢ f ∈ contDiffGroupoid 0 I

Tactic:
ContDiffGroupoid.mem_of_source_eq_empty f hf

Premises used: ContDiffGroupoid.mem_of_source_eq_empty
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : OpenPartialHomeomorph H H
hf : f.source = ∅
⊢ f ∈ contDiffGroupoid 0 I

Tactic:
exact ContDiffGroupoid.mem_of_source_eq_empty f hf

Premises used: ContDiffGroupoid.mem_of_source_eq_empty
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
s : Set H
hs : IsOpen[inst_3] s
h : ContDiffOn 𝕜 n ((↑I : H → E) ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
⊢ (contDiffPregroupoid n I).property (↑(OpenPartialHomeomorph.ofSet s hs) : H → H)
      (OpenPartialHomeomorph.ofSet s hs).source ∧
    (contDiffPregroupoid n I).property (↑(OpenPartialHomeomorph.ofSet s hs).symm : H → H)
      (OpenPartialHomeomorph.ofSet s hs).target

Tactic:
simp [h, contDiffPregroupoid]

Premises used: contDiffPregroupoid
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
s : Set H
hs : IsOpen[inst_3] s
suffices : ContDiffOn 𝕜 n ((↑I : H → E) ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
⊢ (contDiffPregroupoid n I).property (↑(OpenPartialHomeomorph.ofSet s hs) : H → H)
      (OpenPartialHomeomorph.ofSet s hs).source ∧
    (contDiffPregroupoid n I).property (↑(OpenPartialHomeomorph.ofSet s hs).symm : H → H)
      (OpenPartialHomeomorph.ofSet s hs).target

Tactic:
suffices h : ContDiffOn 𝕜 n (I ∘ I.symm) (I.symm ⁻¹' s ∩ range I) by
    simp [h, contDiffPregroupoid]
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
s : Set H
hs : IsOpen[inst_3] s
⊢ ContDiffOn.{u_1, u_2, u_2} 𝕜 (E := E) n id univ

Tactic:
have : ContDiffOn 𝕜 n id (univ : Set E) := contDiff_id.contDiffOn
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
s : Set H
hs : IsOpen[inst_3] s
this : ContDiffOn.{u_1, u_2, u_2} 𝕜 (E := E) n id univ
⊢ ContDiffOn 𝕜 n ((↑I : H → E) ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))

Tactic:
this.congr_mono (fun x hx => I.right_inv hx.2) (subset_univ _)

Premises used: Set.subset_univ, ContDiffOn.congr_mono, ModelWithCorners.right_inv, And.right
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
s : Set H
hs : IsOpen[inst_3] s
this : ContDiffOn.{u_1, u_2, u_2} 𝕜 (E := E) n id univ
⊢ ContDiffOn 𝕜 n ((↑I : H → E) ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))

Tactic:
exact this.congr_mono (fun x hx => I.right_inv hx.2) (subset_univ _)

Premises used: Set.subset_univ, ContDiffOn.congr_mono, ModelWithCorners.right_inv
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
e : OpenPartialHomeomorph M H
⊢ e.symm ≫ₕ e ∈ contDiffGroupoid n I

Tactic:
haveI : e.symm.trans e ≈ OpenPartialHomeomorph.ofSet e.target e.open_target :=
    OpenPartialHomeomorph.symm_trans_self _
  StructureGroupoid.mem_of_eqOnSource _ (ofSet_mem_contDiffGroupoid e.open_target) this

Premises used: StructureGroupoid.mem_of_eqOnSource, contDiffGroupoid, OpenPartialHomeomorph.symm_trans_self, ofSet_mem_contDiffGroupoid, OpenPartialHomeomorph.open_target
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
E' : Type u_5
H' : Type u_6
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : e ∈ contDiffGroupoid n I
he' : e' ∈ contDiffGroupoid n I'
⊢ (contDiffPregroupoid n I).property (↑e : H → H) e.source

Tactic:
obtain ⟨he, he_symm⟩ := he
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
E' : Type u_5
H' : Type u_6
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : e ∈ contDiffGroupoid n I
he' : e' ∈ contDiffGroupoid n I'
he₁ : (contDiffPregroupoid n I).property (↑e : H → H) e.source
⊢ (contDiffPregroupoid n I).property (↑e.symm : H → H) e.target

Tactic:
obtain ⟨he, he_symm⟩ := he
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
E' : Type u_5
H' : Type u_6
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ contDiffGroupoid n I'
he : (contDiffPregroupoid n I).property (↑e : H → H) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm : H → H) e.target
⊢ (contDiffPregroupoid n I').property (↑e' : H' → H') e'.source

Tactic:
obtain ⟨he', he'_symm⟩ := he'
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
E' : Type u_5
H' : Type u_6
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ contDiffGroupoid n I'
he : (contDiffPregroupoid n I).property (↑e : H → H) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm : H → H) e.target
he'₁ : (contDiffPregroupoid n I').property (↑e' : H' → H') e'.source
⊢ (contDiffPregroupoid n I').property (↑e'.symm : H' → H') e'.target

Tactic:
obtain ⟨he', he'_symm⟩ := he'
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
E' : Type u_5
H' : Type u_6
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e : H → H) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm : H → H) e.target
he' : (contDiffPregroupoid n I').property (↑e' : H' → H') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm : H' → H') e'.target
left : (contDiffPregroupoid n (I.prod I')).property (↑(e.prod e') : ModelProd H H' → ModelProd H H') (e.prod e').source
right :
  (contDiffPregroupoid n (I.prod I')).property (↑(e.prod e').symm : ModelProd H H' → ModelProd H H') (e.prod e').target
⊢ e.prod e' ∈ contDiffGroupoid n (I.prod I')

Tactic:
constructor
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
E' : Type u_5
H' : Type u_6
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e : H → H) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm : H → H) e.target
he' : (contDiffPregroupoid n I').property (↑e' : H' → H') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm : H' → H') e'.target
⊢ ContDiffOn 𝕜 n
    (Prod.map ((↑I : H → E) ∘ (↑e : H → H) ∘ (↑I.symm : E → H))
      ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H')))
    (((↑I.symm : E → H) ⁻¹' e.source ∩ range (↑I : H → E)) ×ˢ
      ((↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E')))

Tactic:
have h3 := ContDiffOn.prodMap he he'
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
E' : Type u_5
H' : Type u_6
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e : H → H) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm : H → H) e.target
he' : (contDiffPregroupoid n I').property (↑e' : H' → H') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm : H' → H') e'.target
h3 :
  ContDiffOn 𝕜 n
    (Prod.map ((↑I : H → E) ∘ (↑e : H → H) ∘ (↑I.symm : E → H))
      ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H')))
    (((↑I.symm : E → H) ⁻¹' e.source ∩ range (↑I : H → E)) ×ˢ
      ((↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E')))
⊢ ContDiffOn 𝕜 n
    (Prod.map ((↑I : H → E) ∘ (↑e : H → H) ∘ (↑I.symm : E → H))
      ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H')))
    ((fun (p : H × H') ↦ ((↑I : H → E) p.1, (↑I' : H' → E') p.2)) '' e.source ×ˢ e'.source)

Tactic:
rw [← I.image_eq, ← I'.image_eq, prod_image_image_eq] at h3

Premises used: ModelWithCorners.image_eq, Set.prod_image_image_eq
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
E' : Type u_5
H' : Type u_6
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e : H → H) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm : H → H) e.target
he' : (contDiffPregroupoid n I').property (↑e' : H' → H') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm : H' → H') e'.target
h3 :
  ContDiffOn 𝕜 n
    (Prod.map ((↑I : H → E) ∘ (↑e : H → H) ∘ (↑I.symm : E → H))
      ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H')))
    ((fun (p : H × H') ↦ ((↑I : H → E) p.1, (↑I' : H' → E') p.2)) '' e.source ×ˢ e'.source)
left :
  ContDiffOn 𝕜 n
    ((↑(I.prod I') : ModelProd H H' → E × E') ∘
      (↑(e.prod e') : ModelProd H H' → ModelProd H H') ∘ (↑(I.prod I').symm : E × E' → ModelProd H H'))
    ((↑(I.prod I') : ModelProd H H' → E × E') '' e.source ×ˢ e'.source)
⊢ ContDiffOn 𝕜 n
    ((↑(I.prod I') : ModelProd H H' → E × E') ∘
      (↑(e.prod e') : ModelProd H H' → ModelProd H H') ∘ (↑(I.prod I').symm : E × E' → ModelProd H H'))
    ((↑(I.prod I').symm : E × E' → ModelProd H H') ⁻¹' e.source ×ˢ e'.source ∩
      range (↑(I.prod I') : ModelProd H H' → E × E'))

Tactic:
rw [← (I.prod I').image_eq]

Premises used: ModelWithCorners.image_eq, ModelWithCorners.prod
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
E' : Type u_5
H' : Type u_6
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e : H → H) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm : H → H) e.target
he' : (contDiffPregroupoid n I').property (↑e' : H' → H') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm : H' → H') e'.target
h3 :
  ContDiffOn 𝕜 n
    (Prod.map ((↑I : H → E) ∘ (↑e : H → H) ∘ (↑I.symm : E → H))
      ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H')))
    ((fun (p : H × H') ↦ ((↑I : H → E) p.1, (↑I' : H' → E') p.2)) '' e.source ×ˢ e'.source)
⊢ ContDiffOn 𝕜 n
    ((↑(I.prod I') : ModelProd H H' → E × E') ∘
      (↑(e.prod e') : ModelProd H H' → ModelProd H H') ∘ (↑(I.prod I').symm : E × E' → ModelProd H H'))
    ((↑(I.prod I') : ModelProd H H' → E × E') '' e.source ×ˢ e'.source)

Tactic:
h3

Premises used: OpenPartialHomeomorph.toFun', ModelWithCorners.toFun', ModelProd
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
E' : Type u_5
H' : Type u_6
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e : H → H) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm : H → H) e.target
he' : (contDiffPregroupoid n I').property (↑e' : H' → H') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm : H' → H') e'.target
h3 :
  ContDiffOn 𝕜 n
    (Prod.map ((↑I : H → E) ∘ (↑e : H → H) ∘ (↑I.symm : E → H))
      ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H')))
    ((fun (p : H × H') ↦ ((↑I : H → E) p.1, (↑I' : H' → E') p.2)) '' e.source ×ˢ e'.source)
⊢ ContDiffOn 𝕜 n
    ((↑(I.prod I') : ModelProd H H' → E × E') ∘
      (↑(e.prod e') : ModelProd H H' → ModelProd H H') ∘ (↑(I.prod I').symm : E × E' → ModelProd H H'))
    ((↑(I.prod I') : ModelProd H H' → E × E') '' e.source ×ˢ e'.source)

Tactic:
exact h3
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
E' : Type u_5
H' : Type u_6
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e : H → H) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm : H → H) e.target
he' : (contDiffPregroupoid n I').property (↑e' : H' → H') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm : H' → H') e'.target
⊢ ContDiffOn 𝕜 n
    (Prod.map ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H))
      ((↑I' : H' → E') ∘ (↑e'.symm : H' → H') ∘ (↑I'.symm : E' → H')))
    (((↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E)) ×ˢ
      ((↑I'.symm : E' → H') ⁻¹' e'.target ∩ range (↑I' : H' → E')))

Tactic:
have h3 := ContDiffOn.prodMap he_symm he'_symm
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
E' : Type u_5
H' : Type u_6
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e : H → H) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm : H → H) e.target
he' : (contDiffPregroupoid n I').property (↑e' : H' → H') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm : H' → H') e'.target
h3 :
  ContDiffOn 𝕜 n
    (Prod.map ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H))
      ((↑I' : H' → E') ∘ (↑e'.symm : H' → H') ∘ (↑I'.symm : E' → H')))
    (((↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E)) ×ˢ
      ((↑I'.symm : E' → H') ⁻¹' e'.target ∩ range (↑I' : H' → E')))
⊢ ContDiffOn 𝕜 n
    (Prod.map ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H))
      ((↑I' : H' → E') ∘ (↑e'.symm : H' → H') ∘ (↑I'.symm : E' → H')))
    ((fun (p : H × H') ↦ ((↑I : H → E) p.1, (↑I' : H' → E') p.2)) '' e.target ×ˢ e'.target)

Tactic:
rw [← I.image_eq, ← I'.image_eq, prod_image_image_eq] at h3

Premises used: ModelWithCorners.image_eq, Set.prod_image_image_eq