awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
ι : Type v
inst_1 : Fintype ι
E : ι → Type w
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, w} 𝕜 (E i)
H : ι → Type u'
inst_4 : (i : ι) → TopologicalSpace (H i)
I : (i : ι) → ModelWithCorners.{u, w, u'} 𝕜 (E i) (H i)
h : ¬IsRCLikeNormedField 𝕜
⊢ Eq (α := Set ((i : ι) → E i)) (Set.pi (α := E) univ fun (i : ι) ↦ range (↑(I i).toPartialEquiv : H i → E i)) univ

Tactic:
simp [range_eq_univ_of_not_isRCLikeNormedField, h]

Premises used: ModelWithCorners.range_eq_univ_of_not_isRCLikeNormedField
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
ι : Type v
inst_1 : Fintype ι
E : ι → Type w
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, w} 𝕜 (E i)
H : ι → Type u'
inst_4 : (i : ι) → TopologicalSpace (H i)
I : (i : ι) → ModelWithCorners.{u, w, u'} 𝕜 (E i) (H i)
rw :
  Set.Nonempty (α := (i : ι) → E i)
    (interior (Set.pi (α := E) univ fun (i : ι) ↦ range (↑(I i).toPartialEquiv : H i → E i)))
⊢ Set.Nonempty (α := (i : ι) → E i)
    (interior
      (range (ι := ModelPi H)
        (↑(PartialEquiv.pi (αi := H) (βi := E) fun (i : ι) ↦ (I i).toPartialEquiv) : ModelPi H → (i : ι) → E i)))

Tactic:
rw [PartialEquiv.pi_apply, Set.range_piMap]

Premises used: Set.range_piMap, PartialEquiv.pi_apply
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
ι : Type v
inst_1 : Fintype ι
E : ι → Type w
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, w} 𝕜 (E i)
H : ι → Type u'
inst_4 : (i : ι) → TopologicalSpace (H i)
I : (i : ι) → ModelWithCorners.{u, w, u'} 𝕜 (E i) (H i)
⊢ Set.Nonempty (α := (i : ι) → E i)
    (interior (Set.pi (α := E) univ fun (i : ι) ↦ range (↑(I i).toPartialEquiv : H i → E i)))

Tactic:
simp [interior_pi_set finite_univ, univ_pi_nonempty_iff, nonempty_interior]

Premises used: Set.univ_pi_nonempty_iff, ModelWithCorners.nonempty_interior, Set.finite_univ, interior_pi_set
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_5
inst_5 : TopologicalSpace H
G : Type u_7
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
⊢ (I.prod J).toPartialEquiv = I.prod J.toPartialEquiv

Tactic:
rfl

Premises used: PartialEquiv.prod, setOf, Set.prod, ModelWithCorners.toFun', ModelProd, rfl
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H : Type u_5
inst_5 : TopologicalSpace H
H' : Type u_6
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
⊢ (↑(I.prod I') : ModelProd H H' → E × E') = Prod.map (↑I : H → E) (↑I' : H' → E')

Tactic:
rfl

Premises used: Prod.map, ModelWithCorners.toFun', ModelProd, rfl
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H : Type u_5
inst_5 : TopologicalSpace H
H' : Type u_6
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
⊢ (↑(I.prod I').symm : E × E' → ModelProd H H') = Prod.map (↑I.symm : E → H) (↑I'.symm : E' → H')

Tactic:
rfl

Premises used: Prod.map, rfl
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
toFun :
  (↑(ModelWithCorners.toPartialEquiv 𝓘(𝕜, E × F)) : E × F → E × F) =
    (↑(ModelWithCorners.toPartialEquiv (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, F))) : E × F → E × F)
invFun :
  PartialEquiv.invFun (ModelWithCorners.toPartialEquiv 𝓘(𝕜, E × F)) =
    (ModelWithCorners.toPartialEquiv (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, F))).invFun
source :
  PartialEquiv.source (ModelWithCorners.toPartialEquiv 𝓘(𝕜, E × F)) =
    (ModelWithCorners.toPartialEquiv (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, F))).source
target :
  PartialEquiv.target (ModelWithCorners.toPartialEquiv 𝓘(𝕜, E × F)) =
    (ModelWithCorners.toPartialEquiv (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, F))).target
⊢ Eq (α := ModelWithCorners 𝕜 (E × F) (E × F)) 𝓘(𝕜, E × F) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, F))

