-- Mathlib/Topology/ContinuousMap/Interval.lean
theorem tendsto_concat {ι : Type*} {p : Filter ι} {F : ι → C(Icc a b, E)} {G : ι → C(Icc b c, E)}
    (hfg : ∀ᶠ i in p, (F i) ⊤ = (G i) ⊥) (hfg' : f ⊤ = g ⊥)
    (hf : Tendsto F p (𝓝 f)) (hg : Tendsto G p (𝓝 g)) :
    Tendsto (fun i => concat (F i) (G i)) p (𝓝 (concat f g))

Proof state:
case intro.intro.intro.mk.intro.intro
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
ι : Type u_3
p : Filter ι
F : ι → C(↑(Icc a b), E)
G : ι → C(↑(Icc b c), E)
hfg : ∀ᶠ (i : ι) in p, (F i) ⊤ = (G i) ⊥
hfg' : f ⊤ = g ⊥
hf :
  ∀ (K : Set ↑(Icc a b)),
    IsCompact K → ∀ (U : Set E), IsOpen U → MapsTo (⇑f) K U → ∀ᶠ (a_4 : ι) in p, MapsTo (⇑(F a_4)) K U
hg :
  ∀ (K : Set ↑(Icc b c)), IsCompact K → ∀ (U : Set E), IsOpen U → MapsTo (⇑g) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(G a)) K U
K : Set ↑(Icc a c)
hK : IsCompact K
U : Set E
hU : IsOpen U
hfgU : MapsTo (⇑(f.concat g)) K U
h : b ∈ Icc a c
K₁ : Set ↑(Icc a b) := ⇑projIccCM '' (Subtype.val '' (K ∩ Iic ⟨b, h⟩))
K₂ : Set ↑(Icc b c) := ⇑projIccCM '' (Subtype.val '' (K ∩ Ici ⟨b, h⟩))
hK₁ : IsCompact K₁
hK₂ : IsCompact K₂
z : α
hz : z ∈ Icc a c
h1 : ⟨z, hz⟩ ∈ K
h2 : z ≤ b
⊢ IccInclusionLeft (projIccCM ↑⟨z, hz⟩) ∈ K

Tactic:
simpa [projIccCM, projIcc, h2, hz.1] using h1

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
ι : Type u_3
p : Filter ι
F : ι → C(↑(Icc a b), E)
G : ι → C(↑(Icc b c), E)
hfg✝ : ∀ᶠ (i : ι) in p, (F i) ⊤ = (G i) ⊥
hfg' : f ⊤ = g ⊥
hf✝ :
  ∀ (K : Set ↑(Icc a b)),
    IsCompact K → ∀ (U : Set E), IsOpen U → MapsTo (⇑f) K U → ∀ᶠ (a_4 : ι) in p, MapsTo (⇑(F a_4)) K U
hg✝ :
  ∀ (K : Set ↑(Icc b c)), IsCompact K → ∀ (U : Set E), IsOpen U → MapsTo (⇑g) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(G a)) K U
K : Set ↑(Icc a c)
hK : IsCompact K
U : Set E
hU : IsOpen U
hfgU : MapsTo (⇑(f.concat g)) K U
h : b ∈ Icc a c
K₁ : Set ↑(Icc a b) := ⇑projIccCM '' (Subtype.val '' (K ∩ Iic ⟨b, h⟩))
K₂ : Set ↑(Icc b c) := ⇑projIccCM '' (Subtype.val '' (K ∩ Ici ⟨b, h⟩))
hK₁ : IsCompact K₁
hK₂ : IsCompact K₂
hfU : MapsTo (⇑f) K₁ U
hgU : MapsTo (⇑g) K₂ U
i : ι
hf : MapsTo (⇑(F i)) K₁ U
hg : MapsTo (⇑(G i)) K₂ U
hfg : (F i) ⊤ = (G i) ⊥
x : ↑(Icc a c)
hx : x ∈ K
hxb : ↑x ≤ b
⊢ ((F i).concat (G i)) x ∈ U

Tactic:
rw [concat_left hfg hxb]

Result:
case pos
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
ι : Type u_3
p : Filter ι
F : ι → C(↑(Icc a b), E)
G : ι → C(↑(Icc b c), E)
hfg✝ : ∀ᶠ (i : ι) in p, (F i) ⊤ = (G i) ⊥
hfg' : f ⊤ = g ⊥
hf✝ :
  ∀ (K : Set ↑(Icc a b)),
    IsCompact K → ∀ (U : Set E), IsOpen U → MapsTo (⇑f) K U → ∀ᶠ (a_4 : ι) in p, MapsTo (⇑(F a_4)) K U
hg✝ :
  ∀ (K : Set ↑(Icc b c)), IsCompact K → ∀ (U : Set E), IsOpen U → MapsTo (⇑g) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(G a)) K U
K : Set ↑(Icc a c)
hK : IsCompact K
U : Set E
hU : IsOpen U
hfgU : MapsTo (⇑(f.concat g)) K U
h : b ∈ Icc a c
K₁ : Set ↑(Icc a b) := ⇑projIccCM '' (Subtype.val '' (K ∩ Iic ⟨b, h⟩))
K₂ : Set ↑(Icc b c) := ⇑projIccCM '' (Subtype.val '' (K ∩ Ici ⟨b, h⟩))
hK₁ : IsCompact K₁
hK₂ : IsCompact K₂
hfU : MapsTo (⇑f) K₁ U
hgU : MapsTo (⇑g) K₂ U
i : ι
hf : MapsTo (⇑(F i)) K₁ U
hg : MapsTo (⇑(G i)) K₂ U
hfg : (F i) ⊤ = (G i) ⊥
x : ↑(Icc a c)
hx : x ∈ K
hxb : ↑x ≤ b
⊢ (F i) ⟨↑x, ⋯⟩ ∈ U

