[GOAL]
I : Type u_1
A : Type u_2
X : I → Type u_3
inst✝¹ : (i : I) → TopologicalSpace (X i)
inst✝ : TopologicalSpace A
f g : (i : I) → C(A, X i)
S : Set A
homotopies : (i : I) → HomotopyRel (f i) (g i) S
src✝ : Homotopy (ContinuousMap.pi fun i => f i) (ContinuousMap.pi fun i => g i) :=
  Homotopy.pi fun i => (homotopies i).toHomotopy
⊢ ∀ (t : ↑unitInterval) (x : A),
    x ∈ S →
      ↑(mk fun x =>
                ContinuousMap.toFun
                  { toContinuousMap := src✝.toContinuousMap,
                      map_zero_left :=
                        (_ :
                          ∀ (x : A),
                            ContinuousMap.toFun src✝.toContinuousMap (0, x) = ↑(ContinuousMap.pi fun i => f i) x),
                      map_one_left :=
                        (_ :
                          ∀ (x : A),
                            ContinuousMap.toFun src✝.toContinuousMap (1, x) =
                              ↑(ContinuousMap.pi fun i => g i) x) }.toContinuousMap
                  (t, x))
            x =
          ↑(ContinuousMap.pi f) x ∧
        ↑(mk fun x =>
                ContinuousMap.toFun
                  { toContinuousMap := src✝.toContinuousMap,
                      map_zero_left :=
                        (_ :
                          ∀ (x : A),
                            ContinuousMap.toFun src✝.toContinuousMap (0, x) = ↑(ContinuousMap.pi fun i => f i) x),
                      map_one_left :=
                        (_ :
                          ∀ (x : A),
                            ContinuousMap.toFun src✝.toContinuousMap (1, x) =
                              ↑(ContinuousMap.pi fun i => g i) x) }.toContinuousMap
                  (t, x))
            x =
          ↑(ContinuousMap.pi g) x
[PROOFSTEP]
intro t x hx
[GOAL]
I : Type u_1
A : Type u_2
X : I → Type u_3
inst✝¹ : (i : I) → TopologicalSpace (X i)
inst✝ : TopologicalSpace A
f g : (i : I) → C(A, X i)
S : Set A
homotopies : (i : I) → HomotopyRel (f i) (g i) S
src✝ : Homotopy (ContinuousMap.pi fun i => f i) (ContinuousMap.pi fun i => g i) :=
  Homotopy.pi fun i => (homotopies i).toHomotopy
t : ↑unitInterval
x : A
hx : x ∈ S
⊢ ↑(mk fun x =>
            ContinuousMap.toFun
              { toContinuousMap := src✝.toContinuousMap,
                  map_zero_left :=
                    (_ :
                      ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (0, x) = ↑(ContinuousMap.pi fun i => f i) x),
                  map_one_left :=
                    (_ :
                      ∀ (x : A),
                        ContinuousMap.toFun src✝.toContinuousMap (1, x) =
                          ↑(ContinuousMap.pi fun i => g i) x) }.toContinuousMap
              (t, x))
        x =
      ↑(ContinuousMap.pi f) x ∧
    ↑(mk fun x =>
            ContinuousMap.toFun
              { toContinuousMap := src✝.toContinuousMap,
                  map_zero_left :=
                    (_ :
                      ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (0, x) = ↑(ContinuousMap.pi fun i => f i) x),
                  map_one_left :=
                    (_ :
                      ∀ (x : A),
                        ContinuousMap.toFun src✝.toContinuousMap (1, x) =
                          ↑(ContinuousMap.pi fun i => g i) x) }.toContinuousMap
              (t, x))
        x =
      ↑(ContinuousMap.pi g) x
[PROOFSTEP]
dsimp only [coe_mk, pi_eval, toFun_eq_coe, HomotopyWith.coe_toContinuousMap]
[GOAL]
I : Type u_1
A : Type u_2
X : I → Type u_3
inst✝¹ : (i : I) → TopologicalSpace (X i)
inst✝ : TopologicalSpace A
f g : (i : I) → C(A, X i)
S : Set A
homotopies : (i : I) → HomotopyRel (f i) (g i) S
src✝ : Homotopy (ContinuousMap.pi fun i => f i) (ContinuousMap.pi fun i => g i) :=
  Homotopy.pi fun i => (homotopies i).toHomotopy
t : ↑unitInterval
x : A
hx : x ∈ S
⊢ (↑(Homotopy.pi fun i => (homotopies i).toHomotopy).toContinuousMap (t, x) = fun i => ↑(f i) x) ∧
    ↑(Homotopy.pi fun i => (homotopies i).toHomotopy).toContinuousMap (t, x) = fun i => ↑(g i) x
