awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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
hy2 : y ∈ range (↑I : H_1 → E)
x : H_1
hy1 : (↑I : H_1 → E) x ∈ (↑I.symm : E → H_1) ⁻¹' u
hx : (↑I : H_1 → E) x = y
⊢ x ∈ u

Tactic:
simp only [mfld_simps] at hy1 ⊢
-- 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
hy2 : y ∈ range (↑I : H_1 → E)
x : H_1
hx : (↑I : H_1 → E) x = y
hy1 : x ∈ u
h :
  ∀ (v : Set H_1) (v_open : IsOpen[inst_3] v) (xv : x ∈ v)
    (hv :
      ContDiffOn 𝕜 n ((↑I : H_1 → E) ∘ f ∘ (↑I.symm : E → H_1))
        ((↑I.symm : E → H_1) ⁻¹' (u ∩ v) ∩ range (↑I : H_1 → E))),
    ∃ (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 ∧
      (↑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)

Tactic:
rcases H x hy1 with ⟨v, v_open, xv, hv⟩
-- 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 : 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
hy2 : y ∈ range (↑I : H_1 → E)
x : H_1
hx : (↑I : H_1 → E) x = y
hy1 : x ∈ u
v : Set H_1
v_open : IsOpen[inst_3] v
xv : x ∈ v
hv : ContDiffOn 𝕜 n ((↑I : H_1 → E) ∘ f ∘ (↑I.symm : E → H_1)) ((↑I.symm : E → H_1) ⁻¹' (u ∩ v) ∩ range (↑I : H_1 → E))
rw :
  (↑I.symm : E → H_1) ⁻¹' u ∩ ((↑I.symm : E → H_1) ⁻¹' v ∩ range (↑I : H_1 → E)) =
    (↑I.symm : E → H_1) ⁻¹' u ∩ (range (↑I : H_1 → E) ∩ (↑I.symm : E → H_1) ⁻¹' v)
⊢ (↑I.symm : E → H_1) ⁻¹' (u ∩ v) ∩ range (↑I : H_1 → E) =
    (↑I.symm : E → H_1) ⁻¹' u ∩ range (↑I : H_1 → E) ∩ (↑I.symm : E → H_1) ⁻¹' v

Tactic:
rw [preimage_inter, inter_assoc, inter_assoc]

Premises used: Set.preimage_inter, Set.inter_assoc
-- 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 : 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
hy2 : y ∈ range (↑I : H_1 → E)
x : H_1
hx : (↑I : H_1 → E) x = y
hy1 : x ∈ u
v : Set H_1
v_open : IsOpen[inst_3] v
xv : x ∈ v
hv : ContDiffOn 𝕜 n ((↑I : H_1 → E) ∘ f ∘ (↑I.symm : E → H_1)) ((↑I.symm : E → H_1) ⁻¹' (u ∩ v) ∩ range (↑I : H_1 → E))
e_a : (↑I.symm : E → H_1) ⁻¹' v ∩ range (↑I : H_1 → E) = range (↑I : H_1 → E) ∩ (↑I.symm : E → H_1) ⁻¹' v
⊢ (↑I.symm : E → H_1) ⁻¹' u ∩ ((↑I.symm : E → H_1) ⁻¹' v ∩ range (↑I : H_1 → E)) =
    (↑I.symm : E → H_1) ⁻¹' u ∩ (range (↑I : H_1 → E) ∩ (↑I.symm : E → H_1) ⁻¹' v)

Tactic:
congr 1
-- 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 : 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
hy2 : y ∈ range (↑I : H_1 → E)
x : H_1
hx : (↑I : H_1 → E) x = y
hy1 : x ∈ u
v : Set H_1
v_open : IsOpen[inst_3] v
xv : x ∈ v
hv : ContDiffOn 𝕜 n ((↑I : H_1 → E) ∘ f ∘ (↑I.symm : E → H_1)) ((↑I.symm : E → H_1) ⁻¹' (u ∩ v) ∩ range (↑I : H_1 → E))
e_a e_a₁ : range (↑I : H_1 → E) ∩ (↑I.symm : E → H_1) ⁻¹' v = range (↑I : H_1 → E) ∩ (↑I.symm : E → H_1) ⁻¹' v
⊢ (↑I.symm : E → H_1) ⁻¹' v ∩ range (↑I : H_1 → E) = range (↑I : H_1 → E) ∩ (↑I.symm : E → H_1) ⁻¹' v

Tactic:
rw [inter_comm]

Premises used: Set.inter_comm
-- 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 : 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
hy2 : y ∈ range (↑I : H_1 → E)
x : H_1
hx : (↑I : H_1 → E) x = y
hy1 : x ∈ u
v : Set H_1
v_open : IsOpen[inst_3] v
xv : x ∈ v
hv : ContDiffOn 𝕜 n ((↑I : H_1 → E) ∘ f ∘ (↑I.symm : E → H_1)) ((↑I.symm : E → H_1) ⁻¹' (u ∩ v) ∩ range (↑I : H_1 → E))
⊢ (↑I.symm : E → H_1) ⁻¹' (u ∩ v) ∩ range (↑I : H_1 → E) =
    (↑I.symm : E → H_1) ⁻¹' u ∩ range (↑I : H_1 → E) ∩ (↑I.symm : E → H_1) ⁻¹' v

Tactic:
have : I.symm ⁻¹' (u ∩ v) ∩ range I = I.symm ⁻¹' u ∩ range I ∩ I.symm ⁻¹' v := by
      rw [preimage_inter, inter_assoc, inter_assoc]
      congr 1
      rw [inter_comm]
-- 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 : 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
hy2 : y ∈ range (↑I : H_1 → E)
x : H_1
hx : (↑I : H_1 → E) x = y
hy1 : x ∈ u
v : Set H_1
v_open : IsOpen[inst_3] v
xv : x ∈ v
hv : ContDiffOn 𝕜 n ((↑I : H_1 → E) ∘ f ∘ (↑I.symm : E → H_1)) ((↑I.symm : E → H_1) ⁻¹' (u ∩ v) ∩ range (↑I : H_1 → E))
this :
  (↑I.symm : E → H_1) ⁻¹' (u ∩ v) ∩ range (↑I : H_1 → E) =
    (↑I.symm : E → H_1) ⁻¹' u ∩ range (↑I : H_1 → E) ∩ (↑I.symm : E → H_1) ⁻¹' v
⊢ ContDiffOn 𝕜 n ((↑I : H_1 → E) ∘ f ∘ (↑I.symm : E → H_1))
    ((↑I.symm : E → H_1) ⁻¹' u ∩ range (↑I : H_1 → E) ∩ (↑I.symm : E → H_1) ⁻¹' v)

Tactic:
rw [this] at hv
-- 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 : 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
hy2 : y ∈ range (↑I : H_1 → E)
x : H_1
hx : (↑I : H_1 → E) x = y
hy1 : x ∈ u
v : Set H_1
v_open : IsOpen[inst_3] v
xv : x ∈ v
hv : ContDiffOn 𝕜 n ((↑I : H_1 → E) ∘ f ∘ (↑I.symm : E → H_1)) ((↑I.symm : E → H_1) ⁻¹' (u ∩ v) ∩ range (↑I : H_1 → E))
this :
  (↑I.symm : E → H_1) ⁻¹' (u ∩ v) ∩ range (↑I : H_1 → E) =
    (↑I.symm : E → H_1) ⁻¹' u ∩ range (↑I : H_1 → E) ∩ (↑I.symm : E → H_1) ⁻¹' v
hv₁ :
  ContDiffOn 𝕜 n ((↑I : H_1 → E) ∘ f ∘ (↑I.symm : E → H_1))
    ((↑I.symm : E → H_1) ⁻¹' u ∩ range (↑I : H_1 → E) ∩ (↑I.symm : E → H_1) ⁻¹' v)
⊢ (↑I.symm : E → H_1) ⁻¹' (u ∩ v) ∩ range (↑I : H_1 → E) =
    (↑I.symm : E → H_1) ⁻¹' u ∩ range (↑I : H_1 → E) ∩ (↑I.symm : E → H_1) ⁻¹' v

Tactic:
rw [this] at hv
-- 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 : 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
hy2 : y ∈ range (↑I : H_1 → E)
x : H_1
hx : (↑I : H_1 → E) x = y
hy1 : x ∈ u
v : Set H_1
v_open : IsOpen[inst_3] v
xv : x ∈ v
hv :
  ContDiffOn 𝕜 n ((↑I : H_1 → E) ∘ f ∘ (↑I.symm : E → H_1))
    ((↑I.symm : E → H_1) ⁻¹' u ∩ range (↑I : H_1 → E) ∩ (↑I.symm : E → H_1) ⁻¹' v)
this :
  (↑I.symm : E → H_1) ⁻¹' (u ∩ v) ∩ range (↑I : H_1 → E) =
    (↑I.symm : E → H_1) ⁻¹' u ∩ range (↑I : H_1 → E) ∩ (↑I.symm : E → H_1) ⁻¹' v
⊢ (↑I : H_1 → E) x ∈ (↑I.symm : E → H_1) ⁻¹' v

Tactic:
simpa
-- 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 : 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
hy2 : y ∈ range (↑I : H_1 → E)
x : H_1
hx : (↑I : H_1 → E) x = y
hy1 : x ∈ u
v : Set H_1
v_open : IsOpen[inst_3] v
xv : x ∈ v
hv :
  ContDiffOn 𝕜 n ((↑I : H_1 → E) ∘ f ∘ (↑I.symm : E → H_1))
    ((↑I.symm : E → H_1) ⁻¹' u ∩ range (↑I : H_1 → E) ∩ (↑I.symm : E → H_1) ⁻¹' v)
this :
  (↑I.symm : E → H_1) ⁻¹' (u ∩ v) ∩ range (↑I : H_1 → E) =
    (↑I.symm : E → H_1) ⁻¹' u ∩ range (↑I : H_1 → E) ∩ (↑I.symm : E → H_1) ⁻¹' v
⊢ ∃ (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)

Tactic:
exact ⟨I.symm ⁻¹' v, v_open.preimage I.continuous_symm, by simpa, hv⟩
-- 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 : Set H
h : IsOpen[inst_3] u
fg : ∀ x ∈ u, g x = f x
hf : ContDiffOn 𝕜 n ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' u ∩ range (↑I : H → E))
apply :
  ∀ x ∈ (↑I.symm : E → H) ⁻¹' u ∩ range (↑I : H → E),
    ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) x = ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) x
⊢ ContDiffOn 𝕜 n ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' u ∩ range (↑I : H → E))

Tactic:
apply hf.congr

Premises used: ContDiffOn.congr
-- 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 : Set H
h : IsOpen[inst_3] u
fg : ∀ x ∈ u, g x = f x
hf : ContDiffOn 𝕜 n ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' u ∩ range (↑I : H → E))
y : E
hy1 : y ∈ (↑I.symm : E → H) ⁻¹' u
hy2 : y ∈ range (↑I : H → E)
rcases :
  ∀ (x : H) (hx : (↑I : H → E) x = y),
    ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) y = ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) y
⊢ ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) y = ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) y

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 : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
f g : H → H
u : Set H
h : IsOpen[inst_3] u
fg : ∀ x ∈ u, g x = f x
hf : ContDiffOn 𝕜 n ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' u ∩ range (↑I : H → E))
y : E
hy1 : y ∈ (↑I.symm : E → H) ⁻¹' u
hy2 : y ∈ range (↑I : H → E)
x : H
hx : (↑I : H → E) x = y
rw :
  ∀ (hy1 : (↑I : H → E) x ∈ (↑I.symm : E → H) ⁻¹' u) (hx : (↑I : H → E) x = y),
    ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ((↑I : H → E) x) = ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x)
