awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
t : Set (↑s : Type u)
ht : IsClosed[instTopologicalSpaceSubtype] t
⊢ ∃ (c : Set X), IsClosed[inst] c ∧ Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t = c ∩ s

Tactic:
simpa using IsInducing.subtypeVal.image_eq_isClosed_inter_range ht

Premises used: Topology.IsInducing.image_eq_isClosed_inter_range, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsOpen[inst] s
h : IsOpen[instTopologicalSpaceSubtype] (s ↓∩ t)
⊢ IsOpen[inst] (s ∩ t)

Tactic:
simpa using hs.isOpenMap_subtype_val _ h

Premises used: IsOpen.isOpenMap_subtype_val
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsClosed[inst] s
h : IsClosed[instTopologicalSpaceSubtype] (s ↓∩ t)
⊢ IsClosed[inst] (s ∩ t)

Tactic:
simpa using hs.isClosedMap_subtype_val _ h

Premises used: IsClosed.isClosedMap_subtype_val
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
r : X → X → Prop
⊢ IsQuotientMap (Quot.mk r)

Tactic:
⟨⟨rfl⟩, Quot.exists_rep⟩

Premises used: Topology.IsCoinducing.mk, Quot.exists_rep, Topology.IsQuotientMap.mk, rfl
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
r : X → X → Prop
⊢ Continuous[inst, instTopologicalSpaceQuot] (Quot.mk r)

Tactic:
continuous_coinduced_rng

Premises used: continuous_coinduced_rng
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
r : X → X → Prop
f : X → Y
hr : ∀ (a b : X), r a b → f a = f b
h : Continuous[inst, inst_1] f
⊢ Continuous[instTopologicalSpaceQuot, inst_1] (Quot.lift (r := r) f hr)

Tactic:
continuous_coinduced_dom.2 h