[PROOFSTEP]
simp only [Function.funext_iff, ← forall_and]
[GOAL]
I : Type u_1
A : Type u_2
X : I → Type u_3
inst✝¹ : (i : I) → TopologicalSpace (X i)
inst✝ : TopologicalSpace A
f g : (i : I) → C(A, X i)
S : Set A
homotopies : (i : I) → HomotopyRel (f i) (g i) S
src✝ : Homotopy (ContinuousMap.pi fun i => f i) (ContinuousMap.pi fun i => g i) :=
  Homotopy.pi fun i => (homotopies i).toHomotopy
t : ↑unitInterval
x : A
hx : x ∈ S
⊢ ∀ (x_1 : I),
    ↑(Homotopy.pi fun i => (homotopies i).toHomotopy).toContinuousMap (t, x) x_1 = ↑(f x_1) x ∧
      ↑(Homotopy.pi fun i => (homotopies i).toHomotopy).toContinuousMap (t, x) x_1 = ↑(g x_1) x
[PROOFSTEP]
intro i
[GOAL]
I : Type u_1
A : Type u_2
X : I → Type u_3
inst✝¹ : (i : I) → TopologicalSpace (X i)
inst✝ : TopologicalSpace A
f g : (i : I) → C(A, X i)
S : Set A
homotopies : (i : I) → HomotopyRel (f i) (g i) S
src✝ : Homotopy (ContinuousMap.pi fun i => f i) (ContinuousMap.pi fun i => g i) :=
  Homotopy.pi fun i => (homotopies i).toHomotopy
t : ↑unitInterval
x : A
hx : x ∈ S
i : I
⊢ ↑(Homotopy.pi fun i => (homotopies i).toHomotopy).toContinuousMap (t, x) i = ↑(f i) x ∧
    ↑(Homotopy.pi fun i => (homotopies i).toHomotopy).toContinuousMap (t, x) i = ↑(g i) x
[PROOFSTEP]
exact (homotopies i).prop' t x hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
A : Type u_3
inst✝ : TopologicalSpace A
f₀ f₁ : C(A, α)
g₀ g₁ : C(A, β)
S : Set A
F : Homotopy f₀ f₁
G : Homotopy g₀ g₁
x : A
⊢ ContinuousMap.toFun (ContinuousMap.mk fun t => (↑F t, ↑G t)) (0, x) = ↑(ContinuousMap.prodMk f₀ g₀) x
[PROOFSTEP]
simp only [prod_eval, Homotopy.apply_zero]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
A : Type u_3
inst✝ : TopologicalSpace A
f₀ f₁ : C(A, α)
g₀ g₁ : C(A, β)
S : Set A
F : Homotopy f₀ f₁
G : Homotopy g₀ g₁
x : A
⊢ ContinuousMap.toFun (ContinuousMap.mk fun t => (↑F t, ↑G t)) (1, x) = ↑(ContinuousMap.prodMk f₁ g₁) x
[PROOFSTEP]
simp only [prod_eval, Homotopy.apply_one]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
A : Type u_3
inst✝ : TopologicalSpace A
f₀ f₁ : C(A, α)
g₀ g₁ : C(A, β)
S : Set A
F : HomotopyRel f₀ f₁ S
G : HomotopyRel g₀ g₁ S
src✝ : Homotopy (prodMk f₀ g₀) (prodMk f₁ g₁) := Homotopy.prod F.toHomotopy G.toHomotopy
⊢ ∀ (t : ↑unitInterval) (x : A),
    x ∈ S →
      ↑(mk fun x =>
                ContinuousMap.toFun
                  { toContinuousMap := src✝.toContinuousMap,
                      map_zero_left :=
                        (_ : ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (0, x) = ↑(prodMk f₀ g₀) x),
                      map_one_left :=
                        (_ :
                          ∀ (x : A),
                            ContinuousMap.toFun src✝.toContinuousMap (1, x) = ↑(prodMk f₁ g₁) x) }.toContinuousMap
                  (t, x))
            x =
          ↑(prodMk f₀ g₀) x ∧
        ↑(mk fun x =>
                ContinuousMap.toFun
                  { toContinuousMap := src✝.toContinuousMap,
                      map_zero_left :=
                        (_ : ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (0, x) = ↑(prodMk f₀ g₀) x),
                      map_one_left :=
                        (_ :
                          ∀ (x : A),
                            ContinuousMap.toFun src✝.toContinuousMap (1, x) = ↑(prodMk f₁ g₁) x) }.toContinuousMap
                  (t, x))
            x =
          ↑(prodMk f₁ g₁) x
