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
pos :
  (hb :
      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)) →
    ContinuousMap.{u_1, u_2} (↑(Icc a c) : Type u_1) E
neg :
  (hb :
      ¬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)) →
    ContinuousMap.{u_1, u_2} (↑(Icc a c) : Type u_1) E
⊢ ContinuousMap.{u_1, u_2} (↑(Icc a c) : Type u_1) E

Tactic:
by_cases hb : f ⊤ = g ⊥

Premises used: Bot.bot, Top.top, DFunLike.coe
-- 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
hb :
  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)
h : (t : α) → E :=
  fun (t : α) ↦
    if t ≤ b then (((IccExtendCM : (a : C((↑(Icc a b) : Type u_1), E)) → C(α, E)) f : C(α, E)) : (a : α) → E) t
    else (((IccExtendCM : (a : C((↑(Icc b c) : Type u_1), E)) → C(α, E)) g : C(α, E)) : (a : α) → E) t
this : Continuous[inst_1, inst_5] h
⊢ Continuous[instTopologicalSpaceSubtype, inst_5] fun (t : (↑(Icc a c) : Type u_1)) ↦ h (↑t : α)

Tactic:
fun_prop
-- 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
hb :
  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)
h : (t : α) → E :=
  fun (t : α) ↦
    if t ≤ b then (((IccExtendCM : (a : C((↑(Icc a b) : Type u_1), E)) → C(α, E)) f : C(α, E)) : (a : α) → E) t
    else (((IccExtendCM : (a : C((↑(Icc b c) : Type u_1), E)) → C(α, E)) g : C(α, E)) : (a : α) → E) t
pos : Continuous[inst_1, inst_5] h
⊢ ContinuousMap.{u_1, u_2} (↑(Icc a c) : Type u_1) E

Tactic:
suffices Continuous h from ⟨fun t => h t, by fun_prop⟩
-- 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
hb :
  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)
h : (t : α) → E :=
  fun (t : α) ↦
    if t ≤ b then (((IccExtendCM : (a : C((↑(Icc a b) : Type u_1), E)) → C(α, E)) f : C(α, E)) : (a : α) → E) t
    else (((IccExtendCM : (a : C((↑(Icc b c) : Type u_1), E)) → C(α, E)) g : C(α, E)) : (a : α) → E) t
⊢ Continuous[inst_1, inst_5]
    (⇑((IccExtendCM : (a : C((↑(Icc a b) : Type u_1), E)) → C(α, E)) f : C(α, E)) : (a : α) → E)

Tactic:
fun_prop
-- 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
hb :
  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)
h : (t : α) → E :=
  fun (t : α) ↦
    if t ≤ b then (((IccExtendCM : (a : C((↑(Icc a b) : Type u_1), E)) → C(α, E)) f : C(α, E)) : (a : α) → E) t
    else (((IccExtendCM : (a : C((↑(Icc b c) : Type u_1), E)) → C(α, E)) g : C(α, E)) : (a : α) → E) t
⊢ Continuous[inst_1, inst_5]
    (⇑((IccExtendCM : (a : C((↑(Icc b c) : Type u_1), E)) → C(α, E)) g : C(α, E)) : (a : α) → E)

Tactic:
fun_prop
-- 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
hb :
  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)
h : (t : α) → E :=
  fun (t : α) ↦
    if t ≤ b then (((IccExtendCM : (a : C((↑(Icc a b) : Type u_1), E)) → C(α, E)) f : C(α, E)) : (a : α) → E) t
    else (((IccExtendCM : (a : C((↑(Icc b c) : Type u_1), E)) → C(α, E)) g : C(α, E)) : (a : α) → E) t
pos :
  ∀ (x : α),
    id x = b →
      Eq.{u_2 + 1} (α := E)
        ((((IccExtendCM : (a : C((↑(Icc a b) : Type u_1), E)) → C(α, E)) f : C(α, E)) : (a : α) → E) x : E)
        ((((IccExtendCM : (a : C((↑(Icc b c) : Type u_1), E)) → C(α, E)) g : C(α, E)) : (a : α) → E) x : E)