Premises used: Iff.mpr, continuous_coinduced_dom
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
r : X → X → Prop
r' : Y → Y → Prop
f : X → Y
hr : ∀ (a b : X), r a b → r' (f a) (f b)
h : Continuous[inst, inst_1] f
⊢ Continuous[instTopologicalSpaceQuot, instTopologicalSpaceQuot] (Quot.map (ra := r) (rb := r') f hr)

Tactic:
continuous_quot_lift _ (continuous_quot_mk.comp h)

Premises used: continuous_quot_lift, Continuous.comp, continuous_quot_mk, Quot.map
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Setoid X
⊢ IsQuotientMap.{u, u} (X := X) (Y := Quotient s) Quotient.mk'

Tactic:
isQuotientMap_quot_mk

Premises used: Quotient, Quotient.mk', isQuotientMap_quot_mk
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Setoid X
⊢ Continuous[inst, instTopologicalSpaceQuotient] Quotient.mk'

Tactic:
continuous_coinduced_rng

Premises used: continuous_coinduced_rng
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Setoid X
f : X → Y
h : Continuous[inst, inst_1] f
hs : ∀ (a b : X), a ≈ b → f a = f b
⊢ Continuous[instTopologicalSpaceQuotient, inst_1] (Quotient.lift f hs)

Tactic:
continuous_coinduced_dom.2 h

Premises used: Iff.mpr, continuous_coinduced_dom
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Setoid X
f : X → Y
h : Continuous[inst, inst_1] f
hs : ∀ (a b : X), (s : X → X → Prop) a b → f a = f b
⊢ Continuous[instTopologicalSpaceQuotient, inst_1] fun (x : Quotient s) ↦ x.liftOn' f hs

Tactic:
h.quotient_lift hs

Premises used: Quotient.liftOn', Continuous.quotient_lift
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Setoid X
t : Setoid Y
f : X → Y
hf : Continuous[inst, inst_1] f
H : ((⇑s : X → X → Prop) ⇒ (⇑t : Y → Y → Prop)) f f
⊢ Continuous[instTopologicalSpaceQuotient, instTopologicalSpaceQuotient] (Quotient.map' f H)

Tactic:
(continuous_quotient_mk'.comp hf).quotient_lift _

Premises used: continuous_quotient_mk', Continuous.comp, Quotient, Quotient.mk', Quot.map, Quotient.map', Continuous.quotient_lift
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
ι : Type u_5
A : ι → Type u_6
inst : TopologicalSpace X
T : (i : ι) → TopologicalSpace (A i)
f : X → (i : ι) → A i
⊢ Continuous[inst, Pi.topologicalSpace] f ↔ ∀ (i : ι), Continuous[inst, T i] fun (a : X) ↦ f a i

Tactic:
simp only [continuous_iInf_rng, continuous_induced_rng, comp_def]

Premises used: continuous_iInf_rng, Function.comp_def, continuous_induced_rng
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
ι : Type u_5
A : ι → Type u_6
inst : TopologicalSpace X
T : (i : ι) → TopologicalSpace (A i)
f : X → (i : ι) → A i
h : ∀ (i : ι), Continuous[inst, T i] fun (a : X) ↦ f a i
⊢ Continuous[inst, Pi.topologicalSpace] f

Tactic:
continuous_pi_iff.2 h

Premises used: Iff.mpr, continuous_pi_iff
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : ι
⊢ Continuous[Pi.topologicalSpace, T i] fun (p : (i : ι) → A i) ↦ p i

Tactic:
continuous_iInf_dom continuous_induced_dom

Premises used: continuous_induced_dom, continuous_iInf_dom
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
κ : Type u_8
ρ : κ → ι → Type u_9
inst : (j : κ) → (i : ι) → TopologicalSpace (ρ j i)
j : κ
i : ι
⊢ Continuous[Pi.topologicalSpace, inst j i] fun (p : (j : κ) → (i : ι) → ρ j i) ↦ p j i

Tactic:
(continuous_apply i).comp (continuous_apply j)

Premises used: Continuous.comp, continuous_apply
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : ι
x : (i : ι) → A i
⊢ ContinuousAt (Y := A i) (fun (p : (i : ι) → A i) ↦ p i) x

Tactic:
(continuous_apply i).continuousAt

Premises used: Continuous.continuousAt, continuous_apply
-- Module: Mathlib.Topology.Constructions
Goal:
Y : Type v
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
l : Filter Y
f : Y → (i : ι) → A i
x : (i : ι) → A i
h : Tendsto f l (𝓝 x)
i : ι
⊢ Tendsto (fun (a : Y) ↦ f a i) l (𝓝 (x i))

Tactic:
(continuousAt_apply i _).tendsto.comp h

Premises used: ContinuousAt.tendsto, continuousAt_apply, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
T : (i : ι) → TopologicalSpace (A i)
inst : (i : ι) → TopologicalSpace (B i)
f : (i : ι) → A i → B i
hf : ∀ (i : ι), Continuous[T i, inst i] (f i)
⊢ Continuous[Pi.topologicalSpace, Pi.topologicalSpace] (Pi.map (α := A) (β := B) f)

Tactic:
continuous_pi fun i ↦ (hf i).comp (continuous_apply i)

Premises used: Continuous.comp, continuous_pi, continuous_apply
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
a : (i : ι) → A i
⊢ 𝓝 a = Filter.pi (α := A) fun (i : ι) ↦ 𝓝 (a i)

Tactic:
simp only [nhds_iInf, nhds_induced, Filter.pi]

Premises used: nhds_iInf, nhds_induced, Filter.pi
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
T : (i : ι) → TopologicalSpace (A i)
inst : (i : ι) → TopologicalSpace (B i)
f : (i : ι) → A i → B i
hfo : ∀ (i : ι), IsOpenMap (f i)
hsurj : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
⊢ IsOpenMap (Pi.map (α := A) (β := B) f)

Tactic:
IsOpenMap.of_nhds_le fun x ↦ ?_

Premises used: IsOpenMap.of_nhds_le
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
T : (i : ι) → TopologicalSpace (A i)
inst : (i : ι) → TopologicalSpace (B i)
f : (i : ι) → A i → B i
hfo : ∀ (i : ι), IsOpenMap (f i)
hsurj : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
refine : ∀ (x : (i : ι) → A i), 𝓝 (Pi.map (α := A) (β := B) f x) ≤ map (Pi.map (α := A) (β := B) f) (𝓝 x)
⊢ IsOpenMap (Pi.map (α := A) (β := B) f)

Tactic:
refine IsOpenMap.of_nhds_le fun x ↦ ?_

Premises used: IsOpenMap.of_nhds_le
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
T : (i : ι) → TopologicalSpace (A i)
inst : (i : ι) → TopologicalSpace (B i)
f : (i : ι) → A i → B i
hfo : ∀ (i : ι), IsOpenMap (f i)
hsurj : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
x : (i : ι) → A i
rw :
  LE.le (α := Filter ((i : ι) → B i)) (Filter.pi (α := B) fun (i : ι) ↦ 𝓝 (Pi.map (α := A) (β := B) f x i))
    (Filter.pi (α := B) fun (i : ι) ↦ map (f i) (𝓝 (x i)))
⊢ 𝓝 (Pi.map (α := A) (β := B) f x) ≤ map (Pi.map (α := A) (β := B) f) (𝓝 x)

Tactic:
rw [nhds_pi, nhds_pi, map_piMap_pi hsurj]

Premises used: nhds_pi, Filter.map_piMap_pi
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
T : (i : ι) → TopologicalSpace (A i)
inst : (i : ι) → TopologicalSpace (B i)
f : (i : ι) → A i → B i
hfo : ∀ (i : ι), IsOpenMap (f i)
hsurj : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
x : (i : ι) → A i
⊢ LE.le (α := Filter ((i : ι) → B i)) (Filter.pi (α := B) fun (i : ι) ↦ 𝓝 (Pi.map (α := A) (β := B) f x i))
    (Filter.pi (α := B) fun (i : ι) ↦ map (f i) (𝓝 (x i)))

Tactic:
Filter.pi_mono fun i ↦ (hfo i).nhds_le _

Premises used: IsOpenMap.nhds_le, Filter.pi_mono
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
T : (i : ι) → TopologicalSpace (A i)
inst : (i : ι) → TopologicalSpace (B i)
f : (i : ι) → A i → B i
hfo : ∀ (i : ι), IsOpenMap (f i)
hsurj : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
x : (i : ι) → A i
⊢ LE.le (α := Filter ((i : ι) → B i)) (Filter.pi (α := B) fun (i : ι) ↦ 𝓝 (Pi.map (α := A) (β := B) f x i))
    (Filter.pi (α := B) fun (i : ι) ↦ map (f i) (𝓝 (x i)))

Tactic:
exact Filter.pi_mono fun i ↦ (hfo i).nhds_le _

Premises used: IsOpenMap.nhds_le, Filter.pi_mono
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
T : (i : ι) → TopologicalSpace (A i)
inst : (i : ι) → TopologicalSpace (B i)
f : (i : ι) → A i → B i
hf : ∀ (i : ι), IsOpenQuotientMap (f i)
⊢ IsOpenQuotientMap (Pi.map (α := A) (β := B) f)

Tactic:
⟨.piMap fun i ↦ (hf i).1, .piMap fun i ↦ (hf i).2, .piMap (fun i ↦ (hf i).3) <|
    .of_forall fun i ↦ (hf i).1⟩

Premises used: IsOpenQuotientMap.continuous, IsOpenQuotientMap.mk, Continuous.piMap, Filter.Eventually.of_forall, IsOpenQuotientMap.surjective, IsOpenMap.piMap, Function.Surjective.piMap, IsOpenQuotientMap.isOpenMap
-- Module: Mathlib.Topology.Constructions
Goal:
Y : Type v
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
f : Y → (i : ι) → A i
g : (i : ι) → A i
u : Filter Y
rw : Tendsto f u (Filter.pi (α := A) fun (i : ι) ↦ 𝓝 (g i)) ↔ ∀ (x : ι), Tendsto (fun (i : Y) ↦ f i x) u (𝓝 (g x))
rw₁ rw₂ : (∀ (i : ι), Tendsto (fun (x : Y) ↦ f x i) u (𝓝 (g i))) ↔ ∀ (x : ι), Tendsto (fun (i : Y) ↦ f i x) u (𝓝 (g x))
⊢ Tendsto f u (𝓝 g) ↔ ∀ (x : ι), Tendsto (fun (i : Y) ↦ f i x) u (𝓝 (g x))

Tactic:
rw [nhds_pi, Filter.tendsto_pi]

Premises used: nhds_pi, Filter.tendsto_pi
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
ι : Type u_5
A : ι → Type u_6
inst : TopologicalSpace X
T : (i : ι) → TopologicalSpace (A i)
f : X → (i : ι) → A i
x : X
⊢ ContinuousAt f x ↔ ∀ (i : ι), ContinuousAt.{u, u_6} (Y := A i) (fun (y : X) ↦ f y i) x

Tactic:
tendsto_pi_nhds

Premises used: ContinuousAt, tendsto_pi_nhds
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
ι : Type u_5
A : ι → Type u_6
inst : TopologicalSpace X
T : (i : ι) → TopologicalSpace (A i)
f : X → (i : ι) → A i
x : X
hf : ∀ (i : ι), ContinuousAt.{u, u_6} (Y := A i) (fun (y : X) ↦ f y i) x
⊢ ContinuousAt f x

Tactic:
continuousAt_pi.2 hf

Premises used: Iff.mpr, continuousAt_pi
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
T : (i : ι) → TopologicalSpace (A i)
inst : (i : ι) → TopologicalSpace (B i)
f : (i : ι) → A i → B i
x : (i : ι) → A i
hf : ∀ (i : ι), ContinuousAt (f i) (x i)
⊢ ContinuousAt (Pi.map (α := A) (β := B) f) x

Tactic:
continuousAt_pi.2 fun i ↦ (hf i).comp (continuousAt_apply i x)

Premises used: Iff.mpr, continuousAt_pi, ContinuousAt.comp, continuousAt_apply
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
T : (i : ι) → TopologicalSpace (A i)
inst : (i : ι) → TopologicalSpace (B i)
f : (i : ι) → A i → B i
hf : ∀ (i : ι), IsInducing (f i)
⊢ IsInducing (Pi.map (α := A) (β := B) f)

Tactic:
simp [isInducing_iff_nhds, nhds_pi, (hf _).nhds_eq_comap, Filter.pi_comap]

Premises used: Topology.IsInducing.nhds_eq_comap, nhds_pi, Filter.pi_comap, Topology.isInducing_iff_nhds
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
T : (i : ι) → TopologicalSpace (A i)
inst : (i : ι) → TopologicalSpace (B i)
f : (i : ι) → A i → B i
hf : ∀ (i : ι), IsEmbedding (f i)
⊢ IsEmbedding (Pi.map (α := A) (β := B) f)

Tactic:
⟨.piMap fun i ↦ (hf i).1, .piMap fun i ↦ (hf i).2⟩

Premises used: Topology.IsEmbedding.injective, Topology.IsInducing.piMap, Function.Injective.piMap, Topology.IsEmbedding.toIsInducing, Topology.IsEmbedding.mk
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
ι' : Type u_9
φ : ι' → ι
⊢ Continuous[topologicalSpace, topologicalSpace] fun (f : (i : ι) → A i) (j : ι') ↦ f (φ j)

Tactic:
continuous_pi fun j ↦ continuous_apply (φ j)

Premises used: continuous_pi, continuous_apply
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
ι : Type u_5
inst : TopologicalSpace X
ι' : Type u_9
φ : ι' → ι
⊢ Continuous[topologicalSpace, topologicalSpace] fun (x : ι → X) ↦ x ∘ φ

Tactic:
Pi.continuous_precomp' φ

Premises used: Pi.continuous_precomp'
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
X : ι → Type u_9
inst : (i : ι) → TopologicalSpace (X i)
g : (i : ι) → A i → X i
hg : ∀ (i : ι), Continuous[T i, inst i] (g i)
⊢ Continuous[topologicalSpace, topologicalSpace] fun (f : (i : ι) → A i) (i : ι) ↦ g i (f i)

Tactic:
continuous_pi fun i ↦ (hg i).comp <| continuous_apply i

Premises used: Continuous.comp, continuous_pi, continuous_apply
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
ι : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
g : X → Y
hg : Continuous[inst, inst_1] g
⊢ Continuous[topologicalSpace, topologicalSpace] fun (x : ι → X) ↦ g ∘ x

Tactic:
Pi.continuous_postcomp' fun _ ↦ hg

Premises used: Pi.continuous_postcomp'
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
ι' : Type u_9
φ : ι' → ι
⊢ Eq (α := TopologicalSpace ((i : ι) → A i))
    (induced (Y := (j : ι') → A (φ j)) (fun (f : (i : ι) → A i) (j : ι') ↦ f (φ j))
      (topologicalSpace (Y := fun (j : ι') ↦ A (φ j))))
    (⨅ (i' : ι'), induced (eval (β := A) (φ i')) (T (φ i')))

Tactic:
simp [Pi.topologicalSpace, induced_iInf, induced_compose, comp_def]

Premises used: Pi.topologicalSpace, induced_compose, Function.comp_def, induced_iInf
-- Module: Mathlib.Topology.Constructions
Goal:
Y : Type v
ι : Type u_5
inst : TopologicalSpace Y
ι' : Type u_9
φ : ι' → ι
⊢ Eq (α := TopologicalSpace (ι → Y))
    (induced (Y := ι' → Y) (fun (x : ι → Y) ↦ x ∘ φ) (topologicalSpace (Y := fun (a : ι') ↦ Y)))
    (⨅ (i' : ι'), induced (eval (β := fun (a : ι) ↦ Y) (φ i')) inst)

Tactic:
induced_precomp' φ

Premises used: Pi.induced_precomp'
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
S : Set ι
⊢ Continuous[topologicalSpace, topologicalSpace] (S.restrict (π := A))

Tactic:
Pi.continuous_precomp' ((↑) : S → ι)

Premises used: Pi.continuous_precomp', Set.restrict, Subtype.val
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s t : Set ι
hst : s ⊆ t
⊢ Continuous[topologicalSpace, topologicalSpace] (restrict₂ (π := A) (s := s) (t := t) hst)

Tactic:
continuous_pi fun _ ↦ continuous_apply _

Premises used: continuous_pi, Subtype.mk, continuous_apply, Set.restrict₂._proof_1, Subtype.val
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Finset ι
⊢ Continuous[Pi.topologicalSpace, Pi.topologicalSpace] (s.restrict (π := A))

Tactic:
continuous_pi fun _ ↦ continuous_apply _

Premises used: continuous_pi, continuous_apply, Subtype.val
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s t : Finset ι
hst : s ⊆ t
⊢ Continuous[Pi.topologicalSpace, Pi.topologicalSpace] (restrict₂ (π := A) hst)

Tactic:
continuous_pi fun _ ↦ continuous_apply _

Premises used: continuous_pi, Subtype.mk, continuous_apply, Finset.restrict₂._proof_1, Subtype.val
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Z : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Z
s : Set X
f : X → Z
hf : Continuous[inst, inst_1] f
⊢ Continuous[instTopologicalSpaceSubtype, inst_1] (s.restrict (π := fun (a : X) ↦ Z) f)

Tactic:
hf.comp continuous_subtype_val

Premises used: continuous_subtype_val, Continuous.comp, Set.restrict
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Z : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Z
s t : Set X
hst : s ⊆ t
f : (↑t : Type u) → Z
hf : Continuous[instTopologicalSpaceSubtype, inst_1] f
⊢ Continuous[instTopologicalSpaceSubtype, inst_1] (restrict₂ (π := fun (x : X) ↦ Z) (s := s) (t := t) hst f)

Tactic:
hf.comp (continuous_inclusion hst)

Premises used: Continuous.comp, continuous_inclusion, Set.restrict₂
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Z : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Z
s : Finset X
f : X → Z
hf : Continuous[inst, inst_1] f
⊢ Continuous[instTopologicalSpaceSubtype, inst_1] (s.restrict (π := fun (i : X) ↦ Z) f)

Tactic:
hf.comp continuous_subtype_val

Premises used: continuous_subtype_val, Continuous.comp, Finset.restrict
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Z : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Z
s t : Finset X
hst : s ⊆ t
f : ↥t → Z
hf : Continuous[instTopologicalSpaceSubtype, inst_1] f
⊢ Continuous[instTopologicalSpaceSubtype, inst_1] (restrict₂ (π := fun (x : X) ↦ Z) hst f)

Tactic:
hf.comp (continuous_inclusion hst)

Premises used: Continuous.comp, continuous_inclusion, Finset.restrict₂
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
S : Set ι
⊢ Eq (α := TopologicalSpace ((a : ι) → A a))
    (induced (S.restrict (π := A)) (topologicalSpace (Y := fun (a : (↑S : Type u_5)) ↦ A (↑a : ι))))
    (⨅ i ∈ S, induced (eval (β := A) i) (T i))

Tactic:
simp +unfoldPartialApp [← iInf_subtype'', ← induced_precomp' ((↑) : S → ι),
    restrict]

Premises used: iInf_subtype'', Pi.induced_precomp', Set.restrict, Subtype.val
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
𝔖 : Set (Set ι)
simp_rw :
  Eq (α := TopologicalSpace ((a : ι) → A a)) (⨅ i ∈ ⋃₀ 𝔖, induced (eval (β := A) i) (T i))
    (⨅ S ∈ 𝔖, ⨅ i ∈ S, induced (eval (β := A) i) (T i))
⊢ Eq (α := TopologicalSpace ((a : ι) → A a))
    (induced ((⋃₀ 𝔖).restrict (π := A)) (topologicalSpace (Y := fun (i : (↑(⋃₀ 𝔖) : Type u_5)) ↦ A (↑i : ι))))
    (⨅ S ∈ 𝔖, induced (S.restrict (π := A)) (topologicalSpace (Y := fun (a : (↑S : Type u_5)) ↦ A (↑a : ι))))

Tactic:
simp_rw [Pi.induced_restrict, iInf_sUnion]

Premises used: Pi.induced_restrict, iInf_sUnion
-- Module: Mathlib.Topology.Constructions
Goal:
Y : Type v
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst : DecidableEq ι
l : Filter Y
f : Y → (i : ι) → A i
x : (i : ι) → A i
hf : Tendsto f l (𝓝 x)
i : ι
g : Y → A i
xi : A i
hg : Tendsto g l (𝓝 xi)
j : ι
inl :
  ∀ {g : Y → A j} {xi : A j} (hg : Tendsto g l (𝓝 xi)),
    Tendsto (fun (i : Y) ↦ Function.update (β := A) (f i) j (g i) j) l (𝓝 (Function.update (β := A) x j xi j))
inr :
  ∀ (hj : j ≠ i),
    Tendsto (fun (i_1 : Y) ↦ Function.update (β := A) (f i_1) i (g i_1) j) l (𝓝 (Function.update (β := A) x i xi j))
⊢ Tendsto (fun (i_1 : Y) ↦ Function.update (β := A) (f i_1) i (g i_1) j) l (𝓝 (Function.update (β := A) x i xi j))

Tactic:
rcases eq_or_ne j i with (rfl | hj)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.Constructions
Goal:
Y : Type v
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst : DecidableEq ι
l : Filter Y
f : Y → (i : ι) → A i
x : (i : ι) → A i
hf : Tendsto f l (𝓝 x)
j : ι
g : Y → A j
xi : A j
hg : Tendsto g l (𝓝 xi)
⊢ Tendsto (fun (i : Y) ↦ Function.update (β := A) (f i) j (g i) j) l (𝓝 (Function.update (β := A) x j xi j))

Tactic:
simp [*, hf.apply_nhds]

Premises used: Filter.Tendsto.apply_nhds
-- Module: Mathlib.Topology.Constructions
Goal:
Y : Type v
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst : DecidableEq ι
l : Filter Y
f : Y → (i : ι) → A i
x : (i : ι) → A i
hf : Tendsto f l (𝓝 x)
i : ι
g : Y → A i
xi : A i
hg : Tendsto g l (𝓝 xi)
j : ι
hj : j ≠ i
⊢ Tendsto (fun (i_1 : Y) ↦ Function.update (β := A) (f i_1) i (g i_1) j) l (𝓝 (Function.update (β := A) x i xi j))

Tactic:
simp [*, hf.apply_nhds]

Premises used: Filter.Tendsto.apply_nhds
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
ι : Type u_5
A : ι → Type u_6
inst : TopologicalSpace X
T : (i : ι) → TopologicalSpace (A i)
f : X → (i : ι) → A i
inst_1 : DecidableEq ι
x : X
hf : ContinuousAt f x
i : ι
g : X → A i
hg : ContinuousAt g x
⊢ ContinuousAt (Y := (a : ι) → A a) (fun (a : X) ↦ Function.update (β := A) (f a) i (g a)) x

Tactic:
hf.tendsto.update i hg

Premises used: ContinuousAt, Filter.Tendsto.update, ContinuousAt.tendsto
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
ι : Type u_5
A : ι → Type u_6
inst : TopologicalSpace X
T : (i : ι) → TopologicalSpace (A i)
f : X → (i : ι) → A i
inst_1 : DecidableEq ι
hf : Continuous[inst, Pi.topologicalSpace] f
i : ι
g : X → A i
hg : Continuous[inst, T i] g
⊢ Continuous[inst, Pi.topologicalSpace] fun (a : X) ↦ Function.update (β := A) (f a) i (g a)

Tactic:
continuous_iff_continuousAt.2 fun _ => hf.continuousAt.update i hg.continuousAt

Premises used: Iff.mpr, ContinuousAt.update, Continuous.continuousAt, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst : DecidableEq ι
i : ι
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace] fun (f : ((j : ι) → A j) × A i) ↦ update (β := A) f.1 i f.2

Tactic:
continuous_fst.update i continuous_snd

Premises used: continuous_snd, continuous_fst, Continuous.update
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst : (i : ι) → One (A i)
inst_1 : DecidableEq ι
i : ι
⊢ Continuous[T i, Pi.topologicalSpace] fun (x : A i) ↦ Pi.mulSingle (M := A) i x

Tactic:
continuous_const.update _ continuous_id

Premises used: continuous_const, Continuous.update, continuous_id, Pi.mulSingle
-- Module: Mathlib.Topology.Constructions
Goal:
Y : Type v
n : ℕ
A : Fin (n + 1) → Type u_9
inst : (i : Fin (n + 1)) → TopologicalSpace (A i)
f : Y → A 0
g : Y → (j : Fin n) → A j.succ
l : Filter Y
x : A 0
y : (j : Fin n) → A j.succ
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ Tendsto (β := A 0) (fun (i : Y) ↦ Fin.cons (α := A) (f i) (g i) 0) l (𝓝 (Fin.cons (α := A) x y 0))

Tactic:
simpa
-- Module: Mathlib.Topology.Constructions
Goal:
Y : Type v
n : ℕ
A : Fin (n + 1) → Type u_9
inst : (i : Fin (n + 1)) → TopologicalSpace (A i)
f : Y → A 0
g : Y → (j : Fin n) → A j.succ
l : Filter Y
x : A 0
y : (j : Fin n) → A j.succ
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ ∀ (i : Fin n),
    Tendsto (β := A i.succ) (fun (i_1 : Y) ↦ Fin.cons (α := A) (f i_1) (g i_1) i.succ) l
      (𝓝 (Fin.cons (α := A) x y i.succ))

Tactic:
simpa using tendsto_pi_nhds.1 hg

Premises used: tendsto_pi_nhds, Iff.mp
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
n : ℕ
A : Fin (n + 1) → Type u_9
inst_1 : (i : Fin (n + 1)) → TopologicalSpace (A i)
f : X → A 0
g : X → (j : Fin n) → A j.succ
x : X
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ ContinuousAt.{u, u_9} (Y := (i : Fin (n + 1)) → A i) (fun (a : X) ↦ Fin.cons (α := A) (f a) (g a)) x

Tactic:
hf.tendsto.finCons hg

Premises used: ContinuousAt, ContinuousAt.tendsto, Filter.Tendsto.finCons