awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Homotopy.Path
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)
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 := ⋯ : 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)

Tactic:
rcases hx with hx | hx
-- Module: Mathlib.Topology.Homotopy.Path
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 : 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)

Tactic:
simp [hx]
-- Module: Mathlib.Topology.Homotopy.Path
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
⊢ x = 1

Tactic:
rw [Set.mem_singleton_iff] at hx

Premises used: Set.mem_singleton_iff
-- Module: Mathlib.Topology.Homotopy.Path
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 : x = 1
⊢ 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)

Tactic:
simp [hx]
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
⊢ p.Homotopic p

Tactic:
⟨Homotopy.refl p⟩

Premises used: Path.Homotopy.refl, Nonempty.intro, Path.Homotopic
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ : X
p₀ p₁ : Path x₀ x₁
h : p₀.Homotopic p₁
⊢ p₁.Homotopic p₀

Tactic:
h.map Homotopy.symm

Premises used: Nonempty.map, Path.Homotopic, Path.Homotopy.symm
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ : X
p q : Path x₀ x₁
h : p.Homotopic q
⊢ p.symm.Homotopic q.symm

Tactic:
h.map Homotopy.symm₂

Premises used: Path.Homotopy.symm₂, Nonempty.map, Path.Homotopic
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ : X
p₀ p₁ p₂ : Path x₀ x₁
h₀ : p₀.Homotopic p₁
h₁ : p₁.Homotopic p₂
⊢ p₀.Homotopic p₂

Tactic:
h₀.map2 Homotopy.trans h₁

Premises used: Path.Homotopy.trans, Nonempty.map2, Path.Homotopic
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ : X
⊢ Equivalence.{u + 1} (α := Path x₀ x₁) Homotopic

Tactic:
⟨refl, (symm ·), (trans · ·)⟩

Premises used: Path.Homotopic.trans, Path.Homotopic.symm, Path.Homotopic.refl, Equivalence.mk
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
p q : Path x₀ x₁
h : p.Homotopic q
f : C(X, Y)
⊢ (p.map ⋯).Homotopic (q.map ⋯)

Tactic:
h.map fun F => F.map f

Premises used: Nonempty.map, Path.Homotopic
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ x₂ : X
p₀ p₁ : Path x₀ x₁
q₀ q₁ : Path x₁ x₂
hp : p₀.Homotopic p₁
hq : q₀.Homotopic q₁
⊢ (p₀.trans q₀).Homotopic (p₁.trans q₁)

Tactic:
hp.map2 Homotopy.hcomp hq

Premises used: Nonempty.map2, Path.Homotopy.hcomp, Path.Homotopic
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
hpq : p.Homotopic q
hsource : x₂ = x₀
htarget : x₃ = x₁
⊢ (p.cast hsource htarget).Homotopic (q.cast hsource htarget)

Tactic:
hpq

Premises used: Path.cast, Path.Homotopic
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ : X
⊢ Function.Surjective.{u + 1, u + 1} (α := Path x₀ x₁) mk

Tactic:
Quotient.mk'_surjective

Premises used: Quotient.mk'_surjective, Path.Homotopic.Quotient, Path.Homotopic.Quotient.mk
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
⊢ Quotient.mk' p = mk p

Tactic:
rfl

Premises used: rfl, Path.Homotopic.Quotient.mk
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
⊢ Quotient.mk'' p = mk p

Tactic:
rfl

Premises used: Quotient.mk', rfl, Path.Homotopic.Quotient.mk
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ : X
p q : Path x₀ x₁
h : mk p = mk q
⊢ p.Homotopic q

Tactic:
_root_.Quotient.exact h

Premises used: Quotient.exact
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ : X
p q : Path x₀ x₁
h : mk p = mk q
⊢ p.Homotopic q

Tactic:
exact _root_.Quotient.exact h

Premises used: Quotient.exact
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ : X
p q : Path x₀ x₁
⊢ mk p = mk q ↔ p.Homotopic q

Tactic:
_root_.Quotient.eq

