awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.MFDeriv.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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
X : TangentSpace I x
⊢ Eq (α :=
    TangentSpace I'
      (TotalSpace.proj (E := TangentSpace I') (tangentMapWithin I I' f s (TotalSpace.mk (E := TangentSpace I) x X))))
    (TotalSpace.snd (E := TangentSpace I') (tangentMapWithin I I' f s (TotalSpace.mk (E := TangentSpace I) x X)))
    (((mfderivWithin I I' f s x :
          ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))) :
        (a : TangentSpace I x) → TangentSpace I' (f x))
      X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.MFDeriv.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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
p : TangentBundle I M
⊢ TotalSpace.proj (E := TangentSpace I') (tangentMap I I' f p) = f (p.proj (E := TangentSpace I))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.MFDeriv.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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
X : TangentSpace I x
⊢ Eq (α :=
    TangentSpace I'
      (TotalSpace.proj (E := TangentSpace I') (tangentMap I I' f (TotalSpace.mk (E := TangentSpace I) x X))))
    (TotalSpace.snd (E := TangentSpace I') (tangentMap I I' f (TotalSpace.mk (E := TangentSpace I) x X)))
    (((mfderiv I I' f x :
          ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))) :
        (a : TangentSpace I x) → TangentSpace I' (f x))
      X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.MFDeriv.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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ T1Space M

Tactic:
have : T1Space M := I.t1Space M
-- Module: Mathlib.Geometry.Manifold.MFDeriv.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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
⊢ ∃ u ∈ 𝓝 x, u ∩ {x}ᶜ ⊆ {y : M | (y ∈ s) = (y ∈ t)}

Tactic:
mem_nhdsWithin_iff_exists_mem_nhds_inter.1 (nhdsWithin_compl_singleton_le x y h)

Premises used: nhdsWithin_compl_singleton_le, Iff.mp, mem_nhdsWithin_iff_exists_mem_nhds_inter
-- Module: Mathlib.Geometry.Manifold.MFDeriv.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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
obtain :
  ∀ (u : Set M) (u_mem : u ∈ 𝓝 x) (hu : u ∩ {x}ᶜ ⊆ {y : M | (y ∈ s) = (y ∈ t)}),
    (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) =ᶠ[𝓝[≠] (↑(extChartAt I x) : M → E) x]
      (↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)
⊢ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) =ᶠ[𝓝[≠] (↑(extChartAt I x) : M → E) x]
    (↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)

Tactic:
obtain ⟨u, u_mem, hu⟩ : ∃ u ∈ 𝓝 x, u ∩ {x}ᶜ ⊆ {y | (y ∈ s) = (y ∈ t)} :=
    mem_nhdsWithin_iff_exists_mem_nhds_inter.1 (nhdsWithin_compl_singleton_le x y h)

Premises used: nhdsWithin_compl_singleton_le, Membership.mem, nhds, Iff.mp, mem_nhdsWithin_iff_exists_mem_nhds_inter
-- Module: Mathlib.Geometry.Manifold.MFDeriv.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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 x
hu : u ∩ {x}ᶜ ⊆ {y : M | (y ∈ s) = (y ∈ t)}
⊢ u ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))

Tactic:
rw [← extChartAt_to_inv (I := I) x] at u_mem

Premises used: extChartAt_to_inv
-- Module: Mathlib.Geometry.Manifold.MFDeriv.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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 x
hu : u ∩ {x}ᶜ ⊆ {y : M | (y ∈ s) = (y ∈ t)}
u_mem₁ : u ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
⊢ u ∩ {x}ᶜ ⊆ {y : M | (y ∈ s) = (y ∈ t)}

Tactic:
rw [← extChartAt_to_inv (I := I) x] at u_mem

