mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case pos.refine_2
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) C
hC : Nonempty ↑C
a : A
c : ↑C
⊢ (↑c ∩ X ⁻¹' {a}).Nonempty

pp: case pos.refine_3
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) C
hC : Nonempty ↑C
a : A
c : ↑C
⊢ IsClosed (↑c ∩ X ⁻¹' {a})

pp: case pos.refine_4
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) C
hC : Nonempty ↑C
a : A
c : ↑C
⊢ IsClosed (↑c ∩ X ⁻¹' {a})

Tactic:
·

Goal state after:
case pos.refine_2
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) C
hC : Nonempty ↑C
a : A
c : ↑C
⊢ (↑c ∩ X ⁻¹' {a}).Nonempty
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case neg
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) C
hC : ¬Nonempty ↑C
⊢ X '' ⋂ c, ↑c = univ

Tactic:
·

Goal state after:
case neg
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) C
hC : ¬Nonempty ↑C
⊢ X '' ⋂ c, ↑c = univ
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case pos
A E : Type u
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
G_empty : G = ∅
⊢ ρ '' G ⊆ closure (ρ '' Gᶜ)ᶜ

pp: case neg
A E : Type u
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
G_empty : ¬G = ∅
⊢ ρ '' G ⊆ closure (ρ '' Gᶜ)ᶜ

Tactic:
·

Goal state after:
case pos
A E : Type u
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
G_empty : G = ∅
⊢ ρ '' G ⊆ closure (ρ '' Gᶜ)ᶜ
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case neg
A E : Type u
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
G_empty : ¬G = ∅
⊢ ρ '' G ⊆ closure (ρ '' Gᶜ)ᶜ

Tactic:
·