Proof state:
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
ι : Type u_3
p : Filter ι
F : ι → C(↑(Icc a b), E)
G : ι → C(↑(Icc b c), E)
hfg : ∀ᶠ (i : ι) in p, (F i) ⊤ = (G i) ⊥
hfg' : f ⊤ = g ⊥
hf :
  ∀ (K : Set ↑(Icc a b)),
    IsCompact K → ∀ (U : Set E), IsOpen U → MapsTo (⇑f) K U → ∀ᶠ (a_4 : ι) in p, MapsTo (⇑(F a_4)) K U
hg :
  ∀ (K : Set ↑(Icc b c)), IsCompact K → ∀ (U : Set E), IsOpen U → MapsTo (⇑g) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(G a)) K U
K : Set ↑(Icc a c)
hK : IsCompact K
U : Set E
hU : IsOpen U
hfgU : MapsTo (⇑(f.concat g)) K U
h : b ∈ Icc a c
K₁ : Set ↑(Icc a b) := ⇑projIccCM '' (Subtype.val '' (K ∩ Iic ⟨b, h⟩))
⊢ ∀ᶠ (a_1 : ι) in p, MapsTo (⇑((F a_1).concat (G a_1))) K U

Tactic:
let K₂ : Set (Icc b c) := projIccCM '' (Subtype.val '' (K ∩ Ici ⟨b, h⟩))

Result:
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
ι : Type u_3
p : Filter ι
F : ι → C(↑(Icc a b), E)
G : ι → C(↑(Icc b c), E)
hfg : ∀ᶠ (i : ι) in p, (F i) ⊤ = (G i) ⊥
hfg' : f ⊤ = g ⊥
hf :
  ∀ (K : Set ↑(Icc a b)),
    IsCompact K → ∀ (U : Set E), IsOpen U → MapsTo (⇑f) K U → ∀ᶠ (a_4 : ι) in p, MapsTo (⇑(F a_4)) K U
hg :
  ∀ (K : Set ↑(Icc b c)), IsCompact K → ∀ (U : Set E), IsOpen U → MapsTo (⇑g) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(G a)) K U
K : Set ↑(Icc a c)
hK : IsCompact K
U : Set E
hU : IsOpen U
hfgU : MapsTo (⇑(f.concat g)) K U
h : b ∈ Icc a c
K₁ : Set ↑(Icc a b) := ⇑projIccCM '' (Subtype.val '' (K ∩ Iic ⟨b, h⟩))
K₂ : Set ↑(Icc b c) := ⇑projIccCM '' (Subtype.val '' (K ∩ Ici ⟨b, h⟩))
⊢ ∀ᶠ (a_1 : ι) in p, MapsTo (⇑((F a_1).concat (G a_1))) K U

Proof state:
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
ι : Type u_3
p : Filter ι
F : ι → C(↑(Icc a b), E)
G : ι → C(↑(Icc b c), E)
hfg : ∀ᶠ (i : ι) in p, (F i) ⊤ = (G i) ⊥
hfg' : f ⊤ = g ⊥
hf :
  ∀ (K : Set ↑(Icc a b)),
    IsCompact K → ∀ (U : Set E), IsOpen U → MapsTo (⇑f) K U → ∀ᶠ (a_4 : ι) in p, MapsTo (⇑(F a_4)) K U
hg :
  ∀ (K : Set ↑(Icc b c)), IsCompact K → ∀ (U : Set E), IsOpen U → MapsTo (⇑g) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(G a)) K U
K : Set ↑(Icc a c)
hK : IsCompact K
U : Set E
hU : IsOpen U
hfgU : MapsTo (⇑(f.concat g)) K U
h : b ∈ Icc a c
K₁ : Set ↑(Icc a b) := ⇑projIccCM '' (Subtype.val '' (K ∩ Iic ⟨b, h⟩))
K₂ : Set ↑(Icc b c) := ⇑projIccCM '' (Subtype.val '' (K ∩ Ici ⟨b, h⟩))
⊢ ∀ᶠ (a_1 : ι) in p, MapsTo (⇑((F a_1).concat (G a_1))) K U

Tactic:
have hK₁ : IsCompact K₁ :=
  hK.inter_right isClosed_Iic |>.image continuous_subtype_val |>.image projIccCM.continuous

Result:
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
ι : Type u_3
p : Filter ι
F : ι → C(↑(Icc a b), E)
G : ι → C(↑(Icc b c), E)
hfg : ∀ᶠ (i : ι) in p, (F i) ⊤ = (G i) ⊥
hfg' : f ⊤ = g ⊥
hf :
  ∀ (K : Set ↑(Icc a b)),
    IsCompact K → ∀ (U : Set E), IsOpen U → MapsTo (⇑f) K U → ∀ᶠ (a_4 : ι) in p, MapsTo (⇑(F a_4)) K U
hg :
  ∀ (K : Set ↑(Icc b c)), IsCompact K → ∀ (U : Set E), IsOpen U → MapsTo (⇑g) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(G a)) K U
K : Set ↑(Icc a c)
hK : IsCompact K
U : Set E
hU : IsOpen U
hfgU : MapsTo (⇑(f.concat g)) K U
h : b ∈ Icc a c
K₁ : Set ↑(Icc a b) := ⇑projIccCM '' (Subtype.val '' (K ∩ Iic ⟨b, h⟩))
K₂ : Set ↑(Icc b c) := ⇑projIccCM '' (Subtype.val '' (K ∩ Ici ⟨b, h⟩))
hK₁ : IsCompact K₁
⊢ ∀ᶠ (a_1 : ι) in p, MapsTo (⇑((F a_1).concat (G a_1))) K U