awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H' : Type u_6
inst_5 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
f : E → H'
s : Set E
x : E
simp_rw :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E))
      ((↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) ⁻¹' s ∩ range (↑𝓘(𝕜, E) : E → E)) ((↑𝓘(𝕜, E) : E → E) x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
simp_rw₁ :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E))
      ((↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) ⁻¹' s ∩ range id) (id x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
⊢ DifferentiableWithinAtProp 𝓘(𝕜, E) I' f s x ↔ DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
have simp_rw₂ : DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E))
    ((↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) ⁻¹' s ∩ univ) (id x) ↔
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
Tactic: simp_rw [DifferentiableWithinAtProp, modelWithCornersSelf_coe, range_id, inter_univ,
    modelWithCornersSelf_coe_symm, CompTriple.comp_eq, preimage_id_eq, id_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H' : Type u_6
inst_5 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
f : E → H'
s : Set E
x : E
simp_rw :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E))
      ((↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) ⁻¹' s ∩ range (↑𝓘(𝕜, E) : E → E)) ((↑𝓘(𝕜, E) : E → E) x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
simp_rw₁ :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E))
      ((↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) ⁻¹' s ∩ range id) (id x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
simp_rw₂ :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E))
      ((↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) ⁻¹' s ∩ univ) (id x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
⊢ DifferentiableWithinAtProp 𝓘(𝕜, E) I' f s x ↔ DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
have simp_rw₃ : DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E))
    ((↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) ⁻¹' s) (id x) ↔
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
Tactic: simp_rw [DifferentiableWithinAtProp, modelWithCornersSelf_coe, range_id, inter_univ,
    modelWithCornersSelf_coe_symm, CompTriple.comp_eq, preimage_id_eq, id_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H' : Type u_6
inst_5 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
f : E → H'
s : Set E
x : E
simp_rw :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E))
      ((↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) ⁻¹' s ∩ range (↑𝓘(𝕜, E) : E → E)) ((↑𝓘(𝕜, E) : E → E) x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
simp_rw₁ :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E))
      ((↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) ⁻¹' s ∩ range id) (id x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
simp_rw₂ :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E))
      ((↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) ⁻¹' s ∩ univ) (id x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
simp_rw₃ :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E))
      ((↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) ⁻¹' s) (id x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
⊢ DifferentiableWithinAtProp 𝓘(𝕜, E) I' f s x ↔ DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
have simp_rw₄ : DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ id) (id ⁻¹' s) (id x) ↔
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
Tactic: simp_rw [DifferentiableWithinAtProp, modelWithCornersSelf_coe, range_id, inter_univ,
    modelWithCornersSelf_coe_symm, CompTriple.comp_eq, preimage_id_eq, id_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H' : Type u_6
inst_5 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
f : E → H'
s : Set E
x : E
simp_rw :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E))
      ((↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) ⁻¹' s ∩ range (↑𝓘(𝕜, E) : E → E)) ((↑𝓘(𝕜, E) : E → E) x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
simp_rw₁ :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E))
      ((↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) ⁻¹' s ∩ range id) (id x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
simp_rw₂ :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E))
      ((↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) ⁻¹' s ∩ univ) (id x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
simp_rw₃ :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E))
      ((↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) ⁻¹' s) (id x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
simp_rw₄ :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ id) (id ⁻¹' s) (id x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
⊢ DifferentiableWithinAtProp 𝓘(𝕜, E) I' f s x ↔ DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
have simp_rw₅ : DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) (id ⁻¹' s) (id x) ↔ DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
Tactic: simp_rw [DifferentiableWithinAtProp, modelWithCornersSelf_coe, range_id, inter_univ,
    modelWithCornersSelf_coe_symm, CompTriple.comp_eq, preimage_id_eq, id_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H' : Type u_6
inst_5 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
f : E → H'
s : Set E
x : E
simp_rw :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E))
      ((↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) ⁻¹' s ∩ range (↑𝓘(𝕜, E) : E → E)) ((↑𝓘(𝕜, E) : E → E) x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
simp_rw₁ :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E))
      ((↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) ⁻¹' s ∩ range id) (id x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
simp_rw₂ :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E))
      ((↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) ⁻¹' s ∩ univ) (id x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
simp_rw₃ :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E))
      ((↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) ⁻¹' s) (id x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
simp_rw₄ :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ id) (id ⁻¹' s) (id x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
simp_rw₅ :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) (id ⁻¹' s) (id x) ↔ DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
⊢ DifferentiableWithinAtProp 𝓘(𝕜, E) I' f s x ↔ DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
have simp_rw₆ : DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) (id s) (id x) ↔ DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
Tactic: simp_rw [DifferentiableWithinAtProp, modelWithCornersSelf_coe, range_id, inter_univ,
    modelWithCornersSelf_coe_symm, CompTriple.comp_eq, preimage_id_eq, id_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Defs (hypothesis)
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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst_3] u
xu : x ∈ u
⊢ DifferentiableWithinAtProp I I' f s x ↔ DifferentiableWithinAtProp I I' f (s ∩ u) x
have this : (↑I.symm : E → H) ⁻¹' (s ∩ u) ∩ range (↑I : H → E) =
  (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u
Tactic: have : I.symm ⁻¹' (s ∩ u) ∩ Set.range I = I.symm ⁻¹' s ∩ Set.range I ∩ I.symm ⁻¹' u := by
        simp only [Set.inter_right_comm, Set.preimage_inter]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Defs (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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst_3] u
xu : x ∈ u
this :
  (↑I.symm : E → H) ⁻¹' (s ∩ u) ∩ range (↑I : H → E) =
    (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u
⊢ DifferentiableWithinAtProp I I' f s x ↔ DifferentiableWithinAtProp I I' f (s ∩ u) x
have rw : DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I : H → E) x) ↔
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u) ((↑I : H → E) x)
Tactic: rw [DifferentiableWithinAtProp, DifferentiableWithinAtProp, this]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Defs (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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst_3] u
xu : x ∈ u
this :
  (↑I.symm : E → H) ⁻¹' (s ∩ u) ∩ range (↑I : H → E) =
    (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u
⊢ DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
      ((↑I : H → E) x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H))
      ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u) ((↑I : H → E) x)
