awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.Interval
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b c : α
inst_3 : Fact (a ≤ b)
inst_4 : Fact (b ≤ c)
E : Type u_2
inst_5 : TopologicalSpace E
f : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E
g : ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E
ι : Type u_3
p : Filter ι
F : ι → ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E
G : ι → ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E
hfg_1 :
  ∀ᶠ (i : ι) in p,
    Eq.{u_2 + 1} (α := E) ((F i : (a : (↑(Icc a b) : Type u_1)) → E) ⊤ : E)
      ((G i : (a : (↑(Icc b c) : Type u_1)) → E) ⊥ : E)
hfg' :
  Eq.{u_2 + 1} (α := E) ((f : (a : (↑(Icc a b) : Type u_1)) → E) ⊤ : E) ((g : (a : (↑(Icc b c) : Type u_1)) → E) ⊥ : E)
hf_1 :
  ∀ (K : Set (↑(Icc a b) : Type u_1)),
    IsCompact K →
      ∀ (U : Set E),
        IsOpen[inst_5] U →
          MapsTo (⇑f : (a : (↑(Icc a b) : Type u_1)) → E) K U →
            ∀ᶠ (a_4 : ι) in p, MapsTo (⇑(F a_4) : (a : (↑(Icc a b) : Type u_1)) → E) K U
hg_1 :
  ∀ (K : Set (↑(Icc b c) : Type u_1)),
    IsCompact K →
      ∀ (U : Set E),
        IsOpen[inst_5] U →
          MapsTo (⇑g : (a : (↑(Icc b c) : Type u_1)) → E) K U →
            ∀ᶠ (a : ι) in p, MapsTo (⇑(G a) : (a : (↑(Icc b c) : Type u_1)) → E) K U
K : Set (↑(Icc a c) : Type u_1)
hK : IsCompact K
U : Set E
hU : IsOpen[inst_5] U
hfgU : MapsTo (⇑(f.concat g) : (a : (↑(Icc a c) : Type u_1)) → E) K U
h : b ∈ Icc a c
K₁ : Set (↑(Icc a b) : Type u_1) :=
  (⇑projIccCM : (a_1 : α) → (↑(Icc a b) : Type u_1)) ''
    Subtype.val (p := fun (x : α) ↦ x ∈ Icc a c) '' (K ∩ Iic (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a c) b h))
K₂ : Set (↑(Icc b c) : Type u_1) :=
  (⇑projIccCM : (a : α) → (↑(Icc b c) : Type u_1)) ''
    Subtype.val (p := fun (x : α) ↦ x ∈ Icc a c) '' (K ∩ Ici (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a c) b h))
hK₁ : IsCompact K₁
hK₂ : IsCompact K₂
hfU : MapsTo (⇑f : (a : (↑(Icc a b) : Type u_1)) → E) K₁ U
hgU : MapsTo (⇑g : (a : (↑(Icc b c) : Type u_1)) → E) K₂ U
i : ι
hf : MapsTo (⇑(F i) : (a : (↑(Icc a b) : Type u_1)) → E) K₁ U
hg : MapsTo (⇑(G i) : (a : (↑(Icc b c) : Type u_1)) → E) K₂ U
hfg :
  Eq.{u_2 + 1} (α := E) ((F i : (a : (↑(Icc a b) : Type u_1)) → E) ⊤ : E)
    ((G i : (a : (↑(Icc b c) : Type u_1)) → E) ⊥ : E)
