awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
f : List α → β
b : Filter β
a : α
l : List α
⊢ 𝓝 (a :: l) = Filter.map (fun (p : α × List α) ↦ p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l)
have simp : cons <$> 𝓝 a <*> 𝓝 l = (fun (p : α × List α) ↦ p.1 :: p.2) <$> (Prod.mk <$> 𝓝 a <*> 𝓝 l)
Tactic: simp only [nhds_cons, Filter.prod_eq, (Filter.map_def _ _).symm,
      (Filter.seq_eq_filter_seq _ _).symm]
-- Lean 4 proof step from Mathlib.Topology.List (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
f : List α → β
b : Filter β
a : α
l : List α
⊢ Tendsto f (𝓝 (a :: l)) b ↔ Tendsto (fun (p : α × List α) ↦ f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) b
have this : 𝓝 (a :: l) = Filter.map (fun (p : α × List α) ↦ p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l)
Tactic: have : 𝓝 (a::l) = (𝓝 a ×ˢ 𝓝 l).map fun p : α × List α => p.1::p.2 := by
    simp only [nhds_cons, Filter.prod_eq, (Filter.map_def _ _).symm,
      (Filter.seq_eq_filter_seq _ _).symm]
    simp [-Filter.map_def, Function.comp_def, functor_norm]
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
f : List α → β
b : Filter β
a : α
l : List α
this : 𝓝 (a :: l) = Filter.map (fun (p : α × List α) ↦ p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l)
⊢ Tendsto f (𝓝 (a :: l)) b ↔ Tendsto (fun (p : α × List α) ↦ f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) b
have rw : Tendsto (f ∘ fun (p : α × List α) ↦ p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l) b ↔
  Tendsto (fun (p : α × List α) ↦ f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) b
Tactic: rw [this, Filter.tendsto_map'_iff]
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
f : List α → β
r : List α → Filter β
h_nil : Tendsto f (pure []) (r [])
h_cons :
  ∀ (l : List α) (a : α),
    Tendsto f (𝓝 l) (r l) → Tendsto (fun (p : α × List α) ↦ f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))
a : α
l : List α
⊢ Tendsto f (𝓝 (a :: l)) (r (a :: l))
have rw : Tendsto (fun (p : α × List α) ↦ f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))
Tactic: rw [tendsto_cons_iff]
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : DiscreteTopology α
⊢ DiscreteTopology.{u_1} (List α)
have rw : ∀ (x : List α), 𝓝 x = pure x
Tactic: rw [discreteTopology_iff_nhds]
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : DiscreteTopology α
l : List α
⊢ 𝓝 l = pure l
have nil : Eq.{u_1 + 1} (α := Filter (List α)) (𝓝 []) (pure [])
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : DiscreteTopology α
l : List α
nil : Eq.{u_1 + 1} (α := Filter (List α)) (𝓝 []) (pure [])
⊢ 𝓝 l = pure l
have cons : ∀ (head : α) (tail : List α), 𝓝 tail = pure tail → 𝓝 (head :: tail) = pure (head :: tail)
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ ∀ (l : List α), ContinuousAt length l
have simp : ∀ (l : List α), Tendsto length (𝓝 l) (pure l.length)
Tactic: simp only [ContinuousAt, nhds_discrete]
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ ∀ (l : List α), Tendsto length (𝓝 l) (pure l.length)
have refine_1 : Tendsto.{u_1, 0} (α := List α) length (pure []) (pure (length.{u_1} (α := α) []))
Tactic: refine tendsto_nhds ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
refine_1 : Tendsto.{u_1, 0} (α := List α) length (pure []) (pure (length.{u_1} (α := α) []))
⊢ ∀ (l : List α), Tendsto length (𝓝 l) (pure l.length)
have refine_2 : ∀ (l : List α) (a : α),
  Tendsto length (𝓝 l) (pure l.length) →
    Tendsto (fun (p : α × List α) ↦ (p.1 :: p.2).length) (𝓝 a ×ˢ 𝓝 l) (pure (a :: l).length)
