awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Convex.Set
Goal:
K : Type u_4
X : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
t_1 : Finset X
x : X
t : Finset X
hx : x ∉ t
ht : t.Nonempty
ih : ∀ ⦃w : StdSimplex K X⦄ (hw : (↑t : Set X) ⊆ s) (hsw : t = w.weights.support), sConvexComb w ∈ s
w : StdSimplex K X
hw : (↑(Finset.cons x t hx) : Set X) ⊆ s
hsw : Finset.cons x t hx = w.weights.support
hwx : Ne.{u_4 + 1} (α := K) ((w.weights : (a : X) → K) x : K) (0 : K)
hwx' : ∃ (y : X), y ≠ x ∧ Ne.{u_4 + 1} (α := K) ((w.weights : (a : X) → K) y : K) (0 : K)
cons :
  sConvexComb
      (convexCombPair
        ((filter (fun (x_1 : X) ↦ Membership.mem (γ := Set X) {x} x_1) w.weights).sum fun (_x : X) (k : K) ↦ k)
        ((filter (fun (x_1 : X) ↦ x_1 ∉ {x}) w.weights).sum fun (_x : X) (k : K) ↦ k) ⋯ ⋯ ⋯ (w.restrict {x} ⋯)
        (w.restrict {x}ᶜ hwx')) ∈
    s
⊢ sConvexComb w ∈ s

Tactic:
rw [← w.convexCombPair_restrict_restrict_compl {x} (by simpa) hwx']

Premises used: Convexity.StdSimplex.convexCombPair_restrict_restrict_compl, Singleton.singleton
-- Module: Mathlib.Geometry.Convex.Set
Goal:
K : Type u_4
X : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
t_1 : Finset X
x : X
t : Finset X
hx : x ∉ t
ht : t.Nonempty
ih : ∀ ⦃w : StdSimplex K X⦄ (hw : (↑t : Set X) ⊆ s) (hsw : t = w.weights.support), sConvexComb w ∈ s
w : StdSimplex K X
hw : (↑(Finset.cons x t hx) : Set X) ⊆ s
hsw : Finset.cons x t hx = w.weights.support
hwx : Ne.{u_4 + 1} (α := K) ((w.weights : (a : X) → K) x : K) (0 : K)
hwx' : ∃ (y : X), y ≠ x ∧ Ne.{u_4 + 1} (α := K) ((w.weights : (a : X) → K) y : K) (0 : K)
cons :
  convexCombPair ((filter (fun (x_1 : X) ↦ x_1 = x) w.weights).sum fun (_x : X) (k : K) ↦ k)
      ((filter (fun (x_1 : X) ↦ ¬x_1 = x) w.weights).sum fun (_x : X) (k : K) ↦ k) ⋯ ⋯ ⋯ x
      (sConvexComb (w.restrict {x}ᶜ hwx')) ∈
    s
⊢ sConvexComb
      (convexCombPair
        ((filter (fun (x_1 : X) ↦ Membership.mem (γ := Set X) {x} x_1) w.weights).sum fun (_x : X) (k : K) ↦ k)
        ((filter (fun (x_1 : X) ↦ x_1 ∉ {x}) w.weights).sum fun (_x : X) (k : K) ↦ k) ⋯ ⋯ ⋯ (w.restrict {x} ⋯)
        (w.restrict {x}ᶜ hwx')) ∈
    s

Tactic:
simp only [mem_singleton_iff, StdSimplex.restrict_singleton, sConvexComb_convexCombPair,
    sConvexComb_single]

Premises used: Set.mem_singleton_iff, Convexity.StdSimplex.restrict_singleton, Convexity.ConvexSpace.sConvexComb_single, Convexity.sConvexComb_convexCombPair
-- Module: Mathlib.Geometry.Convex.Set
Goal:
K : Type u_4
X : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
t_1 : Finset X
x : X
t : Finset X
hx : x ∉ t
ht : t.Nonempty
ih : ∀ ⦃w : StdSimplex K X⦄ (hw : (↑t : Set X) ⊆ s) (hsw : t = w.weights.support), sConvexComb w ∈ s
w : StdSimplex K X
hw : (↑(Finset.cons x t hx) : Set X) ⊆ s
hsw : Finset.cons x t hx = w.weights.support
hwx : Ne.{u_4 + 1} (α := K) ((w.weights : (a : X) → K) x : K) (0 : K)
hwx' : ∃ (y : X), y ≠ x ∧ Ne.{u_4 + 1} (α := K) ((w.weights : (a : X) → K) y : K) (0 : K)
⊢ x ∈ (↑(Finset.cons x t hx) : Set X)

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.Set
Goal:
K : Type u_4
X : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
t_1 : Finset X
x : X
t : Finset X
hx : x ∉ t
ht : t.Nonempty
ih : ∀ ⦃w : StdSimplex K X⦄ (hw : (↑t : Set X) ⊆ s) (hsw : t = w.weights.support), sConvexComb w ∈ s
w : StdSimplex K X
hw : (↑(Finset.cons x t hx) : Set X) ⊆ s
hsw : Finset.cons x t hx = w.weights.support
hwx : Ne.{u_4 + 1} (α := K) ((w.weights : (a : X) → K) x : K) (0 : K)
hwx' : ∃ (y : X), y ≠ x ∧ Ne.{u_4 + 1} (α := K) ((w.weights : (a : X) → K) y : K) (0 : K)
grw : (↑t : Set X) ⊆ (↑(Finset.cons x t hx) : Set X)
grw₁ grw₂ : (↑t : Set X) ⊆ (↑t : Set X)
⊢ (↑t : Set X) ⊆ s

Tactic:
grw [← hw, ← Finset.subset_cons]

Premises used: Finset.subset_cons
-- Module: Mathlib.Geometry.Convex.Set
Goal:
K : Type u_4
X : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
t_1 : Finset X
x : X
t : Finset X
hx : x ∉ t
ht : t.Nonempty
ih : ∀ ⦃w : StdSimplex K X⦄ (hw : (↑t : Set X) ⊆ s) (hsw : t = w.weights.support), sConvexComb w ∈ s
w : StdSimplex K X
hw : (↑(Finset.cons x t hx) : Set X) ⊆ s
hsw : Finset.cons x t hx = w.weights.support
hwx : Ne.{u_4 + 1} (α := K) ((w.weights : (a : X) → K) x : K) (0 : K)
hwx' : ∃ (y : X), y ≠ x ∧ Ne.{u_4 + 1} (α := K) ((w.weights : (a : X) → K) y : K) (0 : K)
simp : t = {x_1 ∈ insert x t | ¬x_1 = x}
⊢ t = (w.restrict {x}ᶜ hwx').weights.support

Tactic:
simp [← hsw]
-- Module: Mathlib.Geometry.Convex.Set
Goal:
K : Type u_4
X : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
t_1 : Finset X
x : X
t : Finset X
hx : x ∉ t
ht : t.Nonempty
ih : ∀ ⦃w : StdSimplex K X⦄ (hw : (↑t : Set X) ⊆ s) (hsw : t = w.weights.support), sConvexComb w ∈ s
w : StdSimplex K X
hw : (↑(Finset.cons x t hx) : Set X) ⊆ s
hsw : Finset.cons x t hx = w.weights.support
hwx : Ne.{u_4 + 1} (α := K) ((w.weights : (a : X) → K) x : K) (0 : K)
hwx' : ∃ (y : X), y ≠ x ∧ Ne.{u_4 + 1} (α := K) ((w.weights : (a : X) → K) y : K) (0 : K)
⊢ t = {x_1 ∈ insert x t | ¬x_1 = x}

Tactic:
grind
-- Module: Mathlib.Geometry.Convex.Set
Goal:
K : Type u_4
X : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
t_1 : Finset X
x : X
t : Finset X
hx : x ∉ t
ht : t.Nonempty
ih : ∀ ⦃w : StdSimplex K X⦄ (hw : (↑t : Set X) ⊆ s) (hsw : t = w.weights.support), sConvexComb w ∈ s
w : StdSimplex K X
hw : (↑(Finset.cons x t hx) : Set X) ⊆ s
hsw : Finset.cons x t hx = w.weights.support
hwx : Ne.{u_4 + 1} (α := K) ((w.weights : (a : X) → K) x : K) (0 : K)
hwx' : ∃ (y : X), y ≠ x ∧ Ne.{u_4 + 1} (α := K) ((w.weights : (a : X) → K) y : K) (0 : K)
⊢ convexCombPair ((filter (fun (x_1 : X) ↦ x_1 = x) w.weights).sum fun (_x : X) (k : K) ↦ k)
      ((filter (fun (x_1 : X) ↦ ¬x_1 = x) w.weights).sum fun (_x : X) (k : K) ↦ k) ⋯ ⋯ ⋯ x
      (sConvexComb (w.restrict {x}ᶜ hwx')) ∈
    s

Tactic:
exact hs _ _ _ _ _ _ (hw <| by simp) _ <| ih (by grw [← hw, ← Finset.subset_cons])
    (by simp [← hsw]; grind)
-- Module: Mathlib.Geometry.Convex.Set
Goal:
K : Type u_4
X : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
w : StdSimplex K X
t : Finset X
hw : (↑t : Set X) ⊆ s
hsw : t = w.weights.support
ht : t.Nonempty
singleton : ∀ (x : X) ⦃w : StdSimplex K X⦄ (hw : (↑{x} : Set X) ⊆ s) (hsw : {x} = w.weights.support), sConvexComb w ∈ s
cons :
  ∀ (x : X) (t : Finset X) (hx : x ∉ t) (ht : t.Nonempty)
    (ih : ∀ ⦃w : StdSimplex K X⦄ (hw : (↑t : Set X) ⊆ s) (hsw : t = w.weights.support), sConvexComb w ∈ s)
    ⦃w : StdSimplex K X⦄ (hw : (↑(Finset.cons x t hx) : Set X) ⊆ s) (hsw : Finset.cons x t hx = w.weights.support),
    sConvexComb w ∈ s
⊢ sConvexComb w ∈ s

Tactic:
induction ht using Finset.Nonempty.cons_induction generalizing w with
  | singleton x => simp_all [eq_comm]
  | cons x t hx ht ih =>
  have hwx : w.weights x ≠ 0 := by simpa using congr(x ∈ $hsw)
  have hwx' : ∃ y ≠ x, w.weights y ≠ 0 := by
    obtain ⟨y, hy⟩ := ht
    exact ⟨y, ne_of_mem_of_not_mem hy hx, by simpa [hy] using congr(y ∈ $hsw)⟩
  rw [← w.convexCombPair_restrict_restrict_compl {x} (by simpa) hwx']
  simp only [mem_singleton_iff, StdSimplex.restrict_singleton, sConvexComb_convexCombPair,
    sConvexComb_single]
  exact hs _ _ _ _ _ _ (hw <| by simp) _ <| ih (by grw [← hw, ← Finset.subset_cons])
    (by simp [← hsw]; grind)

Premises used: eq_comm, Set.mem_singleton_iff, Convexity.StdSimplex.restrict_singleton, Convexity.ConvexSpace.sConvexComb_single, Singleton.singleton, Convexity.sConvexComb_convexCombPair
-- Module: Mathlib.Geometry.Convex.Set
Goal:
K : Type u_4
X : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
rintro : ∀ ⦃w : StdSimplex K X⦄ (hw : (↑w.weights.support : Set X) ⊆ s), sConvexComb w ∈ s
rintro₁ :
  ∀ ⦃w : StdSimplex K X⦄,
    let t := w.weights.support;
    ∀ (hw : (↑t : Set X) ⊆ s) (hsw : t = w.weights.support), sConvexComb w ∈ s
rintro₂ :
  ∀ ⦃w : StdSimplex K X⦄,
    let t := w.weights.support;
    ∀ (hw : (↑t : Set X) ⊆ s) (hsw : t = w.weights.support) (ht : t.Nonempty), sConvexComb w ∈ s
rintro₃ :
  ∀ ⦃w : StdSimplex K X⦄ (t : Finset X) (hw : (↑t : Set X) ⊆ s) (hsw : t = w.weights.support) (ht : t.Nonempty),
    sConvexComb w ∈ s
⊢ IsConvexSet K s

Tactic:
classical
  rintro w hw
  set t := w.weights.support with hsw
  have ht : t.Nonempty := w.support_weights_nonempty
  clear_value t
  induction ht using Finset.Nonempty.cons_induction generalizing w with
  | singleton x => simp_all [eq_comm]
  | cons x t hx ht ih =>
  have hwx : w.weights x ≠ 0 := by simpa using congr(x ∈ $hsw)
  have hwx' : ∃ y ≠ x, w.weights y ≠ 0 := by
    obtain ⟨y, hy⟩ := ht
    exact ⟨y, ne_of_mem_of_not_mem hy hx, by simpa [hy] using congr(y ∈ $hsw)⟩
  rw [← w.convexCombPair_restrict_restrict_compl {x} (by simpa) hwx']
  simp only [mem_singleton_iff, StdSimplex.restrict_singleton, sConvexComb_convexCombPair,
    sConvexComb_single]
  exact hs _ _ _ _ _ _ (hw <| by simp) _ <| ih (by grw [← hw, ← Finset.subset_cons])
    (by simp [← hsw]; grind)

Premises used: eq_comm, Set.mem_singleton_iff, Convexity.StdSimplex.restrict_singleton, Convexity.ConvexSpace.sConvexComb_single, Singleton.singleton, Convexity.sConvexComb_convexCombPair
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_4
d₁ d₂ : DiffeologicalSpace X
h : Eq.{u_4 + 1} (α := {n : ℕ} → (p : EuclideanSpace ℝ (Fin n) → X) → Prop) (@IsPlot X d₁) (@IsPlot X d₂)
obtain :
  ∀ (p₁ : (n : ℕ) → Set (EuclideanSpace ℝ (Fin n) → X))
    (constant_plots : ∀ {n : ℕ} (x : X), (fun (x_1 : EuclideanSpace ℝ (Fin n)) ↦ x) ∈ p₁ n)
    (plot_reparam :
      ∀ {n m : ℕ} {p : EuclideanSpace ℝ (Fin m) → X} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)}
        (hp : p ∈ p₁ m) (hf : ContDiff ℝ ∞ f), p ∘ f ∈ p₁ n)
    (locality :
      ∀ {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 → p ∘ f ∈ p₁ m),
        p ∈ p₁ n)
    (t₁ : TopologicalSpace X) (h₁ : ∀ {u : Set X}, TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ}, ∀ p ∈ p₁ n, IsOpen (p ⁻¹' u))
    (h :
      Eq.{u_4 + 1} (α := {n : ℕ} → (p : EuclideanSpace ℝ (Fin n) → X) → Prop)
        (@IsPlot X
          { plots := p₁, constant_plots := constant_plots, plot_reparam := plot_reparam, locality := locality,
            dTopology := t₁, isOpen_iff_preimages_plots := h₁ })
        (@IsPlot X d₂)),
    { plots := p₁, constant_plots := @constant_plots, plot_reparam := @plot_reparam, locality := @locality,
        dTopology := t₁, isOpen_iff_preimages_plots := @h₁ : DiffeologicalSpace X } =
      d₂
⊢ d₁ = d₂

Tactic:
obtain ⟨p₁, _, _, _, t₁, h₁⟩ := d₁
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_4
d₂ : DiffeologicalSpace X
p₁ : (n : ℕ) → Set (EuclideanSpace ℝ (Fin n) → X)
constant_plots : ∀ {n : ℕ} (x : X), (fun (x_1 : EuclideanSpace ℝ (Fin n)) ↦ x) ∈ p₁ n
plot_reparam :
  ∀ {n m : ℕ} {p : EuclideanSpace ℝ (Fin m) → X} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)}
    (hp : p ∈ p₁ m) (hf : ContDiff ℝ ∞ f), p ∘ f ∈ p₁ n
locality :
  ∀ {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 → p ∘ f ∈ p₁ m),
    p ∈ p₁ n
t₁ : TopologicalSpace X
h₁ : ∀ {u : Set X}, TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ}, ∀ p ∈ p₁ n, IsOpen (p ⁻¹' u)
h :
  Eq.{u_4 + 1} (α := {n : ℕ} → (p : EuclideanSpace ℝ (Fin n) → X) → Prop)
    (@IsPlot X
      { plots := p₁, constant_plots := constant_plots, plot_reparam := plot_reparam, locality := locality,
        dTopology := t₁, isOpen_iff_preimages_plots := h₁ })
    (@IsPlot X d₂)
obtain :
  ∀ (p₂ : (n : ℕ) → Set (EuclideanSpace ℝ (Fin n) → X))
    (constant_plots_1 : ∀ {n : ℕ} (x : X), (fun (x_1 : EuclideanSpace ℝ (Fin n)) ↦ x) ∈ p₂ n)
    (plot_reparam_1 :
      ∀ {n m : ℕ} {p : EuclideanSpace ℝ (Fin m) → X} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)}
        (hp : p ∈ p₂ m) (hf : ContDiff ℝ ∞ f), p ∘ f ∈ p₂ n)
    (locality_1 :
      ∀ {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 → p ∘ f ∈ p₂ m),
        p ∈ p₂ n)
    (t₂ : TopologicalSpace X) (h₂ : ∀ {u : Set X}, TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ}, ∀ p ∈ p₂ n, IsOpen (p ⁻¹' u))
    (h :
      Eq.{u_4 + 1} (α := {n : ℕ} → (p : EuclideanSpace ℝ (Fin n) → X) → Prop)
        (@IsPlot X
          { plots := p₁, constant_plots := constant_plots, plot_reparam := plot_reparam, locality := locality,
            dTopology := t₁, isOpen_iff_preimages_plots := h₁ })
        (@IsPlot X
          { plots := p₂, constant_plots := constant_plots_1, plot_reparam := plot_reparam_1, locality := locality_1,
            dTopology := t₂, isOpen_iff_preimages_plots := h₂ })),
    { plots := p₁, constant_plots := @constant_plots, plot_reparam := @plot_reparam, locality := @locality,
        dTopology := t₁, isOpen_iff_preimages_plots := @h₁ : DiffeologicalSpace X } =
      { plots := p₂, constant_plots := @constant_plots_1, plot_reparam := @plot_reparam_1, locality := @locality_1,
        dTopology := t₂, isOpen_iff_preimages_plots := @h₂ }
⊢ { plots := p₁, constant_plots := @constant_plots, plot_reparam := @plot_reparam, locality := @locality,
      dTopology := t₁, isOpen_iff_preimages_plots := @h₁ : DiffeologicalSpace X } =
    d₂

Tactic:
obtain ⟨p₂, _, _, _, t₂, h₂⟩ := d₂
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_4
p₁ : (n : ℕ) → Set (EuclideanSpace ℝ (Fin n) → X)
constant_plots : ∀ {n : ℕ} (x : X), (fun (x_1 : EuclideanSpace ℝ (Fin n)) ↦ x) ∈ p₁ n
plot_reparam :
  ∀ {n m : ℕ} {p : EuclideanSpace ℝ (Fin m) → X} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)}
    (hp : p ∈ p₁ m) (hf : ContDiff ℝ ∞ f), p ∘ f ∈ p₁ n
locality :
  ∀ {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 → p ∘ f ∈ p₁ m),
    p ∈ p₁ n
t₁ : TopologicalSpace X
h₁ : ∀ {u : Set X}, TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ}, ∀ p ∈ p₁ n, IsOpen (p ⁻¹' u)
p₂ : (n : ℕ) → Set (EuclideanSpace ℝ (Fin n) → X)
constant_plots_1 : ∀ {n : ℕ} (x : X), (fun (x_1 : EuclideanSpace ℝ (Fin n)) ↦ x) ∈ p₂ n
plot_reparam_1 :
  ∀ {n m : ℕ} {p : EuclideanSpace ℝ (Fin m) → X} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)}
    (hp : p ∈ p₂ m) (hf : ContDiff ℝ ∞ f), p ∘ f ∈ p₂ n
locality_1 :
  ∀ {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 → p ∘ f ∈ p₂ m),
    p ∈ p₂ n
t₂ : TopologicalSpace X
h₂ : ∀ {u : Set X}, TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ}, ∀ p ∈ p₂ n, IsOpen (p ⁻¹' u)
h :
  Eq.{u_4 + 1} (α := {n : ℕ} → (p : EuclideanSpace ℝ (Fin n) → X) → Prop)
    (@IsPlot X
      { plots := p₁, constant_plots := constant_plots, plot_reparam := plot_reparam, locality := locality,
        dTopology := t₁, isOpen_iff_preimages_plots := h₁ })
    (@IsPlot X
      { plots := p₂, constant_plots := constant_plots_1, plot_reparam := plot_reparam_1, locality := locality_1,
        dTopology := t₂, isOpen_iff_preimages_plots := h₂ })
e_dTopology : t₁ = t₂
⊢ { plots := p₁, constant_plots := @constant_plots, plot_reparam := @plot_reparam, locality := @locality,
      dTopology := t₁, isOpen_iff_preimages_plots := @h₁ : DiffeologicalSpace X } =
    { plots := p₂, constant_plots := @constant_plots_1, plot_reparam := @plot_reparam_1, locality := @locality_1,
      dTopology := t₂, isOpen_iff_preimages_plots := @h₂ }

Tactic:
congr 1
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_4
p₁ : (n : ℕ) → Set (EuclideanSpace ℝ (Fin n) → X)
constant_plots : ∀ {n : ℕ} (x : X), (fun (x_1 : EuclideanSpace ℝ (Fin n)) ↦ x) ∈ p₁ n
plot_reparam :
  ∀ {n m : ℕ} {p : EuclideanSpace ℝ (Fin m) → X} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)}
    (hp : p ∈ p₁ m) (hf : ContDiff ℝ ∞ f), p ∘ f ∈ p₁ n
locality :
  ∀ {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 → p ∘ f ∈ p₁ m),
    p ∈ p₁ n
t₁ : TopologicalSpace X
h₁ : ∀ {u : Set X}, TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ}, ∀ p ∈ p₁ n, IsOpen (p ⁻¹' u)
p₂ : (n : ℕ) → Set (EuclideanSpace ℝ (Fin n) → X)
constant_plots_1 : ∀ {n : ℕ} (x : X), (fun (x_1 : EuclideanSpace ℝ (Fin n)) ↦ x) ∈ p₂ n
plot_reparam_1 :
  ∀ {n m : ℕ} {p : EuclideanSpace ℝ (Fin m) → X} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)}
    (hp : p ∈ p₂ m) (hf : ContDiff ℝ ∞ f), p ∘ f ∈ p₂ n