x : (↑(Icc a c) : Type u_1)
hx : x ∈ K
hxb : b ≤ (↑x : α)
⊢ Eq (α := (↑(Icc b c) : Type u_1)) ((projIccCM : (a : α) → (↑(Icc b c) : Type u_1)) (↑x : α) : (↑(Icc b c) : Type u_1))
    (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc b c) (↑x : α) ⋯ : { x : α // x ∈ Icc b c })

Tactic:
simp [projIccCM, projIcc, hxb, x.2.2]

Premises used: ContinuousMap.projIccCM, Set.projIcc, And.right, Subtype.property
-- Module: Mathlib.Topology.ContinuousMap.Interval
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b c : α
inst_3 : Fact (a ≤ b)
inst_4 : Fact (b ≤ c)
E : Type u_2
inst_5 : TopologicalSpace E
f : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E
g : ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E
S : Set (ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E) :=
  {fg : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E |
    Eq.{u_2 + 1} (α := E) ((fg.1 : (a : (↑(Icc a b) : Type u_1)) → E) ⊤ : E)
      ((fg.2 : (a : (↑(Icc b c) : Type u_1)) → E) ⊥ : E)}
change :
  Continuous
    (S.restrict (π :=
      fun
        (a_1 :
          ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E) ↦
      ContinuousMap.{u_1, u_2} (↑(Icc a c) : Type u_1) E) (Function.uncurry concat))
⊢ Continuous (Y := ContinuousMap.{u_1, u_2} (↑(Icc a c) : Type u_1) E)
    fun
      (fg :
        { fg :
          ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E //
          Eq.{u_2 + 1} (α := E) ((fg.1 : (a : (↑(Icc a b) : Type u_1)) → E) ⊤ : E)
            ((fg.2 : (a : (↑(Icc b c) : Type u_1)) → E) ⊥ : E) }) ↦
    (↑fg : C((↑(Icc a b) : Type u_1), E) × C((↑(Icc b c) : Type u_1), E)).1.concat
      (↑fg : C((↑(Icc a b) : Type u_1), E) × C((↑(Icc b c) : Type u_1), E)).2

Tactic:
change Continuous (S.restrict concat.uncurry)

Premises used: Continuous, ContinuousMap.concat, Set.restrict, Function.uncurry
-- Module: Mathlib.Topology.ContinuousMap.Interval
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b c : α
inst_3 : Fact (a ≤ b)
inst_4 : Fact (b ≤ c)
E : Type u_2
inst_5 : TopologicalSpace E
f : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E
g : ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E
S : Set (ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E) :=
  {fg : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E |
    Eq.{u_2 + 1} (α := E) ((fg.1 : (a : (↑(Icc a b) : Type u_1)) → E) ⊤ : E)
      ((fg.2 : (a : (↑(Icc b c) : Type u_1)) → E) ⊥ : E)}
⊢ Continuous
    (S.restrict (π :=
      fun
        (a_1 :
          ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E) ↦
      ContinuousMap.{u_1, u_2} (↑(Icc a c) : Type u_1) E) (Function.uncurry concat))

Tactic:
continuousOn_iff_continuous_restrict.mp (fun fg hfg => ?_)

Premises used: continuousOn_iff_continuous_restrict, Iff.mp
-- Module: Mathlib.Topology.ContinuousMap.Interval
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b c : α
inst_3 : Fact (a ≤ b)
inst_4 : Fact (b ≤ c)
E : Type u_2
inst_5 : TopologicalSpace E
f : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E
g : ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E
S : Set (ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E) :=
  {fg : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E |
    Eq.{u_2 + 1} (α := E) ((fg.1 : (a : (↑(Icc a b) : Type u_1)) → E) ⊤ : E)
      ((fg.2 : (a : (↑(Icc b c) : Type u_1)) → E) ⊥ : E)}
refine :
  ∀ (fg : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E)
    (hfg : fg ∈ S), ContinuousWithinAt (Function.uncurry concat) S fg
⊢ Continuous
    (S.restrict (π :=
      fun
        (a_1 :
          ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E) ↦
      ContinuousMap.{u_1, u_2} (↑(Icc a c) : Type u_1) E) (Function.uncurry concat))

Tactic:
refine continuousOn_iff_continuous_restrict.mp (fun fg hfg => ?_)

Premises used: continuousOn_iff_continuous_restrict, Iff.mp
-- Module: Mathlib.Topology.ContinuousMap.Interval
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b c : α
inst_3 : Fact (a ≤ b)
inst_4 : Fact (b ≤ c)
E : Type u_2
inst_5 : TopologicalSpace E
f : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E
g : ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E
S : Set (ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E) :=
  {fg : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E |
    Eq.{u_2 + 1} (α := E) ((fg.1 : (a : (↑(Icc a b) : Type u_1)) → E) ⊤ : E)
      ((fg.2 : (a : (↑(Icc b c) : Type u_1)) → E) ⊥ : E)}
fg : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E
hfg : fg ∈ S
⊢ ContinuousWithinAt (Function.uncurry concat) S fg

Tactic:
tendsto_concat ?_ hfg ?_ ?_

Premises used: ContinuousWithinAt, ContinuousMap.concat, dite, ContinuousMap.tendsto_concat
-- Module: Mathlib.Topology.ContinuousMap.Interval
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b c : α
inst_3 : Fact (a ≤ b)
inst_4 : Fact (b ≤ c)
E : Type u_2
inst_5 : TopologicalSpace E
f : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E
g : ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E
S : Set (ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E) :=
  {fg : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E |
    Eq.{u_2 + 1} (α := E) ((fg.1 : (a : (↑(Icc a b) : Type u_1)) → E) ⊤ : E)
      ((fg.2 : (a : (↑(Icc b c) : Type u_1)) → E) ⊥ : E)}
fg : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E
hfg : fg ∈ S
refine_1 :
  ∀ᶠ (i : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E) in
    𝓝[S] fg,
    Eq.{u_2 + 1} (α := E) ((i.1 : (a : (↑(Icc a b) : Type u_1)) → E) ⊤ : E)
      ((i.2 : (a : (↑(Icc b c) : Type u_1)) → E) ⊥ : E)
refine_2 : Tendsto Prod.fst (𝓝[S] fg) (𝓝 fg.1)
refine_3 : Tendsto Prod.snd (𝓝[S] fg) (𝓝 fg.2)
⊢ ContinuousWithinAt (Function.uncurry concat) S fg

Tactic:
refine tendsto_concat ?_ hfg ?_ ?_

Premises used: ContinuousMap.tendsto_concat
-- Module: Mathlib.Topology.ContinuousMap.Interval
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b c : α
inst_3 : Fact (a ≤ b)
inst_4 : Fact (b ≤ c)
E : Type u_2
inst_5 : TopologicalSpace E
f : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E
g : ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E
S : Set (ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E) :=
  {fg : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E |
    Eq.{u_2 + 1} (α := E) ((fg.1 : (a : (↑(Icc a b) : Type u_1)) → E) ⊤ : E)
      ((fg.2 : (a : (↑(Icc b c) : Type u_1)) → E) ⊥ : E)}
fg : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E
hfg : fg ∈ S
⊢ ∀ᶠ (i : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E) in
    𝓝[S] fg,
    Eq.{u_2 + 1} (α := E) ((i.1 : (a : (↑(Icc a b) : Type u_1)) → E) ⊤ : E)
      ((i.2 : (a : (↑(Icc b c) : Type u_1)) → E) ⊥ : E)

Tactic:
eventually_nhdsWithin_of_forall (fun _ => id)

Premises used: id, eventually_nhdsWithin_of_forall
-- Module: Mathlib.Topology.ContinuousMap.Interval
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b c : α
inst_3 : Fact (a ≤ b)
inst_4 : Fact (b ≤ c)
E : Type u_2
inst_5 : TopologicalSpace E
f : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E
g : ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E
S : Set (ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E) :=
  {fg : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E |
    Eq.{u_2 + 1} (α := E) ((fg.1 : (a : (↑(Icc a b) : Type u_1)) → E) ⊤ : E)
      ((fg.2 : (a : (↑(Icc b c) : Type u_1)) → E) ⊥ : E)}
fg : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E
hfg : fg ∈ S
⊢ ∀ᶠ (i : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E) in
    𝓝[S] fg,
    Eq.{u_2 + 1} (α := E) ((i.1 : (a : (↑(Icc a b) : Type u_1)) → E) ⊤ : E)
      ((i.2 : (a : (↑(Icc b c) : Type u_1)) → E) ⊥ : E)

Tactic:
exact eventually_nhdsWithin_of_forall (fun _ => id)

Premises used: id, eventually_nhdsWithin_of_forall
-- Module: Mathlib.Topology.ContinuousMap.Interval
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b c : α
inst_3 : Fact (a ≤ b)
inst_4 : Fact (b ≤ c)
E : Type u_2
inst_5 : TopologicalSpace E
f : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E
g : ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E
S : Set (ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E) :=
  {fg : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E |
    Eq.{u_2 + 1} (α := E) ((fg.1 : (a : (↑(Icc a b) : Type u_1)) → E) ⊤ : E)
      ((fg.2 : (a : (↑(Icc b c) : Type u_1)) → E) ⊥ : E)}
fg : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E
hfg : fg ∈ S
⊢ Tendsto Prod.fst (𝓝[S] fg) (𝓝 fg.1)

Tactic:
tendsto_nhdsWithin_of_tendsto_nhds continuousAt_fst

Premises used: tendsto_nhdsWithin_of_tendsto_nhds, continuousAt_fst
-- Module: Mathlib.Topology.ContinuousMap.Interval
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b c : α
inst_3 : Fact (a ≤ b)
inst_4 : Fact (b ≤ c)
E : Type u_2
inst_5 : TopologicalSpace E
f : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E
g : ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E
S : Set (ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E) :=
  {fg : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E |
    Eq.{u_2 + 1} (α := E) ((fg.1 : (a : (↑(Icc a b) : Type u_1)) → E) ⊤ : E)
      ((fg.2 : (a : (↑(Icc b c) : Type u_1)) → E) ⊥ : E)}
fg : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E
hfg : fg ∈ S
⊢ Tendsto Prod.fst (𝓝[S] fg) (𝓝 fg.1)

Tactic:
exact tendsto_nhdsWithin_of_tendsto_nhds continuousAt_fst

Premises used: tendsto_nhdsWithin_of_tendsto_nhds, continuousAt_fst
-- Module: Mathlib.Topology.ContinuousMap.Interval
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b c : α
inst_3 : Fact (a ≤ b)
inst_4 : Fact (b ≤ c)
E : Type u_2
inst_5 : TopologicalSpace E
f : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E
g : ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E
S : Set (ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E) :=
  {fg : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E |
    Eq.{u_2 + 1} (α := E) ((fg.1 : (a : (↑(Icc a b) : Type u_1)) → E) ⊤ : E)
      ((fg.2 : (a : (↑(Icc b c) : Type u_1)) → E) ⊥ : E)}
fg : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E
hfg : fg ∈ S
⊢ Tendsto Prod.snd (𝓝[S] fg) (𝓝 fg.2)

Tactic:
tendsto_nhdsWithin_of_tendsto_nhds continuousAt_snd

Premises used: tendsto_nhdsWithin_of_tendsto_nhds, continuousAt_snd
-- Module: Mathlib.Topology.ContinuousMap.Interval
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b c : α
inst_3 : Fact (a ≤ b)
inst_4 : Fact (b ≤ c)
E : Type u_2
inst_5 : TopologicalSpace E
f : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E
g : ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E
S : Set (ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E) :=
  {fg : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E |
    Eq.{u_2 + 1} (α := E) ((fg.1 : (a : (↑(Icc a b) : Type u_1)) → E) ⊤ : E)
      ((fg.2 : (a : (↑(Icc b c) : Type u_1)) → E) ⊥ : E)}
fg : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E
hfg : fg ∈ S
⊢ Tendsto Prod.snd (𝓝[S] fg) (𝓝 fg.2)

Tactic:
exact tendsto_nhdsWithin_of_tendsto_nhds continuousAt_snd

Premises used: tendsto_nhdsWithin_of_tendsto_nhds, continuousAt_snd
-- Module: Mathlib.Topology.ContinuousMap.Interval
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b c : α
inst_3 : Fact (a ≤ b)
inst_4 : Fact (b ≤ c)
E : Type u_2
inst_5 : TopologicalSpace E
x : (↑(Icc a c) : Type u_1)
hx : (↑x : α) ≤ b
fg :
  { fg : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E //
    Eq.{u_2 + 1} (α := E) ((fg.1 : (a : (↑(Icc a b) : Type u_1)) → E) ⊤ : E)
      ((fg.2 : (a : (↑(Icc b c) : Type u_1)) → E) ⊥ : E) }
⊢ Eq.{u_2 + 1} (α := E)
    ((((concatCM :
                (a_1 :
                    { fg : C((↑(Icc a b) : Type u_1), E) × C((↑(Icc b c) : Type u_1), E) //
                      (fg.1 : (a : (↑(Icc a b) : Type u_1)) → E) ⊤ = (fg.2 : (a : (↑(Icc b c) : Type u_1)) → E) ⊥ }) →
                  C((↑(Icc a c) : Type u_1), E))
              fg :
            ContinuousMap.{u_1, u_2} (↑(Icc a c) : Type u_1) E) :
          (a : (↑(Icc a c) : Type u_1)) → E)
        x :
      E)
    (((↑fg : C((↑(Icc a b) : Type u_1), E) × C((↑(Icc b c) : Type u_1), E)).1 : (a : (↑(Icc a b) : Type u_1)) → E)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) (↑x : α) ⋯) :
      E)