[PROOFSTEP]
intro t x hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
A : Type u_3
inst✝ : TopologicalSpace A
f₀ f₁ : C(A, α)
g₀ g₁ : C(A, β)
S : Set A
F : HomotopyRel f₀ f₁ S
G : HomotopyRel g₀ g₁ S
src✝ : Homotopy (prodMk f₀ g₀) (prodMk f₁ g₁) := Homotopy.prod F.toHomotopy G.toHomotopy
t : ↑unitInterval
x : A
hx : x ∈ S
⊢ ↑(mk fun x =>
            ContinuousMap.toFun
              { toContinuousMap := src✝.toContinuousMap,
                  map_zero_left := (_ : ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (0, x) = ↑(prodMk f₀ g₀) x),
                  map_one_left :=
                    (_ :
                      ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (1, x) = ↑(prodMk f₁ g₁) x) }.toContinuousMap
              (t, x))
        x =
      ↑(prodMk f₀ g₀) x ∧
    ↑(mk fun x =>
            ContinuousMap.toFun
              { toContinuousMap := src✝.toContinuousMap,
                  map_zero_left := (_ : ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (0, x) = ↑(prodMk f₀ g₀) x),
                  map_one_left :=
                    (_ :
                      ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (1, x) = ↑(prodMk f₁ g₁) x) }.toContinuousMap
              (t, x))
        x =
      ↑(prodMk f₁ g₁) x
[PROOFSTEP]
have hF := F.prop' t x hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
A : Type u_3
inst✝ : TopologicalSpace A
f₀ f₁ : C(A, α)
g₀ g₁ : C(A, β)
S : Set A
F : HomotopyRel f₀ f₁ S
G : HomotopyRel g₀ g₁ S
src✝ : Homotopy (prodMk f₀ g₀) (prodMk f₁ g₁) := Homotopy.prod F.toHomotopy G.toHomotopy
t : ↑unitInterval
x : A
hx : x ∈ S
hF :
  ↑(mk fun x => ContinuousMap.toFun F.toContinuousMap (t, x)) x = ↑f₀ x ∧
    ↑(mk fun x => ContinuousMap.toFun F.toContinuousMap (t, x)) x = ↑f₁ x
⊢ ↑(mk fun x =>
            ContinuousMap.toFun
              { toContinuousMap := src✝.toContinuousMap,
                  map_zero_left := (_ : ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (0, x) = ↑(prodMk f₀ g₀) x),
                  map_one_left :=
                    (_ :
                      ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (1, x) = ↑(prodMk f₁ g₁) x) }.toContinuousMap
              (t, x))
        x =
      ↑(prodMk f₀ g₀) x ∧
    ↑(mk fun x =>
            ContinuousMap.toFun
              { toContinuousMap := src✝.toContinuousMap,
                  map_zero_left := (_ : ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (0, x) = ↑(prodMk f₀ g₀) x),
                  map_one_left :=
                    (_ :
                      ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (1, x) = ↑(prodMk f₁ g₁) x) }.toContinuousMap
              (t, x))
        x =
      ↑(prodMk f₁ g₁) x
[PROOFSTEP]
have hG := G.prop' t x hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
A : Type u_3
inst✝ : TopologicalSpace A
f₀ f₁ : C(A, α)
g₀ g₁ : C(A, β)
S : Set A
F : HomotopyRel f₀ f₁ S
G : HomotopyRel g₀ g₁ S
src✝ : Homotopy (prodMk f₀ g₀) (prodMk f₁ g₁) := Homotopy.prod F.toHomotopy G.toHomotopy
t : ↑unitInterval
x : A
hx : x ∈ S
hF :
  ↑(mk fun x => ContinuousMap.toFun F.toContinuousMap (t, x)) x = ↑f₀ x ∧
    ↑(mk fun x => ContinuousMap.toFun F.toContinuousMap (t, x)) x = ↑f₁ x
hG :
  ↑(mk fun x => ContinuousMap.toFun G.toContinuousMap (t, x)) x = ↑g₀ x ∧
    ↑(mk fun x => ContinuousMap.toFun G.toContinuousMap (t, x)) x = ↑g₁ x
⊢ ↑(mk fun x =>
            ContinuousMap.toFun
              { toContinuousMap := src✝.toContinuousMap,
                  map_zero_left := (_ : ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (0, x) = ↑(prodMk f₀ g₀) x),
                  map_one_left :=
                    (_ :
                      ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (1, x) = ↑(prodMk f₁ g₁) x) }.toContinuousMap
              (t, x))
        x =
      ↑(prodMk f₀ g₀) x ∧
    ↑(mk fun x =>
            ContinuousMap.toFun
              { toContinuousMap := src✝.toContinuousMap,
                  map_zero_left := (_ : ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (0, x) = ↑(prodMk f₀ g₀) x),
                  map_one_left :=
                    (_ :
                      ∀ (x : A), ContinuousMap.toFun src✝.toContinuousMap (1, x) = ↑(prodMk f₁ g₁) x) }.toContinuousMap
              (t, x))
        x =
      ↑(prodMk f₁ g₁) x
