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 :
  ∀ᶠ (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))
hK₁ : IsCompact K₁
⊢ IsCompact K₂

Tactic:
have hK₂ : IsCompact K₂ :=
    hK.inter_right isClosed_Ici |>.image continuous_subtype_val |>.image projIccCM.continuous
-- 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))
hK₁ : IsCompact K₁
hK₂ : IsCompact K₂
rw : MapsTo (⇑((f.concat g).comp IccInclusionLeft) : (a : (↑(Icc a b) : Type u_1)) → E) K₁ U
⊢ MapsTo (⇑f : (a : (↑(Icc a b) : Type u_1)) → E) K₁ U

Tactic:
rw [← concat_comp_IccInclusionLeft hfg']

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
ι : 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))
hK₁ : IsCompact K₁
hK₂ : IsCompact K₂
apply : MapsTo (⇑IccInclusionLeft : (a_1 : (↑(Icc a b) : Type u_1)) → (↑(Icc a c) : Type u_1)) K₁ K
⊢ MapsTo (⇑((f.concat g).comp IccInclusionLeft) : (a : (↑(Icc a b) : Type u_1)) → E) K₁ U

Tactic:
apply hfgU.comp

Premises used: Set.MapsTo.comp
-- 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))
hK₁ : IsCompact K₁
hK₂ : IsCompact K₂
z : α
hz : z ∈ Icc a c
h1 : Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a c) z hz ∈ K
h2 : z ≤ b
⊢ Membership.mem (α := (↑(Icc a c) : Type u_1)) K
    ((IccInclusionLeft : (a_1 : (↑(Icc a b) : Type u_1)) → (↑(Icc a c) : Type u_1))
        ((projIccCM : (a_1 : α) → (↑(Icc a b) : Type u_1)) (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a c) z hz) : α)) :
      (↑(Icc a c) : Type u_1))

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

Premises used: ContinuousMap.projIccCM, Set.projIcc, And.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 :
  ∀ᶠ (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))
hK₁ : IsCompact K₁
hK₂ : IsCompact K₂
⊢ MapsTo (⇑f : (a : (↑(Icc a b) : Type u_1)) → E) K₁ U

Tactic:
have hfU : MapsTo f K₁ U := by
    rw [← concat_comp_IccInclusionLeft hfg']
    apply hfgU.comp
    rintro x ⟨y, ⟨⟨z, hz⟩, ⟨h1, (h2 : z ≤ b)⟩, rfl⟩, rfl⟩
    simpa [projIccCM, projIcc, h2, hz.1] using h1
-- 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))
hK₁ : IsCompact K₁
hK₂ : IsCompact K₂
hfU : MapsTo (⇑f : (a : (↑(Icc a b) : Type u_1)) → E) K₁ U
rw : MapsTo (⇑((f.concat g).comp IccInclusionRight) : (a : (↑(Icc b c) : Type u_1)) → E) K₂ U
⊢ MapsTo (⇑g : (a : (↑(Icc b c) : Type u_1)) → E) K₂ U

Tactic:
rw [← concat_comp_IccInclusionRight hfg']

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
ι : 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))
hK₁ : IsCompact K₁
hK₂ : IsCompact K₂
hfU : MapsTo (⇑f : (a : (↑(Icc a b) : Type u_1)) → E) K₁ U
apply : MapsTo (⇑IccInclusionRight : (a_1 : (↑(Icc b c) : Type u_1)) → (↑(Icc a c) : Type u_1)) K₂ K
⊢ MapsTo (⇑((f.concat g).comp IccInclusionRight) : (a : (↑(Icc b c) : Type u_1)) → E) K₂ U

Tactic:
apply hfgU.comp

Premises used: Set.MapsTo.comp
-- 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))
hK₁ : IsCompact K₁
hK₂ : IsCompact K₂
hfU : MapsTo (⇑f : (a : (↑(Icc a b) : Type u_1)) → E) K₁ U
z : α
hz : z ∈ Icc a c
h1 : Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a c) z hz ∈ K
h2 : b ≤ z
⊢ Membership.mem (α := (↑(Icc a c) : Type u_1)) K
    ((IccInclusionRight : (a_1 : (↑(Icc b c) : Type u_1)) → (↑(Icc a c) : Type u_1))
        ((projIccCM : (a : α) → (↑(Icc b c) : Type u_1)) (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a c) z hz) : α)) :
      (↑(Icc a c) : Type u_1))

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

Premises used: ContinuousMap.projIccCM, Set.projIcc, And.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 :
  ∀ᶠ (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))
hK₁ : IsCompact K₁
hK₂ : IsCompact K₂
hfU : MapsTo (⇑f : (a : (↑(Icc a b) : Type u_1)) → E) K₁ U
⊢ MapsTo (⇑g : (a : (↑(Icc b c) : Type u_1)) → E) K₂ U

Tactic:
have hgU : MapsTo g K₂ U := by
    rw [← concat_comp_IccInclusionRight hfg']
    apply hfgU.comp
    rintro x ⟨y, ⟨⟨z, hz⟩, ⟨h1, (h2 : b ≤ z)⟩, rfl⟩, rfl⟩
    simpa [projIccCM, projIcc, h2, hz.2] using h1
-- 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))
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
h₁ :
  ∀ (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),
    Membership.mem (α := E) U (((F i).concat (G i) : (a : (↑(Icc a c) : Type u_1)) → E) x : E)
⊢ ∀ᶠ (a_1 : ι) in p, MapsTo (⇑((F a_1).concat (G a_1)) : (a : (↑(Icc a c) : Type u_1)) → E) K U

Tactic:
filter_upwards [hf K₁ hK₁ U hU hfU, hg K₂ hK₂ U hU hgU, hfg] with i hf hg hfg x hx