awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : DiffeologicalSpace X
inst_1 : DiffeologicalSpace Y
f : X → Y
hf : DSmooth f
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)
⊢ Continuous[dTopology, dTopology] f

Tactic:
simp_rw [continuous_def, isOpen_iff_preimages_plots (X := X), isOpen_iff_preimages_plots (X := Y)]

Premises used: Diffeology.isOpen_iff_preimages_plots, continuous_def
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : DiffeologicalSpace X
inst_1 : DiffeologicalSpace Y
f : X → Y
hf : DSmooth f
⊢ ∀ (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:
fun u hu n p hp ↦ hu n (f ∘ p) (hf n p hp)

Premises used: Set.Mem, setOf, Function.comp, Set.preimage
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : DiffeologicalSpace X
inst_1 : DiffeologicalSpace Y
f : X → Y
hf : DSmooth f
⊢ ∀ (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:
exact fun u hu n p hp ↦ hu n (f ∘ p) (hf n p hp)
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : DiffeologicalSpace X
inst_1 : DiffeologicalSpace Y
f : X → Y
⊢ DSmooth f ↔ ∀ (n : ℕ) (p : EuclideanSpace ℝ (Fin n) → X), IsPlot p → IsPlot (f ∘ p)

Tactic:
Iff.rfl

Premises used: Iff.rfl, Diffeology.DSmooth
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
inst : DiffeologicalSpace X
⊢ DSmooth.{u_1, u_1} (X := X) id

Tactic:
simp [DSmooth]

Premises used: Diffeology.DSmooth
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
inst : DiffeologicalSpace X
⊢ DSmooth (Y := X) fun (x : X) ↦ x

Tactic:
dSmooth_id

Premises used: Diffeology.dSmooth_id
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : DiffeologicalSpace X
inst_1 : DiffeologicalSpace Y
inst_2 : DiffeologicalSpace Z
f : X → Y
g : Y → Z
hg : DSmooth g
hf : DSmooth f
⊢ DSmooth (g ∘ f)

Tactic:
fun _ _ hp ↦ hg _ _ (hf _ _ hp)

Premises used: Diffeology.DSmooth
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : DiffeologicalSpace X
inst_1 : DiffeologicalSpace Y
inst_2 : DiffeologicalSpace Z
f : X → Y
g : Y → Z
hg : DSmooth g
hf : DSmooth f
⊢ DSmooth.{u_1, u_3} (Y := Z) fun (x : X) ↦ g (f x)

Tactic:
hg.comp hf

Premises used: Diffeology.DSmooth.comp
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : DiffeologicalSpace X
inst_1 : DiffeologicalSpace Y
y : Y
⊢ DSmooth.{u_1, u_2} (Y := Y) fun (x : X) ↦ y

Tactic:
fun _ _ _ ↦ isPlot_const

Premises used: Diffeology.DSmooth, Diffeology.isPlot_const
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
d : DiffeologicalSpace X
t : TopologicalSpace X
h : dTopology = t
u : Set X
rw : TopologicalSpace.IsOpen u ↔ TopologicalSpace.IsOpen u
rw₁ 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)

Tactic:
rw [← d.isOpen_iff_preimages_plots, ← h]

Premises used: DiffeologicalSpace.isOpen_iff_preimages_plots
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
d : DiffeologicalSpace X
t : TopologicalSpace X
h : dTopology = t
h₁ : ∀ (x : ℕ) (x_1 : EuclideanSpace ℝ (Fin x) → X), Diffeology.IsPlot x_1 ↔ Diffeology.IsPlot x_1
⊢ d.replaceDTopology t h = d

Tactic:
ext
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
d : DiffeologicalSpace X
t : TopologicalSpace X
h : dTopology = t
x : ℕ
x_1 : EuclideanSpace ℝ (Fin x) → X
⊢ Diffeology.IsPlot x_1 ↔ Diffeology.IsPlot x_1

Tactic:
rfl
-- Module: Mathlib.Geometry.Diffeology.Basic
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

Tactic:
d.isPlotOn_univ.mp <| d.locality _ fun x _ ↦ ?_

Premises used: Set.Mem, setOf, Iff.mp, DiffeologicalSpace.CorePlotsOn.locality, DiffeologicalSpace.CorePlotsOn.isPlotOn_univ
-- Module: Mathlib.Geometry.Diffeology.Basic
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)
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
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n) → X)) {p : EuclideanSpace ℝ (Fin n) → X | d.isPlot p} p

