awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Product (goal)
Goal:
I : Type u
X : I → TopCat
⊢ Limits.IsLimit (π.mapCone (TopCat.piFan X))
have apply : Limits.IsLimit ((coneDiscreteComp X).functor.obj (π.mapCone (TopCat.piFan X)))
Tactic: apply (Limits.IsLimit.ofConeEquiv (coneDiscreteComp X)).toFun
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Product (goal)
Goal:
I : Type u
X : I → TopCat
⊢ Limits.IsLimit ((coneDiscreteComp X).functor.obj (π.mapCone (TopCat.piFan X)))
have simp : Limits.IsLimit (Limits.Fan.mk (π.obj (TopCat.of ((i : I) → (↑(X i) : Type u)))) (proj X))
Tactic: simp only [coneDiscreteComp_obj_mapCone]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Product (goal)
Goal:
I : Type u
X : I → TopCat
⊢ Limits.IsLimit (Limits.Fan.mk (π.obj (TopCat.of ((i : I) → (↑(X i) : Type u)))) (proj X))
have apply : Limits.IsLimit (J := Discrete I) (F := Discrete.functor fun (i : I) ↦ π.obj (X i))
  (Grpd.piLimitFan fun (i : I) ↦ π.obj (X i))
Tactic: apply Limits.IsLimit.ofIsoLimit _ (asIso (piTopToPiCone X)).symm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Product (goal)
Goal:
A : TopCat
B : TopCat
x₀ : (↑(π.obj A) : Type u)
x₁ : (↑(π.obj B) : Type v)
⊢ Eq (α :=
    { as := ((x₀, x₁).1.as, (x₀, x₁).2.as) :
        FundamentalGroupoid (↑(TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v))) : Type (max v u)) } ⟶
      { as := ((x₀, x₁).1.as, (x₀, x₁).2.as) })
    (match (motive :=
        (x y : Prod.{u, v} (↑(π.obj A) : Type u) (↑(π.obj B) : Type v)) →
          (x ⟶ y) →
            ({ as := (x.1.as, x.2.as) :
                FundamentalGroupoid (↑(TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v))) : Type (max v u)) } ⟶
              { as := (y.1.as, y.2.as) }))
        (x₀, x₁), (x₀, x₁), 𝟙 (x₀, x₁) with
      | (fst, snd), (fst_1, snd_1), (p₀, p₁) => Path.Homotopic.prod p₀ p₁ :
      { as := ((x₀, x₁).1.as, (x₀, x₁).2.as) :
          FundamentalGroupoid (↑(TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v))) : Type (max v u)) } ⟶
        { as := ((x₀, x₁).1.as, (x₀, x₁).2.as) })
    (𝟙 { as := ((x₀, x₁).1.as, (x₀, x₁).2.as) } :
      { as := ((x₀, x₁).1.as, (x₀, x₁).2.as) :
          FundamentalGroupoid (↑(TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v))) : Type (max v u)) } ⟶
        { as := ((x₀, x₁).1.as, (x₀, x₁).2.as) })
