awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Diffeology.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : DiffeologicalSpace X
inst_1 : DiffeologicalSpace Y
f : X → Y
hf : DSmooth f
⊢ Continuous[dTopology, dTopology] f
have simp_rw : ∀ (s : Set Y),
  (∀ (n : ℕ) (p : EuclideanSpace ℝ (Fin n) → Y), IsPlot p → IsOpen (p ⁻¹' s)) →
    ∀ (n : ℕ) (p : EuclideanSpace ℝ (Fin n) → X), IsPlot p → IsOpen (p ⁻¹' f ⁻¹' s)
Tactic: simp_rw [continuous_def, isOpen_iff_preimages_plots (X := X), isOpen_iff_preimages_plots (X := Y)]
-- Lean 4 proof step from Mathlib.Geometry.Diffeology.Basic (goal)
Goal:
X : Type u_1
d : DiffeologicalSpace X
t : TopologicalSpace X
h : dTopology = t
u : Set X
⊢ TopologicalSpace.IsOpen u ↔
    ∀ {n : ℕ} (p : EuclideanSpace ℝ (Fin n) → X),
      Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n) → X)) (plots n) p → IsOpen (p ⁻¹' u)
have rw : TopologicalSpace.IsOpen u ↔ TopologicalSpace.IsOpen u
Tactic: rw [← d.isOpen_iff_preimages_plots, ← h]
-- Lean 4 proof step from Mathlib.Geometry.Diffeology.Basic (goal)
Goal:
X : Type u_1
d : DiffeologicalSpace X
t : TopologicalSpace X
h : dTopology = t
u : Set X
rw : TopologicalSpace.IsOpen u ↔ TopologicalSpace.IsOpen u
⊢ TopologicalSpace.IsOpen u ↔
    ∀ {n : ℕ} (p : EuclideanSpace ℝ (Fin n) → X),
      Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n) → X)) (plots n) p → IsOpen (p ⁻¹' u)
have rw₁ : TopologicalSpace.IsOpen u ↔ TopologicalSpace.IsOpen u
Tactic: rw [← d.isOpen_iff_preimages_plots, ← h]
-- Lean 4 proof step from Mathlib.Geometry.Diffeology.Basic (goal)
Goal:
X : Type u_1
d : DiffeologicalSpace X
t : TopologicalSpace X
h : dTopology = t
⊢ d.replaceDTopology t h = d
have h₁ : ∀ (x : ℕ) (x_1 : EuclideanSpace ℝ (Fin x) → X), Diffeology.IsPlot x_1 ↔ Diffeology.IsPlot x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Diffeology.Basic (goal)
Goal:
X : Type u_1
d : CorePlotsOn X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
h :
  ∀ (x : EuclideanSpace ℝ (Fin n)),
    ∃ (u : Set (EuclideanSpace ℝ (Fin n))),
      IsOpen u ∧
        x ∈ u ∧
          ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
            (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) →
              ContDiff ℝ ∞ f →
                Membership.mem (γ := Set (EuclideanSpace ℝ (Fin m) → X)) {p : EuclideanSpace ℝ (Fin m) → X | d.isPlot p}
                  (p ∘ f)
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n) → X)) {p : EuclideanSpace ℝ (Fin n) → X | d.isPlot p} p
have refine : ∀ (x : EuclideanSpace ℝ (Fin n)),
  Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) Set.univ x →
    ∃ (v : Set (EuclideanSpace ℝ (Fin n))) (hv : IsOpen v), x ∈ v ∧ d.isPlotOn (u := v) hv p
Tactic: refine d.isPlotOn_univ.mp <| d.locality _ fun x _ ↦ ?_
-- Lean 4 proof step from Mathlib.Geometry.Diffeology.Basic (goal)
Goal:
X : Type u_1
d : CorePlotsOn X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
h :
  ∀ (x : EuclideanSpace ℝ (Fin n)),
    ∃ (u : Set (EuclideanSpace ℝ (Fin n))),
      IsOpen u ∧
        x ∈ u ∧
          ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
            (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) →
              ContDiff ℝ ∞ f →
                Membership.mem (γ := Set (EuclideanSpace ℝ (Fin m) → X)) {p : EuclideanSpace ℝ (Fin m) → X | d.isPlot p}
                  (p ∘ f)
