awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
rwa : ∀ (hS' : IsIrreducible (closure[inst] S)), IsIrreducible (S ∩ closedPoints X)
rwa₁ : ∀ (hS' : IsIrreducible (closure[inst] (S ∩ closedPoints X))), IsIrreducible (S ∩ closedPoints X)
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (hS' : IsIrreducible (S ∩ closedPoints X)), IsIrreducible (S ∩ closedPoints X)
⊢ IsIrreducible (S ∩ closedPoints X)

Tactic:
rwa [← isIrreducible_iff_closure, ← JacobsonSpace.closure_inter_closedPoints_eq_closure hS,
      isIrreducible_iff_closure] at hS'

Premises used: JacobsonSpace.closure_inter_closedPoints_eq_closure, isIrreducible_iff_closure
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
⊢ IsIrreducible (S ∩ closedPoints X)

Tactic:
have H₁ : IsIrreducible (S ∩ closedPoints X) := by
    rwa [← isIrreducible_iff_closure, ← JacobsonSpace.closure_inter_closedPoints_eq_closure hS,
      isIrreducible_iff_closure] at hS'
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
x : X
hx : x ∈ S ∩ closedPoints X
⊢ f x ∈ closedPoints Y

Tactic:
simpa using hf₂ _ hx.2

Premises used: And.right
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
⊢ f '' (S ∩ closedPoints X) ⊆ closedPoints Y

Tactic:
have H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y := by
    rintro _ ⟨x, hx, rfl⟩; simpa using hf₂ _ hx.2
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y
⊢ (f '' (S ∩ closedPoints X)).Subsingleton

Tactic:
have H₃ := ((hfS.subset (Set.image_mono Set.inter_subset_left)).isDiscrete_of_subset_closedPoints
    H₂).subsingleton_of_isPreirreducible (H₁.image _ hf₁.continuousOn).isPreirreducible
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y
H₃ : (f '' (S ∩ closedPoints X)).Subsingleton
inl : ∀ (h : f '' (S ∩ closedPoints X) = ∅), IsClosed[inst_1] (f '' (S ∩ closedPoints X))
inr : ∀ (x : Y) (hx : x ∈ f '' (S ∩ closedPoints X)), IsClosed[inst_1] (f '' (S ∩ closedPoints X))
⊢ IsClosed[inst_1] (f '' (S ∩ closedPoints X))

Tactic:
obtain (h | ⟨x, hx⟩) := Set.eq_empty_or_nonempty (f '' (S ∩ closedPoints X))

Premises used: closedPoints, Inter.inter, Set.eq_empty_or_nonempty, Set.image
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y
H₃ : (f '' (S ∩ closedPoints X)).Subsingleton
h : f '' (S ∩ closedPoints X) = ∅
⊢ IsClosed[inst_1] (f '' (S ∩ closedPoints X))

Tactic:
simp [h]
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y
H₃ : (f '' (S ∩ closedPoints X)).Subsingleton
x : Y
hx : x ∈ f '' (S ∩ closedPoints X)
inr : IsClosed[inst_1] {x}
⊢ IsClosed[inst_1] (f '' (S ∩ closedPoints X))

Tactic:
rw [H₃.eq_singleton_of_mem hx]

Premises used: Set.Subsingleton.eq_singleton_of_mem
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y
H₃ : (f '' (S ∩ closedPoints X)).Subsingleton
x : Y
hx : x ∈ f '' (S ∩ closedPoints X)
⊢ IsClosed[inst_1] {x}

Tactic:
H₂ hx

Premises used: Set.Mem, setOf, closedPoints
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y
H₃ : (f '' (S ∩ closedPoints X)).Subsingleton
x : Y
hx : x ∈ f '' (S ∩ closedPoints X)
⊢ IsClosed[inst_1] {x}

Tactic:
exact H₂ hx
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y
H₃ : (f '' (S ∩ closedPoints X)).Subsingleton
⊢ IsClosed[inst_1] (f '' (S ∩ closedPoints X))

Tactic:
have H₄ : IsClosed (f '' (S ∩ closedPoints X)) := by
    obtain (h | ⟨x, hx⟩) := Set.eq_empty_or_nonempty (f '' (S ∩ closedPoints X))
    · simp [h]
    · rw [H₃.eq_singleton_of_mem hx]; exact H₂ hx
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y
H₃ : (f '' (S ∩ closedPoints X)).Subsingleton
H₄ : IsClosed[inst_1] (f '' (S ∩ closedPoints X))
⊢ f '' closure[inst] (S ∩ closedPoints X) ⊆ closure[inst_1] (f '' (S ∩ closedPoints X))

Tactic:
have := image_closure_subset_closure_image (s := S ∩ closedPoints X) hf₁
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y
H₃ : (f '' (S ∩ closedPoints X)).Subsingleton
H₄ : IsClosed[inst_1] (f '' (S ∩ closedPoints X))
this : f '' closure[inst] (S ∩ closedPoints X) ⊆ closure[inst_1] (f '' (S ∩ closedPoints X))
⊢ f '' closure[inst] S ⊆ f '' (S ∩ closedPoints X)

Tactic:
rw [JacobsonSpace.closure_inter_closedPoints_eq_closure hS, H₄.closure_eq] at this

Premises used: IsClosed.closure_eq, JacobsonSpace.closure_inter_closedPoints_eq_closure
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y
H₃ : (f '' (S ∩ closedPoints X)).Subsingleton
H₄ : IsClosed[inst_1] (f '' (S ∩ closedPoints X))
this : f '' closure[inst] S ⊆ f '' (S ∩ closedPoints X)
⊢ (f '' closure[inst] S).Subsingleton

Tactic:
H₃.anti this

Premises used: Set.Subsingleton.anti
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y
H₃ : (f '' (S ∩ closedPoints X)).Subsingleton
H₄ : IsClosed[inst_1] (f '' (S ∩ closedPoints X))
this : f '' closure[inst] S ⊆ f '' (S ∩ closedPoints X)
⊢ (f '' closure[inst] S).Subsingleton

Tactic:
exact H₃.anti this

Premises used: Set.Subsingleton.anti
-- Module: Mathlib.Topology.KrullDimension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : Y → X
hf : IsInducing f
⊢ topologicalKrullDim Y ≤ topologicalKrullDim X

Tactic:
krullDim_le_of_strictMono _ (map_strictMono_of_isInducing hf)

Premises used: TopologicalSpace.IrreducibleCloseds.map_strictMono_of_isInducing, Order.krullDim_le_of_strictMono, topologicalKrullDim
-- Module: Mathlib.Topology.KrullDimension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsHomeomorph f
⊢ topologicalKrullDim X = topologicalKrullDim Y

Tactic:
have fwd : topologicalKrullDim X ≤ topologicalKrullDim Y :=
    IsInducing.topologicalKrullDim_le h.isClosedEmbedding.toIsInducing
  have bwd : topologicalKrullDim Y ≤ topologicalKrullDim X :=
    IsInducing.topologicalKrullDim_le (h.homeomorph f).symm.isClosedEmbedding.toIsInducing
  le_antisymm fwd bwd

Premises used: IsHomeomorph.homeomorph, IsHomeomorph.isClosedEmbedding, IsInducing.topologicalKrullDim_le, Topology.IsClosedEmbedding.toIsEmbedding, le_antisymm, Homeomorph.symm, Topology.IsEmbedding.toIsInducing, Homeomorph.isClosedEmbedding
-- Module: Mathlib.Topology.KrullDimension
Goal:
X : Type u_3
inst : TopologicalSpace X
Y : Set X
⊢ topologicalKrullDim.{u_3} (↑Y : Type u_3) ≤ topologicalKrullDim X

Tactic:
IsInducing.topologicalKrullDim_le IsInducing.subtypeVal

Premises used: IsInducing.topologicalKrullDim_le, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.KrullDimension
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
⊢ topologicalKrullDim X ≤ 0

Tactic:
krullDim_nonpos_iff_forall_isMax.mpr fun Z Y h ↦ (h.antisymm' fun x hx ↦ ?_).le

Premises used: Iff.mpr, LE.le.antisymm', Order.krullDim_nonpos_iff_forall_isMax, Eq.le, topologicalKrullDim
-- Module: Mathlib.Topology.KrullDimension
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
refine : ∀ (Z Y : IrreducibleCloseds X) (h : Z ≤ Y) (x : X) (hx : x ∈ Y), x ∈ Z
⊢ topologicalKrullDim X ≤ 0

Tactic:
refine krullDim_nonpos_iff_forall_isMax.mpr fun Z Y h ↦ (h.antisymm' fun x hx ↦ ?_).le

Premises used: Iff.mpr, LE.le.antisymm', Order.krullDim_nonpos_iff_forall_isMax, Eq.le
-- Module: Mathlib.Topology.KrullDimension
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
Z Y : IrreducibleCloseds X
h : Z ≤ Y
x : X
hx : x ∈ Y
obtain : ∀ (z : X) (hz : z ∈ Z.carrier), x ∈ Z
⊢ x ∈ Z

Tactic:
obtain ⟨z, hz⟩ := Z.2.nonempty

Premises used: TopologicalSpace.IrreducibleCloseds.isIrreducible', IsIrreducible.nonempty
-- Module: Mathlib.Topology.KrullDimension
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
Z Y : IrreducibleCloseds X
h : Z ≤ Y
x : X
hx : x ∈ Y
z : X
hz : z ∈ Z.carrier
rwa rwa₁ rwa₂ rwa₃ : z ∈ Z
⊢ x ∈ Z

Tactic:
rwa [DiscreteTopology.isDiscrete.subsingleton_of_isPreirreducible Y.2.isPreirreducible hx (h hz)]

Premises used: IsDiscrete.subsingleton_of_isPreirreducible, DiscreteTopology.isDiscrete, TopologicalSpace.IrreducibleCloseds.isIrreducible', IsIrreducible.isPreirreducible
-- Module: Mathlib.Topology.KrullDimension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
Z : IrreducibleCloseds X
rw :
  coheight (map f ⋯ Z) =
    coheight.{u_2} (α := (↑{V : IrreducibleCloseds Y | (f ⁻¹' (↑V : Set Y)).Nonempty} : Type u_2))
      ((orderIsoOfIsOpenEmbedding f hf :
            (a : IrreducibleCloseds X) → (↑{V : IrreducibleCloseds Y | (f ⁻¹' (↑V : Set Y)).Nonempty} : Type u_2))
          Z :
        (↑{V : IrreducibleCloseds Y | (f ⁻¹' (↑V : Set Y)).Nonempty} : Type u_2))
⊢ coheight (map f ⋯ Z) = coheight Z

Tactic:
rw [← coheight_orderIso (orderIsoOfIsOpenEmbedding f hf) Z]

Premises used: TopologicalSpace.IrreducibleCloseds.orderIsoOfIsOpenEmbedding, Order.coheight_orderIso
-- Module: Mathlib.Topology.KrullDimension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
Z : IrreducibleCloseds X
⊢ coheight (map f ⋯ Z) =
    coheight.{u_2} (α := (↑{V : IrreducibleCloseds Y | (f ⁻¹' (↑V : Set Y)).Nonempty} : Type u_2))
      ((orderIsoOfIsOpenEmbedding f hf :
            (a : IrreducibleCloseds X) → (↑{V : IrreducibleCloseds Y | (f ⁻¹' (↑V : Set Y)).Nonempty} : Type u_2))
          Z :
        (↑{V : IrreducibleCloseds Y | (f ⁻¹' (↑V : Set Y)).Nonempty} : Type u_2))

Tactic:
.symm (coheight_eq_of_strictMono Subtype.val (Subtype.strictMono_coe _) ?_ _)

Premises used: Order.coheight_eq_of_strictMono, Eq.symm, Subtype.val, Subtype.strictMono_coe
-- Module: Mathlib.Topology.KrullDimension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
Z : IrreducibleCloseds X
refine :
  ∀
    (a :
      { x : IrreducibleCloseds Y //
        Membership.mem (γ := Set (IrreducibleCloseds Y)) {V : IrreducibleCloseds Y | (f ⁻¹' (↑V : Set Y)).Nonempty} x })
    (b : IrreducibleCloseds Y),
    (↑a : IrreducibleCloseds Y) < b →
      ∃ (a' :
        { x : IrreducibleCloseds Y //
          Membership.mem (γ := Set (IrreducibleCloseds Y)) {V : IrreducibleCloseds Y | (f ⁻¹' (↑V : Set Y)).Nonempty}
            x }),
        a < a' ∧ (↑a' : IrreducibleCloseds Y) = b
⊢ coheight (map f ⋯ Z) =
    coheight.{u_2} (α := (↑{V : IrreducibleCloseds Y | (f ⁻¹' (↑V : Set Y)).Nonempty} : Type u_2))
      ((orderIsoOfIsOpenEmbedding f hf :
            (a : IrreducibleCloseds X) → (↑{V : IrreducibleCloseds Y | (f ⁻¹' (↑V : Set Y)).Nonempty} : Type u_2))
          Z :
        (↑{V : IrreducibleCloseds Y | (f ⁻¹' (↑V : Set Y)).Nonempty} : Type u_2))

Tactic:
refine .symm (coheight_eq_of_strictMono Subtype.val (Subtype.strictMono_coe _) ?_ _)
-- Module: Mathlib.Topology.KrullDimension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
Z : IrreducibleCloseds X
a :
  { x : IrreducibleCloseds Y //
    Membership.mem (γ := Set (IrreducibleCloseds Y)) {V : IrreducibleCloseds Y | (f ⁻¹' (↑V : Set Y)).Nonempty} x }
b : IrreducibleCloseds Y
hlt : (↑a : IrreducibleCloseds Y) < b
⊢ ∃ (a' :
    { x : IrreducibleCloseds Y //
      Membership.mem (γ := Set (IrreducibleCloseds Y)) {V : IrreducibleCloseds Y | (f ⁻¹' (↑V : Set Y)).Nonempty} x }),
    a < a' ∧ (↑a' : IrreducibleCloseds Y) = b

Tactic:
⟨⟨b, a.2.mono (Set.preimage_mono hlt.le)⟩, hlt, rfl⟩

Premises used: LT.lt.le, Set.Nonempty.mono, Subtype.mk, Set.preimage_mono, And.intro, Exists.intro, rfl, Subtype.property
-- Module: Mathlib.Topology.KrullDimension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
Z : IrreducibleCloseds X
a :
  { x : IrreducibleCloseds Y //
    Membership.mem (γ := Set (IrreducibleCloseds Y)) {V : IrreducibleCloseds Y | (f ⁻¹' (↑V : Set Y)).Nonempty} x }
b : IrreducibleCloseds Y
hlt : (↑a : IrreducibleCloseds Y) < b
⊢ ∃ (a' :
    { x : IrreducibleCloseds Y //
      Membership.mem (γ := Set (IrreducibleCloseds Y)) {V : IrreducibleCloseds Y | (f ⁻¹' (↑V : Set Y)).Nonempty} x }),
    a < a' ∧ (↑a' : IrreducibleCloseds Y) = b

Tactic:
exact ⟨⟨b, a.2.mono (Set.preimage_mono hlt.le)⟩, hlt, rfl⟩
-- Module: Mathlib.Topology.KrullDimension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : QuasiSober Y
inst_3 : T0Space Y
inst_4 : QuasiSober X
inst_5 : T0Space X
x : X
f : X → Y
hf : IsOpenEmbedding f
rw :
  coheight (α := IrreducibleCloseds Y)
      ((OrderIso.symm irreducibleSetEquivPoints : (a : Y) → IrreducibleCloseds Y) (f x) : IrreducibleCloseds Y) =
    coheight (map f ⋯ ((OrderIso.symm irreducibleSetEquivPoints : (a : X) → IrreducibleCloseds X) x))
⊢ coheight (f x) = coheight x

Tactic:
rw [← coheight_orderIso (irreducibleSetEquivPoints (α := Y)).symm (f x),
    ← coheight_orderIso (irreducibleSetEquivPoints (α := X)).symm x,
    ← Topology.IsOpenEmbedding.coheight_map hf]

Premises used: irreducibleSetEquivPoints, Topology.IsOpenEmbedding.coheight_map, OrderIso.symm, Order.coheight_orderIso
-- Module: Mathlib.Topology.KrullDimension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : QuasiSober Y
inst_3 : T0Space Y
inst_4 : QuasiSober X
inst_5 : T0Space X
x : X
f : X → Y
hf : IsOpenEmbedding f
e_a :
  (OrderIso.symm irreducibleSetEquivPoints : (a : Y) → IrreducibleCloseds Y) (f x) =
    map f ⋯ ((OrderIso.symm irreducibleSetEquivPoints : (a : X) → IrreducibleCloseds X) x)
⊢ coheight (α := IrreducibleCloseds Y)
      ((OrderIso.symm irreducibleSetEquivPoints : (a : Y) → IrreducibleCloseds Y) (f x) : IrreducibleCloseds Y) =
    coheight (map f ⋯ ((OrderIso.symm irreducibleSetEquivPoints : (a : X) → IrreducibleCloseds X) x))

Tactic:
congr
-- Module: Mathlib.Topology.KrullDimension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : QuasiSober Y
inst_3 : T0Space Y
inst_4 : QuasiSober X
inst_5 : T0Space X
x : X
f : X → Y
hf : IsOpenEmbedding f
e_a :
  (↑((OrderIso.symm irreducibleSetEquivPoints : (a : Y) → IrreducibleCloseds Y) (f x) : IrreducibleCloseds Y) : Set Y) =
    (↑(map f ⋯ ((OrderIso.symm irreducibleSetEquivPoints : (a : X) → IrreducibleCloseds X) x)) : Set Y)
⊢ (OrderIso.symm irreducibleSetEquivPoints : (a : Y) → IrreducibleCloseds Y) (f x) =
    map f ⋯ ((OrderIso.symm irreducibleSetEquivPoints : (a : X) → IrreducibleCloseds X) x)

Tactic:
ext : 1
-- Module: Mathlib.Topology.KrullDimension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : QuasiSober Y
inst_3 : T0Space Y
inst_4 : QuasiSober X
inst_5 : T0Space X
x : X
f : X → Y
hf : IsOpenEmbedding f
⊢ (↑((OrderIso.symm irreducibleSetEquivPoints : (a : Y) → IrreducibleCloseds Y) (f x) : IrreducibleCloseds Y) : Set Y) =
    (↑(map f ⋯ ((OrderIso.symm irreducibleSetEquivPoints : (a : X) → IrreducibleCloseds X) x)) : Set Y)

Tactic:
simp [closure_image_closure hf.continuous]

Premises used: closure_image_closure, Topology.IsOpenEmbedding.continuous
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
as : List α
⊢ 𝓝 as = traverse 𝓝 as

Tactic:
nhds_mkOfNhds _ _ ?_ ?_

Premises used: TopologicalSpace.nhds_mkOfNhds
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
as : List α
refine_1 : LE.le.{u_1} (α := List α → Filter (List α)) pure (traverse 𝓝)
refine_2 : ∀ (a : List α), ∀ s ∈ traverse 𝓝 a, ∀ᶠ (y : List α) in traverse 𝓝 a, s ∈ traverse 𝓝 y
⊢ 𝓝 as = traverse 𝓝 as

Tactic:
refine nhds_mkOfNhds _ _ ?_ ?_

Premises used: TopologicalSpace.nhds_mkOfNhds
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
as : List α
⊢ LE.le.{u_1} (α := (fun (a : List α) ↦ Filter.{u_1} (List α)) []) (pure []) (traverse 𝓝 [])

Tactic:
le_rfl

Premises used: le_rfl, Set.Mem
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
as : List α
⊢ LE.le.{u_1} (α := (fun (a : List α) ↦ Filter.{u_1} (List α)) []) (pure []) (traverse 𝓝 [])

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
as : List α
a : α
l : List α
ih : pure l ≤ traverse 𝓝 l
this : List.cons <$> pure a <*> pure l ≤ List.cons <$> 𝓝 a <*> traverse 𝓝 l
⊢ pure (a :: l) ≤ traverse 𝓝 (a :: l)

Tactic:
simpa only [functor_norm] using this
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
as : List α
a : α
l : List α
ih : pure l ≤ traverse 𝓝 l
refine_1 : List.cons <$> pure a <*> pure l ≤ List.cons <$> 𝓝 a <*> traverse 𝓝 l
⊢ pure (a :: l) ≤ traverse 𝓝 (a :: l)

Tactic:
suffices List.cons <$> pure a <*> pure l ≤ List.cons <$> 𝓝 a <*> traverse 𝓝 l by
        simpa only [functor_norm] using this
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
as : List α
a : α
l : List α
ih : pure l ≤ traverse 𝓝 l
⊢ List.cons <$> pure a <*> pure l ≤ List.cons <$> 𝓝 a <*> traverse 𝓝 l

Tactic:
Filter.seq_mono (Filter.map_mono <| pure_le_nhds a) ih

Premises used: Filter.map_mono, Set.Mem, pure_le_nhds, Filter.seq_mono
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
as : List α
a : α
l : List α
ih : pure l ≤ traverse 𝓝 l
⊢ List.cons <$> pure a <*> pure l ≤ List.cons <$> 𝓝 a <*> traverse 𝓝 l

Tactic:
exact Filter.seq_mono (Filter.map_mono <| pure_le_nhds a) ih

Premises used: Filter.map_mono, pure_le_nhds, Filter.seq_mono
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
as l : List α
refine_1 : LE.le.{u_1} (α := (fun (a : List α) ↦ Filter.{u_1} (List α)) []) (pure []) (traverse 𝓝 [])
refine_1₁ : ∀ (a : α) (l : List α) (ih : pure l ≤ traverse 𝓝 l), pure (a :: l) ≤ traverse 𝓝 (a :: l)
⊢ pure l ≤ traverse 𝓝 l

Tactic:
induction l with
    | nil => exact le_rfl
    | cons a l ih =>
      suffices List.cons <$> pure a <*> pure l ≤ List.cons <$> 𝓝 a <*> traverse 𝓝 l by
        simpa only [functor_norm] using this
      exact Filter.seq_mono (Filter.map_mono <| pure_le_nhds a) ih

Premises used: le_rfl
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
as l : List α
s : Set (List α)
hs : s ∈ traverse 𝓝 l
refine_2 :
  ∀ (u : List (Set α)) (hu : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u) (hus : sequence u ⊆ s),
    ∀ᶠ (y : List α) in traverse 𝓝 l, s ∈ traverse 𝓝 y
⊢ ∀ᶠ (y : List α) in traverse 𝓝 l, s ∈ traverse 𝓝 y

Tactic:
rcases (mem_traverse_iff _ _).1 hs with ⟨u, hu, hus⟩

Premises used: Filter.mem_traverse_iff, Iff.mp
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
u : List (Set α)
s : Set (List α)
hus : sequence [] ⊆ s
nil : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) [] [] ∧ sequence [] ⊆ s
⊢ ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) [] v ∧ sequence v ⊆ s

Tactic:
exists []
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
u : List (Set α)
s : Set (List α)
hus : sequence [] ⊆ s
nil : True ∧ sequence [] ⊆ s
⊢ List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) [] [] ∧ sequence [] ⊆ s

Tactic:
simp only [List.forall₂_nil_left_iff]

Premises used: List.forall₂_nil_left_iff
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
u : List (Set α)
s : Set (List α)
hus : sequence [] ⊆ s
⊢ True ∧ sequence [] ⊆ s

Tactic:
⟨trivial, hus⟩

Premises used: trivial, And.intro
-- Module: Mathlib.Topology.List
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
u : List (Set α)
s : Set (List α)
hus : sequence [] ⊆ s
⊢ True ∧ sequence [] ⊆ s

Tactic:
exact ⟨trivial, hus⟩