have symm : DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u) ((↑I : H → E) x) ↔
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I : H → E) x)
Tactic: symm
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Defs (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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst_3] u
xu : x ∈ u
this :
  (↑I.symm : E → H) ⁻¹' (s ∩ u) ∩ range (↑I : H → E) =
    (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u
⊢ DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H))
      ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u) ((↑I : H → E) x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
      ((↑I : H → E) x)
have ht : (↑I.symm : E → H) ⁻¹' u ∈ 𝓝 ((↑I : H → E) x)
Tactic: apply differentiableWithinAt_inter
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Defs (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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst_3] u
xu : x ∈ u
this :
  (↑I.symm : E → H) ⁻¹' (s ∩ u) ∩ range (↑I : H → E) =
    (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u
⊢ u ∈ 𝓝 ((↑I.symm : E → H) ((↑I : H → E) x))
have rw : u ∈ 𝓝 x
Tactic: rw [ModelWithCorners.left_inv]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Defs (hypothesis)
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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
u : Set H
f : H → H'
u_open : IsOpen[inst_3] u
xu : x ∈ u
this :
  (↑I.symm : E → H) ⁻¹' (s ∩ u) ∩ range (↑I : H → E) =
    (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' u
⊢ (↑I.symm : E → H) ⁻¹' u ∈ 𝓝 ((↑I : H → E) x)
have this₁ : u ∈ 𝓝 ((↑I.symm : E → H) ((↑I : H → E) x))
Tactic: have : u ∈ 𝓝 (I.symm (I x)) := by
        rw [ModelWithCorners.left_inv]
        exact u_open.mem_nhds xu
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Defs (hypothesis)
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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid 1 I
hx : x ∈ e.source
h : DifferentiableWithinAtProp I I' f s x
⊢ DifferentiableWithinAtProp I I' (f ∘ (↑e.symm : H → H)) ((↑e.symm : H → H) ⁻¹' s) ((↑e : H → H) x)
have h₁ : DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
  ((↑I : H → E) x)
Tactic: rw [DifferentiableWithinAtProp] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Defs (hypothesis)
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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid 1 I
hx : x ∈ e.source
h :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I : H → E) x)
⊢ DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ (f ∘ (↑e.symm : H → H)) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) ((↑e : H → H) x))
have this : (↑I : H → E) x = ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x))
Tactic: have : I x = (I ∘ e.symm ∘ I.symm) (I (e x)) := by simp only [hx, mfld_simps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Defs (hypothesis)
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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid 1 I
hx : x ∈ e.source
h :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I : H → E) x)
this : (↑I : H → E) x = ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x))
⊢ DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ (f ∘ (↑e.symm : H → H)) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) ((↑e : H → H) x))
have h₁ : DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
  (((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x)))