Tactic:
concat_left fg.2 hx

Premises used: ContinuousMap.concat_left, Subtype.property
-- Module: Mathlib.Topology.ContinuousMap.Interval
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b c : α
inst_3 : Fact (a ≤ b)
inst_4 : Fact (b ≤ c)
E : Type u_2
inst_5 : TopologicalSpace E
x : (↑(Icc a c) : Type u_1)
hx : (↑x : α) ≤ b
fg :
  { fg : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E //
    Eq.{u_2 + 1} (α := E) ((fg.1 : (a : (↑(Icc a b) : Type u_1)) → E) ⊤ : E)
      ((fg.2 : (a : (↑(Icc b c) : Type u_1)) → E) ⊥ : E) }
⊢ Eq.{u_2 + 1} (α := E)
    ((((concatCM :
                (a_1 :
                    { fg : C((↑(Icc a b) : Type u_1), E) × C((↑(Icc b c) : Type u_1), E) //
                      (fg.1 : (a : (↑(Icc a b) : Type u_1)) → E) ⊤ = (fg.2 : (a : (↑(Icc b c) : Type u_1)) → E) ⊥ }) →
                  C((↑(Icc a c) : Type u_1), E))
              fg :
            ContinuousMap.{u_1, u_2} (↑(Icc a c) : Type u_1) E) :
          (a : (↑(Icc a c) : Type u_1)) → E)
        x :
      E)
    (((↑fg : C((↑(Icc a b) : Type u_1), E) × C((↑(Icc b c) : Type u_1), E)).1 : (a : (↑(Icc a b) : Type u_1)) → E)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) (↑x : α) ⋯) :
      E)