⊢ Continuous[inst_1, inst_5] h

Tactic:
apply Continuous.if_le (by fun_prop) (by fun_prop) continuous_id continuous_const

Premises used: continuous_const, Continuous.if_le, continuous_id
-- Module: Mathlib.Topology.ContinuousMap.Interval
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a c : α
E : Type u_2
inst_3 : TopologicalSpace E
x : α
inst_4 : Fact (a ≤ id x)
inst_5 : Fact (id x ≤ c)
f : ContinuousMap.{u_1, u_2} (↑(Icc a (id x)) : Type u_1) E
g : ContinuousMap.{u_1, u_2} (↑(Icc (id x) c) : Type u_1) E
hb :
  Eq.{u_2 + 1} (α := E) ((f : (a : (↑(Icc a (id x)) : Type u_1)) → E) ⊤ : E)
    ((g : (a : (↑(Icc (id x) c) : Type u_1)) → E) ⊥ : E)
h : (t : α) → E :=
  fun (t : α) ↦
    if t ≤ id x then (((IccExtendCM : (a : C((↑(Icc a (id x)) : Type u_1), E)) → C(α, E)) f : C(α, E)) : (a : α) → E) t
    else (((IccExtendCM : (a : C((↑(Icc (id x) c) : Type u_1), E)) → C(α, E)) g : C(α, E)) : (a : α) → E) t
⊢ Eq.{u_2 + 1} (α := E)
    ((((IccExtendCM : (a : C((↑(Icc a (id x)) : Type u_1), E)) → C(α, E)) f : C(α, E)) : (a : α) → E) x : E)
    ((((IccExtendCM : (a : C((↑(Icc (id x) c) : Type u_1), E)) → C(α, E)) g : C(α, E)) : (a : α) → E) x : E)

Tactic:
simpa [IccExtendCM, projIccCM]

Premises used: ContinuousMap.projIccCM, ContinuousMap.IccExtendCM
-- 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
hb :
  ¬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)
⊢ ContinuousMap.{u_1, u_2} (↑(Icc a c) : Type u_1) E

Tactic:
exact .const _ (f ⊥)
-- 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
hb :
  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)
h :
  ∀ (x : (↑(Icc a b) : Type u_1)),
    Eq.{u_2 + 1} (α := E) (((f.concat g).comp IccInclusionLeft : (a : (↑(Icc a b) : Type u_1)) → E) x : E)
      ((f : (a : (↑(Icc a b) : Type u_1)) → E) x : E)
⊢ (f.concat g).comp IccInclusionLeft = f

Tactic:
ext x
-- 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
hb :
  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)
x : (↑(Icc a b) : Type u_1)
⊢ Eq.{u_2 + 1} (α := E) (((f.concat g).comp IccInclusionLeft : (a : (↑(Icc a b) : Type u_1)) → E) x : E)
    ((f : (a : (↑(Icc a b) : Type u_1)) → E) x : E)

Tactic:
simp [concat, IccExtendCM, hb, IccInclusionLeft, projIccCM, inclusion, x.2.2]

Premises used: ContinuousMap.projIccCM, ContinuousMap.concat, ContinuousMap.IccInclusionLeft, And.right, ContinuousMap.inclusion, ContinuousMap.IccExtendCM, 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
hb :
  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)
h :
  ∀ (x : α) (hx : x ∈ Icc b c),
    Eq.{u_2 + 1} (α := E)
      (((f.concat g).comp IccInclusionRight : (a : (↑(Icc b c) : Type u_1)) → E)
          (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc b c) x hx) :
        E)
      ((g : (a : (↑(Icc b c) : Type u_1)) → E) (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc b c) x hx) : E)
⊢ (f.concat g).comp IccInclusionRight = g

Tactic:
ext ⟨x, hx⟩
-- 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
hb :
  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)