[PROOFSTEP]
simp only [coe_mk, prod_eval, Prod.mk.inj_iff, Homotopy.prod] at hF hG ⊢
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
A : Type u_3
inst✝ : TopologicalSpace A
f₀ f₁ : C(A, α)
g₀ g₁ : C(A, β)
S : Set A
F : HomotopyRel f₀ f₁ S
G : HomotopyRel g₀ g₁ S
src✝ : Homotopy (prodMk f₀ g₀) (prodMk f₁ g₁) := Homotopy.prod F.toHomotopy G.toHomotopy
t : ↑unitInterval
x : A
hx : x ∈ S
hF : ContinuousMap.toFun F.toContinuousMap (t, x) = ↑f₀ x ∧ ContinuousMap.toFun F.toContinuousMap (t, x) = ↑f₁ x
hG : ContinuousMap.toFun G.toContinuousMap (t, x) = ↑g₀ x ∧ ContinuousMap.toFun G.toContinuousMap (t, x) = ↑g₁ x
⊢ (↑F.toHomotopy (t, x) = ↑f₀ x ∧ ↑G.toHomotopy (t, x) = ↑g₀ x) ∧
    ↑F.toHomotopy (t, x) = ↑f₁ x ∧ ↑G.toHomotopy (t, x) = ↑g₁ x
[PROOFSTEP]
exact ⟨⟨hF.1, hG.1⟩, ⟨hF.2, hG.2⟩⟩
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
γ : (i : ι) → Path (as i) (bs i)
⊢ (pi fun i => Quotient.mk (Homotopic.setoid (as i) (bs i)) (γ i)) =
    Quotient.mk (Homotopic.setoid (fun i => as i) fun i => bs i) (Path.pi γ)
[PROOFSTEP]
unfold pi
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
γ : (i : ι) → Path (as i) (bs i)
⊢ Quotient.map Path.pi (_ : ∀ (x y : (i : ι) → Path (as i) (bs i)), x ≈ y → Nonempty (Homotopy (Path.pi x) (Path.pi y)))
      (Quotient.choice fun i => Quotient.mk (Homotopic.setoid (as i) (bs i)) (γ i)) =
    Quotient.mk (Homotopic.setoid (fun i => as i) fun i => bs i) (Path.pi γ)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
γ₀ : (i : ι) → Homotopic.Quotient (as i) (bs i)
γ₁ : (i : ι) → Homotopic.Quotient (bs i) (cs i)
⊢ pi γ₀ ⬝ pi γ₁ = pi fun i => γ₀ i ⬝ γ₁ i
[PROOFSTEP]
apply Quotient.induction_on_pi (p := _) γ₁
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
γ₀ : (i : ι) → Homotopic.Quotient (as i) (bs i)
γ₁ : (i : ι) → Homotopic.Quotient (bs i) (cs i)
⊢ ∀ (a : (i : ι) → Path (bs i) (cs i)),
    (pi γ₀ ⬝ pi fun i => Quotient.mk (Homotopic.setoid (bs i) (cs i)) (a i)) =
      pi fun i => γ₀ i ⬝ (fun i => Quotient.mk (Homotopic.setoid (bs i) (cs i)) (a i)) i
[PROOFSTEP]
intro a
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
γ₀ : (i : ι) → Homotopic.Quotient (as i) (bs i)
γ₁ : (i : ι) → Homotopic.Quotient (bs i) (cs i)
a : (i : ι) → Path (bs i) (cs i)
⊢ (pi γ₀ ⬝ pi fun i => Quotient.mk (Homotopic.setoid (bs i) (cs i)) (a i)) =
    pi fun i => γ₀ i ⬝ (fun i => Quotient.mk (Homotopic.setoid (bs i) (cs i)) (a i)) i
