awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y_1 : Type u_2
W : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace W
inst_3 : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst_4 : TopologicalSpace X'
inst_5 : TopologicalSpace Y'
ι : Type u_7
p : ι → Prop
Y : ι → Type u_8
inst_6 : (i : ι) → TopologicalSpace (Y i)
inst_7 : DecidablePred p
j : ι
⊢ Continuous[instTopologicalSpaceProd, inst_6 j]
    fun (a : ((i : { x : ι // p x }) → Y (↑i : ι)) × ((i : { x : ι // ¬p x }) → Y (↑i : ι))) ↦
    if h : p j then a.1 (Subtype.mk (p := fun (x : ι) ↦ p x) j h) else a.2 (Subtype.mk (p := fun (x : ι) ↦ ¬p x) j h)
have pos : ∀ (h : p j),
  Continuous[instTopologicalSpaceProd, inst_6 j]
    fun (a : ((i : { x : ι // p x }) → Y (↑i : ι)) × ((i : { x : ι // ¬p x }) → Y (↑i : ι))) ↦
    a.1 (Subtype.mk (p := fun (x : ι) ↦ p x) j h)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y_1 : Type u_2
W : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace W
inst_3 : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst_4 : TopologicalSpace X'
inst_5 : TopologicalSpace Y'
ι : Type u_7
p : ι → Prop
Y : ι → Type u_8
inst_6 : (i : ι) → TopologicalSpace (Y i)
inst_7 : DecidablePred p
j : ι
pos :
  ∀ (h : p j),
    Continuous[instTopologicalSpaceProd, inst_6 j]
      fun (a : ((i : { x : ι // p x }) → Y (↑i : ι)) × ((i : { x : ι // ¬p x }) → Y (↑i : ι))) ↦
      a.1 (Subtype.mk (p := fun (x : ι) ↦ p x) j h)
⊢ Continuous[instTopologicalSpaceProd, inst_6 j]
    fun (a : ((i : { x : ι // p x }) → Y (↑i : ι)) × ((i : { x : ι // ¬p x }) → Y (↑i : ι))) ↦
    if h : p j then a.1 (Subtype.mk (p := fun (x : ι) ↦ p x) j h) else a.2 (Subtype.mk (p := fun (x : ι) ↦ ¬p x) j h)
have neg : ∀ (h : ¬p j),
  Continuous[instTopologicalSpaceProd, inst_6 j]
    fun (a : ((i : { x : ι // p x }) → Y (↑i : ι)) × ((i : { x : ι // ¬p x }) → Y (↑i : ι))) ↦
    a.2 (Subtype.mk (p := fun (x : ι) ↦ ¬p x) j h)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y_1 : Type u_2
W : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace W
inst_3 : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst_4 : TopologicalSpace X'
inst_5 : TopologicalSpace Y'
ι : Type u_7
inst_6 : DecidableEq ι
i : ι
Y : ι → Type u_8
inst_7 : (j : ι) → TopologicalSpace (Y j)
j : ι
⊢ Continuous[instTopologicalSpaceProd, inst_7 j] fun (a : Y i × ((j : { j : ι // j ≠ i }) → Y (↑j : ι))) ↦
    (Equiv.piSplitAt i Y).invFun a j
have dsimp : Continuous[instTopologicalSpaceProd, inst_7 j] fun (a : Y i × ((j : { j : ι // j ≠ i }) → Y (↑j : ι))) ↦
  if h : j = i then Eq.rec (motive := fun (x : ι) (x_1 : i = x) ↦ Y x) a.1 sorry
  else a.2 (Subtype.mk (p := fun (j : ι) ↦ j ≠ i) j h)
Tactic: dsimp only [Equiv.piSplitAt]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y_1 : Type u_2
W : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace W
inst_3 : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst_4 : TopologicalSpace X'
inst_5 : TopologicalSpace Y'
ι : Type u_7
inst_6 : DecidableEq ι
i : ι
Y : ι → Type u_8
inst_7 : (j : ι) → TopologicalSpace (Y j)
j : ι
⊢ Continuous[instTopologicalSpaceProd, inst_7 j] fun (a : Y i × ((j : { j : ι // j ≠ i }) → Y (↑j : ι))) ↦
    if h : j = i then Eq.rec (motive := fun (x : ι) (x_1 : i = x) ↦ Y x) a.1 ⋯
    else a.2 (Subtype.mk (p := fun (j : ι) ↦ j ≠ i) j h)
have pos : ∀ (h : j = i),
  Continuous[instTopologicalSpaceProd, inst_7 j] fun (a : Y i × ((j : { j : ι // j ≠ i }) → Y (↑j : ι))) ↦
    Eq.rec (motive := fun (x : ι) (x_1 : i = x) ↦ Y x) a.1 sorry
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y_1 : Type u_2
W : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace W
inst_3 : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst_4 : TopologicalSpace X'
inst_5 : TopologicalSpace Y'
ι : Type u_7
inst_6 : DecidableEq ι
i : ι
Y : ι → Type u_8
inst_7 : (j : ι) → TopologicalSpace (Y j)
j : ι
pos :
  ∀ (h : j = i),
    Continuous[instTopologicalSpaceProd, inst_7 j] fun (a : Y i × ((j : { j : ι // j ≠ i }) → Y (↑j : ι))) ↦
      Eq.rec (motive := fun (x : ι) (x_1 : i = x) ↦ Y x) a.1 ⋯
⊢ Continuous[instTopologicalSpaceProd, inst_7 j] fun (a : Y i × ((j : { j : ι // j ≠ i }) → Y (↑j : ι))) ↦
    if h : j = i then Eq.rec (motive := fun (x : ι) (x_1 : i = x) ↦ Y x) a.1 ⋯
    else a.2 (Subtype.mk (p := fun (j : ι) ↦ j ≠ i) j h)
have neg : ∀ (h : ¬j = i),
  Continuous[instTopologicalSpaceProd, inst_7 j] fun (a : Y i × ((j : { j : ι // j ≠ i }) → Y (↑j : ι))) ↦
    a.2 (Subtype.mk (p := fun (j : ι) ↦ j ≠ i) j h)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y_1 : Type u_2
W : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace W
inst_3 : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst_4 : TopologicalSpace X'
inst_5 : TopologicalSpace Y'
ι : Type u_7
inst_6 : DecidableEq ι
i : ι
Y : ι → Type u_8
inst_7 : (j : ι) → TopologicalSpace (Y j)
j : ι
h : j = i
⊢ Continuous[instTopologicalSpaceProd, inst_7 j] fun (a : Y i × ((j : { j : ι // j ≠ i }) → Y (↑j : ι))) ↦
    Eq.rec (motive := fun (x : ι) (x_1 : i = x) ↦ Y x) a.1 ⋯
have pos : Continuous[instTopologicalSpaceProd, inst_7 j] fun (a : Y j × ((j_1 : { j_1 : ι // j_1 ≠ j }) → Y (↑j_1 : ι))) ↦
  Eq.rec (motive := fun (x : ι) (x_1 : j = x) ↦ Y x) a.1 sorry
Tactic: subst h
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsEmbedding f
x : X
⊢ Eq.{u_2 + 1} (α := (↑(range f) : Type u_2))
    ((hf.toHomeomorph : (a : X) → (↑(range f) : Type u_2))
        ((hf.toHomeomorph.symm : (a : (↑(range f) : Type u_2)) → X)
          (Subtype.mk (p := fun (x : Y) ↦ x ∈ range f) (f x) ⋯)) :
      (↑(range f) : Type u_2))
    ((hf.toHomeomorph : (a : X) → (↑(range f) : Type u_2)) x : (↑(range f) : Type u_2))
have a : Eq.{u_2 + 1} (α := Y)
  (↑((hf.toHomeomorph : (a : X) → (↑(range f) : Type u_2))
        ((hf.toHomeomorph.symm : (a : (↑(range f) : Type u_2)) → X)
          (Subtype.mk (p := fun (x : Y) ↦ x ∈ range f) (f x) sorry))) :
    Y)
  (↑((hf.toHomeomorph : (a : X) → (↑(range f) : Type u_2)) x) : Y)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
inst_3 : T2Space Y
f : X ≃ Y
hf : Continuous[inst, inst_1] (⇑f : (a : X) → Y)
⊢ Continuous[inst_1, inst] (⇑f.symm : (a : Y) → X)
have rw : ∀ (s : Set X), IsClosed[inst] s → IsClosed[inst_1] ((⇑f.symm : (a : Y) → X) ⁻¹' s)
Tactic: rw [continuous_iff_isClosed]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
inst_3 : T2Space Y
f : X ≃ Y
hf : Continuous[inst, inst_1] (⇑f : (a : X) → Y)
C : Set X
hC : IsClosed[inst] C
⊢ IsClosed[inst_1] ((⇑f.symm : (a : Y) → X) ⁻¹' C)
have hC' : IsClosed[inst_1] ((⇑f : (a : X) → Y) '' C)
Tactic: have hC' : IsClosed (f '' C) := (hC.isCompact.image hf).isClosed
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
inst_3 : T2Space Y
f : X ≃ Y
hf : Continuous[inst, inst_1] (⇑f : (a : X) → Y)
C : Set X
hC : IsClosed[inst] C
hC' : IsClosed[inst_1] ((⇑f : (a : X) → Y) '' C)
⊢ IsClosed[inst_1] ((⇑f.symm : (a : Y) → X) ⁻¹' C)
have rwa : ∀ (hC' : IsClosed[inst_1] ((⇑f.symm : (a : Y) → X) ⁻¹' C)), IsClosed[inst_1] ((⇑f.symm : (a : Y) → X) ⁻¹' C)
Tactic: rwa [Equiv.image_eq_preimage_symm] at hC'
Cleared hypotheses: hC'
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
W_1 : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
W : Type u_5
inst_3 : TopologicalSpace W
f : X → Y
hf : IsHomeomorph f
⊢ Continuous[inst_1, inst] (Equiv.ofBijective f ⋯).invFun
have rw : ContinuousOn (Equiv.ofBijective f sorry).invFun (range f)
Tactic: rw [← continuousOn_univ, ← hf.bijective.2.range_eq]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ IsHomeomorph f ↔
    Continuous[inst, inst_1] f ∧ ∃ (g : Y → X), LeftInverse g f ∧ RightInverse g f ∧ Continuous[inst_1, inst] g
have refine_1 : ∀ (hf : IsHomeomorph f), ∃ (g : Y → X), LeftInverse g f ∧ RightInverse g f ∧ Continuous[inst_1, inst] g
Tactic: refine ⟨fun hf ↦ ⟨hf.continuous, ?_⟩, fun ⟨hf, g, hg⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
refine_1 : ∀ (hf : IsHomeomorph f), ∃ (g : Y → X), LeftInverse g f ∧ RightInverse g f ∧ Continuous[inst_1, inst] g
⊢ IsHomeomorph f ↔
    Continuous[inst, inst_1] f ∧ ∃ (g : Y → X), LeftInverse g f ∧ RightInverse g f ∧ Continuous[inst_1, inst] g
have refine_2 : (Continuous[inst, inst_1] f ∧ ∃ (g : Y → X), LeftInverse g f ∧ RightInverse g f ∧ Continuous[inst_1, inst] g) →
  ∀ (hf : Continuous[inst, inst_1] f) (g : Y → X)
    (hg : LeftInverse g f ∧ RightInverse g f ∧ Continuous[inst_1, inst] g), IsHomeomorph f
Tactic: refine ⟨fun hf ↦ ⟨hf.continuous, ?_⟩, fun ⟨hf, g, hg⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X ≃ Y
⊢ IsHomeomorph.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y) ↔
    Continuous[inst, inst_1] (⇑e : (a : X) → Y) ∧ Continuous[inst_1, inst] (⇑e.symm : (a : Y) → X)
have rw : IsHomeomorph.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y) ↔
  Continuous[inst, inst_1] (⇑e : (a : X) → Y) ∧ IsOpenMap.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
Tactic: rw [e.continuous_symm_iff]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ IsHomeomorph f ↔ IsQuotientMap f ∧ Injective f
have refine : ∀ (h : IsQuotientMap f ∧ Injective f) (s : Set X) (hs : IsOpen[inst] s), IsOpen[inst_1] (f '' s)
Tactic: refine ⟨fun h ↦ ⟨h.isQuotientMap, h.injective⟩,
    fun h ↦ ⟨h.1.continuous, fun s hs ↦ ?_, h.2, h.1.surjective⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsQuotientMap f ∧ Injective f
s : Set X
hs : IsOpen[inst] s
⊢ IsOpen[inst_1] (f '' s)
have rwa : IsOpen[inst] (f ⁻¹' f '' s)
Tactic: rwa [← h.1.isOpen_preimage, Set.preimage_image_eq _ h.2]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : CompactSpace X
inst_3 : T2Space Y
⊢ IsHomeomorph f ↔ Continuous[inst, inst_1] f ∧ Bijective f
have rw : Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ Bijective f ↔ Continuous[inst, inst_1] f ∧ Bijective f
Tactic: rw [isHomeomorph_iff_continuous_isClosedMap_bijective]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : CompactSpace X
inst_3 : T2Space Y
⊢ Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ Bijective f ↔ Continuous[inst, inst_1] f ∧ Bijective f
have refine : ∀ (hf : Continuous[inst, inst_1] f), IsClosedMap f ∧ Bijective f ↔ Bijective f
Tactic: refine and_congr_right fun hf ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : CompactSpace X
inst_3 : T2Space Y
hf : Continuous[inst, inst_1] f
⊢ IsClosedMap f ∧ Bijective f ↔ Bijective f
have rw : True ∧ Bijective f ↔ Bijective f
Tactic: rw [eq_true hf.isClosedMap, true_and]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : CompactSpace X
inst_3 : T2Space Y
hf : Continuous[inst, inst_1] f
rw : True ∧ Bijective f ↔ Bijective f
⊢ IsClosedMap f ∧ Bijective f ↔ Bijective f
have rw₁ : Bijective f ↔ Bijective f
Tactic: rw [eq_true hf.isClosedMap, true_and]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
ι : Type u_6
κ : Type u_7
X : ι → Type u_8
Y : κ → Type u_9
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : (i : κ) → TopologicalSpace (Y i)
f : ι → κ
hf : Bijective f
g : (i : ι) → X i → Y (f i)
hg : ∀ (i : ι), IsHomeomorph (g i)
⊢ IsHomeomorph (Sigma.map (β₁ := X) (β₂ := Y) f g)
have simp_rw : ∀ (hg : ∀ (i : ι), IsEmbedding (g i) ∧ Surjective (g i)),
  IsEmbedding (Sigma.map (β₁ := X) (β₂ := Y) f g) ∧ Surjective (Sigma.map (β₁ := X) (β₂ := Y) f g)
Tactic: simp_rw [isHomeomorph_iff_isEmbedding_surjective] at hg ⊢
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
W_1 : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
W : Type u_5
inst_3 : TopologicalSpace W
f_1 f : X → Y
hf : IsCoinducing f
hf' : ∀ (y : Y), IsConnected (f ⁻¹' {y})
⊢ IsHomeomorph ⋯.connectedComponentsMap
have hbij : Bijective sorry.connectedComponentsMap
Tactic: have hbij := hf.connectedComponentsMap_bijective hf'
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.TransferInstance (goal)
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
e : α ≃ β
this : TopologicalSpace α := e.topologicalSpace
⊢ Continuous e.invFun
have simp : Continuous.{u_3, u_2} (X := β) (Y := α) (⇑e.symm : (a : β) → α)
Tactic: simp only [Equiv.invFun_as_coe]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.TransferInstance (goal)
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
e : α ≃ β
this : TopologicalSpace α := e.topologicalSpace
⊢ Continuous.{u_3, u_2} (X := β) (Y := α) (⇑e.symm : (a : β) → α)
have h : e.topologicalSpace = TopologicalSpace.coinduced (⇑e.symm : (a : β) → α) inst
Tactic: convert! continuous_coinduced_rng
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.TransferInstance (goal)
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
e : α ≃ β
this : TopologicalSpace α := e.topologicalSpace
⊢ e.topologicalSpace = TopologicalSpace.coinduced (⇑e.symm : (a : β) → α) inst
have h : e.topologicalSpace = TopologicalSpace.induced (⇑e : (a : α) → β) inst
Tactic: rw [e.coinduced_symm]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Affine (goal)
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
f g : C(X, E)
⊢ Continuous.{u_1, u_2} (Y := E) fun (x : (↑unitInterval : Type) × X) ↦
    ((Path.segment ((f : (a : X) → E) x.2) ((g : (a : X) → E) x.2) :
          Path (X := E) ((f : (a : X) → E) x.2 : E) ((g : (a : X) → E) x.2 : E)) :
        (a : (↑unitInterval : Type)) → E)
      x.1
have dsimp : Continuous.{u_1, u_2} (Y := E) fun (x : (↑unitInterval : Type) × X) ↦
  HAdd.hAdd (β := E) ((↑x.1 : ℝ) • HSub.hSub (α := E) (β := E) ((g : (a : X) → E) x.2 : E) ((f : (a : X) → E) x.2 : E))
    ((f : (a : X) → E) x.2 : E)
Tactic: dsimp [AffineMap.lineMap_apply]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
Goal:
F : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
f₀ f₁ : C(X, Y)
f g : f₀.Homotopy f₁
h :
  Eq (α := (a : (↑I : Type) × X) → Y) ((fun (f : f₀.Homotopy f₁) ↦ f.toFun) f) ((fun (f : f₀.Homotopy f₁) ↦ f.toFun) g)
⊢ f = g
have obtain : ∀ (toFun : (↑I : Type) × X → Y) (continuous_toFun : Continuous toFun)
  (map_zero_left :
    ∀ (x : X),
      { toFun := toFun, continuous_toFun := continuous_toFun : ContinuousMap.{u, v} ((↑I : Type) × X) Y }.toFun (0, x) =
        (f₀ : (a : X) → Y) x)
  (map_one_left :
    ∀ (x : X),
      { toFun := toFun, continuous_toFun := continuous_toFun : ContinuousMap.{u, v} ((↑I : Type) × X) Y }.toFun (1, x) =
        (f₁ : (a : X) → Y) x)
  (h :
    Eq (α := (a : (↑I : Type) × X) → Y)
      ((fun (f : f₀.Homotopy f₁) ↦ f.toFun)
        { toFun := toFun, continuous_toFun := continuous_toFun, map_zero_left := map_zero_left,
          map_one_left := map_one_left })
      ((fun (f : f₀.Homotopy f₁) ↦ f.toFun) g)),
  { toFun := toFun, continuous_toFun := continuous_toFun, map_zero_left := map_zero_left, map_one_left := map_one_left :
      f₀.Homotopy f₁ } =
    g
Tactic: obtain ⟨⟨_, _⟩, _⟩ := f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
Goal:
F : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
f₀ f₁ : C(X, Y)
g : f₀.Homotopy f₁
toFun : (↑I : Type) × X → Y
continuous_toFun : Continuous toFun
map_zero_left :
  ∀ (x : X),
    { toFun := toFun, continuous_toFun := continuous_toFun : ContinuousMap.{u, v} ((↑I : Type) × X) Y }.toFun (0, x) =
      (f₀ : (a : X) → Y) x
map_one_left :
  ∀ (x : X),
    { toFun := toFun, continuous_toFun := continuous_toFun : ContinuousMap.{u, v} ((↑I : Type) × X) Y }.toFun (1, x) =
      (f₁ : (a : X) → Y) x
h :
  Eq (α := (a : (↑I : Type) × X) → Y)
    ((fun (f : f₀.Homotopy f₁) ↦ f.toFun)
      { toFun := toFun, continuous_toFun := continuous_toFun, map_zero_left := map_zero_left,
        map_one_left := map_one_left })
    ((fun (f : f₀.Homotopy f₁) ↦ f.toFun) g)
⊢ { toFun := toFun, continuous_toFun := continuous_toFun, map_zero_left := map_zero_left, map_one_left := map_one_left :
      f₀.Homotopy f₁ } =
    g
have obtain : ∀ (toFun_1 : (↑I : Type) × X → Y) (continuous_toFun_1 : Continuous toFun_1)
  (map_zero_left_1 :
    ∀ (x : X),
      { toFun := toFun_1, continuous_toFun := continuous_toFun_1 : ContinuousMap.{u, v} ((↑I : Type) × X) Y }.toFun
          (0, x) =
        (f₀ : (a : X) → Y) x)
  (map_one_left_1 :
    ∀ (x : X),
      { toFun := toFun_1, continuous_toFun := continuous_toFun_1 : ContinuousMap.{u, v} ((↑I : Type) × X) Y }.toFun
          (1, x) =
        (f₁ : (a : X) → Y) x)
  (h :
    Eq (α := (a : (↑I : Type) × X) → Y)
      ((fun (f : f₀.Homotopy f₁) ↦ f.toFun)
        { toFun := toFun, continuous_toFun := continuous_toFun, map_zero_left := map_zero_left,
          map_one_left := map_one_left })
      ((fun (f : f₀.Homotopy f₁) ↦ f.toFun)
        { toFun := toFun_1, continuous_toFun := continuous_toFun_1, map_zero_left := map_zero_left_1,
          map_one_left := map_one_left_1 })),
  { toFun := toFun, continuous_toFun := continuous_toFun, map_zero_left := map_zero_left, map_one_left := map_one_left :
      f₀.Homotopy f₁ } =
    { toFun := toFun_1, continuous_toFun := continuous_toFun_1, map_zero_left := map_zero_left_1,
      map_one_left := map_one_left_1 }
Tactic: obtain ⟨⟨_, _⟩, _⟩ := g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
⊢ (F.curry : (a : (↑I : Type)) → C(X, Y)) 0 = f₀
have h : ∀ (a : X),
  Eq.{v + 1} (α := Y) ((((F.curry : (a : (↑I : Type)) → C(X, Y)) 0 : C(X, Y)) : (a : X) → Y) a : Y)
    ((f₀ : (a : X) → Y) a : Y)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
⊢ (F.curry : (a : (↑I : Type)) → C(X, Y)) 1 = f₁
have h : ∀ (a : X),
  Eq.{v + 1} (α := Y) ((((F.curry : (a : (↑I : Type)) → C(X, Y)) 1 : C(X, Y)) : (a : X) → Y) a : Y)
    ((f₁ : (a : X) → Y) a : Y)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
t : ℝ
ht : t ≤ 0
x : X
⊢ Eq.{v + 1} (α := Y) ((((F.extend : (a : ℝ) → C(X, Y)) t : C(X, Y)) : (a : X) → Y) x : Y) ((f₀ : (a : X) → Y) x : Y)
have rw : Eq.{v + 1} (α := Y) ((((F.extend : (a : ℝ) → C(X, Y)) t : C(X, Y)) : (a : X) → Y) x : Y)
  ((F : (a : (↑I : Type) × X) → Y) (0, x) : Y)
Tactic: rw [← F.apply_zero]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
t : ℝ
ht : 1 ≤ t
x : X
⊢ Eq.{v + 1} (α := Y) ((((F.extend : (a : ℝ) → C(X, Y)) t : C(X, Y)) : (a : X) → Y) x : Y) ((f₁ : (a : X) → Y) x : Y)
have rw : Eq.{v + 1} (α := Y) ((((F.extend : (a : ℝ) → C(X, Y)) t : C(X, Y)) : (a : X) → Y) x : Y)
  ((F : (a : (↑I : Type) × X) → Y) (1, x) : Y)
Tactic: rw [← F.apply_one]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
⊢ F.symm.symm = F
have h : ∀ (x : (↑I : Type) × X),
  Eq.{v + 1} (α := Y) ((F.symm.symm : (a : (↑I : Type) × X) → Y) x : Y) ((F : (a : (↑I : Type) × X) → Y) x : Y)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : (↑I : Type) × X
⊢ Eq.{v + 1} (α := Y)
    (if (↑x.1 : ℝ) ≤ 1 / 2 then (((F.extend : (a : ℝ) → C(X, Y)) (2 * (↑x.1 : ℝ)) : C(X, Y)) : (a : X) → Y) x.2
      else (((G.extend : (a : ℝ) → C(X, Y)) (2 * (↑x.1 : ℝ) - 1) : C(X, Y)) : (a : X) → Y) x.2 :
      Y)
    (if h : (↑x.1 : ℝ) ≤ 1 / 2 then
        (F : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.1 : ℝ)) ⋯, x.2)
      else (G : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.1 : ℝ) - 1) ⋯, x.2) :
      Y)
have pos : ∀ (h : (↑x.1 : ℝ) ≤ 1 / 2),
  Eq.{v + 1} (α := Y) ((((F.extend : (a : ℝ) → C(X, Y)) (2 * (↑x.1 : ℝ)) : C(X, Y)) : (a : X) → Y) x.2 : Y)
    ((F : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.1 : ℝ)) sorry, x.2) : Y)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Basic (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : (↑I : Type) × X
pos :
  ∀ (h : (↑x.1 : ℝ) ≤ 1 / 2),
    Eq.{v + 1} (α := Y) ((((F.extend : (a : ℝ) → C(X, Y)) (2 * (↑x.1 : ℝ)) : C(X, Y)) : (a : X) → Y) x.2 : Y)
      ((F : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.1 : ℝ)) ⋯, x.2) : Y)
⊢ Eq.{v + 1} (α := Y)
    (if (↑x.1 : ℝ) ≤ 1 / 2 then (((F.extend : (a : ℝ) → C(X, Y)) (2 * (↑x.1 : ℝ)) : C(X, Y)) : (a : X) → Y) x.2
      else (((G.extend : (a : ℝ) → C(X, Y)) (2 * (↑x.1 : ℝ) - 1) : C(X, Y)) : (a : X) → Y) x.2 :
      Y)
    (if h : (↑x.1 : ℝ) ≤ 1 / 2 then
        (F : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.1 : ℝ)) ⋯, x.2)
      else (G : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.1 : ℝ) - 1) ⋯, x.2) :
      Y)
have neg : ∀ (h : ¬(↑x.1 : ℝ) ≤ 1 / 2),
  Eq.{v + 1} (α := Y) ((((G.extend : (a : ℝ) → C(X, Y)) (2 * (↑x.1 : ℝ) - 1) : C(X, Y)) : (a : X) → Y) x.2 : Y)
    ((G : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.1 : ℝ) - 1) sorry, x.2) : Y)
Tactic: split_ifs