awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
calc : ⟦p₁⟧ = (Path.Homotopic.Quotient.trans ⟦p₁⟧ (Path.Homotopic.Quotient.symm ⟦p₂⟧)).trans ⟦p₂⟧
calc₁ : (Path.Homotopic.Quotient.trans ⟦p₁⟧ (Path.Homotopic.Quotient.symm ⟦p₂⟧)).trans ⟦p₂⟧ = ⟦p₂⟧
⊢ mk p₁ = mk p₂

Tactic:
calc ⟦p₁⟧
      _ = trans (trans ⟦p₁⟧ (symm ⟦p₂⟧)) ⟦p₂⟧ := by simp
      _ = ⟦p₂⟧ := by grind

Premises used: Quotient.mk, Path.Homotopic.Quotient.trans, Path.Homotopic.Quotient.symm
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsSimplyConnected s
⊢ SimplyConnectedSpace.{u_1} (↑s : Type u_1)

Tactic:
hs

Premises used: IsSimplyConnected
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsSimplyConnected s
⊢ IsPathConnected s

Tactic:
have := hs.simplyConnectedSpace
  isPathConnected_iff_pathConnectedSpace.mpr inferInstance

Premises used: Iff.mpr, inferInstance, IsSimplyConnected.simplyConnectedSpace, isPathConnected_iff_pathConnectedSpace
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsSimplyConnected s
⊢ s.Nonempty

Tactic:
hs.isPathConnected.nonempty

Premises used: IsSimplyConnected.isPathConnected, IsPathConnected.nonempty
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsEmbedding f
s : Set X
⊢ IsSimplyConnected (f '' s) ↔ IsSimplyConnected s

Tactic:
hf.homeomorphImage s |>.toHomotopyEquiv |>.simplyConnectedSpace_iff |>.symm

Premises used: IsSimplyConnected, Topology.IsEmbedding.homeomorphImage, Homeomorph.toHomotopyEquiv, ContinuousMap.HomotopyEquiv.simplyConnectedSpace_iff, Iff.symm
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X ≃ₜ Y
s : Set X
⊢ IsSimplyConnected.{u_2} (X := Y) ((⇑f : (a : X) → Y) '' s) ↔ IsSimplyConnected s

Tactic:
f.isEmbedding.isSimplyConnected_image

Premises used: Homeomorph.isEmbedding, Topology.IsEmbedding.isSimplyConnected_image
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
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
rw₁ rw₂ : IsSimplyConnected s ↔ IsSimplyConnected s
⊢ IsSimplyConnected.{u_1} (X := X) ((⇑f : (a : X) → Y) ⁻¹' s) ↔ IsSimplyConnected s

Tactic:
rw [← image_symm, isSimplyConnected_image]

Premises used: Homeomorph.isSimplyConnected_image, Homeomorph.image_symm
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
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)
⊢ 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)

Tactic:
rw [IsSimplyConnected, simply_connected_iff_loops_nullhomotopic,
    ← isPathConnected_iff_pathConnectedSpace]

