awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
i : I
⊢ Eq.{u_3 + 1} (α := 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 :
      X i)
    ((f i : (a : A) → X i) x : X i)

Tactic:
(homotopies i).prop' t x hx

Premises used: ContinuousMap.HomotopyWith.prop'
-- 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
i : I
⊢ Eq.{u_3 + 1} (α := 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 :
      X i)
    ((f i : (a : A) → X i) x : X i)

Tactic:
exact (homotopies i).prop' t x hx

Premises used: ContinuousMap.HomotopyWith.prop'
-- Module: Mathlib.Topology.Homotopy.Product
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
A : Type u_3
inst_2 : TopologicalSpace A
f₀ f₁ : C(A, α)
g₀ g₁ : C(A, β)
S : Set A
F : f₀.Homotopy f₁
G : g₀.Homotopy g₁
x : A
⊢ Eq (α := α × β)
    (((F : (a : (↑unitInterval : Type) × A) → α) (0, x), (G : (a : (↑unitInterval : Type) × A) → β) (0, x)) : α × β)
    ((f₀.prodMk g₀ : (a : A) → α × β) x : α × β)

Tactic:
simp only [prod_eval, Homotopy.apply_zero]

Premises used: ContinuousMap.Homotopy.apply_zero, ContinuousMap.prod_eval
-- Module: Mathlib.Topology.Homotopy.Product
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
A : Type u_3
inst_2 : TopologicalSpace A
f₀ f₁ : C(A, α)
g₀ g₁ : C(A, β)
S : Set A
F : f₀.Homotopy f₁
G : g₀.Homotopy g₁
x : A
⊢ Eq (α := α × β)
    (((F : (a : (↑unitInterval : Type) × A) → α) (1, x), (G : (a : (↑unitInterval : Type) × A) → β) (1, x)) : α × β)
    ((f₁.prodMk g₁ : (a : A) → α × β) x : α × β)

Tactic:
simp only [prod_eval, Homotopy.apply_one]

Premises used: ContinuousMap.Homotopy.apply_one, ContinuousMap.prod_eval
-- Module: Mathlib.Topology.Homotopy.Product
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
γ : (i : ι) → Path (as i) (bs i)
simp_rw : (pi (X := X) fun (i : ι) ↦ Quotient.mk' (γ i)) = Quotient.mk' (Path.pi (χ := X) γ)
simp_rw₁ : (pi (X := X) fun (i : ι) ↦ ⟦γ i⟧) = ⟦Path.pi (χ := X) γ⟧
simp_rw₂ :
  Eq (α := Homotopic.Quotient as bs)
    (_root_.Quotient.map (Path.pi (χ := X)) ⋯
      (Quotient.choice (α := fun (i : ι) ↦ Path (as i) (bs i)) fun (i : ι) ↦ ⟦γ i⟧))
    ⟦Path.pi (χ := X) γ⟧
simp_rw₃ : Eq (α := Homotopic.Quotient as bs) (_root_.Quotient.map (Path.pi (χ := X)) ⋯ ⟦γ⟧) ⟦Path.pi (χ := X) γ⟧
⊢ (pi (X := X) fun (i : ι) ↦ Quotient.mk (γ i)) = Quotient.mk (Path.pi (χ := X) γ)

Tactic:
simp_rw [← Quotient.mk'_eq_mk, Quotient.mk', pi, Quotient.choice_eq, Quotient.map_mk]

Premises used: Path.Homotopic.Quotient.mk'_eq_mk, Quotient.map_mk, Path.Homotopic.pi, Quotient.mk', Quotient.choice_eq
-- Module: Mathlib.Topology.Homotopy.Product
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)
a : (i : ι) → Path (bs i) (cs i)
h :
  ∀ (a_1 : (i : ι) → Path (as i) (bs i)),
    Eq (α := Homotopic.Quotient as cs)
      (Quotient.trans (x₁ := bs) (pi (X := X) fun (i : ι) ↦ ⟦a_1 i⟧) (pi (X := X) fun (i : ι) ↦ ⟦a i⟧))
      (pi (X := X) fun (i : ι) ↦
        Quotient.trans (x₁ := bs i)
          ((fun (i : ι) ↦ (⟦a_1 i⟧ : Quotient (α := Path (as i) (bs i)) (Homotopic.setoid (as i) (bs i)))) i)
          ((fun (i : ι) ↦ (⟦a i⟧ : Quotient (α := Path (bs i) (cs i)) (Homotopic.setoid (bs i) (cs i)))) i))
