awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : RCLike 𝕜
x y : X
hxy : x ≠ y
f : C(X, ℝ)
fx : Set.EqOn (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) 0 {x}
fy : Set.EqOn (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) 1 {y}
⊢ Ne (α := (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))
    (((continuousMapEval X 𝕜 : C(X, (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))) :
          (a : X) → (↑(characterSpace 𝕜 C(X, 𝕜)) : Type (max u_1 u_2)))
        x :
      (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))
    (((continuousMapEval X 𝕜 : C(X, (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))) :
          (a : X) → (↑(characterSpace 𝕜 C(X, 𝕜)) : Type (max u_1 u_2)))
        y :
      (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))
have refine_1 : ∃ (a : C(X, 𝕜)),
  Ne.{u_2 + 1} (α := 𝕜)
    (((((continuousMapEval X 𝕜 : C(X, (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))) :
                (a : X) → (↑(characterSpace 𝕜 C(X, 𝕜)) : Type (max u_1 u_2)))
              x :
            (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2))) :
          (a : C(X, 𝕜)) → 𝕜)
        a :
      𝕜)
    (((((continuousMapEval X 𝕜 : C(X, (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))) :
                (a : X) → (↑(characterSpace 𝕜 C(X, 𝕜)) : Type (max u_1 u_2)))
              y :
            (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2))) :
          (a : C(X, 𝕜)) → 𝕜)
        a :
      𝕜)
Tactic: rw [DFunLike.ne_iff]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : RCLike 𝕜
x y : X
hxy : x ≠ y
f : C(X, ℝ)
fx : Set.EqOn (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) 0 {x}
fy : Set.EqOn (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) 1 {y}
⊢ ∃ (a : C(X, 𝕜)),
    Ne.{u_2 + 1} (α := 𝕜)
      (((((continuousMapEval X 𝕜 :
                    C(X, (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))) :
                  (a : X) → (↑(characterSpace 𝕜 C(X, 𝕜)) : Type (max u_1 u_2)))
                x :
              (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2))) :
            (a : C(X, 𝕜)) → 𝕜)
          a :
        𝕜)
      (((((continuousMapEval X 𝕜 :
                    C(X, (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))) :
                  (a : X) → (↑(characterSpace 𝕜 C(X, 𝕜)) : Type (max u_1 u_2)))
                y :
              (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2))) :
            (a : C(X, 𝕜)) → 𝕜)
          a :
        𝕜)
have h : Ne.{u_2 + 1} (α := 𝕜)
  (((((continuousMapEval X 𝕜 : C(X, (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))) :
              (a : X) → (↑(characterSpace 𝕜 C(X, 𝕜)) : Type (max u_1 u_2)))
            x :
          (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2))) :
        (a : C(X, 𝕜)) → 𝕜)
      (ContinuousMap.comp { toFun := fun (x : ℝ) ↦ (↑x : 𝕜), continuous_toFun := sorry } f) :
    𝕜)
  (((((continuousMapEval X 𝕜 : C(X, (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))) :
              (a : X) → (↑(characterSpace 𝕜 C(X, 𝕜)) : Type (max u_1 u_2)))
            y :
          (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2))) :
        (a : C(X, 𝕜)) → 𝕜)
      (ContinuousMap.comp { toFun := fun (x : ℝ) ↦ (↑x : 𝕜), continuous_toFun := sorry } f) :
    𝕜)
Tactic: use (⟨fun (x : ℝ) => (x : 𝕜), RCLike.continuous_ofReal⟩ : C(ℝ, 𝕜)).comp f
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : RCLike 𝕜
φ : (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2))
⊢ ∃ (a : X),
    ((continuousMapEval X 𝕜 : C(X, (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))) :
          (a : X) → (↑(characterSpace 𝕜 C(X, 𝕜)) : Type (max u_1 u_2)))
        a =
      φ
have refine_2 : ∀ (x : X) (hx : Eq (α := Ideal C(X, 𝕜)) (idealOfSet 𝕜 {x}ᶜ) (RingHom.ker φ)),
  ∃ (a : X),
    ((continuousMapEval X 𝕜 : C(X, (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))) :
          (a : X) → (↑(characterSpace 𝕜 C(X, 𝕜)) : Type (max u_1 u_2)))
        a =
      φ
