awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
a b : π_ 1 X x
p q : (↑(Ω^ (Fin 1) X x) : Type u_2)
a₁ :
  HasEquiv.Equiv (α := Path { as := x : FundamentalGroupoid X }.as { as := x }.as)
    ((genLoopEquivOfUnique (Fin 1) : (a : (↑(Ω^ (Fin 1) X x) : Type u_2)) → Path { as := x }.as { as := x }.as)
        (transAt default q p) :
      Path { as := x : FundamentalGroupoid X }.as { as := x }.as)
    (Path.trans (y := { as := x }.as)
        ((genLoopEquivOfUnique (Fin 1) : (a : (↑(Ω^ (Fin 1) X x) : Type u_2)) → Path { as := x }.as { as := x }.as) q)
        ((genLoopEquivOfUnique (Fin 1) : (a : (↑(Ω^ (Fin 1) X x) : Type u_2)) → Path { as := x }.as { as := x }.as) p) :
      Path { as := x : FundamentalGroupoid X }.as { as := x }.as)
⊢ HasEquiv.Equiv (α := Path { as := x : FundamentalGroupoid X }.as { as := x }.as)
    ((genLoopEquivOfUnique (Fin 1) : (a : (↑(Ω^ (Fin 1) X x) : Type u_2)) → Path { as := x }.as { as := x }.as)
        (transAt 0 q p) :
      Path { as := x : FundamentalGroupoid X }.as { as := x }.as)
    (Path.trans (y := { as := x }.as)
        ((genLoopEquivOfUnique (Fin 1) : (a : (↑(Ω^ (Fin 1) X x) : Type u_2)) → Path { as := x }.as { as := x }.as) q)
        ((genLoopEquivOfUnique (Fin 1) : (a : (↑(Ω^ (Fin 1) X x) : Type u_2)) → Path { as := x }.as { as := x }.as) p) :
      Path { as := x : FundamentalGroupoid X }.as { as := x }.as)
have a₂ : (Path.Homotopic.setoid { as := x }.as { as := x }.as :
    Path { as := x }.as { as := x }.as → Path { as := x }.as { as := x }.as → Prop)
  (Path.trans (y := x) ((genLoopEquivOfUnique (Fin 1) : (a : (↑(Ω^ (Fin 1) X x) : Type u_2)) → Ω X x) q)
      ((genLoopEquivOfUnique (Fin 1) : (a : (↑(Ω^ (Fin 1) X x) : Type u_2)) → Ω X x) p) :
    Path x x)
  (Path.trans (y := x) ((genLoopEquivOfUnique (Fin 1) : (a : (↑(Ω^ (Fin 1) X x) : Type u_2)) → Ω X x) q)
      ((genLoopEquivOfUnique (Fin 1) : (a : (↑(Ω^ (Fin 1) X x) : Type u_2)) → Ω X x) p) :
    Path x x)
Tactic: rw [Unique.eq_default 0, genLoopEquivOfUnique_transAt]
-- 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
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)
⊢ ∃ 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)
have choose : ∀ (q : (x : E) → OpenPartialHomeomorph E X) (mem_source : ∀ (x : E), x ∈ (q x).source)
  (hpq : ∀ (x : E), p = (↑(q x) : E → X)),
  ∃ 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: choose q mem_source hpq using homeo
Cleared hypotheses: homeo
-- 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)
⊢ ∃ 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)
have obtain : ∀ (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 ∈ 𝓝 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 ⟨t, t_0, t_mono, ⟨n_max, h_max⟩, t_sub⟩ :=
    exists_monotone_Icc_subset_open_cover_unitInterval
      (fun e ↦ (q e).open_source.preimage cont_a)
      fun t _ ↦ Set.mem_iUnion.mpr ⟨g (t, a), mem_source _⟩
-- 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
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 ∈ 𝓝 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)
have 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)
Tactic: obtain ⟨N, haN, N_open, hN⟩ := this n_max
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (hypothesis)
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
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)
⊢ ∃ 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)
have 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)
Tactic: simp_rw [h_max _ le_rfl] at hN
Cleared hypotheses: hN
-- 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
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.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)
have h : ∀ (x : (↑I : Type) × A → E), Eq (α := Set (↑I : Type)) Set.univ (Set.Icc 0 1)
Tactic: convert! hN
-- 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
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)
⊢ ∃ (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)
have 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)
Tactic: convert! hN
-- 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
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
⊢ Eq (α := Set (↑I : Type)) Set.univ (Set.Icc 0 1)
have h : ∀ (x : (↑I : Type)), Membership.mem (γ := Set (↑I : Type)) (Set.Icc 0 1) x
Tactic: rw [eq_comm, Set.eq_univ_iff_forall]
-- 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
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)
⊢ x (a_1, a) = g (a_1, a) ↔ a_1 ≤ 1 → x (a_1, a) = g (a_1, a)
have h : a_1 ≤ 1
Tactic: rw [imp_iff_right]
-- 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 ∈ 𝓝 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)
have 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)
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
-- 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 : ℕ),
    ∃ (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)
have refine_1 : ContinuousOn g (SProd.sprod (β := Set A) (Set.Icc 0 (t Nat.zero)) Set.univ)
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⟩ ↦ ?_)
-- 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
refine_1 : ContinuousOn g (SProd.sprod (β := Set A) (Set.Icc 0 (t Nat.zero)) Set.univ)
⊢ ∀ (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)
have 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)
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⟩ ↦ ?_)
-- 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
⊢ ContinuousOn g (SProd.sprod (β := Set A) (Set.Icc 0 (t Nat.zero)) Set.univ)
have refine_1 : ∀ ta ∈ SProd.sprod (β := Set A) (Set.Icc 0 (t Nat.zero)) Set.univ,
  ∀ (ht : ta.1 ∈ Set.Icc 0 (t Nat.zero)),
    Membership.mem (γ := Set A) Set.univ ta.2 → g ta = ((fun (x : A) ↦ g (0, x)) ∘ Prod.snd) ta
Tactic: refine (cont_0.comp continuous_snd).continuousOn.congr (fun ta ⟨ht, _⟩ ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Lifting (hypothesis)
Goal:
E : Type u_1
X : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace A
p : E → X
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
ta : (↑I : Type) × A
h : ta ∈ SProd.sprod (β := Set A) (Set.Icc 0 (t Nat.zero)) Set.univ
ht : ta.1 ∈ Set.Icc 0 (t Nat.zero)
right : Membership.mem (γ := Set A) Set.univ ta.2
⊢ g ta = ((fun (x : A) ↦ g (0, x)) ∘ Prod.snd) ta
have ht₁ : ta.1 = 0
Tactic: rw [t_0, Set.Icc_self, Set.mem_singleton_iff] at ht
Cleared hypotheses: ht, right
-- 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
ta : (↑I : Type) × A
h : ta ∈ SProd.sprod (β := Set A) (Set.Icc 0 (t Nat.zero)) Set.univ
ht : ta.1 = 0
right : Membership.mem (γ := Set A) Set.univ ta.2
⊢ g ta = ((fun (x : A) ↦ g (0, x)) ∘ Prod.snd) ta
have refine_1 : g (0, ta.2) = Function.comp (α := (↑I : Type) × A) (fun (x : A) ↦ g (0, x)) Prod.snd (0, ta.2)
Tactic: rw [← ta.eta, ht]