⊢ Eq (α := Homotopic.Quotient as cs) (pi (X := X) γ₀ ⬝ pi (X := X) fun (i : ι) ↦ ⟦a i⟧)
    (pi (X := X) fun (i : ι) ↦
      γ₀ i ⬝ (fun (i : ι) ↦ (⟦a i⟧ : Quotient (α := Path (bs i) (cs i)) (Homotopic.setoid (bs i) (cs i)))) i)

Tactic:
induction γ₀ using Quotient.induction_on_pi
-- Module: Mathlib.Topology.Homotopy.Product
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
a : (i : ι) → Path (bs i) (cs i)
a_1 : (i : ι) → Path (as i) (bs i)
h :
  Quotient.mk (Path.pi (χ := X) a_1) ⬝ Quotient.mk (Path.pi (χ := X) a) =
    pi (X := X) fun (i : ι) ↦ Quotient.mk (a_1 i) ⬝ Quotient.mk (a i)
⊢ Eq (α := Homotopic.Quotient as cs)
    (Quotient.trans (x₁ := bs) (pi (X := X) fun (i : ι) ↦ ⟦a_1 i⟧) (pi (X := X) fun (i : ι) ↦ ⟦a i⟧))
    (pi (X := X) fun (i : ι) ↦
      Quotient.trans (x₁ := bs i)
        ((fun (i : ι) ↦ (⟦a_1 i⟧ : Quotient (α := Path (as i) (bs i)) (Homotopic.setoid (as i) (bs i)))) i)
        ((fun (i : ι) ↦ (⟦a i⟧ : Quotient (α := Path (bs i) (cs i)) (Homotopic.setoid (bs i) (cs i)))) i))

Tactic:
simp only [Quotient.mk''_eq_mk, pi_lift]

Premises used: Path.Homotopic.pi_lift, Path.Homotopic.Quotient.mk''_eq_mk
-- Module: Mathlib.Topology.Homotopy.Product
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
a : (i : ι) → Path (bs i) (cs i)
a_1 : (i : ι) → Path (as i) (bs i)
h :
  Eq (α := Homotopic.Quotient as cs) (pi (X := X) fun (i : ι) ↦ Quotient.mk ((a_1 i).trans (a i)))
    (pi (X := X) fun (i : ι) ↦ Quotient.mk (a_1 i) ⬝ Quotient.mk (a i))
⊢ Quotient.mk (Path.pi (χ := X) a_1) ⬝ Quotient.mk (Path.pi (χ := X) a) =
    pi (X := X) fun (i : ι) ↦ Quotient.mk (a_1 i) ⬝ Quotient.mk (a i)

Tactic:
rw [← Path.Homotopic.Quotient.mk_trans, Path.trans_pi_eq_pi_trans, ← pi_lift]

Premises used: Path.trans_pi_eq_pi_trans, Path.Homotopic.pi_lift, Path.Homotopic.Quotient.mk_trans
-- Module: Mathlib.Topology.Homotopy.Product
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
a : (i : ι) → Path (bs i) (cs i)
a_1 : (i : ι) → Path (as i) (bs i)
⊢ Eq (α := Homotopic.Quotient as cs) (pi (X := X) fun (i : ι) ↦ Quotient.mk ((a_1 i).trans (a i)))
    (pi (X := X) fun (i : ι) ↦ Quotient.mk (a_1 i) ⬝ Quotient.mk (a i))