Tactic: rw [this] at h
Cleared hypotheses: h, this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Defs (hypothesis)
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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid 1 I
hx : x ∈ e.source
h :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    (((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x)))
this : (↑I : H → E) x = ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x))
⊢ DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ (f ∘ (↑e.symm : H → H)) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) ((↑e : H → H) x))
have this₁ : (↑I : H → E) ((↑e : H → H) x) ∈ (↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E)
Tactic: have : I (e x) ∈ I.symm ⁻¹' e.target ∩ Set.range I := by simp only [hx, mfld_simps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Defs (hypothesis)
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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid 1 I
hx : x ∈ e.source
h :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    (((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x)))
this_1 : (↑I : H → E) x = ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x))
this : (↑I : H → E) ((↑e : H → H) x) ∈ (↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E)
⊢ DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ (f ∘ (↑e.symm : H → H)) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) ((↑e : H → H) x))
have this₁ : ContDiffWithinAt 𝕜 1 ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H))
  ((↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E)) ((↑I : H → E) ((↑e : H → H) x))
Tactic: have := (mem_groupoid_of_pregroupoid.2 he).2.contDiffWithinAt this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Defs (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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid 1 I
hx : x ∈ e.source
h :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    (((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x)))
this_1 : (↑I : H → E) x = ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x))
this_2 : (↑I : H → E) ((↑e : H → H) x) ∈ (↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E)
this :
  ContDiffWithinAt 𝕜 1 ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E)) ((↑I : H → E) ((↑e : H → H) x))
⊢ DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ (f ∘ (↑e.symm : H → H)) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) ((↑e : H → H) x))
have h₁ : (↑I' : H' → E') ∘ (f ∘ (↑e.symm : H → H)) ∘ (↑I.symm : E → H) =
  ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ∘ (↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)
Tactic: convert! (h.comp' _ (this.differentiableWithinAt one_ne_zero)).mono_of_mem_nhdsWithin _
        using 1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Defs (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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid 1 I
hx : x ∈ e.source
h :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    (((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x)))
this_1 : (↑I : H → E) x = ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) ((↑I : H → E) ((↑e : H → H) x))
this_2 : (↑I : H → E) ((↑e : H → H) x) ∈ (↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E)
this :
  ContDiffWithinAt 𝕜 1 ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E)) ((↑I : H → E) ((↑e : H → H) x))
h₁ :
  (↑I' : H' → E') ∘ (f ∘ (↑e.symm : H → H)) ∘ (↑I.symm : E → H) =
    ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ∘ (↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)
⊢ DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ (f ∘ (↑e.symm : H → H)) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) ((↑e : H → H) x))
have convert_2 : (↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E) ∩
    (↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H) ⁻¹' ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ∈
  𝓝[(↑I.symm : E → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s ∩ range (↑I : H → E)] (↑I : H → E) ((↑e : H → H) x)
Tactic: convert! (h.comp' _ (this.differentiableWithinAt one_ne_zero)).mono_of_mem_nhdsWithin _
        using 1