Tactic:
exact concat_left fg.2 hx

Premises used: ContinuousMap.concat_left, Subtype.property
-- Module: Mathlib.Topology.ContinuousMap.Interval
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b c : α
inst_3 : Fact (a ≤ b)
inst_4 : Fact (b ≤ c)
E : Type u_2
inst_5 : TopologicalSpace E
x : (↑(Icc a c) : Type u_1)
hx : b ≤ (↑x : α)
fg :
  { fg : ContinuousMap.{u_1, u_2} (↑(Icc a b) : Type u_1) E × ContinuousMap.{u_1, u_2} (↑(Icc b c) : Type u_1) E //
    Eq.{u_2 + 1} (α := E) ((fg.1 : (a : (↑(Icc a b) : Type u_1)) → E) ⊤ : E)
      ((fg.2 : (a : (↑(Icc b c) : Type u_1)) → E) ⊥ : E) }
⊢ Eq.{u_2 + 1} (α := E)
    ((((concatCM :
                (a_1 :
                    { fg : C((↑(Icc a b) : Type u_1), E) × C((↑(Icc b c) : Type u_1), E) //
                      (fg.1 : (a : (↑(Icc a b) : Type u_1)) → E) ⊤ = (fg.2 : (a : (↑(Icc b c) : Type u_1)) → E) ⊥ }) →
                  C((↑(Icc a c) : Type u_1), E))
              fg :
            ContinuousMap.{u_1, u_2} (↑(Icc a c) : Type u_1) E) :
          (a : (↑(Icc a c) : Type u_1)) → E)
        x :
      E)
    (((↑fg : C((↑(Icc a b) : Type u_1), E) × C((↑(Icc b c) : Type u_1), E)).2 : (a : (↑(Icc b c) : Type u_1)) → E)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc b c) (↑x : α) ⋯) :
      E)