Goal state after:
case neg
A E : Type u
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
G_empty : ¬G = ∅
⊢ ρ '' G ⊆ closure (ρ '' Gᶜ)ᶜ
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons.nil
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := o, stk := update S k L₂ }
s : Option Γ'
S : K' → List Γ'
e : ([], none, []) = (a :: L₁, o, L₂)
e₁ : S k = []
⊢ TransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    (bif
        match [].head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := [].head?, stk := update S k [].tail }
    else { l := some (Λ'.clear p k q), var := [].head?, stk := update S k [].tail })
    { l := some q, var := o, stk := update S k L₂ }

pp: case cons.cons
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := o, stk := update S k L₂ }
s : Option Γ'
S : K' → List Γ'
a' : Γ'
Sk : List Γ'
e :
  (bif p a' then ([], some a', Sk)
    else
      match splitAtPred p Sk with
      | (l₁, o, l₂) => (a' :: l₁, o, l₂)) =
    (a :: L₁, o, L₂)
e₁ : S k = a' :: Sk
⊢ TransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    (bif
        match (a' :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (a' :: Sk).head?, stk := update S k (a' :: Sk).tail }
    else { l := some (Λ'.clear p k q), var := (a' :: Sk).head?, stk := update S k (a' :: Sk).tail })
    { l := some q, var := o, stk := update S k L₂ }

Tactic:
·

Goal state after:
case cons.nil
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := o, stk := update S k L₂ }
s : Option Γ'
S : K' → List Γ'
e : ([], none, []) = (a :: L₁, o, L₂)
e₁ : S k = []
⊢ TransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    (bif
        match [].head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := [].head?, stk := update S k [].tail }
    else { l := some (Λ'.clear p k q), var := [].head?, stk := update S k [].tail })
    { l := some q, var := o, stk := update S k L₂ }
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: A : Type u
inst✝⁹ : TopologicalSpace A
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.1 = f x.2}
D_comp : CompactSpace ↑D
X₁ : ↑D → A := Prod.fst ∘ Subtype.val
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : X₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.domRestrict X₁ '' E₀ ≠ univ
ρ : ↑E → A := E.domRestrict X₁
ρ_cont : Continuous ρ
⊢ ∃ h, Continuous h ∧ f ∘ h = φ

Tactic:
have ρ_surj : ρ.Surjective := fun a => by
    rcases (E_onto ▸ mem_univ a : a ∈ X₁ '' E) with ⟨d, ⟨hd, rfl⟩⟩; exact ⟨⟨d, hd⟩, rfl⟩

Goal state after:
A : Type u
inst✝⁹ : TopologicalSpace A
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.1 = f x.2}
D_comp : CompactSpace ↑D
X₁ : ↑D → A := Prod.fst ∘ Subtype.val
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : X₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.domRestrict X₁ '' E₀ ≠ univ
ρ : ↑E → A := E.domRestrict X₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
⊢ ∃ h, Continuous h ∧ f ∘ h = φ
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons.cons.true
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := o, stk := update S k L₂ }
s : Option Γ'
S : K' → List Γ'
a' : Γ'
Sk : List Γ'
e₁ : S k = a' :: Sk
e₂ : p a' = true
e : ([], some a', Sk) = (a :: L₁, o, L₂)
⊢ TransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    (bif
        match (a' :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (a' :: Sk).head?, stk := update S k (a' :: Sk).tail }
    else { l := some (Λ'.clear p k q), var := (a' :: Sk).head?, stk := update S k (a' :: Sk).tail })
    { l := some q, var := o, stk := update S k L₂ }

pp: case cons.cons.false
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := o, stk := update S k L₂ }
s : Option Γ'
S : K' → List Γ'
a' : Γ'
Sk : List Γ'
e₁ : S k = a' :: Sk
e₂ : p a' = false
e : (a' :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2) = (a :: L₁, o, L₂)
⊢ TransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    (bif
        match (a' :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (a' :: Sk).head?, stk := update S k (a' :: Sk).tail }
    else { l := some (Λ'.clear p k q), var := (a' :: Sk).head?, stk := update S k (a' :: Sk).tail })
    { l := some q, var := o, stk := update S k L₂ }

Tactic:
·

Goal state after:
case cons.cons.true
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := o, stk := update S k L₂ }
s : Option Γ'
S : K' → List Γ'
a' : Γ'
Sk : List Γ'
e₁ : S k = a' :: Sk
e₂ : p a' = true
e : ([], some a', Sk) = (a :: L₁, o, L₂)
⊢ TransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    (bif
        match (a' :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (a' :: Sk).head?, stk := update S k (a' :: Sk).tail }
    else { l := some (Λ'.clear p k q), var := (a' :: Sk).head?, stk := update S k (a' :: Sk).tail })
    { l := some q, var := o, stk := update S k L₂ }
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case hf
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
⊢ IsOpenMap (Sigma.mk i)

pp: case hfc
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
⊢ Continuous (Sigma.mk i)

Tactic:
·

Goal state after:
case hf
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
⊢ IsOpenMap (Sigma.mk i)
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case pos
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
U : Set (X i)
a✝ : IsOpen U
j : ι
ij : i = j
⊢ IsOpen (Sigma.mk j ⁻¹' Sigma.mk i '' U)

pp: case neg
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
U : Set (X i)
a✝ : IsOpen U
j : ι
ij : ¬i = j
⊢ IsOpen (Sigma.mk j ⁻¹' Sigma.mk i '' U)

Tactic:
·

Goal state after:
case pos
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
U : Set (X i)
a✝ : IsOpen U
j : ι
ij : i = j
⊢ IsOpen (Sigma.mk j ⁻¹' Sigma.mk i '' U)
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case neg
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
U : Set (X i)
a✝ : IsOpen U
j : ι
ij : ¬i = j
⊢ IsOpen (Sigma.mk j ⁻¹' Sigma.mk i '' U)

Tactic:
·

Goal state after:
case neg
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
U : Set (X i)
a✝ : IsOpen U
j : ι
ij : ¬i = j
⊢ IsOpen (Sigma.mk j ⁻¹' Sigma.mk i '' U)
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case hfc
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
⊢ Continuous (Sigma.mk i)

Tactic:
·

Goal state after:
case hfc
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
⊢ Continuous (Sigma.mk i)
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case pos
X : Type u
inst✝ : TopologicalSpace X
h : PreirreducibleSpace X
U : Set X
hU : IsOpen U
Un : U = ∅
⊢ IsOpen (closure U)

pp: case neg
X : Type u
inst✝ : TopologicalSpace X
h : PreirreducibleSpace X
U : Set X
hU : IsOpen U
Un : U.Nonempty
⊢ IsOpen (closure U)

Tactic:
·

Goal state after:
case pos
X : Type u
inst✝ : TopologicalSpace X
h : PreirreducibleSpace X
U : Set X
hU : IsOpen U
Un : U = ∅
⊢ IsOpen (closure U)
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case neg
X : Type u
inst✝ : TopologicalSpace X
h : PreirreducibleSpace X
U : Set X
hU : IsOpen U
Un : U.Nonempty
⊢ IsOpen (closure U)

Tactic:
·

Goal state after:
case neg
X : Type u
inst✝ : TopologicalSpace X
h : PreirreducibleSpace X
U : Set X
hU : IsOpen U
Un : U.Nonempty
⊢ IsOpen (closure U)
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case inl
X : Type u
inst✝ : TopologicalSpace X
h : ExtremallyDisconnected X
h' : PreconnectedSpace X
s : Set X
hs : IsOpen s
sn : s.Nonempty
h✝ : closure s = ∅
⊢ closure s = univ

pp: case inr
X : Type u
inst✝ : TopologicalSpace X
h : ExtremallyDisconnected X
h' : PreconnectedSpace X
s : Set X
hs : IsOpen s
sn : s.Nonempty
h✝ : closure s = univ
⊢ closure s = univ

Tactic:
·

Goal state after:
case inl
X : Type u
inst✝ : TopologicalSpace X
h : ExtremallyDisconnected X
h' : PreconnectedSpace X
s : Set X
hs : IsOpen s
sn : s.Nonempty
h✝ : closure s = ∅
⊢ closure s = univ
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case inr
X : Type u
inst✝ : TopologicalSpace X
h : ExtremallyDisconnected X
h' : PreconnectedSpace X
s : Set X
hs : IsOpen s
sn : s.Nonempty
h✝ : closure s = univ
⊢ closure s = univ

Tactic:
·

Goal state after:
case inr
X : Type u
inst✝ : TopologicalSpace X
h : ExtremallyDisconnected X
h' : PreconnectedSpace X
s : Set X
hs : IsOpen s
sn : s.Nonempty
h✝ : closure s = univ
⊢ closure s = univ
Module: Mathlib.Topology.Category.Profinite.EffectiveEpi

Goal state before:
pp: B X : Profinite
π : X ⟶ B
tfae_1_to_2 : EffectiveEpi π → Epi π
tfae_2_iff_3 : Epi π ↔ Function.Surjective ⇑(ConcreteCategory.hom π)
tfae_3_to_1 : Function.Surjective ⇑(ConcreteCategory.hom π) → EffectiveEpi π
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE

Tactic:
tfae_finish

Goal state after:
Module: Mathlib.Topology.Category.Profinite.EffectiveEpi

Goal state before:
pp: α : Type
inst✝ : Finite α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
x✝ : Epi (Sigma.desc π)
⊢ EffectiveEpiFamily X π

Tactic:
by
    simpa [← effectiveEpi_desc_iff_effectiveEpiFamily, (effectiveEpi_tfae (Sigma.desc π)).out 0 1]

Goal state after:
Module: Mathlib.Topology.Category.Profinite.EffectiveEpi

Goal state before:
pp: α : Type
inst✝ : Finite α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
tfae_3_iff_1 : (∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b) ↔ EffectiveEpiFamily X π
⊢ [EffectiveEpiFamily X π, Epi (Sigma.desc π), ∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b].TFAE

Tactic:
tfae_finish

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case inl
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trNat a
⊢ x ≠ Γ'.consₗ

pp: case inr.inl
a : ℕ
l : List ℕ
⊢ Γ'.cons ≠ Γ'.consₗ

pp: case inr.inr
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trList l
⊢ x ≠ Γ'.consₗ

Tactic:
·

Goal state after:
case inl
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trNat a
⊢ x ≠ Γ'.consₗ
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case inr.inl
a : ℕ
l : List ℕ
⊢ Γ'.cons ≠ Γ'.consₗ

pp: case inr.inr
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trList l
⊢ x ≠ Γ'.consₗ

Tactic:
·

Goal state after:
case inr.inl
a : ℕ
l : List ℕ
⊢ Γ'.cons ≠ Γ'.consₗ
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case inr.inr
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trList l
⊢ x ≠ Γ'.consₗ

Tactic:
·

Goal state after:
case inr.inr
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trList l
⊢ x ≠ Γ'.consₗ
Module: Mathlib.Topology.Category.Stonean.EffectiveEpi

Goal state before:
pp: B X : Stonean
π : X ⟶ B
tfae_1_to_2 : EffectiveEpi π → Epi π
tfae_2_iff_3 : Epi π ↔ Function.Surjective ⇑(ConcreteCategory.hom π)
tfae_3_to_1 : Function.Surjective ⇑(ConcreteCategory.hom π) → EffectiveEpi π
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE

Tactic:
tfae_finish

Goal state after:
Module: Mathlib.Topology.Category.Stonean.EffectiveEpi

Goal state before:
pp: α : Type
inst✝ : Finite α
B : Stonean
X : α → Stonean
π : (a : α) → X a ⟶ B
x✝ : Epi (Sigma.desc π)
⊢ EffectiveEpiFamily X π

Tactic:
by
    simpa [← effectiveEpi_desc_iff_effectiveEpiFamily, (effectiveEpi_tfae (Sigma.desc π)).out 0 1]

Goal state after:
Module: Mathlib.Topology.Category.Stonean.EffectiveEpi

Goal state before:
pp: α : Type
inst✝ : Finite α
B : Stonean
X : α → Stonean
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
tfae_3_iff_1 : (∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b) ↔ EffectiveEpiFamily X π
⊢ [EffectiveEpiFamily X π, Epi (Sigma.desc π), ∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b].TFAE

Tactic:
tfae_finish

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case refine_1
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn L none fun x x_1 ↦ some Γ'.cons
⊢ Option.elim' (elim (trList L) [] c d main = trNat L.headI ∧ trList L.tail = [])
    (fun a ↦ natEnd a = true ∧ elim (trList L) [] c d main = trNat L.headI ++ a :: trList L.tail) o

pp: case refine_2
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn L none fun x x_1 ↦ some Γ'.cons
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (TM2.stepAux
      (tr
        ((fun x ↦
            Λ'.read fun s ↦ (if s = some Γ'.consₗ then id else Λ'.clear (fun x ↦ decide (x = Γ'.consₗ)) main) (unrev q))
          o))
      o
      (update
        (update (update (elim (trList L) [] c d) main (trList L.tail)) rev
          ((trNat L.headI).reverseAux (elim (trList L) [] c d rev)))
        rev
        ((fun s ↦ ((fun x ↦ some Γ'.cons) s).getD default) o ::
          update (update (elim (trList L) [] c d) main (trList L.tail)) rev
            ((trNat L.headI).reverseAux (elim (trList L) [] c d rev)) rev)))
    { l := some q, var := none, stk := elim (trList [L.headI]) [] c d }

Tactic:
·

Goal state after:
case refine_1
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn L none fun x x_1 ↦ some Γ'.cons
⊢ Option.elim' (elim (trList L) [] c d main = trNat L.headI ∧ trList L.tail = [])
    (fun a ↦ natEnd a = true ∧ elim (trList L) [] c d main = trNat L.headI ++ a :: trList L.tail) o
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case refine_2.refine_1
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn L none fun x x_1 ↦ some Γ'.cons
⊢ ∀ x ∈ elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d main,
    decide (x = Γ'.consₗ) = false

pp: case refine_2.refine_2
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn L none fun x x_1 ↦ some Γ'.cons
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    { l := some (unrev q), var := none,
      stk := update (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d) main [] }
    { l := some q, var := none, stk := elim (trNat L.headI ++ [Γ'.cons]) [] c d }

Tactic:
·

Goal state after:
case refine_2.refine_1
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn L none fun x x_1 ↦ some Γ'.cons
⊢ ∀ x ∈ elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d main,
    decide (x = Γ'.consₗ) = false