awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)))
⊢ Set.EqOn
    (↑(OpenPartialHomeomorph.trans (OpenPartialHomeomorph.symm (OpenPartialHomeomorph.univBall x ε))
          (OpenPartialHomeomorph.univBall x ε)) :
      EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
    (↑(OpenPartialHomeomorph.ofSet (OpenPartialHomeomorph.toPartialEquiv (OpenPartialHomeomorph.univBall x ε)).target
          ⋯) :
      EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
    (OpenPartialHomeomorph.toPartialEquiv
        (OpenPartialHomeomorph.trans (OpenPartialHomeomorph.symm (OpenPartialHomeomorph.univBall x ε))
          (OpenPartialHomeomorph.univBall x ε))).source

Tactic:
(OpenPartialHomeomorph.symm_trans_self (OpenPartialHomeomorph.univBall x ε)).2

Premises used: OpenPartialHomeomorph.univBall, OpenPartialHomeomorph.symm_trans_self, And.right
-- 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₁ :
  Metric.ball x ε =
    (OpenPartialHomeomorph.toPartialEquiv
        (OpenPartialHomeomorph.trans (OpenPartialHomeomorph.symm (OpenPartialHomeomorph.univBall x ε))
          (OpenPartialHomeomorph.univBall x ε))).source
⊢ 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:
convert! (OpenPartialHomeomorph.symm_trans_self (OpenPartialHomeomorph.univBall x ε)).2

Premises used: OpenPartialHomeomorph.univBall, OpenPartialHomeomorph.symm_trans_self, And.right
-- 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)))
⊢ Metric.ball x ε =
    (OpenPartialHomeomorph.toPartialEquiv
        (OpenPartialHomeomorph.trans (OpenPartialHomeomorph.symm (OpenPartialHomeomorph.univBall x ε))
          (OpenPartialHomeomorph.univBall x ε))).source

Tactic:
simp [OpenPartialHomeomorph.univBall_target x hε]

Premises used: OpenPartialHomeomorph.univBall_target
-- Module: Mathlib.Geometry.Diffeology.Basic
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[dTopology, dTopology] f

Tactic:
hf.continuous

Premises used: Diffeology.DSmooth.continuous
-- Module: Mathlib.Geometry.Diffeology.Basic
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
h₁ : inst_3 = dTopology
⊢ Continuous[inst, inst_3] f

Tactic:
convert! hf.continuous

Premises used: Diffeology.DSmooth.continuous
-- Module: Mathlib.Geometry.Diffeology.Basic
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 h₁ : inst = inst
⊢ inst = dTopology

Tactic:
rw [IsDTopologyCompatible.dTop_eq X]

Premises used: Diffeology.IsDTopologyCompatible.dTop_eq
-- Module: Mathlib.Geometry.Diffeology.Basic
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 h₁ : inst_3 = inst_3
⊢ inst_3 = dTopology

Tactic:
rw [IsDTopologyCompatible.dTop_eq Y]