Tactic:
rfl
-- Module: Mathlib.Topology.Homotopy.Product
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)
h :
  ∀ (a : (i : ι) → Path (bs i) (cs i)),
    Eq (α := Homotopic.Quotient as cs) (pi (X := X) γ₀ ⬝ pi (X := X) fun (i : ι) ↦ ⟦a i⟧)
      (pi (X := X) fun (i : ι) ↦
        γ₀ i ⬝ (fun (i : ι) ↦ (⟦a i⟧ : Quotient (α := Path (bs i) (cs i)) (Homotopic.setoid (bs i) (cs i)))) i)
⊢ pi (X := X) γ₀ ⬝ pi (X := X) γ₁ = pi (X := X) fun (i : ι) ↦ γ₀ i ⬝ γ₁ i

Tactic:
induction γ₁ using Quotient.induction_on_pi with | _ a =>
  induction γ₀ using Quotient.induction_on_pi
  simp only [Quotient.mk''_eq_mk, pi_lift]
  rw [← Path.Homotopic.Quotient.mk_trans, Path.trans_pi_eq_pi_trans, ← pi_lift]
  rfl

Premises used: Path.trans_pi_eq_pi_trans, Path.Homotopic.pi_lift, Path.Homotopic.Quotient.mk_trans, Path.Homotopic.Quotient.mk''_eq_mk
-- Module: Mathlib.Topology.Homotopy.Product
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
i : ι
paths : (i : ι) → Homotopic.Quotient (as i) (bs i)
h :
  ∀ (a : (i : ι) → Path (as i) (bs i)),
    Eq.{u_2 + 1} (α := Homotopic.Quotient (as i) (bs i)) (proj (X := X) i (pi (X := X) fun (i : ι) ↦ ⟦a i⟧))
      ((fun (i : ι) ↦ (⟦a i⟧ : Quotient (α := Path (as i) (bs i)) (Homotopic.setoid (as i) (bs i)))) i)
⊢ proj (X := X) i (pi (X := X) paths) = paths i

Tactic:
induction paths using Quotient.induction_on_pi
-- Module: Mathlib.Topology.Homotopy.Product
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
i : ι
a : (i : ι) → Path (as i) (bs i)
h :
  (Quotient.mk (Path.pi (χ := X) a)).map
      { toFun := fun (p : (i : ι) → X i) ↦ p i, continuous_toFun := ⋯ : C((i : ι) → X i, X i) } =
    Quotient.mk (a i)
⊢ proj (X := X) i (pi (X := X) fun (i : ι) ↦ Quotient.mk (a i)) = Quotient.mk (a i)

Tactic:
rw [proj, pi_lift]

Premises used: Path.Homotopic.pi_lift, Path.Homotopic.proj
-- Module: Mathlib.Topology.Homotopy.Product
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
i : ι
a : (i : ι) → Path (as i) (bs i)
⊢ (Quotient.mk (Path.pi (χ := X) a)).map
      { toFun := fun (p : (i : ι) → X i) ↦ p i, continuous_toFun := ⋯ : C((i : ι) → X i, X i) } =
    Quotient.mk (a i)

Tactic:
congr
-- Module: Mathlib.Topology.Homotopy.Product
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
p : Homotopic.Quotient as bs
h : ∀ (a : Path as bs), (pi (X := fun (i : ι) ↦ X i) fun (i : ι) ↦ proj (X := X) i ⟦a⟧) = ⟦a⟧
⊢ (pi (X := fun (i : ι) ↦ X i) fun (i : ι) ↦ proj (X := X) i p) = p