Premises used: Path.Homotopic.Quotient, Quotient.mk', Quotient.eq, Path.Homotopic.Quotient.mk
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
motive : Homotopic.Quotient x y → Prop
⊢ ∀ (mk : ∀ (a : Path x y), motive (mk a)) (q : Homotopic.Quotient x y), motive q

Tactic:
Quot.ind

Premises used: Quot.ind, Path.Homotopic.Quotient, Quotient, Quotient.mk', Path.Homotopic.Quotient.mk
-- Module: Mathlib.Topology.Homotopy.Path
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)
a : Path x₀ y₀
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:
mk a b

Premises used: Quotient.mk', Path.Homotopic.Quotient.mk
-- Module: Mathlib.Topology.Homotopy.Path
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)
a : Path x₀ y₀
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:
exact mk a b
-- Module: Mathlib.Topology.Homotopy.Path
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₀
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)
⊢ motive (Quot.mk (⇑(Homotopic.setoid x₀ y₀) : Path x₀ y₀ → Path x₀ y₀ → Prop) a) q₁

Tactic:
induction q₁ using Quot.ind with | mk b =>
  exact mk a b

Premises used: Quot.ind
-- Module: Mathlib.Topology.Homotopy.Path
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₁
mk₁ : ∀ (a : Path x₀ y₀), motive (Quot.mk (⇑(Homotopic.setoid x₀ y₀) : Path x₀ y₀ → Path x₀ y₀ → Prop) a) q₁
⊢ motive q₀ q₁

Tactic:
induction q₀ using Quot.ind with | mk a =>
  induction q₁ using Quot.ind with | mk b =>
  exact mk a b

Premises used: Quot.ind
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x : X
⊢ Eq (α := Homotopic.Quotient x x) (mk (Path.refl x)) (refl x)

Tactic:
rfl

Premises used: Path.Homotopic.Quotient.refl, rfl
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ : X
P : Path x₀ x₁
⊢ mk P.symm = (mk P).symm

Tactic:
rfl

Premises used: Quotient.map, Quot.map, Path.Homotopic.Quotient.symm, rfl, Path.Homotopic.Quotient.mk
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
P : Path x y
x' y' : X
hx : x' = x
hy : y' = y
⊢ mk (P.cast hx hy) = (mk P).cast hx hy

Tactic:
rfl

Premises used: Quotient.map, Path.Homotopic.Quotient.cast, Quot.map, rfl, Path.Homotopic.Quotient.mk
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
⊢ (mk γ).cast ⋯ ⋯ = mk γ

Tactic:
rfl
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Homotopic.Quotient x y
mk : ∀ (γ : Path x y), (Quotient.mk γ).cast ⋯ ⋯ = Quotient.mk γ
⊢ γ.cast ⋯ ⋯ = γ

Tactic:
induction γ using Quotient.ind with | mk γ =>
  rfl

Premises used: Path.Homotopic.Quotient.ind, Path.Homotopic.Quotient.mk
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x y x' y' : X
hx : x' = x
hy : y' = y
x'' y'' : X
hx' : x'' = x'
hy' : y'' = y'
γ : Path x y
⊢ ((mk γ).cast hx hy).cast hx' hy' = (mk γ).cast ⋯ ⋯

Tactic:
rfl
-- Module: Mathlib.Topology.Homotopy.Path
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'
mk : ∀ (γ : Path x y), ((Quotient.mk γ).cast hx hy).cast hx' hy' = (Quotient.mk γ).cast ⋯ ⋯
⊢ (γ.cast hx hy).cast hx' hy' = γ.cast ⋯ ⋯

Tactic:
induction γ using Quotient.ind with | mk γ =>
  rfl

Premises used: Path.Homotopic.Quotient.ind, Path.Homotopic.Quotient.mk
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ x₂ : X
P₀ : Path x₀ x₁
P₁ : Path x₁ x₂
⊢ mk (P₀.trans P₁) = (mk P₀).trans (mk P₁)

Tactic:
rfl

Premises used: Quotient.map₂, Path.Homotopic.Quotient.trans, rfl, Path.Homotopic.Quotient.mk
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
P₀ : Path x₀ x₁
f : C(X, Y)
⊢ mk (P₀.map ⋯) = (mk P₀).map f