⊢ ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) y = ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) y

Tactic:
rw [← hx] at hy1 ⊢
-- 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 : Set H
h : IsOpen[inst_3] u
fg : ∀ x ∈ u, g x = f x
hf : ContDiffOn 𝕜 n ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' u ∩ range (↑I : H → E))
y : E
hy2 : y ∈ range (↑I : H → E)
x : H
hy1 : (↑I : H → E) x ∈ (↑I.symm : E → H) ⁻¹' u
hx : (↑I : H → E) x = y
simp : ∀ (hy1 : x ∈ u), (↑I : H → E) (g x) = (↑I : H → E) (f x)
⊢ ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ((↑I : H → E) x) = ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x)

Tactic:
simp only [mfld_simps] at hy1 ⊢
-- 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 : Set H
h : IsOpen[inst_3] u
fg : ∀ x ∈ u, g x = f x
hf : ContDiffOn 𝕜 n ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' u ∩ range (↑I : H → E))
y : E
hy2 : y ∈ range (↑I : H → E)
x : H
hx : (↑I : H → E) x = y
hy1 : x ∈ u
rw rw₁ : (↑I : H → E) (f x) = (↑I : H → E) (f x)
⊢ (↑I : H → E) (g x) = (↑I : H → E) (f x)

Tactic:
rw [fg _ hy1]
-- 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
h : m ≤ n
h₁ : ∀ (f : H → H) (s : Set H), (contDiffPregroupoid n I).property f s → (contDiffPregroupoid m I).property f s
⊢ (contDiffPregroupoid n I).groupoid ≤ (contDiffPregroupoid m I).groupoid