Tactic:
induction p using Quotient.inductionOn
-- Module: Mathlib.Topology.Homotopy.Product
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
a : Path as bs
h : Quotient.mk (Path.pi (χ := fun (i : ι) ↦ X i) fun (i : ι) ↦ a.map ⋯) = Quotient.mk a
⊢ (pi (X := fun (i : ι) ↦ X i) fun (i : ι) ↦ proj (X := X) i ⟦a⟧) = ⟦a⟧

Tactic:
simp only [Quotient.mk''_eq_mk, ← Path.Homotopic.Quotient.mk_map, pi_lift]

Premises used: Path.Homotopic.pi_lift, Path.Homotopic.Quotient.mk_map, Path.Homotopic.Quotient.mk''_eq_mk
-- Module: Mathlib.Topology.Homotopy.Product
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
a : Path as bs
⊢ Quotient.mk (Path.pi (χ := fun (i : ι) ↦ X i) fun (i : ι) ↦ a.map ⋯) = Quotient.mk a

Tactic:
congr
-- Module: Mathlib.Topology.Homotopy.Product
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
p₁ : Path a₁ a₂
p₂ : Path b₁ b₂
⊢ prod (Quotient.mk p₁) (Quotient.mk p₂) = Quotient.mk (p₁.prod p₂)

Tactic:
rfl

Premises used: Path.Homotopic.prod, Quotient.mk', rfl, Path.Homotopic.Quotient.mk
-- Module: Mathlib.Topology.Homotopy.Product
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
mk :
  ∀ (a : Path a₁ a₂) (b : Path b₁ b₂),
    prod (Quotient.mk a) (Quotient.mk b) ⬝ prod r₁ r₂ = prod (Quotient.mk a ⬝ r₁) (Quotient.mk b ⬝ r₂)
⊢ prod q₁ q₂ ⬝ prod r₁ r₂ = prod (q₁ ⬝ r₁) (q₂ ⬝ r₂)

Tactic:
induction q₁, q₂ using Path.Homotopic.Quotient.ind₂
-- Module: Mathlib.Topology.Homotopy.Product
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ 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₂
mk :
  ∀ (a_1 : Path a₂ a₃) (b_1 : Path b₂ b₃),
    prod (Quotient.mk a) (Quotient.mk b) ⬝ prod (Quotient.mk a_1) (Quotient.mk b_1) =
      prod (Quotient.mk a ⬝ Quotient.mk a_1) (Quotient.mk b ⬝ Quotient.mk b_1)
⊢ prod (Quotient.mk a) (Quotient.mk b) ⬝ prod r₁ r₂ = prod (Quotient.mk a ⬝ r₁) (Quotient.mk b ⬝ r₂)

Tactic:
induction r₁, r₂ using Path.Homotopic.Quotient.ind₂
-- Module: Mathlib.Topology.Homotopy.Product
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ 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 a) (Quotient.mk b) ⬝ prod (Quotient.mk a_1) (Quotient.mk b_1) =
    prod (Quotient.mk a ⬝ Quotient.mk a_1) (Quotient.mk b ⬝ Quotient.mk b_1)

Tactic:
simp only [prod_lift, ← Path.Homotopic.Quotient.mk_trans, Path.trans_prod_eq_prod_trans]

Premises used: Path.trans_prod_eq_prod_trans, Path.Homotopic.Quotient.mk_trans, Path.Homotopic.prod_lift
-- Module: Mathlib.Topology.Homotopy.Product
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
mk : ∀ (a : Path a₁ a₂) (b : Path b₁ b₂), projLeft (prod (Quotient.mk a) (Quotient.mk b)) = Quotient.mk a
⊢ projLeft (prod q₁ q₂) = q₁

Tactic:
induction q₁, q₂ using Path.Homotopic.Quotient.ind₂
-- Module: Mathlib.Topology.Homotopy.Product
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
a : Path a₁ a₂
b : Path b₁ b₂
⊢ Quotient.mk ((a.prod b).map ⋯) = Quotient.mk a