Tactic:
ext1
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
⊢ (↑(ModelWithCorners.toPartialEquiv 𝓘(𝕜, E × F)) : E × F → E × F) =
    (↑(ModelWithCorners.toPartialEquiv (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, F))) : E × F → E × F)

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
⊢ PartialEquiv.invFun (ModelWithCorners.toPartialEquiv 𝓘(𝕜, E × F)) =
    (ModelWithCorners.toPartialEquiv (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, F))).invFun

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
⊢ source (ModelWithCorners.toPartialEquiv 𝓘(𝕜, E × F)) =
    (ModelWithCorners.toPartialEquiv (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, F))).source

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
⊢ target (ModelWithCorners.toPartialEquiv 𝓘(𝕜, E × F)) =
    (ModelWithCorners.toPartialEquiv (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, F))).target

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_5
inst_5 : TopologicalSpace H
G : Type u_7
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
simp_rw : (I.prod J).target = I.target ×ˢ J.target
⊢ range (↑(I.prod J) : ModelProd H G → E × F) = range (↑I : H → E) ×ˢ range (↑J : G → F)

Tactic:
simp_rw [← ModelWithCorners.target_eq]

Premises used: ModelWithCorners.target_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
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_5
inst_5 : TopologicalSpace H
G : Type u_7
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
⊢ (I.prod J).target = I.target ×ˢ J.target

Tactic:
rfl
-- 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
inst_4 : I.Boundaryless
⊢ range (↑I : H → E) = univ

Tactic:
ModelWithCorners.Boundaryless.range_eq_univ

