awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
A : TopCat
B : TopCat
h_obj :
  ∀ (X : Prod.{u, v} (↑(π.obj A) : Type u) (↑(π.obj B) : Type v)),
    (prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B)).obj X =
      CategoryTheory.Functor.obj (𝟭 (Prod.{u, v} (↑(π.obj A) : Type u) (↑(π.obj B) : Type v))) X
h_map :
  ∀ (X Y : Prod.{u, v} (↑(π.obj A) : Type u) (↑(π.obj B) : Type v)) (f : X ⟶ Y),
    HEq ((prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B)).map f) (β :=
      CategoryTheory.Functor.obj (𝟭 (Prod.{u, v} (↑(π.obj A) : Type u) (↑(π.obj B) : Type v))) X ⟶
        CategoryTheory.Functor.obj (𝟭 (Prod.{u, v} (↑(π.obj A) : Type u) (↑(π.obj B) : Type v))) Y)
      (CategoryTheory.Functor.map (𝟭 (Prod.{u, v} (↑(π.obj A) : Type u) (↑(π.obj B) : Type v))) f)
⊢ prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B) = 𝟭 (Prod.{u, v} (↑(π.obj A) : Type u) (↑(π.obj B) : Type v))

Tactic:
apply CategoryTheory.Functor.hext

Premises used: CategoryTheory.Functor.hext
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
A : TopCat
B : TopCat
X : Prod.{u, v} (↑(π.obj A) : Type u) (↑(π.obj B) : Type v)
h_obj :
  ((prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B)).obj X).1 =
    (CategoryTheory.Functor.obj (𝟭 (Prod.{u, v} (↑(π.obj A) : Type u) (↑(π.obj B) : Type v))) X).1
h_obj₁ :
  ((prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B)).obj X).2 =
    (CategoryTheory.Functor.obj (𝟭 (Prod.{u, v} (↑(π.obj A) : Type u) (↑(π.obj B) : Type v))) X).2
⊢ (prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B)).obj X =
    CategoryTheory.Functor.obj (𝟭 (Prod.{u, v} (↑(π.obj A) : Type u) (↑(π.obj B) : Type v))) X

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
A : TopCat
B : TopCat
X : Prod.{u, v} (↑(π.obj A) : Type u) (↑(π.obj B) : Type v)
h_obj :
  (projLeft A B).obj { as := (X.1.as, X.2.as) : FundamentalGroupoid (Prod.{u, v} (↑A : Type u) (↑B : Type v)) } = X.1
⊢ ((prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B)).obj X).1 =
    (CategoryTheory.Functor.obj (𝟭 (Prod.{u, v} (↑(π.obj A) : Type u) (↑(π.obj B) : Type v))) X).1

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
A : TopCat
B : TopCat
X : Prod.{u, v} (↑(π.obj A) : Type u) (↑(π.obj B) : Type v)
h_obj :
  (projRight A B).obj { as := (X.1.as, X.2.as) : FundamentalGroupoid (Prod.{u, v} (↑A : Type u) (↑B : Type v)) } = X.2
⊢ ((prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B)).obj X).2 =
    (CategoryTheory.Functor.obj (𝟭 (Prod.{u, v} (↑(π.obj A) : Type u) (↑(π.obj B) : Type v))) X).2

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
A : TopCat
B : TopCat
X : Prod.{u, v} (↑(π.obj A) : Type u) (↑(π.obj B) : Type v)
⊢ (projLeft A B).obj { as := (X.1.as, X.2.as) : FundamentalGroupoid (Prod.{u, v} (↑A : Type u) (↑B : Type v)) } = X.1

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
A : TopCat
B : TopCat
X : Prod.{u, v} (↑(π.obj A) : Type u) (↑(π.obj B) : Type v)
⊢ (projRight A B).obj { as := (X.1.as, X.2.as) : FundamentalGroupoid (Prod.{u, v} (↑A : Type u) (↑B : Type v)) } = X.2

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
A : TopCat
B : TopCat
x₀ : (↑(π.obj A) : Type u)
x₁ : (↑(π.obj B) : Type v)
y₀ : (↑(π.obj A) : Type u)
y₁ : (↑(π.obj B) : Type v)
f₀ : (x₀, x₁).1 ⟶ (y₀, y₁).1
f₁ : (x₀, x₁).2 ⟶ (y₀, y₁).2
⊢ Path.Homotopic.projLeft ((prodToProdTop A B).map (f₀, f₁)) = f₀ ∧
    Path.Homotopic.projRight ((prodToProdTop A B).map (f₀, f₁)) = f₁