Tactic:
congr
-- Module: Mathlib.Topology.Homotopy.Product
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
mk : ∀ (a : Path a₁ a₂) (b : Path b₁ b₂), projRight (prod (Quotient.mk a) (Quotient.mk b)) = Quotient.mk b
⊢ projRight (prod q₁ q₂) = q₂

Tactic:
induction q₁, q₂ using Path.Homotopic.Quotient.ind₂
-- Module: Mathlib.Topology.Homotopy.Product
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
a : Path a₁ a₂
b : Path b₁ b₂
⊢ Quotient.mk ((a.prod b).map ⋯) = Quotient.mk b

Tactic:
congr
-- Module: Mathlib.Topology.Homotopy.Product
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
p : Homotopic.Quotient (a₁, b₁) (a₂, b₂)
mk : ∀ (a : Path (a₁, b₁) (a₂, b₂)), prod (projLeft (Quotient.mk a)) (projRight (Quotient.mk a)) = Quotient.mk a
⊢ prod (projLeft p) (projRight p) = p

Tactic:
induction p using Path.Homotopic.Quotient.ind

Premises used: Path.Homotopic.Quotient.ind
-- Module: Mathlib.Topology.Homotopy.Product
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
a : Path (a₁, b₁) (a₂, b₂)
mk : prod (Quotient.mk (a.map ⋯)) (Quotient.mk (a.map ⋯)) = Quotient.mk a
⊢ prod (projLeft (Quotient.mk a)) (projRight (Quotient.mk a)) = Quotient.mk a

Tactic:
simp only [projLeft, projRight, ← Path.Homotopic.Quotient.mk_map]

Premises used: Path.Homotopic.projLeft, Path.Homotopic.Quotient.mk_map, Path.Homotopic.projRight
-- Module: Mathlib.Topology.Homotopy.Product
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
a : Path (a₁, b₁) (a₂, b₂)
⊢ prod (Quotient.mk (a.map ⋯)) (Quotient.mk (a.map ⋯)) = Quotient.mk a

Tactic:
congr
-- Module: Mathlib.Topology.Homotopy.TopCat.Basic
Goal:
X Y : TopCat
f₀ f₁ : X ⟶ Y
F : Homotopy f₀ f₁
p : (↑(tensorObj (𝒞 := instCategory) X I) : Type u)
⊢ Eq (α := (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) F.h :
          (a : (↑(X ⊗ I) : Type u)) → (↑Y : Type u))
        p :
      (↑Y : Type u))
    ((F : (a : (↑unitInterval : Type) × (↑X : Type u)) → (↑Y : Type u))
        (((I.homeomorph : (a : (↑I : Type u)) → (↑unitInterval : Type)) p.2, p.1) :
          (↑unitInterval : Type) × (↑X : Type u)) :
      (↑Y : Type u))

Tactic:
rfl

Premises used: Prod.map, rfl
-- Module: Mathlib.Topology.Homotopy.TopCat.Basic
Goal:
X Y : TopCat
f₀ f₁ : X ⟶ Y
F : Homotopy f₀ f₁
w :
  ∀ (x : (↑X : Type u)),
    Eq (α := (↑Y : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (ι₀ ≫ F.h) :
            (a : (↑X : Type u)) → (↑Y : Type u))
          x :
        (↑Y : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f₀ :
            (a : (↑X : Type u)) → (↑Y : Type u))
          x :
        (↑Y : Type u))
⊢ ι₀ ≫ F.h = f₀

