awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x t : (↑I : Type)
ht : Membership.mem (γ := Set (↑I : Type)) {0, 1} t
inl :
  ∀ (ht : t = 0),
    Eq (α := X)
      (({
              toFun := fun (x_1 : (↑I : Type)) ↦
                if (↑(x, x_1).2 : ℝ) ≤ 1 / 2 then ((F.eval (x, x_1).1).extend : (a : ℝ) → X) (2 * (↑(x, x_1).2 : ℝ))
                else ((G.eval (x, x_1).1).extend : (a : ℝ) → X) (2 * (↑(x, x_1).2 : ℝ) - 1),
              continuous_toFun := ⋯ : C((↑I : Type), X) } :
            (a : (↑I : Type)) → X)
          t :
        X)
      (((p₀.trans p₁).toContinuousMap : (a : (↑I : Type)) → X) t : X)
⊢ Eq (α := X)
    (({
            toFun := fun (x_1 : (↑I : Type)) ↦
              if (↑(x, x_1).2 : ℝ) ≤ 1 / 2 then ((F.eval (x, x_1).1).extend : (a : ℝ) → X) (2 * (↑(x, x_1).2 : ℝ))
              else ((G.eval (x, x_1).1).extend : (a : ℝ) → X) (2 * (↑(x, x_1).2 : ℝ) - 1),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        t :
      X)
    (((p₀.trans p₁).toContinuousMap : (a : (↑I : Type)) → X) t : X)
have inr : ∀ (ht : Membership.mem (γ := Set (↑I : Type)) {1} t),
  Eq (α := X)
    (({
            toFun := fun (x_1 : (↑I : Type)) ↦
              if (↑(x, x_1).2 : ℝ) ≤ 1 / 2 then ((F.eval (x, x_1).1).extend : (a : ℝ) → X) (2 * (↑(x, x_1).2 : ℝ))
              else ((G.eval (x, x_1).1).extend : (a : ℝ) → X) (2 * (↑(x, x_1).2 : ℝ) - 1),
            continuous_toFun := sorry : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        t :
      X)
    (((p₀.trans p₁).toContinuousMap : (a : (↑I : Type)) → X) t : X)
Tactic: rcases ht with ht | ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (hypothesis)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x t : (↑I : Type)
ht : Membership.mem (γ := Set (↑I : Type)) {1} t
⊢ Eq (α := X)
    (({
            toFun := fun (x_1 : (↑I : Type)) ↦
              if (↑(x, x_1).2 : ℝ) ≤ 1 / 2 then ((F.eval (x, x_1).1).extend : (a : ℝ) → X) (2 * (↑(x, x_1).2 : ℝ))
              else ((G.eval (x, x_1).1).extend : (a : ℝ) → X) (2 * (↑(x, x_1).2 : ℝ) - 1),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        t :
      X)
    (((p₀.trans p₁).toContinuousMap : (a : (↑I : Type)) → X) t : X)
have ht₁ : t = 1
Tactic: rw [Set.mem_singleton_iff] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ x₂ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x : (↑I : Type) × (↑I : Type)
⊢ Eq (α := X)
    (if (↑x.2 : ℝ) ≤ 1 / 2 then ((F.eval x.1).extend : (a : ℝ) → X) (2 * (↑x.2 : ℝ))
      else ((G.eval x.1).extend : (a : ℝ) → X) (2 * (↑x.2 : ℝ) - 1) :
      X)
    (if h : (↑x.2 : ℝ) ≤ 1 / 2 then
        (F.eval x.1 : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.2 : ℝ)) ⋯)
      else (G.eval x.1 : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.2 : ℝ) - 1) ⋯) :
      X)
have pos : ∀ (h : (↑x.2 : ℝ) ≤ 1 / 2),
  Eq (α := X) (((F.eval x.1).extend : (a : ℝ) → X) (2 * (↑x.2 : ℝ)) : X)
    ((F.eval x.1 : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.2 : ℝ)) sorry) : X)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ x₂ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x : (↑I : Type) × (↑I : Type)