Tactic:
have : Path.Homotopic.projLeft ((prodToProdTop A B).map (f₀, f₁)) = f₀ ∧
      Path.Homotopic.projRight ((prodToProdTop A B).map (f₀, f₁)) = f₁ :=
        And.intro (Path.Homotopic.projLeft_prod f₀ f₁) (Path.Homotopic.projRight_prod f₀ f₁)
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
A : TopCat
B : TopCat
h_obj :
  ∀ (X : (↑(π.obj (TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v)))) : Type (max u v))),
    ((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).obj X =
      CategoryTheory.Functor.obj (𝟭 (↑(π.obj (TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v)))) : Type (max u v))) X
h_map :
  ∀ (X Y : (↑(π.obj (TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v)))) : Type (max u v))) (f : X ⟶ Y),
    HEq (((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).map f) (β :=
      CategoryTheory.Functor.obj (𝟭 (↑(π.obj (TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v)))) : Type (max u v)))
          X ⟶
        CategoryTheory.Functor.obj (𝟭 (↑(π.obj (TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v)))) : Type (max u v)))
          Y)
      (CategoryTheory.Functor.map (𝟭 (↑(π.obj (TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v)))) : Type (max u v)))
        f)
⊢ (projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B =
    𝟭 (↑(π.obj (TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v)))) : Type (max u v))

Tactic:
apply CategoryTheory.Functor.hext

Premises used: CategoryTheory.Functor.hext
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
A : TopCat
B : TopCat
X : (↑(π.obj (TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v)))) : Type (max u v))
h_obj :
  (((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).obj X).as =
    (CategoryTheory.Functor.obj (𝟭 (↑(π.obj (TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v)))) : Type (max u v)))
        X).as
⊢ ((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).obj X =
    CategoryTheory.Functor.obj (𝟭 (↑(π.obj (TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v)))) : Type (max u v))) X

Tactic:
apply FundamentalGroupoid.ext

Premises used: FundamentalGroupoid.ext
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
A : TopCat
B : TopCat
X : (↑(π.obj (TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v)))) : Type (max u v))
h_obj :
  (((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).obj X).as.1 =
    (CategoryTheory.Functor.obj (𝟭 (↑(π.obj (TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v)))) : Type (max u v)))
          X).as.1
h_obj₁ :
  (((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).obj X).as.2 =
    (CategoryTheory.Functor.obj (𝟭 (↑(π.obj (TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v)))) : Type (max u v)))
          X).as.2
⊢ (((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).obj X).as =
    (CategoryTheory.Functor.obj (𝟭 (↑(π.obj (TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v)))) : Type (max u v)))
        X).as

Tactic:
apply Prod.ext

Premises used: Prod.ext
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
A : TopCat
B : TopCat
X : (↑(π.obj (TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v)))) : Type (max u v))
h_obj : ((projLeft A B).obj X).as = X.as.1
⊢ (((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).obj X).as.1 =
    (CategoryTheory.Functor.obj (𝟭 (↑(π.obj (TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v)))) : Type (max u v)))
          X).as.1

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
A : TopCat
B : TopCat
X : (↑(π.obj (TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v)))) : Type (max u v))
h_obj : ((projRight A B).obj X).as = X.as.2
⊢ (((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).obj X).as.2 =
    (CategoryTheory.Functor.obj (𝟭 (↑(π.obj (TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v)))) : Type (max u v)))
          X).as.2

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
A : TopCat
B : TopCat
X : (↑(π.obj (TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v)))) : Type (max u v))
⊢ ((projLeft A B).obj X).as = X.as.1

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
A : TopCat
B : TopCat
X : (↑(π.obj (TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v)))) : Type (max u v))
⊢ ((projRight A B).obj X).as = X.as.2

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
A : TopCat
B : TopCat
x₀ : (↑A : Type u)
x₁ : (↑B : Type v)
y₀ : (↑A : Type u)
y₁ : (↑B : Type v)
f :
  { as := (x₀, x₁) : FundamentalGroupoid (↑(TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v))) : Type (max v u)) } ⟶
    { as := (y₀, y₁) }
