awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
xs : List ((_ : α) × α)
nil :
  Eq.{u + 1} (α := List ((_ : α) × α)) []
    (map
      (fun (x : α × α) ↦
        match (motive := α × α → (_ : α) × α) x with
        | (a, b) => Sigma.mk (β := fun (x : α) ↦ α) a b)
      (zip (map (α := (_ : α) × α) (Sigma.fst (β := fun (x : α) ↦ α)) [])
        (map (α := (_ : α) × α) (Sigma.snd (β := fun (x : α) ↦ α)) [])))
⊢ xs =
    map
      (fun (x : α × α) ↦
        match (motive := α × α → (_ : α) × α) x with
        | (a, b) => Sigma.mk (β := fun (x : α) ↦ α) a b)
      ((map (Sigma.fst (β := fun (x : α) ↦ α)) xs).zip (map (Sigma.snd (β := fun (x : α) ↦ α)) xs))
have cons : ∀ (xs_hd : (_ : α) × α) (xs_tl : List ((_ : α) × α))
  (xs_ih :
    xs_tl =
      map
        (fun (x : α × α) ↦
          match (motive := α × α → (_ : α) × α) x with
          | (a, b) => Sigma.mk (β := fun (x : α) ↦ α) a b)
        ((map (Sigma.fst (β := fun (x : α) ↦ α)) xs_tl).zip (map (Sigma.snd (β := fun (x : α) ↦ α)) xs_tl))),
  xs_hd :: xs_tl =
    map
      (fun (x : α × α) ↦
        match (motive := α × α → (_ : α) × α) x with
        | (a, b) => Sigma.mk (β := fun (x : α) ↦ α) a b)
      ((map (Sigma.fst (β := fun (x : α) ↦ α)) (xs_hd :: xs_tl)).zip
        (map (Sigma.snd (β := fun (x : α) ↦ α)) (xs_hd :: xs_tl)))
Tactic: induction xs with
    | nil => simp only [List.zip_nil_right, List.map_nil]
    | cons xs_hd xs_tl xs_ih =>
      simp only [Sigma.eta, List.zip_cons_cons,
        List.map, List.cons_inj_right]
      exact xs_ih
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (hypothesis)
Goal:
α : Type u
inst : DecidableEq α
xs : List ((_ : α) × α)
hperm : map (Sigma.fst (β := fun (x : α) ↦ α)) xs ~ map (Sigma.snd (β := fun (x : α) ↦ α)) xs
hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) xs)
xs₀ : List α
h₀ : map (Sigma.fst (β := fun (x : α) ↦ α)) xs = xs₀
xs₁ : List α
h₁ : map (Sigma.snd (β := fun (x : α) ↦ α)) xs = xs₁
⊢ Injective (mapToSelf xs hperm hnodup).apply
have hxs : xs = List.toFinmap' (xs₀.zip xs₁)
Tactic: have hxs : xs = TotalFunction.List.toFinmap' (xs₀.zip xs₁) := by
    rw [← h₀, ← h₁, List.toFinmap']; clear h₀ h₁ xs₀ xs₁ hperm hnodup
    induction xs with
    | nil => simp only [List.zip_nil_right, List.map_nil]
    | cons xs_hd xs_tl xs_ih =>
      simp only [Sigma.eta, List.zip_cons_cons,
        List.map, List.cons_inj_right]
      exact xs_ih
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
xs : List ((_ : α) × α)
hperm : map (Sigma.fst (β := fun (x : α) ↦ α)) xs ~ map (Sigma.snd (β := fun (x : α) ↦ α)) xs
hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) xs)
xs₀ : List α
h₀ : map (Sigma.fst (β := fun (x : α) ↦ α)) xs = xs₀
xs₁ : List α
h₁ : map (Sigma.snd (β := fun (x : α) ↦ α)) xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
⊢ Injective (mapToSelf xs hperm hnodup).apply
have revert : ∀ (hperm : map (Sigma.fst (β := fun (x : α) ↦ α)) xs ~ map (Sigma.snd (β := fun (x : α) ↦ α)) xs)
  (hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) xs)), Injective (mapToSelf xs hperm hnodup).apply
