awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C((↑I : Type), X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : (↑I : Type) → C((↑I : Type), E)
Γ_lifts : ∀ (t s : (↑I : Type)), p ((Γ t : (a : (↑I : Type)) → E) s) = (γ : (a : (↑I : Type) × (↑I : Type)) → X) (t, s)
Γ_0 : ∀ (t : (↑I : Type)), Eq (α := E) ((Γ t : (a : (↑I : Type)) → E) 0 : E) ((Γ 0 : (a : (↑I : Type)) → E) 0 : E)
t : (↑I : Type)
⊢ Eq (α := (↑I : Type) × (↑I : Type) → X)
    (p ∘ fun (st : (↑I : Type) × (↑I : Type)) ↦ (Γ st.2 : (a : (↑I : Type)) → E) st.1)
    (⇑(ContinuousMap.comp (↑γ : C((↑I : Type) × (↑I : Type), X)) ContinuousMap.prodSwap) :
      (a : (↑I : Type) × (↑I : Type)) → X)
have refine_1 : ∀ (x : (↑I : Type) × (↑I : Type)),
  (p ∘ fun (st : (↑I : Type) × (↑I : Type)) ↦ (Γ st.2 : (a : (↑I : Type)) → E) st.1) x =
    (ContinuousMap.comp (↑γ : C((↑I : Type) × (↑I : Type), X)) ContinuousMap.prodSwap :
        (a : (↑I : Type) × (↑I : Type)) → X)
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C((↑I : Type), X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : (↑I : Type) → C((↑I : Type), E)
Γ_lifts : ∀ (t s : (↑I : Type)), p ((Γ t : (a : (↑I : Type)) → E) s) = (γ : (a : (↑I : Type) × (↑I : Type)) → X) (t, s)
Γ_0 : ∀ (t : (↑I : Type)), Eq (α := E) ((Γ t : (a : (↑I : Type)) → E) 0 : E) ((Γ 0 : (a : (↑I : Type)) → E) 0 : E)
t : (↑I : Type)
⊢ Continuous[_, inst] fun (x : (↑I : Type)) ↦
    (fun (st : (↑I : Type) × (↑I : Type)) ↦ ((Γ st.2 : (a : (↑I : Type)) → E) st.1 : E)) (0, x)
have refine_2 : Continuous[_, inst] fun (x : (↑I : Type)) ↦ (Γ 0 : (a : (↑I : Type)) → E) 0
Tactic: simp_rw [Γ_0]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
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
homeo : IsLocalHomeomorph p
inst_3 : PathConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = (f : (a : A) → X) a₀
ex :
  ∀ (γ : C((↑I : Type), A)),
    (γ : (a : (↑I : Type)) → A) 0 = a₀ →
      ∃ (Γ : C((↑I : Type), E)),
        (Γ : (a : (↑I : Type)) → E) 0 = e₀ ∧
          Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)
uniq :
  ∀ (γ γ' : C((↑I : Type), A)) (Γ Γ' : C((↑I : Type), E)),
    (γ : (a : (↑I : Type)) → A) 0 = a₀ →
      (γ' : (a : (↑I : Type)) → A) 0 = a₀ →
        (Γ : (a : (↑I : Type)) → E) 0 = e₀ →
          (Γ' : (a : (↑I : Type)) → E) 0 = e₀ →
            Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X) →
              Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ' : (a : (↑I : Type)) → E)) (⇑(f.comp γ') : (a : (↑I : Type)) → X) →
                Eq (α := A) ((γ : (a : (↑I : Type)) → A) 1 : A) ((γ' : (a : (↑I : Type)) → A) 1 : A) →
                  Eq (α := E) ((Γ : (a : (↑I : Type)) → E) 1 : E) ((Γ' : (a : (↑I : Type)) → E) 1 : E)
⊢ ∃! F : C(A, E), (F : (a : A) → E) a₀ = e₀ ∧ Eq (α := A → X) (p ∘ (⇑F : (a : A) → E)) (⇑f : (a : A) → X)
have choose : ∀ (Γ : (γ : C((↑I : Type), A)) → (γ : (a : (↑I : Type)) → A) 0 = a₀ → C((↑I : Type), E))
  (Γ_0 : ∀ (γ : C((↑I : Type), A)) (a : (γ : (a : (↑I : Type)) → A) 0 = a₀), (Γ γ a : (a : (↑I : Type)) → E) 0 = e₀)
  (Γ_lifts :
    ∀ (γ : C((↑I : Type), A)) (a : (γ : (a : (↑I : Type)) → A) 0 = a₀),
      Eq (α := (↑I : Type) → X) (p ∘ (⇑(Γ γ a) : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)),
  ∃! F : C(A, E), (F : (a : A) → E) a₀ = e₀ ∧ Eq (α := A → X) (p ∘ (⇑F : (a : A) → E)) (⇑f : (a : A) → X)
Tactic: choose Γ Γ_0 Γ_lifts using ex
Cleared hypotheses: ex
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (hypothesis)
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
homeo : IsLocalHomeomorph p
inst_3 : PathConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = (f : (a : A) → X) a₀
uniq :
  ∀ (γ γ' : C((↑I : Type), A)) (Γ Γ' : C((↑I : Type), E)),
    (γ : (a : (↑I : Type)) → A) 0 = a₀ →
      (γ' : (a : (↑I : Type)) → A) 0 = a₀ →
        (Γ : (a : (↑I : Type)) → E) 0 = e₀ →
          (Γ' : (a : (↑I : Type)) → E) 0 = e₀ →
            Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X) →
              Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ' : (a : (↑I : Type)) → E)) (⇑(f.comp γ') : (a : (↑I : Type)) → X) →
                Eq (α := A) ((γ : (a : (↑I : Type)) → A) 1 : A) ((γ' : (a : (↑I : Type)) → A) 1 : A) →
                  Eq (α := E) ((Γ : (a : (↑I : Type)) → E) 1 : E) ((Γ' : (a : (↑I : Type)) → E) 1 : E)
Γ : (γ : C((↑I : Type), A)) → (γ : (a : (↑I : Type)) → A) 0 = a₀ → C((↑I : Type), E)
Γ_0 : ∀ (γ : C((↑I : Type), A)) (a : (γ : (a : (↑I : Type)) → A) 0 = a₀), (Γ γ a : (a : (↑I : Type)) → E) 0 = e₀
Γ_lifts :
  ∀ (γ : C((↑I : Type), A)) (a : (γ : (a : (↑I : Type)) → A) 0 = a₀),
    Eq (α := (↑I : Type) → X) (p ∘ (⇑(Γ γ a) : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)
F : (a : A) → E := fun (a : A) ↦ (Γ (Path.toContinuousMap (somePath a₀ a)) ⋯ : (a : (↑I : Type)) → E) 1
⊢ ∃! F : C(A, E), (F : (a : A) → E) a₀ = e₀ ∧ Eq (α := A → X) (p ∘ (⇑F : (a : A) → E)) (⇑f : (a : A) → X)
have this : ∀ (a : A), p (F a) = (f : (a : A) → X) a
Tactic: have (a : A) : p (F a) = f a := by simpa using congr_fun (Γ_lifts _ (Path.source _)) 1
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
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
homeo : IsLocalHomeomorph p
inst_3 : PathConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = (f : (a : A) → X) a₀
uniq :
  ∀ (γ γ' : C((↑I : Type), A)) (Γ Γ' : C((↑I : Type), E)),
    (γ : (a : (↑I : Type)) → A) 0 = a₀ →
      (γ' : (a : (↑I : Type)) → A) 0 = a₀ →
        (Γ : (a : (↑I : Type)) → E) 0 = e₀ →
          (Γ' : (a : (↑I : Type)) → E) 0 = e₀ →
            Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X) →
              Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ' : (a : (↑I : Type)) → E)) (⇑(f.comp γ') : (a : (↑I : Type)) → X) →
                Eq (α := A) ((γ : (a : (↑I : Type)) → A) 1 : A) ((γ' : (a : (↑I : Type)) → A) 1 : A) →
                  Eq (α := E) ((Γ : (a : (↑I : Type)) → E) 1 : E) ((Γ' : (a : (↑I : Type)) → E) 1 : E)
Γ : (γ : C((↑I : Type), A)) → (γ : (a : (↑I : Type)) → A) 0 = a₀ → C((↑I : Type), E)
Γ_0 : ∀ (γ : C((↑I : Type), A)) (a : (γ : (a : (↑I : Type)) → A) 0 = a₀), (Γ γ a : (a : (↑I : Type)) → E) 0 = e₀
Γ_lifts :
  ∀ (γ : C((↑I : Type), A)) (a : (γ : (a : (↑I : Type)) → A) 0 = a₀),
    Eq (α := (↑I : Type) → X) (p ∘ (⇑(Γ γ a) : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)
F : (a : A) → E := fun (a : A) ↦ (Γ (Path.toContinuousMap (somePath a₀ a)) ⋯ : (a : (↑I : Type)) → E) 1
this : ∀ (a : A), p (F a) = (f : (a : A) → X) a
⊢ ∃! F : C(A, E), (F : (a : A) → E) a₀ = e₀ ∧ Eq (α := A → X) (p ∘ (⇑F : (a : A) → E)) (⇑f : (a : A) → X)
have refine_1 : ∀ (a : A), ContinuousAt F a
Tactic: refine ⟨⟨F, continuous_iff_continuousAt.mpr fun a ↦ ?_⟩, ⟨?_, funext this⟩, fun F' ⟨F'_0, hpF'⟩ ↦
    DFunLike.ext _ _ fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
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
homeo : IsLocalHomeomorph p
inst_3 : PathConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = (f : (a : A) → X) a₀
uniq :
  ∀ (γ γ' : C((↑I : Type), A)) (Γ Γ' : C((↑I : Type), E)),
    (γ : (a : (↑I : Type)) → A) 0 = a₀ →
      (γ' : (a : (↑I : Type)) → A) 0 = a₀ →
        (Γ : (a : (↑I : Type)) → E) 0 = e₀ →
          (Γ' : (a : (↑I : Type)) → E) 0 = e₀ →
            Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X) →
              Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ' : (a : (↑I : Type)) → E)) (⇑(f.comp γ') : (a : (↑I : Type)) → X) →
                Eq (α := A) ((γ : (a : (↑I : Type)) → A) 1 : A) ((γ' : (a : (↑I : Type)) → A) 1 : A) →
                  Eq (α := E) ((Γ : (a : (↑I : Type)) → E) 1 : E) ((Γ' : (a : (↑I : Type)) → E) 1 : E)
Γ : (γ : C((↑I : Type), A)) → (γ : (a : (↑I : Type)) → A) 0 = a₀ → C((↑I : Type), E)
Γ_0 : ∀ (γ : C((↑I : Type), A)) (a : (γ : (a : (↑I : Type)) → A) 0 = a₀), (Γ γ a : (a : (↑I : Type)) → E) 0 = e₀
Γ_lifts :
  ∀ (γ : C((↑I : Type), A)) (a : (γ : (a : (↑I : Type)) → A) 0 = a₀),
    Eq (α := (↑I : Type) → X) (p ∘ (⇑(Γ γ a) : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)
F : (a : A) → E := fun (a : A) ↦ (Γ (Path.toContinuousMap (somePath a₀ a)) ⋯ : (a : (↑I : Type)) → E) 1
this : ∀ (a : A), p (F a) = (f : (a : A) → X) a
refine_1 : ∀ (a : A), ContinuousAt F a
⊢ ∃! F : C(A, E), (F : (a : A) → E) a₀ = e₀ ∧ Eq (α := A → X) (p ∘ (⇑F : (a : A) → E)) (⇑f : (a : A) → X)
have refine_2 : ({ toFun := F, continuous_toFun := sorry } : (a : A) → E) a₀ = e₀
Tactic: refine ⟨⟨F, continuous_iff_continuousAt.mpr fun a ↦ ?_⟩, ⟨?_, funext this⟩, fun F' ⟨F'_0, hpF'⟩ ↦
    DFunLike.ext _ _ fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
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
homeo : IsLocalHomeomorph p
inst_3 : PathConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = (f : (a : A) → X) a₀
uniq :
  ∀ (γ γ' : C((↑I : Type), A)) (Γ Γ' : C((↑I : Type), E)),
    (γ : (a : (↑I : Type)) → A) 0 = a₀ →
      (γ' : (a : (↑I : Type)) → A) 0 = a₀ →
        (Γ : (a : (↑I : Type)) → E) 0 = e₀ →
          (Γ' : (a : (↑I : Type)) → E) 0 = e₀ →
            Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X) →
              Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ' : (a : (↑I : Type)) → E)) (⇑(f.comp γ') : (a : (↑I : Type)) → X) →
                Eq (α := A) ((γ : (a : (↑I : Type)) → A) 1 : A) ((γ' : (a : (↑I : Type)) → A) 1 : A) →
                  Eq (α := E) ((Γ : (a : (↑I : Type)) → E) 1 : E) ((Γ' : (a : (↑I : Type)) → E) 1 : E)
Γ : (γ : C((↑I : Type), A)) → (γ : (a : (↑I : Type)) → A) 0 = a₀ → C((↑I : Type), E)
Γ_0 : ∀ (γ : C((↑I : Type), A)) (a : (γ : (a : (↑I : Type)) → A) 0 = a₀), (Γ γ a : (a : (↑I : Type)) → E) 0 = e₀
Γ_lifts :
  ∀ (γ : C((↑I : Type), A)) (a : (γ : (a : (↑I : Type)) → A) 0 = a₀),
    Eq (α := (↑I : Type) → X) (p ∘ (⇑(Γ γ a) : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)
F : (a : A) → E := fun (a : A) ↦ (Γ (Path.toContinuousMap (somePath a₀ a)) ⋯ : (a : (↑I : Type)) → E) 1
this : ∀ (a : A), p (F a) = (f : (a : A) → X) a
refine_1 : ∀ (a : A), ContinuousAt F a
refine_2 : ({ toFun := F, continuous_toFun := ⋯ } : (a : A) → E) a₀ = e₀
⊢ ∃! F : C(A, E), (F : (a : A) → E) a₀ = e₀ ∧ Eq (α := A → X) (p ∘ (⇑F : (a : A) → E)) (⇑f : (a : A) → X)
have refine_3 : ∀ (F' : C(A, E)),
  (fun (F : C(A, E)) ↦ (F : (a : A) → E) a₀ = e₀ ∧ Eq (α := A → X) (p ∘ (⇑F : (a : A) → E)) (⇑f : (a : A) → X)) F' →
    ∀ (F'_0 : (F' : (a : A) → E) a₀ = e₀) (hpF' : Eq (α := A → X) (p ∘ (⇑F' : (a : A) → E)) (⇑f : (a : A) → X)) (a : A),
      Eq.{u_1 + 1} (α := E) ((F' : (a : A) → E) a : E) (({ toFun := F, continuous_toFun := sorry } : (a : A) → E) a : E)
Tactic: refine ⟨⟨F, continuous_iff_continuousAt.mpr fun a ↦ ?_⟩, ⟨?_, funext this⟩, fun F' ⟨F'_0, hpF'⟩ ↦
    DFunLike.ext _ _ fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
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
homeo : IsLocalHomeomorph p
inst_3 : PathConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = (f : (a : A) → X) a₀
uniq :
  ∀ (γ γ' : C((↑I : Type), A)) (Γ Γ' : C((↑I : Type), E)),
    (γ : (a : (↑I : Type)) → A) 0 = a₀ →
      (γ' : (a : (↑I : Type)) → A) 0 = a₀ →
        (Γ : (a : (↑I : Type)) → E) 0 = e₀ →
          (Γ' : (a : (↑I : Type)) → E) 0 = e₀ →
            Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X) →
              Eq (α := (↑I : Type) → X) (p ∘ (⇑Γ' : (a : (↑I : Type)) → E)) (⇑(f.comp γ') : (a : (↑I : Type)) → X) →
                Eq (α := A) ((γ : (a : (↑I : Type)) → A) 1 : A) ((γ' : (a : (↑I : Type)) → A) 1 : A) →
                  Eq (α := E) ((Γ : (a : (↑I : Type)) → E) 1 : E) ((Γ' : (a : (↑I : Type)) → E) 1 : E)
Γ : (γ : C((↑I : Type), A)) → (γ : (a : (↑I : Type)) → A) 0 = a₀ → C((↑I : Type), E)
Γ_0 : ∀ (γ : C((↑I : Type), A)) (a : (γ : (a : (↑I : Type)) → A) 0 = a₀), (Γ γ a : (a : (↑I : Type)) → E) 0 = e₀
Γ_lifts :
  ∀ (γ : C((↑I : Type), A)) (a : (γ : (a : (↑I : Type)) → A) 0 = a₀),
    Eq (α := (↑I : Type) → X) (p ∘ (⇑(Γ γ a) : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)
F : (a : A) → E := fun (a : A) ↦ (Γ (Path.toContinuousMap (somePath a₀ a)) ⋯ : (a : (↑I : Type)) → E) 1
this : ∀ (a : A), p (F a) = (f : (a : A) → X) a
a : A
⊢ ContinuousAt F a
have refine_1 : ∀ (p : OpenPartialHomeomorph E X) (hep : F a ∈ p.source) (homeo : IsLocalHomeomorph (↑p : E → X))
  (he : (↑p : E → X) e₀ = (f : (a : A) → X) a₀)
  (uniq :
    ∀ (γ γ' : C((↑I : Type), A)) (Γ Γ' : C((↑I : Type), E)),
      (γ : (a : (↑I : Type)) → A) 0 = a₀ →
        (γ' : (a : (↑I : Type)) → A) 0 = a₀ →
          (Γ : (a : (↑I : Type)) → E) 0 = e₀ →
            (Γ' : (a : (↑I : Type)) → E) 0 = e₀ →
              Eq (α := (↑I : Type) → X) ((↑p : E → X) ∘ (⇑Γ : (a : (↑I : Type)) → E))
                  (⇑(f.comp γ) : (a : (↑I : Type)) → X) →
                Eq (α := (↑I : Type) → X) ((↑p : E → X) ∘ (⇑Γ' : (a : (↑I : Type)) → E))
                    (⇑(f.comp γ') : (a : (↑I : Type)) → X) →
                  Eq (α := A) ((γ : (a : (↑I : Type)) → A) 1 : A) ((γ' : (a : (↑I : Type)) → A) 1 : A) →
                    Eq (α := E) ((Γ : (a : (↑I : Type)) → E) 1 : E) ((Γ' : (a : (↑I : Type)) → E) 1 : E))
  (Γ_lifts :
    ∀ (γ : C((↑I : Type), A)) (a : (γ : (a : (↑I : Type)) → A) 0 = a₀),
      Eq (α := (↑I : Type) → X) ((↑p : E → X) ∘ (⇑(Γ γ a) : (a : (↑I : Type)) → E))
        (⇑(f.comp γ) : (a : (↑I : Type)) → X))
  (this : ∀ (a : A), (↑p : E → X) (F a) = (f : (a : A) → X) a), ContinuousAt F a
Tactic: obtain ⟨p, hep, rfl⟩ := homeo (F a)
Cleared hypotheses: p, homeo, he, uniq, Γ_lifts, this
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
inst_3 : PathConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
Γ : (γ : C((↑I : Type), A)) → (γ : (a : (↑I : Type)) → A) 0 = a₀ → C((↑I : Type), E)
Γ_0 : ∀ (γ : C((↑I : Type), A)) (a : (γ : (a : (↑I : Type)) → A) 0 = a₀), (Γ γ a : (a : (↑I : Type)) → E) 0 = e₀
F : (a : A) → E := fun (a : A) ↦ (Γ (Path.toContinuousMap (somePath a₀ a)) ⋯ : (a : (↑I : Type)) → E) 1
a : A
p : OpenPartialHomeomorph E X
hep : F a ∈ p.source
homeo : IsLocalHomeomorph (↑p : E → X)
he : (↑p : E → X) e₀ = (f : (a : A) → X) a₀
uniq :
  ∀ (γ γ' : C((↑I : Type), A)) (Γ Γ' : C((↑I : Type), E)),
    (γ : (a : (↑I : Type)) → A) 0 = a₀ →
      (γ' : (a : (↑I : Type)) → A) 0 = a₀ →
        (Γ : (a : (↑I : Type)) → E) 0 = e₀ →
          (Γ' : (a : (↑I : Type)) → E) 0 = e₀ →
            Eq (α := (↑I : Type) → X) ((↑p : E → X) ∘ (⇑Γ : (a : (↑I : Type)) → E))
                (⇑(f.comp γ) : (a : (↑I : Type)) → X) →
              Eq (α := (↑I : Type) → X) ((↑p : E → X) ∘ (⇑Γ' : (a : (↑I : Type)) → E))
                  (⇑(f.comp γ') : (a : (↑I : Type)) → X) →
                Eq (α := A) ((γ : (a : (↑I : Type)) → A) 1 : A) ((γ' : (a : (↑I : Type)) → A) 1 : A) →
                  Eq (α := E) ((Γ : (a : (↑I : Type)) → E) 1 : E) ((Γ' : (a : (↑I : Type)) → E) 1 : E)
Γ_lifts :
  ∀ (γ : C((↑I : Type), A)) (a : (γ : (a : (↑I : Type)) → A) 0 = a₀),
    Eq (α := (↑I : Type) → X) ((↑p : E → X) ∘ (⇑(Γ γ a) : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)
this : ∀ (a : A), (↑p : E → X) (F a) = (f : (a : A) → X) a
⊢ Membership.mem (α := X) p.target ((f : (a : A) → X) a : X)
have rw : (↑p : E → X) (F a) ∈ p.target
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (hypothesis)
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
inst_3 : PathConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
Γ : (γ : C((↑I : Type), A)) → (γ : (a : (↑I : Type)) → A) 0 = a₀ → C((↑I : Type), E)
Γ_0 : ∀ (γ : C((↑I : Type), A)) (a : (γ : (a : (↑I : Type)) → A) 0 = a₀), (Γ γ a : (a : (↑I : Type)) → E) 0 = e₀
F : (a : A) → E := fun (a : A) ↦ (Γ (Path.toContinuousMap (somePath a₀ a)) ⋯ : (a : (↑I : Type)) → E) 1
a : A
p : OpenPartialHomeomorph E X
hep : F a ∈ p.source
homeo : IsLocalHomeomorph (↑p : E → X)
he : (↑p : E → X) e₀ = (f : (a : A) → X) a₀
uniq :
  ∀ (γ γ' : C((↑I : Type), A)) (Γ Γ' : C((↑I : Type), E)),
    (γ : (a : (↑I : Type)) → A) 0 = a₀ →
      (γ' : (a : (↑I : Type)) → A) 0 = a₀ →
        (Γ : (a : (↑I : Type)) → E) 0 = e₀ →
          (Γ' : (a : (↑I : Type)) → E) 0 = e₀ →
            Eq (α := (↑I : Type) → X) ((↑p : E → X) ∘ (⇑Γ : (a : (↑I : Type)) → E))
                (⇑(f.comp γ) : (a : (↑I : Type)) → X) →
              Eq (α := (↑I : Type) → X) ((↑p : E → X) ∘ (⇑Γ' : (a : (↑I : Type)) → E))
                  (⇑(f.comp γ') : (a : (↑I : Type)) → X) →
                Eq (α := A) ((γ : (a : (↑I : Type)) → A) 1 : A) ((γ' : (a : (↑I : Type)) → A) 1 : A) →
                  Eq (α := E) ((Γ : (a : (↑I : Type)) → E) 1 : E) ((Γ' : (a : (↑I : Type)) → E) 1 : E)
Γ_lifts :
  ∀ (γ : C((↑I : Type), A)) (a : (γ : (a : (↑I : Type)) → A) 0 = a₀),
    Eq (α := (↑I : Type) → X) ((↑p : E → X) ∘ (⇑(Γ γ a) : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)
this : ∀ (a : A), (↑p : E → X) (F a) = (f : (a : A) → X) a
⊢ ContinuousAt F a
have hfap : Membership.mem (α := X) p.target ((f : (a : A) → X) a : X)
Tactic: have hfap : f a ∈ p.target := by rw [← this]; exact p.map_source hep
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
inst_3 : PathConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
Γ : (γ : C((↑I : Type), A)) → (γ : (a : (↑I : Type)) → A) 0 = a₀ → C((↑I : Type), E)
Γ_0 : ∀ (γ : C((↑I : Type), A)) (a : (γ : (a : (↑I : Type)) → A) 0 = a₀), (Γ γ a : (a : (↑I : Type)) → E) 0 = e₀
F : (a : A) → E := fun (a : A) ↦ (Γ (Path.toContinuousMap (somePath a₀ a)) ⋯ : (a : (↑I : Type)) → E) 1
a : A
p : OpenPartialHomeomorph E X
hep : F a ∈ p.source
homeo : IsLocalHomeomorph (↑p : E → X)
he : (↑p : E → X) e₀ = (f : (a : A) → X) a₀
uniq :
  ∀ (γ γ' : C((↑I : Type), A)) (Γ Γ' : C((↑I : Type), E)),
    (γ : (a : (↑I : Type)) → A) 0 = a₀ →
      (γ' : (a : (↑I : Type)) → A) 0 = a₀ →
        (Γ : (a : (↑I : Type)) → E) 0 = e₀ →
          (Γ' : (a : (↑I : Type)) → E) 0 = e₀ →
            Eq (α := (↑I : Type) → X) ((↑p : E → X) ∘ (⇑Γ : (a : (↑I : Type)) → E))
                (⇑(f.comp γ) : (a : (↑I : Type)) → X) →
              Eq (α := (↑I : Type) → X) ((↑p : E → X) ∘ (⇑Γ' : (a : (↑I : Type)) → E))
                  (⇑(f.comp γ') : (a : (↑I : Type)) → X) →
                Eq (α := A) ((γ : (a : (↑I : Type)) → A) 1 : A) ((γ' : (a : (↑I : Type)) → A) 1 : A) →
                  Eq (α := E) ((Γ : (a : (↑I : Type)) → E) 1 : E) ((Γ' : (a : (↑I : Type)) → E) 1 : E)
Γ_lifts :
  ∀ (γ : C((↑I : Type), A)) (a : (γ : (a : (↑I : Type)) → A) 0 = a₀),
    Eq (α := (↑I : Type) → X) ((↑p : E → X) ∘ (⇑(Γ γ a) : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)
this : ∀ (a : A), (↑p : E → X) (F a) = (f : (a : A) → X) a
hfap : Membership.mem (α := X) p.target ((f : (a : A) → X) a : X)
⊢ ContinuousAt F a
have refine_1 : (↑p.symm : X → E) ∘ (⇑f : (a : A) → X) =ᶠ[𝓝 a] F
Tactic: refine ContinuousAt.congr (f := p.symm ∘ f)
      ((p.continuousAt_symm hfap).comp f.2.continuousAt) ?_
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (goal)
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
inst_3 : PathConnectedSpace A
inst_4 : LocPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
Γ : (γ : C((↑I : Type), A)) → (γ : (a : (↑I : Type)) → A) 0 = a₀ → C((↑I : Type), E)
Γ_0 : ∀ (γ : C((↑I : Type), A)) (a : (γ : (a : (↑I : Type)) → A) 0 = a₀), (Γ γ a : (a : (↑I : Type)) → E) 0 = e₀
F : (a : A) → E := fun (a : A) ↦ (Γ (Path.toContinuousMap (somePath a₀ a)) ⋯ : (a : (↑I : Type)) → E) 1
a : A
p : OpenPartialHomeomorph E X
hep : F a ∈ p.source
homeo : IsLocalHomeomorph (↑p : E → X)
he : (↑p : E → X) e₀ = (f : (a : A) → X) a₀
uniq :
  ∀ (γ γ' : C((↑I : Type), A)) (Γ Γ' : C((↑I : Type), E)),
    (γ : (a : (↑I : Type)) → A) 0 = a₀ →
      (γ' : (a : (↑I : Type)) → A) 0 = a₀ →
        (Γ : (a : (↑I : Type)) → E) 0 = e₀ →
          (Γ' : (a : (↑I : Type)) → E) 0 = e₀ →
            Eq (α := (↑I : Type) → X) ((↑p : E → X) ∘ (⇑Γ : (a : (↑I : Type)) → E))
                (⇑(f.comp γ) : (a : (↑I : Type)) → X) →
              Eq (α := (↑I : Type) → X) ((↑p : E → X) ∘ (⇑Γ' : (a : (↑I : Type)) → E))
                  (⇑(f.comp γ') : (a : (↑I : Type)) → X) →
                Eq (α := A) ((γ : (a : (↑I : Type)) → A) 1 : A) ((γ' : (a : (↑I : Type)) → A) 1 : A) →
                  Eq (α := E) ((Γ : (a : (↑I : Type)) → E) 1 : E) ((Γ' : (a : (↑I : Type)) → E) 1 : E)
Γ_lifts :
  ∀ (γ : C((↑I : Type), A)) (a : (γ : (a : (↑I : Type)) → A) 0 = a₀),
    Eq (α := (↑I : Type) → X) ((↑p : E → X) ∘ (⇑(Γ γ a) : (a : (↑I : Type)) → E)) (⇑(f.comp γ) : (a : (↑I : Type)) → X)
this : ∀ (a : A), (↑p : E → X) (F a) = (f : (a : A) → X) a
hfap : Membership.mem (α := X) p.target ((f : (a : A) → X) a : X)
⊢ (↑p.symm : X → E) ∘ (⇑f : (a : A) → X) =ᶠ[𝓝 a] F
have refine_1 : ∀ (U : Set A) (haU : U ∈ 𝓝 a) (U_conn : IsPathConnected U) (hUp : id U ⊆ (⇑f : (a : A) → X) ⁻¹' p.target),
  (↑p.symm : X → E) ∘ (⇑f : (a : A) → X) =ᶠ[𝓝 a] F
Tactic: have ⟨U, ⟨haU, U_conn⟩, hUp⟩ := (path_connected_basis a).mem_iff.mp
      ((p.open_target.preimage f.continuous).mem_nhds hfap)