⊢ HEq (((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).map f) (β :=
    CategoryTheory.Functor.obj (𝟭 (↑(π.obj (TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v)))) : Type (max u v)))
        { as := (x₀, x₁) :
          FundamentalGroupoid (↑(TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v))) : Type (max v u)) } ⟶
      CategoryTheory.Functor.obj (𝟭 (↑(π.obj (TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v)))) : Type (max u v)))
        { as := (y₀, y₁) :
          FundamentalGroupoid (↑(TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v))) : Type (max v u)) })
    (CategoryTheory.Functor.map (𝟭 (↑(π.obj (TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v)))) : Type (max u v))) f)

Tactic:
simpa [-Path.Homotopic.prod_projLeft_projRight] using Path.Homotopic.prod_projLeft_projRight f

Premises used: Path.Homotopic.prod_projLeft_projRight
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X : Type u_3
inst : TopologicalSpace X
simp :
  ∀ (a : X),
    (∀ (x y : FundamentalGroupoid X), Nonempty.{u_3 + 1} (Unique (x ⟶ y))) ↔
      ∀ (x y : X), Nonempty.{max 1 (u_3 + 1)} (Unique (Path.Homotopic.Quotient x y))
⊢ SimplyConnectedSpace X ↔ Nonempty X ∧ ∀ (x y : X), Nonempty.{max 1 (u_3 + 1)} (Unique (Path.Homotopic.Quotient x y))

Tactic:
simp only [simplyConnectedSpace_iff, equiv_punit_iff_unique,
    FundamentalGroupoid.nonempty_iff X, and_congr_right_iff, Nonempty.forall]

Premises used: Nonempty.forall, FundamentalGroupoid.nonempty_iff, and_congr_right_iff, simplyConnectedSpace_iff, CategoryTheory.equiv_punit_iff_unique
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X : Type u_3
inst : TopologicalSpace X
a : X
⊢ (∀ (x y : FundamentalGroupoid X), Nonempty.{u_3 + 1} (Unique (x ⟶ y))) ↔
    ∀ (x y : X), Nonempty.{max 1 (u_3 + 1)} (Unique (Path.Homotopic.Quotient x y))

Tactic:
⟨fun h _ _ => h _ _, fun h _ _ => h _ _⟩

Premises used: FundamentalGroupoid.mk, FundamentalGroupoid.as, Iff.intro
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X : Type u_3
inst : TopologicalSpace X
a : X
⊢ (∀ (x y : FundamentalGroupoid X), Nonempty.{u_3 + 1} (Unique (x ⟶ y))) ↔
    ∀ (x y : X), Nonempty.{max 1 (u_3 + 1)} (Unique (Path.Homotopic.Quotient x y))

Tactic:
exact ⟨fun h _ _ => h _ _, fun h _ _ => h _ _⟩
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hY : SimplyConnectedSpace Y
e : X ≃ₕ Y
⊢ SimplyConnectedSpace X

Tactic:
⟨hY.1.map (FundamentalGroupoidFunctor.equivOfHomotopyEquiv e).trans⟩

Premises used: SimplyConnectedSpace.equiv_unit, SimplyConnectedSpace.mk, FundamentalGroupoidFunctor.equivOfHomotopyEquiv, CategoryTheory.Equivalence.trans, Nonempty.map
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X ≃ₕ Y
⊢ SimplyConnectedSpace X ↔ SimplyConnectedSpace Y

Tactic:
⟨fun _ ↦ e.symm.simplyConnectedSpace, fun _ ↦ e.simplyConnectedSpace⟩

Premises used: ContinuousMap.HomotopyEquiv.symm, ContinuousMap.HomotopyEquiv.simplyConnectedSpace, Iff.intro
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
X : Type u_3
inst_2 : TopologicalSpace X
inst_3 : SimplyConnectedSpace X
x y : X
rw :
  (Nonempty X ∧ ∀ (x y : X), Nonempty.{u_3 + 1} (Unique (Path.Homotopic.Quotient x y))) →
    ∀ (x y : X), Nonempty.{u_3 + 1} (Unique (Path.Homotopic.Quotient x y))
⊢ Nonempty.{u_3 + 1} (Unique (Path.Homotopic.Quotient x y))

Tactic:
rw [simply_connected_iff_unique_homotopic] at *