Tactic:
rfl

Premises used: Quotient.map, Path.Homotopic.Quotient.map, Quot.map, rfl, Path.Homotopic.Quotient.mk
-- Module: Mathlib.Topology.Homotopy.Path
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)
⊢ Eq (α := X) ((p₁ : (a : (↑I : Type)) → X) 0 : X) ((p₂ : (a : (↑I : Type)) → X) 0 : X)

Tactic:
hp 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Topology.Homotopy.Path
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
h₁ : x₂ = (p₂ : (a : (↑I : Type)) → X) 0
⊢ x₀ = x₂

Tactic:
convert! hp 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Topology.Homotopy.Path
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₀ = (p₁ : (a : (↑I : Type)) → X) 0

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.Path
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₂ = (p₂ : (a : (↑I : Type)) → X) 0

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.Path
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)
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₂⟧
⊢ HEq (α := Homotopic.Quotient x₀ x₁) ⟦p₁⟧ (β := Homotopic.Quotient x₂ x₃) ⟦p₂⟧

Tactic:
obtain rfl : x₀ = x₂ := by convert! hp 0 <;> simp

Premises used: rfl
-- Module: Mathlib.Topology.Homotopy.Path
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)
⊢ Eq (α := X) ((p₁ : (a : (↑I : Type)) → X) 1 : X) ((p₂ : (a : (↑I : Type)) → X) 1 : X)

Tactic:
hp 1

Premises used: OfNat.ofNat
-- Module: Mathlib.Topology.Homotopy.Path
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
h₁ : x₃ = (p₂ : (a : (↑I : Type)) → X) 1
⊢ x₁ = x₃

Tactic:
convert! hp 1

Premises used: OfNat.ofNat
-- Module: Mathlib.Topology.Homotopy.Path
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₁ = (p₁ : (a : (↑I : Type)) → X) 1

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.Path
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₃ = (p₂ : (a : (↑I : Type)) → X) 1

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.Path
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)
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₂⟧
⊢ HEq (α := Homotopic.Quotient x₀ x₁) ⟦p₁⟧ (β := Homotopic.Quotient x₀ x₃) ⟦p₂⟧

Tactic:
obtain rfl : x₁ = x₃ := by convert! hp 1 <;> simp

Premises used: rfl
-- Module: Mathlib.Topology.Homotopy.Path
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)
rw : Eq (α := Homotopic.Quotient x₀ x₁) ⟦p₁⟧ ⟦p₂⟧
⊢ HEq (α := Homotopic.Quotient x₀ x₁) ⟦p₁⟧ (β := Homotopic.Quotient x₀ x₁) ⟦p₂⟧

Tactic:
rw [heq_iff_eq]

Premises used: heq_iff_eq
-- Module: Mathlib.Topology.Homotopy.Path
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)
e_a : p₁ = p₂
⊢ Eq (α := Homotopic.Quotient x₀ x₁) ⟦p₁⟧ ⟦p₂⟧

Tactic:
congr
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ : X
p₁ p₂ : Path x₀ x₁
hp e_a : ∀ (t : (↑I : Type)), Eq (α := X) ((p₁ : (a : (↑I : Type)) → X) t : X) ((p₂ : (a : (↑I : Type)) → X) t : X)
⊢ p₁ = p₂

Tactic:
ext t
-- Module: Mathlib.Topology.Homotopy.Path
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)
t : (↑I : Type)
⊢ Eq (α := X) ((p₁ : (a : (↑I : Type)) → X) t : X) ((p₂ : (a : (↑I : Type)) → X) t : X)

Tactic:
hp t
-- Module: Mathlib.Topology.Homotopy.Path
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)
t : (↑I : Type)
⊢ Eq (α := X) ((p₁ : (a : (↑I : Type)) → X) t : X) ((p₂ : (a : (↑I : Type)) → X) t : X)