Premises used: extChartAt_to_inv
-- Module: Mathlib.Geometry.Manifold.MFDeriv.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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
hu : u ∩ {x}ᶜ ⊆ {y : M | (y ∈ s) = (y ∈ t)}
rw :
  (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈
    𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x ⊔ 𝓝[(range (↑I : H → E))ᶜ] (↑(extChartAt I x) : M → E) x
⊢ (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)

Tactic:
rw [← nhdsWithin_univ, ← union_compl_self (range I), nhdsWithin_union]

Premises used: nhdsWithin_univ, Set.union_compl_self, ModelWithCorners.toFun', nhdsWithin_union, Set.range
-- Module: Mathlib.Geometry.Manifold.MFDeriv.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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
hu : u ∩ {x}ᶜ ⊆ {y : M | (y ∈ s) = (y ∈ t)}
⊢ (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈
    𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x ⊔ 𝓝[(range (↑I : H → E))ᶜ] (↑(extChartAt I x) : M → E) x

Tactic:
apply Filter.union_mem_sup (extChartAt_target_mem_nhdsWithin x) self_mem_nhdsWithin

Premises used: extChartAt_target_mem_nhdsWithin, self_mem_nhdsWithin, Filter.union_mem_sup
-- Module: Mathlib.Geometry.Manifold.MFDeriv.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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
hu : u ∩ {x}ᶜ ⊆ {y : M | (y ∈ s) = (y ∈ t)}
⊢ (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)

Tactic:
have B : (extChartAt I x).target ∪ (range I)ᶜ ∈ 𝓝 (extChartAt I x x) := by
    rw [← nhdsWithin_univ, ← union_compl_self (range I), nhdsWithin_union]
    apply Filter.union_mem_sup (extChartAt_target_mem_nhdsWithin x) self_mem_nhdsWithin
-- Module: Mathlib.Geometry.Manifold.MFDeriv.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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
hu : u ∩ {x}ᶜ ⊆ {y : M | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
apply :
  (↑(extChartAt I x).symm : E → M) ⁻¹' u ∩ ((extChartAt I x).target ∪ (range (↑I : H → E))ᶜ) ∩
      {(↑(extChartAt I x) : M → E) x}ᶜ ⊆
    {x_1 : E |
      (fun (x_2 : E) ↦
          ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) x_2 =
            ((↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)) x_2)
        x_1}
⊢ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) =ᶠ[𝓝[≠] (↑(extChartAt I x) : M → E) x]
    (↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)

Tactic:
apply mem_nhdsWithin_iff_exists_mem_nhds_inter.2
    ⟨_, Filter.inter_mem ((continuousAt_extChartAt_symm x).preimage_mem_nhds u_mem) B, ?_⟩

Premises used: Iff.mpr, Filter.inter_mem, ContinuousAt.preimage_mem_nhds, continuousAt_extChartAt_symm, And.intro, Exists.intro, mem_nhdsWithin_iff_exists_mem_nhds_inter
-- Module: Mathlib.Geometry.Manifold.MFDeriv.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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
hu : u ∩ {x}ᶜ ⊆ {y : M | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
z : E
hz : z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' u ∩ ((extChartAt I x).target ∪ (range (↑I : H → E))ᶜ)
h'z : Membership.mem (γ := Set E) {(↑(extChartAt I x) : M → E) x}ᶜ z
simp :
  ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) z ↔
    ((↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)) z
⊢ Membership.mem (γ := Set E)
    {x_1 : E |
      (fun (x_2 : E) ↦
          ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) x_2 =
            ((↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)) x_2)
        x_1}
    z

Tactic:
simp only [eq_iff_iff, mem_setOf_eq]

Premises used: Set.mem_setOf_eq, eq_iff_iff
-- Module: Mathlib.Geometry.Manifold.MFDeriv.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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
hu : u ∩ {x}ᶜ ⊆ {y : M | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
z : E
hz : z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' u ∩ ((extChartAt I x).target ∪ (range (↑I : H → E))ᶜ)
h'z : Membership.mem (γ := Set E) {(↑(extChartAt I x) : M → E) x}ᶜ z
pos :
  ∀ (hIz : z ∈ range (↑I : H → E)),
    z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) ↔
      z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)
neg :
  ∀ (hIz : z ∉ range (↑I : H → E)),
    z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) ↔
      z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)
⊢ z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) ↔
    z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)

Tactic:
by_cases hIz : z ∈ range I

Premises used: ModelWithCorners.toFun', Set.range
-- Module: Mathlib.Geometry.Manifold.MFDeriv.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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
hu : u ∩ {x}ᶜ ⊆ {y : M | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
z : E
hz : z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' u ∩ ((extChartAt I x).target ∪ (range (↑I : H → E))ᶜ)
h'z : Membership.mem (γ := Set E) {(↑(extChartAt I x) : M → E) x}ᶜ z
hIz : z ∈ range (↑I : H → E)
pos :
  ∀ (hz : (↑(extChartAt I x).symm : E → M) z ∈ u ∧ z ∈ (extChartAt I x).target),
    (↑(extChartAt I x).symm : E → M) z ∈ s ↔ (↑(extChartAt I x).symm : E → M) z ∈ t
⊢ z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) ↔
    z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)

Tactic:
simp only [mem_inter_iff, mem_preimage, mem_union, mem_compl_iff, hIz, not_true_eq_false,
      or_false, and_true] at hz ⊢