Premises used: ModelWithCorners.Boundaryless.range_eq_univ
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
⊢ range (↑𝓘(𝕜, E) : E → E) = univ

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type w
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
inst_4 : I.Boundaryless
E' : Type v'
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type w'
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
inst_8 : I'.Boundaryless
range_eq_univ : range (↑(I.prod I') : ModelProd H H' → E × E') = univ
⊢ (I.prod I').Boundaryless

Tactic:
constructor
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type w
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
inst_4 : I.Boundaryless
E' : Type v'
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type w'
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
inst_8 : I'.Boundaryless
range_eq_univ : range (↑I : H → E) ×ˢ range (↑I' : H' → E') = univ
range_eq_univ₁ : SProd.sprod (α := Set E) univ (range (↑I' : H' → E')) = univ
range_eq_univ₂ : SProd.sprod (α := Set E) (β := Set E') univ univ = univ
range_eq_univ₃ range_eq_univ₄ : Eq (α := Set (E × E')) univ univ
⊢ Eq (α := Set (E × E')) (range fun (x : H × H') ↦ ((↑I : H → E) x.1, (↑I' : H' → E') x.2)) univ

Tactic:
rw [← prod_range_range_eq, ModelWithCorners.Boundaryless.range_eq_univ,
    ModelWithCorners.Boundaryless.range_eq_univ, univ_prod_univ]

Premises used: Set.univ_prod_univ, Set.prod_range_range_eq, ModelWithCorners.Boundaryless.range_eq_univ
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
m 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
f g : H → H
u v : Set H
hf : ContDiffOn 𝕜 n ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' u ∩ range (↑I : H → E))
hg : ContDiffOn 𝕜 n ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' v ∩ range (↑I : H → E))
h_1 : IsOpen[inst_3] u
h_2 : IsOpen[inst_3] v
h_3 : IsOpen[inst_3] (u ∩ f ⁻¹' v)
h :
  ∀ (x : E),
    ((↑I : H → E) ∘ (g ∘ f) ∘ (↑I.symm : E → H)) x =
      (((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ∘ (↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) x
⊢ (↑I : H → E) ∘ (g ∘ f) ∘ (↑I.symm : E → H) =
    ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ∘ (↑I : H → E) ∘ f ∘ (↑I.symm : E → H)

Tactic:
ext x
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
m 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
f g : H → H
u v : Set H
hf : ContDiffOn 𝕜 n ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' u ∩ range (↑I : H → E))
hg : ContDiffOn 𝕜 n ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' v ∩ range (↑I : H → E))
h : IsOpen[inst_3] u
h_1 : IsOpen[inst_3] v
h_2 : IsOpen[inst_3] (u ∩ f ⁻¹' v)
x : E
⊢ ((↑I : H → E) ∘ (g ∘ f) ∘ (↑I.symm : E → H)) x =
    (((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ∘ (↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) x

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
m 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
f g : H → H
u v : Set H
hf : ContDiffOn 𝕜 n ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' u ∩ range (↑I : H → E))
hg : ContDiffOn 𝕜 n ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' v ∩ range (↑I : H → E))
h : IsOpen[inst_3] u
h_1 : IsOpen[inst_3] v
h_2 : IsOpen[inst_3] (u ∩ f ⁻¹' v)
⊢ (↑I : H → E) ∘ (g ∘ f) ∘ (↑I.symm : E → H) =
    ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ∘ (↑I : H → E) ∘ f ∘ (↑I.symm : E → H)

Tactic:
have : I ∘ (g ∘ f) ∘ I.symm = (I ∘ g ∘ I.symm) ∘ I ∘ f ∘ I.symm := by ext x; simp
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
m 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
f g : H → H
u v : Set H
hf : ContDiffOn 𝕜 n ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' u ∩ range (↑I : H → E))
hg : ContDiffOn 𝕜 n ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' v ∩ range (↑I : H → E))
h : IsOpen[inst_3] u
h_1 : IsOpen[inst_3] v
h_2 : IsOpen[inst_3] (u ∩ f ⁻¹' v)
this :
  (↑I : H → E) ∘ (g ∘ f) ∘ (↑I.symm : E → H) =
    ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ∘ (↑I : H → E) ∘ f ∘ (↑I.symm : E → H)
simp :
  ContDiffOn 𝕜 n (((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ∘ (↑I : H → E) ∘ f ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' (u ∩ f ⁻¹' v) ∩ range (↑I : H → E))
⊢ ContDiffOn 𝕜 n ((↑I : H → E) ∘ (g ∘ f) ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' (u ∩ f ⁻¹' v) ∩ range (↑I : H → E))

Tactic:
simp only [this]
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
m 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
f g : H → H
u v : Set H
hf : ContDiffOn 𝕜 n ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' u ∩ range (↑I : H → E))
hg : ContDiffOn 𝕜 n ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' v ∩ range (↑I : H → E))
h : IsOpen[inst_3] u
h_1 : IsOpen[inst_3] v
h_2 : IsOpen[inst_3] (u ∩ f ⁻¹' v)
this :
  (↑I : H → E) ∘ (g ∘ f) ∘ (↑I.symm : E → H) =
    ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ∘ (↑I : H → E) ∘ f ∘ (↑I.symm : E → H)
⊢ ContDiffOn 𝕜 n (((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ∘ (↑I : H → E) ∘ f ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' (u ∩ f ⁻¹' v) ∩ range (↑I : H → E))

Tactic:
hg.comp (hf.mono fun x ⟨hx1, hx2⟩ ↦ ⟨hx1.1, hx2⟩) ?_

Premises used: ContDiffOn.comp, ContDiffOn.mono, Membership.mem, ModelWithCorners.toFun', Inter.inter, _private.0.contDiffPregroupoid.match_1, Set.preimage, And.left, And.intro, ModelWithCorners.symm, Set.range, PartialEquiv.toFun
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
m 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
f g : H → H
u v : Set H
hf : ContDiffOn 𝕜 n ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' u ∩ range (↑I : H → E))
hg : ContDiffOn 𝕜 n ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' v ∩ range (↑I : H → E))
h : IsOpen[inst_3] u
h_1 : IsOpen[inst_3] v
h_2 : IsOpen[inst_3] (u ∩ f ⁻¹' v)
this :
  (↑I : H → E) ∘ (g ∘ f) ∘ (↑I.symm : E → H) =
    ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ∘ (↑I : H → E) ∘ f ∘ (↑I.symm : E → H)
refine :
  MapsTo ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' (u ∩ f ⁻¹' v) ∩ range (↑I : H → E))
    ((↑I.symm : E → H) ⁻¹' v ∩ range (↑I : H → E))
⊢ ContDiffOn 𝕜 n (((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ∘ (↑I : H → E) ∘ f ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' (u ∩ f ⁻¹' v) ∩ range (↑I : H → E))

Tactic:
refine hg.comp (hf.mono fun x ⟨hx1, hx2⟩ ↦ ⟨hx1.1, hx2⟩) ?_
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
m 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
f g : H → H
u v : Set H
hf : ContDiffOn 𝕜 n ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' u ∩ range (↑I : H → E))
hg : ContDiffOn 𝕜 n ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' v ∩ range (↑I : H → E))
h : IsOpen[inst_3] u
h_1 : IsOpen[inst_3] v
h_2 : IsOpen[inst_3] (u ∩ f ⁻¹' v)
this :
  (↑I : H → E) ∘ (g ∘ f) ∘ (↑I.symm : E → H) =
    ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ∘ (↑I : H → E) ∘ f ∘ (↑I.symm : E → H)
x : E
hx1 : x ∈ (↑I.symm : E → H) ⁻¹' (u ∩ f ⁻¹' v)
right : x ∈ range (↑I : H → E)
simp : ∀ (hx1 : (↑I.symm : E → H) x ∈ u ∧ f ((↑I.symm : E → H) x) ∈ v), f ((↑I.symm : E → H) x) ∈ v
⊢ ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) x ∈ (↑I.symm : E → H) ⁻¹' v ∩ range (↑I : H → E)

Tactic:
simp only [mfld_simps] at hx1 ⊢
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
m 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
f g : H → H
u v : Set H
hf : ContDiffOn 𝕜 n ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' u ∩ range (↑I : H → E))
hg : ContDiffOn 𝕜 n ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' v ∩ range (↑I : H → E))
h : IsOpen[inst_3] u
h_1 : IsOpen[inst_3] v
h_2 : IsOpen[inst_3] (u ∩ f ⁻¹' v)
this :
  (↑I : H → E) ∘ (g ∘ f) ∘ (↑I.symm : E → H) =
    ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ∘ (↑I : H → E) ∘ f ∘ (↑I.symm : E → H)
x : E
right : x ∈ range (↑I : H → E)
hx1 : (↑I.symm : E → H) x ∈ u ∧ f ((↑I.symm : E → H) x) ∈ v
⊢ f ((↑I.symm : E → H) x) ∈ v

Tactic:
hx1.2

Premises used: And.right
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
m 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
f g : H → H
u v : Set H
hf : ContDiffOn 𝕜 n ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' u ∩ range (↑I : H → E))
hg : ContDiffOn 𝕜 n ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' v ∩ range (↑I : H → E))
h : IsOpen[inst_3] u
h_1 : IsOpen[inst_3] v
h_2 : IsOpen[inst_3] (u ∩ f ⁻¹' v)
this :
  (↑I : H → E) ∘ (g ∘ f) ∘ (↑I.symm : E → H) =
    ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ∘ (↑I : H → E) ∘ f ∘ (↑I.symm : E → H)
x : E
right : x ∈ range (↑I : H → E)
hx1 : (↑I.symm : E → H) x ∈ u ∧ f ((↑I.symm : E → H) x) ∈ v
⊢ f ((↑I.symm : E → H) x) ∈ v

Tactic:
exact hx1.2

Premises used: And.right
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
m 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
apply : ∀ x ∈ (↑I.symm : E → H) ⁻¹' univ ∩ range (↑I : H → E), ((↑I : H → E) ∘ id ∘ (↑I.symm : E → H)) x = id x
⊢ ContDiffOn 𝕜 n ((↑I : H → E) ∘ id ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' univ ∩ range (↑I : H → E))

Tactic:
apply ContDiffOn.congr contDiff_id.contDiffOn

Premises used: ContDiffOn.congr, contDiff_id, ContDiff.contDiffOn
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
m 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
x : E
left : x ∈ (↑I.symm : E → H) ⁻¹' univ
hx2 : x ∈ range (↑I : H → E)
rcases : ∀ (y : H) (hy : (↑I : H → E) y = x), ((↑I : H → E) ∘ id ∘ (↑I.symm : E → H)) x = id x
⊢ ((↑I : H → E) ∘ id ∘ (↑I.symm : E → H)) x = id x

Tactic:
rcases mem_range.1 hx2 with ⟨y, hy⟩

Premises used: Set.mem_range, Iff.mp
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
m 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
x : E
left : x ∈ (↑I.symm : E → H) ⁻¹' univ
hx2 : x ∈ range (↑I : H → E)
y : H
hy : (↑I : H → E) y = x
rw : ((↑I : H → E) ∘ id ∘ (↑I.symm : E → H)) ((↑I : H → E) y) = id ((↑I : H → E) y)
⊢ ((↑I : H → E) ∘ id ∘ (↑I.symm : E → H)) x = id x

Tactic:
rw [← hy]
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
m 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
x : E
left : x ∈ (↑I.symm : E → H) ⁻¹' univ
hx2 : x ∈ range (↑I : H → E)
y : H
hy : (↑I : H → E) y = x
⊢ ((↑I : H → E) ∘ id ∘ (↑I.symm : E → H)) ((↑I : H → E) y) = id ((↑I : H → E) y)

Tactic:
simp only [mfld_simps]
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
m n : ℕ∞ω
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I : ModelWithCorners 𝕜 E H_1
M : Type u_4
inst_4 : TopologicalSpace M
f : H_1 → H_1
u : Set H_1
h_1 : IsOpen[inst_3] u
H :
  ∀ x ∈ u,
    ∃ (v : Set H_1),
      IsOpen[inst_3] v ∧
        x ∈ v ∧
          ContDiffOn 𝕜 n ((↑I : H_1 → E) ∘ f ∘ (↑I.symm : E → H_1))
            ((↑I.symm : E → H_1) ⁻¹' (u ∩ v) ∩ range (↑I : H_1 → E))
h :
  ∀ x ∈ (↑I.symm : E → H_1) ⁻¹' u ∩ range (↑I : H_1 → E),
    ∃ (u_1 : Set E),
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u_1 ∧
        x ∈ u_1 ∧
          ContDiffOn 𝕜 n ((↑I : H_1 → E) ∘ f ∘ (↑I.symm : E → H_1))
            ((↑I.symm : E → H_1) ⁻¹' u ∩ range (↑I : H_1 → E) ∩ u_1)
⊢ ContDiffOn 𝕜 n ((↑I : H_1 → E) ∘ f ∘ (↑I.symm : E → H_1)) ((↑I.symm : E → H_1) ⁻¹' u ∩ range (↑I : H_1 → E))

Tactic:
apply contDiffOn_of_locally_contDiffOn

Premises used: contDiffOn_of_locally_contDiffOn
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
m n : ℕ∞ω
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I : ModelWithCorners 𝕜 E H_1
M : Type u_4
inst_4 : TopologicalSpace M
f : H_1 → H_1
u : Set H_1
h_1 : IsOpen[inst_3] u
H :
  ∀ x ∈ u,
    ∃ (v : Set H_1),
      IsOpen[inst_3] v ∧
        x ∈ v ∧
          ContDiffOn 𝕜 n ((↑I : H_1 → E) ∘ f ∘ (↑I.symm : E → H_1))
            ((↑I.symm : E → H_1) ⁻¹' (u ∩ v) ∩ range (↑I : H_1 → E))
y : E
hy1 : y ∈ (↑I.symm : E → H_1) ⁻¹' u
hy2 : y ∈ range (↑I : H_1 → E)
h :
  ∀ (x : H_1) (hx : (↑I : H_1 → E) x = y),
    ∃ (u_1 : Set E),
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u_1 ∧
        y ∈ u_1 ∧
          ContDiffOn 𝕜 n ((↑I : H_1 → E) ∘ f ∘ (↑I.symm : E → H_1))
            ((↑I.symm : E → H_1) ⁻¹' u ∩ range (↑I : H_1 → E) ∩ u_1)
⊢ ∃ (u_1 : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u_1 ∧
      y ∈ u_1 ∧
        ContDiffOn 𝕜 n ((↑I : H_1 → E) ∘ f ∘ (↑I.symm : E → H_1))
          ((↑I.symm : E → H_1) ⁻¹' u ∩ range (↑I : H_1 → E) ∩ u_1)

Tactic:
rcases mem_range.1 hy2 with ⟨x, hx⟩

Premises used: Set.mem_range, Iff.mp
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
m n : ℕ∞ω
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I : ModelWithCorners 𝕜 E H_1
M : Type u_4
inst_4 : TopologicalSpace M
f : H_1 → H_1
u : Set H_1
h_1 : IsOpen[inst_3] u
H :
  ∀ x ∈ u,
    ∃ (v : Set H_1),
      IsOpen[inst_3] v ∧
        x ∈ v ∧
          ContDiffOn 𝕜 n ((↑I : H_1 → E) ∘ f ∘ (↑I.symm : E → H_1))
            ((↑I.symm : E → H_1) ⁻¹' (u ∩ v) ∩ range (↑I : H_1 → E))
y : E
hy1 : y ∈ (↑I.symm : E → H_1) ⁻¹' u
hy2 : y ∈ range (↑I : H_1 → E)
x : H_1
hx : (↑I : H_1 → E) x = y
h :
  ∀ (hy1 : (↑I : H_1 → E) x ∈ (↑I.symm : E → H_1) ⁻¹' u) (hx : (↑I : H_1 → E) x = y),
    ∃ (u_1 : Set E),
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u_1 ∧
        (↑I : H_1 → E) x ∈ u_1 ∧
          ContDiffOn 𝕜 n ((↑I : H_1 → E) ∘ f ∘ (↑I.symm : E → H_1))
            ((↑I.symm : E → H_1) ⁻¹' u ∩ range (↑I : H_1 → E) ∩ u_1)
⊢ ∃ (u_1 : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u_1 ∧
      y ∈ u_1 ∧
        ContDiffOn 𝕜 n ((↑I : H_1 → E) ∘ f ∘ (↑I.symm : E → H_1))
          ((↑I.symm : E → H_1) ⁻¹' u ∩ range (↑I : H_1 → E) ∩ u_1)

Tactic:
rw [← hx] at hy1 ⊢