Tactic:
refine d.isPlotOn_univ.mp <| d.locality _ fun x _ ↦ ?_

Premises used: Iff.mp, DiffeologicalSpace.CorePlotsOn.locality, DiffeologicalSpace.CorePlotsOn.isPlotOn_univ
-- Module: Mathlib.Geometry.Diffeology.Basic
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
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
⊢ ∃ (v : Set (EuclideanSpace ℝ (Fin n))) (hv : IsOpen v), x ∈ v ∧ d.isPlotOn (u := v) hv p

Tactic:
let ⟨u, hu, hxu, hu'⟩ := h x
-- Module: Mathlib.Geometry.Diffeology.Basic
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)
let :
  ∀ (ε : ℝ) (hε : ε > 0) (hε' : Metric.ball x ε ⊆ u),
    ∃ (v : Set (EuclideanSpace ℝ (Fin n))) (hv : IsOpen v), x ∈ v ∧ d.isPlotOn (u := v) hv p
⊢ ∃ (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
-- Module: Mathlib.Geometry.Diffeology.Basic
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)
⊢ ∀ (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')
-- Module: Mathlib.Geometry.Diffeology.Basic
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
⊢ ∀ (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

Premises used: OpenPartialHomeomorph.univBall_target
-- Module: Mathlib.Geometry.Diffeology.Basic
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' ∈ Metric.ball x ε
⊢ (↑(OpenPartialHomeomorph.univBall x ε) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) x' ∈ u

Tactic:
aesop
-- Module: Mathlib.Geometry.Diffeology.Basic
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
⊢ 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
-- Module: Mathlib.Geometry.Diffeology.Basic
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)))
⊢ 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)))

Tactic:
have h' := d.isPlotOn_reparam (Metric.isOpen_ball) (Set.mapsTo_univ _ _)
      (d.isPlotOn_univ.mpr h) (OpenPartialHomeomorph.contDiffOn_univBall_symm (c := x) (r := ε))
-- Module: Mathlib.Geometry.Diffeology.Basic
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

Tactic:
⟨_, Metric.isOpen_ball, Metric.mem_ball_self hε, (d.isPlotOn_congr _ ?_).mp h'⟩

Premises used: Metric.mem_ball_self, Metric.isOpen_ball, And.intro, DiffeologicalSpace.CorePlotsOn.isPlotOn_congr, Exists.intro, Iff.mp
-- Module: Mathlib.Geometry.Diffeology.Basic
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)))
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 ε)
⊢ ∃ (v : Set (EuclideanSpace ℝ (Fin n))) (hv : IsOpen v), x ∈ v ∧ d.isPlotOn (u := v) hv p

Tactic:
refine ⟨_, Metric.isOpen_ball, Metric.mem_ball_self hε, (d.isPlotOn_congr _ ?_).mp h'⟩
-- Module: Mathlib.Geometry.Diffeology.Basic
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)))
rw :
  Set.EqOn
    (p ∘
      (↑(OpenPartialHomeomorph.trans (OpenPartialHomeomorph.symm (OpenPartialHomeomorph.univBall x ε))
            (OpenPartialHomeomorph.univBall x ε)) :
        EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)))
    p (Metric.ball x ε)
⊢ 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:
rw [Function.comp_assoc, ← OpenPartialHomeomorph.coe_trans]

Premises used: OpenPartialHomeomorph.coe_trans, Function.comp_assoc
-- Module: Mathlib.Geometry.Diffeology.Basic
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)))
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 ε)
⊢ Set.EqOn
    (p ∘
      (↑(OpenPartialHomeomorph.trans (OpenPartialHomeomorph.symm (OpenPartialHomeomorph.univBall x ε))
            (OpenPartialHomeomorph.univBall x ε)) :
        EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)))
    p (Metric.ball x ε)

Tactic:
apply Set.EqOn.comp_left

Premises used: Set.EqOn.comp_left