awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
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
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
⊢ ∃ (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)
have 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)
Tactic: rw [← hx] at hy1 ⊢
Cleared hypotheses: hy1, hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (hypothesis)
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
⊢ ∃ (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)
have hy1₁ : x ∈ u
Tactic: simp only [mfld_simps] at hy1 ⊢
Cleared hypotheses: hy1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
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
⊢ ∃ (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)
have 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)
Tactic: rcases H x hy1 with ⟨v, v_open, xv, hv⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
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
have 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)
Tactic: rw [preimage_inter, inter_assoc, inter_assoc]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
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 ∩ ((↑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)
have e_a : (↑I.symm : E → H_1) ⁻¹' v ∩ range (↑I : H_1 → E) = range (↑I : H_1 → E) ∩ (↑I.symm : E → H_1) ⁻¹' v
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
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) ⁻¹' v ∩ range (↑I : H_1 → E) = range (↑I : H_1 → E) ∩ (↑I.symm : E → H_1) ⁻¹' v
have e_a : range (↑I : H_1 → E) ∩ (↑I.symm : E → H_1) ⁻¹' v = range (↑I : H_1 → E) ∩ (↑I.symm : E → H_1) ⁻¹' v
Tactic: rw [inter_comm]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (hypothesis)
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))
⊢ ∃ (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)
have 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
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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (hypothesis)
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
⊢ ∃ (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)
have 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)
Tactic: rw [this] at hv
Cleared hypotheses: hv, this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
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))
⊢ ContDiffOn 𝕜 n ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' u ∩ range (↑I : H → E))
have 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
Tactic: apply hf.congr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
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)
⊢ ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) y = ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) y
have 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
Tactic: rcases mem_range.1 hy2 with ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
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
⊢ ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) y = ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) y
have 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)
Tactic: rw [← hx] at hy1 ⊢
Cleared hypotheses: hy1, hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
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
⊢ ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ((↑I : H → E) x) = ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x)
have simp : ∀ (hy1 : x ∈ u), (↑I : H → E) (g x) = (↑I : H → E) (f x)
Tactic: simp only [mfld_simps] at hy1 ⊢
Cleared hypotheses: hy1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
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
⊢ (↑I : H → E) (g x) = (↑I : H → E) (f x)
have rw : (↑I : H → E) (f x) = (↑I : H → E) (f x)
Tactic: rw [fg _ hy1]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
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
⊢ (contDiffPregroupoid n I).groupoid ≤ (contDiffPregroupoid m I).groupoid
have h₁ : ∀ (f : H → H) (s : Set H), (contDiffPregroupoid n I).property f s → (contDiffPregroupoid m I).property f s
Tactic: apply groupoid_of_pregroupoid_le
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
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
⊢ contDiffGroupoid 0 I = continuousGroupoid H
have apply : ⊤ ≤ contDiffGroupoid 0 I
Tactic: apply le_antisymm le_top
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
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
⊢ 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
have 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))
Tactic: simp only [contDiffOn_zero]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
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)) ∧
    ContinuousOn ((↑I : H → E) ∘ (↑u.symm : H → H) ∘ (↑I.symm : E → H))
      ((↑I.symm : E → H) ⁻¹' u.target ∩ range (↑I : H → E))
have left : ContinuousOn ((↑I : H → E) ∘ (↑u : H → H) ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' u.source ∩ range (↑I : H → E))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
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))
⊢ 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))
have right : ContinuousOn ((↑I : H → E) ∘ (↑u.symm : H → H) ∘ (↑I.symm : E → H))
  ((↑I.symm : E → H) ⁻¹' u.target ∩ range (↑I : H → E))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
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))
have left : MapsTo (↑I.symm : E → H) ((↑I.symm : E → H) ⁻¹' u.source ∩ range (↑I : H → E)) u.source
Tactic: refine I.continuous.comp_continuousOn (u.continuousOn.comp I.continuousOn_symm ?_)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
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))
have right : MapsTo (↑I.symm : E → H) ((↑I.symm : E → H) ⁻¹' u.target ∩ range (↑I : H → E)) u.symm.source
Tactic: refine I.continuous.comp_continuousOn (u.symm.continuousOn.comp I.continuousOn_symm ?_)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
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 = ∅
⊢ f ∈ contDiffGroupoid n I
have left : (contDiffPregroupoid n I).property (↑f : H → H) f.source
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
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
⊢ f ∈ contDiffGroupoid n I
have right : (contDiffPregroupoid n I).property (↑f.symm : H → H) f.target
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
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
⊢ 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
have 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
Tactic: ⟨hx, _⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (hypothesis)
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)
⊢ ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑f : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' f.source ∩ range (↑I : H → E)) x
have hx₁ : (↑I.symm : E → H) x ∈ f.source
Tactic: rw [mem_preimage] at hx
Cleared hypotheses: hx, right
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
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
⊢ 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
have 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
Tactic: ⟨hx, _⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (hypothesis)
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)
⊢ ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑f.symm : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' f.target ∩ range (↑I : H → E)) x
have this : f.target = ∅
Tactic: have : f.target = ∅ := by simp [← f.image_source_eq_target, hf]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
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 = ∅
⊢ Membership.mem (γ := StructureGroupoid H) (continuousGroupoid H) f
have rw : f ∈ contDiffGroupoid 0 I
Tactic: rw [← contDiffGroupoid_zero_eq (I := I)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
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
⊢ (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
have suffices : ContDiffOn 𝕜 n ((↑I : H → E) ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
Tactic: suffices h : ContDiffOn 𝕜 n (I ∘ I.symm) (I.symm ⁻¹' s ∩ range I) by
    simp [h, contDiffPregroupoid]