Premises used: simply_connected_iff_unique_homotopic
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
X : Type u_3
inst_2 : TopologicalSpace X
inst_3 : Nonempty X ∧ ∀ (x y : X), Nonempty.{u_3 + 1} (Unique (Path.Homotopic.Quotient x y))
x y : X
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  Nonempty X →
    (∀ (x y : X), Nonempty.{u_3 + 1} (Unique (Path.Homotopic.Quotient x y))) →
      Nonempty.{u_3 + 1} (Unique (Path.Homotopic.Quotient x y))
⊢ Nonempty.{u_3 + 1} (Unique (Path.Homotopic.Quotient x y))

Tactic:
tauto
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
X : Type u_3
inst_2 : TopologicalSpace X
inst_3 : SimplyConnectedSpace X
⊢ PathConnectedSpace X

Tactic:
let unique_homotopic := (simply_connected_iff_unique_homotopic X).mp inferInstance
  { nonempty := unique_homotopic.1
    joined := fun x y => ⟨(unique_homotopic.2 x y).some.default.out⟩ }

Premises used: Inhabited.default, inferInstance, simply_connected_iff_unique_homotopic, Quotient.out, PathConnectedSpace.mk, Nonempty.intro, And.left, Iff.mp
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : SimplyConnectedSpace X
x y : X
p₁ p₂ : Path x y
⊢ p₁.Homotopic p₂

Tactic:
Quotient.eq.mp (@Subsingleton.elim (Path.Homotopic.Quotient x y) _ _ _)

Premises used: Iff.mp, Subsingleton.elim, Quotient.eq
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X_1 : Type u_1
Y_1 : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y_1
X : Type u_3
inst_2 : TopologicalSpace X
inst_3 : SimplyConnectedSpace X
Y : Type u_4
inst_4 : TopologicalSpace Y
inst_5 : ContractibleSpace Y
⊢ SimplyConnectedSpace Y

Tactic:
haveI : SimplyConnectedSpace Unit := ⟨⟨FundamentalGroupoid.punitEquivDiscretePUnit⟩⟩
  (ContractibleSpace.hequiv Y Unit).some.simplyConnectedSpace

Premises used: Nonempty.some, ContractibleSpace.hequiv, Unit, ContinuousMap.HomotopyEquiv.simplyConnectedSpace
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
Y : Type u_2
inst : TopologicalSpace Y
h : SimplyConnectedSpace Y
left : PathConnectedSpace Y
right : ∀ (x y : Y), Subsingleton.{u_2 + 1} (Path.Homotopic.Quotient x y)
⊢ PathConnectedSpace Y ∧ ∀ (x y : Y), Subsingleton.{u_2 + 1} (Path.Homotopic.Quotient x y)

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
Y : Type u_2
inst : TopologicalSpace Y
h : SimplyConnectedSpace Y
⊢ PathConnectedSpace Y

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
Y : Type u_2
inst : TopologicalSpace Y
h : SimplyConnectedSpace Y
⊢ ∀ (x y : Y), Subsingleton.{u_2 + 1} (Path.Homotopic.Quotient x y)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
Y : Type u_2
inst : TopologicalSpace Y
h : PathConnectedSpace Y ∧ ∀ (x y : Y), Subsingleton.{u_2 + 1} (Path.Homotopic.Quotient x y)
⊢ PathConnectedSpace Y

Tactic:
cases h
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
Y : Type u_2
inst : TopologicalSpace Y
h : PathConnectedSpace Y ∧ ∀ (x y : Y), Subsingleton.{u_2 + 1} (Path.Homotopic.Quotient x y)
left : PathConnectedSpace Y
⊢ ∀ (x y : Y), Subsingleton.{u_2 + 1} (Path.Homotopic.Quotient x y)

Tactic:
cases h
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
Y : Type u_2
inst : TopologicalSpace Y
left : PathConnectedSpace Y
right : ∀ (x y : Y), Subsingleton.{u_2 + 1} (Path.Homotopic.Quotient x y)
intro : Nonempty Y ∧ ∀ (x y : Y), Nonempty.{u_2 + 1} (Unique (Path.Homotopic.Quotient x y))
⊢ SimplyConnectedSpace Y

Tactic:
rw [simply_connected_iff_unique_homotopic]

Premises used: simply_connected_iff_unique_homotopic
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
Y : Type u_2
inst : TopologicalSpace Y
left : PathConnectedSpace Y
right : ∀ (x y : Y), Subsingleton.{u_2 + 1} (Path.Homotopic.Quotient x y)
⊢ Nonempty Y ∧ ∀ (x y : Y), Nonempty.{u_2 + 1} (Unique (Path.Homotopic.Quotient x y))