[PROOFSTEP]
apply Quotient.induction_on_pi (p := _) γ₀
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
γ₀ : (i : ι) → Homotopic.Quotient (as i) (bs i)
γ₁ : (i : ι) → Homotopic.Quotient (bs i) (cs i)
a : (i : ι) → Path (bs i) (cs i)
⊢ ∀ (a_1 : (i : ι) → Path (as i) (bs i)),
    ((pi fun i => Quotient.mk (Homotopic.setoid (as i) (bs i)) (a_1 i)) ⬝
        pi fun i => Quotient.mk (Homotopic.setoid (bs i) (cs i)) (a i)) =
      pi fun i =>
        (fun i => Quotient.mk (Homotopic.setoid (as i) (bs i)) (a_1 i)) i ⬝
          (fun i => Quotient.mk (Homotopic.setoid (bs i) (cs i)) (a i)) i
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
γ₀ : (i : ι) → Homotopic.Quotient (as i) (bs i)
γ₁ : (i : ι) → Homotopic.Quotient (bs i) (cs i)
a : (i : ι) → Path (bs i) (cs i)
a✝ : (i : ι) → Path (as i) (bs i)
⊢ ((pi fun i => Quotient.mk (Homotopic.setoid (as i) (bs i)) (a✝ i)) ⬝
      pi fun i => Quotient.mk (Homotopic.setoid (bs i) (cs i)) (a i)) =
    pi fun i =>
      (fun i => Quotient.mk (Homotopic.setoid (as i) (bs i)) (a✝ i)) i ⬝
        (fun i => Quotient.mk (Homotopic.setoid (bs i) (cs i)) (a i)) i
[PROOFSTEP]
simp only [pi_lift]
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
γ₀ : (i : ι) → Homotopic.Quotient (as i) (bs i)
γ₁ : (i : ι) → Homotopic.Quotient (bs i) (cs i)
a : (i : ι) → Path (bs i) (cs i)
a✝ : (i : ι) → Path (as i) (bs i)
⊢ Quotient.mk (Homotopic.setoid (fun i => as i) fun i => bs i) (Path.pi fun i => a✝ i) ⬝
      Quotient.mk (Homotopic.setoid (fun i => bs i) fun i => cs i) (Path.pi fun i => a i) =
    pi fun i => Quotient.mk (Homotopic.setoid (as i) (bs i)) (a✝ i) ⬝ Quotient.mk (Homotopic.setoid (bs i) (cs i)) (a i)
[PROOFSTEP]
rw [← Path.Homotopic.comp_lift, Path.trans_pi_eq_pi_trans, ← pi_lift]
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
γ₀ : (i : ι) → Homotopic.Quotient (as i) (bs i)
γ₁ : (i : ι) → Homotopic.Quotient (bs i) (cs i)
a : (i : ι) → Path (bs i) (cs i)
a✝ : (i : ι) → Path (as i) (bs i)
⊢ (pi fun i => Quotient.mk (Homotopic.setoid (as i) (cs i)) (Path.trans (a✝ i) (a i))) =
    pi fun i => Quotient.mk (Homotopic.setoid (as i) (bs i)) (a✝ i) ⬝ Quotient.mk (Homotopic.setoid (bs i) (cs i)) (a i)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
i : ι
paths : (i : ι) → Homotopic.Quotient (as i) (bs i)
⊢ proj i (pi paths) = paths i
[PROOFSTEP]
apply Quotient.induction_on_pi (p := _) paths
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
i : ι
paths : (i : ι) → Homotopic.Quotient (as i) (bs i)
⊢ ∀ (a : (i : ι) → Path (as i) (bs i)),
    proj i (pi fun i => Quotient.mk (Homotopic.setoid (as i) (bs i)) (a i)) =
      (fun i => Quotient.mk (Homotopic.setoid (as i) (bs i)) (a i)) i
[PROOFSTEP]
intro
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
i : ι
paths : (i : ι) → Homotopic.Quotient (as i) (bs i)
a✝ : (i : ι) → Path (as i) (bs i)
⊢ proj i (pi fun i => Quotient.mk (Homotopic.setoid (as i) (bs i)) (a✝ i)) =
    (fun i => Quotient.mk (Homotopic.setoid (as i) (bs i)) (a✝ i)) i
[PROOFSTEP]
unfold proj
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
i : ι
paths : (i : ι) → Homotopic.Quotient (as i) (bs i)
a✝ : (i : ι) → Path (as i) (bs i)
⊢ Quotient.mapFn (pi fun i => Quotient.mk (Homotopic.setoid (as i) (bs i)) (a✝ i)) (ContinuousMap.mk fun p => p i) =
    (fun i => Quotient.mk (Homotopic.setoid (as i) (bs i)) (a✝ i)) i
[PROOFSTEP]
rw [pi_lift, ← Path.Homotopic.map_lift]
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
i : ι
paths : (i : ι) → Homotopic.Quotient (as i) (bs i)
a✝ : (i : ι) → Path (as i) (bs i)
⊢ Quotient.mk
      (Homotopic.setoid (↑(ContinuousMap.mk fun p => p i) fun i => as i)
        (↑(ContinuousMap.mk fun p => p i) fun i => bs i))
      (Path.map (Path.pi fun i => a✝ i) (_ : Continuous ↑(ContinuousMap.mk fun p => p i))) =
    (fun i => Quotient.mk (Homotopic.setoid (as i) (bs i)) (a✝ i)) i