Tactic:
concat_right fg.2 hx

Premises used: ContinuousMap.concat_right, Subtype.property
-- Module: Mathlib.Topology.ContinuousMap.Lattice
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_2
inst_1 : TopologicalSpace β
inst_2 : Group β
inst_3 : IsTopologicalGroup β
inst_4 : Lattice β
inst_5 : TopologicalLattice β
f : C(α, β)
⊢ Eq (α := (a : α) → β) (⇑|f|ₘ : (a : α) → β) |(⇑f : (a : α) → β)|ₘ

Tactic:
rfl

Premises used: rfl, mabs
-- Module: Mathlib.Topology.ContinuousMap.Lattice
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_2
inst_1 : TopologicalSpace β
inst_2 : Group β
inst_3 : IsTopologicalGroup β
inst_4 : Lattice β
inst_5 : TopologicalLattice β
f : C(α, β)
x : α
⊢ Eq.{u_2 + 1} (α := β) ((|f|ₘ : (a : α) → β) x : β) (|(f : (a : α) → β) x|ₘ : β)

Tactic:
rfl

Premises used: rfl, mabs
-- Module: Mathlib.Topology.ContinuousMap.LocallyConstant
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Monoid Y
inst_3 : ContinuousMul Y
h : ∀ (a : X), Eq.{u_2 + 1} (α := Y) (((↑1 : C(X, Y)) : (a : X) → Y) a : Y) ((1 : (a : X) → Y) a : Y)
⊢ Eq (α := C(X, Y)) (↑1 : C(X, Y)) 1

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.LocallyConstant
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Monoid Y
inst_3 : ContinuousMul Y
a : X
⊢ Eq.{u_2 + 1} (α := Y) (((↑1 : C(X, Y)) : (a : X) → Y) a : Y) ((1 : (a : X) → Y) a : Y)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.LocallyConstant
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Monoid Y
inst_3 : ContinuousMul Y
x y : LocallyConstant X Y
h :
  ∀ (a : X),
    Eq.{u_2 + 1} (α := Y) (((↑(x * y) : C(X, Y)) : (a : X) → Y) a : Y)
      ((HMul.hMul (α := C(X, Y)) (↑x : C(X, Y)) (↑y : C(X, Y)) : (a : X) → Y) a : Y)
