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
f : ContinuousMap.{u_3, u_2} ((↑I : Type) × A) X
g : (↑I : Type) × A → E
g_lifts : p ∘ g = (⇑f : (a : (↑I : Type) × A) → X)
cont_0 : Continuous[inst_2, inst] fun (x : A) ↦ g (0, x)
a : A
cont_a : Continuous[_, inst] fun (x : (↑I : Type)) ↦ g (x, a)
q : (x : E) → OpenPartialHomeomorph E X
mem_source : ∀ (x : E), x ∈ (q x).source
hpq : ∀ (x : E), p = (↑(q x) : E → X)
t : ℕ → (↑I : Type)
t_0 : t 0 = 0
t_mono : Monotone t
t_sub : ∀ (n : ℕ), ∃ (i : E), Set.Icc (t n) (t (n + 1)) ⊆ (fun (x : (↑I : Type)) ↦ g (x, a)) ⁻¹' (q i).source
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
h :
  ∃ (N : Set A),
    a ∈ N ∧
      IsOpen[inst_2] N ∧
        ∃ (g' : (↑I : Type) × A → E),
          ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N) ∧
            p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X) ∧
              (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n, g' (t', a) = g (t', a)
N : Set A
haN : a ∈ N
N_open : IsOpen[inst_2] N
g' : (↑I : Type) × A → E
cont_g' : ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N)
g'_lifts : p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X)
g'_0 : ∀ (a : A), g' (0, a) = g (0, a)
g'_a : ∀ t' ≤ t n, g' (t', a) = g (t', a)
e : E
h_sub : Set.Icc (t n) (t (n + 1)) ⊆ (fun (x : (↑I : Type)) ↦ g (x, a)) ⁻¹' (q e).source
this : SProd.sprod (β := Set A) (Set.Icc (t n) (t (n + 1))) {a} ⊆ (⇑f : (a : (↑I : Type) × A) → X) ⁻¹' (q e).target
u : Set (↑I : Type)
v : Set A
v_open : IsOpen[inst_2] v
hu : Set.Icc (t n) (t (n + 1)) ⊆ u
hav : {a} ⊆ v
huv : u ×ˢ v ⊆ (⇑f : (a : (↑I : Type) × A) → X) ⁻¹' (q e).target
t0 : (↑I : Type)
htn1 : t0 ≤ t n.succ
htn : ¬t0 ≤ t n
hf : Membership.mem (α := X) (q e).target ((f : (a : (↑I : Type) × A) → X) (t0, a) : X)
⊢ (f : (a : (↑I : Type) × A) → X) (t0, a) = p ((fun (x : (↑I : Type)) ↦ g (x, a)) t0)

Tactic:
exact (congr_fun g_lifts _).symm

Premises used: congr_fun, Eq.symm
-- 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
f : ContinuousMap.{u_3, u_2} ((↑I : Type) × A) X
g : (↑I : Type) × A → E
g_lifts : p ∘ g = (⇑f : (a : (↑I : Type) × A) → X)
cont_0 : Continuous[inst_2, inst] fun (x : A) ↦ g (0, x)
a : A
cont_a : Continuous[_, inst] fun (x : (↑I : Type)) ↦ g (x, a)
q : (x : E) → OpenPartialHomeomorph E X
mem_source : ∀ (x : E), x ∈ (q x).source
hpq : ∀ (x : E), p = (↑(q x) : E → X)
t : ℕ → (↑I : Type)
t_0 : t 0 = 0
t_mono : Monotone t
t_sub : ∀ (n : ℕ), ∃ (i : E), Set.Icc (t n) (t (n + 1)) ⊆ (fun (x : (↑I : Type)) ↦ g (x, a)) ⁻¹' (q i).source
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
h :
  ∃ (N : Set A),
    a ∈ N ∧
      IsOpen[inst_2] N ∧
        ∃ (g' : (↑I : Type) × A → E),
          ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N) ∧
            p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X) ∧
              (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n, g' (t', a) = g (t', a)
N : Set A
haN : a ∈ N
N_open : IsOpen[inst_2] N
g' : (↑I : Type) × A → E
cont_g' : ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N)
g'_lifts : p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X)
g'_0 : ∀ (a : A), g' (0, a) = g (0, a)
g'_a : ∀ t' ≤ t n, g' (t', a) = g (t', a)
e : E
h_sub : Set.Icc (t n) (t (n + 1)) ⊆ (fun (x : (↑I : Type)) ↦ g (x, a)) ⁻¹' (q e).source
this : SProd.sprod (β := Set A) (Set.Icc (t n) (t (n + 1))) {a} ⊆ (⇑f : (a : (↑I : Type) × A) → X) ⁻¹' (q e).target
u : Set (↑I : Type)
v : Set A
v_open : IsOpen[inst_2] v
hu : Set.Icc (t n) (t (n + 1)) ⊆ u
hav : {a} ⊆ v
huv : u ×ˢ v ⊆ (⇑f : (a : (↑I : Type) × A) → X) ⁻¹' (q e).target
t0 : (↑I : Type)
htn1 : t0 ≤ t n.succ
htn : ¬t0 ≤ t n
hf : ((f : (a : (↑I : Type) × A) → X) (t0, a) : X) ∉ (q e).target
⊢ g (t0, a) = g (t0, a)

Tactic:
rfl
-- 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
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
f : ContinuousMap.{u_3, u_2} ((↑I : Type) × A) X
g : (↑I : Type) × A → E
g_lifts : p ∘ g = (⇑f : (a : (↑I : Type) × A) → X)
cont_0 : Continuous[inst_2, inst] fun (x : A) ↦ g (0, x)
cont_A : ∀ (a : A), Continuous[_, inst] fun (x : (↑I : Type)) ↦ g (x, a)
rw : ∀ (x : (↑I : Type) × A), ContinuousAt g x
⊢ Continuous[instTopologicalSpaceProd, inst] g

Tactic:
rw [continuous_iff_continuousAt]

Premises used: continuous_iff_continuousAt
-- 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
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
f : ContinuousMap.{u_3, u_2} ((↑I : Type) × A) X
g : (↑I : Type) × A → E
g_lifts : p ∘ g = (⇑f : (a : (↑I : Type) × A) → X)
cont_0 : Continuous[inst_2, inst] fun (x : A) ↦ g (0, x)
cont_A : ∀ (a : A), Continuous[_, inst] fun (x : (↑I : Type)) ↦ g (x, a)
t : (↑I : Type)
a : A
obtain :
  ∀ (N : Set A) (haN : N ∈ 𝓝 a) (g' : (↑I : Type) × A → E)
    (cont_g' : ContinuousOn g' (SProd.sprod (α := Set (↑I : Type)) Set.univ N))
    (g'_lifts : p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X)) (g'_0 : ∀ (a : A), g' (0, a) = g (0, a)),
    ContinuousAt g (t, a)
⊢ ContinuousAt g (t, a)

Tactic:
obtain ⟨N, haN, g', cont_g', g'_lifts, g'_0, -⟩ :=
    homeo.exists_lift_nhds g_lifts cont_0 a (cont_A a)

Premises used: IsLocalHomeomorph.exists_lift_nhds
-- 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
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
f : ContinuousMap.{u_3, u_2} ((↑I : Type) × A) X
g : (↑I : Type) × A → E
g_lifts : p ∘ g = (⇑f : (a : (↑I : Type) × A) → X)
cont_0 : Continuous[inst_2, inst] fun (x : A) ↦ g (0, x)
cont_A : ∀ (a : A), Continuous[_, inst] fun (x : (↑I : Type)) ↦ g (x, a)
t : (↑I : Type)
a : A
N : Set A
haN : N ∈ 𝓝 a
g' : (↑I : Type) × A → E
cont_g' : ContinuousOn g' (SProd.sprod (α := Set (↑I : Type)) Set.univ N)
g'_lifts : p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X)
g'_0 : ∀ (a : A), g' (0, a) = g (0, a)
⊢ ContinuousAt g (t, a)

Tactic:
(cont_g'.congr fun ⟨t, a⟩ ⟨_, ha⟩ ↦ ?_).continuousAt (prod_mem_nhds Filter.univ_mem haN)

Premises used: prod_mem_nhds, Prod.mk, ContinuousOn.congr, _private.0.IsLocalHomeomorph.continuous_lift.match_2, Filter.univ_mem, ContinuousOn.continuousAt, Eq, _private.0.IsLocalHomeomorph.continuous_lift.match_3
-- 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
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
f : ContinuousMap.{u_3, u_2} ((↑I : Type) × A) X
g : (↑I : Type) × A → E
g_lifts : p ∘ g = (⇑f : (a : (↑I : Type) × A) → X)
cont_0 : Continuous[inst_2, inst] fun (x : A) ↦ g (0, x)
cont_A : ∀ (a : A), Continuous[_, inst] fun (x : (↑I : Type)) ↦ g (x, a)
t : (↑I : Type)
a : A
N : Set A
haN : N ∈ 𝓝 a
g' : (↑I : Type) × A → E
cont_g' : ContinuousOn g' (SProd.sprod (α := Set (↑I : Type)) Set.univ N)
g'_lifts : p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X)
g'_0 : ∀ (a : A), g' (0, a) = g (0, a)
refine :
  ∀ (x : (↑I : Type) × A) (t : (↑I : Type)) (a : A),
    (t, a) ∈ SProd.sprod (α := Set (↑I : Type)) Set.univ N →
      Membership.mem (γ := Set (↑I : Type)) Set.univ (t, a).1 → ∀ (ha : (t, a).2 ∈ N), g (t, a) = g' (t, a)
⊢ ContinuousAt g (t, a)

Tactic:
refine (cont_g'.congr fun ⟨t, a⟩ ⟨_, ha⟩ ↦ ?_).continuousAt (prod_mem_nhds Filter.univ_mem haN)

Premises used: prod_mem_nhds, Prod.mk, ContinuousOn.congr, _private.0.IsLocalHomeomorph.continuous_lift.match_2, Filter.univ_mem, ContinuousOn.continuousAt, Eq, _private.0.IsLocalHomeomorph.continuous_lift.match_3
-- 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
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
f : ContinuousMap.{u_3, u_2} ((↑I : Type) × A) X
g : (↑I : Type) × A → E
g_lifts : p ∘ g = (⇑f : (a : (↑I : Type) × A) → X)
cont_0 : Continuous[inst_2, inst] fun (x : A) ↦ g (0, x)
cont_A : ∀ (a : A), Continuous[_, inst] fun (x : (↑I : Type)) ↦ g (x, a)
t_1 : (↑I : Type)
a_1 : A
N : Set A
haN : N ∈ 𝓝 a_1
g' : (↑I : Type) × A → E
cont_g' : ContinuousOn g' (SProd.sprod (α := Set (↑I : Type)) Set.univ N)
g'_lifts : p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X)
g'_0 : ∀ (a : A), g' (0, a) = g (0, a)
x : (↑I : Type) × A
t : (↑I : Type)
a : A
h : (t, a) ∈ SProd.sprod (α := Set (↑I : Type)) Set.univ N
left : Membership.mem (γ := Set (↑I : Type)) Set.univ (t, a).1
ha : (t, a).2 ∈ N
⊢ g (t, a) = g' (t, a)

Tactic:
congr_fun (sep.eq_of_comp_eq homeo.isLocallyInjective (cont_A a)
    (cont_g'.comp_continuous (.prodMk_left a) fun _ ↦ ⟨⟨⟩, ha⟩) ?_ 0 (g'_0 a).symm) t

Premises used: ContinuousOn.comp_continuous, IsSeparatedMap.eq_of_comp_eq, And.intro, IsLocalHomeomorph.isLocallyInjective, congr_fun, OfNat.ofNat, Eq.symm, Continuous.prodMk_left, True.intro
-- 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
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
f : ContinuousMap.{u_3, u_2} ((↑I : Type) × A) X
g : (↑I : Type) × A → E
g_lifts : p ∘ g = (⇑f : (a : (↑I : Type) × A) → X)
cont_0 : Continuous[inst_2, inst] fun (x : A) ↦ g (0, x)
cont_A : ∀ (a : A), Continuous[_, inst] fun (x : (↑I : Type)) ↦ g (x, a)
t_1 : (↑I : Type)
a_1 : A
N : Set A
haN : N ∈ 𝓝 a_1
g' : (↑I : Type) × A → E
cont_g' : ContinuousOn g' (SProd.sprod (α := Set (↑I : Type)) Set.univ N)
g'_lifts : p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X)
g'_0 : ∀ (a : A), g' (0, a) = g (0, a)
x : (↑I : Type) × A
t : (↑I : Type)
a : A
h : (t, a) ∈ SProd.sprod (α := Set (↑I : Type)) Set.univ N
left : Membership.mem (γ := Set (↑I : Type)) Set.univ (t, a).1
ha : (t, a).2 ∈ N
refine : Eq (α := (↑I : Type) → X) (p ∘ fun (x : (↑I : Type)) ↦ g (x, a)) (p ∘ g' ∘ fun (x : (↑I : Type)) ↦ (x, a))
⊢ g (t, a) = g' (t, a)

Tactic:
refine congr_fun (sep.eq_of_comp_eq homeo.isLocallyInjective (cont_A a)
    (cont_g'.comp_continuous (.prodMk_left a) fun _ ↦ ⟨⟨⟩, ha⟩) ?_ 0 (g'_0 a).symm) t

Premises used: ContinuousOn.comp_continuous, IsSeparatedMap.eq_of_comp_eq, And.intro, IsLocalHomeomorph.isLocallyInjective, congr_fun, OfNat.ofNat, Eq.symm, Continuous.prodMk_left, True.intro
-- 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
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
f : ContinuousMap.{u_3, u_2} ((↑I : Type) × A) X
g : (↑I : Type) × A → E
g_lifts : p ∘ g = (⇑f : (a : (↑I : Type) × A) → X)
cont_0 : Continuous[inst_2, inst] fun (x : A) ↦ g (0, x)
cont_A : ∀ (a : A), Continuous[_, inst] fun (x : (↑I : Type)) ↦ g (x, a)
t_1 : (↑I : Type)
a_1 : A
N : Set A
haN : N ∈ 𝓝 a_1
g' : (↑I : Type) × A → E
cont_g' : ContinuousOn g' (SProd.sprod (α := Set (↑I : Type)) Set.univ N)
g'_lifts : p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X)
g'_0 : ∀ (a : A), g' (0, a) = g (0, a)
x : (↑I : Type) × A
t : (↑I : Type)
a : A
h_1 : (t, a) ∈ SProd.sprod (α := Set (↑I : Type)) Set.univ N
left : Membership.mem (γ := Set (↑I : Type)) Set.univ (t, a).1
ha : (t, a).2 ∈ N
h : ∀ (t : (↑I : Type)), (p ∘ fun (x : (↑I : Type)) ↦ g (x, a)) t = (p ∘ g' ∘ fun (x : (↑I : Type)) ↦ (x, a)) t
⊢ Eq (α := (↑I : Type) → X) (p ∘ fun (x : (↑I : Type)) ↦ g (x, a)) (p ∘ g' ∘ fun (x : (↑I : Type)) ↦ (x, a))

Tactic:
ext t
-- 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
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
f : ContinuousMap.{u_3, u_2} ((↑I : Type) × A) X
g : (↑I : Type) × A → E
g_lifts : p ∘ g = (⇑f : (a : (↑I : Type) × A) → X)
cont_0 : Continuous[inst_2, inst] fun (x : A) ↦ g (0, x)
cont_A : ∀ (a : A), Continuous[_, inst] fun (x : (↑I : Type)) ↦ g (x, a)
t_1 : (↑I : Type)
a_1 : A
N : Set A
haN : N ∈ 𝓝 a_1
g' : (↑I : Type) × A → E
cont_g' : ContinuousOn g' (SProd.sprod (α := Set (↑I : Type)) Set.univ N)
g'_lifts : p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X)
g'_0 : ∀ (a : A), g' (0, a) = g (0, a)
x : (↑I : Type) × A
t_2 : (↑I : Type)
a : A
h : (t_2, a) ∈ SProd.sprod (α := Set (↑I : Type)) Set.univ N
left : Membership.mem (γ := Set (↑I : Type)) Set.univ (t_2, a).1
ha : (t_2, a).2 ∈ N
t : (↑I : Type)
⊢ (p ∘ fun (x : (↑I : Type)) ↦ g (x, a)) t = (p ∘ g' ∘ fun (x : (↑I : Type)) ↦ (x, a)) t

Tactic:
apply congr_fun (g_lifts.trans g'_lifts.symm)

Premises used: congr_fun, Eq.symm, Eq.trans
-- Module: Mathlib.Topology.Homotopy.Lifting
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)
refine_4 :
  ∀ (this : Continuous[_, inst] fun (st : (↑I : Type) × (↑I : Type)) ↦ (Γ st.2 : (a : (↑I : Type)) → E) st.1),
    Eq (α := E) ((Γ t : (a : (↑I : Type)) → E) 1 : E) ((Γ 0 : (a : (↑I : Type)) → E) 1 : E)
refine_1 :
  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)
refine_2 :
  Continuous[_, inst] fun (x : (↑I : Type)) ↦
    (fun (st : (↑I : Type) × (↑I : Type)) ↦ ((Γ st.2 : (a : (↑I : Type)) → E) st.1 : E)) (0, x)
refine_3 :
  ∀ (a : (↑I : Type)),
    Continuous[_, inst] fun (x : (↑I : Type)) ↦
      (fun (st : (↑I : Type) × (↑I : Type)) ↦ ((Γ st.2 : (a : (↑I : Type)) → E) st.1 : E)) (x, a)
⊢ Eq (α := E) ((Γ t : (a : (↑I : Type)) → E) 1 : E) ((Γ 0 : (a : (↑I : Type)) → E) 1 : E)

Tactic:
have := homeo.continuous_lift sep (.comp γ .prodSwap) (g := fun st ↦ Γ st.2 st.1) ?_ ?_ ?_
-- Module: Mathlib.Topology.Homotopy.Lifting
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)
this : Continuous[_, inst] fun (st : (↑I : Type) × (↑I : Type)) ↦ (Γ st.2 : (a : (↑I : Type)) → E) st.1
refine_4 :
  ∀ (a a' : (↑I : Type)),
    p
        (((fun (st : (↑I : Type) × (↑I : Type)) ↦ (Γ st.2 : (a : (↑I : Type)) → E) st.1) ∘ fun (y : (↑I : Type)) ↦
            (1, y))
          a) =
      p
        (((fun (st : (↑I : Type) × (↑I : Type)) ↦ (Γ st.2 : (a : (↑I : Type)) → E) st.1) ∘ fun (y : (↑I : Type)) ↦
            (1, y))
          a')
⊢ Eq (α := E) ((Γ t : (a : (↑I : Type)) → E) 1 : E) ((Γ 0 : (a : (↑I : Type)) → E) 1 : E)

Tactic:
apply sep.const_of_comp homeo.isLocallyInjective (this.comp (.prodMk_right 1))

Premises used: Continuous.comp, Continuous.prodMk_right, IsSeparatedMap.const_of_comp, IsLocalHomeomorph.isLocallyInjective, OfNat.ofNat
-- Module: Mathlib.Topology.Homotopy.Lifting
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_1 : (↑I : Type)
this : Continuous[_, inst] fun (st : (↑I : Type) × (↑I : Type)) ↦ (Γ st.2 : (a : (↑I : Type)) → E) st.1
t t' : (↑I : Type)
refine_4 :
  p
      ((Γ ((fun (y : (↑I : Type)) ↦ ((1, y) : (↑I : Type) × (↑I : Type))) t).2 : (a : (↑I : Type)) → E)
        ((fun (y : (↑I : Type)) ↦ ((1, y) : (↑I : Type) × (↑I : Type))) t).1) =
    p
      ((Γ ((fun (y : (↑I : Type)) ↦ ((1, y) : (↑I : Type) × (↑I : Type))) t').2 : (a : (↑I : Type)) → E)
        ((fun (y : (↑I : Type)) ↦ ((1, y) : (↑I : Type) × (↑I : Type))) t').1)
⊢ p
      (((fun (st : (↑I : Type) × (↑I : Type)) ↦ (Γ st.2 : (a : (↑I : Type)) → E) st.1) ∘ fun (y : (↑I : Type)) ↦ (1, y))
        t) =
    p
      (((fun (st : (↑I : Type) × (↑I : Type)) ↦ (Γ st.2 : (a : (↑I : Type)) → E) st.1) ∘ fun (y : (↑I : Type)) ↦ (1, y))
        t')

Tactic:
change p (Γ _ _) = p (Γ _ _)

Premises used: DFunLike.coe
-- Module: Mathlib.Topology.Homotopy.Lifting
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_1 : (↑I : Type)
this : Continuous[_, inst] fun (st : (↑I : Type) × (↑I : Type)) ↦ (Γ st.2 : (a : (↑I : Type)) → E) st.1
t t' : (↑I : Type)
refine_4 refine_4₁ : p ((Γ t : (a : (↑I : Type)) → E) 1) = p ((Γ t' : (a : (↑I : Type)) → E) 1)
refine_4₂ :
  Eq (α := X) ((γ : (a : (↑I : Type) × (↑I : Type)) → X) (t, 1) : X)
    ((γ : (a : (↑I : Type) × (↑I : Type)) → X) (t', 1) : X)
⊢ p
      ((Γ ((fun (y : (↑I : Type)) ↦ ((1, y) : (↑I : Type) × (↑I : Type))) t).2 : (a : (↑I : Type)) → E)
        ((fun (y : (↑I : Type)) ↦ ((1, y) : (↑I : Type) × (↑I : Type))) t).1) =
    p
      ((Γ ((fun (y : (↑I : Type)) ↦ ((1, y) : (↑I : Type) × (↑I : Type))) t').2 : (a : (↑I : Type)) → E)
        ((fun (y : (↑I : Type)) ↦ ((1, y) : (↑I : Type) × (↑I : Type))) t').1)

Tactic:
simp_rw [Γ_lifts, γ.eq_fst _ (.inr rfl)]

Premises used: ContinuousMap.HomotopyRel.eq_fst, Or.inr, rfl
-- Module: Mathlib.Topology.Homotopy.Lifting
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)
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
⊢ 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)

Tactic:
ext
-- Module: Mathlib.Topology.Homotopy.Lifting
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)
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:
apply Γ_lifts
-- Module: Mathlib.Topology.Homotopy.Lifting
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)
refine_2 : Continuous[_, inst] fun (x : (↑I : Type)) ↦ (Γ 0 : (a : (↑I : Type)) → E) 0
⊢ Continuous[_, inst] fun (x : (↑I : Type)) ↦
    (fun (st : (↑I : Type) × (↑I : Type)) ↦ ((Γ st.2 : (a : (↑I : Type)) → E) st.1 : E)) (0, x)

Tactic:
simp_rw [Γ_0]
-- Module: Mathlib.Topology.Homotopy.Lifting
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)) ↦ (Γ 0 : (a : (↑I : Type)) → E) 0

Tactic:
continuous_const

Premises used: continuous_const
-- Module: Mathlib.Topology.Homotopy.Lifting
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)) ↦ (Γ 0 : (a : (↑I : Type)) → E) 0

Tactic:
exact continuous_const

Premises used: continuous_const
-- Module: Mathlib.Topology.Homotopy.Lifting
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)
⊢ ∀ (a : (↑I : Type)),
    Continuous[_, inst] fun (x : (↑I : Type)) ↦
      (fun (st : (↑I : Type) × (↑I : Type)) ↦ ((Γ st.2 : (a : (↑I : Type)) → E) st.1 : E)) (x, a)

Tactic:
fun t ↦ (Γ t).2

Premises used: ContinuousMap.continuous_toFun
-- Module: Mathlib.Topology.Homotopy.Lifting
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)
⊢ ∀ (a : (↑I : Type)),
    Continuous[_, inst] fun (x : (↑I : Type)) ↦
      (fun (st : (↑I : Type) × (↑I : Type)) ↦ ((Γ st.2 : (a : (↑I : Type)) → E) st.1 : E)) (x, a)

Tactic:
exact fun t ↦ (Γ t).2

Premises used: ContinuousMap.continuous_toFun