pos :
  ∀ (h : (↑x.2 : ℝ) ≤ 1 / 2),
    Eq (α := X) (((F.eval x.1).extend : (a : ℝ) → X) (2 * (↑x.2 : ℝ)) : X)
      ((F.eval x.1 : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.2 : ℝ)) ⋯) : X)
⊢ Eq (α := X)
    (if (↑x.2 : ℝ) ≤ 1 / 2 then ((F.eval x.1).extend : (a : ℝ) → X) (2 * (↑x.2 : ℝ))
      else ((G.eval x.1).extend : (a : ℝ) → X) (2 * (↑x.2 : ℝ) - 1) :
      X)
    (if h : (↑x.2 : ℝ) ≤ 1 / 2 then
        (F.eval x.1 : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.2 : ℝ)) ⋯)
      else (G.eval x.1 : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.2 : ℝ) - 1) ⋯) :
      X)
have neg : ∀ (h : ¬(↑x.2 : ℝ) ≤ 1 / 2),
  Eq (α := X) (((G.eval x.1).extend : (a : ℝ) → X) (2 * (↑x.2 : ℝ) - 1) : X)
    ((G.eval x.1 : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.2 : ℝ) - 1) sorry) : X)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : (↑I : Type) → (↑I : Type)
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t x : (↑I : Type)
hx : Membership.mem (γ := Set (↑I : Type)) {0, 1} x
⊢ Eq (α := X)
    (({
            toFun := fun (x : (↑I : Type)) ↦
              (p : (a : (↑I : Type)) → X)
                (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
                  ((↑(σ (t, x).1) : ℝ) * (↑(t, x).2 : ℝ) + (↑(t, x).1 : ℝ) * (↑(f (t, x).2) : ℝ)) ⋯),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        x :
      X)
    ((p.toContinuousMap : (a : (↑I : Type)) → X) x : X)
have inl : ∀ (hx : x = 0),
  Eq (α := X)
    (({
            toFun := fun (x : (↑I : Type)) ↦
              (p : (a : (↑I : Type)) → X)
                (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
                  ((↑(σ (t, x).1) : ℝ) * (↑(t, x).2 : ℝ) + (↑(t, x).1 : ℝ) * (↑(f (t, x).2) : ℝ)) sorry),
            continuous_toFun := sorry : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        x :
      X)
    ((p.toContinuousMap : (a : (↑I : Type)) → X) x : X)
Tactic: rcases hx with hx | hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : (↑I : Type) → (↑I : Type)
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t x : (↑I : Type)
hx : Membership.mem (γ := Set (↑I : Type)) {0, 1} x
inl :
  ∀ (hx : x = 0),
    Eq (α := X)
      (({
              toFun := fun (x : (↑I : Type)) ↦
                (p : (a : (↑I : Type)) → X)
                  (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
                    ((↑(σ (t, x).1) : ℝ) * (↑(t, x).2 : ℝ) + (↑(t, x).1 : ℝ) * (↑(f (t, x).2) : ℝ)) ⋯),
              continuous_toFun := ⋯ : C((↑I : Type), X) } :
            (a : (↑I : Type)) → X)
          x :
        X)
      ((p.toContinuousMap : (a : (↑I : Type)) → X) x : X)
⊢ Eq (α := X)
    (({
            toFun := fun (x : (↑I : Type)) ↦
              (p : (a : (↑I : Type)) → X)
                (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
                  ((↑(σ (t, x).1) : ℝ) * (↑(t, x).2 : ℝ) + (↑(t, x).1 : ℝ) * (↑(f (t, x).2) : ℝ)) ⋯),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        x :
      X)
    ((p.toContinuousMap : (a : (↑I : Type)) → X) x : X)
have inr : ∀ (hx : Membership.mem (γ := Set (↑I : Type)) {1} x),
  Eq (α := X)
    (({
            toFun := fun (x : (↑I : Type)) ↦
              (p : (a : (↑I : Type)) → X)
                (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
                  ((↑(σ (t, x).1) : ℝ) * (↑(t, x).2 : ℝ) + (↑(t, x).1 : ℝ) * (↑(f (t, x).2) : ℝ)) sorry),
            continuous_toFun := sorry : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        x :
      X)
    ((p.toContinuousMap : (a : (↑I : Type)) → X) x : X)
Tactic: rcases hx with hx | hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : (↑I : Type) → (↑I : Type)
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t x : (↑I : Type)
hx : x = 0
⊢ Eq (α := X)
    (({
            toFun := fun (x : (↑I : Type)) ↦
              (p : (a : (↑I : Type)) → X)
                (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
                  ((↑(σ (t, x).1) : ℝ) * (↑(t, x).2 : ℝ) + (↑(t, x).1 : ℝ) * (↑(f (t, x).2) : ℝ)) ⋯),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        x :
      X)
    ((p.toContinuousMap : (a : (↑I : Type)) → X) x : X)
have inl : Eq (α := X)
  (({
          toFun := fun (x : (↑I : Type)) ↦
            (p : (a : (↑I : Type)) → X)
              (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
                ((↑(σ (t, x).1) : ℝ) * (↑(t, x).2 : ℝ) + (↑(t, x).1 : ℝ) * (↑(f (t, x).2) : ℝ)) sorry),
          continuous_toFun := sorry : C((↑I : Type), X) } :
        (a : (↑I : Type)) → X)
      0 :
    X)
  ((p.toContinuousMap : (a : (↑I : Type)) → X) 0 : X)
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (hypothesis)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : (↑I : Type) → (↑I : Type)
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t x : (↑I : Type)
hx : Membership.mem (γ := Set (↑I : Type)) {1} x
⊢ Eq (α := X)
    (({
            toFun := fun (x : (↑I : Type)) ↦
              (p : (a : (↑I : Type)) → X)
                (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
                  ((↑(σ (t, x).1) : ℝ) * (↑(t, x).2 : ℝ) + (↑(t, x).1 : ℝ) * (↑(f (t, x).2) : ℝ)) ⋯),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        x :
      X)
    ((p.toContinuousMap : (a : (↑I : Type)) → X) x : X)
have hx₁ : x = 1
Tactic: rw [Set.mem_singleton_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : (↑I : Type) → (↑I : Type)
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t x : (↑I : Type)
hx : x = 1
⊢ Eq (α := X)
    (({
            toFun := fun (x : (↑I : Type)) ↦
              (p : (a : (↑I : Type)) → X)
                (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
                  ((↑(σ (t, x).1) : ℝ) * (↑(t, x).2 : ℝ) + (↑(t, x).1 : ℝ) * (↑(f (t, x).2) : ℝ)) ⋯),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        x :
      X)
    ((p.toContinuousMap : (a : (↑I : Type)) → X) x : X)
have inr : Eq (α := X)
  (({
          toFun := fun (x : (↑I : Type)) ↦
            (p : (a : (↑I : Type)) → X)
              (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
                ((↑(σ (t, x).1) : ℝ) * (↑(t, x).2 : ℝ) + (↑(t, x).1 : ℝ) * (↑(f (t, x).2) : ℝ)) sorry),
          continuous_toFun := sorry : C((↑I : Type), X) } :
        (a : (↑I : Type)) → X)
      1 :
    X)
  ((p.toContinuousMap : (a : (↑I : Type)) → X) 1 : X)
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
t x : (↑I : Type)
hx : Membership.mem (γ := Set (↑I : Type)) {0, 1} x
⊢ Eq (α := X)
    (({ toFun := fun (x : (↑I : Type)) ↦ (F : (a : (↑I : Type) × (↑I : Type)) → X) ((t, x).1, σ (t, x).2),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        x :
      X)
    ((p.symm.toContinuousMap : (a : (↑I : Type)) → X) x : X)
have inl : ∀ (hx : x = 0),
  Eq (α := X)
    (({ toFun := fun (x : (↑I : Type)) ↦ (F : (a : (↑I : Type) × (↑I : Type)) → X) ((t, x).1, σ (t, x).2),
            continuous_toFun := sorry : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        x :
      X)
    ((p.symm.toContinuousMap : (a : (↑I : Type)) → X) x : X)
Tactic: rcases hx with hx | hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
t x : (↑I : Type)
hx : Membership.mem (γ := Set (↑I : Type)) {0, 1} x
inl :
  ∀ (hx : x = 0),
    Eq (α := X)
      (({ toFun := fun (x : (↑I : Type)) ↦ (F : (a : (↑I : Type) × (↑I : Type)) → X) ((t, x).1, σ (t, x).2),
              continuous_toFun := ⋯ : C((↑I : Type), X) } :
            (a : (↑I : Type)) → X)
          x :
        X)
      ((p.symm.toContinuousMap : (a : (↑I : Type)) → X) x : X)
⊢ Eq (α := X)
    (({ toFun := fun (x : (↑I : Type)) ↦ (F : (a : (↑I : Type) × (↑I : Type)) → X) ((t, x).1, σ (t, x).2),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        x :
      X)
    ((p.symm.toContinuousMap : (a : (↑I : Type)) → X) x : X)
have inr : ∀ (hx : Membership.mem (γ := Set (↑I : Type)) {1} x),
  Eq (α := X)
    (({ toFun := fun (x : (↑I : Type)) ↦ (F : (a : (↑I : Type) × (↑I : Type)) → X) ((t, x).1, σ (t, x).2),
            continuous_toFun := sorry : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        x :
      X)
    ((p.symm.toContinuousMap : (a : (↑I : Type)) → X) x : X)
Tactic: rcases hx with hx | hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
t x : (↑I : Type)
hx : x = 0
⊢ Eq (α := X)
    (({ toFun := fun (x : (↑I : Type)) ↦ (F : (a : (↑I : Type) × (↑I : Type)) → X) ((t, x).1, σ (t, x).2),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        x :
      X)
    ((p.symm.toContinuousMap : (a : (↑I : Type)) → X) x : X)
have inl : Eq (α := X)
  (({ toFun := fun (x : (↑I : Type)) ↦ (F : (a : (↑I : Type) × (↑I : Type)) → X) ((t, x).1, σ (t, x).2),
          continuous_toFun := sorry : C((↑I : Type), X) } :
        (a : (↑I : Type)) → X)
      0 :
    X)
  ((p.symm.toContinuousMap : (a : (↑I : Type)) → X) 0 : X)
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (hypothesis)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
t x : (↑I : Type)
hx : Membership.mem (γ := Set (↑I : Type)) {1} x
⊢ Eq (α := X)
    (({ toFun := fun (x : (↑I : Type)) ↦ (F : (a : (↑I : Type) × (↑I : Type)) → X) ((t, x).1, σ (t, x).2),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        x :
      X)
    ((p.symm.toContinuousMap : (a : (↑I : Type)) → X) x : X)
have hx₁ : x = 1
Tactic: rw [Set.mem_singleton_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
t x : (↑I : Type)
hx : x = 1
⊢ Eq (α := X)
    (({ toFun := fun (x : (↑I : Type)) ↦ (F : (a : (↑I : Type) × (↑I : Type)) → X) ((t, x).1, σ (t, x).2),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        x :
      X)
    ((p.symm.toContinuousMap : (a : (↑I : Type)) → X) x : X)
have inr : Eq (α := X)
  (({ toFun := fun (x : (↑I : Type)) ↦ (F : (a : (↑I : Type) × (↑I : Type)) → X) ((t, x).1, σ (t, x).2),
          continuous_toFun := sorry : C((↑I : Type), X) } :
        (a : (↑I : Type)) → X)
      1 :
    X)
  ((p.symm.toContinuousMap : (a : (↑I : Type)) → X) 1 : X)
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
f : C(X, Y)
t x : (↑I : Type)
hx : Membership.mem (γ := Set (↑I : Type)) {0, 1} x
⊢ Eq (α := Y)
    (({
            toFun := fun (x : (↑I : Type)) ↦
              Function.comp (β := X) (⇑f : (a : X) → Y) (⇑F : (a : (↑I : Type) × (↑I : Type)) → X) (t, x),
            continuous_toFun := ⋯ : C((↑I : Type), Y) } :
          (a : (↑I : Type)) → Y)
        x :
      Y)
    (((p.map ⋯).toContinuousMap : (a : (↑I : Type)) → Y) x : Y)
have inl : ∀ (hx : x = 0),
  Eq (α := Y)
    (({
            toFun := fun (x : (↑I : Type)) ↦
              Function.comp (β := X) (⇑f : (a : X) → Y) (⇑F : (a : (↑I : Type) × (↑I : Type)) → X) (t, x),
            continuous_toFun := sorry : C((↑I : Type), Y) } :
          (a : (↑I : Type)) → Y)
        x :
      Y)
    (((p.map sorry).toContinuousMap : (a : (↑I : Type)) → Y) x : Y)
Tactic: rcases hx with hx | hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
f : C(X, Y)
t x : (↑I : Type)
hx : Membership.mem (γ := Set (↑I : Type)) {0, 1} x
inl :
  ∀ (hx : x = 0),
    Eq (α := Y)
      (({
              toFun := fun (x : (↑I : Type)) ↦
                Function.comp (β := X) (⇑f : (a : X) → Y) (⇑F : (a : (↑I : Type) × (↑I : Type)) → X) (t, x),
              continuous_toFun := ⋯ : C((↑I : Type), Y) } :
            (a : (↑I : Type)) → Y)
          x :
        Y)
      (((p.map ⋯).toContinuousMap : (a : (↑I : Type)) → Y) x : Y)
⊢ Eq (α := Y)
    (({
            toFun := fun (x : (↑I : Type)) ↦
              Function.comp (β := X) (⇑f : (a : X) → Y) (⇑F : (a : (↑I : Type) × (↑I : Type)) → X) (t, x),
            continuous_toFun := ⋯ : C((↑I : Type), Y) } :
          (a : (↑I : Type)) → Y)
        x :
      Y)
    (((p.map ⋯).toContinuousMap : (a : (↑I : Type)) → Y) x : Y)
have inr : ∀ (hx : Membership.mem (γ := Set (↑I : Type)) {1} x),
  Eq (α := Y)
    (({
            toFun := fun (x : (↑I : Type)) ↦
              Function.comp (β := X) (⇑f : (a : X) → Y) (⇑F : (a : (↑I : Type) × (↑I : Type)) → X) (t, x),
            continuous_toFun := sorry : C((↑I : Type), Y) } :
          (a : (↑I : Type)) → Y)
        x :
      Y)
    (((p.map sorry).toContinuousMap : (a : (↑I : Type)) → Y) x : Y)
Tactic: rcases hx with hx | hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (hypothesis)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
f : C(X, Y)
t x : (↑I : Type)
hx : Membership.mem (γ := Set (↑I : Type)) {1} x
⊢ Eq (α := Y)
    (({
            toFun := fun (x : (↑I : Type)) ↦
              Function.comp (β := X) (⇑f : (a : X) → Y) (⇑F : (a : (↑I : Type) × (↑I : Type)) → X) (t, x),
            continuous_toFun := ⋯ : C((↑I : Type), Y) } :
          (a : (↑I : Type)) → Y)
        x :
      Y)
    (((p.map ⋯).toContinuousMap : (a : (↑I : Type)) → Y) x : Y)
have hx₁ : x = 1
Tactic: rw [Set.mem_singleton_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (goal)
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type u_1
inst_1 : TopologicalSpace Y
x₀ y₀ : X
x₁ y₁ : Y
motive : Homotopic.Quotient x₀ y₀ → Homotopic.Quotient x₁ y₁ → Prop
mk : ∀ (a : Path x₀ y₀) (b : Path x₁ y₁), motive (Quotient.mk a) (Quotient.mk b)
q₁ : Homotopic.Quotient x₁ y₁
a : Path x₀ y₀
⊢ motive (Quot.mk (⇑(Homotopic.setoid x₀ y₀) : Path x₀ y₀ → Path x₀ y₀ → Prop) a) q₁
have mk₁ : ∀ (b : Path x₁ y₁),
  motive (Quot.mk (⇑(Homotopic.setoid x₀ y₀) : Path x₀ y₀ → Path x₀ y₀ → Prop) a)
    (Quot.mk (⇑(Homotopic.setoid x₁ y₁) : Path x₁ y₁ → Path x₁ y₁ → Prop) b)
Tactic: induction q₁ using Quot.ind with | mk b =>
  exact mk a b
Cleared hypotheses: q₁
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (goal)
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type u_1
inst_1 : TopologicalSpace Y
x₀ y₀ : X
x₁ y₁ : Y
motive : Homotopic.Quotient x₀ y₀ → Homotopic.Quotient x₁ y₁ → Prop
mk : ∀ (a : Path x₀ y₀) (b : Path x₁ y₁), motive (Quotient.mk a) (Quotient.mk b)
q₀ : Homotopic.Quotient x₀ y₀
q₁ : Homotopic.Quotient x₁ y₁
⊢ motive q₀ q₁
have mk₁ : ∀ (a : Path x₀ y₀), motive (Quot.mk (⇑(Homotopic.setoid x₀ y₀) : Path x₀ y₀ → Path x₀ y₀ → Prop) a) q₁
Tactic: induction q₀ using Quot.ind with | mk a =>
  induction q₁ using Quot.ind with | mk b =>
  exact mk a b
Cleared hypotheses: q₀
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Homotopic.Quotient x y
⊢ γ.cast ⋯ ⋯ = γ
have mk : ∀ (γ : Path x y), (mk γ).cast sorry sorry = mk γ
Tactic: induction γ using Quotient.ind with | mk γ =>
  rfl
Cleared hypotheses: γ
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Homotopic.Quotient x y
x' y' : X
hx : x' = x
hy : y' = y
x'' y'' : X
hx' : x'' = x'
hy' : y'' = y'
⊢ (γ.cast hx hy).cast hx' hy' = γ.cast ⋯ ⋯
have mk : ∀ (γ : Path x y), ((mk γ).cast hx hy).cast hx' hy' = (mk γ).cast sorry sorry
Tactic: induction γ using Quotient.ind with | mk γ =>
  rfl
Cleared hypotheses: γ
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p₁ : Path x₀ x₁
p₂ : Path x₂ x₃
hp : ∀ (t : (↑I : Type)), Eq (α := X) ((p₁ : (a : (↑I : Type)) → X) t : X) ((p₂ : (a : (↑I : Type)) → X) t : X)
⊢ x₀ = x₂
have h : x₀ = (p₁ : (a : (↑I : Type)) → X) 0
Tactic: convert! hp 0
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p₁ : Path x₀ x₁
p₂ : Path x₂ x₃
hp : ∀ (t : (↑I : Type)), Eq (α := X) ((p₁ : (a : (↑I : Type)) → X) t : X) ((p₂ : (a : (↑I : Type)) → X) t : X)
h : x₀ = (p₁ : (a : (↑I : Type)) → X) 0
⊢ x₀ = x₂
have h₁ : x₂ = (p₂ : (a : (↑I : Type)) → X) 0
Tactic: convert! hp 0
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p₁ : Path x₀ x₁
p₂ : Path x₂ x₃
hp : ∀ (t : (↑I : Type)), Eq (α := X) ((p₁ : (a : (↑I : Type)) → X) t : X) ((p₂ : (a : (↑I : Type)) → X) t : X)
⊢ HEq (α := Homotopic.Quotient x₀ x₁) ⟦p₁⟧ (β := Homotopic.Quotient x₂ x₃) ⟦p₂⟧
have obtain : ∀ {p₂ : Path x₀ x₃}
  (hp : ∀ (t : (↑I : Type)), Eq (α := X) ((p₁ : (a : (↑I : Type)) → X) t : X) ((p₂ : (a : (↑I : Type)) → X) t : X)),
  HEq (α := Homotopic.Quotient x₀ x₁) ⟦p₁⟧ (β := Homotopic.Quotient x₀ x₃) ⟦p₂⟧
Tactic: obtain rfl : x₀ = x₂ := by convert! hp 0 <;> simp
Cleared hypotheses: x₂, p₂, hp
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ x₃ : X
p₁ : Path x₀ x₁
p₂ : Path x₀ x₃
hp : ∀ (t : (↑I : Type)), Eq (α := X) ((p₁ : (a : (↑I : Type)) → X) t : X) ((p₂ : (a : (↑I : Type)) → X) t : X)
⊢ x₁ = x₃
have h : x₁ = (p₁ : (a : (↑I : Type)) → X) 1
Tactic: convert! hp 1
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ x₃ : X
p₁ : Path x₀ x₁
p₂ : Path x₀ x₃
hp : ∀ (t : (↑I : Type)), Eq (α := X) ((p₁ : (a : (↑I : Type)) → X) t : X) ((p₂ : (a : (↑I : Type)) → X) t : X)
h : x₁ = (p₁ : (a : (↑I : Type)) → X) 1
⊢ x₁ = x₃
have h₁ : x₃ = (p₂ : (a : (↑I : Type)) → X) 1
Tactic: convert! hp 1
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ x₃ : X
p₁ : Path x₀ x₁
p₂ : Path x₀ x₃
hp : ∀ (t : (↑I : Type)), Eq (α := X) ((p₁ : (a : (↑I : Type)) → X) t : X) ((p₂ : (a : (↑I : Type)) → X) t : X)
⊢ HEq (α := Homotopic.Quotient x₀ x₁) ⟦p₁⟧ (β := Homotopic.Quotient x₀ x₃) ⟦p₂⟧
have obtain : ∀ {p₂ : Path x₀ x₁}
  (hp : ∀ (t : (↑I : Type)), Eq (α := X) ((p₁ : (a : (↑I : Type)) → X) t : X) ((p₂ : (a : (↑I : Type)) → X) t : X)),
  HEq (α := Homotopic.Quotient x₀ x₁) ⟦p₁⟧ (β := Homotopic.Quotient x₀ x₁) ⟦p₂⟧
Tactic: obtain rfl : x₁ = x₃ := by convert! hp 1 <;> simp
Cleared hypotheses: x₃, p₂, hp
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ : X
p₁ p₂ : Path x₀ x₁
hp : ∀ (t : (↑I : Type)), Eq (α := X) ((p₁ : (a : (↑I : Type)) → X) t : X) ((p₂ : (a : (↑I : Type)) → X) t : X)
⊢ HEq (α := Homotopic.Quotient x₀ x₁) ⟦p₁⟧ (β := Homotopic.Quotient x₀ x₁) ⟦p₂⟧
have rw : Eq (α := Homotopic.Quotient x₀ x₁) ⟦p₁⟧ ⟦p₂⟧
Tactic: rw [heq_iff_eq]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ : X
p₁ p₂ : Path x₀ x₁
hp : ∀ (t : (↑I : Type)), Eq (α := X) ((p₁ : (a : (↑I : Type)) → X) t : X) ((p₂ : (a : (↑I : Type)) → X) t : X)
⊢ Eq (α := Homotopic.Quotient x₀ x₁) ⟦p₁⟧ ⟦p₂⟧
have e_a : p₁ = p₂
Tactic: congr