Premises used: Diffeology.IsDTopologyCompatible.dTop_eq
-- Module: Mathlib.Geometry.Diffeology.Basic
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
let :
  ∀ (v : Set (EuclideanSpace ℝ (Fin n))) (hv : IsOpen v) (hxv : x ∈ v) (hv' : ContDiffOn ℝ ∞ x_1 v),
    ContDiffWithinAt ℝ ∞ x_1 u x
⊢ ContDiffWithinAt ℝ ∞ x_1 u x

Tactic:
let ⟨v, hv, hxv, hv'⟩ := h x hxu
-- Module: Mathlib.Geometry.Diffeology.Basic
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
v : Set (EuclideanSpace ℝ (Fin n))
hv : IsOpen v
hxv : x ∈ v
hv' : ContDiffOn ℝ ∞ x_1 v
⊢ ContDiffWithinAt ℝ ∞ x_1 u x

Tactic:
((hv' x hxv).contDiffAt (hv.mem_nhds hxv)).contDiffWithinAt

Premises used: ContDiffWithinAt.contDiffAt, IsOpen.mem_nhds, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Geometry.Diffeology.Basic
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
v : Set (EuclideanSpace ℝ (Fin n))
hv : IsOpen v
hxv : x ∈ v
hv' : ContDiffOn ℝ ∞ x_1 v
⊢ ContDiffWithinAt ℝ ∞ x_1 u x

Tactic:
exact ((hv' x hxv).contDiffAt (hv.mem_nhds hxv)).contDiffWithinAt

Premises used: ContDiffWithinAt.contDiffAt, IsOpen.mem_nhds, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Geometry.Diffeology.Basic
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)

Tactic:
⟨fun hu _ _ hp ↦ IsOpen.preimage (hp.continuous) hu, fun h ↦ ?_⟩

Premises used: ContDiff.continuous, Iff.intro, IsOpen.preimage
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
inst : NormedAddCommGroup X
inst_1 : NormedSpace ℝ X
inst_2 : FiniteDimensional ℝ X
u : Set X
refine :
  ∀ (h : ∀ {n : ℕ} (p : EuclideanSpace ℝ (Fin n) → X), ContDiff ℝ ∞ p → IsOpen (p ⁻¹' u)), TopologicalSpace.IsOpen u
⊢ TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ} (p : EuclideanSpace ℝ (Fin n) → X), ContDiff ℝ ∞ p → IsOpen (p ⁻¹' u)

Tactic:
refine ⟨fun hu _ _ hp ↦ IsOpen.preimage (hp.continuous) hu, fun h ↦ ?_⟩
-- Module: Mathlib.Geometry.Diffeology.Basic
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)
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))
⊢ TopologicalSpace.IsOpen u

Tactic:
rw [← toEuclidean.preimage_symm_preimage u]

Premises used: ContinuousLinearEquiv.preimage_symm_preimage, toEuclidean
-- Module: Mathlib.Geometry.Diffeology.Basic
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_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:
toEuclidean.continuous.isOpen_preimage _ (h _ toEuclidean.symm.contDiff)

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearEquiv.continuous, IsOpen, Continuous.isOpen_preimage, toEuclidean, ContinuousLinearEquiv.contDiff
-- Module: Mathlib.Geometry.Diffeology.Basic
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_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:
exact toEuclidean.continuous.isOpen_preimage _ (h _ toEuclidean.symm.contDiff)

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearEquiv.continuous, Continuous.isOpen_preimage, toEuclidean, ContinuousLinearEquiv.contDiff
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
inst : NormedAddCommGroup X
inst_1 : NormedSpace ℝ X
inst_2 : FiniteDimensional ℝ X
⊢ IsContDiffCompatible X

Tactic:
⟨Iff.rfl⟩

Premises used: Diffeology.IsContDiffCompatible.mk, Iff.rfl
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
inst : NormedAddCommGroup X
inst_1 : NormedSpace ℝ X
inst_2 : FiniteDimensional ℝ X
d : DiffeologicalSpace X
h_1 : IsContDiffCompatible X
h : ∀ (n : ℕ) (p : EuclideanSpace ℝ (Fin n) → X), IsPlot p ↔ IsPlot p
⊢ d = NormedSpace.toDiffeology X

Tactic:
ext n p
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
inst : NormedAddCommGroup X
inst_1 : NormedSpace ℝ X
inst_2 : FiniteDimensional ℝ X
d : DiffeologicalSpace X
h : IsContDiffCompatible X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
⊢ IsPlot p ↔ IsPlot p

Tactic:
IsContDiffCompatible.isPlot_iff

Premises used: Set.Mem, setOf, Diffeology.IsPlot, ContDiff, Diffeology.IsContDiffCompatible.isPlot_iff
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
inst : NormedAddCommGroup X
inst_1 : NormedSpace ℝ X
inst_2 : FiniteDimensional ℝ X
d : DiffeologicalSpace X
h : IsContDiffCompatible X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
⊢ IsPlot p ↔ IsPlot p

Tactic:
exact IsContDiffCompatible.isPlot_iff

Premises used: Diffeology.IsContDiffCompatible.isPlot_iff
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
inst : NormedAddCommGroup X
inst_1 : NormedSpace ℝ X
inst_2 : FiniteDimensional ℝ X
⊢ IsDTopologyCompatible X

Tactic:
⟨rfl⟩

Premises used: Diffeology.IsDTopologyCompatible.mk, rfl
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
inst : DiffeologicalSpace X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
hp : IsPlot p
⊢ DSmooth p

Tactic:
fun _ _ ↦ isPlot_reparam hp

Premises used: Set.Mem, setOf, Diffeology.IsPlot, ContDiff, Diffeology.isPlot_reparam, Diffeology.DSmooth
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
inst : DiffeologicalSpace X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
hp : DSmooth p
⊢ IsPlot p

Tactic:
hp n id <| contDiff_id (n := ∞)

Premises used: contDiff_id, id
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
inst : DiffeologicalSpace X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
⊢ IsPlot p ↔ DSmooth p

Tactic:
⟨IsPlot.dSmooth, DSmooth.isPlot⟩

Premises used: Diffeology.DSmooth.isPlot, Diffeology.IsPlot.dSmooth, Iff.intro
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
n : ℕ
⊢ IsPlot (X := EuclideanSpace ℝ (Fin n)) id

Tactic:
contDiff_id (n := ∞)

Premises used: contDiff_id, Set.Mem, setOf, Diffeology.IsPlot, ContDiff
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
n : ℕ
⊢ IsPlot (X := EuclideanSpace ℝ (Fin n)) (n := n) fun (x : EuclideanSpace ℝ (Fin n)) ↦ x

Tactic:
isPlot_id

Premises used: Diffeology.isPlot_id
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
inst : DiffeologicalSpace X
n : ℕ
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace ℝ X
inst_3 : IsContDiffCompatible X
p : EuclideanSpace ℝ (Fin n) → X
⊢ IsPlot p ↔ ContDiff ℝ ∞ p

Tactic:
IsContDiffCompatible.isPlot_iff

Premises used: Diffeology.IsContDiffCompatible.isPlot_iff
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
inst : DiffeologicalSpace X
n : ℕ
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace ℝ X
inst_3 : IsContDiffCompatible X
p : EuclideanSpace ℝ (Fin n) → X
hp : ContDiff ℝ ∞ p
⊢ IsPlot p

Tactic:
isPlot_iff_contDiff.2 hp

Premises used: Iff.mpr, Diffeology.isPlot_iff_contDiff
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
inst : DiffeologicalSpace X
n : ℕ
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace ℝ X
inst_3 : IsContDiffCompatible X
p : EuclideanSpace ℝ (Fin n) → X
hp : IsPlot p
⊢ ContDiff ℝ ∞ p

Tactic:
isPlot_iff_contDiff.1 hp

Premises used: Diffeology.isPlot_iff_contDiff, Iff.mp
-- Module: Mathlib.Geometry.Diffeology.Basic
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
f : X → Y
hf : ContDiff ℝ ∞ f
⊢ DSmooth f

Tactic:
fun _ _ hp ↦ (hf.comp hp.contDiff).isPlot

Premises used: ContDiff.comp, Diffeology.IsPlot.contDiff, Diffeology.DSmooth, ContDiff.isPlot
-- Module: Mathlib.Geometry.Diffeology.Basic
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
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))))
⊢ ContDiff ℝ ∞ f