Tactic: revert hperm hnodup
Cleared hypotheses: hperm, hnodup
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map (Sigma.fst (β := fun (x : α) ↦ α)) xs = xs₀
xs₁ : List α
h₁ : map (Sigma.snd (β := fun (x : α) ↦ α)) xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
⊢ ∀ (hperm : map (Sigma.fst (β := fun (x : α) ↦ α)) xs ~ map (Sigma.snd (β := fun (x : α) ↦ α)) xs)
    (hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) xs)), Injective (mapToSelf xs hperm hnodup).apply
have rw : ∀
  (hperm :
    map (Sigma.fst (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)) ~
      map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)))
  (hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)))),
  Injective (mapToSelf (List.toFinmap' (xs₀.zip xs₁)) hperm hnodup).apply
Tactic: rw [hxs]
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map (Sigma.fst (β := fun (x : α) ↦ α)) xs = xs₀
xs₁ : List α
h₁ : map (Sigma.snd (β := fun (x : α) ↦ α)) xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
hperm :
  map (Sigma.fst (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)) ~
    map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁))
hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)))
⊢ Injective (mapToSelf (List.toFinmap' (xs₀.zip xs₁)) hperm hnodup).apply
have h₂ : xs₀.Nodup
Tactic: apply InjectiveFunction.applyId_injective
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map (Sigma.fst (β := fun (x : α) ↦ α)) xs = xs₀
xs₁ : List α
h₁ : map (Sigma.snd (β := fun (x : α) ↦ α)) xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
hperm :
  map (Sigma.fst (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)) ~
    map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁))
hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)))
h₂ : xs₀.Nodup
⊢ Injective (mapToSelf (List.toFinmap' (xs₀.zip xs₁)) hperm hnodup).apply
have h₃ : xs₀ ~ xs₁
Tactic: apply InjectiveFunction.applyId_injective
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map (Sigma.fst (β := fun (x : α) ↦ α)) xs = xs₀
xs₁ : List α
h₁ : map (Sigma.snd (β := fun (x : α) ↦ α)) xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
hperm :
  map (Sigma.fst (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)) ~
    map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁))
hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)))
⊢ xs₀.Nodup
have h₂ : (map (Sigma.fst (β := fun (x : α) ↦ α)) xs).Nodup
Tactic: rwa [← h₀, hxs, hperm.nodup_iff]
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map (Sigma.fst (β := fun (x : α) ↦ α)) xs = xs₀
xs₁ : List α
h₁ : map (Sigma.snd (β := fun (x : α) ↦ α)) xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
hperm :
  map (Sigma.fst (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)) ~
    map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁))
hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)))
h₂ : (map (Sigma.fst (β := fun (x : α) ↦ α)) xs).Nodup
⊢ xs₀.Nodup
have h₃ : (map (Sigma.fst (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁))).Nodup
Tactic: rwa [← h₀, hxs, hperm.nodup_iff]
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map (Sigma.fst (β := fun (x : α) ↦ α)) xs = xs₀
xs₁ : List α
h₁ : map (Sigma.snd (β := fun (x : α) ↦ α)) xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
hperm :
  map (Sigma.fst (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)) ~
    map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁))
hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)))
⊢ xs₀ ~ xs₁
have h₂ : ∀ (hperm : map (Sigma.fst (β := fun (x : α) ↦ α)) xs ~ map (Sigma.snd (β := fun (x : α) ↦ α)) xs)
  (hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)))), xs₀ ~ xs₁
Tactic: rwa [← hxs, h₀, h₁] at hperm
Cleared hypotheses: hperm, hnodup
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map (Sigma.fst (β := fun (x : α) ↦ α)) xs = xs₀
xs₁ : List α
h₁ : map (Sigma.snd (β := fun (x : α) ↦ α)) xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
hperm :
  map (Sigma.fst (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)) ~
    map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁))
hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)))
h₂ :
  ∀ (hperm : map (Sigma.fst (β := fun (x : α) ↦ α)) xs ~ map (Sigma.snd (β := fun (x : α) ↦ α)) xs)
    (hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)))), xs₀ ~ xs₁