locality_1 :
  ∀ {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 → p ∘ f ∈ p₂ m),
    p ∈ p₂ n
t₂ : TopologicalSpace X
h₂ : ∀ {u : Set X}, TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ}, ∀ p ∈ p₂ n, IsOpen (p ⁻¹' u)
h :
  Eq.{u_4 + 1} (α := {n : ℕ} → (p : EuclideanSpace ℝ (Fin n) → X) → Prop)
    (@IsPlot X
      { plots := p₁, constant_plots := constant_plots, plot_reparam := plot_reparam, locality := locality,
        dTopology := t₁, isOpen_iff_preimages_plots := h₁ })
    (@IsPlot X
      { plots := p₂, constant_plots := constant_plots_1, plot_reparam := plot_reparam_1, locality := locality_1,
        dTopology := t₂, isOpen_iff_preimages_plots := h₂ })
e_dTopology : ∀ (s : Set X), IsOpen[t₁] s ↔ IsOpen[t₂] s
⊢ t₁ = t₂

Tactic:
ext s
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_4
p₁ : (n : ℕ) → Set (EuclideanSpace ℝ (Fin n) → X)
constant_plots : ∀ {n : ℕ} (x : X), (fun (x_1 : EuclideanSpace ℝ (Fin n)) ↦ x) ∈ p₁ n
plot_reparam :
  ∀ {n m : ℕ} {p : EuclideanSpace ℝ (Fin m) → X} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)}
    (hp : p ∈ p₁ m) (hf : ContDiff ℝ ∞ f), p ∘ f ∈ p₁ n