Tactic:
rw [← Function.comp_id f, ← g.symm_comp_self]

Premises used: Function.comp_id, ContinuousLinearEquiv.symm_comp_self
-- Module: Mathlib.Geometry.Diffeology.Basic
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 ℝ (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:
(hf _ _ g.symm.contDiff.isPlot).contDiff.comp g.contDiff

Premises used: ContinuousLinearEquiv.symm, ContDiff.comp, Diffeology.IsPlot.contDiff, ContDiff.isPlot, ContinuousLinearEquiv.contDiff
-- Module: Mathlib.Geometry.Diffeology.Basic
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 ℝ (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:
exact (hf _ _ g.symm.contDiff.isPlot).contDiff.comp g.contDiff

Premises used: ContinuousLinearEquiv.symm, ContDiff.comp, Diffeology.IsPlot.contDiff, ContDiff.isPlot, ContinuousLinearEquiv.contDiff
-- Module: Mathlib.Geometry.Diffeology.Basic
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
⊢ DSmooth f ↔ ContDiff ℝ ∞ f

Tactic:
⟨DSmooth.contDiff, ContDiff.dSmooth⟩

Premises used: Iff.intro, ContDiff.dSmooth, Diffeology.DSmooth.contDiff
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
d d' : DiffeologicalSpace X
h : d.toPlots = d'.toPlots
h₁ : ∀ (n : ℕ) (p : EuclideanSpace ℝ (Fin n) → X), IsPlot p ↔ IsPlot p
⊢ d = d'

Tactic:
ext n p
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
d d' : DiffeologicalSpace X
h : d.toPlots = d'.toPlots
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
⊢ IsPlot p ↔ IsPlot p

Tactic:
Set.ext_iff.1 h ⟨n, p⟩

Premises used: Set.Mem, setOf, Diffeology.IsPlot, Iff.mp, DiffeologicalSpace.toPlots, Set.ext_iff, Sigma.mk
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
d d' : DiffeologicalSpace X
h : d.toPlots = d'.toPlots
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
⊢ IsPlot p ↔ IsPlot p

Tactic:
exact Set.ext_iff.1 h ⟨n, p⟩

Premises used: Iff.mp, Set.ext_iff, Sigma.mk
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
g : Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X))
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
hp :
  ∀ (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 : DiffeologicalSpace X),
                      g ⊆ d.toPlots → Sigma.mk (β := fun (n : ℕ) ↦ EuclideanSpace ℝ (Fin n) → X) m p ∈ d.toPlots}
                  (p ∘ f)
d : DiffeologicalSpace X
hd : g ⊆ d.toPlots
x : EuclideanSpace ℝ (Fin n)
let :
  ∀ (u : Set (EuclideanSpace ℝ (Fin n))) (hxu : IsOpen u) (hu : 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 : DiffeologicalSpace X),
                  g ⊆ d.toPlots → Sigma.mk (β := fun (n : ℕ) ↦ EuclideanSpace ℝ (Fin n) → X) m p ∈ d.toPlots}
              (p ∘ f)),
    ∃ (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)) (plots m) (p ∘ f)
⊢ ∃ (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)) (plots m) (p ∘ f)

Tactic:
let ⟨u, hxu, hu, hu'⟩ := hp x