X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₃ : X
p₁ : Path x₀ x₁
p₂ : Path x₀ x₃
hp : ∀ (t : ↑I), ↑p₁ t = ↑p₂ t
⊢ HEq (Quotient.mk (Homotopic.setoid x₀ x₁) p₁) (Quotient.mk (Homotopic.setoid x₀ x₃) p₂)
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₁ : Path x₀ x₁
p₂ : Path x₂ x₃
hp : ∀ (t : ↑I), ↑p₁ t = ↑p₂ t
⊢ HEq (Quotient.mk (Homotopic.setoid x₀ x₁) p₁) (Quotient.mk (Homotopic.setoid x₂ x₃) p₂)
obtain rfl : x₀ = x₂ := by convert hp 0 <;> simp
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p₁ p₂ : Path x₀ x₁
hp : ∀ (t : ↑I), ↑p₁ t = ↑p₂ t
⊢ HEq (Quotient.mk (Homotopic.setoid x₀ x₁) p₁) (Quotient.mk (Homotopic.setoid x₀ x₁) p₂)
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₃ : X
p₁ : Path x₀ x₁
p₂ : Path x₀ x₃
hp : ∀ (t : ↑I), ↑p₁ t = ↑p₂ t
⊢ HEq (Quotient.mk (Homotopic.setoid x₀ x₁) p₁) (Quotient.mk (Homotopic.setoid x₀ x₃) p₂)
obtain rfl : x₁ = x₃ := by convert hp 1 <;> simp
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p₁ p₂ : Path x₀ x₁
hp : ∀ (t : ↑I), ↑p₁ t = ↑p₂ t
⊢ Quotient.mk (Homotopic.setoid x₀ x₁) p₁ = Quotient.mk (Homotopic.setoid x₀ x₁) p₂
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p₁ p₂ : Path x₀ x₁
hp : ∀ (t : ↑I), ↑p₁ t = ↑p₂ t
⊢ HEq (Quotient.mk (Homotopic.setoid x₀ x₁) p₁) (Quotient.mk (Homotopic.setoid x₀ x₁) p₂)
rw [heq_iff_eq]
case e_a
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p₁ p₂ : Path x₀ x₁
hp : ∀ (t : ↑I), ↑p₁ t = ↑p₂ t
⊢ p₁ = p₂
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p₁ p₂ : Path x₀ x₁
hp : ∀ (t : ↑I), ↑p₁ t = ↑p₂ t
⊢ Quotient.mk (Homotopic.setoid x₀ x₁) p₁ = Quotient.mk (Homotopic.setoid x₀ x₁) p₂
congr
case e_a.a.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p₁ p₂ : Path x₀ x₁
hp : ∀ (t : ↑I), ↑p₁ t = ↑p₂ t
t : ↑I
⊢ ↑p₁ t = ↑p₂ t
case e_a
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p₁ p₂ : Path x₀ x₁
hp : ∀ (t : ↑I), ↑p₁ t = ↑p₂ t
⊢ p₁ = p₂
ext t
no goals
case e_a.a.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p₁ p₂ : Path x₀ x₁
hp : ∀ (t : ↑I), ↑p₁ t = ↑p₂ t
t : ↑I
⊢ ↑p₁ t = ↑p₂ t
exact hp t
no goals
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₁ : Path x₀ x₁
p₂ : Path x₂ x₃
hp : ∀ (t : ↑I), ↑p₁ t = ↑p₂ t
⊢ x₀ = x₂
convert hp 0 <;> simp
no goals
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₃ : X
p₁ : Path x₀ x₁
p₂ : Path x₀ x₃
hp : ∀ (t : ↑I), ↑p₁ t = ↑p₂ t
⊢ x₁ = x₃
convert hp 1 <;> simp