x : α
hx : x ∈ Icc b c
h :
  ∀ [inst_6 : Fact (a ≤ x)] [inst_7 : Fact (x ≤ c)] {f : ContinuousMap.{u_1, u_2} (↑(Icc a x) : Type u_1) E}
    {g : ContinuousMap.{u_1, u_2} (↑(Icc x c) : Type u_1) E}
    (hb :
      Eq.{u_2 + 1} (α := E) ((f : (a : (↑(Icc a x) : Type u_1)) → E) ⊤ : E)
        ((g : (a : (↑(Icc x c) : Type u_1)) → E) ⊥ : E))
    (hx : x ∈ Icc x c),
    Eq.{u_2 + 1} (α := E)
      (((f.concat g).comp IccInclusionRight : (a : (↑(Icc x c) : Type u_1)) → E)
          (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Icc x c) x hx) :
        E)
      ((g : (a : (↑(Icc x c) : Type u_1)) → E) (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Icc x c) x hx) : E)
h₁ :
  ∀ (hxb : x ≠ b),
    Eq.{u_2 + 1} (α := E)
      (((f.concat g).comp IccInclusionRight : (a : (↑(Icc b c) : Type u_1)) → E)
          (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc b c) x hx) :
        E)
      ((g : (a : (↑(Icc b c) : Type u_1)) → E) (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc b c) x hx) : E)
⊢ Eq.{u_2 + 1} (α := E)
    (((f.concat g).comp IccInclusionRight : (a : (↑(Icc b c) : Type u_1)) → E)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc b c) x hx) :
      E)
    ((g : (a : (↑(Icc b c) : Type u_1)) → E) (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc b c) x hx) : E)

Tactic:
obtain rfl | hxb := eq_or_ne x b

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.ContinuousMap.Interval
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a c : α
E : Type u_2
inst_3 : TopologicalSpace E
x : α
inst_4 : Fact (a ≤ x)
inst_5 : Fact (x ≤ c)
f : ContinuousMap.{u_1, u_2} (↑(Icc a x) : Type u_1) E
g : ContinuousMap.{u_1, u_2} (↑(Icc x c) : Type u_1) E
hb :
  Eq.{u_2 + 1} (α := E) ((f : (a : (↑(Icc a x) : Type u_1)) → E) ⊤ : E) ((g : (a : (↑(Icc x c) : Type u_1)) → E) ⊥ : E)
hx : x ∈ Icc x c
⊢ Eq.{u_2 + 1} (α := E)
    (((f.concat g).comp IccInclusionRight : (a : (↑(Icc x c) : Type u_1)) → E)
        (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Icc x c) x hx) :
      E)
    ((g : (a : (↑(Icc x c) : Type u_1)) → E) (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Icc x c) x hx) : E)

Tactic:
simpa [concat, IccInclusionRight, IccExtendCM, projIccCM, inclusion, hb]

Premises used: ContinuousMap.projIccCM, ContinuousMap.IccInclusionRight, ContinuousMap.concat, ContinuousMap.inclusion, ContinuousMap.IccExtendCM
-- 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
hb :
  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)
x : α
hx : x ∈ Icc b c
hxb : x ≠ b
⊢ ¬x ≤ b

Tactic:
have h : ¬ x ≤ b := lt_of_le_of_ne hx.1 (Ne.symm hxb) |>.not_ge
-- 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
hb :
  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)
x : α
hx : x ∈ Icc b c
hxb : x ≠ b
h : ¬x ≤ b
⊢ Eq.{u_2 + 1} (α := E)
    (((f.concat g).comp IccInclusionRight : (a : (↑(Icc b c) : Type u_1)) → E)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc b c) x hx) :
      E)
    ((g : (a : (↑(Icc b c) : Type u_1)) → E) (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc b c) x hx) : E)

Tactic:
simp [concat, hb, IccInclusionRight, h, IccExtendCM, projIccCM, projIcc, inclusion, hx.2, hx.1]

Premises used: ContinuousMap.projIccCM, Set.projIcc, ContinuousMap.IccInclusionRight, ContinuousMap.concat, And.right, And.left, ContinuousMap.inclusion, ContinuousMap.IccExtendCM
-- 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
hb :
  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)