Tactic: refine tendsto_nhds ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
a : α
ih : Tendsto length (𝓝 l) (pure l.length)
⊢ Tendsto (fun (p : α × List α) ↦ p.2.length + 1) (𝓝 a ×ˢ 𝓝 l) (pure (l.length + 1))
have refine_2 : Tendsto (fun (p : α × List α) ↦ p.2.length.add 0) (𝓝 a ×ˢ 𝓝 l) (pure l.length)
Tactic: refine Tendsto.comp (tendsto_pure_pure (fun x => x + 1) _) ?_
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
n : ℕ
a' : α
l : List α
⊢ 𝓝 a ×ˢ 𝓝 (a' :: l) = Filter.map (fun (p : α × α × List α) ↦ (p.1, p.2.1 :: p.2.2)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)
have simp : Eq (α := Filter (α × List α)) (Prod.mk <$> 𝓝 a <*> (cons <$> 𝓝 a' <*> 𝓝 l))
  ((fun (p : α × α × List α) ↦ (p.1, p.2.1 :: p.2.2)) <$> (Prod.mk <$> 𝓝 a <*> (Prod.mk <$> 𝓝 a' <*> 𝓝 l)))
Tactic: simp only [nhds_cons, Filter.prod_eq, ← Filter.map_def, ← Filter.seq_eq_filter_seq]
-- Lean 4 proof step from Mathlib.Topology.List (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
n : ℕ
a' : α
l : List α
⊢ Tendsto (fun (p : α × List α) ↦ p.2.insertIdx (n + 1) p.1) (𝓝 a ×ˢ 𝓝 (a' :: l)) (𝓝 ((a' :: l).insertIdx (n + 1) a))
have this : 𝓝 a ×ˢ 𝓝 (a' :: l) = Filter.map (fun (p : α × α × List α) ↦ (p.1, p.2.1 :: p.2.2)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)
Tactic: have : 𝓝 a ×ˢ 𝓝 (a'::l) =
        (𝓝 a ×ˢ (𝓝 a' ×ˢ 𝓝 l)).map fun p : α × α × List α => (p.1, p.2.1::p.2.2) := by
      simp only [nhds_cons, Filter.prod_eq, ← Filter.map_def, ← Filter.seq_eq_filter_seq]
      simp [-Filter.map_def, Function.comp_def, functor_norm]
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
n : ℕ
a' : α
l : List α
this : 𝓝 a ×ˢ 𝓝 (a' :: l) = Filter.map (fun (p : α × α × List α) ↦ (p.1, p.2.1 :: p.2.2)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)
⊢ Tendsto (fun (p : α × List α) ↦ p.2.insertIdx (n + 1) p.1) (𝓝 a ×ˢ 𝓝 (a' :: l)) (𝓝 ((a' :: l).insertIdx (n + 1) a))
have rw : Tendsto ((fun (p : α × List α) ↦ p.2.insertIdx (n + 1) p.1) ∘ fun (p : α × α × List α) ↦ (p.1, p.2.1 :: p.2.2))
  (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l) (𝓝 ((a' :: l).insertIdx (n + 1) a))
Tactic: rw [this, tendsto_map'_iff]
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
x : α × List α
a : α
l : List α
⊢ ContinuousAt (Y := List α) (fun (p : α × List α) ↦ p.2.insertIdx n p.1) (a, l)
have rw : Tendsto (fun (p : α × List α) ↦ p.2.insertIdx n p.1) (𝓝 a ×ˢ 𝓝 l) (𝓝 ((a, l).2.insertIdx n (a, l).1))
Tactic: rw [ContinuousAt, nhds_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
x : ℕ
⊢ Tendsto (β := List α) (fun (x_1 : List α) ↦ x_1.eraseIdx x) (𝓝 []) (𝓝 (eraseIdx [] x))
have rw : Tendsto (β := List α) (fun (x_1 : List α) ↦ x_1.eraseIdx x) (pure []) (𝓝 (eraseIdx [] x))
Tactic: rw [nhds_nil]
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
l : List α
⊢ Tendsto (fun (x : List α) ↦ x.eraseIdx 0) (𝓝 (a :: l)) (𝓝 ((a :: l).eraseIdx 0))
have rw : Tendsto (fun (p : α × List α) ↦ (p.1 :: p.2).eraseIdx 0) (𝓝 a ×ˢ 𝓝 l) (𝓝 ((a :: l).eraseIdx 0))
Tactic: rw [tendsto_cons_iff]
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
a : α
l : List α
⊢ Tendsto (fun (x : List α) ↦ x.eraseIdx (n + 1)) (𝓝 (a :: l)) (𝓝 ((a :: l).eraseIdx (n + 1)))
have rw : Tendsto (fun (p : α × List α) ↦ (p.1 :: p.2).eraseIdx (n + 1)) (𝓝 a ×ˢ 𝓝 l) (𝓝 ((a :: l).eraseIdx (n + 1)))
Tactic: rw [tendsto_cons_iff]
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MulOneClass α
inst_2 : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 l.prod)
⊢ Tendsto prod (𝓝 (x :: l)) (𝓝 (x :: l).prod)
have cons : Tendsto (fun (p : α × List α) ↦ p.1 * p.2.prod) (𝓝 x ×ˢ 𝓝 l) (𝓝 (x * l.prod))
Tactic: simp_rw [tendsto_cons_iff, prod_cons]
-- Lean 4 proof step from Mathlib.Topology.List (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MulOneClass α
inst_2 : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 l.prod)
⊢ Tendsto (fun (p : α × List α) ↦ p.1 * p.2.prod) (𝓝 x ×ˢ 𝓝 l) (𝓝 (x * l.prod))
have this : ContinuousAt (Y := α) (fun (p : α × α) ↦ p.1 * p.2) (x, l.prod)
Tactic: have := continuous_iff_continuousAt.mp continuous_mul (x, l.prod)
-- Lean 4 proof step from Mathlib.Topology.List (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MulOneClass α
inst_2 : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 l.prod)
this : ContinuousAt (Y := α) (fun (p : α × α) ↦ p.1 * p.2) (x, l.prod)
⊢ Tendsto (fun (p : α × List α) ↦ p.1 * p.2.prod) (𝓝 x ×ˢ 𝓝 l) (𝓝 (x * l.prod))
have this₁ : Tendsto (fun (p : α × α) ↦ p.1 * p.2) (𝓝 x ×ˢ 𝓝 l.prod) (𝓝 ((x, l.prod).1 * (x, l.prod).2))
Tactic: rw [ContinuousAt, nhds_prod_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MulOneClass α
inst_2 : ContinuousMul α
l : List α
⊢ Tendsto prod (𝓝 l) (𝓝 l.prod)
have nil : Tendsto.{u_1, u_1} (α := List α) prod (𝓝 []) (𝓝 (prod []))
Tactic: induction l with
  | nil => simp +contextual [nhds_nil, mem_of_mem_nhds, tendsto_pure_left]
  | cons x l ih =>
    simp_rw [tendsto_cons_iff, prod_cons]
    have := continuous_iff_continuousAt.mp continuous_mul (x, l.prod)
    rw [ContinuousAt, nhds_prod_eq] at this
    exact this.comp (tendsto_id.prodMap ih)
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MulOneClass α
inst_2 : ContinuousMul α
l : List α
nil : Tendsto.{u_1, u_1} (α := List α) prod (𝓝 []) (𝓝 (prod []))
⊢ Tendsto prod (𝓝 l) (𝓝 l.prod)
have cons : ∀ (x : α) (l : List α) (ih : Tendsto prod (𝓝 l) (𝓝 l.prod)), Tendsto prod (𝓝 (x :: l)) (𝓝 (x :: l).prod)
Tactic: induction l with
  | nil => simp +contextual [nhds_nil, mem_of_mem_nhds, tendsto_pure_left]
  | cons x l ih =>
    simp_rw [tendsto_cons_iff, prod_cons]
    have := continuous_iff_continuousAt.mp continuous_mul (x, l.prod)
    rw [ContinuousAt, nhds_prod_eq] at this
    exact this.comp (tendsto_id.prodMap ih)
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
a : α
l : Vector α n
⊢ Tendsto (fun (p : α × Vector α n) ↦ p.1 ::ᵥ p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a ::ᵥ l))
have rw : Tendsto (fun (x : α × Vector α n) ↦ (↑(x.1 ::ᵥ x.2) : List α)) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a :: (↑l : List α)))
Tactic: rw [tendsto_subtype_rng, Vector.cons_val]
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
a : α
l : List α
hl : l.length = n
⊢ Tendsto (fun (p : α × Vector α n) ↦ insertIdx p.1 i p.2)
    (SProd.sprod (β := Filter (Vector α n)) (𝓝 a) (𝓝 (Subtype.mk (p := fun (l : List α) ↦ l.length = n) l hl)))
    (𝓝 (insertIdx a i (Subtype.mk (p := fun (l : List α) ↦ l.length = n) l hl)))
have rw : Tendsto (fun (x : α × Vector α n) ↦ (↑(insertIdx x.1 i x.2) : List α))
  (SProd.sprod (β := Filter (Vector α n)) (𝓝 a) (𝓝 (Subtype.mk (p := fun (l : List α) ↦ l.length = n) l hl)))
  (𝓝
    (↑(Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1)
          ((↑(Subtype.mk (p := fun (l : List α) ↦ l.length = n) l hl) : List α).insertIdx (↑i : ℕ) a) sorry) :
      List α))
Tactic: rw [insertIdx, tendsto_subtype_rng]
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
a : α
l : List α
hl : l.length = n
⊢ Tendsto (fun (x : α × Vector α n) ↦ (↑(insertIdx x.1 i x.2) : List α))
    (SProd.sprod (β := Filter (Vector α n)) (𝓝 a) (𝓝 (Subtype.mk (p := fun (l : List α) ↦ l.length = n) l hl)))
    (𝓝
      (↑(Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1)
            ((↑(Subtype.mk (p := fun (l : List α) ↦ l.length = n) l hl) : List α).insertIdx (↑i : ℕ) a) ⋯) :
        List α))
have simp : Tendsto (fun (x : α × Vector α n) ↦ (↑x.2 : List α).insertIdx (↑i : ℕ) x.1)
  (SProd.sprod (β := Filter (Vector α n)) (𝓝 a) (𝓝 (Subtype.mk (p := fun (l : List α) ↦ l.length = n) l hl)))
  (𝓝 (l.insertIdx (↑i : ℕ) a))
Tactic: simp only [insertIdx_val]
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
x : α × Vector α n
a : α
l : Vector α n
⊢ ContinuousAt (Y := Vector α (n + 1)) (fun (p : α × Vector α n) ↦ insertIdx p.1 i p.2) (a, l)
have rw : Tendsto (fun (p : α × Vector α n) ↦ insertIdx p.1 i p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (insertIdx (a, l).1 i (a, l).2))
Tactic: rw [ContinuousAt, nhds_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
l : List α
hl : l.length = n + 1
⊢ ContinuousAt (eraseIdx i) (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) l hl)
have rw : Tendsto (fun (x : Vector α (n + 1)) ↦ (↑(eraseIdx i x) : List α))
  (𝓝 (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) l hl))
  (𝓝 (↑(Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1 - 1) (l.eraseIdx (↑i : ℕ)) sorry) : List α))
Tactic: rw [ContinuousAt, Vector.eraseIdx, tendsto_subtype_rng]
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
l : List α
hl : l.length = n + 1
⊢ Tendsto (fun (x : Vector α (n + 1)) ↦ (↑(eraseIdx i x) : List α))
    (𝓝 (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) l hl))
    (𝓝 (↑(Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1 - 1) (l.eraseIdx (↑i : ℕ)) ⋯) : List α))
have simp : Tendsto (fun (x : Vector α (n + 1)) ↦ (↑x : List α).eraseIdx (↑i : ℕ))
  (𝓝 (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) l hl)) (𝓝 (l.eraseIdx (↑i : ℕ)))
Tactic: simp only [Vector.eraseIdx_val]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set β
h : IsInducing f
⊢ IsInducing (s.restrictPreimage f)
have simp_rw : ∀ (h : ∀ (x : α), 𝓝 x = comap f (𝓝 (f x))) (x : (↑(f ⁻¹' s) : Type u_1)),
  𝓝 x = comap (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' s)) (comap f (𝓝 (f (↑x : α))))
Tactic: simp_rw [← IsInducing.subtypeVal.of_comp_iff, isInducing_iff_nhds, restrictPreimage,
    MapsTo.coe_restrict, restrict_eq, ← @Filter.comap_comap _ _ _ _ _ f, Function.comp_apply] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set β
h : ∀ (x : α), 𝓝 x = comap f (𝓝 (f x))
a : (↑(f ⁻¹' s) : Type u_1)
⊢ 𝓝 a = comap (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' s)) (comap f (𝓝 (f (↑a : α))))
have rw : 𝓝 a = comap (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' s)) (𝓝 (↑a : α))
Tactic: rw [← h, ← IsInducing.subtypeVal.nhds_eq_comap]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set β
h : ∀ (x : α), 𝓝 x = comap f (𝓝 (f x))
a : (↑(f ⁻¹' s) : Type u_1)
rw : 𝓝 a = comap (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' s)) (𝓝 (↑a : α))
⊢ 𝓝 a = comap (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' s)) (comap f (𝓝 (f (↑a : α))))
have rw₁ : 𝓝 a = 𝓝 a
Tactic: rw [← h, ← IsInducing.subtypeVal.nhds_eq_comap]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
H : IsClosedMap f
s : Set β
t : Set (↑(f ⁻¹' s) : Type u_1)
⊢ IsClosed[instTopologicalSpaceSubtype] t → IsClosed[instTopologicalSpaceSubtype] (s.restrictPreimage f '' t)
have suffices : ∀ (u : Set α),
  IsClosed[inst] u →
    Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' s) ⁻¹' u = t →
      ∃ (v : Set β), IsClosed[inst_1] v ∧ Subtype.val (p := fun (x : β) ↦ x ∈ s) ⁻¹' v = s.restrictPreimage f '' t
Tactic: suffices ∀ u, IsClosed u → Subtype.val ⁻¹' u = t →
    ∃ v, IsClosed v ∧ Subtype.val ⁻¹' v = s.restrictPreimage f '' t by
      simpa [isClosed_induced_iff]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
H : IsOpenMap f
s : Set β
t : Set (↑(f ⁻¹' s) : Type u_1)
⊢ IsOpen[instTopologicalSpaceSubtype] t → IsOpen[instTopologicalSpaceSubtype] (s.restrictPreimage f '' t)
have suffices : ∀ (u : Set α),
  IsOpen[inst] u →
    Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' s) ⁻¹' u = t →
      ∃ (v : Set β), IsOpen[inst_1] v ∧ Subtype.val (p := fun (x : β) ↦ x ∈ s) ⁻¹' v = s.restrictPreimage f '' t
Tactic: suffices ∀ u, IsOpen u → Subtype.val ⁻¹' u = t →
    ∃ v, IsOpen v ∧ Subtype.val ⁻¹' v = s.restrictPreimage f '' t by
      simpa [isOpen_induced_iff]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
H : GeneralizingMap f
s : Set β
x : (↑(f ⁻¹' s) : Type u_1)
y : (↑s : Type u_2)
h : y ⤳ s.restrictPreimage f x
⊢ ∃ (a' : (↑(f ⁻¹' s) : Type u_1)), (fun (x1 x2 : (↑(f ⁻¹' s) : Type u_1)) ↦ x1 ⤳ x2) a' x ∧ s.restrictPreimage f a' = y
have obtain : ∀ (a : α) (ha : a ⤳ (↑x : α)) (hy : f a = (↑y : β)),
  ∃ (a' : (↑(f ⁻¹' s) : Type u_1)), (fun (x1 x2 : (↑(f ⁻¹' s) : Type u_1)) ↦ x1 ⤳ x2) a' x ∧ s.restrictPreimage f a' = y
Tactic: obtain ⟨a, ha, hy⟩ := H (h.map <| continuous_subtype_val (p := (· ∈ s)))
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
H : GeneralizingMap f
s : Set β
x : (↑(f ⁻¹' s) : Type u_1)
y : (↑s : Type u_2)
h : y ⤳ s.restrictPreimage f x
a : α
ha : a ⤳ (↑x : α)
hy : f a = (↑y : β)
⊢ ∃ (a' : (↑(f ⁻¹' s) : Type u_1)), (fun (x1 x2 : (↑(f ⁻¹' s) : Type u_1)) ↦ x1 ⤳ x2) a' x ∧ s.restrictPreimage f a' = y
have h₁ : (fun (x1 x2 : (↑(f ⁻¹' s) : Type u_1)) ↦ x1 ⤳ x2) (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' s) a sorry) x ∧
  s.restrictPreimage f (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' s) a sorry) = y
Tactic: use ⟨a, by simp [hy]⟩
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
H : IsProperMap f
s : Set β
⊢ IsProperMap (s.restrictPreimage f)
have rw : Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (s.restrictPreimage f) ∧
  IsClosedMap (s.restrictPreimage f) ∧ ∀ (y : (↑s : Type u_2)), IsCompact (s.restrictPreimage f ⁻¹' {y})
Tactic: rw [isProperMap_iff_isClosedMap_and_compact_fibers]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
H : IsProperMap f
s : Set β
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (s.restrictPreimage f) ∧
    IsClosedMap (s.restrictPreimage f) ∧ ∀ (y : (↑s : Type u_2)), IsCompact (s.restrictPreimage f ⁻¹' {y})
have refine : ∀ (y : (↑s : Type u_2)), IsCompact (s.restrictPreimage f ⁻¹' {y})
Tactic: refine ⟨H.continuous.restrictPreimage, H.isClosedMap.restrictPreimage _, fun y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
H : IsProperMap f
s : Set β
y : (↑s : Type u_2)
⊢ IsCompact (s.restrictPreimage f ⁻¹' {y})
have rw : IsCompact (f ⁻¹' {(↑y : β)})
Tactic: rw [IsEmbedding.subtypeVal.isCompact_iff, image_val_preimage_restrictPreimage, image_singleton]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
Goal:
β : Type u_2
inst : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
s : Set β
hU : IsOpenCover U
⊢ IsOpen[inst] s ↔ ∀ (i : ι), IsOpen[inst] (s ∩ (↑(U i) : Set β))
have mp : IsOpen[inst] s → ∀ (i : ι), IsOpen[inst] (s ∩ (↑(U i) : Set β))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
Goal:
β : Type u_2
inst : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
s : Set β
hU : IsOpenCover U
mp : IsOpen[inst] s → ∀ (i : ι), IsOpen[inst] (s ∩ (↑(U i) : Set β))
⊢ IsOpen[inst] s ↔ ∀ (i : ι), IsOpen[inst] (s ∩ (↑(U i) : Set β))
have mpr : (∀ (i : ι), IsOpen[inst] (s ∩ (↑(U i) : Set β))) → IsOpen[inst] s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (hypothesis)
Goal:
β : Type u_2
inst : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
s : Set β
⊢ IsLocallyClosed s ↔ ∀ (i : ι), IsLocallyClosed (X := ↥(U i)) (Subtype.val (p := fun (x : β) ↦ x ∈ U i) ⁻¹' s)
have this : ∀ (i : ι),
  Eq (α := Set ↥(U i)) (coborder (Subtype.val (p := fun (x : β) ↦ x ∈ U i) ⁻¹' s))
    (Subtype.val (p := fun (x : β) ↦ x ∈ U i) ⁻¹' coborder s)
Tactic: have (i : _) : coborder ((↑) ⁻¹' s : Set (U i)) = Subtype.val ⁻¹' coborder s :=
    (U i).isOpen.isOpenEmbedding_subtypeVal.coborder_preimage _
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
⊢ IsOpenMap f ↔ ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
have refine : ∀ (H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)) (s : Set α) (hs : IsOpen[inst] s),
  IsOpen[inst_1] (f '' s)
Tactic: refine ⟨fun h i ↦ h.restrictPreimage _, fun H s hs ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsOpen[inst] s
⊢ IsOpen[inst_1] (f '' s)
have rw : ∀ (i : ι), IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : β) ↦ x ∈ U i) ⁻¹' f '' s)
Tactic: rw [hU.isOpen_iff_coe_preimage]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsOpen[inst] s
i : ι
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : β) ↦ x ∈ U i) ⁻¹' f '' s)
have h : ↥(U i) = (↑(U i).carrier : Type u_2) →
  Subtype.val (p := fun (x : β) ↦ x ∈ U i) ⁻¹' f '' s =
    (U i).carrier.restrictPreimage f '' Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) ⁻¹' s
Tactic: convert! H i _ (hs.preimage continuous_subtype_val)
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsOpen[inst] s
i : ι
e_1 : ↥(U i) = (↑(U i).carrier : Type u_2)
⊢ Subtype.val (p := fun (x : β) ↦ x ∈ U i) ⁻¹' f '' s =
    (U i).carrier.restrictPreimage f '' Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) ⁻¹' s
have h : ∀ (x : β) (hx : x ∈ U i),
  Membership.mem (γ := Set ↥(U i)) (Subtype.val (p := fun (x : β) ↦ x ∈ U i) ⁻¹' f '' s)
      (Subtype.mk (p := fun (x : β) ↦ x ∈ U i) x hx) ↔
    Subtype.mk (p := fun (x : β) ↦ x ∈ U i) x hx ∈
      (U i).carrier.restrictPreimage f '' Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) ⁻¹' s
Tactic: ext ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsOpen[inst] s
i : ι
e_1 : ↥(U i) = (↑(U i).carrier : Type u_2)
x : β
hx : x ∈ U i
⊢ Membership.mem (γ := Set ↥(U i)) (Subtype.val (p := fun (x : β) ↦ x ∈ U i) ⁻¹' f '' s)
      (Subtype.mk (p := fun (x : β) ↦ x ∈ U i) x hx) ↔
    Subtype.mk (p := fun (x : β) ↦ x ∈ U i) x hx ∈
      (U i).carrier.restrictPreimage f '' Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) ⁻¹' s
have h : (∃ y ∈ s, f y = x) ↔ ∃ y ∈ s, f y ∈ U i ∧ f y = x
Tactic: suffices (∃ y, y ∈ s ∧ f y = x) ↔ ∃ y, y ∈ s ∧ f y ∈ U i ∧ f y = x by simpa [← Subtype.coe_inj]