have simp : Path.Homotopic.prod (𝟙 x₀) (𝟙 x₁) = 𝟙 { as := (x₀.as, x₁.as) }
Tactic: simp only
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Product (goal)
Goal:
A : TopCat
B : TopCat
⊢ prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B) = 𝟭 (Prod.{u, v} (↑(π.obj A) : Type u) (↑(π.obj B) : Type v))
have 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
Tactic: apply CategoryTheory.Functor.hext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Product (goal)
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
⊢ prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B) = 𝟭 (Prod.{u, v} (↑(π.obj A) : Type u) (↑(π.obj B) : Type v))
have 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)
Tactic: apply CategoryTheory.Functor.hext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Product (goal)
Goal:
A : TopCat
B : TopCat
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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Product (goal)
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
⊢ (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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Product (goal)
Goal:
A : TopCat
B : TopCat
X : Prod.{u, v} (↑(π.obj A) : Type u) (↑(π.obj B) : Type v)
⊢ ((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
have 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
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Product (goal)
Goal:
A : TopCat
B : TopCat
X : Prod.{u, v} (↑(π.obj A) : Type u) (↑(π.obj B) : Type v)
⊢ ((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
have 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
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Product (hypothesis)
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
⊢ HEq ((prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B)).map (f₀, f₁)) (β :=
    CategoryTheory.Functor.obj (𝟭 (Prod.{u, v} (↑(π.obj A) : Type u) (↑(π.obj B) : Type v))) (x₀, x₁) ⟶
      CategoryTheory.Functor.obj (𝟭 (Prod.{u, v} (↑(π.obj A) : Type u) (↑(π.obj B) : Type v))) (y₀, y₁))
    (CategoryTheory.Functor.map (𝟭 (Prod.{u, v} (↑(π.obj A) : Type u) (↑(π.obj B) : Type v))) (f₀, f₁))
have this : 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₁)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Product (goal)
Goal:
A : TopCat
B : TopCat
⊢ (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))
have 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
Tactic: apply CategoryTheory.Functor.hext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Product (goal)
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
⊢ (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))
have 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)
Tactic: apply CategoryTheory.Functor.hext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Product (goal)
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).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
have 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
Tactic: apply FundamentalGroupoid.ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Product (goal)
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).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
have 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
Tactic: apply Prod.ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Product (goal)
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
⊢ (((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
have 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
Tactic: apply Prod.ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Product (goal)
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).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
have h_obj : ((projLeft A B).obj X).as = X.as.1
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Product (goal)
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).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
have h_obj : ((projRight A B).obj X).as = X.as.2
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
⊢ SimplyConnectedSpace X ↔ Nonempty X ∧ ∀ (x y : X), Nonempty.{max 1 (u_3 + 1)} (Unique (Path.Homotopic.Quotient x y))
have 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))
Tactic: simp only [simplyConnectedSpace_iff, equiv_punit_iff_unique,
    FundamentalGroupoid.nonempty_iff X, and_congr_right_iff, Nonempty.forall]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected (goal)
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
⊢ Nonempty.{u_3 + 1} (Unique (Path.Homotopic.Quotient x y))
have 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))
Tactic: rw [simply_connected_iff_unique_homotopic] at *
Cleared hypotheses: inst_3, x, y
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected (goal)
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
⊢ Nonempty.{u_3 + 1} (Unique (Path.Homotopic.Quotient x y))
have 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))
Tactic: tauto
Cleared hypotheses: inst_3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected (goal)
Goal:
Y : Type u_2
inst : TopologicalSpace Y
h : SimplyConnectedSpace Y
⊢ PathConnectedSpace Y ∧ ∀ (x y : Y), Subsingleton.{u_2 + 1} (Path.Homotopic.Quotient x y)
have left : PathConnectedSpace Y
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected (goal)
Goal:
Y : Type u_2
inst : TopologicalSpace Y
h : SimplyConnectedSpace Y
left : PathConnectedSpace Y
⊢ PathConnectedSpace Y ∧ ∀ (x y : Y), Subsingleton.{u_2 + 1} (Path.Homotopic.Quotient x y)
have right : ∀ (x y : Y), Subsingleton.{u_2 + 1} (Path.Homotopic.Quotient x y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected (hypothesis)
Goal:
Y : Type u_2
inst : TopologicalSpace Y
h : PathConnectedSpace Y ∧ ∀ (x y : Y), Subsingleton.{u_2 + 1} (Path.Homotopic.Quotient x y)
⊢ SimplyConnectedSpace Y
have left : PathConnectedSpace Y
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected (hypothesis)
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
⊢ SimplyConnectedSpace Y
have right : ∀ (x y : Y), Subsingleton.{u_2 + 1} (Path.Homotopic.Quotient x y)
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected (goal)
Goal:
Y : Type u_2
inst : TopologicalSpace Y
left : PathConnectedSpace Y
right : ∀ (x y : Y), Subsingleton.{u_2 + 1} (Path.Homotopic.Quotient x y)
⊢ SimplyConnectedSpace Y
have intro : Nonempty Y ∧ ∀ (x y : Y), Nonempty.{u_2 + 1} (Unique (Path.Homotopic.Quotient x y))
Tactic: rw [simply_connected_iff_unique_homotopic]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected (goal)
Goal:
Y : Type u_2
inst : TopologicalSpace Y
⊢ SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂
have h : ∀ (a a_1 : Y), (∀ (p₁ p₂ : Path a a_1), p₁.Homotopic p₂) ↔ Subsingleton.{u_2 + 1} (Path.Homotopic.Quotient a a_1)
Tactic: convert! simply_connected_iff_paths_homotopic (Y := Y)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected (goal)
Goal:
Y : Type u_2
inst : TopologicalSpace Y
a a_1 : Y
⊢ (∀ (p₁ p₂ : Path a a_1), p₁.Homotopic p₂) ↔ Subsingleton.{u_2 + 1} (Path.Homotopic.Quotient a a_1)
have 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
Tactic: simp [Path.Homotopic.Quotient, Setoid.eq_top_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected (goal)
Goal:
Y : Type u_2
inst : TopologicalSpace Y
⊢ SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)
have 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)
Tactic: rw [simply_connected_iff_paths_homotopic']
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected (goal)
Goal:
Y : Type u_2
inst : TopologicalSpace Y
⊢ (PathConnectedSpace Y ∧ ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂) ↔
    PathConnectedSpace Y ∧ ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected (goal)
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)
⊢ (PathConnectedSpace Y ∧ ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂) ↔
    PathConnectedSpace Y ∧ ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)