x : EuclideanSpace ℝ (Fin n)
h_1 : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) Set.univ x
⊢ ∃ (v : Set (EuclideanSpace ℝ (Fin n))) (hv : IsOpen v), x ∈ v ∧ d.isPlotOn (u := v) hv p
have let : ∀ (u : Set (EuclideanSpace ℝ (Fin n))) (hu : IsOpen u) (hxu : x ∈ u)
  (hu' :
    ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
      (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) →
        ContDiff ℝ ∞ f →
          Membership.mem (γ := Set (EuclideanSpace ℝ (Fin m) → X)) {p : EuclideanSpace ℝ (Fin m) → X | d.isPlot p}
            (p ∘ f)),
  ∃ (v : Set (EuclideanSpace ℝ (Fin n))) (hv : IsOpen v), x ∈ v ∧ d.isPlotOn (u := v) hv p
Tactic: let ⟨u, hu, hxu, hu'⟩ := h x
-- Lean 4 proof step from Mathlib.Geometry.Diffeology.Basic (goal)
Goal:
X : Type u_1
d : CorePlotsOn X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
h :
  ∀ (x : EuclideanSpace ℝ (Fin n)),
    ∃ (u : Set (EuclideanSpace ℝ (Fin n))),
      IsOpen u ∧
        x ∈ u ∧
          ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
            (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) →
              ContDiff ℝ ∞ f →
                Membership.mem (γ := Set (EuclideanSpace ℝ (Fin m) → X)) {p : EuclideanSpace ℝ (Fin m) → X | d.isPlot p}
                  (p ∘ f)
x : EuclideanSpace ℝ (Fin n)
h_1 : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) Set.univ x
u : Set (EuclideanSpace ℝ (Fin n))
hu : IsOpen u
hxu : x ∈ u
hu' :
  ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
    (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) →
      ContDiff ℝ ∞ f →
        Membership.mem (γ := Set (EuclideanSpace ℝ (Fin m) → X)) {p : EuclideanSpace ℝ (Fin m) → X | d.isPlot p} (p ∘ f)
⊢ ∃ (v : Set (EuclideanSpace ℝ (Fin n))) (hv : IsOpen v), x ∈ v ∧ d.isPlotOn (u := v) hv p
have let : ∀ (ε : ℝ) (hε : ε > 0) (hε' : Metric.ball x ε ⊆ u),
  ∃ (v : Set (EuclideanSpace ℝ (Fin n))) (hv : IsOpen v), x ∈ v ∧ d.isPlotOn (u := v) hv p
Tactic: let ⟨ε, hε, hε'⟩ := Metric.isOpen_iff.mp hu x hxu
-- Lean 4 proof step from Mathlib.Geometry.Diffeology.Basic (hypothesis)
Goal:
X : Type u_1
d : CorePlotsOn X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
h :
  ∀ (x : EuclideanSpace ℝ (Fin n)),
    ∃ (u : Set (EuclideanSpace ℝ (Fin n))),
      IsOpen u ∧
        x ∈ u ∧
          ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
            (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) →
              ContDiff ℝ ∞ f →
                Membership.mem (γ := Set (EuclideanSpace ℝ (Fin m) → X)) {p : EuclideanSpace ℝ (Fin m) → X | d.isPlot p}
                  (p ∘ f)
x : EuclideanSpace ℝ (Fin n)
h_1 : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) Set.univ x
u : Set (EuclideanSpace ℝ (Fin n))
hu : IsOpen u
hxu : x ∈ u
hu' :
  ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
    (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) →
      ContDiff ℝ ∞ f →
        Membership.mem (γ := Set (EuclideanSpace ℝ (Fin m) → X)) {p : EuclideanSpace ℝ (Fin m) → X | d.isPlot p} (p ∘ f)