Premises used: IsSimplyConnected, isPathConnected_iff_pathConnectedSpace, simply_connected_iff_loops_nullhomotopic
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ (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:
.and .rfl ⟨fun h x p hp ↦ ?_, fun h x p ↦ ?_⟩

Premises used: Iff.rfl, Iff.and, Iff.intro
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
refine_1 :
  ∀ (h : ∀ (x : (↑s : Type u_1)) (γ : Path x x), γ.Homotopic (Path.refl x)) (x : X) (p : Path x x)
    (hp : ∀ (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)
refine_2 :
  ∀
    (h :
      ∀ (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))
    (x : (↑s : Type u_1)) (p : Path x x), p.Homotopic (Path.refl x)
⊢ (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:
refine .and .rfl ⟨fun h x p hp ↦ ?_, fun h x p ↦ ?_⟩
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : ∀ (x : (↑s : Type u_1)) (γ : Path x x), γ.Homotopic (Path.refl x)
x : X
p : Path x x
hp : ∀ (t : (↑unitInterval : Type)), Membership.mem (α := X) s ((p : (a : (↑unitInterval : Type)) → X) t : X)
⊢ x ∈ s

Tactic:
simpa using hp 0

Premises used: OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : ∀ (x : (↑s : Type u_1)) (γ : Path x x), γ.Homotopic (Path.refl x)
x : X
p : Path x x
hp : ∀ (t : (↑unitInterval : Type)), Membership.mem (α := X) s ((p : (a : (↑unitInterval : Type)) → X) t : X)
refine_1 :
  ∀ (x : { x : X // x ∈ s }) (p : Path (↑x : X) (↑x : X))
    (hp : ∀ (t : (↑unitInterval : Type)), Membership.mem (α := X) s ((p : (a : (↑unitInterval : Type)) → X) t : X)),
    ∃ (F : p.Homotopy (Path.refl (↑x : X))),
      ∀ (t : (↑unitInterval : Type) × (↑unitInterval : Type)),
        Membership.mem (α := X) s ((F : (a : (↑unitInterval : Type) × (↑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:
lift x to s using by simpa using hp 0
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : ∀ (x : (↑s : Type u_1)) (γ : Path x x), γ.Homotopic (Path.refl x)
x : { x : X // x ∈ s }
p : Path (↑x : X) (↑x : X)
hp : ∀ (t : (↑unitInterval : Type)), Membership.mem (α := X) s ((p : (a : (↑unitInterval : Type)) → X) t : X)
⊢ Subtype.mk (p := fun (x : X) ↦ x ∈ s) ((p : (a : (↑unitInterval : Type)) → X) 0) ⋯ = x

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : ∀ (x : (↑s : Type u_1)) (γ : Path x x), γ.Homotopic (Path.refl x)
x : { x : X // x ∈ s }
p : Path (↑x : X) (↑x : X)
hp : ∀ (t : (↑unitInterval : Type)), Membership.mem (α := X) s ((p : (a : (↑unitInterval : Type)) → X) t : X)
⊢ Subtype.mk (p := fun (x : X) ↦ x ∈ s) ((p : (a : (↑unitInterval : Type)) → X) 1) ⋯ = x

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : ∀ (x : (↑s : Type u_1)) (γ : Path x x), γ.Homotopic (Path.refl x)
x : { x : X // x ∈ s }
p : Path (↑x : X) (↑x : X)
hp : ∀ (t : (↑unitInterval : Type)), Membership.mem (α := X) s ((p : (a : (↑unitInterval : Type)) → X) t : X)
refine_1 :
  ∀
    (F :
      Path.Homotopy
        {
          toFun := fun (t : (↑unitInterval : Type)) ↦
            Subtype.mk (p := fun (x : X) ↦ x ∈ s) ((p : (a : (↑unitInterval : Type)) → X) t) ⋯,
          continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
        (Path.refl x)),
    ∃ (F : p.Homotopy (Path.refl (↑x : X))),
      ∀ (t : (↑unitInterval : Type) × (↑unitInterval : Type)),
        Membership.mem (α := X) s ((F : (a : (↑unitInterval : Type) × (↑unitInterval : Type)) → X) t : X)
⊢ ∃ (F : p.Homotopy (Path.refl (↑x : X))),
    ∀ (t : (↑unitInterval : Type) × (↑unitInterval : Type)),
      Membership.mem (α := X) s ((F : (a : (↑unitInterval : Type) × (↑unitInterval : Type)) → X) t : X)

Tactic:
rcases h x {
      toFun := fun t ↦ ⟨p t, hp t⟩
      source' := by simp
      target' := by simp
    } with ⟨F⟩

Premises used: ContinuousMap.mk, Subtype.mk, Path.mk, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : ∀ (x : (↑s : Type u_1)) (γ : Path x x), γ.Homotopic (Path.refl x)
x : { x : X // x ∈ s }
p : Path (↑x : X) (↑x : X)
hp : ∀ (t : (↑unitInterval : Type)), Membership.mem (α := X) s ((p : (a : (↑unitInterval : Type)) → X) t : X)
F :
  Path.Homotopy
    {
      toFun := fun (t : (↑unitInterval : Type)) ↦
        Subtype.mk (p := fun (x : X) ↦ x ∈ s) ((p : (a : (↑unitInterval : Type)) → X) t) ⋯,
      continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
    (Path.refl x)
⊢ ∃ (F : p.Homotopy (Path.refl (↑x : X))),
    ∀ (t : (↑unitInterval : Type) × (↑unitInterval : Type)),
      Membership.mem (α := X) s ((F : (a : (↑unitInterval : Type) × (↑unitInterval : Type)) → X) t : X)

Tactic:
⟨F.map (.restrict s (.id _)), fun t ↦ (F t).2⟩

Premises used: ContinuousMap.id, Exists.intro, DFunLike.coe, Path.Homotopy.map, Subtype.property, ContinuousMap.restrict
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : ∀ (x : (↑s : Type u_1)) (γ : Path x x), γ.Homotopic (Path.refl x)
x : { x : X // x ∈ s }
p : Path (↑x : X) (↑x : X)
hp : ∀ (t : (↑unitInterval : Type)), Membership.mem (α := X) s ((p : (a : (↑unitInterval : Type)) → X) t : X)
F :
  Path.Homotopy
    {
      toFun := fun (t : (↑unitInterval : Type)) ↦
        Subtype.mk (p := fun (x : X) ↦ x ∈ s) ((p : (a : (↑unitInterval : Type)) → X) t) ⋯,
      continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
    (Path.refl x)
⊢ ∃ (F : p.Homotopy (Path.refl (↑x : X))),
    ∀ (t : (↑unitInterval : Type) × (↑unitInterval : Type)),
      Membership.mem (α := X) s ((F : (a : (↑unitInterval : Type) × (↑unitInterval : Type)) → X) t : X)

Tactic:
exact ⟨F.map (.restrict s (.id _)), fun t ↦ (F t).2⟩
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h :
  ∀ (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)
x : (↑s : Type u_1)
p : Path x x
refine_2 :
  ∀ (F : (p.map ⋯).Homotopy (Path.refl (↑x : X)))
    (hF :
      ∀ (t : (↑unitInterval : Type) × (↑unitInterval : Type)),
        Membership.mem (α := X) s ((F : (a : (↑unitInterval : Type) × (↑unitInterval : Type)) → X) t : X)),
    p.Homotopic (Path.refl x)
⊢ p.Homotopic (Path.refl x)

Tactic:
rcases h x (p.map continuous_subtype_val) (fun t ↦ (p t).2) with ⟨F, hF⟩

Premises used: Path.map, continuous_subtype_val, Subtype.val, DFunLike.coe, Subtype.property
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h :
  ∀ (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)
x : (↑s : Type u_1)
p : Path x x
F : (p.map ⋯).Homotopy (Path.refl (↑x : X))
hF :
  ∀ (t : (↑unitInterval : Type) × (↑unitInterval : Type)),
    Membership.mem (α := X) s ((F : (a : (↑unitInterval : Type) × (↑unitInterval : Type)) → X) t : X)
⊢ ∀ (x_1 : (↑unitInterval : Type)),
    Eq (α := (↑s : Type u_1))
      (Subtype.mk (p := fun (x : X) ↦ x ∈ s) ((F : (a : (↑unitInterval : Type) × (↑unitInterval : Type)) → X) (0, x_1))
          ⋯ :
        { x : X // x ∈ s })
      ((p.toContinuousMap : (a : (↑unitInterval : Type)) → (↑s : Type u_1)) x_1 : (↑s : Type u_1))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h :
  ∀ (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)
x : (↑s : Type u_1)
p : Path x x
F : (p.map ⋯).Homotopy (Path.refl (↑x : X))
hF :
  ∀ (t : (↑unitInterval : Type) × (↑unitInterval : Type)),
    Membership.mem (α := X) s ((F : (a : (↑unitInterval : Type) × (↑unitInterval : Type)) → X) t : X)
⊢ ∀ (x_1 : (↑unitInterval : Type)),
    Eq (α := (↑s : Type u_1))
      (Subtype.mk (p := fun (x : X) ↦ x ∈ s) ((F : (a : (↑unitInterval : Type) × (↑unitInterval : Type)) → X) (1, x_1))
          ⋯ :
        { x : X // x ∈ s })
      ((Path.toContinuousMap (Path.refl x) : (a : (↑unitInterval : Type)) → (↑s : Type u_1)) x_1 : (↑s : Type u_1))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h :
  ∀ (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)
x : (↑s : Type u_1)
p : Path x x
F : (p.map ⋯).Homotopy (Path.refl (↑x : X))
hF :
  ∀ (t : (↑unitInterval : Type) × (↑unitInterval : Type)),
    Membership.mem (α := X) s ((F : (a : (↑unitInterval : Type) × (↑unitInterval : Type)) → X) t : X)
⊢ ∀ (t x_1 : (↑unitInterval : Type)),
    Membership.mem (γ := Set (↑unitInterval : Type)) {0, 1} x_1 →
      Eq (α := (↑s : Type u_1))
        (({
                toFun := fun (x_2 : (↑unitInterval : Type)) ↦
                  Subtype.mk (p := fun (x : X) ↦ x ∈ s)
                    ((F : (a : (↑unitInterval : Type) × (↑unitInterval : Type)) → X) (t, x_2)) ⋯,
                continuous_toFun := ⋯ } :
              (a : (↑unitInterval : Type)) → (↑s : Type u_1))
            x_1 :
          (↑s : Type u_1))
        ((p.toContinuousMap : (a : (↑unitInterval : Type)) → (↑s : Type u_1)) x_1 : (↑s : Type u_1))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h :
  ∀ (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)
x : (↑s : Type u_1)
p : Path x x
F : (p.map ⋯).Homotopy (Path.refl (↑x : X))
hF :
  ∀ (t : (↑unitInterval : Type) × (↑unitInterval : Type)),
    Membership.mem (α := X) s ((F : (a : (↑unitInterval : Type) × (↑unitInterval : Type)) → X) t : X)
⊢ p.Homotopic (Path.refl x)

Tactic:
exact ⟨{
      toFun t := ⟨F t, hF t⟩
      map_zero_left := by simp
      map_one_left := by simp
      prop' := by simp
    }⟩
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
G : Type u_3
inst_1 : Group G
inst_2 : MulAction G X
inst_3 : ContinuousConstSMul G X
c : G
s : Set X
⊢ IsSimplyConnected (c • s) ↔ IsSimplyConnected s

Tactic:
Homeomorph.smul c |>.isSimplyConnected_image

Premises used: Homeomorph.isSimplyConnected_image, Homeomorph.smul
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
G : Type u_3
inst_1 : GroupWithZero G
inst_2 : MulAction G X
inst_3 : ContinuousConstSMul G X
c : G
s : Set X
hc : c ≠ 0
⊢ IsSimplyConnected (c • s) ↔ IsSimplyConnected s

Tactic:
isSimplyConnected_smul_set_iff (c := Units.mk0 c hc)

Premises used: isSimplyConnected_smul_set_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
hi : trivialCofibrations C i
hp : fibrations C p
⊢ Cofibration i

Tactic:
obtain ⟨_, _⟩ := mem_trivialCofibrations_iff i |>.mp hi

Premises used: HomotopicalAlgebra.mem_trivialCofibrations_iff, Iff.mp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
hi : trivialCofibrations C i
hp : fibrations C p
left : Cofibration i
⊢ WeakEquivalence i

Tactic:
obtain ⟨_, _⟩ := mem_trivialCofibrations_iff i |>.mp hi

Premises used: HomotopicalAlgebra.mem_trivialCofibrations_iff, Iff.mp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
hi : trivialCofibrations C i
hp : fibrations C p
left : Cofibration i
right : WeakEquivalence i
⊢ Fibration p

Tactic:
rw [← fibration_iff] at hp

Premises used: HomotopicalAlgebra.fibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
hi : trivialCofibrations C i
hp : fibrations C p
left : Cofibration i
right : WeakEquivalence i
hp₁ : Fibration p
⊢ Cofibration i

Tactic:
rw [← fibration_iff] at hp

Premises used: HomotopicalAlgebra.fibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
hi : trivialCofibrations C i
hp : fibrations C p
left_1 : Cofibration i
right : WeakEquivalence i
hp₁ : Fibration p
left : Cofibration i
⊢ WeakEquivalence i

Tactic:
rw [← fibration_iff] at hp

Premises used: HomotopicalAlgebra.fibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
hi : trivialCofibrations C i
hp : Fibration p
left : Cofibration i
right : WeakEquivalence i
⊢ HasLiftingProperty i p

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
hi : cofibrations C i
hp : trivialFibrations C p
⊢ Fibration p ∧ WeakEquivalence p

Tactic:
rw [mem_trivialFibrations_iff] at hp

Premises used: HomotopicalAlgebra.mem_trivialFibrations_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
hi : cofibrations C i
hp : Fibration p ∧ WeakEquivalence p
⊢ Cofibration i

Tactic:
rw [← cofibration_iff] at hi

Premises used: HomotopicalAlgebra.cofibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
hi : cofibrations C i
hp : Fibration p ∧ WeakEquivalence p
hi₁ : Cofibration i
⊢ Fibration p ∧ WeakEquivalence p

Tactic:
rw [← cofibration_iff] at hi

Premises used: HomotopicalAlgebra.cofibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
hi : Cofibration i
hp : Fibration p ∧ WeakEquivalence p
⊢ Fibration p

Tactic:
have := hp.1
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
hi : Cofibration i
hp : Fibration p ∧ WeakEquivalence p
this : Fibration p
⊢ WeakEquivalence p

Tactic:
have := hp.2
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
hi : Cofibration i
hp : Fibration p ∧ WeakEquivalence p
this_1 : Fibration p
this : WeakEquivalence p
⊢ HasLiftingProperty i p

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_5 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_6 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
inst_7 : Fibration f
inst_8 : WeakEquivalence w
h : RetractArrow f w
have : ∀ (hw : MapFactorizationData (trivialCofibrations C) (fibrations C) w), WeakEquivalence f
⊢ WeakEquivalence f

Tactic:
have hw := factorizationData (trivialCofibrations C) (fibrations C) w
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_5 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_6 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
inst_7 : Fibration f
inst_8 : WeakEquivalence w
h : RetractArrow f w
hw : MapFactorizationData (trivialCofibrations C) (fibrations C) w
rw : IsStableUnderRetracts.{v, u} (rlp (cofibrations C))
⊢ IsStableUnderRetracts.{v, u} (trivialFibrations C)

Tactic:
rw [← cofibrations_rlp]

Premises used: HomotopicalAlgebra.cofibrations_rlp