Tactic:
apply groupoid_of_pregroupoid_le

Premises used: groupoid_of_pregroupoid_le
-- 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
h : m ≤ n
f : H → H
s : Set H
hfs : (contDiffPregroupoid n I).property f s
⊢ (contDiffPregroupoid m I).property f s

Tactic:
ContDiffOn.of_le hfs h

Premises used: ContDiffOn, ContDiffOn.of_le
-- 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
h : m ≤ n
f : H → H
s : Set H
hfs : (contDiffPregroupoid n I).property f s
⊢ (contDiffPregroupoid m I).property f s

Tactic:
exact ContDiffOn.of_le hfs h

Premises used: ContDiffOn.of_le
-- 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
apply : ⊤ ≤ contDiffGroupoid 0 I
⊢ contDiffGroupoid 0 I = continuousGroupoid H

Tactic:
apply le_antisymm le_top

Premises used: le_antisymm, le_top
-- 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
_ :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (StructureGroupoid.members ⊤) u →
    u ∈ (contDiffGroupoid 0 I).members
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (StructureGroupoid.members ⊤) u →
    u ∈ (contDiffGroupoid 0 I).members

Tactic:
_
-- 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
simp :
  ContinuousOn ((↑I : H → E) ∘ (↑u : H → H) ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' u.source ∩ range (↑I : H → E)) ∧
    ContinuousOn ((↑I : H → E) ∘ (↑u.symm : H → H) ∘ (↑I.symm : E → H))
      ((↑I.symm : E → H) ⁻¹' u.target ∩ range (↑I : H → E))
⊢ Pregroupoid.property
      {
        property := fun (f : H → H) (s : Set H) ↦
          ContDiffOn 𝕜 0 ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)),
        comp := ⋯, id_mem := ⋯, locality := ⋯, congr := ⋯ }
      (↑u : H → H) u.source ∧
    Pregroupoid.property
      {
        property := fun (f : H → H) (s : Set H) ↦
          ContDiffOn 𝕜 0 ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)),
        comp := ⋯, id_mem := ⋯, locality := ⋯, congr := ⋯ }
      (↑u.symm : H → H) u.target