ε : ℝ
hε : ε > 0
hε' : Metric.ball x ε ⊆ u
x' : EuclideanSpace ℝ (Fin n)
⊢ (↑(OpenPartialHomeomorph.univBall x ε) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) x' ∈ u
have h₁ : ∀ (h : x' ∈ (OpenPartialHomeomorph.toPartialEquiv (OpenPartialHomeomorph.univBall x ε)).source),
  (↑(OpenPartialHomeomorph.univBall x ε) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) x' ∈
    (OpenPartialHomeomorph.toPartialEquiv (OpenPartialHomeomorph.univBall x ε)).target
Tactic: replace h := (OpenPartialHomeomorph.univBall x ε).map_source (x := x')
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Diffeology.Basic (hypothesis)
Goal:
X : Type u_1
d : CorePlotsOn X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
x : EuclideanSpace ℝ (Fin n)
h_1 : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) Set.univ x
u : Set (EuclideanSpace ℝ (Fin n))
hu : IsOpen u
hxu : x ∈ u
hu' :
  ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
    (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) →
      ContDiff ℝ ∞ f →
        Membership.mem (γ := Set (EuclideanSpace ℝ (Fin m) → X)) {p : EuclideanSpace ℝ (Fin m) → X | d.isPlot p} (p ∘ f)
ε : ℝ
hε : ε > 0
hε' : Metric.ball x ε ⊆ u
x' : EuclideanSpace ℝ (Fin n)
h :
  ∀ (h : x' ∈ (OpenPartialHomeomorph.toPartialEquiv (OpenPartialHomeomorph.univBall x ε)).source),
    (↑(OpenPartialHomeomorph.univBall x ε) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) x' ∈
      (OpenPartialHomeomorph.toPartialEquiv (OpenPartialHomeomorph.univBall x ε)).target
⊢ (↑(OpenPartialHomeomorph.univBall x ε) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) x' ∈ u
have h₁ : ∀ (h : x' ∈ (OpenPartialHomeomorph.toPartialEquiv (OpenPartialHomeomorph.univBall x ε)).source),
  (↑(OpenPartialHomeomorph.univBall x ε) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) x' ∈ Metric.ball x ε
Tactic: rw [OpenPartialHomeomorph.univBall_target x hε] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Diffeology.Basic (hypothesis)
Goal:
X : Type u_1
d : CorePlotsOn X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
h :
  ∀ (x : EuclideanSpace ℝ (Fin n)),
    ∃ (u : Set (EuclideanSpace ℝ (Fin n))),
      IsOpen u ∧
        x ∈ u ∧
          ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
            (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) →
              ContDiff ℝ ∞ f →
                Membership.mem (γ := Set (EuclideanSpace ℝ (Fin m) → X)) {p : EuclideanSpace ℝ (Fin m) → X | d.isPlot p}
                  (p ∘ f)
x : EuclideanSpace ℝ (Fin n)
h_1 : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) Set.univ x
u : Set (EuclideanSpace ℝ (Fin n))
hu : IsOpen u
hxu : x ∈ u
hu' :
  ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
    (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) →
      ContDiff ℝ ∞ f →
        Membership.mem (γ := Set (EuclideanSpace ℝ (Fin m) → X)) {p : EuclideanSpace ℝ (Fin m) → X | d.isPlot p} (p ∘ f)
ε : ℝ
hε : ε > 0
hε' : Metric.ball x ε ⊆ u
⊢ ∃ (v : Set (EuclideanSpace ℝ (Fin n))) (hv : IsOpen v), x ∈ v ∧ d.isPlotOn (u := v) hv p
have h₁ : d.isPlot (p ∘ (↑(OpenPartialHomeomorph.univBall x ε) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)))
Tactic: have h : d.isPlot (p ∘ OpenPartialHomeomorph.univBall x ε) := hu'
      (f := OpenPartialHomeomorph.univBall x ε)
      (fun x' ↦ by
        replace h := (OpenPartialHomeomorph.univBall x ε).map_source (x := x')
        rw [OpenPartialHomeomorph.univBall_target x hε] at h
        aesop)
      OpenPartialHomeomorph.contDiff_univBall
-- Lean 4 proof step from Mathlib.Geometry.Diffeology.Basic (hypothesis)
Goal:
X : Type u_1
d : CorePlotsOn X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
h_1 :
  ∀ (x : EuclideanSpace ℝ (Fin n)),
    ∃ (u : Set (EuclideanSpace ℝ (Fin n))),
      IsOpen u ∧
        x ∈ u ∧
          ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
            (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) →
              ContDiff ℝ ∞ f →
                Membership.mem (γ := Set (EuclideanSpace ℝ (Fin m) → X)) {p : EuclideanSpace ℝ (Fin m) → X | d.isPlot p}
                  (p ∘ f)
x : EuclideanSpace ℝ (Fin n)
h_2 : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) Set.univ x
u : Set (EuclideanSpace ℝ (Fin n))
hu : IsOpen u
hxu : x ∈ u
hu' :
  ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
    (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) →
      ContDiff ℝ ∞ f →
        Membership.mem (γ := Set (EuclideanSpace ℝ (Fin m) → X)) {p : EuclideanSpace ℝ (Fin m) → X | d.isPlot p} (p ∘ f)
ε : ℝ
hε : ε > 0
hε' : Metric.ball x ε ⊆ u
h : d.isPlot (p ∘ (↑(OpenPartialHomeomorph.univBall x ε) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)))
⊢ ∃ (v : Set (EuclideanSpace ℝ (Fin n))) (hv : IsOpen v), x ∈ v ∧ d.isPlotOn (u := v) hv p
have h' : d.isPlotOn (u := Metric.ball x ε) sorry
  ((p ∘ (↑(OpenPartialHomeomorph.univBall x ε) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))) ∘
    (↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.univBall x ε)) :
      EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)))