⊢ xs₀ ~ xs₁
have h₃ : ∀ (hperm : xs₀ ~ map (Sigma.snd (β := fun (x : α) ↦ α)) xs)
  (hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)))), xs₀ ~ xs₁
Tactic: rwa [← hxs, h₀, h₁] at hperm
Cleared hypotheses: hperm, hnodup
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map (Sigma.fst (β := fun (x : α) ↦ α)) xs = xs₀
xs₁ : List α
h₁ : map (Sigma.snd (β := fun (x : α) ↦ α)) xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
hperm :
  map (Sigma.fst (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)) ~
    map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁))
hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)))
h₂ :
  ∀ (hperm : map (Sigma.fst (β := fun (x : α) ↦ α)) xs ~ map (Sigma.snd (β := fun (x : α) ↦ α)) xs)
    (hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)))), xs₀ ~ xs₁
h₃ :
  ∀ (hperm : xs₀ ~ map (Sigma.snd (β := fun (x : α) ↦ α)) xs)
    (hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)))), xs₀ ~ xs₁
⊢ xs₀ ~ xs₁
have h₄ : ∀ (hperm : xs₀ ~ xs₁) (hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)))),
  xs₀ ~ xs₁
Tactic: rwa [← hxs, h₀, h₁] at hperm
Cleared hypotheses: hperm, hnodup
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (goal)
Goal:
α : Type u_3
inst : TopologicalSpace α
⊢ AlexandrovDiscrete α = ∀ (x : Set (Set α)), (∀ ⦃x_1 : Set α⦄, x_1 ∈ x → IsClosed[inst] x_1) → IsClosed[inst] (⋃₀ x)
have simp_rw : Eq (α := Prop) (∀ (x : Set (Set α)), (∀ ⦃x_1 : Set α⦄, x_1 ∈ x → IsClosed[inst] x_1) → IsClosed[inst] (⋃₀ x))
  (∀ (x : Set (Set α)), (∀ ⦃x_1 : Set α⦄, x_1 ∈ x → IsClosed[inst] x_1) → IsClosed[inst] (⋃₀ x))
Tactic: simp_rw +singlePass [alexandrovDiscrete_iff, compl_surjective.image_surjective.forall,
      forall_mem_image, ← compl_sUnion, isOpen_compl_iff]
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (goal)
Goal:
α : Type u_3
inst : TopologicalSpace α
| AlexandrovDiscrete α
have tactic : ∀ (x : Set (Set α)), (∀ ⦃x_1 : Set α⦄, x_1 ∈ x → IsClosed[inst] x_1) → IsClosed[inst] (⋃₀ x)
Tactic: tactic =>
    simp_rw +singlePass [alexandrovDiscrete_iff, compl_surjective.image_surjective.forall,
      forall_mem_image, ← compl_sUnion, isOpen_compl_iff]
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (goal)
Goal:
α : Type u_3
inst : TopologicalSpace α
⊢ AlexandrovDiscrete α ↔ ∀ (S : Set (Set α)), (∀ s ∈ S, IsClosed[inst] s) → IsClosed[inst] (⋃₀ S)
have conv_lhs : AlexandrovDiscrete α ↔ ∀ (S : Set (Set α)), (∀ s ∈ S, IsClosed[inst] s) → IsClosed[inst] (⋃₀ S)
Tactic: conv_lhs => tactic =>
    simp_rw +singlePass [alexandrovDiscrete_iff, compl_surjective.image_surjective.forall,
      forall_mem_image, ← compl_sUnion, isOpen_compl_iff]
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (goal)
Goal:
α : Type u_3
inst : TopologicalSpace α
conv_lhs : AlexandrovDiscrete α ↔ ∀ (S : Set (Set α)), (∀ s ∈ S, IsClosed[inst] s) → IsClosed[inst] (⋃₀ S)
⊢ AlexandrovDiscrete α ↔ ∀ (S : Set (Set α)), (∀ s ∈ S, IsClosed[inst] s) → IsClosed[inst] (⋃₀ S)
have conv_lhs₁ : (∀ (x : Set (Set α)), (∀ ⦃x_1 : Set α⦄, x_1 ∈ x → IsClosed[inst] x_1) → IsClosed[inst] (⋃₀ x)) ↔
  ∀ (S : Set (Set α)), (∀ s ∈ S, IsClosed[inst] s) → IsClosed[inst] (⋃₀ S)