have 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₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected (goal)
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₂
have mpr : ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂
Tactic: refine ⟨hpc, fun {x y} p₁ p₂ => ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected (goal)
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
⊢ p₁.Homotopic p₂
have mpr : mk p₁ = mk p₂
Tactic: rw [← eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected (hypothesis)
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
⊢ mk p₁ = mk p₂
have hloops₁ : ∀ (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 γ)
Cleared hypotheses: hloops
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected (hypothesis)
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⟧
⊢ mk p₁ = mk p₂
have h : 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)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected (goal)
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
⊢ mk p₁ = mk p₂
have calc : ⟦p₁⟧ = (Path.Homotopic.Quotient.trans ⟦p₁⟧ (Path.Homotopic.Quotient.symm ⟦p₂⟧)).trans ⟦p₂⟧
Tactic: calc ⟦p₁⟧
      _ = trans (trans ⟦p₁⟧ (symm ⟦p₂⟧)) ⟦p₂⟧ := by simp
      _ = ⟦p₂⟧ := by grind
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected (goal)
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
calc : ⟦p₁⟧ = (Path.Homotopic.Quotient.trans ⟦p₁⟧ (Path.Homotopic.Quotient.symm ⟦p₂⟧)).trans ⟦p₂⟧
⊢ mk p₁ = mk p₂
have calc₁ : (Path.Homotopic.Quotient.trans ⟦p₁⟧ (Path.Homotopic.Quotient.symm ⟦p₂⟧)).trans ⟦p₂⟧ = ⟦p₂⟧
Tactic: calc ⟦p₁⟧
      _ = trans (trans ⟦p₁⟧ (symm ⟦p₂⟧)) ⟦p₂⟧ := by simp
      _ = ⟦p₂⟧ := by grind
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X ≃ₜ Y
s : Set Y
⊢ IsSimplyConnected.{u_1} (X := X) ((⇑f : (a : X) → Y) ⁻¹' s) ↔ IsSimplyConnected s
have rw : IsSimplyConnected.{u_1} (X := X) ((⇑f.symm : (a : Y) → X) '' s) ↔ IsSimplyConnected s
Tactic: rw [← image_symm, isSimplyConnected_image]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X ≃ₜ Y
s : Set Y
rw : IsSimplyConnected.{u_1} (X := X) ((⇑f.symm : (a : Y) → X) '' s) ↔ IsSimplyConnected s
⊢ IsSimplyConnected.{u_1} (X := X) ((⇑f : (a : X) → Y) ⁻¹' s) ↔ IsSimplyConnected s
have rw₁ : IsSimplyConnected s ↔ IsSimplyConnected s
Tactic: rw [← image_symm, isSimplyConnected_image]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ IsSimplyConnected s ↔
    IsPathConnected s ∧
      ∀ (x : X) (p : Path x x),
        (∀ (t : (↑unitInterval : Type)), Membership.mem (α := X) s ((p : (a : (↑unitInterval : Type)) → X) t : X)) →
          ∃ (F : p.Homotopy (Path.refl x)),
            ∀ (t : (↑unitInterval : Type) × (↑unitInterval : Type)),
              Membership.mem (α := X) s ((F : (a : (↑unitInterval : Type) × (↑unitInterval : Type)) → X) t : X)
have rw : (IsPathConnected s ∧ ∀ (x : (↑s : Type u_1)) (γ : Path x x), γ.Homotopic (Path.refl x)) ↔
  IsPathConnected s ∧
    ∀ (x : X) (p : Path x x),
      (∀ (t : (↑unitInterval : Type)), Membership.mem (α := X) s ((p : (a : (↑unitInterval : Type)) → X) t : X)) →
        ∃ (F : p.Homotopy (Path.refl x)),
          ∀ (t : (↑unitInterval : Type) × (↑unitInterval : Type)),
            Membership.mem (α := X) s ((F : (a : (↑unitInterval : Type) × (↑unitInterval : Type)) → X) t : X)
Tactic: rw [IsSimplyConnected, simply_connected_iff_loops_nullhomotopic,
    ← isPathConnected_iff_pathConnectedSpace]