awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : WithTop ℕ∞
inst_6 : IsManifold I n M
e e' : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
hex : x ∈ e.source
hex' : x ∈ e'.source
mp :
  (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target → (↑(e'.extend I) : M → E) x ∈ interior (e'.extend I).target
⊢ (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target ↔ (↑(e'.extend I) : M → E) x ∈ interior (e'.extend I).target
have mpr : (↑(e'.extend I) : M → E) x ∈ interior (e'.extend I).target → (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : WithTop ℕ∞
inst_6 : IsManifold I n M
e : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
hx : x ∈ e.source
⊢ I.IsInteriorPoint x ↔ (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target
have rw : (↑(extChartAt I x) : M → E) x ∈ interior (extChartAt I x).target ↔
  (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target
Tactic: rw [isInteriorPoint_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : WithTop ℕ∞
inst_6 : IsManifold I n M
e : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
hx : x ∈ e.source
⊢ I.IsBoundaryPoint x ↔ (↑(e.extend I) : M → E) x ∈ frontier (e.extend I).target
have rw : (↑(e.extend I) : M → E) x ∈ (e.extend I).target
Tactic: rw [← not_iff_not, ← I.isInteriorPoint_iff_not_isBoundaryPoint,
    I.isInteriorPoint_iff_of_mem_atlas hn he hx, mem_interior_iff_notMem_frontier]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : WithTop ℕ∞
inst_6 : IsManifold I n M
hn : n ≠ 0
⊢ IsOpen[inst_4] (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)
have refine : ∀ (x : M) (hx : x ∈ ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M),
  (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∩
      (↑(extChartAt I x) : M → E) ⁻¹' interior (extChartAt I x).target ⊆
    ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M
Tactic: refine isOpen_iff_forall_mem_open.2 fun x hx ↦ ⟨_, ?_, isOpen_extChartAt_preimage (I := I) x
    isOpen_interior, mem_chart_source H x, isInteriorPoint_iff.1 hx⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : WithTop ℕ∞
inst_6 : IsManifold I n M
hn : n ≠ 0
⊢ IsClosed[inst_4] (ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)
have rw : IsOpen[inst_4] (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)
Tactic: rw [← I.compl_interior, isClosed_compl_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (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
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'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
f : M → N
x : M
hf : MDiffAt f x
hf' :
  Surjective.{u_2 + 1, u_5 + 1} (α := TangentSpace I x) (β := TangentSpace I' (f x))
    (⇑(mfderiv% f x) : (a : TangentSpace I x) → TangentSpace I' (f x))
hx : I.IsInteriorPoint x
⊢ I'.IsInteriorPoint (f x)
have inr : ∀
  (this :
    ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_11 : NormedAddCommGroup E]
      [inst_12 : NormedSpace 𝕜 E] {H : Type u_3} [inst_13 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
      {M : Type u_4} [inst_14 : TopologicalSpace M] [inst_15 : ChartedSpace H M] {E' : Type u_5}
      [inst_16 : NormedAddCommGroup E'] [inst_17 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_18 : TopologicalSpace H']
      {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_7} [inst_19 : TopologicalSpace N] [inst_20 : ChartedSpace H' N]
      {f : M → N} {x : M} (hf : MDiffAt f x)
      (hf' :
        Surjective.{u_2 + 1, u_5 + 1} (α := TangentSpace I x) (β := TangentSpace I' (f x))
          (⇑(mfderiv% f x) : (a : TangentSpace I x) → TangentSpace I' (f x)))
      (hx : I.IsInteriorPoint x) (h : IsRCLikeNormedField 𝕜), I'.IsInteriorPoint (f x)),
  ¬IsRCLikeNormedField 𝕜 → I'.IsInteriorPoint (f x)
Tactic: wlog _ : IsRCLikeNormedField 𝕜
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (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
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'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
f : M → N
x : M
hf : MDiffAt f x
hf' :
  Surjective.{u_2 + 1, u_5 + 1} (α := TangentSpace I x) (β := TangentSpace I' (f x))
    (⇑(mfderiv% f x) : (a : TangentSpace I x) → TangentSpace I' (f x))
hx : I.IsInteriorPoint x
inr :
  ∀
    (this :
      ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_11 : NormedAddCommGroup E]
        [inst_12 : NormedSpace 𝕜 E] {H : Type u_3} [inst_13 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
        {M : Type u_4} [inst_14 : TopologicalSpace M] [inst_15 : ChartedSpace H M] {E' : Type u_5}
        [inst_16 : NormedAddCommGroup E'] [inst_17 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_18 : TopologicalSpace H']
        {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_7} [inst_19 : TopologicalSpace N] [inst_20 : ChartedSpace H' N]
        {f : M → N} {x : M} (hf : MDiffAt f x)
        (hf' :
          Surjective.{u_2 + 1, u_5 + 1} (α := TangentSpace I x) (β := TangentSpace I' (f x))
            (⇑(mfderiv% f x) : (a : TangentSpace I x) → TangentSpace I' (f x)))
        (hx : I.IsInteriorPoint x) (h : IsRCLikeNormedField 𝕜), I'.IsInteriorPoint (f x)),
    ¬IsRCLikeNormedField 𝕜 → I'.IsInteriorPoint (f x)
⊢ I'.IsInteriorPoint (f x)
have wlog : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_11 : NormedAddCommGroup E]
  [inst_12 : NormedSpace 𝕜 E] {H : Type u_3} [inst_13 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_14 : TopologicalSpace M] [inst_15 : ChartedSpace H M] {E' : Type u_5} [inst_16 : NormedAddCommGroup E']
  [inst_17 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_18 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {N : Type u_7} [inst_19 : TopologicalSpace N] [inst_20 : ChartedSpace H' N] {f : M → N} {x : M} (hf : MDiffAt f x)
  (hf' :
    Surjective.{u_2 + 1, u_5 + 1} (α := TangentSpace I x) (β := TangentSpace I' (f x))
      (⇑(mfderiv% f x) : (a : TangentSpace I x) → TangentSpace I' (f x)))
  (hx : I.IsInteriorPoint x), IsRCLikeNormedField 𝕜 → I'.IsInteriorPoint (f x)
Tactic: wlog _ : IsRCLikeNormedField 𝕜
Cleared hypotheses: f, x, hf, hf', hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (hypothesis)
Goal:
𝕜_1 : Type u_1
inst : NontriviallyNormedField 𝕜_1
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜_1 E_1
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I_1 : ModelWithCorners 𝕜_1 E_1 H_1
M_1 : Type u_4
inst_4 : TopologicalSpace M_1
inst_5 : ChartedSpace H_1 M_1
E'_1 : Type u_5
inst_6 : NormedAddCommGroup E'_1
inst_7 : NormedSpace 𝕜_1 E'_1
H'_1 : Type u_6
inst_8 : TopologicalSpace H'_1
I'_1 : ModelWithCorners 𝕜_1 E'_1 H'_1
N_1 : Type u_7
inst_9 : TopologicalSpace N_1
inst_10 : ChartedSpace H'_1 N_1
𝕜 : Type u_1
inst_11 : NontriviallyNormedField 𝕜
E : Type u_2
inst_12 : NormedAddCommGroup E
inst_13 : NormedSpace 𝕜 E
H : Type u_3
inst_14 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_15 : TopologicalSpace M
inst_16 : ChartedSpace H M
E' : Type u_5
inst_17 : NormedAddCommGroup E'
inst_18 : NormedSpace 𝕜 E'
H' : Type u_6
inst_19 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_20 : TopologicalSpace N
inst_21 : ChartedSpace H' N
f : M → N
x : M
hf : MDiffAt f x
hf' :
  Surjective.{u_2 + 1, u_5 + 1} (α := TangentSpace I x) (β := TangentSpace I' (f x))
    (⇑(mfderiv% f x) : (a : TangentSpace I x) → TangentSpace I' (f x))
hx : I.IsInteriorPoint x
h : IsRCLikeNormedField 𝕜
x_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x_3 : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
⊢ I'.IsInteriorPoint (f x)
have hf'₁ : Surjective.{u_2 + 1, u_5 + 1} (α := TangentSpace I x) (β := TangentSpace I' (f x))
  (⇑(fderivWithin 𝕜 (writtenInExtChartAt I I' x f) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)) :
    (a : TangentSpace I x) → TangentSpace I' (f x))
Tactic: simp only [mfderiv, hf, ite_true] at hf'
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (hypothesis)
Goal:
𝕜_1 : Type u_1
inst : NontriviallyNormedField 𝕜_1
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜_1 E_1
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I_1 : ModelWithCorners 𝕜_1 E_1 H_1
M_1 : Type u_4
inst_4 : TopologicalSpace M_1
inst_5 : ChartedSpace H_1 M_1
E'_1 : Type u_5
inst_6 : NormedAddCommGroup E'_1
inst_7 : NormedSpace 𝕜_1 E'_1
H'_1 : Type u_6
inst_8 : TopologicalSpace H'_1
I'_1 : ModelWithCorners 𝕜_1 E'_1 H'_1
N_1 : Type u_7
inst_9 : TopologicalSpace N_1
inst_10 : ChartedSpace H'_1 N_1
𝕜 : Type u_1
inst_11 : NontriviallyNormedField 𝕜
E : Type u_2
inst_12 : NormedAddCommGroup E
inst_13 : NormedSpace 𝕜 E
H : Type u_3
inst_14 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_15 : TopologicalSpace M
inst_16 : ChartedSpace H M
E' : Type u_5
inst_17 : NormedAddCommGroup E'
inst_18 : NormedSpace 𝕜 E'
H' : Type u_6
inst_19 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_20 : TopologicalSpace N
inst_21 : ChartedSpace H' N
f : M → N
x : M
hf : MDiffAt f x
hx : I.IsInteriorPoint x
h : IsRCLikeNormedField 𝕜
x_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x_3 : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
hf' :
  Surjective.{u_2 + 1, u_5 + 1} (α := TangentSpace I x) (β := TangentSpace I' (f x))
    (⇑(fderivWithin 𝕜 (writtenInExtChartAt I I' x f) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)) :
      (a : TangentSpace I x) → TangentSpace I' (f x))
⊢ I'.IsInteriorPoint (f x)
have hf'' : DifferentiableAt 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)
Tactic: have hf'' := hf.differentiableWithinAt_writtenInExtChartAt.differentiableAt <| by
    simpa [← mem_interior_iff_mem_nhds] using hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (hypothesis)
Goal:
𝕜_1 : Type u_1
inst : NontriviallyNormedField 𝕜_1
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜_1 E_1
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I_1 : ModelWithCorners 𝕜_1 E_1 H_1
M_1 : Type u_4
inst_4 : TopologicalSpace M_1
inst_5 : ChartedSpace H_1 M_1
E'_1 : Type u_5
inst_6 : NormedAddCommGroup E'_1
inst_7 : NormedSpace 𝕜_1 E'_1
H'_1 : Type u_6
inst_8 : TopologicalSpace H'_1
I'_1 : ModelWithCorners 𝕜_1 E'_1 H'_1
N_1 : Type u_7
inst_9 : TopologicalSpace N_1
inst_10 : ChartedSpace H'_1 N_1
𝕜 : Type u_1
inst_11 : NontriviallyNormedField 𝕜
E : Type u_2
inst_12 : NormedAddCommGroup E
inst_13 : NormedSpace 𝕜 E
H : Type u_3
inst_14 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_15 : TopologicalSpace M
inst_16 : ChartedSpace H M
E' : Type u_5
inst_17 : NormedAddCommGroup E'
inst_18 : NormedSpace 𝕜 E'
H' : Type u_6
inst_19 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_20 : TopologicalSpace N
inst_21 : ChartedSpace H' N
f : M → N
x : M
hf : MDiffAt f x
hx : I.IsInteriorPoint x
h : IsRCLikeNormedField 𝕜
x_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x_3 : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
hf' :
  Surjective.{u_2 + 1, u_5 + 1} (α := TangentSpace I x) (β := TangentSpace I' (f x))
    (⇑(fderivWithin 𝕜 (writtenInExtChartAt I I' x f) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)) :
      (a : TangentSpace I x) → TangentSpace I' (f x))
hf'' : DifferentiableAt 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)
⊢ I'.IsInteriorPoint (f x)
have hf'₁ : Surjective.{u_2 + 1, u_5 + 1} (α := TangentSpace I x) (β := TangentSpace I' (f x))
  (⇑(fderiv 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)) :
    (a : TangentSpace I x) → TangentSpace I' (f x))
Tactic: rw [fderivWithin_eq_fderiv (I.uniqueDiffOn _ <| by simp) hf''] at hf'
Cleared hypotheses: hf', hf''
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (goal)
Goal:
𝕜_1 : Type u_1
inst : NontriviallyNormedField 𝕜_1
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜_1 E_1
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I_1 : ModelWithCorners 𝕜_1 E_1 H_1
M_1 : Type u_4
inst_4 : TopologicalSpace M_1
inst_5 : ChartedSpace H_1 M_1
E'_1 : Type u_5
inst_6 : NormedAddCommGroup E'_1
inst_7 : NormedSpace 𝕜_1 E'_1
H'_1 : Type u_6
inst_8 : TopologicalSpace H'_1
I'_1 : ModelWithCorners 𝕜_1 E'_1 H'_1
N_1 : Type u_7
inst_9 : TopologicalSpace N_1
inst_10 : ChartedSpace H'_1 N_1
𝕜 : Type u_1
inst_11 : NontriviallyNormedField 𝕜
E : Type u_2
inst_12 : NormedAddCommGroup E
inst_13 : NormedSpace 𝕜 E
H : Type u_3
inst_14 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_15 : TopologicalSpace M
inst_16 : ChartedSpace H M
E' : Type u_5
inst_17 : NormedAddCommGroup E'
inst_18 : NormedSpace 𝕜 E'
H' : Type u_6
inst_19 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_20 : TopologicalSpace N
inst_21 : ChartedSpace H' N
f : M → N
x : M
hf : MDiffAt f x
hx : I.IsInteriorPoint x
h : IsRCLikeNormedField 𝕜
x_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x_3 : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
hf' :
  Surjective.{u_2 + 1, u_5 + 1} (α := TangentSpace I x) (β := TangentSpace I' (f x))
    (⇑(fderiv 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)) :
      (a : TangentSpace I x) → TangentSpace I' (f x))
hf'' : DifferentiableAt 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)
⊢ Surjective.{u_2 + 1, u_5 + 1} (α := E) (β := E')
    (⇑(fderiv ℝ (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)) : (a : E) → E')
have rwa : Surjective.{u_2 + 1, u_5 + 1} (α := E) (β := E')
  (⇑(ContinuousLinearMap.restrictScalars ℝ (fderiv 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x))) :
    (a : E) → E')
Tactic: rwa [hf''.fderiv_restrictScalars (𝕜 := ℝ), ContinuousLinearMap.coe_restrictScalars']
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (goal)
Goal:
𝕜_1 : Type u_1
inst : NontriviallyNormedField 𝕜_1
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜_1 E_1
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I_1 : ModelWithCorners 𝕜_1 E_1 H_1
M_1 : Type u_4
inst_4 : TopologicalSpace M_1
inst_5 : ChartedSpace H_1 M_1
E'_1 : Type u_5
inst_6 : NormedAddCommGroup E'_1
inst_7 : NormedSpace 𝕜_1 E'_1
H'_1 : Type u_6
inst_8 : TopologicalSpace H'_1
I'_1 : ModelWithCorners 𝕜_1 E'_1 H'_1
N_1 : Type u_7
inst_9 : TopologicalSpace N_1
inst_10 : ChartedSpace H'_1 N_1
𝕜 : Type u_1
inst_11 : NontriviallyNormedField 𝕜
E : Type u_2
inst_12 : NormedAddCommGroup E
inst_13 : NormedSpace 𝕜 E
H : Type u_3
inst_14 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_15 : TopologicalSpace M
inst_16 : ChartedSpace H M
E' : Type u_5
inst_17 : NormedAddCommGroup E'
inst_18 : NormedSpace 𝕜 E'
H' : Type u_6
inst_19 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_20 : TopologicalSpace N
inst_21 : ChartedSpace H' N
f : M → N
x : M
hf : MDiffAt f x
hx : I.IsInteriorPoint x
h : IsRCLikeNormedField 𝕜
x_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x_3 : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
hf' :
  Surjective.{u_2 + 1, u_5 + 1} (α := TangentSpace I x) (β := TangentSpace I' (f x))
    (⇑(fderiv 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)) :
      (a : TangentSpace I x) → TangentSpace I' (f x))
hf'' : DifferentiableAt 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)
rwa :
  Surjective.{u_2 + 1, u_5 + 1} (α := E) (β := E')
    (⇑(ContinuousLinearMap.restrictScalars ℝ
          (fderiv 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x))) :
      (a : E) → E')
⊢ Surjective.{u_2 + 1, u_5 + 1} (α := E) (β := E')
    (⇑(fderiv ℝ (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)) : (a : E) → E')
have rwa₁ : Surjective.{u_2 + 1, u_5 + 1} (α := E) (β := E')
  (⇑(fderiv 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)) : (a : E) → E')
Tactic: rwa [hf''.fderiv_restrictScalars (𝕜 := ℝ), ContinuousLinearMap.coe_restrictScalars']
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (hypothesis)
Goal:
𝕜_1 : Type u_1
inst : NontriviallyNormedField 𝕜_1
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜_1 E_1
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I_1 : ModelWithCorners 𝕜_1 E_1 H_1
M_1 : Type u_4
inst_4 : TopologicalSpace M_1
inst_5 : ChartedSpace H_1 M_1
E'_1 : Type u_5
inst_6 : NormedAddCommGroup E'_1
inst_7 : NormedSpace 𝕜_1 E'_1
H'_1 : Type u_6
inst_8 : TopologicalSpace H'_1
I'_1 : ModelWithCorners 𝕜_1 E'_1 H'_1
N_1 : Type u_7
inst_9 : TopologicalSpace N_1
inst_10 : ChartedSpace H'_1 N_1
𝕜 : Type u_1
inst_11 : NontriviallyNormedField 𝕜
E : Type u_2
inst_12 : NormedAddCommGroup E
inst_13 : NormedSpace 𝕜 E
H : Type u_3
inst_14 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_15 : TopologicalSpace M
inst_16 : ChartedSpace H M
E' : Type u_5
inst_17 : NormedAddCommGroup E'
inst_18 : NormedSpace 𝕜 E'
H' : Type u_6
inst_19 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_20 : TopologicalSpace N
inst_21 : ChartedSpace H' N
f : M → N
x : M
hf : MDiffAt f x
hx : I.IsInteriorPoint x
h : IsRCLikeNormedField 𝕜
x_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x_3 : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
hf' :
  Surjective.{u_2 + 1, u_5 + 1} (α := TangentSpace I x) (β := TangentSpace I' (f x))
    (⇑(fderiv 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)) :
      (a : TangentSpace I x) → TangentSpace I' (f x))
hf'' : DifferentiableAt 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)
⊢ I'.IsInteriorPoint (f x)
have hf'₁ : Surjective.{u_2 + 1, u_5 + 1} (α := E) (β := E')
  (⇑(fderiv ℝ (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)) : (a : E) → E')
Tactic: replace hf' : Surjective (fderiv ℝ (writtenInExtChartAt I I' x f) (extChartAt I x x)) := by
    rwa [hf''.fderiv_restrictScalars (𝕜 := ℝ), ContinuousLinearMap.coe_restrictScalars']
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (hypothesis)
Goal:
𝕜_1 : Type u_1
inst : NontriviallyNormedField 𝕜_1
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜_1 E_1
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I_1 : ModelWithCorners 𝕜_1 E_1 H_1
M_1 : Type u_4
inst_4 : TopologicalSpace M_1
inst_5 : ChartedSpace H_1 M_1
E'_1 : Type u_5
inst_6 : NormedAddCommGroup E'_1
inst_7 : NormedSpace 𝕜_1 E'_1
H'_1 : Type u_6
inst_8 : TopologicalSpace H'_1
I'_1 : ModelWithCorners 𝕜_1 E'_1 H'_1
N_1 : Type u_7
inst_9 : TopologicalSpace N_1
inst_10 : ChartedSpace H'_1 N_1
𝕜 : Type u_1
inst_11 : NontriviallyNormedField 𝕜
E : Type u_2
inst_12 : NormedAddCommGroup E
inst_13 : NormedSpace 𝕜 E
H : Type u_3
inst_14 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_15 : TopologicalSpace M
inst_16 : ChartedSpace H M
E' : Type u_5
inst_17 : NormedAddCommGroup E'
inst_18 : NormedSpace 𝕜 E'
H' : Type u_6
inst_19 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_20 : TopologicalSpace N
inst_21 : ChartedSpace H' N
f : M → N
x : M
hf : MDiffAt f x
hx : I.IsInteriorPoint x
h : IsRCLikeNormedField 𝕜
x_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x_3 : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
hf'' : DifferentiableAt 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)
hf' :
  Surjective.{u_2 + 1, u_5 + 1} (α := E) (β := E')
    (⇑(fderiv ℝ (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)) : (a : E) → E')
⊢ I'.IsInteriorPoint (f x)
have hf''₁ : DifferentiableAt ℝ (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)
Tactic: replace hf'' := hf''.restrictScalars ℝ
Cleared hypotheses: hf''