awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
inst_3 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
f : ContinuousMap.{u_3, u_2} A (↑s : Type u_2)
hs :
  ∀ (a : A),
    Membership.mem (α := X) s
      ((ContinuousMap.comp
              { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
            (a : A) → X)
          a :
        X)
F : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)
hF :
  Eq (α := A → (↑s : Type u_2)) (s.restrictPreimage p ∘ (⇑F : (a : A) → (↑(p ⁻¹' s) : Type u_1)))
    (⇑f : (a : A) → (↑s : Type u_2))
he :
  p (↑((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀) : E) =
    (ContinuousMap.comp
          { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
        (a : A) → X)
      a₀
hF_unique :
  ∀ (y : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)),
    (fun (F_1 : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)) ↦
          Eq.{u_1 + 1} (α := (↑(p ⁻¹' s) : Type u_1))
              ((F_1 : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀ : (↑(p ⁻¹' s) : Type u_1))
              ((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀ : (↑(p ⁻¹' s) : Type u_1)) ∧
            Eq (α := A → (↑s : Type u_2)) (s.restrictPreimage p ∘ (⇑F_1 : (a : A) → (↑(p ⁻¹' s) : Type u_1)))
              (⇑f : (a : A) → (↑s : Type u_2)))
        y →
      y = F
F' : C(A, E)
hF'₁ : Eq.{u_1 + 1} (α := E) ((F' : (a : A) → E) a₀ : E) ((↑((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀) : E) : E)
hF'₂ : ∀ (x : A), p ((F' : (a : A) → E) x) = (↑((f : (a : A) → { x : X // x ∈ s }) x) : X)
a : A
⊢ (↑((f : (a : A) → { x : X // x ∈ s }) a) : X) ∈ s

Tactic:
(f a).2

Premises used: Set.Mem, DFunLike.coe, Subtype.property
-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
inst_3 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
f : ContinuousMap.{u_3, u_2} A (↑s : Type u_2)
hs :
  ∀ (a : A),
    Membership.mem (α := X) s
      ((ContinuousMap.comp
              { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
            (a : A) → X)
          a :
        X)
F : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)
hF :
  Eq (α := A → (↑s : Type u_2)) (s.restrictPreimage p ∘ (⇑F : (a : A) → (↑(p ⁻¹' s) : Type u_1)))
    (⇑f : (a : A) → (↑s : Type u_2))
he :
  p (↑((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀) : E) =
    (ContinuousMap.comp
          { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
        (a : A) → X)
      a₀
hF_unique :
  ∀ (y : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)),
    (fun (F_1 : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)) ↦
          Eq.{u_1 + 1} (α := (↑(p ⁻¹' s) : Type u_1))
              ((F_1 : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀ : (↑(p ⁻¹' s) : Type u_1))
              ((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀ : (↑(p ⁻¹' s) : Type u_1)) ∧
            Eq (α := A → (↑s : Type u_2)) (s.restrictPreimage p ∘ (⇑F_1 : (a : A) → (↑(p ⁻¹' s) : Type u_1)))
              (⇑f : (a : A) → (↑s : Type u_2)))
        y →
      y = F
F' : C(A, E)
hF'₁ : Eq.{u_1 + 1} (α := E) ((F' : (a : A) → E) a₀ : E) ((↑((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀) : E) : E)
hF'₂ : ∀ (x : A), p ((F' : (a : A) → E) x) = (↑((f : (a : A) → { x : X // x ∈ s }) x) : X)
a : A
⊢ (↑((f : (a : A) → { x : X // x ∈ s }) a) : X) ∈ s

Tactic:
exact (f a).2

Premises used: DFunLike.coe, Subtype.property
-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
inst_3 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
f : ContinuousMap.{u_3, u_2} A (↑s : Type u_2)
hs :
  ∀ (a : A),
    Membership.mem (α := X) s
      ((ContinuousMap.comp
              { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
            (a : A) → X)
          a :
        X)
F : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)
hF :
  Eq (α := A → (↑s : Type u_2)) (s.restrictPreimage p ∘ (⇑F : (a : A) → (↑(p ⁻¹' s) : Type u_1)))
    (⇑f : (a : A) → (↑s : Type u_2))
he :
  p (↑((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀) : E) =
    (ContinuousMap.comp
          { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
        (a : A) → X)
      a₀
hF_unique :
  ∀ (y : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)),
    (fun (F_1 : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)) ↦
          Eq.{u_1 + 1} (α := (↑(p ⁻¹' s) : Type u_1))
              ((F_1 : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀ : (↑(p ⁻¹' s) : Type u_1))
              ((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀ : (↑(p ⁻¹' s) : Type u_1)) ∧
            Eq (α := A → (↑s : Type u_2)) (s.restrictPreimage p ∘ (⇑F_1 : (a : A) → (↑(p ⁻¹' s) : Type u_1)))
              (⇑f : (a : A) → (↑s : Type u_2)))
        y →
      y = F
F' : C(A, E)
hF'₁ : Eq.{u_1 + 1} (α := E) ((F' : (a : A) → E) a₀ : E) ((↑((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀) : E) : E)
hF'₂ : ∀ (x : A), p ((F' : (a : A) → E) x) = (↑((f : (a : A) → { x : X // x ∈ s }) x) : X)
⊢ Continuous[inst_2, instTopologicalSpaceSubtype] fun (a : A) ↦
    Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' s) ((F' : (a : A) → E) a) ⋯

Tactic:
fun_prop
-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
inst_3 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
f : ContinuousMap.{u_3, u_2} A (↑s : Type u_2)
hs :
  ∀ (a : A),
    Membership.mem (α := X) s
      ((ContinuousMap.comp
              { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
            (a : A) → X)
          a :
        X)
F : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)
hF :
  Eq (α := A → (↑s : Type u_2)) (s.restrictPreimage p ∘ (⇑F : (a : A) → (↑(p ⁻¹' s) : Type u_1)))
    (⇑f : (a : A) → (↑s : Type u_2))
he :
  p (↑((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀) : E) =
    (ContinuousMap.comp
          { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
        (a : A) → X)
      a₀
hF_unique :
  ∀ (y : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)),
    (fun (F_1 : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)) ↦
          Eq.{u_1 + 1} (α := (↑(p ⁻¹' s) : Type u_1))
              ((F_1 : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀ : (↑(p ⁻¹' s) : Type u_1))
              ((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀ : (↑(p ⁻¹' s) : Type u_1)) ∧
            Eq (α := A → (↑s : Type u_2)) (s.restrictPreimage p ∘ (⇑F_1 : (a : A) → (↑(p ⁻¹' s) : Type u_1)))
              (⇑f : (a : A) → (↑s : Type u_2)))
        y →
      y = F
F' : C(A, E)
hF'₁ : Eq.{u_1 + 1} (α := E) ((F' : (a : A) → E) a₀ : E) ((↑((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀) : E) : E)
hF'₂ : ∀ (x : A), p ((F' : (a : A) → E) x) = (↑((f : (a : A) → { x : X // x ∈ s }) x) : X)
refine_2 :
  Eq (α := A → (↑s : Type u_2))
    (s.restrictPreimage p ∘
      (⇑{ toFun := fun (a : A) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' s) ((F' : (a : A) → E) a) ⋯,
            continuous_toFun := ⋯ } :
        (a : A) → (↑(p ⁻¹' s) : Type u_1)))
    (⇑f : (a : A) → (↑s : Type u_2))
refine_2₁ :
  ∀
    (hF_unique :
      { toFun := fun (a : A) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' s) ((F' : (a : A) → E) a) ⋯,
          continuous_toFun := ⋯ } =
        F),
    F' = ContinuousMap.comp { toFun := Subtype.val (p := fun (x : E) ↦ x ∈ p ⁻¹' s), continuous_toFun := ⋯ } F
⊢ F' = ContinuousMap.comp { toFun := Subtype.val (p := fun (x : E) ↦ x ∈ p ⁻¹' s), continuous_toFun := ⋯ } F

Tactic:
specialize hF_unique
      ⟨fun a ↦ ⟨F' a, by rw [Set.mem_preimage, hF'₂]; exact (f a).2⟩, by fun_prop⟩
      ⟨Subtype.ext hF'₁, ?_⟩

Premises used: ContinuousMap.mk, Subtype.mk, And.intro, DFunLike.coe, Subtype.ext
-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
inst_3 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
f : ContinuousMap.{u_3, u_2} A (↑s : Type u_2)
hs :
  ∀ (a : A),
    Membership.mem (α := X) s
      ((ContinuousMap.comp
              { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
            (a : A) → X)
          a :
        X)
F : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)
hF :
  Eq (α := A → (↑s : Type u_2)) (s.restrictPreimage p ∘ (⇑F : (a : A) → (↑(p ⁻¹' s) : Type u_1)))
    (⇑f : (a : A) → (↑s : Type u_2))
he :
  p (↑((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀) : E) =
    (ContinuousMap.comp
          { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
        (a : A) → X)
      a₀
hF_unique :
  ∀ (y : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)),
    (fun (F_1 : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)) ↦
          Eq.{u_1 + 1} (α := (↑(p ⁻¹' s) : Type u_1))
              ((F_1 : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀ : (↑(p ⁻¹' s) : Type u_1))
              ((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀ : (↑(p ⁻¹' s) : Type u_1)) ∧
            Eq (α := A → (↑s : Type u_2)) (s.restrictPreimage p ∘ (⇑F_1 : (a : A) → (↑(p ⁻¹' s) : Type u_1)))
              (⇑f : (a : A) → (↑s : Type u_2)))
        y →
      y = F
F' : C(A, E)
hF'₁ : Eq.{u_1 + 1} (α := E) ((F' : (a : A) → E) a₀ : E) ((↑((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀) : E) : E)
hF'₂ : ∀ (x : A), p ((F' : (a : A) → E) x) = (↑((f : (a : A) → { x : X // x ∈ s }) x) : X)
refine_2 :
  ∀ (x : A),
    (↑((s.restrictPreimage p ∘
              (⇑{ toFun := fun (a : A) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' s) ((F' : (a : A) → E) a) ⋯,
                    continuous_toFun := ⋯ : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1) } :
                (a : A) → (↑(p ⁻¹' s) : Type u_1)))
            x) :
        X) =
      (↑((f : (a : A) → (↑s : Type u_2)) x) : X)
⊢ Eq (α := A → (↑s : Type u_2))
    (s.restrictPreimage p ∘
      (⇑{ toFun := fun (a : A) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' s) ((F' : (a : A) → E) a) ⋯,
            continuous_toFun := ⋯ } :
        (a : A) → (↑(p ⁻¹' s) : Type u_1)))
    (⇑f : (a : A) → (↑s : Type u_2))

Tactic:
ext
-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
inst_3 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
f : ContinuousMap.{u_3, u_2} A (↑s : Type u_2)
hs :
  ∀ (a : A),
    Membership.mem (α := X) s
      ((ContinuousMap.comp
              { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
            (a : A) → X)
          a :
        X)
F : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)
hF :
  Eq (α := A → (↑s : Type u_2)) (s.restrictPreimage p ∘ (⇑F : (a : A) → (↑(p ⁻¹' s) : Type u_1)))
    (⇑f : (a : A) → (↑s : Type u_2))
he :
  p (↑((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀) : E) =
    (ContinuousMap.comp
          { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
        (a : A) → X)
      a₀
hF_unique :
  ∀ (y : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)),
    (fun (F_1 : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)) ↦
          Eq.{u_1 + 1} (α := (↑(p ⁻¹' s) : Type u_1))
              ((F_1 : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀ : (↑(p ⁻¹' s) : Type u_1))
              ((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀ : (↑(p ⁻¹' s) : Type u_1)) ∧
            Eq (α := A → (↑s : Type u_2)) (s.restrictPreimage p ∘ (⇑F_1 : (a : A) → (↑(p ⁻¹' s) : Type u_1)))
              (⇑f : (a : A) → (↑s : Type u_2)))
        y →
      y = F
F' : C(A, E)
hF'₁ : Eq.{u_1 + 1} (α := E) ((F' : (a : A) → E) a₀ : E) ((↑((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀) : E) : E)
hF'₂ : ∀ (x : A), p ((F' : (a : A) → E) x) = (↑((f : (a : A) → { x : X // x ∈ s }) x) : X)
x : A
⊢ (↑((s.restrictPreimage p ∘
            (⇑{ toFun := fun (a : A) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' s) ((F' : (a : A) → E) a) ⋯,
                  continuous_toFun := ⋯ : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1) } :
              (a : A) → (↑(p ⁻¹' s) : Type u_1)))
          x) :
      X) =
    (↑((f : (a : A) → (↑s : Type u_2)) x) : X)

Tactic:
simp [← hF'₂]
-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
inst_3 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
f : ContinuousMap.{u_3, u_2} A (↑s : Type u_2)
hs :
  ∀ (a : A),
    Membership.mem (α := X) s
      ((ContinuousMap.comp
              { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
            (a : A) → X)
          a :
        X)
F : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)
hF :
  Eq (α := A → (↑s : Type u_2)) (s.restrictPreimage p ∘ (⇑F : (a : A) → (↑(p ⁻¹' s) : Type u_1)))
    (⇑f : (a : A) → (↑s : Type u_2))
he :
  p (↑((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀) : E) =
    (ContinuousMap.comp
          { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
        (a : A) → X)
      a₀
F' : C(A, E)
hF'₁ : Eq.{u_1 + 1} (α := E) ((F' : (a : A) → E) a₀ : E) ((↑((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀) : E) : E)
hF'₂ : ∀ (x : A), p ((F' : (a : A) → E) x) = (↑((f : (a : A) → { x : X // x ∈ s }) x) : X)
hF_unique :
  { toFun := fun (a : A) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' s) ((F' : (a : A) → E) a) ⋯,
      continuous_toFun := ⋯ } =
    F
refine_2 :
  ∀ (a : A),
    Eq.{u_1 + 1} (α := E) ((F' : (a : A) → E) a : E)
      ((ContinuousMap.comp
              { toFun := Subtype.val (p := fun (x : E) ↦ x ∈ p ⁻¹' s), continuous_toFun := ⋯ :
                C({ x : E // x ∈ p ⁻¹' s }, E) }
              F :
            (a : A) → E)
          a :
        E)
⊢ F' = ContinuousMap.comp { toFun := Subtype.val (p := fun (x : E) ↦ x ∈ p ⁻¹' s), continuous_toFun := ⋯ } F

Tactic:
ext
-- Module: Mathlib.Topology.Homotopy.Lifting
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
inst_3 : SimplyConnectedSpace A
inst_4 : LocPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
f : ContinuousMap.{u_3, u_2} A (↑s : Type u_2)
hs :
  ∀ (a : A),
    Membership.mem (α := X) s
      ((ContinuousMap.comp
              { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
            (a : A) → X)
          a :
        X)
F : ContinuousMap.{u_3, u_1} A (↑(p ⁻¹' s) : Type u_1)
hF :
  Eq (α := A → (↑s : Type u_2)) (s.restrictPreimage p ∘ (⇑F : (a : A) → (↑(p ⁻¹' s) : Type u_1)))
    (⇑f : (a : A) → (↑s : Type u_2))
he :
  p (↑((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀) : E) =
    (ContinuousMap.comp
          { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), continuous_toFun := ⋯ : C({ x : X // x ∈ s }, X) } f :
        (a : A) → X)
      a₀
F' : C(A, E)
hF'₁ : Eq.{u_1 + 1} (α := E) ((F' : (a : A) → E) a₀ : E) ((↑((F : (a : A) → (↑(p ⁻¹' s) : Type u_1)) a₀) : E) : E)
hF'₂ : ∀ (x : A), p ((F' : (a : A) → E) x) = (↑((f : (a : A) → { x : X // x ∈ s }) x) : X)
hF_unique :
  { toFun := fun (a : A) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ p ⁻¹' s) ((F' : (a : A) → E) a) ⋯,
      continuous_toFun := ⋯ } =
    F
a : A
⊢ Eq.{u_1 + 1} (α := E) ((F' : (a : A) → E) a : E)
    ((ContinuousMap.comp
            { toFun := Subtype.val (p := fun (x : E) ↦ x ∈ p ⁻¹' s), continuous_toFun := ⋯ :
              C({ x : E // x ∈ p ⁻¹' s }, E) }
            F :
          (a : A) → E)
        a :
      E)

Tactic:
simp [← hF_unique]
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
p : X → ι → Prop
s : X → ι → Set X
h : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h' : ∀ (x : X) (i : ι), p x i → ContractibleSpace.{u_1} (↑(s x i) : Type u_1)
x : X
rw : ∀ t ∈ 𝓝 x, ∃ r ∈ 𝓝 x, ContractibleSpace.{u_1} (↑r : Type u_1) ∧ r ⊆ t
⊢ (𝓝 x).HasBasis (fun (s : Set X) ↦ s ∈ 𝓝 x ∧ ContractibleSpace.{u_1} (↑s : Type u_1)) id

Tactic:
rw [hasBasis_self]

Premises used: Filter.hasBasis_self
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
p : X → ι → Prop
s : X → ι → Set X
h : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h' : ∀ (x : X) (i : ι), p x i → ContractibleSpace.{u_1} (↑(s x i) : Type u_1)
x : X
t : Set X
ht : t ∈ 𝓝 x
obtain : ∀ (i : ι) (hpi : p x i) (hi : s x i ⊆ t), ∃ r ∈ 𝓝 x, ContractibleSpace.{u_1} (↑r : Type u_1) ∧ r ⊆ t
⊢ ∃ r ∈ 𝓝 x, ContractibleSpace.{u_1} (↑r : Type u_1) ∧ r ⊆ t

Tactic:
obtain ⟨i, hpi, hi⟩ := (h x).mem_iff.mp ht

Premises used: Filter.HasBasis.mem_iff, Iff.mp
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
p : X → ι → Prop
s : X → ι → Set X
h : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h' : ∀ (x : X) (i : ι), p x i → ContractibleSpace.{u_1} (↑(s x i) : Type u_1)
x : X
t : Set X
ht : t ∈ 𝓝 x
i : ι
hpi : p x i
hi : s x i ⊆ t
⊢ ∃ r ∈ 𝓝 x, ContractibleSpace.{u_1} (↑r : Type u_1) ∧ r ⊆ t

Tactic:
⟨s x i, (h x).mem_of_mem hpi, h' x i hpi, hi⟩

Premises used: And.intro, Exists.intro, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
p : X → ι → Prop
s : X → ι → Set X
h : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h' : ∀ (x : X) (i : ι), p x i → ContractibleSpace.{u_1} (↑(s x i) : Type u_1)
x : X
t : Set X
ht : t ∈ 𝓝 x
i : ι
hpi : p x i
hi : s x i ⊆ t
⊢ ∃ r ∈ 𝓝 x, ContractibleSpace.{u_1} (↑r : Type u_1) ∧ r ⊆ t

Tactic:
exact ⟨s x i, (h x).mem_of_mem hpi, h' x i hpi, hi⟩
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
inst_1 : StronglyLocallyContractibleSpace X
U : Set X
h : IsOpen[inst] U
hx : x ∈ U
⊢ (𝓝 x).HasBasis (fun (s : Set X) ↦ s ∈ 𝓝 x ∧ ContractibleSpace.{u_1} (↑s : Type u_1) ∧ s ⊆ U) id

Tactic:
(contractible_basis x).hasBasis_self_subset (IsOpen.mem_nhds h hx)

Premises used: StronglyLocallyContractibleSpace.contractible_basis, IsOpen.mem_nhds, Filter.HasBasis.hasBasis_self_subset
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y : X
ι : Type u_3
inst_2 : StronglyLocallyContractibleSpace X
x : X
⊢ (𝓝 x).HasBasis (fun (s : Set X) ↦ s ∈ 𝓝 x ∧ IsPathConnected s) id

Tactic:
contractible_basis x |>.to_hasBasis'
      (fun s ⟨hs, hs'⟩ ↦ ⟨s, ⟨hs, ?_⟩, le_rfl⟩) (fun s hs ↦ hs.1)

Premises used: IsPathConnected, le_rfl, StronglyLocallyContractibleSpace.contractible_basis, _private.0.instLocPathConnectedSpace.match_1, Membership.mem, Exists, nhds, id, HasSubset.Subset, And, And.left, And.intro, Exists.intro, Filter.HasBasis.to_hasBasis'
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y : X
ι : Type u_3
inst_2 : StronglyLocallyContractibleSpace X
x : X
refine :
  ∀ (s : Set X),
    s ∈ 𝓝 x ∧ ContractibleSpace.{u_1} (↑s : Type u_1) →
      ∀ (hs : s ∈ 𝓝 x) (hs' : ContractibleSpace.{u_1} (↑s : Type u_1)), IsPathConnected s
⊢ (𝓝 x).HasBasis (fun (s : Set X) ↦ s ∈ 𝓝 x ∧ IsPathConnected s) id

Tactic:
refine contractible_basis x |>.to_hasBasis'
      (fun s ⟨hs, hs'⟩ ↦ ⟨s, ⟨hs, ?_⟩, le_rfl⟩) (fun s hs ↦ hs.1)

Premises used: le_rfl, StronglyLocallyContractibleSpace.contractible_basis, _private.0.instLocPathConnectedSpace.match_1, Exists, id, HasSubset.Subset, And, And.intro, Exists.intro, Filter.HasBasis.to_hasBasis'
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y : X
ι : Type u_3
inst_2 : StronglyLocallyContractibleSpace X
x : X
s : Set X
h : s ∈ 𝓝 x ∧ ContractibleSpace.{u_1} (↑s : Type u_1)
hs : s ∈ 𝓝 x
hs' : ContractibleSpace.{u_1} (↑s : Type u_1)
rw : PathConnectedSpace.{u_1} (↑s : Type u_1)
⊢ IsPathConnected s

Tactic:
rw [isPathConnected_iff_pathConnectedSpace]

Premises used: isPathConnected_iff_pathConnectedSpace
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y : X
ι : Type u_3
inst_2 : StronglyLocallyContractibleSpace X
x : X
s : Set X
h : s ∈ 𝓝 x ∧ ContractibleSpace.{u_1} (↑s : Type u_1)
hs : s ∈ 𝓝 x
hs' : ContractibleSpace.{u_1} (↑s : Type u_1)
⊢ PathConnectedSpace.{u_1} (↑s : Type u_1)

Tactic:
infer_instance
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : StronglyLocallyContractibleSpace X
e : Y → X
he : IsOpenEmbedding e
⊢ StronglyLocallyContractibleSpace Y

Tactic:
.of_bases
    (fun _ ↦ he.basis_nhds <| contractible_subset_basis he.isOpen_range (mem_range_self _))
    fun _ _ ⟨_, hs, hse⟩ ↦
      (he.toIsEmbedding.homeomorphOfSubsetRange hse).contractibleSpace_iff.mpr hs

Premises used: Set.mem_range_self, Iff.mpr, Topology.IsOpenEmbedding.toIsEmbedding, Homeomorph.contractibleSpace_iff, contractible_subset_basis, Topology.IsInducing.basis_nhds, _private.0.Topology.IsOpenEmbedding.stronglyLocallyContractibleSpace.match_1, Function.comp, Set.Elem, id, ContractibleSpace, Topology.IsOpenEmbedding.isOpen_range, Set.preimage, StronglyLocallyContractibleSpace.of_bases, Topology.IsEmbedding.toIsInducing, Topology.IsEmbedding.homeomorphOfSubsetRange
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : StronglyLocallyContractibleSpace X
U : Set X
h : IsOpen[inst] U
⊢ StronglyLocallyContractibleSpace.{u_1} (↑U : Type u_1)

Tactic:
h.isOpenEmbedding_subtypeVal.stronglyLocallyContractibleSpace

Premises used: IsOpen.isOpenEmbedding_subtypeVal, Topology.IsOpenEmbedding.stronglyLocallyContractibleSpace
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
ι : Type u_3
inst_2 : StronglyLocallyContractibleSpace X
inst_3 : StronglyLocallyContractibleSpace Y
⊢ StronglyLocallyContractibleSpace (X × Y)

Tactic:
.of_bases (ι := Set X × Set Y)
    (p := fun (x, y) (Ux, Uy) =>
      (Ux ∈ 𝓝 x ∧ ContractibleSpace Ux) ∧ (Uy ∈ 𝓝 y ∧ ContractibleSpace Uy))
    (s := fun _ (Ux, Uy) => Ux ×ˢ Uy) ?_ ?_

Premises used: StronglyLocallyContractibleSpace.of_bases