[PROOFSTEP]
congr
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
p : Homotopic.Quotient as bs
⊢ (pi fun i => proj i p) = p
[PROOFSTEP]
apply Quotient.inductionOn (motive := _) p
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
p : Homotopic.Quotient as bs
⊢ ∀ (a : Path as bs),
    (pi fun i => proj i (Quotient.mk (Homotopic.setoid as bs) a)) = Quotient.mk (Homotopic.setoid as bs) a
[PROOFSTEP]
intro
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
p : Homotopic.Quotient as bs
a✝ : Path as bs
⊢ (pi fun i => proj i (Quotient.mk (Homotopic.setoid as bs) a✝)) = Quotient.mk (Homotopic.setoid as bs) a✝
[PROOFSTEP]
unfold proj
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
p : Homotopic.Quotient as bs
a✝ : Path as bs
⊢ (pi fun i => Quotient.mapFn (Quotient.mk (Homotopic.setoid as bs) a✝) (ContinuousMap.mk fun p => p i)) =
    Quotient.mk (Homotopic.setoid as bs) a✝
[PROOFSTEP]
simp_rw [← Path.Homotopic.map_lift]
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
p : Homotopic.Quotient as bs
a✝ : Path as bs
⊢ (pi fun i =>
      Quotient.mk (Homotopic.setoid (↑(ContinuousMap.mk fun p => p i) as) (↑(ContinuousMap.mk fun p => p i) bs))
        (Path.map a✝ (_ : Continuous ↑(ContinuousMap.mk fun p => p i)))) =
    Quotient.mk (Homotopic.setoid as bs) a✝
[PROOFSTEP]
erw [pi_lift]
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
p : Homotopic.Quotient as bs
a✝ : Path as bs
⊢ Quotient.mk (Homotopic.setoid (fun i => as i) fun i => bs i)
      (Path.pi fun i => Path.map a✝ (_ : Continuous ↑(ContinuousMap.mk fun p => p i))) =
    Quotient.mk (Homotopic.setoid as bs) a✝
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁ p₁' : Path a₁ a₂
p₂ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
⊢ prod q₁ q₂ ⬝ prod r₁ r₂ = prod (q₁ ⬝ r₁) (q₂ ⬝ r₂)
[PROOFSTEP]
apply Quotient.inductionOn₂ (motive := _) q₁ q₂
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁ p₁' : Path a₁ a₂
p₂ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
⊢ ∀ (a : Path a₁ a₂) (b : Path b₁ b₂),
    prod (Quotient.mk (Homotopic.setoid a₁ a₂) a) (Quotient.mk (Homotopic.setoid b₁ b₂) b) ⬝ prod r₁ r₂ =
      prod (Quotient.mk (Homotopic.setoid a₁ a₂) a ⬝ r₁) (Quotient.mk (Homotopic.setoid b₁ b₂) b ⬝ r₂)
[PROOFSTEP]
intro a b
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁ p₁' : Path a₁ a₂
p₂ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
a : Path a₁ a₂
b : Path b₁ b₂
⊢ prod (Quotient.mk (Homotopic.setoid a₁ a₂) a) (Quotient.mk (Homotopic.setoid b₁ b₂) b) ⬝ prod r₁ r₂ =
    prod (Quotient.mk (Homotopic.setoid a₁ a₂) a ⬝ r₁) (Quotient.mk (Homotopic.setoid b₁ b₂) b ⬝ r₂)
[PROOFSTEP]
apply Quotient.inductionOn₂ (motive := _) r₁ r₂
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁ p₁' : Path a₁ a₂
p₂ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
a : Path a₁ a₂
b : Path b₁ b₂
⊢ ∀ (a_1 : Path a₂ a₃) (b_1 : Path b₂ b₃),
    prod (Quotient.mk (Homotopic.setoid a₁ a₂) a) (Quotient.mk (Homotopic.setoid b₁ b₂) b) ⬝
        prod (Quotient.mk (Homotopic.setoid a₂ a₃) a_1) (Quotient.mk (Homotopic.setoid b₂ b₃) b_1) =
      prod (Quotient.mk (Homotopic.setoid a₁ a₂) a ⬝ Quotient.mk (Homotopic.setoid a₂ a₃) a_1)
        (Quotient.mk (Homotopic.setoid b₁ b₂) b ⬝ Quotient.mk (Homotopic.setoid b₂ b₃) b_1)