Tactic:
exact hp t
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
inst_2 : Nonempty Y
inhabit : ∀ (inhabited_h : Inhabited Y), Homotopic (const Y x₀) (const Y x₁) ↔ Joined x₀ x₁
⊢ Homotopic (const Y x₀) (const Y x₁) ↔ Joined x₀ x₁

Tactic:
inhabit Y
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
inst_2 : Nonempty Y
inhabited_h : Inhabited Y
⊢ Homotopic (const Y x₀) (const Y x₁) ↔ Joined x₀ x₁

Tactic:
⟨fun ⟨H⟩ ↦ ⟨⟨(H.toContinuousMap.comp .prodSwap).curry default, ?_, ?_⟩⟩,
    fun ⟨p⟩ ↦ ⟨p.toHomotopyConst⟩⟩

Premises used: Inhabited.default, ContinuousMap.curry, ContinuousMap.comp, ContinuousMap.Homotopy.toContinuousMap, Nonempty.intro, Path.toHomotopyConst, _private.0.ContinuousMap.homotopic_const_iff.match_2, _private.0.ContinuousMap.homotopic_const_iff.match_1, Path.mk, Iff.intro, ContinuousMap.const, ContinuousMap.Homotopic, Joined, DFunLike.coe, ContinuousMap.prodSwap
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
inst_2 : Nonempty Y
inhabited_h : Inhabited Y
refine_1 :
  Homotopic (const Y x₀) (const Y x₁) →
    ∀ (H : Homotopy (const Y x₀) (const Y x₁)),
      ContinuousMap.toFun (X := (↑I : Type)) (((H.comp prodSwap).curry : (a : Y) → C((↑I : Type), X)) default) 0 = x₀
refine_2 :
  Homotopic (const Y x₀) (const Y x₁) →
    ∀ (H : Homotopy (const Y x₀) (const Y x₁)),
      ContinuousMap.toFun (X := (↑I : Type)) (((H.comp prodSwap).curry : (a : Y) → C((↑I : Type), X)) default) 1 = x₁
⊢ Homotopic (const Y x₀) (const Y x₁) ↔ Joined x₀ x₁

Tactic:
refine ⟨fun ⟨H⟩ ↦ ⟨⟨(H.toContinuousMap.comp .prodSwap).curry default, ?_, ?_⟩⟩,
    fun ⟨p⟩ ↦ ⟨p.toHomotopyConst⟩⟩
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
inst_2 : Nonempty Y
inhabited_h : Inhabited Y
h : Homotopic (const Y x₀) (const Y x₁)
H : Homotopy (const Y x₀) (const Y x₁)
⊢ ContinuousMap.toFun (X := (↑I : Type)) (((H.comp prodSwap).curry : (a : Y) → C((↑I : Type), X)) default) 0 = x₀

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
inst_2 : Nonempty Y
inhabited_h : Inhabited Y
h : Homotopic (const Y x₀) (const Y x₁)
H : Homotopy (const Y x₀) (const Y x₁)
⊢ ContinuousMap.toFun (X := (↑I : Type)) (((H.comp prodSwap).curry : (a : Y) → C((↑I : Type), X)) default) 1 = x₁

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f g : C(X, Y)
H : f.Homotopy g
x : X
⊢ Eq (α := (a : ℝ) → Y) (⇑(H.evalAt x).extend : (a : ℝ) → Y) fun (t : ℝ) ↦
    (((H.extend : (a : ℝ) → C(X, Y)) t : C(X, Y)) : (a : X) → Y) x

Tactic:
rfl

Premises used: Set.IccExtend, rfl
-- Module: Mathlib.Topology.Homotopy.Product
Goal:
I : Type u_1
A : Type u_2
X : I → Type u_3
inst : (i : I) → TopologicalSpace (X i)
inst_1 : TopologicalSpace A
f g : (i : I) → ContinuousMap.{u_2, u_3} A (X i)
S : Set A
homotopies : (i : I) → (f i).HomotopyRel (g i) S
t : (↑unitInterval : Type)
x : A
hx : x ∈ S
dsimp :
  Eq (α := (i : I) → X i)
    ((Homotopy.toContinuousMap (f₀ := ContinuousMap.pi (X := X) f) (f₁ := ContinuousMap.pi (X := X) g)
            (Homotopy.pi (Y := X) fun (i : I) ↦
              (homotopies i).toHomotopy (P := fun (f_1 : ContinuousMap.{u_2, u_3} A (X i)) ↦
                ∀ x ∈ S, Eq.{u_3 + 1} (α := X i) ((f_1 : (a : A) → X i) x : X i) ((f i : (a : A) → X i) x : X i))) :
          (a : (↑unitInterval : Type) × A) → (i : I) → X i)
        (t, x) :
      (i : I) → X i)
    fun (i : I) ↦ ((f i : (a : A) → X i) x : X i)