Tactic:
ext x
-- Module: Mathlib.Topology.Homotopy.TopCat.Basic
Goal:
X Y : TopCat
f₀ f₁ : X ⟶ Y
F : Homotopy f₀ f₁
x : (↑X : Type u)
⊢ Eq (α := (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (ι₀ ≫ F.h) :
          (a : (↑X : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f₀ :
          (a : (↑X : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))

Tactic:
F.map_zero_left x

Premises used: Prod.map, ContinuousMap.Homotopy.map_zero_left
-- Module: Mathlib.Topology.Homotopy.TopCat.Basic
Goal:
X Y : TopCat
f₀ f₁ : X ⟶ Y
F : Homotopy f₀ f₁
x : (↑X : Type u)
⊢ Eq (α := (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (ι₀ ≫ F.h) :
          (a : (↑X : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f₀ :
          (a : (↑X : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))

Tactic:
exact F.map_zero_left x

Premises used: ContinuousMap.Homotopy.map_zero_left
-- Module: Mathlib.Topology.Homotopy.TopCat.Basic
Goal:
X Y : TopCat
f₀ f₁ : X ⟶ Y
F : Homotopy f₀ f₁
w :
  ∀ (x : (↑X : Type u)),
    Eq (α := (↑Y : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (ι₁ ≫ F.h) :
            (a : (↑X : Type u)) → (↑Y : Type u))
          x :
        (↑Y : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f₁ :
            (a : (↑X : Type u)) → (↑Y : Type u))
          x :
        (↑Y : Type u))
⊢ ι₁ ≫ F.h = f₁

Tactic:
ext x
-- Module: Mathlib.Topology.Homotopy.TopCat.Basic
Goal:
X Y : TopCat
f₀ f₁ : X ⟶ Y
F : Homotopy f₀ f₁
x : (↑X : Type u)
⊢ Eq (α := (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (ι₁ ≫ F.h) :
          (a : (↑X : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f₁ :
          (a : (↑X : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))

Tactic:
F.map_one_left x

Premises used: Prod.map, ContinuousMap.Homotopy.map_one_left
-- Module: Mathlib.Topology.Homotopy.TopCat.Basic
Goal:
X Y : TopCat
f₀ f₁ : X ⟶ Y
F : Homotopy f₀ f₁
x : (↑X : Type u)
⊢ Eq (α := (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (ι₁ ≫ F.h) :
          (a : (↑X : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f₁ :
          (a : (↑X : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))

Tactic:
exact F.map_one_left x

Premises used: ContinuousMap.Homotopy.map_one_left
-- Module: Mathlib.Topology.Homotopy.TopCat.Basic
Goal:
X Y : TopCat
f₀ : X ⟶ Y
⊢ h (refl f₀) = fst X I ≫ f₀

Tactic:
rfl

Premises used: ContinuousMap.comp, rfl, TopCat.Homotopy.h
-- Module: Mathlib.Topology.Homotopy.TopCat.Basic
Goal:
X Y : TopCat
f₀ f₁ : X ⟶ Y
F : Homotopy f₀ f₁
⊢ h F.symm = X ◁ I.symm ≫ F.h

Tactic:
rfl

Premises used: ContinuousMap.comp, Prod.map, unitInterval.symm, rfl, TopCat.Homotopy.h
-- Module: Mathlib.Topology.Homotopy.TopCat.Basic
Goal:
X Y Z : TopCat
f₀ f₁ : X ⟶ Y
g₀ g₁ : Y ⟶ Z
G : Homotopy g₀ g₁
F : Homotopy f₀ f₁
w :
  ∀ (x : (↑(tensorObj (𝒞 := instCategory) X I) : Type u)),
    Eq (α := (↑Z : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (G.comp F).h :
            (a : (↑(X ⊗ I) : Type u)) → (↑Z : Type u))
          x :
        (↑Z : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (X ◁ lift (𝟙 I) (𝟙 I) ≫ Iso.inv (α_ X I I) ≫ F.h ▷ I ≫ G.h) :
            (a : (↑(X ⊗ I) : Type u)) → (↑Z : Type u))
          x :
        (↑Z : Type u))
⊢ (G.comp F).h = X ◁ lift (𝟙 I) (𝟙 I) ≫ Iso.inv (α_ X I I) ≫ F.h ▷ I ≫ G.h

Tactic:
ext
-- Module: Mathlib.Topology.Homotopy.TopCat.Basic
Goal:
X Y Z : TopCat
f₀ f₁ : X ⟶ Y
g₀ g₁ : Y ⟶ Z
G : Homotopy g₀ g₁
F : Homotopy f₀ f₁
x : (↑(tensorObj (𝒞 := instCategory) X I) : Type u)
⊢ Eq (α := (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (G.comp F).h :
          (a : (↑(X ⊗ I) : Type u)) → (↑Z : Type u))
        x :
      (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (X ◁ lift (𝟙 I) (𝟙 I) ≫ Iso.inv (α_ X I I) ≫ F.h ▷ I ≫ G.h) :
          (a : (↑(X ⊗ I) : Type u)) → (↑Z : Type u))
        x :
      (↑Z : Type u))

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.TopCat.ToSSet
Goal:
X Y : TopCat
f g : X ⟶ Y
h : Homotopy f g
⊢ SSet.ι₀ ≫ TopCat.toSSet.obj X ◁ SSet.stdSimplex.toSSetObjI ≫ μ TopCat.toSSet X I ≫ TopCat.toSSet.map h.h =
    SSet.RelativeMorphism.map (A := ⊥) (B := ⊥) (φ :=
      Limits.IsInitial.to SSet.Subcomplex.isInitialBot (SSet.Subcomplex.toSSet (X := TopCat.toSSet.obj Y) ⊥))
      ((Equiv.symm SSet.RelativeMorphism.botEquiv :
          (a : TopCat.toSSet.obj X ⟶ TopCat.toSSet.obj Y) →
            SSet.RelativeMorphism ⊥ ⊥ (SSet.Subcomplex.isInitialBot.to ⊥.toSSet))
        (TopCat.toSSet.map f))

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.Topology.Homotopy.TopCat.ToSSet
Goal:
X Y : TopCat
f g : X ⟶ Y
h : Homotopy f g
⊢ SSet.ι₁ ≫ TopCat.toSSet.obj X ◁ SSet.stdSimplex.toSSetObjI ≫ μ TopCat.toSSet X I ≫ TopCat.toSSet.map h.h =
    SSet.RelativeMorphism.map (A := ⊥) (B := ⊥) (φ :=
      Limits.IsInitial.to SSet.Subcomplex.isInitialBot (SSet.Subcomplex.toSSet (X := TopCat.toSSet.obj Y) ⊥))
      ((Equiv.symm SSet.RelativeMorphism.botEquiv :
          (a : TopCat.toSSet.obj X ⟶ TopCat.toSSet.obj Y) →
            SSet.RelativeMorphism ⊥ ⊥ (SSet.Subcomplex.isInitialBot.to ⊥.toSSet))
        (TopCat.toSSet.map g))

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.Topology.Homotopy.TopCat.ToSSet
Goal:
X Y : TopCat
f g : X ⟶ Y
h : Homotopy f g
⊢ SSet.Subcomplex.ι ⊥ ▷ SSet.stdSimplex.obj { len := 1 : SimplexCategory } ≫
      TopCat.toSSet.obj X ◁ SSet.stdSimplex.toSSetObjI ≫ μ TopCat.toSSet X I ≫ TopCat.toSSet.map h.h =
    SemiCartesianMonoidalCategory.fst (SSet.Subcomplex.toSSet (X := TopCat.toSSet.obj X) ⊥)
        (SSet.stdSimplex.obj { len := 1 : SimplexCategory }) ≫
      CategoryStruct.comp (Y := SSet.Subcomplex.toSSet (X := TopCat.toSSet.obj Y) ⊥)
        (Limits.IsInitial.to SSet.Subcomplex.isInitialBot (SSet.Subcomplex.toSSet (X := TopCat.toSSet.obj Y) ⊥))
        (SSet.Subcomplex.ι ⊥)

Tactic:
ext _ ⟨⟨_, ⟨⟩⟩, _⟩