[PROOFSTEP]
intros
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁ p₁' : Path a₁ a₂
p₂ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
a : Path a₁ a₂
b : Path b₁ b₂
a✝ : Path a₂ a₃
b✝ : Path b₂ b₃
⊢ prod (Quotient.mk (Homotopic.setoid a₁ a₂) a) (Quotient.mk (Homotopic.setoid b₁ b₂) b) ⬝
      prod (Quotient.mk (Homotopic.setoid a₂ a₃) a✝) (Quotient.mk (Homotopic.setoid b₂ b₃) b✝) =
    prod (Quotient.mk (Homotopic.setoid a₁ a₂) a ⬝ Quotient.mk (Homotopic.setoid a₂ a₃) a✝)
      (Quotient.mk (Homotopic.setoid b₁ b₂) b ⬝ Quotient.mk (Homotopic.setoid b₂ b₃) b✝)
[PROOFSTEP]
simp only [prod_lift, ← Path.Homotopic.comp_lift, Path.trans_prod_eq_prod_trans]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁ p₁' : Path a₁ a₂
p₂ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
⊢ projLeft (prod q₁ q₂) = q₁
[PROOFSTEP]
apply Quotient.inductionOn₂ (motive := _) q₁ q₂
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁ p₁' : Path a₁ a₂
p₂ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
⊢ ∀ (a : Path a₁ a₂) (b : Path b₁ b₂),
    projLeft (prod (Quotient.mk (Homotopic.setoid a₁ a₂) a) (Quotient.mk (Homotopic.setoid b₁ b₂) b)) =
      Quotient.mk (Homotopic.setoid a₁ a₂) a
[PROOFSTEP]
intro p₁ p₂
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁✝ p₁' : Path a₁ a₂
p₂✝ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
p₁ : Path a₁ a₂
p₂ : Path b₁ b₂
⊢ projLeft (prod (Quotient.mk (Homotopic.setoid a₁ a₂) p₁) (Quotient.mk (Homotopic.setoid b₁ b₂) p₂)) =
    Quotient.mk (Homotopic.setoid a₁ a₂) p₁
[PROOFSTEP]
unfold projLeft
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁✝ p₁' : Path a₁ a₂
p₂✝ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
p₁ : Path a₁ a₂
p₂ : Path b₁ b₂
⊢ Quotient.mapFn (prod (Quotient.mk (Homotopic.setoid a₁ a₂) p₁) (Quotient.mk (Homotopic.setoid b₁ b₂) p₂))
      (ContinuousMap.mk Prod.fst) =
    Quotient.mk (Homotopic.setoid a₁ a₂) p₁
[PROOFSTEP]
rw [prod_lift, ← Path.Homotopic.map_lift]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁✝ p₁' : Path a₁ a₂
p₂✝ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
p₁ : Path a₁ a₂
p₂ : Path b₁ b₂
⊢ Quotient.mk (Homotopic.setoid (↑(ContinuousMap.mk Prod.fst) (a₁, b₁)) (↑(ContinuousMap.mk Prod.fst) (a₂, b₂)))
      (Path.map (Path.prod p₁ p₂) (_ : Continuous ↑(ContinuousMap.mk Prod.fst))) =
    Quotient.mk (Homotopic.setoid a₁ a₂) p₁
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁ p₁' : Path a₁ a₂
p₂ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
⊢ projRight (prod q₁ q₂) = q₂
[PROOFSTEP]
apply Quotient.inductionOn₂ (motive := _) q₁ q₂
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁ p₁' : Path a₁ a₂
p₂ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
⊢ ∀ (a : Path a₁ a₂) (b : Path b₁ b₂),
    projRight (prod (Quotient.mk (Homotopic.setoid a₁ a₂) a) (Quotient.mk (Homotopic.setoid b₁ b₂) b)) =
      Quotient.mk (Homotopic.setoid b₁ b₂) b
[PROOFSTEP]
intro p₁ p₂
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁✝ p₁' : Path a₁ a₂
p₂✝ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
p₁ : Path a₁ a₂
p₂ : Path b₁ b₂
⊢ projRight (prod (Quotient.mk (Homotopic.setoid a₁ a₂) p₁) (Quotient.mk (Homotopic.setoid b₁ b₂) p₂)) =
    Quotient.mk (Homotopic.setoid b₁ b₂) p₂
[PROOFSTEP]
unfold projRight
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁✝ p₁' : Path a₁ a₂
p₂✝ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
p₁ : Path a₁ a₂
p₂ : Path b₁ b₂
⊢ Quotient.mapFn (prod (Quotient.mk (Homotopic.setoid a₁ a₂) p₁) (Quotient.mk (Homotopic.setoid b₁ b₂) p₂))
      (ContinuousMap.mk Prod.snd) =
    Quotient.mk (Homotopic.setoid b₁ b₂) p₂
