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
this :
  ∀ (n : ℕ),
    ∃ (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)
obtain :
  ∀ (N : Set A) (haN : a ∈ N) (N_open : IsOpen[inst_2] N)
    (hN :
      ∃ (g' : (↑I : Type) × A → E),
        ContinuousOn g' (Set.Icc 0 (t n_max) ×ˢ N) ∧
          p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X) ∧
            (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n_max, g' (t', a) = g (t', a)),
    ∃ N ∈ 𝓝 a,
      ∃ (g' : (↑I : Type) × A → E),
        ContinuousOn g' (SProd.sprod (α := Set (↑I : Type)) Set.univ N) ∧
          p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X) ∧
            (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ (t : (↑I : Type)), g' (t, a) = g (t, a)
⊢ ∃ N ∈ 𝓝 a,
    ∃ (g' : (↑I : Type) × A → E),
      ContinuousOn g' (SProd.sprod (α := Set (↑I : Type)) Set.univ N) ∧
        p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X) ∧
          (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ (t : (↑I : Type)), g' (t, a) = g (t, a)

Tactic:
obtain ⟨N, haN, N_open, hN⟩ := this n_max
-- 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
this :
  ∀ (n : ℕ),
    ∃ (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
hN :
  ∃ (g' : (↑I : Type) × A → E),
    ContinuousOn g' (Set.Icc 0 (t n_max) ×ˢ N) ∧
      p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X) ∧
        (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n_max, g' (t', a) = g (t', a)
⊢ ∃ (g' : (↑I : Type) × A → E),
    ContinuousOn g' (SProd.sprod (α := Set (↑I : Type)) (Set.Icc 0 1) N) ∧
      p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X) ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ 1, g' (t', a) = g (t', a)

Tactic:
simp_rw [h_max _ le_rfl] at hN

Premises used: le_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
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
this :
  ∀ (n : ℕ),
    ∃ (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
hN :
  ∃ (g' : (↑I : Type) × A → E),
    ContinuousOn g' (SProd.sprod (α := Set (↑I : Type)) (Set.Icc 0 1) N) ∧
      p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X) ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ 1, g' (t', a) = g (t', a)
⊢ ∃ N ∈ 𝓝 a,
    ∃ (g' : (↑I : Type) × A → E),
      ContinuousOn g' (SProd.sprod (α := Set (↑I : Type)) Set.univ N) ∧
        p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X) ∧
          (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ (t : (↑I : Type)), g' (t, a) = g (t, a)

Tactic:
⟨N, N_open.mem_nhds haN, ?_⟩

Premises used: And.intro, IsOpen.mem_nhds, Exists.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
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
this :
  ∀ (n : ℕ),
    ∃ (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
hN :
  ∃ (g' : (↑I : Type) × A → E),
    ContinuousOn g' (SProd.sprod (α := Set (↑I : Type)) (Set.Icc 0 1) N) ∧
      p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X) ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ 1, g' (t', a) = g (t', a)
⊢ ∃ (g' : (↑I : Type) × A → E),
    ContinuousOn g' (SProd.sprod (α := Set (↑I : Type)) (Set.Icc 0 1) N) ∧
      p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X) ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ 1, g' (t', a) = g (t', a)

Tactic:
hN
-- 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
this :
  ∀ (n : ℕ),
    ∃ (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
hN :
  ∃ (g' : (↑I : Type) × A → E),
    ContinuousOn g' (SProd.sprod (α := Set (↑I : Type)) (Set.Icc 0 1) N) ∧
      p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X) ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ 1, g' (t', a) = g (t', a)
h : ∀ (x : (↑I : Type) × A → E), Eq (α := Set (↑I : Type)) Set.univ (Set.Icc 0 1)
h₁ : ∀ (x : (↑I : Type) × A → E) (a_1 : (↑I : Type)), x (a_1, a) = g (a_1, a) ↔ a_1 ≤ 1 → x (a_1, a) = g (a_1, a)
⊢ ∃ (g' : (↑I : Type) × A → E),
    ContinuousOn g' (SProd.sprod (α := Set (↑I : Type)) Set.univ N) ∧
      p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X) ∧
        (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ (t : (↑I : Type)), g' (t, a) = g (t, a)

Tactic:
convert! hN
-- 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
this :
  ∀ (n : ℕ),
    ∃ (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
hN :
  ∃ (g' : (↑I : Type) × A → E),
    ContinuousOn g' (SProd.sprod (α := Set (↑I : Type)) (Set.Icc 0 1) N) ∧
      p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X) ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ 1, g' (t', a) = g (t', a)
x : (↑I : Type) × A → E
h : ∀ (x : (↑I : Type)), Membership.mem (γ := Set (↑I : Type)) (Set.Icc 0 1) x
⊢ Eq (α := Set (↑I : Type)) Set.univ (Set.Icc 0 1)

Tactic:
rw [eq_comm, Set.eq_univ_iff_forall]

Premises used: Set.eq_univ_iff_forall, eq_comm
-- 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
this :
  ∀ (n : ℕ),
    ∃ (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
hN :
  ∃ (g' : (↑I : Type) × A → E),
    ContinuousOn g' (SProd.sprod (α := Set (↑I : Type)) (Set.Icc 0 1) N) ∧
      p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X) ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ 1, g' (t', a) = g (t', a)
x : (↑I : Type) × A → E
⊢ ∀ (x : (↑I : Type)), Membership.mem (γ := Set (↑I : Type)) (Set.Icc 0 1) x

Tactic:
fun t ↦ ⟨bot_le, le_top⟩

Premises used: Set.Mem, setOf, Set.Icc, le_top, And.intro, 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
this :
  ∀ (n : ℕ),
    ∃ (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
hN :
  ∃ (g' : (↑I : Type) × A → E),
    ContinuousOn g' (SProd.sprod (α := Set (↑I : Type)) (Set.Icc 0 1) N) ∧
      p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X) ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ 1, g' (t', a) = g (t', a)
x : (↑I : Type) × A → E
⊢ ∀ (x : (↑I : Type)), Membership.mem (γ := Set (↑I : Type)) (Set.Icc 0 1) x

Tactic:
exact fun t ↦ ⟨bot_le, le_top⟩
-- 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
this :
  ∀ (n : ℕ),
    ∃ (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
hN :
  ∃ (g' : (↑I : Type) × A → E),
    ContinuousOn g' (SProd.sprod (α := Set (↑I : Type)) (Set.Icc 0 1) N) ∧
      p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X) ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ 1, g' (t', a) = g (t', a)
x : (↑I : Type) × A → E
a_1 : (↑I : Type)
h : a_1 ≤ 1
⊢ x (a_1, a) = g (a_1, a) ↔ a_1 ≤ 1 → x (a_1, a) = g (a_1, a)

Tactic:
rw [imp_iff_right]

Premises used: imp_iff_right
-- 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
this :
  ∀ (n : ℕ),
    ∃ (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
hN :
  ∃ (g' : (↑I : Type) × A → E),
    ContinuousOn g' (SProd.sprod (α := Set (↑I : Type)) (Set.Icc 0 1) N) ∧
      p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X) ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ 1, g' (t', a) = g (t', a)
x : (↑I : Type) × A → E
a_1 : (↑I : Type)
⊢ a_1 ≤ 1

Tactic:
le_top

Premises used: le_top
-- 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
this :
  ∀ (n : ℕ),
    ∃ (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
hN :
  ∃ (g' : (↑I : Type) × A → E),
    ContinuousOn g' (SProd.sprod (α := Set (↑I : Type)) (Set.Icc 0 1) N) ∧
      p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X) ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ 1, g' (t', a) = g (t', a)
x : (↑I : Type) × A → E
a_1 : (↑I : Type)
⊢ a_1 ≤ 1

Tactic:
exact le_top

Premises used: le_top
-- 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
suffices :
  ∀ (n : ℕ),
    ∃ (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 ∈ 𝓝 a,
    ∃ (g' : (↑I : Type) × A → E),
      ContinuousOn g' (SProd.sprod (α := Set (↑I : Type)) Set.univ N) ∧
        p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X) ∧
          (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ (t : (↑I : Type)), g' (t, a) = g (t, a)

Tactic:
suffices ∀ n, ∃ N, a ∈ N ∧ IsOpen N ∧ ∃ g' : I × A → E, ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N) ∧
      p ∘ g' = f ∧ (∀ a, g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n, g' (t', a) = g (t', a) by
    obtain ⟨N, haN, N_open, hN⟩ := this n_max
    simp_rw [h_max _ le_rfl] at hN
    refine ⟨N, N_open.mem_nhds haN, ?_⟩; convert! hN
    · rw [eq_comm, Set.eq_univ_iff_forall]; exact fun t ↦ ⟨bot_le, le_top⟩
    · rw [imp_iff_right]; exact le_top
-- 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 : ℕ),
    ∃ (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)

Tactic:
Nat.rec ⟨_, Set.mem_univ a, isOpen_univ, g, ?_, g_lifts, fun a ↦ rfl, fun _ _ ↦ rfl⟩
    (fun n ⟨N, haN, N_open, g', cont_g', g'_lifts, g'_0, g'_a⟩ ↦ ?_)

Premises used: Nat.rec
-- 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
refine_1 : ContinuousOn g (SProd.sprod (β := Set A) (Set.Icc 0 (t Nat.zero)) Set.univ)
refine_2 :
  ∀ (n : ℕ),
    (∃ (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)),
        ∃ (N : Set A),
          a ∈ N ∧
            IsOpen[inst_2] N ∧
              ∃ (g' : (↑I : Type) × A → E),
                ContinuousOn g' (Set.Icc 0 (t n.succ) ×ˢ N) ∧
                  p ∘ g' = (⇑f : (a : (↑I : Type) × A) → X) ∧
                    (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n.succ, g' (t', a) = g (t', a)
⊢ ∀ (n : ℕ),
    ∃ (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)

Tactic:
refine Nat.rec ⟨_, Set.mem_univ a, isOpen_univ, g, ?_, g_lifts, fun a ↦ rfl, fun _ _ ↦ rfl⟩
    (fun n ⟨N, haN, N_open, g', cont_g', g'_lifts, g'_0, g'_a⟩ ↦ ?_)
-- 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
⊢ ContinuousOn g (SProd.sprod (β := Set A) (Set.Icc 0 (t Nat.zero)) Set.univ)

Tactic:
(cont_0.comp continuous_snd).continuousOn.congr (fun ta ⟨ht, _⟩ ↦ ?_)

Premises used: Continuous.continuousOn, Continuous.comp, Function.comp, continuous_snd, _private.0.IsLocalHomeomorph.exists_lift_nhds.match_2, Prod.mk, ContinuousOn.congr, OfNat.ofNat, Eq, Prod.snd