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
ta : (↑I : Type) × A
_ : ¬ta.1 ≤ t n
hv : ((f : (a : (↑I : Type) × A) → X) ta : X) ∉ (q e).target
⊢ p (g ta) = (f : (a : (↑I : Type) × A) → X) ta

Tactic:
exact congr_fun g_lifts ta

Premises used: congr_fun
-- 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_1 : A
cont_a : Continuous[_, inst] fun (x : (↑I : Type)) ↦ g (x, a_1)
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_1)) ⁻¹' (q i).source
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
h :
  ∃ (N : Set A),
    a_1 ∈ 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_1) = g (t', a_1)
N : Set A
haN : a_1 ∈ 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_1) = g (t', a_1)
e : E
h_sub : Set.Icc (t n) (t (n + 1)) ⊆ (fun (x : (↑I : Type)) ↦ g (x, a_1)) ⁻¹' (q e).source
this : SProd.sprod (β := Set A) (Set.Icc (t n) (t (n + 1))) {a_1} ⊆ (⇑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_1} ⊆ v
huv : u ×ˢ v ⊆ (⇑f : (a : (↑I : Type) × A) → X) ⁻¹' (q e).target
a : A
refine_2 :
  (fun (ta : (↑I : Type) × A) ↦
        if ta.1 ≤ t n then g' ta
        else
          if Membership.mem (α := X) (q e).target ((f : (a : (↑I : Type) × A) → X) ta : X) then
            (↑(q e).symm : X → E) ((f : (a : (↑I : Type) × A) → X) ta)
          else g ta)
      (0, a) =
    g' (0, a)
⊢ (fun (ta : (↑I : Type) × A) ↦
        if ta.1 ≤ t n then g' ta
        else
          if Membership.mem (α := X) (q e).target ((f : (a : (↑I : Type) × A) → X) ta : X) then
            (↑(q e).symm : X → E) ((f : (a : (↑I : Type) × A) → X) ta)
          else g ta)
      (0, a) =
    g (0, a)

Tactic:
rw [← g'_0]
-- 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_1 : A
cont_a : Continuous[_, inst] fun (x : (↑I : Type)) ↦ g (x, a_1)
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_1)) ⁻¹' (q i).source
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
h :
  ∃ (N : Set A),
    a_1 ∈ 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_1) = g (t', a_1)
N : Set A
haN : a_1 ∈ 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_1) = g (t', a_1)
e : E
h_sub : Set.Icc (t n) (t (n + 1)) ⊆ (fun (x : (↑I : Type)) ↦ g (x, a_1)) ⁻¹' (q e).source
this : SProd.sprod (β := Set A) (Set.Icc (t n) (t (n + 1))) {a_1} ⊆ (⇑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_1} ⊆ v
huv : u ×ˢ v ⊆ (⇑f : (a : (↑I : Type) × A) → X) ⁻¹' (q e).target
a : A
⊢ (fun (ta : (↑I : Type) × A) ↦
        if ta.1 ≤ t n then g' ta
        else
          if Membership.mem (α := X) (q e).target ((f : (a : (↑I : Type) × A) → X) ta : X) then
            (↑(q e).symm : X → E) ((f : (a : (↑I : Type) × A) → X) ta)
          else g ta)
      (0, a) =
    g' (0, a)

Tactic:
if_pos bot_le

Premises used: if_pos, bot_le
-- 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_1 : A
cont_a : Continuous[_, inst] fun (x : (↑I : Type)) ↦ g (x, a_1)
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_1)) ⁻¹' (q i).source
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
h :
  ∃ (N : Set A),
    a_1 ∈ 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_1) = g (t', a_1)
N : Set A
haN : a_1 ∈ 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_1) = g (t', a_1)
e : E
h_sub : Set.Icc (t n) (t (n + 1)) ⊆ (fun (x : (↑I : Type)) ↦ g (x, a_1)) ⁻¹' (q e).source
this : SProd.sprod (β := Set A) (Set.Icc (t n) (t (n + 1))) {a_1} ⊆ (⇑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_1} ⊆ v
huv : u ×ˢ v ⊆ (⇑f : (a : (↑I : Type) × A) → X) ⁻¹' (q e).target
a : A
⊢ (fun (ta : (↑I : Type) × A) ↦
        if ta.1 ≤ t n then g' ta
        else
          if Membership.mem (α := X) (q e).target ((f : (a : (↑I : Type) × A) → X) ta : X) then
            (↑(q e).symm : X → E) ((f : (a : (↑I : Type) × A) → X) ta)
          else g ta)
      (0, a) =
    g' (0, a)

Tactic:
exact if_pos bot_le

Premises used: if_pos, bot_le
-- 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
refine_2 :
  (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)
⊢ (fun (ta : (↑I : Type) × A) ↦
        if ta.1 ≤ t n then g' ta
        else
          if Membership.mem (α := X) (q e).target ((f : (a : (↑I : Type) × A) → X) ta : X) then
            (↑(q e).symm : X → E) ((f : (a : (↑I : Type) × A) → X) ta)
          else g ta)
      (t0, a) =
    g (t0, a)

Tactic:
dsimp only
-- 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
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)
neg : ∀ (htn : ¬t0 ≤ t n) (hf : ((f : (a : (↑I : Type) × A) → X) (t0, a) : X) ∉ (q e).target), 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)

Tactic:
split_ifs with htn 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
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
⊢ g' (t0, a) = g (t0, a)

Tactic:
g'_a t0 htn
-- 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
⊢ g' (t0, a) = g (t0, a)

Tactic:
exact g'_a t0 htn
-- 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)
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)
⊢ (↑(q e).symm : X → E) ((f : (a : (↑I : Type) × A) → X) (t0, a)) = g (t0, a)

Tactic:
apply (q e).injOn ((q e).map_target hf) (h_sub ⟨le_of_not_ge htn, htn1⟩)

Premises used: le_of_not_ge, OpenPartialHomeomorph.map_target, And.intro, OpenPartialHomeomorph.injOn
-- 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)
pos : (f : (a : (↑I : Type) × A) → X) (t0, a) = p ((fun (x : (↑I : Type)) ↦ g (x, a)) t0)
⊢ (↑(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:
rw [(q e).right_inv hf, ← hpq e]

Premises used: OpenPartialHomeomorph.right_inv
-- 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:
(congr_fun g_lifts _).symm

Premises used: congr_fun, Eq.symm