Tactic: have h' := d.isPlotOn_reparam (Metric.isOpen_ball) (Set.mapsTo_univ _ _)
      (d.isPlotOn_univ.mpr h) (OpenPartialHomeomorph.contDiffOn_univBall_symm (c := x) (r := ε))
-- Lean 4 proof step from Mathlib.Geometry.Diffeology.Basic (goal)
Goal:
X : Type u_1
d : CorePlotsOn X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
h_1 :
  ∀ (x : EuclideanSpace ℝ (Fin n)),
    ∃ (u : Set (EuclideanSpace ℝ (Fin n))),
      IsOpen u ∧
        x ∈ u ∧
          ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
            (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) →
              ContDiff ℝ ∞ f →
                Membership.mem (γ := Set (EuclideanSpace ℝ (Fin m) → X)) {p : EuclideanSpace ℝ (Fin m) → X | d.isPlot p}
                  (p ∘ f)
x : EuclideanSpace ℝ (Fin n)
h_2 : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) Set.univ x
u : Set (EuclideanSpace ℝ (Fin n))
hu : IsOpen u
hxu : x ∈ u
hu' :
  ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
    (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) →
      ContDiff ℝ ∞ f →
        Membership.mem (γ := Set (EuclideanSpace ℝ (Fin m) → X)) {p : EuclideanSpace ℝ (Fin m) → X | d.isPlot p} (p ∘ f)
ε : ℝ
hε : ε > 0
hε' : Metric.ball x ε ⊆ u
h : d.isPlot (p ∘ (↑(OpenPartialHomeomorph.univBall x ε) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)))
h' :
  d.isPlotOn (u := Metric.ball x ε) ⋯
    ((p ∘ (↑(OpenPartialHomeomorph.univBall x ε) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))) ∘
      (↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.univBall x ε)) :
        EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)))
⊢ ∃ (v : Set (EuclideanSpace ℝ (Fin n))) (hv : IsOpen v), x ∈ v ∧ d.isPlotOn (u := v) hv p
have refine : Set.EqOn
  ((p ∘ (↑(OpenPartialHomeomorph.univBall x ε) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))) ∘
    (↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.univBall x ε)) :
      EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)))
  p (Metric.ball x ε)
Tactic: refine ⟨_, Metric.isOpen_ball, Metric.mem_ball_self hε, (d.isPlotOn_congr _ ?_).mp h'⟩
-- Lean 4 proof step from Mathlib.Geometry.Diffeology.Basic (goal)
Goal:
X : Type u_1
d : CorePlotsOn X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
h_1 :
  ∀ (x : EuclideanSpace ℝ (Fin n)),
    ∃ (u : Set (EuclideanSpace ℝ (Fin n))),
      IsOpen u ∧
        x ∈ u ∧
          ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
            (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) →
              ContDiff ℝ ∞ f →
                Membership.mem (γ := Set (EuclideanSpace ℝ (Fin m) → X)) {p : EuclideanSpace ℝ (Fin m) → X | d.isPlot p}
                  (p ∘ f)