⊢ (↑(x * y) : C(X, Y)) = HMul.hMul (α := C(X, Y)) (↑x : C(X, Y)) (↑y : C(X, Y))

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.LocallyConstant
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Monoid Y
inst_3 : ContinuousMul Y
x y : LocallyConstant X Y
a : X
⊢ Eq.{u_2 + 1} (α := Y) (((↑(x * y) : C(X, Y)) : (a : X) → Y) a : Y)
    ((HMul.hMul (α := C(X, Y)) (↑x : C(X, Y)) (↑y : C(X, Y)) : (a : X) → Y) a : Y)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.LocallyConstant
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
R : Type u_3
inst_2 : Semiring R
inst_3 : AddCommMonoid Y
inst_4 : Module R Y
inst_5 : ContinuousAdd Y
inst_6 : ContinuousConstSMul R Y
x : R
y : LocallyConstant X Y
h :
  ∀ (a : X),
    Eq.{u_2 + 1} (α := Y) (((↑(x • y) : C(X, Y)) : (a : X) → Y) a : Y)
      ((HSMul.hSMul (α := R) (β := C(X, Y)) ((RingHom.id R : (a : R) → R) x : R) (↑y : C(X, Y)) : (a : X) → Y) a : Y)
⊢ (↑(x • y) : C(X, Y)) = HSMul.hSMul (α := R) (β := C(X, Y)) ((RingHom.id R : (a : R) → R) x : R) (↑y : C(X, Y))

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.LocallyConstant
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
R : Type u_3
inst_2 : Semiring R
inst_3 : AddCommMonoid Y
inst_4 : Module R Y
inst_5 : ContinuousAdd Y
inst_6 : ContinuousConstSMul R Y
x : R
y : LocallyConstant X Y
a : X
⊢ Eq.{u_2 + 1} (α := Y) (((↑(x • y) : C(X, Y)) : (a : X) → Y) a : Y)
    ((HSMul.hSMul (α := R) (β := C(X, Y)) ((RingHom.id R : (a : R) → R) x : R) (↑y : C(X, Y)) : (a : X) → Y) a : Y)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.LocallyConstant
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
R : Type u_3
inst_2 : Semiring R
inst_3 : AddCommMonoid Y
inst_4 : Module R Y
inst_5 : ContinuousAdd Y
inst_6 : ContinuousConstSMul R Y
⊢ Eq (α := LocallyConstant X Y →+ C(X, Y))
    (LinearMap.toAddMonoidHom (modM₁ := instModule) (modM₂ := ContinuousMap.module) (toContinuousMapLinearMap R))
    toContinuousMapAddMonoidHom

Tactic:
rfl

Premises used: LinearMap.toAddMonoidHom, LocallyConstant.toContinuousMapAddMonoidHom, LocallyConstant.toContinuousMap, rfl
-- Module: Mathlib.Topology.ContinuousMap.LocallyConstant
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
R : Type u_3
inst_2 : CommSemiring R
inst_3 : Semiring Y
inst_4 : Algebra R Y
inst_5 : IsTopologicalSemiring Y
r : R
h :
  ∀ (x : X),
    Eq.{u_2 + 1} (α := Y)
      (((↑((algebraMap R (LocallyConstant X Y) : (a : R) → LocallyConstant X Y) r) : C(X, Y)) : (a : X) → Y) x : Y)
      ((((algebraMap R C(X, Y) : (a : R) → C(X, Y)) r : C(X, Y)) : (a : X) → Y) x : Y)
⊢ Eq (α := C(X, Y)) (↑((algebraMap R (LocallyConstant X Y) : (a : R) → LocallyConstant X Y) r) : C(X, Y))
    ((algebraMap R C(X, Y) : (a : R) → C(X, Y)) r)

Tactic:
ext x