Tactic:
⟨inferInstance, fun x y => ⟨uniqueOfSubsingleton ⟦PathConnectedSpace.somePath x y⟧⟩⟩

Premises used: inferInstance, Nonempty.intro, Quotient.mk, Path.Homotopic.setoid, And.intro, PathConnectedSpace.somePath, uniqueOfSubsingleton
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
Y : Type u_2
inst : TopologicalSpace Y
left : PathConnectedSpace Y
right : ∀ (x y : Y), Subsingleton.{u_2 + 1} (Path.Homotopic.Quotient x y)
⊢ Nonempty Y ∧ ∀ (x y : Y), Nonempty.{u_2 + 1} (Unique (Path.Homotopic.Quotient x y))

Tactic:
exact ⟨inferInstance, fun x y => ⟨uniqueOfSubsingleton ⟦PathConnectedSpace.somePath x y⟧⟩⟩
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
Y : Type u_2
inst : TopologicalSpace Y
⊢ SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ (x y : Y), Subsingleton.{u_2 + 1} (Path.Homotopic.Quotient x y)

Tactic:
simply_connected_iff_paths_homotopic (Y := Y)

Premises used: simply_connected_iff_paths_homotopic
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
Y : Type u_2
inst : TopologicalSpace Y
h : ∀ (a a_1 : Y), (∀ (p₁ p₂ : Path a a_1), p₁.Homotopic p₂) ↔ Subsingleton.{u_2 + 1} (Path.Homotopic.Quotient a a_1)
⊢ SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂

Tactic:
convert! simply_connected_iff_paths_homotopic (Y := Y)

Premises used: simply_connected_iff_paths_homotopic
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
Y : Type u_2
inst : TopologicalSpace Y
a a_1 : Y
h :
  (∀ (p₁ p₂ : Path a a_1), p₁.Homotopic p₂) ↔
    ∀ (x y : Path a a_1), (Path.Homotopic.setoid a a_1 : Path a a_1 → Path a a_1 → Prop) x y
⊢ (∀ (p₁ p₂ : Path a a_1), p₁.Homotopic p₂) ↔ Subsingleton.{u_2 + 1} (Path.Homotopic.Quotient a a_1)

Tactic:
simp [Path.Homotopic.Quotient, Setoid.eq_top_iff]

Premises used: Path.Homotopic.Quotient, Setoid.eq_top_iff
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
Y : Type u_2
inst : TopologicalSpace Y
a a_1 : Y
⊢ (∀ (p₁ p₂ : Path a a_1), p₁.Homotopic p₂) ↔
    ∀ (x y : Path a a_1), (Path.Homotopic.setoid a a_1 : Path a a_1 → Path a a_1 → Prop) x y

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
Y : Type u_2
inst : TopologicalSpace Y
rw :
  (PathConnectedSpace Y ∧ ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂) ↔
    PathConnectedSpace Y ∧ ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)
⊢ SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)

Tactic:
rw [simply_connected_iff_paths_homotopic']

Premises used: simply_connected_iff_paths_homotopic'
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
Y : Type u_2
inst : TopologicalSpace Y
mp :
  (PathConnectedSpace Y ∧ ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂) →
    PathConnectedSpace Y ∧ ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)
mpr :
  (PathConnectedSpace Y ∧ ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)) →
    PathConnectedSpace Y ∧ ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂
⊢ (PathConnectedSpace Y ∧ ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂) ↔
    PathConnectedSpace Y ∧ ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
Y : Type u_2
inst : TopologicalSpace Y
hpc : PathConnectedSpace Y
hall : ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂
⊢ PathConnectedSpace Y ∧ ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)

Tactic:
⟨hpc, fun x γ => hall γ (Path.refl x)⟩

Premises used: And.intro, Path.refl
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
Y : Type u_2
inst : TopologicalSpace Y
hpc : PathConnectedSpace Y
hall : ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂
⊢ PathConnectedSpace Y ∧ ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)

Tactic:
exact ⟨hpc, fun x γ => hall γ (Path.refl x)⟩
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
Y : Type u_2
inst : TopologicalSpace Y
hpc : PathConnectedSpace Y
hloops : ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)
⊢ PathConnectedSpace Y ∧ ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂

Tactic:
⟨hpc, fun {x y} p₁ p₂ => ?_⟩

Premises used: And.intro
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
Y : Type u_2
inst : TopologicalSpace Y
hpc : PathConnectedSpace Y
hloops : ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)
mpr : ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂
⊢ PathConnectedSpace Y ∧ ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂

Tactic:
refine ⟨hpc, fun {x y} p₁ p₂ => ?_⟩
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
Y : Type u_2
inst : TopologicalSpace Y
hpc : PathConnectedSpace Y
hloops : ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)
x y : Y
p₁ p₂ : Path x y
mpr : mk p₁ = mk p₂
⊢ p₁.Homotopic p₂

Tactic:
rw [← eq]

Premises used: Path.Homotopic.Quotient.eq
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
Y : Type u_2
inst : TopologicalSpace Y
hpc : PathConnectedSpace Y
hloops : ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)
x y : Y
p₁ p₂ : Path x y
⊢ ∀ (x : Y) (γ : Path x x), Eq (α := Quotient (α := Path x x) (Path.Homotopic.setoid x x)) ⟦γ⟧ ⟦Path.refl x⟧

Tactic:
replace hloops : ∀ (x : Y) (γ : Path x x),
        (⟦γ⟧ : Path.Homotopic.Quotient x x) = ⟦Path.refl x⟧ :=
      fun x γ => Quotient.sound (hloops x γ)
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
Y : Type u_2
inst : TopologicalSpace Y
hpc : PathConnectedSpace Y
x y : Y
p₁ p₂ : Path x y
hloops : ∀ (x : Y) (γ : Path x x), Eq (α := Quotient (α := Path x x) (Path.Homotopic.setoid x x)) ⟦γ⟧ ⟦Path.refl x⟧
⊢ Path.Homotopic.Quotient.trans ⟦p₁⟧ (Path.Homotopic.Quotient.symm ⟦p₂⟧) = Path.Homotopic.Quotient.refl x

Tactic:
simpa using hloops x (p₁.trans p₂.symm)

Premises used: Path.symm, Path.trans
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
Y : Type u_2
inst : TopologicalSpace Y
hpc : PathConnectedSpace Y
x y : Y
p₁ p₂ : Path x y
hloops : ∀ (x : Y) (γ : Path x x), Eq (α := Quotient (α := Path x x) (Path.Homotopic.setoid x x)) ⟦γ⟧ ⟦Path.refl x⟧
⊢ Path.Homotopic.Quotient.trans ⟦p₁⟧ (Path.Homotopic.Quotient.symm ⟦p₂⟧) = Path.Homotopic.Quotient.refl x

Tactic:
have h : trans ⟦p₁⟧ (symm ⟦p₂⟧) = refl x := by
      simpa using hloops x (p₁.trans p₂.symm)
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
Y : Type u_2
inst : TopologicalSpace Y
hpc : PathConnectedSpace Y
x y : Y
p₁ p₂ : Path x y
hloops : ∀ (x : Y) (γ : Path x x), Eq (α := Quotient (α := Path x x) (Path.Homotopic.setoid x x)) ⟦γ⟧ ⟦Path.refl x⟧
h : Path.Homotopic.Quotient.trans ⟦p₁⟧ (Path.Homotopic.Quotient.symm ⟦p₂⟧) = Path.Homotopic.Quotient.refl x
⊢ ⟦p₁⟧ = (Path.Homotopic.Quotient.trans ⟦p₁⟧ (Path.Homotopic.Quotient.symm ⟦p₂⟧)).trans ⟦p₂⟧

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
Y : Type u_2
inst : TopologicalSpace Y
hpc : PathConnectedSpace Y
x y : Y
p₁ p₂ : Path x y
hloops : ∀ (x : Y) (γ : Path x x), Eq (α := Quotient (α := Path x x) (Path.Homotopic.setoid x x)) ⟦γ⟧ ⟦Path.refl x⟧
h : Path.Homotopic.Quotient.trans ⟦p₁⟧ (Path.Homotopic.Quotient.symm ⟦p₂⟧) = Path.Homotopic.Quotient.refl x
⊢ (Path.Homotopic.Quotient.trans ⟦p₁⟧ (Path.Homotopic.Quotient.symm ⟦p₂⟧)).trans ⟦p₂⟧ = ⟦p₂⟧

Tactic:
grind