locality :
  ∀ {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 → p ∘ f ∈ p₁ m),
    p ∈ p₁ n
t₁ : TopologicalSpace X
h₁ : ∀ {u : Set X}, TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ}, ∀ p ∈ p₁ n, IsOpen (p ⁻¹' u)
p₂ : (n : ℕ) → Set (EuclideanSpace ℝ (Fin n) → X)
constant_plots_1 : ∀ {n : ℕ} (x : X), (fun (x_1 : EuclideanSpace ℝ (Fin n)) ↦ x) ∈ p₂ n
plot_reparam_1 :
  ∀ {n m : ℕ} {p : EuclideanSpace ℝ (Fin m) → X} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)}
    (hp : p ∈ p₂ m) (hf : ContDiff ℝ ∞ f), p ∘ f ∈ p₂ n
locality_1 :
  ∀ {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 → p ∘ f ∈ p₂ m),
    p ∈ p₂ n
t₂ : TopologicalSpace X
h₂ : ∀ {u : Set X}, TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ}, ∀ p ∈ p₂ n, IsOpen (p ⁻¹' u)
h :
  Eq.{u_4 + 1} (α := {n : ℕ} → (p : EuclideanSpace ℝ (Fin n) → X) → Prop)
    (@IsPlot X
      { plots := p₁, constant_plots := constant_plots, plot_reparam := plot_reparam, locality := locality,
        dTopology := t₁, isOpen_iff_preimages_plots := h₁ })
    (@IsPlot X
      { plots := p₂, constant_plots := constant_plots_1, plot_reparam := plot_reparam_1, locality := locality_1,
        dTopology := t₂, isOpen_iff_preimages_plots := h₂ })
s : Set X
⊢ IsOpen[t₁] s ↔ IsOpen[t₂] s

Tactic:
exact ((show p₁ = p₂ from h) ▸ @h₁ s).trans (@h₂ s).symm
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
inst : DiffeologicalSpace X
n : ℕ
x : X
⊢ IsPlot.{u_1} (X := X) (n := n) fun (x_1 : EuclideanSpace ℝ (Fin n)) ↦ x

Tactic:
DiffeologicalSpace.constant_plots x

Premises used: Diffeology.IsPlot, DiffeologicalSpace.constant_plots
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
inst : DiffeologicalSpace X
n m : ℕ
p : EuclideanSpace ℝ (Fin m) → X
f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)
hp : IsPlot p
hf : ContDiff ℝ ∞ f
⊢ IsPlot (p ∘ f)