x : EuclideanSpace ℝ (Fin n)
h_2 : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) Set.univ x
u : Set (EuclideanSpace ℝ (Fin n))
hu : IsOpen u
hxu : x ∈ u
hu' :
  ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
    (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) →
      ContDiff ℝ ∞ f →
        Membership.mem (γ := Set (EuclideanSpace ℝ (Fin m) → X)) {p : EuclideanSpace ℝ (Fin m) → X | d.isPlot p} (p ∘ f)
ε : ℝ
hε : ε > 0
hε' : Metric.ball x ε ⊆ u
h : d.isPlot (p ∘ (↑(OpenPartialHomeomorph.univBall x ε) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)))
h' :
  d.isPlotOn (u := Metric.ball x ε) ⋯
    ((p ∘ (↑(OpenPartialHomeomorph.univBall x ε) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))) ∘
      (↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.univBall x ε)) :
        EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)))
⊢ Set.EqOn
    ((p ∘ (↑(OpenPartialHomeomorph.univBall x ε) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))) ∘
      (↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.univBall x ε)) :
        EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)))
    p (Metric.ball x ε)
have rw : Set.EqOn
  (p ∘
    (↑(OpenPartialHomeomorph.trans (OpenPartialHomeomorph.symm (OpenPartialHomeomorph.univBall x ε))
          (OpenPartialHomeomorph.univBall x ε)) :
      EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)))
  p (Metric.ball x ε)
Tactic: rw [Function.comp_assoc, ← OpenPartialHomeomorph.coe_trans]
-- Lean 4 proof step from Mathlib.Geometry.Diffeology.Basic (goal)
Goal:
X : Type u_1
d : CorePlotsOn X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
h_1 :
  ∀ (x : EuclideanSpace ℝ (Fin n)),
    ∃ (u : Set (EuclideanSpace ℝ (Fin n))),
      IsOpen u ∧
        x ∈ u ∧
          ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
            (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) →
              ContDiff ℝ ∞ f →
                Membership.mem (γ := Set (EuclideanSpace ℝ (Fin m) → X)) {p : EuclideanSpace ℝ (Fin m) → X | d.isPlot p}
                  (p ∘ f)
x : EuclideanSpace ℝ (Fin n)
h_2 : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) Set.univ x
u : Set (EuclideanSpace ℝ (Fin n))
hu : IsOpen u
hxu : x ∈ u
hu' :
  ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
    (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) →
      ContDiff ℝ ∞ f →
        Membership.mem (γ := Set (EuclideanSpace ℝ (Fin m) → X)) {p : EuclideanSpace ℝ (Fin m) → X | d.isPlot p} (p ∘ f)
ε : ℝ
hε : ε > 0
hε' : Metric.ball x ε ⊆ u
h : d.isPlot (p ∘ (↑(OpenPartialHomeomorph.univBall x ε) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)))
h' :
  d.isPlotOn (u := Metric.ball x ε) ⋯
    ((p ∘ (↑(OpenPartialHomeomorph.univBall x ε) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))) ∘
      (↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.univBall x ε)) :
        EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)))
⊢ Set.EqOn
    (p ∘
      (↑(OpenPartialHomeomorph.trans (OpenPartialHomeomorph.symm (OpenPartialHomeomorph.univBall x ε))
            (OpenPartialHomeomorph.univBall x ε)) :
        EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)))
    p (Metric.ball x ε)
have h₁ : Set.EqOn
  (↑(OpenPartialHomeomorph.trans (OpenPartialHomeomorph.symm (OpenPartialHomeomorph.univBall x ε))
        (OpenPartialHomeomorph.univBall x ε)) :
    EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
  (fun (x : EuclideanSpace ℝ (Fin n)) ↦ x) (Metric.ball x ε)
Tactic: apply Set.EqOn.comp_left
-- Lean 4 proof step from Mathlib.Geometry.Diffeology.Basic (goal)
Goal:
X : Type u_1
d : CorePlotsOn X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
h_1 :
  ∀ (x : EuclideanSpace ℝ (Fin n)),
    ∃ (u : Set (EuclideanSpace ℝ (Fin n))),
      IsOpen u ∧
        x ∈ u ∧
          ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
            (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) →
              ContDiff ℝ ∞ f →
                Membership.mem (γ := Set (EuclideanSpace ℝ (Fin m) → X)) {p : EuclideanSpace ℝ (Fin m) → X | d.isPlot p}
                  (p ∘ f)
x : EuclideanSpace ℝ (Fin n)
h_2 : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) Set.univ x
u : Set (EuclideanSpace ℝ (Fin n))
hu : IsOpen u
hxu : x ∈ u
hu' :
  ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
    (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) →
      ContDiff ℝ ∞ f →
        Membership.mem (γ := Set (EuclideanSpace ℝ (Fin m) → X)) {p : EuclideanSpace ℝ (Fin m) → X | d.isPlot p} (p ∘ f)