Tactic: obtain ⟨x, hx⟩ := (ideal_isMaximal_iff (RingHom.ker φ)).mp inferInstance
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
Goal:
X : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : RCLike 𝕜
φ : (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2))
x : X
hx : Eq (α := Ideal C(X, 𝕜)) (idealOfSet 𝕜 {x}ᶜ) (RingHom.ker φ)
⊢ ∃ (a : X),
    ((continuousMapEval X 𝕜 : C(X, (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))) :
          (a : X) → (↑(characterSpace 𝕜 C(X, 𝕜)) : Type (max u_1 u_2)))
        a =
      φ
have refine_2 : ∀ (f : C(X, 𝕜)),
  Membership.mem (γ := Ideal C(X, 𝕜))
      (RingHom.ker (F := (↑(characterSpace 𝕜 C(X, 𝕜)) : Type (max u_1 u_2)))
        (((continuousMapEval X 𝕜 :
                C(X, (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2)))) :
              (a : X) → (↑(characterSpace 𝕜 C(X, 𝕜)) : Type (max u_1 u_2)))
            x :
          (↑(characterSpace 𝕜 C(X, 𝕜) : Set (WeakDual 𝕜 C(X, 𝕜))) : Type (max u_1 u_2))))
      f ↔
    Membership.mem (γ := Ideal C(X, 𝕜)) (RingHom.ker φ) f
Tactic: refine ⟨x, CharacterSpace.ext_ker <| Ideal.ext fun f => ?_⟩
-- 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
⊢ ContinuousMap.{u_1, u_2} (↑(Icc a c) : Type u_1) E
have 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
Tactic: by_cases hb : f ⊤ = g ⊥
-- 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
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
⊢ ContinuousMap.{u_1, u_2} (↑(Icc a c) : Type u_1) E
have 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
Tactic: by_cases hb : f ⊤ = g ⊥
-- 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
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
⊢ ContinuousMap.{u_1, u_2} (↑(Icc a c) : Type u_1) E
have pos : Continuous[inst_1, inst_5] h
Tactic: suffices Continuous h from ⟨fun t => h t, by fun_prop⟩
-- 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
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] h
have 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)
Tactic: apply Continuous.if_le (by fun_prop) (by fun_prop) continuous_id continuous_const
-- 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
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)
⊢ (f.concat g).comp IccInclusionLeft = f
have 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)
Tactic: ext x
-- 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
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)
⊢ (f.concat g).comp IccInclusionRight = g
have 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)
Tactic: ext ⟨x, hx⟩
-- 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
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
⊢ 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)
have 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)
Tactic: obtain rfl | hxb := eq_or_ne x b
Cleared hypotheses: b, inst_3, inst_4, f, g, hb, hx
-- 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
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)
⊢ 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)
have 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)
Tactic: obtain rfl | hxb := eq_or_ne x b
-- 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
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
⊢ 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)
have h : ¬x ≤ b
Tactic: have h : ¬ x ≤ b := lt_of_le_of_ne hx.1 (Ne.symm hxb) |>.not_ge
-- 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
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 : (a : (↑(Icc a b) : Type u_1)) → E) (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) (↑t : α) ⋯) : E)
have 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 : α) sorry) :
    E)
Tactic: nth_rewrite 2 [← concat_comp_IccInclusionLeft hb]
-- 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
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)
    ((g : (a : (↑(Icc b c) : Type u_1)) → E) (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc b c) (↑t : α) ⋯) : E)
have 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 : α) sorry) :
    E)
Tactic: nth_rewrite 2 [← concat_comp_IccInclusionRight hb]
-- 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 :
  ∀ᶠ (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)
⊢ Tendsto (fun (i : ι) ↦ (F i).concat (G i)) p (𝓝 (f.concat g))
have 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
Tactic: rw [tendsto_nhds_compactOpen] at hf hg ⊢
Cleared hypotheses: hf, hg
-- 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 :
  ∀ᶠ (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
⊢ ∀ᶠ (a_1 : ι) in p, MapsTo (⇑((F a_1).concat (G a_1)) : (a : (↑(Icc a c) : Type u_1)) → E) K U
have h : b ∈ Icc a c
Tactic: have h : b ∈ Icc a c := ⟨Fact.out, Fact.out⟩
-- 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 :
  ∀ᶠ (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))
⊢ ∀ᶠ (a_1 : ι) in p, MapsTo (⇑((F a_1).concat (G a_1)) : (a : (↑(Icc a c) : Type u_1)) → E) K U
have hK₁ : IsCompact K₁
Tactic: have hK₁ : IsCompact K₁ :=
    hK.inter_right isClosed_Iic |>.image continuous_subtype_val |>.image projIccCM.continuous