awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
hx : x ∈ e.source
h :
  ContDiffWithinAt 𝕜 m ((↑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 𝕜 n ((↑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))
⊢ ContDiffWithinAt 𝕜 m ((↑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_inter _ (this.of_le hmn)).mono_of_mem_nhdsWithin _ using 1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
hx : x ∈ e.source
h :
  ContDiffWithinAt 𝕜 m ((↑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 𝕜 n ((↑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)
⊢ ContDiffWithinAt 𝕜 m ((↑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_inter _ (this.of_le hmn)).mono_of_mem_nhdsWithin _ using 1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
hx : x ∈ e.source
h :
  ContDiffWithinAt 𝕜 m ((↑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 𝕜 n ((↑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))
⊢ (↑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)
have h₁ : ∀ (y : E),
  ((↑I' : H' → E') ∘ (f ∘ (↑e.symm : H → H)) ∘ (↑I.symm : E → H)) y =
    (((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ∘ (↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H)) y
Tactic: ext y
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
hx : x ∈ e.source
h :
  ContDiffWithinAt 𝕜 m ((↑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 𝕜 n ((↑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))
⊢ (↑I : H → E) ((↑e : H → H) x) ∈ (↑I.symm : E → H) ⁻¹' e.target
have simp_rw : (↑I.symm : E → H) ((↑I : H → E) ((↑e : H → H) x)) ∈ e.target
Tactic: simp_rw [mem_preimage, I.left_inv, e.mapsTo hx]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
hx : x ∈ e.source
h :
  ContDiffWithinAt 𝕜 m ((↑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 𝕜 n ((↑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))
simp_rw : (↑I.symm : E → H) ((↑I : H → E) ((↑e : H → H) x)) ∈ e.target
⊢ (↑I : H → E) ((↑e : H → H) x) ∈ (↑I.symm : E → H) ⁻¹' e.target
have simp_rw₁ : (↑e : H → H) x ∈ e.target
Tactic: simp_rw [mem_preimage, I.left_inv, e.mapsTo hx]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
hx : x ∈ e.source
h :
  ContDiffWithinAt 𝕜 m ((↑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 𝕜 n ((↑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))
⊢ (↑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)
have convert_2 : (↑I.symm : E → H) ⁻¹' e.target ∩ ((↑I.symm : E → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s ∩ range (↑I : H → E)) ⊆
  (↑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))
Tactic: refine mem_nhdsWithin.mpr
      ⟨I.symm ⁻¹' e.target, e.open_target.preimage I.continuous_symm, by
        simp_rw [mem_preimage, I.left_inv, e.mapsTo hx], ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
hx : x ∈ e.source
h :
  ContDiffWithinAt 𝕜 m ((↑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 𝕜 n ((↑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))
⊢ (↑I.symm : E → H) ⁻¹' e.target ∩ ((↑I.symm : E → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s ∩ range (↑I : H → E)) ⊆
    (↑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))
have convert_2 : ∀ ⦃my_y : E⦄,
  my_y ∈ (↑I.symm : E → H) ⁻¹' e.target ∩ ((↑I.symm : E → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s ∩ range (↑I : H → E)) →
    my_y ∈
      (↑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))
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
hx : x ∈ e.source
h :
  ContDiffWithinAt 𝕜 m ((↑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 𝕜 n ((↑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))
convert_2 convert_2₁ convert_2₂ :
  ∀ ⦃my_y : E⦄,
    my_y ∈ (↑I.symm : E → H) ⁻¹' e.target ∩ ((↑I.symm : E → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s ∩ range (↑I : H → E)) →
      my_y ∈
        (↑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.target ∩ ((↑I.symm : E → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s ∩ range (↑I : H → E)) ⊆
    (↑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))
have convert_2₃ : ∀ ⦃my_y : E⦄,
  (↑I.symm : E → H) my_y ∈ e.target ∧ (↑e.symm : H → H) ((↑I.symm : E → H) my_y) ∈ s ∧ my_y ∈ range (↑I : H → E) →
    my_y ∈
      (↑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))
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f g : H → H'
h : ∀ y ∈ s, f y = g y
hx : f x = g x
hf : ContDiffWithinAtProp I I' m f s x
⊢ ContDiffWithinAtProp I I' m g s x
have h₁ : ∀ y ∈ (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E),
  ((↑I' : H' → E') ∘ g ∘ (↑I.symm : E → H)) y = ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) y
Tactic: apply hf.congr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f g : H → H'
h : ∀ y ∈ s, f y = g y
hx : f x = g x
hf : ContDiffWithinAtProp I I' m f s x
h₁ :
  ∀ y ∈ (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E),
    ((↑I' : H' → E') ∘ g ∘ (↑I.symm : E → H)) y = ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) y
⊢ ContDiffWithinAtProp I I' m g s x
have hx₁ : ((↑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: apply hf.congr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f g : H → H'
h : ∀ y ∈ s, f y = g y
hx : f x = g x
hf : ContDiffWithinAtProp I I' m f s x
y : E
hy : y ∈ (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)
⊢ ((↑I' : H' → E') ∘ g ∘ (↑I.symm : E → H)) y = ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) y
have hy₁ : (↑I.symm : E → H) y ∈ s ∧ y ∈ range (↑I : H → E)
Tactic: simp only [mfld_simps] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ contDiffGroupoid n I'
hs : s ⊆ f ⁻¹' e'.source
hx : f x ∈ e'.source
h : ContDiffWithinAtProp I I' m f s x
⊢ ContDiffWithinAtProp I I' m ((↑e' : H' → H') ∘ f) s x
have h₁ : ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
  ((↑I : H → E) x)
Tactic: rw [ContDiffWithinAtProp] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ contDiffGroupoid n I'
hs : s ⊆ f ⁻¹' e'.source
hx : f x ∈ e'.source
h :
  ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I : H → E) x)
⊢ ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ ((↑e' : H' → H') ∘ f) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) x)
have A : ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x) ∈ (↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E')
Tactic: have A : (I' ∘ f ∘ I.symm) (I x) ∈ I'.symm ⁻¹' e'.source ∩ range I' := by
      simp only [hx, mfld_simps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ contDiffGroupoid n I'
hs : s ⊆ f ⁻¹' e'.source
hx : f x ∈ e'.source
h :
  ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I : H → E) x)
A :
  ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x) ∈
    (↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E')
⊢ ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ ((↑e' : H' → H') ∘ f) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) x)
have this : ContDiffWithinAt 𝕜 n ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H'))
  ((↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E'))
  (((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x))
Tactic: have := (mem_groupoid_of_pregroupoid.2 he').1.contDiffWithinAt A
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ contDiffGroupoid n I'
hs : s ⊆ f ⁻¹' e'.source
hx : f x ∈ e'.source
h :
  ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I : H → E) x)
A :
  ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x) ∈
    (↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E')
this :
  ContDiffWithinAt 𝕜 n ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H'))
    ((↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E'))
    (((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x))
⊢ ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ ((↑e' : H' → H') ∘ f) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) x)
have h₁ : (↑I' : H' → E') ∘ ((↑e' : H' → H') ∘ f) ∘ (↑I.symm : E → H) =
  ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H')) ∘ (↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)
Tactic: convert! (this.of_le hmn).comp _ h _
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ contDiffGroupoid n I'
hs : s ⊆ f ⁻¹' e'.source
hx : f x ∈ e'.source
h :
  ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I : H → E) x)
A :
  ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x) ∈
    (↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E')
this :
  ContDiffWithinAt 𝕜 n ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H'))
    ((↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E'))
    (((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x))
h₁ :
  (↑I' : H' → E') ∘ ((↑e' : H' → H') ∘ f) ∘ (↑I.symm : E → H) =
    ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H')) ∘ (↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)
⊢ ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ ((↑e' : H' → H') ∘ f) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) x)
have convert! : MapsTo ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
  ((↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E'))
Tactic: convert! (this.of_le hmn).comp _ h _
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ contDiffGroupoid n I'
hs : s ⊆ f ⁻¹' e'.source
hx : f x ∈ e'.source
h :
  ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I : H → E) x)
A :
  ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x) ∈
    (↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E')
this :
  ContDiffWithinAt 𝕜 n ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H'))
    ((↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E'))
    (((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x))
⊢ (↑I' : H' → E') ∘ ((↑e' : H' → H') ∘ f) ∘ (↑I.symm : E → H) =
    ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H')) ∘ (↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)
have h₁ : ∀ (y : E),
  ((↑I' : H' → E') ∘ ((↑e' : H' → H') ∘ f) ∘ (↑I.symm : E → H)) y =
    (((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H')) ∘ (↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) y
Tactic: ext y