⊢ Eq (α := (i : I) → X i)
    (({
            toFun := fun (x : A) ↦
              ContinuousMap.toFun
                (Homotopy.toContinuousMap (f₀ := ContinuousMap.pi (X := X) f) (f₁ := ContinuousMap.pi (X := X) g)
                  (Homotopy.pi (Y := X) fun (i : I) ↦
                    (homotopies i).toHomotopy (P := fun (f_1 : ContinuousMap.{u_2, u_3} A (X i)) ↦
                      ∀ x ∈ S,
                        Eq.{u_3 + 1} (α := X i) ((f_1 : (a : A) → X i) x : X i) ((f i : (a : A) → X i) x : X i))))
                (t, x),
            continuous_toFun := ⋯ } :
          (a : A) → (i : I) → X i)
        x :
      (i : I) → X i)
    ((ContinuousMap.pi (X := X) f : (a : A) → (i : I) → X i) x : (i : I) → X i)

Tactic:
dsimp only [coe_mk, pi_eval, toFun_eq_coe, HomotopyWith.coe_toContinuousMap]

Premises used: ContinuousMap.HomotopyWith.coe_toContinuousMap, ContinuousMap.coe_mk, ContinuousMap.pi_eval, ContinuousMap.toFun_eq_coe
-- Module: Mathlib.Topology.Homotopy.Product
Goal:
I : Type u_1
A : Type u_2
X : I → Type u_3
inst : (i : I) → TopologicalSpace (X i)
inst_1 : TopologicalSpace A
f g : (i : I) → ContinuousMap.{u_2, u_3} A (X i)
S : Set A
homotopies : (i : I) → (f i).HomotopyRel (g i) S
t : (↑unitInterval : Type)
x : A
hx : x ∈ S
simp :
  ∀ (x_1 : I),
    Eq.{u_3 + 1} (α := X x_1)
      ((Homotopy.toContinuousMap (f₀ := ContinuousMap.pi (X := X) f) (f₁ := ContinuousMap.pi (X := X) g)
              (Homotopy.pi (Y := X) fun (i : I) ↦
                (homotopies i).toHomotopy (P := fun (f_1 : ContinuousMap.{u_2, u_3} A (X i)) ↦
                  ∀ x ∈ S, Eq.{u_3 + 1} (α := X i) ((f_1 : (a : A) → X i) x : X i) ((f i : (a : A) → X i) x : X i))) :
            (a : (↑unitInterval : Type) × A) → (i : I) → X i)
          (t, x) x_1 :
        X x_1)
      ((f x_1 : (a : A) → X x_1) x : X x_1)
⊢ Eq (α := (i : I) → X i)
    ((Homotopy.toContinuousMap (f₀ := ContinuousMap.pi (X := X) f) (f₁ := ContinuousMap.pi (X := X) g)
            (Homotopy.pi (Y := X) fun (i : I) ↦
              (homotopies i).toHomotopy (P := fun (f_1 : ContinuousMap.{u_2, u_3} A (X i)) ↦
                ∀ x ∈ S, Eq.{u_3 + 1} (α := X i) ((f_1 : (a : A) → X i) x : X i) ((f i : (a : A) → X i) x : X i))) :
          (a : (↑unitInterval : Type) × A) → (i : I) → X i)
        (t, x) :
      (i : I) → X i)
    fun (i : I) ↦ ((f i : (a : A) → X i) x : X i)

Tactic:
simp only [funext_iff]

Premises used: funext_iff