Tactic:
simp only [contDiffOn_zero]

Premises used: contDiffOn_zero
-- 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
left :
  ContinuousOn ((↑I : H → E) ∘ (↑u : H → H) ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' u.source ∩ range (↑I : H → E))
right :
  ContinuousOn ((↑I : H → E) ∘ (↑u.symm : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' u.target ∩ range (↑I : H → E))
⊢ ContinuousOn ((↑I : H → E) ∘ (↑u : H → H) ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' u.source ∩ range (↑I : H → E)) ∧
    ContinuousOn ((↑I : H → E) ∘ (↑u.symm : H → H) ∘ (↑I.symm : E → H))
      ((↑I.symm : E → H) ⁻¹' u.target ∩ range (↑I : H → E))

Tactic:
constructor
-- 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
⊢ ContinuousOn ((↑I : H → E) ∘ (↑u : H → H) ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' u.source ∩ range (↑I : H → E))

Tactic:
I.continuous.comp_continuousOn (u.continuousOn.comp I.continuousOn_symm ?_)

Premises used: Continuous.comp_continuousOn, ContinuousOn.comp, ModelWithCorners.continuousOn_symm, ModelWithCorners.continuous, OpenPartialHomeomorph.continuousOn
-- 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
left : MapsTo (↑I.symm : E → H) ((↑I.symm : E → H) ⁻¹' u.source ∩ range (↑I : H → E)) u.source
⊢ ContinuousOn ((↑I : H → E) ∘ (↑u : H → H) ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' u.source ∩ range (↑I : H → E))

Tactic:
refine I.continuous.comp_continuousOn (u.continuousOn.comp I.continuousOn_symm ?_)

Premises used: Continuous.comp_continuousOn, ContinuousOn.comp, ModelWithCorners.continuousOn_symm, ModelWithCorners.continuous, OpenPartialHomeomorph.continuousOn
-- 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.source ∩ range (↑I : H → E)) u.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.source ∩ range (↑I : H → E)) u.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:
𝕜 : 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
⊢ ContinuousOn ((↑I : H → E) ∘ (↑u.symm : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' u.target ∩ range (↑I : H → E))

Tactic:
I.continuous.comp_continuousOn (u.symm.continuousOn.comp I.continuousOn_symm ?_)

Premises used: Continuous.comp_continuousOn, ContinuousOn.comp, ModelWithCorners.continuousOn_symm, ModelWithCorners.continuous, OpenPartialHomeomorph.continuousOn, OpenPartialHomeomorph.symm
-- 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
right : MapsTo (↑I.symm : E → H) ((↑I.symm : E → H) ⁻¹' u.target ∩ range (↑I : H → E)) u.symm.source
⊢ ContinuousOn ((↑I : H → E) ∘ (↑u.symm : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' u.target ∩ range (↑I : H → E))

Tactic:
refine I.continuous.comp_continuousOn (u.symm.continuousOn.comp I.continuousOn_symm ?_)

Premises used: Continuous.comp_continuousOn, ContinuousOn.comp, ModelWithCorners.continuousOn_symm, ModelWithCorners.continuous, OpenPartialHomeomorph.continuousOn, OpenPartialHomeomorph.symm