[PROOFSTEP]
rw [prod_lift, ← Path.Homotopic.map_lift]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁✝ p₁' : Path a₁ a₂
p₂✝ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
p₁ : Path a₁ a₂
p₂ : Path b₁ b₂
⊢ Quotient.mk (Homotopic.setoid (↑(ContinuousMap.mk Prod.snd) (a₁, b₁)) (↑(ContinuousMap.mk Prod.snd) (a₂, b₂)))
      (Path.map (Path.prod p₁ p₂) (_ : Continuous ↑(ContinuousMap.mk Prod.snd))) =
    Quotient.mk (Homotopic.setoid b₁ b₂) p₂
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁ p₁' : Path a₁ a₂
p₂ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
p : Homotopic.Quotient (a₁, b₁) (a₂, b₂)
⊢ prod (projLeft p) (projRight p) = p
[PROOFSTEP]
apply Quotient.inductionOn (motive := _) p
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁ p₁' : Path a₁ a₂
p₂ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
p : Homotopic.Quotient (a₁, b₁) (a₂, b₂)
⊢ ∀ (a : Path (a₁, b₁) (a₂, b₂)),
    prod (projLeft (Quotient.mk (Homotopic.setoid (a₁, b₁) (a₂, b₂)) a))
        (projRight (Quotient.mk (Homotopic.setoid (a₁, b₁) (a₂, b₂)) a)) =
      Quotient.mk (Homotopic.setoid (a₁, b₁) (a₂, b₂)) a
[PROOFSTEP]
intro p'
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁ p₁' : Path a₁ a₂
p₂ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
p : Homotopic.Quotient (a₁, b₁) (a₂, b₂)
p' : Path (a₁, b₁) (a₂, b₂)
⊢ prod (projLeft (Quotient.mk (Homotopic.setoid (a₁, b₁) (a₂, b₂)) p'))
      (projRight (Quotient.mk (Homotopic.setoid (a₁, b₁) (a₂, b₂)) p')) =
    Quotient.mk (Homotopic.setoid (a₁, b₁) (a₂, b₂)) p'
[PROOFSTEP]
unfold projLeft
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁ p₁' : Path a₁ a₂
p₂ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
p : Homotopic.Quotient (a₁, b₁) (a₂, b₂)
p' : Path (a₁, b₁) (a₂, b₂)
⊢ prod (Quotient.mapFn (Quotient.mk (Homotopic.setoid (a₁, b₁) (a₂, b₂)) p') (ContinuousMap.mk Prod.fst))
      (projRight (Quotient.mk (Homotopic.setoid (a₁, b₁) (a₂, b₂)) p')) =
    Quotient.mk (Homotopic.setoid (a₁, b₁) (a₂, b₂)) p'
[PROOFSTEP]
unfold projRight
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁ p₁' : Path a₁ a₂
p₂ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
p : Homotopic.Quotient (a₁, b₁) (a₂, b₂)
p' : Path (a₁, b₁) (a₂, b₂)
⊢ prod (Quotient.mapFn (Quotient.mk (Homotopic.setoid (a₁, b₁) (a₂, b₂)) p') (ContinuousMap.mk Prod.fst))
      (Quotient.mapFn (Quotient.mk (Homotopic.setoid (a₁, b₁) (a₂, b₂)) p') (ContinuousMap.mk Prod.snd)) =
    Quotient.mk (Homotopic.setoid (a₁, b₁) (a₂, b₂)) p'
[PROOFSTEP]
simp only [← Path.Homotopic.map_lift, prod_lift]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
p₁ p₁' : Path a₁ a₂
p₂ p₂' : Path b₁ b₂
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
c₁ c₂ : α × β
p : Homotopic.Quotient (a₁, b₁) (a₂, b₂)
p' : Path (a₁, b₁) (a₂, b₂)
⊢ prod
      (Quotient.mk (Homotopic.setoid (↑(ContinuousMap.mk Prod.fst) (a₁, b₁)) (↑(ContinuousMap.mk Prod.fst) (a₂, b₂)))
        (Path.map p' (_ : Continuous ↑(ContinuousMap.mk Prod.fst))))
      (Quotient.mk (Homotopic.setoid (↑(ContinuousMap.mk Prod.snd) (a₁, b₁)) (↑(ContinuousMap.mk Prod.snd) (a₂, b₂)))
        (Path.map p' (_ : Continuous ↑(ContinuousMap.mk Prod.snd)))) =
    Quotient.mk (Homotopic.setoid (a₁, b₁) (a₂, b₂)) p'
[PROOFSTEP]
congr