t : (↑(Icc a c) : Type u_1)
ht : (↑t : α) ≤ b
nth_rewrite :
  Eq.{u_2 + 1} (α := E) ((f.concat g : (a : (↑(Icc a c) : Type u_1)) → E) t : E)
    (((f.concat g).comp IccInclusionLeft : (a : (↑(Icc a b) : Type u_1)) → E)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) (↑t : α) ⋯) :
      E)
⊢ Eq.{u_2 + 1} (α := E) ((f.concat g : (a : (↑(Icc a c) : Type u_1)) → E) t : E)
    ((f : (a : (↑(Icc a b) : Type u_1)) → E) (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) (↑t : α) ⋯) : E)

Tactic:
nth_rewrite 2 [← concat_comp_IccInclusionLeft hb]

Premises used: ContinuousMap.concat_comp_IccInclusionLeft
-- 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
hb :
  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)
t : (↑(Icc a c) : Type u_1)
ht : (↑t : α) ≤ b
⊢ Eq.{u_2 + 1} (α := E) ((f.concat g : (a : (↑(Icc a c) : Type u_1)) → E) t : E)
    (((f.concat g).comp IccInclusionLeft : (a : (↑(Icc a b) : Type u_1)) → E)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) (↑t : α) ⋯) :
      E)

Tactic:
rfl
-- 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
hb :
  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)
t : (↑(Icc a c) : Type u_1)
ht : b ≤ (↑t : α)
nth_rewrite :
  Eq.{u_2 + 1} (α := E) ((f.concat g : (a : (↑(Icc a c) : Type u_1)) → E) t : E)
    (((f.concat g).comp IccInclusionRight : (a : (↑(Icc b c) : Type u_1)) → E)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc b c) (↑t : α) ⋯) :
      E)
⊢ Eq.{u_2 + 1} (α := E) ((f.concat g : (a : (↑(Icc a c) : Type u_1)) → E) t : E)
    ((g : (a : (↑(Icc b c) : Type u_1)) → E) (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc b c) (↑t : α) ⋯) : E)

Tactic:
nth_rewrite 2 [← concat_comp_IccInclusionRight hb]

Premises used: ContinuousMap.concat_comp_IccInclusionRight
-- 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
hb :
  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)
t : (↑(Icc a c) : Type u_1)
ht : b ≤ (↑t : α)
⊢ Eq.{u_2 + 1} (α := E) ((f.concat g : (a : (↑(Icc a c) : Type u_1)) → E) t : E)
    (((f.concat g).comp IccInclusionRight : (a : (↑(Icc b c) : Type u_1)) → E)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc b c) (↑t : α) ⋯) :
      E)

Tactic:
rfl
-- 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 :
  ∀ᶠ (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 : Tendsto F p (𝓝 f)
hg : Tendsto G p (𝓝 g)
rw :
  ∀
    (hf :
      ∀ (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 :
      ∀ (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)),
    IsCompact K →
      ∀ (U : Set E),
        IsOpen[inst_5] U →
          MapsTo (⇑(f.concat g) : (a : (↑(Icc a c) : Type u_1)) → E) K U →
            ∀ᶠ (a_4 : ι) in p, MapsTo (⇑((F a_4).concat (G a_4)) : (a : (↑(Icc a c) : Type u_1)) → E) K U
⊢ Tendsto (fun (i : ι) ↦ (F i).concat (G i)) p (𝓝 (f.concat g))

Tactic:
rw [tendsto_nhds_compactOpen] at hf hg ⊢

Premises used: ContinuousMap.tendsto_nhds_compactOpen
-- 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 :
  ∀ᶠ (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 :
  ∀ (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 :
  ∀ (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
⊢ b ∈ Icc a c

Tactic:
have h : b ∈ Icc a c := ⟨Fact.out, Fact.out⟩
-- 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 :
  ∀ᶠ (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 :
  ∀ (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 :
  ∀ (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))
⊢ IsCompact K₁

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