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
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
pos : ∀ (htn : t0 ≤ t n), g' (t0, a) = g (t0, a)
⊢ (if t0 ≤ t n then g' (t0, a)
    else
      if Membership.mem (α := X) (q e).target ((f : (a : (↑I : Type) × A) → X) (t0, a) : X) then
        (↑(q e).symm : X → E) ((f : (a : (↑I : Type) × A) → X) (t0, a))
      else g (t0, a)) =
    g (t0, a)
have pos₁ : ∀ (htn : ¬t0 ≤ t n) (hf : Membership.mem (α := X) (q e).target ((f : (a : (↑I : Type) × A) → X) (t0, a) : X)),
  (↑(q e).symm : X → E) ((f : (a : (↑I : Type) × A) → X) (t0, a)) = g (t0, a)
Tactic: split_ifs with htn hf
-- 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
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
pos : ∀ (htn : t0 ≤ t n), g' (t0, a) = g (t0, a)
pos₁ :
  ∀ (htn : ¬t0 ≤ t n) (hf : Membership.mem (α := X) (q e).target ((f : (a : (↑I : Type) × A) → X) (t0, a) : X)),
    (↑(q e).symm : X → E) ((f : (a : (↑I : Type) × A) → X) (t0, a)) = g (t0, a)
⊢ (if t0 ≤ t n then g' (t0, a)
    else
      if Membership.mem (α := X) (q e).target ((f : (a : (↑I : Type) × A) → X) (t0, a) : X) then
        (↑(q e).symm : X → E) ((f : (a : (↑I : Type) × A) → X) (t0, a))
      else g (t0, a)) =
    g (t0, a)
have neg : ∀ (htn : ¬t0 ≤ t n) (hf : ((f : (a : (↑I : Type) × A) → X) (t0, a) : X) ∉ (q e).target), g (t0, a) = g (t0, a)
Tactic: split_ifs with htn hf
-- 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
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)
⊢ (↑(q e).symm : X → E) ((f : (a : (↑I : Type) × A) → X) (t0, a)) = g (t0, a)
have pos : (↑(q e) : E → X) ((↑(q e).symm : X → E) ((f : (a : (↑I : Type) × A) → X) (t0, a))) =
  (↑(q e) : E → X) ((fun (x : (↑I : Type)) ↦ g (x, a)) t0)
Tactic: apply (q e).injOn ((q e).map_target hf) (h_sub ⟨le_of_not_ge htn, htn1⟩)
-- 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
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)
⊢ (↑(q e) : E → X) ((↑(q e).symm : X → E) ((f : (a : (↑I : Type) × A) → X) (t0, a))) =
    (↑(q e) : E → X) ((fun (x : (↑I : Type)) ↦ g (x, a)) t0)
have pos : (f : (a : (↑I : Type) × A) → X) (t0, a) = p ((fun (x : (↑I : Type)) ↦ g (x, a)) t0)
Tactic: rw [(q e).right_inv hf, ← hpq e]
-- 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
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)
⊢ Continuous[instTopologicalSpaceProd, inst] g
have rw : ∀ (x : (↑I : Type) × A), ContinuousAt g x
Tactic: rw [continuous_iff_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
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
⊢ ContinuousAt g (t, a)
have 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)
Tactic: obtain ⟨N, haN, g', cont_g', g'_lifts, g'_0, -⟩ :=
    homeo.exists_lift_nhds g_lifts cont_0 a (cont_A 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
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)
have 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)
Tactic: refine (cont_g'.congr fun ⟨t, a⟩ ⟨_, ha⟩ ↦ ?_).continuousAt (prod_mem_nhds Filter.univ_mem haN)
-- 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
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)
have refine : Eq (α := (↑I : Type) → X) (p ∘ fun (x : (↑I : Type)) ↦ g (x, a)) (p ∘ g' ∘ fun (x : (↑I : Type)) ↦ (x, 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
-- 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
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
⊢ Eq (α := (↑I : Type) → X) (p ∘ fun (x : (↑I : Type)) ↦ g (x, a)) (p ∘ g' ∘ fun (x : (↑I : Type)) ↦ (x, a))
have h : ∀ (t : (↑I : Type)), (p ∘ fun (x : (↑I : Type)) ↦ g (x, a)) t = (p ∘ g' ∘ fun (x : (↑I : Type)) ↦ (x, a)) t
Tactic: ext t
-- 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 (α := E) ((Γ t : (a : (↑I : Type)) → E) 1 : E) ((Γ 0 : (a : (↑I : Type)) → E) 1 : E)
have 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)
Tactic: have := homeo.continuous_lift sep (.comp γ .prodSwap) (g := fun st ↦ Γ st.2 st.1) ?_ ?_ ?_
-- 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)
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)
⊢ Eq (α := E) ((Γ t : (a : (↑I : Type)) → E) 1 : E) ((Γ 0 : (a : (↑I : Type)) → E) 1 : E)
have 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)
Tactic: have := homeo.continuous_lift sep (.comp γ .prodSwap) (g := fun st ↦ Γ st.2 st.1) ?_ ?_ ?_
-- 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)
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)
⊢ Eq (α := E) ((Γ t : (a : (↑I : Type)) → E) 1 : E) ((Γ 0 : (a : (↑I : Type)) → E) 1 : E)
have 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)
Tactic: have := homeo.continuous_lift sep (.comp γ .prodSwap) (g := fun st ↦ Γ st.2 st.1) ?_ ?_ ?_
-- 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)
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)
⊢ Eq (α := E) ((Γ t : (a : (↑I : Type)) → E) 1 : E) ((Γ 0 : (a : (↑I : Type)) → E) 1 : E)
have 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)
Tactic: have := homeo.continuous_lift sep (.comp γ .prodSwap) (g := fun st ↦ Γ st.2 st.1) ?_ ?_ ?_
-- 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)
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)
have 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')
Tactic: apply sep.const_of_comp homeo.isLocallyInjective (this.comp (.prodMk_right 1))
-- 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_1 : (↑I : Type)
this : Continuous[_, inst] fun (st : (↑I : Type) × (↑I : Type)) ↦ (Γ st.2 : (a : (↑I : Type)) → E) st.1
t t' : (↑I : Type)
⊢ 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')
have 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)
Tactic: change p (Γ _ _) = p (Γ _ _)
-- 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_1 : (↑I : Type)
this : Continuous[_, inst] fun (st : (↑I : Type) × (↑I : Type)) ↦ (Γ st.2 : (a : (↑I : Type)) → E) st.1
t t' : (↑I : Type)
⊢ 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)
have refine_4 : p ((Γ t : (a : (↑I : Type)) → E) 1) = p ((Γ t' : (a : (↑I : Type)) → E) 1)
Tactic: simp_rw [Γ_lifts, γ.eq_fst _ (.inr rfl)]
-- 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_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)
⊢ 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)
have refine_4₂ : Eq (α := X) ((γ : (a : (↑I : Type) × (↑I : Type)) → X) (t, 1) : X)
  ((γ : (a : (↑I : Type) × (↑I : Type)) → X) (t', 1) : X)
Tactic: simp_rw [Γ_lifts, γ.eq_fst _ (.inr rfl)]