-- Mathlib/Topology/Compactness/DeltaGeneratedSpace.lean
/-- A map out of a delta-generated space is continuous iff it preserves continuity of maps
  from ℝⁿ into X. -/
lemma DeltaGeneratedSpace.continuous_iff [DeltaGeneratedSpace X] {f : X → Y} :
    Continuous f ↔ ∀ (n : ℕ) (p : C(((Fin n) → ℝ), X)), Continuous (f ∘ p)

Proof state:
case mp
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : DeltaGeneratedSpace X
f : X → Y
h : ∀ (i : (n : ℕ) × C(Fin n → ℝ, X)), coinduced (f ∘ ⇑i.snd) inferInstance ≤ tY
n : ℕ
p : C(Fin n → ℝ, X)
⊢ coinduced (f ∘ ⇑p) Pi.topologicalSpace ≤ tY

Tactic:
apply h ⟨n, p⟩

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : DeltaGeneratedSpace X
f : X → Y
⊢ coinduced f tX ≤ tY ↔ ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), coinduced (f ∘ ⇑p) Pi.topologicalSpace ≤ tY

Tactic:
nth_rewrite 1 [eq_deltaGenerated (X := X), deltaGenerated]

Result:
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : DeltaGeneratedSpace X
f : X → Y
⊢ coinduced f (⨆ f, coinduced (⇑f.snd) inferInstance) ≤ tY ↔
    ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), coinduced (f ∘ ⇑p) Pi.topologicalSpace ≤ tY

Proof state:
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : DeltaGeneratedSpace X
f : X → Y
⊢ Continuous f ↔ ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), Continuous (f ∘ ⇑p)

Tactic:
simp_rw [continuous_iff_coinduced_le]

Result:
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : DeltaGeneratedSpace X
f : X → Y
⊢ coinduced f tX ≤ tY ↔ ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), coinduced (f ∘ ⇑p) Pi.topologicalSpace ≤ tY

Proof state:
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : DeltaGeneratedSpace X
f : X → Y
⊢ coinduced f (⨆ f, coinduced (⇑f.snd) inferInstance) ≤ tY ↔
    ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), coinduced (f ∘ ⇑p) Pi.topologicalSpace ≤ tY

Tactic:
simp [coinduced_compose]

Result:
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : DeltaGeneratedSpace X
f : X → Y
⊢ (∀ (i : (n : ℕ) × C(Fin n → ℝ, X)), coinduced (f ∘ ⇑i.snd) inferInstance ≤ tY) ↔
    ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), coinduced (f ∘ ⇑p) Pi.topologicalSpace ≤ tY

Proof state:
case mp
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : DeltaGeneratedSpace X
f : X → Y
⊢ (∀ (i : (n : ℕ) × C(Fin n → ℝ, X)), coinduced (f ∘ ⇑i.snd) inferInstance ≤ tY) →
    ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), coinduced (f ∘ ⇑p) Pi.topologicalSpace ≤ tY

Tactic:
intro h n p

Result:
case mp
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : DeltaGeneratedSpace X
f : X → Y
h : ∀ (i : (n : ℕ) × C(Fin n → ℝ, X)), coinduced (f ∘ ⇑i.snd) inferInstance ≤ tY
n : ℕ
p : C(Fin n → ℝ, X)
⊢ coinduced (f ∘ ⇑p) Pi.topologicalSpace ≤ tY

Proof state:
case mpr
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : DeltaGeneratedSpace X
f : X → Y
⊢ (∀ (n : ℕ) (p : C(Fin n → ℝ, X)), coinduced (f ∘ ⇑p) Pi.topologicalSpace ≤ tY) →
    ∀ (i : (n : ℕ) × C(Fin n → ℝ, X)), coinduced (f ∘ ⇑i.snd) inferInstance ≤ tY

Tactic:
rintro h ⟨n, p⟩

Result:
case mpr.mk
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : DeltaGeneratedSpace X
f : X → Y
h : ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), coinduced (f ∘ ⇑p) Pi.topologicalSpace ≤ tY
n : ℕ
p : C(Fin n → ℝ, X)
⊢ coinduced (f ∘ ⇑⟨n, p⟩.snd) inferInstance ≤ tY

Proof state:
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : DeltaGeneratedSpace X
f : X → Y
⊢ (∀ (i : (n : ℕ) × C(Fin n → ℝ, X)), coinduced (f ∘ ⇑i.snd) inferInstance ≤ tY) ↔
    ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), coinduced (f ∘ ⇑p) Pi.topologicalSpace ≤ tY

Tactic:
constructor

Result:
case mp
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : DeltaGeneratedSpace X
f : X → Y
⊢ (∀ (i : (n : ℕ) × C(Fin n → ℝ, X)), coinduced (f ∘ ⇑i.snd) inferInstance ≤ tY) →
    ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), coinduced (f ∘ ⇑p) Pi.topologicalSpace ≤ tY

case mpr
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : DeltaGeneratedSpace X
f : X → Y
⊢ (∀ (n : ℕ) (p : C(Fin n → ℝ, X)), coinduced (f ∘ ⇑p) Pi.topologicalSpace ≤ tY) →
    ∀ (i : (n : ℕ) × C(Fin n → ℝ, X)), coinduced (f ∘ ⇑i.snd) inferInstance ≤ tY

Proof state:
case mpr.mk
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : DeltaGeneratedSpace X
f : X → Y
h : ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), coinduced (f ∘ ⇑p) Pi.topologicalSpace ≤ tY
n : ℕ
p : C(Fin n → ℝ, X)
⊢ coinduced (f ∘ ⇑⟨n, p⟩.snd) inferInstance ≤ tY

Tactic:
apply h n p

Result:
no goals