awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Interval (goal)
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).concat (G i) : (a : (↑(Icc a c) : Type u_1)) → E) x : E)
have 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 : α) sorry) : E)
Tactic: rw [concat_left hfg hxb]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Interval (goal)
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)
have 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 : α) sorry : { x : α // x ∈ Icc a b })
Tactic: refine hf ⟨x, ⟨x, ⟨hx, hxb⟩, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Interval (hypothesis)
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 (((F i).concat (G i) : (a : (↑(Icc a c) : Type u_1)) → E) x : E)
have hxb₁ : b ≤ (↑x : α)
Tactic: replace hxb : b ≤ x := hxb.le
Cleared hypotheses: hxb
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Interval (goal)
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 (((F i).concat (G i) : (a : (↑(Icc a c) : Type u_1)) → E) x : E)
have 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 : α) sorry) : E)
Tactic: rw [concat_right hfg hxb]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Interval (goal)
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)
have 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 : α) sorry : { x : α // x ∈ Icc b c })
Tactic: refine hg ⟨x, ⟨x, ⟨hx, hxb⟩, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Interval (goal)
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 (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
have 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))
Tactic: change Continuous (S.restrict concat.uncurry)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Interval (goal)
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))
have 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
Tactic: refine continuousOn_iff_continuous_restrict.mp (fun fg hfg => ?_)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Interval (goal)
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
have 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)
Tactic: refine tendsto_concat ?_ hfg ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Interval (goal)
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)
⊢ ContinuousWithinAt (Function.uncurry concat) S fg
have refine_2 : Tendsto Prod.fst (𝓝[S] fg) (𝓝 fg.1)
Tactic: refine tendsto_concat ?_ hfg ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Interval (goal)
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)
⊢ ContinuousWithinAt (Function.uncurry concat) S fg
have refine_3 : Tendsto Prod.snd (𝓝[S] fg) (𝓝 fg.2)
Tactic: refine tendsto_concat ?_ hfg ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.LocallyConstant (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Monoid Y
inst_3 : ContinuousMul Y
⊢ Eq (α := C(X, Y)) (↑1 : C(X, Y)) 1
have h : ∀ (a : X), Eq.{u_2 + 1} (α := Y) (((↑1 : C(X, Y)) : (a : X) → Y) a : Y) ((1 : (a : X) → Y) a : Y)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.LocallyConstant (goal)
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
⊢ (↑(x * y) : C(X, Y)) = HMul.hMul (α := C(X, Y)) (↑x : C(X, Y)) (↑y : C(X, Y))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.LocallyConstant (goal)
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
⊢ (↑(x • y) : C(X, Y)) = HSMul.hSMul (α := R) (β := C(X, Y)) ((RingHom.id R : (a : R) → R) x : R) (↑y : C(X, Y))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.LocallyConstant (goal)
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
⊢ 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)
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ordered (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
ι : Type u_3
s : Finset ι
H : s.Nonempty
f : ι → C(α, β)
⊢ Eq (α := (a : α) → β) (⇑(s.sup' H f) : (a : α) → β) (s.sup' H fun (i : ι) ↦ (⇑(f i) : (a : α) → β))
have h : ∀ (x : α),
  Eq.{u_2 + 1} (α := β) ((s.sup' H f : (a : α) → β) x : β) (s.sup' H (fun (i : ι) ↦ (⇑(f i) : (a : α) → β)) x : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ordered (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
ι : Type u_3
s : Finset ι
H : s.Nonempty
f : ι → C(α, β)
⊢ Eq (α := (a : α) → β) (⇑(s.inf' H f) : (a : α) → β) (s.inf' H fun (i : ι) ↦ (⇑(f i) : (a : α) → β))
have h : ∀ (x : α),
  Eq.{u_2 + 1} (α := β) ((s.inf' H f : (a : α) → β) x : β) (s.inf' H (fun (i : ι) ↦ (⇑(f i) : (a : α) → β)) x : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Periodic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : AddCommGroup X
inst_3 : ContinuousAdd X
inst_4 : AddCommMonoid Y
inst_5 : ContinuousAdd Y
inst_6 : T2Space Y
f : C(X, Y)
p x : X
⊢ Eq.{u_2 + 1} (α := Y) ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)) : (a : X) → Y) (x + p) : Y)
    ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)) : (a : X) → Y) x : Y)
have pos : ∀ (h : Summable (α := C(X, Y)) fun (n : ℤ) ↦ f.comp (ContinuousMap.addRight (n • p))),
  Eq.{u_2 + 1} (α := Y) ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)) : (a : X) → Y) (x + p) : Y)
    ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)) : (a : X) → Y) x : Y)
Tactic: by_cases h : Summable fun n : ℤ => f.comp (ContinuousMap.addRight (n • p))