Tactic: conv_lhs => tactic =>
    simp_rw +singlePass [alexandrovDiscrete_iff, compl_surjective.image_surjective.forall,
      forall_mem_image, ← compl_sUnion, isOpen_compl_iff]
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (goal)
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
S : Set (Set α)
⊢ interior (⋂₀ S) = ⋂ s ∈ S, interior s
have simp_rw : Eq.{u_3 + 1} (α := Set α) (interior (⋂ i ∈ S, i)) (⋂ s ∈ S, interior s)
Tactic: simp_rw [sInter_eq_biInter, interior_iInter]
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (goal)
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
S : Set (Set α)
⊢ closure[inst] (⋃₀ S) = ⋃ s ∈ S, closure[inst] s
have simp_rw : Eq.{u_3 + 1} (α := Set α) (closure[inst] (⋃ i ∈ S, i)) (⋃ s ∈ S, closure[inst] s)
Tactic: simp_rw [sUnion_eq_biUnion, closure_iUnion]
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (goal)
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AlexandrovDiscrete α
f : β → α
h : IsInducing f
S : Set (Set β)
hS : ∀ s ∈ S, IsOpen[inst_1] s
⊢ IsOpen[inst_1] (⋂₀ S)
have simp_rw : ∀ (hS : ∀ s ∈ S, ∃ (t : Set α), IsOpen[inst] t ∧ f ⁻¹' t = s), ∃ (t : Set α), IsOpen[inst] t ∧ f ⁻¹' t = ⋂₀ S
Tactic: simp_rw [h.isOpen_iff] at hS ⊢
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (goal)
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AlexandrovDiscrete α
f : β → α
h : IsInducing f
S : Set (Set β)
hS : ∀ s ∈ S, ∃ (t : Set α), IsOpen[inst] t ∧ f ⁻¹' t = s
⊢ ∃ (t : Set α), IsOpen[inst] t ∧ f ⁻¹' t = ⋂₀ S
have choose : ∀ (U : (s : Set β) → s ∈ S → Set α) (hU : ∀ (s : Set β) (a : s ∈ S), IsOpen[inst] (U s a))
  (htU : ∀ (s : Set β) (a : s ∈ S), f ⁻¹' U s a = s), ∃ (t : Set α), IsOpen[inst] t ∧ f ⁻¹' t = ⋂₀ S
Tactic: choose U hU htU using hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (goal)
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AlexandrovDiscrete α
f : β → α
h : IsInducing f
S : Set (Set β)
U : (s : Set β) → s ∈ S → Set α
hU : ∀ (s : Set β) (a : s ∈ S), IsOpen[inst] (U s a)
htU : ∀ (s : Set β) (a : s ∈ S), f ⁻¹' U s a = s
⊢ ∃ (t : Set α), IsOpen[inst] t ∧ f ⁻¹' t = ⋂₀ S
have refine : f ⁻¹' ⋂ (i : Set β), ⋂ (j : i ∈ S), U i j = ⋂₀ S
Tactic: refine ⟨_, isOpen_iInter₂ hU, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (goal)
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AlexandrovDiscrete α
f : β → α
h : IsInducing f
S : Set (Set β)
U : (s : Set β) → s ∈ S → Set α
hU : ∀ (s : Set β) (a : s ∈ S), IsOpen[inst] (U s a)
htU : ∀ (s : Set β) (a : s ∈ S), f ⁻¹' U s a = s
⊢ f ⁻¹' ⋂ (i : Set β), ⋂ (j : i ∈ S), U i j = ⋂₀ S
have simp_rw : ⋂ (i : Set β), ⋂ (i_1 : i ∈ S), f ⁻¹' U i i_1 = ⋂₀ S
Tactic: simp_rw [preimage_iInter, htU, sInter_eq_biInter]
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (goal)
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AlexandrovDiscrete α
f : β → α
h : IsInducing f
S : Set (Set β)
U : (s : Set β) → s ∈ S → Set α
hU : ∀ (s : Set β) (a : s ∈ S), IsOpen[inst] (U s a)
htU : ∀ (s : Set β) (a : s ∈ S), f ⁻¹' U s a = s
simp_rw : ⋂ (i : Set β), ⋂ (i_1 : i ∈ S), f ⁻¹' U i i_1 = ⋂₀ S
⊢ f ⁻¹' ⋂ (i : Set β), ⋂ (j : i ∈ S), U i j = ⋂₀ S
have simp_rw₁ : ⋂ i ∈ S, i = ⋂₀ S
Tactic: simp_rw [preimage_iInter, htU, sInter_eq_biInter]
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (goal)
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
s : Set α
⊢ IsOpen[inst] (nhdsKer s)
have rw : IsOpen[inst] (⋂₀ {t : Set α | IsOpen[inst] t ∧ s ⊆ t})
Tactic: rw [nhdsKer_def]
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (goal)
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
s : Set α
⊢ 𝓟 (nhdsKer s) = 𝓝ˢ s
have rw : 𝓟 (nhdsKer s) = 𝓝ˢ (nhdsKer s)
Tactic: rw [← nhdsSet_nhdsKer, isOpen_nhdsKer.nhdsSet_eq]
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (goal)
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
s : Set α
rw : 𝓟 (nhdsKer s) = 𝓝ˢ (nhdsKer s)
⊢ 𝓟 (nhdsKer s) = 𝓝ˢ s
have rw₁ : 𝓟 (nhdsKer s) = 𝓟 (nhdsKer s)
Tactic: rw [← nhdsSet_nhdsKer, isOpen_nhdsKer.nhdsSet_eq]
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (goal)
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
a : α
⊢ 𝓟 (nhdsKer {a}) = 𝓝 a
have rw : 𝓝ˢ {a} = 𝓝 a
Tactic: rw [principal_nhdsKer, nhdsSet_singleton]
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (goal)
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
a : α
rw : 𝓝ˢ {a} = 𝓝 a
⊢ 𝓟 (nhdsKer {a}) = 𝓝 a
have rw₁ : 𝓝 a = 𝓝 a
Tactic: rw [principal_nhdsKer, nhdsSet_singleton]
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (goal)
Goal:
α : Type u_3
inst : TopologicalSpace α
hα : ∀ (a : α), 𝓝 a = 𝓟 (nhdsKer {a})
⊢ AlexandrovDiscrete α
have simp : ∀ (S : Set (Set α)),
  (∀ s ∈ S, ∀ (a : α), (nhdsKer {a} ∩ s).Nonempty → a ∈ s) → ∀ (a : α), (nhdsKer {a} ∩ ⋃₀ S).Nonempty → a ∈ ⋃₀ S
Tactic: simp only [alexandrovDiscrete_iff_isClosed, isClosed_iff_clusterPt, ClusterPt, funext hα,
      inf_principal, principal_neBot_iff]
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (hypothesis)
Goal:
α : Type u_3
inst : TopologicalSpace α
hα : ∀ (a : α), 𝓝 a = 𝓟 (nhdsKer {a})
S : Set (Set α)
hS : ∀ s ∈ S, ∀ (a : α), (nhdsKer {a} ∩ s).Nonempty → a ∈ s
a : α
ha : (nhdsKer {a} ∩ ⋃₀ S).Nonempty
⊢ a ∈ ⋃₀ S
have ha₁ : ∃ i ∈ S, (nhdsKer {a} ∩ i).Nonempty
Tactic: rw [sUnion_eq_biUnion, inter_iUnion₂, nonempty_biUnion] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (goal)
Goal:
α : Type u_3
inst : TopologicalSpace α
hα : ∀ (a : α), 𝓝 a = 𝓟 (nhdsKer {a})
S : Set (Set α)
hS : ∀ s ∈ S, ∀ (a : α), (nhdsKer {a} ∩ s).Nonempty → a ∈ s
a : α
ha : ∃ i ∈ S, (nhdsKer {a} ∩ i).Nonempty
⊢ a ∈ ⋃₀ S
have obtain : ∀ (s : Set α) (hs : s ∈ S) (has : (nhdsKer {a} ∩ s).Nonempty), a ∈ ⋃₀ S
Tactic: obtain ⟨s, hs, has⟩ := ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (hypothesis)
Goal:
α : Type u_3
inst : TopologicalSpace α
hα : ∀ (a : α), 𝓝 a = 𝓟 (nhdsKer {a})
S : Set (Set α)
hS : ∀ s ∈ S, ∀ (a : α), (nhdsKer {a} ∩ s).Nonempty → a ∈ s
a : α
s : Set α
hs : s ∈ S
has : (nhdsKer {a} ∩ s).Nonempty
⊢ a ∈ ⋃₀ S
have hS₁ : a ∈ s
Tactic: specialize hS s hs a has
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (goal)
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
β : Type u_5
f : α → β
S : Set (Set β)
hS : ∀ s ∈ S, IsOpen[coinduced f inst] s
⊢ IsOpen[coinduced f inst] (⋂₀ S)
have rw : IsOpen[inst] (⋂ t ∈ S, f ⁻¹' t)
Tactic: rw [isOpen_coinduced, preimage_sInter]
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (goal)
Goal:
ι : Sort u_1
κ : ι → Sort u_2
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AlexandrovDiscrete α
inst_3 : AlexandrovDiscrete β
s t : Set α
a : α
⊢ AlexandrovDiscrete (α × β)
have simp_rw : ∀ (a : α × β), 𝓝 a = 𝓟 (nhdsKer {a})
Tactic: simp_rw [alexandrovDiscrete_iff_nhds, Prod.forall, nhds_prod_eq, ← principal_nhdsKer_singleton,
    prod_principal_principal, nhdsKer_pair, forall_true_iff]
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (goal)
Goal:
ι : Sort u_1
κ : ι → Sort u_2
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AlexandrovDiscrete α
inst_3 : AlexandrovDiscrete β
s t : Set α
a : α
simp_rw : ∀ (a : α × β), 𝓝 a = 𝓟 (nhdsKer {a})
⊢ AlexandrovDiscrete (α × β)
have simp_rw₁ : ∀ (a : α) (b : β), 𝓝 (a, b) = 𝓟 (nhdsKer {(a, b)})
Tactic: simp_rw [alexandrovDiscrete_iff_nhds, Prod.forall, nhds_prod_eq, ← principal_nhdsKer_singleton,
    prod_principal_principal, nhdsKer_pair, forall_true_iff]
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (goal)
Goal:
ι : Sort u_1
κ : ι → Sort u_2
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AlexandrovDiscrete α
inst_3 : AlexandrovDiscrete β
s t : Set α
a : α
simp_rw : ∀ (a : α × β), 𝓝 a = 𝓟 (nhdsKer {a})
simp_rw₁ : ∀ (a : α) (b : β), 𝓝 (a, b) = 𝓟 (nhdsKer {(a, b)})
⊢ AlexandrovDiscrete (α × β)
have simp_rw₂ : ∀ (a : α) (b : β), 𝓝 a ×ˢ 𝓝 b = 𝓟 (nhdsKer {(a, b)})
Tactic: simp_rw [alexandrovDiscrete_iff_nhds, Prod.forall, nhds_prod_eq, ← principal_nhdsKer_singleton,
    prod_principal_principal, nhdsKer_pair, forall_true_iff]
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (goal)
Goal:
ι : Sort u_1
κ : ι → Sort u_2
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AlexandrovDiscrete α
inst_3 : AlexandrovDiscrete β
s t : Set α
a : α
simp_rw : ∀ (a : α × β), 𝓝 a = 𝓟 (nhdsKer {a})
simp_rw₁ : ∀ (a : α) (b : β), 𝓝 (a, b) = 𝓟 (nhdsKer {(a, b)})
simp_rw₂ : ∀ (a : α) (b : β), 𝓝 a ×ˢ 𝓝 b = 𝓟 (nhdsKer {(a, b)})
⊢ AlexandrovDiscrete (α × β)
have simp_rw₃ : ∀ (a : α) (b : β),
  SProd.sprod (α := Filter α) (β := Filter β) (𝓟 (nhdsKer {a})) (𝓟 (nhdsKer {b})) = 𝓟 (nhdsKer {(a, b)})
Tactic: simp_rw [alexandrovDiscrete_iff_nhds, Prod.forall, nhds_prod_eq, ← principal_nhdsKer_singleton,
    prod_principal_principal, nhdsKer_pair, forall_true_iff]
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (goal)
Goal:
ι : Sort u_1
κ : ι → Sort u_2
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AlexandrovDiscrete α
inst_3 : AlexandrovDiscrete β
s t : Set α
a : α
simp_rw : ∀ (a : α × β), 𝓝 a = 𝓟 (nhdsKer {a})
simp_rw₁ : ∀ (a : α) (b : β), 𝓝 (a, b) = 𝓟 (nhdsKer {(a, b)})
simp_rw₂ : ∀ (a : α) (b : β), 𝓝 a ×ˢ 𝓝 b = 𝓟 (nhdsKer {(a, b)})
simp_rw₃ :
  ∀ (a : α) (b : β),
    SProd.sprod (α := Filter α) (β := Filter β) (𝓟 (nhdsKer {a})) (𝓟 (nhdsKer {b})) = 𝓟 (nhdsKer {(a, b)})
⊢ AlexandrovDiscrete (α × β)
have simp_rw₄ : ∀ (a : α) (b : β), 𝓟 (SProd.sprod (α := Set α) (β := Set β) (nhdsKer {a}) (nhdsKer {b})) = 𝓟 (nhdsKer {(a, b)})
Tactic: simp_rw [alexandrovDiscrete_iff_nhds, Prod.forall, nhds_prod_eq, ← principal_nhdsKer_singleton,
    prod_principal_principal, nhdsKer_pair, forall_true_iff]
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (goal)
Goal:
ι : Sort u_1
κ : ι → Sort u_2
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AlexandrovDiscrete α
inst_3 : AlexandrovDiscrete β
s t : Set α
a : α
simp_rw : ∀ (a : α × β), 𝓝 a = 𝓟 (nhdsKer {a})
simp_rw₁ : ∀ (a : α) (b : β), 𝓝 (a, b) = 𝓟 (nhdsKer {(a, b)})
simp_rw₂ : ∀ (a : α) (b : β), 𝓝 a ×ˢ 𝓝 b = 𝓟 (nhdsKer {(a, b)})
simp_rw₃ :
  ∀ (a : α) (b : β),
    SProd.sprod (α := Filter α) (β := Filter β) (𝓟 (nhdsKer {a})) (𝓟 (nhdsKer {b})) = 𝓟 (nhdsKer {(a, b)})
simp_rw₄ :
  ∀ (a : α) (b : β), 𝓟 (SProd.sprod (α := Set α) (β := Set β) (nhdsKer {a}) (nhdsKer {b})) = 𝓟 (nhdsKer {(a, b)})
⊢ AlexandrovDiscrete (α × β)
have simp_rw₅ : ∀ (a : α) (b : β), True
Tactic: simp_rw [alexandrovDiscrete_iff_nhds, Prod.forall, nhds_prod_eq, ← principal_nhdsKer_singleton,
    prod_principal_principal, nhdsKer_pair, forall_true_iff]
-- Lean 4 proof step from Mathlib.Topology.AlexandrovDiscrete (goal)
Goal:
ι_1 : Sort u_1
κ : ι_1 → Sort u_2
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AlexandrovDiscrete α
inst_3 : AlexandrovDiscrete β
s t : Set α
a : α
ι : Type u_5
inst_4 : Finite ι
X : ι → Type u_6
inst_5 : (i : ι) → TopologicalSpace (X i)
inst_6 : ∀ (i : ι), AlexandrovDiscrete.{u_6} (X i)
⊢ AlexandrovDiscrete ((i : ι) → X i)
have simp_rw : ∀ (a : (i : ι) → X i), 𝓝 a = 𝓟 (nhdsKer {a})
Tactic: simp_rw [alexandrovDiscrete_iff_nhds, nhds_pi, ← principal_nhdsKer_singleton,
    pi_principal, nhdsKer_singleton_pi, forall_true_iff]