ε : ℝ
hε : ε > 0
hε' : Metric.ball x ε ⊆ u
h : d.isPlot (p ∘ (↑(OpenPartialHomeomorph.univBall x ε) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)))
h' :
  d.isPlotOn (u := Metric.ball x ε) ⋯
    ((p ∘ (↑(OpenPartialHomeomorph.univBall x ε) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))) ∘
      (↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.univBall x ε)) :
        EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)))
⊢ Set.EqOn
    (↑(OpenPartialHomeomorph.trans (OpenPartialHomeomorph.symm (OpenPartialHomeomorph.univBall x ε))
          (OpenPartialHomeomorph.univBall x ε)) :
      EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
    (fun (x : EuclideanSpace ℝ (Fin n)) ↦ x) (Metric.ball x ε)
have h₁ : Metric.ball x ε =
  (OpenPartialHomeomorph.toPartialEquiv
      (OpenPartialHomeomorph.trans (OpenPartialHomeomorph.symm (OpenPartialHomeomorph.univBall x ε))
        (OpenPartialHomeomorph.univBall x ε))).source
Tactic: convert! (OpenPartialHomeomorph.symm_trans_self (OpenPartialHomeomorph.univBall x ε)).2
-- Lean 4 proof step from Mathlib.Geometry.Diffeology.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiffeologicalSpace X
inst_2 : IsDTopologyCompatible X
inst_3 : TopologicalSpace Y
inst_4 : DiffeologicalSpace Y
inst_5 : IsDTopologyCompatible Y
f : X → Y
hf : DSmooth f
⊢ Continuous[inst, inst_3] f
have h : inst = dTopology
Tactic: convert! hf.continuous
-- Lean 4 proof step from Mathlib.Geometry.Diffeology.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiffeologicalSpace X
inst_2 : IsDTopologyCompatible X
inst_3 : TopologicalSpace Y
inst_4 : DiffeologicalSpace Y
inst_5 : IsDTopologyCompatible Y
f : X → Y
hf : DSmooth f
h : inst = dTopology
⊢ Continuous[inst, inst_3] f
have h₁ : inst_3 = dTopology
Tactic: convert! hf.continuous
-- Lean 4 proof step from Mathlib.Geometry.Diffeology.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiffeologicalSpace X
inst_2 : IsDTopologyCompatible X
inst_3 : TopologicalSpace Y
inst_4 : DiffeologicalSpace Y
inst_5 : IsDTopologyCompatible Y
f : X → Y
hf : DSmooth f
⊢ inst = dTopology
have h : inst = inst
Tactic: rw [IsDTopologyCompatible.dTop_eq X]
-- Lean 4 proof step from Mathlib.Geometry.Diffeology.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiffeologicalSpace X
inst_2 : IsDTopologyCompatible X
inst_3 : TopologicalSpace Y
inst_4 : DiffeologicalSpace Y
inst_5 : IsDTopologyCompatible Y
f : X → Y
hf : DSmooth f
⊢ inst_3 = dTopology
have h : inst_3 = inst_3
Tactic: rw [IsDTopologyCompatible.dTop_eq Y]
-- Lean 4 proof step from Mathlib.Geometry.Diffeology.Basic (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
inst_1 : NormedSpace ℝ X
inst_2 : FiniteDimensional ℝ X
n : ℕ
u : Set (EuclideanSpace ℝ (Fin n))
h_1 : IsOpen u
x_1 : EuclideanSpace ℝ (Fin n) → X
h : ∀ x ∈ u, ∃ (v : Set (EuclideanSpace ℝ (Fin n))) (_ : IsOpen v), x ∈ v ∧ ContDiffOn ℝ ∞ x_1 v
x : EuclideanSpace ℝ (Fin n)
hxu : x ∈ u
⊢ ContDiffWithinAt ℝ ∞ x_1 u x
have let : ∀ (v : Set (EuclideanSpace ℝ (Fin n))) (hv : IsOpen v) (hxv : x ∈ v) (hv' : ContDiffOn ℝ ∞ x_1 v),
  ContDiffWithinAt ℝ ∞ x_1 u x
Tactic: let ⟨v, hv, hxv, hv'⟩ := h x hxu
-- Lean 4 proof step from Mathlib.Geometry.Diffeology.Basic (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
inst_1 : NormedSpace ℝ X
inst_2 : FiniteDimensional ℝ X
u : Set X
⊢ TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ} (p : EuclideanSpace ℝ (Fin n) → X), ContDiff ℝ ∞ p → IsOpen (p ⁻¹' u)
have refine : ∀ (h : ∀ {n : ℕ} (p : EuclideanSpace ℝ (Fin n) → X), ContDiff ℝ ∞ p → IsOpen (p ⁻¹' u)), TopologicalSpace.IsOpen u
Tactic: refine ⟨fun hu _ _ hp ↦ IsOpen.preimage (hp.continuous) hu, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Diffeology.Basic (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
inst_1 : NormedSpace ℝ X
inst_2 : FiniteDimensional ℝ X
u : Set X
h : ∀ {n : ℕ} (p : EuclideanSpace ℝ (Fin n) → X), ContDiff ℝ ∞ p → IsOpen (p ⁻¹' u)
⊢ TopologicalSpace.IsOpen u
have rw : TopologicalSpace.IsOpen.{u_1} (X := X)
  (Set.preimage (β := EuclideanSpace ℝ (Fin (Module.finrank ℝ X)))
    (⇑toEuclidean : (a : X) → EuclideanSpace ℝ (Fin (Module.finrank ℝ X)))
    ((⇑(ContinuousLinearEquiv.symm toEuclidean) : (a : EuclideanSpace ℝ (Fin (Module.finrank ℝ X))) → X) ⁻¹' u))
Tactic: rw [← toEuclidean.preimage_symm_preimage u]
-- Lean 4 proof step from Mathlib.Geometry.Diffeology.Basic (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
inst_1 : NormedSpace ℝ X
inst_2 : FiniteDimensional ℝ X
d : DiffeologicalSpace X
h : IsContDiffCompatible X
⊢ d = NormedSpace.toDiffeology X
have h : ∀ (n : ℕ) (p : EuclideanSpace ℝ (Fin n) → X), IsPlot p ↔ IsPlot p
Tactic: ext n p
-- Lean 4 proof step from Mathlib.Geometry.Diffeology.Basic (goal)
Goal:
X : Type u_1
inst : DiffeologicalSpace X
Y : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace ℝ X
inst_3 : IsContDiffCompatible X
inst_4 : NormedAddCommGroup Y
inst_5 : NormedSpace ℝ Y
inst_6 : DiffeologicalSpace Y
inst_7 : IsContDiffCompatible Y
inst_8 : FiniteDimensional ℝ X
f : X → Y
hf : DSmooth f
g : X ≃L[ℝ] EuclideanSpace ℝ (Fin (Module.finrank ℝ X)) := toEuclidean
⊢ ContDiff ℝ ∞ f
have rw : ContDiff ℝ (E := X) ∞
  (f ∘
    Function.comp (β := EuclideanSpace ℝ (Fin (Module.finrank ℝ X)))
      (⇑g.symm : (a : EuclideanSpace ℝ (Fin (Module.finrank ℝ X))) → X)
      (⇑g : (a : X) → EuclideanSpace ℝ (Fin (Module.finrank ℝ X))))
Tactic: rw [← Function.comp_id f, ← g.symm_comp_self]
-- Lean 4 proof step from Mathlib.Geometry.Diffeology.Basic (goal)
Goal:
X : Type u_1
d d' : DiffeologicalSpace X
h : d.toPlots = d'.toPlots
⊢ d = d'
have h₁ : ∀ (n : ℕ) (p : EuclideanSpace ℝ (Fin n) → X), IsPlot p ↔ IsPlot p
Tactic: ext n p