Premises used: Set.mem_union, and_true, Set.mem_inter_iff, not_true_eq_false, or_false, Set.mem_compl_iff, Set.mem_preimage
-- Module: Mathlib.Geometry.Manifold.MFDeriv.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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
hu : u ∩ {x}ᶜ ⊆ {y : M | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
z : E
h'z : Membership.mem (γ := Set E) {(↑(extChartAt I x) : M → E) x}ᶜ z
hIz : z ∈ range (↑I : H → E)
hz : (↑(extChartAt I x).symm : E → M) z ∈ u ∧ z ∈ (extChartAt I x).target
pos : ((↑(extChartAt I x).symm : E → M) z ∈ s) = ((↑(extChartAt I x).symm : E → M) z ∈ t)
⊢ (↑(extChartAt I x).symm : E → M) z ∈ s ↔ (↑(extChartAt I x).symm : E → M) z ∈ t

Tactic:
rw [← eq_iff_iff]

Premises used: eq_iff_iff
-- Module: Mathlib.Geometry.Manifold.MFDeriv.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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
hu : u ∩ {x}ᶜ ⊆ {y : M | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
z : E
h'z : Membership.mem (γ := Set E) {(↑(extChartAt I x) : M → E) x}ᶜ z
hIz : z ∈ range (↑I : H → E)
hz : (↑(extChartAt I x).symm : E → M) z ∈ u ∧ z ∈ (extChartAt I x).target
apply : Membership.mem (γ := Set M) {x}ᶜ ((↑(extChartAt I x).symm : E → M) z)
⊢ ((↑(extChartAt I x).symm : E → M) z ∈ s) = ((↑(extChartAt I x).symm : E → M) z ∈ t)

Tactic:
apply hu ⟨hz.1, ?_⟩

Premises used: And.left, And.intro
-- Module: Mathlib.Geometry.Manifold.MFDeriv.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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
hu : u ∩ {x}ᶜ ⊆ {y : M | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
z : E
h'z : Membership.mem (γ := Set E) {(↑(extChartAt I x) : M → E) x}ᶜ z
hIz : z ∈ range (↑I : H → E)
hz : (↑(extChartAt I x).symm : E → M) z ∈ u ∧ z ∈ (extChartAt I x).target
⊢ ¬z = (↑(extChartAt I x) : M → E) x

Tactic:
push _ ∈ _ at h'z ⊢
-- Module: Mathlib.Geometry.Manifold.MFDeriv.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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
hu : u ∩ {x}ᶜ ⊆ {y : M | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
z : E
hIz : z ∈ range (↑I : H → E)
hz : (↑(extChartAt I x).symm : E → M) z ∈ u ∧ z ∈ (extChartAt I x).target
h'z : ¬z = (↑(extChartAt I x) : M → E) x
⊢ x ∈ (extChartAt I x).source

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
hu : u ∩ {x}ᶜ ⊆ {y : M | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
z : E
hIz : z ∈ range (↑I : H → E)
hz : (↑(extChartAt I x).symm : E → M) z ∈ u ∧ z ∈ (extChartAt I x).target
h'z : ¬z = (↑(extChartAt I x) : M → E) x
rw : ¬(↑(extChartAt I x) : M → E) x = z
⊢ ¬(↑(extChartAt I x).symm : E → M) z = x

Tactic:
rw [eq_comm, (extChartAt I x).eq_symm_apply (by simp) hz.2]

Premises used: PartialEquiv.eq_symm_apply, extChartAt, eq_comm, And.right
-- Module: Mathlib.Geometry.Manifold.MFDeriv.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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
hu : u ∩ {x}ᶜ ⊆ {y : M | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
z : E
hIz : z ∈ range (↑I : H → E)
hz : (↑(extChartAt I x).symm : E → M) z ∈ u ∧ z ∈ (extChartAt I x).target
h'z : ¬z = (↑(extChartAt I x) : M → E) x
⊢ ¬(↑(extChartAt I x) : M → E) x = z

Tactic:
Ne.symm h'z

Premises used: Ne.symm
-- Module: Mathlib.Geometry.Manifold.MFDeriv.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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
hu : u ∩ {x}ᶜ ⊆ {y : M | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
z : E
hIz : z ∈ range (↑I : H → E)
hz : (↑(extChartAt I x).symm : E → M) z ∈ u ∧ z ∈ (extChartAt I x).target
h'z : ¬z = (↑(extChartAt I x) : M → E) x
⊢ ¬(↑(extChartAt I x) : M → E) x = z

Tactic:
exact Ne.symm h'z

Premises used: Ne.symm
-- Module: Mathlib.Geometry.Manifold.MFDeriv.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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
hu : u ∩ {x}ᶜ ⊆ {y : M | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
z : E
hz : z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' u ∩ ((extChartAt I x).target ∪ (range (↑I : H → E))ᶜ)
h'z : Membership.mem (γ := Set E) {(↑(extChartAt I x) : M → E) x}ᶜ z
hIz : z ∉ range (↑I : H → E)
⊢ z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) ↔
    z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)

Tactic:
simp [hIz]
-- Module: Mathlib.Geometry.Manifold.MFDeriv.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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
s t : Set M
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ T1Space M

Tactic:
have : T1Space M := I.t1Space M
-- Module: Mathlib.Geometry.Manifold.MFDeriv.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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
s t : Set M
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
⊢ ContinuousWithinAt f s x ∧
      HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
        ((↑(extChartAt I x) : M → E) x) ↔
    ContinuousWithinAt f t x ∧
      HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' ((↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E))
        ((↑(extChartAt I x) : M → E) x)

Tactic:
and_congr ?_ ?_

Premises used: and_congr