Tactic:
DiffeologicalSpace.plot_reparam hp hf

Premises used: Diffeology.IsPlot, DiffeologicalSpace.plot_reparam
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : DiffeologicalSpace X
inst_1 : DiffeologicalSpace Y
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
f : X → Y
hp : IsPlot p
hf : DSmooth f
⊢ IsPlot (f ∘ p)

Tactic:
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
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
f : X → Y
hp : IsPlot p
hf : DSmooth f
⊢ IsPlot.{u_2} (X := Y) (n := n) fun (x : EuclideanSpace ℝ (Fin n)) ↦ f (p x)

Tactic:
hf n p hp
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
inst : DiffeologicalSpace X
u : Set X
⊢ IsOpen[dTopology] u ↔ ∀ (n : ℕ) (p : EuclideanSpace ℝ (Fin n) → X), IsPlot p → IsOpen (p ⁻¹' u)

Tactic:
DiffeologicalSpace.isOpen_iff_preimages_plots

Premises used: Diffeology.IsPlot, IsOpen, DiffeologicalSpace.isOpen_iff_preimages_plots
-- Module: Mathlib.Geometry.Diffeology.Basic
Goal:
X : Type u_1
inst : DiffeologicalSpace X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
hp : IsPlot p
⊢ Continuous[_, dTopology] p

Tactic:
continuous_def.2 fun _ hu ↦ isOpen_iff_preimages_plots.1 hu n p hp

Premises used: Iff.mpr, Diffeology.isOpen_iff_preimages_plots, Iff.mp, continuous_def