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
pos : ∀ (hxb : (↑x : α) ≤ b), Membership.mem (α := E) U (((F i).concat (G i) : (a : (↑(Icc a c) : Type u_1)) → E) x : E)
neg : ∀ (hxb : b < (↑x : α)), Membership.mem (α := E) U (((F i).concat (G i) : (a : (↑(Icc a c) : Type u_1)) → E) x : E)
⊢ Membership.mem (α := E) U (((F i).concat (G i) : (a : (↑(Icc a c) : Type u_1)) → E) x : E)

Tactic:
by_cases! hxb : x ≤ b
-- 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 : (↑x : α) ≤ b
pos :
  Membership.mem (α := E) U
    ((F i : (a : (↑(Icc a b) : Type u_1)) → E) (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) (↑x : α) ⋯) : E)
⊢ Membership.mem (α := E) U (((F i).concat (G i) : (a : (↑(Icc a c) : Type u_1)) → E) x : E)

Tactic:
rw [concat_left hfg hxb]

Premises used: ContinuousMap.concat_left
-- 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 : (↑x : α) ≤ b
⊢ Membership.mem (α := E) U
    ((F i : (a : (↑(Icc a b) : Type u_1)) → E) (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) (↑x : α) ⋯) : E)

Tactic:
hf ⟨x, ⟨x, ⟨hx, hxb⟩, rfl⟩, ?_⟩

Premises used: And.intro, Exists.intro, Subtype.val, 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_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 : (↑x : α) ≤ b
pos :
  Eq (α := (↑(Icc a b) : Type u_1))
    ((projIccCM : (a_1 : α) → (↑(Icc a b) : Type u_1)) (↑x : α) : (↑(Icc a b) : Type u_1))
    (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) (↑x : α) ⋯ : { x : α // x ∈ Icc a b })
⊢ Membership.mem (α := E) U
    ((F i : (a : (↑(Icc a b) : Type u_1)) → E) (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) (↑x : α) ⋯) : E)

Tactic:
refine hf ⟨x, ⟨x, ⟨hx, hxb⟩, rfl⟩, ?_⟩

Premises used: And.intro, Exists.intro, Subtype.val, 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_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 : (↑x : α) ≤ b
⊢ Eq (α := (↑(Icc a b) : Type u_1))
    ((projIccCM : (a_1 : α) → (↑(Icc a b) : Type u_1)) (↑x : α) : (↑(Icc a b) : Type u_1))
    (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) (↑x : α) ⋯ : { x : α // x ∈ Icc a b })

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

Premises used: ContinuousMap.projIccCM, Set.projIcc, And.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
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 : α)
⊢ b ≤ (↑x : α)

Tactic:
replace hxb : b ≤ x := hxb.le
-- 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 : α)
neg :
  Membership.mem (α := E) U
    ((G i : (a : (↑(Icc b c) : Type u_1)) → E) (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc b c) (↑x : α) ⋯) : E)
⊢ Membership.mem (α := E) U (((F i).concat (G i) : (a : (↑(Icc a c) : Type u_1)) → E) x : E)

Tactic:
rw [concat_right hfg hxb]

Premises used: ContinuousMap.concat_right
-- 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 : α)
⊢ Membership.mem (α := E) U
    ((G i : (a : (↑(Icc b c) : Type u_1)) → E) (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc b c) (↑x : α) ⋯) : E)

Tactic:
hg ⟨x, ⟨x, ⟨hx, hxb⟩, rfl⟩, ?_⟩

Premises used: And.intro, Exists.intro, Subtype.val, 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_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 : α)
neg :
  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 })
⊢ Membership.mem (α := E) U
    ((G i : (a : (↑(Icc b c) : Type u_1)) → E) (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc b c) (↑x : α) ⋯) : E)

Tactic:
refine hg ⟨x, ⟨x, ⟨hx, hxb⟩, rfl⟩, ?_⟩

Premises used: And.intro, Exists.intro, Subtype.val, rfl