mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case comp
k' : Cont
c c' : Code
a_ih✝ : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
ih' : ∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k'
k : Cont
v : List ℕ
⊢ stepNormal c' (Cont.comp c (k.then k')) v = stepNormal c' ((Cont.comp c k).then k') v

Tactic:
Cont.then

Goal state after:
case comp
k' : Cont
c c' : Code
a_ih✝ : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
ih' : ∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k'
k : Cont
v : List ℕ
⊢ stepNormal c' (Cont.comp c (k.then k')) v = stepNormal c' ((fun k' ↦ Cont.comp c (k.then k')) k') v
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case fix
k' : Cont
c : Code
ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
k : Cont
v : List ℕ
⊢ stepNormal c (Cont.fix c (k.then k')) v = stepNormal c ((Cont.fix c k).then k') v

Tactic:
Cont.then

Goal state after:
case fix
k' : Cont
c : Code
ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
k : Cont
v : List ℕ
⊢ stepNormal c (Cont.fix c (k.then k')) v = stepNormal c ((fun k' ↦ Cont.fix c (k.then k')) k') v
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case succ
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
k : K
o : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
v : σ
S : List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse
n : ℕ
IH :
  n ≤ S.length →
    Reaches₀ (TM1.step (tr M)) { l := some (go k o q), var := v, Tape := Tape.mk' ∅ (addBottom L) }
      { l := some (go k o q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
H : n + 1 ≤ S.length
⊢ n < S.reverse.length

Tactic:
rwa [List.length_reverse]

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

Goal state before:
pp: f : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f a = b)
f' : Option Γ' → Λ'
⊢ Decidable (read f = read f')

Tactic:
exact decidable_of_iff' (∀ a, f a = f' a) (by simp [funext_iff])

Goal state after:
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
hx : ⋂ s, ↑s = {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := { s // IsClopen s ∧ x ∈ s }
this : Nonempty N
hNcl : ∀ (s : N), IsClosed[inst✝³] ↑s
hdir : Directed GE.ge fun s ↦ ↑s
y : X
y_in : y ∈ ⋂ s, ↑s
⊢ U ∈ 𝓝 y

Tactic:
rw [hx, mem_singleton_iff] at y_in

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
hx : ⋂ s, ↑s = {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := { s // IsClopen s ∧ x ∈ s }
this : Nonempty N
hNcl : ∀ (s : N), IsClosed[inst✝³] ↑s
hdir : Directed GE.ge fun s ↦ ↑s
y : X
y_in : y = x
⊢ U ∈ 𝓝 y
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: case of_equiv
X : Type u_4
I : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : TotallyDisconnectedSpace X
inst✝ : Finite I
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
IH :
  ∀ {Z D : α✝ → Set X},
    (∀ (i : α✝), IsClosed[inst✝⁴] (Z i)) →
      (∀ (i : α✝), IsClopen (D i)) →
        (∀ (i : α✝), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : α✝), IsClopen (C i)) ∧
                (∀ (i : α✝), Z i ⊆ C i) ∧ (∀ (i : α✝), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : β✝ → Set X
Z_closed : ∀ (i : β✝), IsClosed[inst✝⁴] (Z i)
D_clopen : ∀ (i : β✝), IsClopen (D i)
Z_subset_D : ∀ (i : β✝), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
⊢ ∃ C,
    (∀ (i : β✝), IsClopen (C i)) ∧
      (∀ (i : β✝), Z i ⊆ C i) ∧ (∀ (i : β✝), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C

Tactic:
obtain ⟨C, h1, h2, h3, h4, h5⟩ := IH (Z := Z ∘ e) (D := D ∘ e)
      (fun i ↦ Z_closed (e i)) (fun i ↦ D_clopen (e i))
      (fun i ↦ Z_subset_D (e i)) (by simpa [← e.injective.injOn.pairwiseDisjoint_image])

Goal state after:
case of_equiv
X : Type u_4
I : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : TotallyDisconnectedSpace X
inst✝ : Finite I
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
IH :
  ∀ {Z D : α✝ → Set X},
    (∀ (i : α✝), IsClosed[inst✝⁴] (Z i)) →
      (∀ (i : α✝), IsClopen (D i)) →
        (∀ (i : α✝), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : α✝), IsClopen (C i)) ∧
                (∀ (i : α✝), Z i ⊆ C i) ∧ (∀ (i : α✝), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : β✝ → Set X
Z_closed : ∀ (i : β✝), IsClosed[inst✝⁴] (Z i)
D_clopen : ∀ (i : β✝), IsClopen (D i)
Z_subset_D : ∀ (i : β✝), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
C : α✝ → Set X
h1 : ∀ (i : α✝), IsClopen (C i)
h2 : ∀ (i : α✝), (Z ∘ ⇑e) i ⊆ C i
h3 : ∀ (i : α✝), C i ⊆ (D ∘ ⇑e) i
h4 : ⋃ i, (D ∘ ⇑e) i ⊆ ⋃ i, C i
h5 : univ.PairwiseDisjoint C
⊢ ∃ C,
    (∀ (i : β✝), IsClopen (C i)) ∧
      (∀ (i : β✝), Z i ⊆ C i) ∧ (∀ (i : β✝), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: X : Type u_4
I : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : TotallyDisconnectedSpace X
inst✝ : Finite I
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
IH :
  ∀ {Z D : α✝ → Set X},
    (∀ (i : α✝), IsClosed[inst✝⁴] (Z i)) →
      (∀ (i : α✝), IsClopen (D i)) →
        (∀ (i : α✝), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : α✝), IsClopen (C i)) ∧
                (∀ (i : α✝), Z i ⊆ C i) ∧ (∀ (i : α✝), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : β✝ → Set X
Z_closed : ∀ (i : β✝), IsClosed[inst✝⁴] (Z i)
D_clopen : ∀ (i : β✝), IsClopen (D i)
Z_subset_D : ∀ (i : β✝), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
C : α✝ → Set X
h1 : ∀ (i : α✝), IsClopen (C i)
h2 : ∀ (i : α✝), (Z ∘ ⇑e) i ⊆ C i
h3 : ∀ (i : α✝), C i ⊆ (D ∘ ⇑e) i
h4 : ⋃ i, (D ∘ ⇑e) i ⊆ ⋃ i, C i
h5 : univ.PairwiseDisjoint C
i : β✝
⊢ (C ∘ ⇑e.symm) i ⊆ D i

Tactic:
by simpa using h3 (e.symm i)

Goal state after:
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: case of_equiv
X : Type u_4
I : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : TotallyDisconnectedSpace X
inst✝ : Finite I
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
IH :
  ∀ {Z D : α✝ → Set X},
    (∀ (i : α✝), IsClosed[inst✝⁴] (Z i)) →
      (∀ (i : α✝), IsClopen (D i)) →
        (∀ (i : α✝), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : α✝), IsClopen (C i)) ∧
                (∀ (i : α✝), Z i ⊆ C i) ∧ (∀ (i : α✝), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : β✝ → Set X
Z_closed : ∀ (i : β✝), IsClosed[inst✝⁴] (Z i)
D_clopen : ∀ (i : β✝), IsClopen (D i)
Z_subset_D : ∀ (i : β✝), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
C : α✝ → Set X
h1 : ∀ (i : α✝), IsClopen (C i)
h2 : ∀ (i : α✝), (Z ∘ ⇑e) i ⊆ C i
h3 : ∀ (i : α✝), C i ⊆ (D ∘ ⇑e) i
h5 : univ.PairwiseDisjoint C
h4 : ∀ (i : α✝), D (e i) ⊆ ⋃ i, C i
⊢ ⋃ i, D i ⊆ ⋃ i, (C ∘ ⇑e.symm) i

Tactic:
simpa [e.symm.surjective.iUnion_comp C] using fun i ↦ h4 (e.symm i)

Goal state after:
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: X : Type u_4
I✝ : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : CompactSpace X
inst✝³ : T2Space X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : Finite I✝
I : Type u_5
inst✝ : Fintype I
IH :
  ∀ {Z D : I → Set X},
    (∀ (i : I), IsClosed[inst✝⁵] (Z i)) →
      (∀ (i : I), IsClopen (D i)) →
        (∀ (i : I), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : I), IsClopen (C i)) ∧
                (∀ (i : I), Z i ⊆ C i) ∧ (∀ (i : I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst✝⁵] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
Z' : I → Set X := fun i ↦ Z (some i)
Z'_closed : ∀ (i : I), IsClosed[inst✝⁵] (Z (some i))
Z'_disj : univ.PairwiseDisjoint (Z ∘ some)
U : Set X := D none \ ⋃ i, Z (some i)
U_open : IsOpen[inst✝⁵] U
i : I
⊢ Disjoint (Z none) (Z (some i))

Tactic:
apply Z_disj; all_goals simp

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

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

Tactic:
rcases e₁ : S k₁ with - | ⟨a', Sk⟩

Goal state after:
case cons.nil
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k₁) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.move p k₁ k₂ q), var := s, stk := S }
        { l := some q, var := o, stk := update (update S k₁ L₂) k₂ (L₁.reverseAux (S k₂)) }
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k₁) = (a :: L₁, o, L₂)
e₁ : S k₁ = []
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (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 (Λ'.move p k₁ k₂ q), var := [].head?,
        stk := update (update S k₁ [].tail) k₂ ([].head?.getD default :: update S k₁ [].tail k₂) })
    { l := some q, var := o, stk := update (update S k₁ L₂) k₂ ((a :: L₁).reverseAux (S k₂)) }

case cons.cons
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k₁) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.move p k₁ k₂ q), var := s, stk := S }
        { l := some q, var := o, stk := update (update S k₁ L₂) k₂ (L₁.reverseAux (S k₂)) }
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k₁) = (a :: L₁, o, L₂)
a' : Γ'
Sk : List Γ'
e₁ : S k₁ = a' :: Sk
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (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 (Λ'.move p k₁ k₂ q), var := (a' :: Sk).head?,
        stk :=
          update (update S k₁ (a' :: Sk).tail) k₂ ((a' :: Sk).head?.getD default :: update S k₁ (a' :: Sk).tail k₂) })
    { l := some q, var := o, stk := update (update S k₁ L₂) k₂ ((a :: L₁).reverseAux (S k₂)) }
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case e_a
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ eval step (stepRet k (v.headI :: v')) = do
    let a ← k.eval (v.headI :: v')
    pure (Cfg.halt a)

Tactic:
IH,

Goal state after:
case e_a
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ Cfg.halt <$> k.eval (v.headI :: v') = do
    let a ← k.eval (v.headI :: v')
    pure (Cfg.halt a)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case e_a
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ eval step (stepRet k v') = do
    let a ← k.eval v'
    pure (Cfg.halt a)

Tactic:
IH,

Goal state after:
case e_a
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ Cfg.halt <$> k.eval v' = do
    let a ← k.eval v'
    pure (Cfg.halt a)
Module: Mathlib.Topology.Category.Profinite.Basic

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Profinite
S : Limits.Cone F
x✝ : S.pt ⟶ (limitCone F).pt
h : ∀ (j : J), x✝ ≫ (limitCone F).π.app j = S.π.app j
j : J
⊢ profiniteToCompHaus.map x✝ ≫ (CompHaus.limitCone (F ⋙ profiniteToCompHaus)).π.app j =
    (profiniteToCompHaus.mapCone S).π.app j

Tactic:
by
          simp [← h]
          rfl

Goal state after:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
Y Z : Type u
⊢ ∀ [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace Z] [CompactSpace Y] [T2Space Y] [CompactSpace Z] [T2Space Z]
    {f : StoneCech X → Z} {g : Y → Z}, Continuous f → Continuous g → Surjective g → ∃ h, Continuous h ∧ g ∘ h = f

Tactic:
_tsY

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
⊢ ∀ [inst : TopologicalSpace Z] [CompactSpace Y] [T2Space Y] [CompactSpace Z] [T2Space Z] {f : StoneCech X → Z}
    {g : Y → Z}, Continuous f → Continuous g → Surjective g → ∃ h, Continuous h ∧ g ∘ h = f
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: 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}
this : ∀ C ⊆ S, IsChain (fun x1 x2 ↦ x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c
E : Set D
E_min : Minimal (fun x ↦ x ∈ S) E
E_closed : IsClosed E
E_surj : X '' E = univ
⊢ ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.domRestrict X '' E₀ ≠ univ

Tactic:
intro E₀ E₀_min E₀_closed

Goal state after:
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}
this : ∀ C ⊆ S, IsChain (fun x1 x2 ↦ x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c
E : Set D
E_min : Minimal (fun x ↦ x ∈ S) E
E_closed : IsClosed E
E_surj : X '' E = univ
E₀ : Set ↑E
E₀_min : E₀ ≠ univ
E₀_closed : IsClosed E₀
⊢ E.domRestrict X '' E₀ ≠ univ
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: 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}
⊢ ∃ E, CompactSpace ↑E ∧ X '' E = univ ∧ ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.domRestrict X '' E₀ ≠ univ

Tactic:
suffices ∀ (C : Set <| Set D) (_ : C ⊆ S) (_ : IsChain (· ⊆ ·) C), ∃ s ∈ S, ∀ c ∈ C, s ⊆ c by
    rcases zorn_superset S this with ⟨E, E_min⟩
    obtain ⟨E_closed, E_surj⟩ := E_min.prop
    refine ⟨E, isCompact_iff_compactSpace.mp E_closed.isCompact, E_surj, ?_⟩
    intro E₀ E₀_min E₀_closed
    contrapose E₀_min
    exact eq_univ_of_image_val_eq <|
      E_min.eq_of_subset ⟨E₀_closed.trans E_closed, image_image_val_eq_domRestrict_image ▸ E₀_min⟩
        image_val_subset

Goal state after:
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 ⊆ S, IsChain (fun x1 x2 ↦ x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: 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)
h : Sigma.mk i ⁻¹' closure s = closure (Sigma.mk i ⁻¹' s)
⊢ IsOpen (Sigma.mk i ⁻¹' closure s)

Tactic:
by
    rw [h]
    exact h₀ _ (hs i)

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

Goal state before:
pp: case cons
f fs : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal f (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
a_ih✝ :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal fs k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal fs (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
k : Cont
v : List ℕ
s : Option Γ'
c : Cfg'
h₁ : TrCfg (stepNormal f (Cont.cons₁ fs v k) v) c
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal f (trCont (Cont.cons₁ fs v k))), var := none,
      stk := elim (trList v) [] [] (trContStack (Cont.cons₁ fs v k)) }
    c
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    { l := some (trNormal f (Cont'.cons₁ fs (trCont k))), var := none,
      stk :=
        elim ((trList v).reverse.reverseAux []) [] []
          ((trList v).reverse.reverseAux ((some Γ'.consₗ).getD default :: trContStack k)) }
    c

Tactic:
convert! h₂ using 2

Goal state after:
case e'_1.e'_7
f fs : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal f (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
a_ih✝ :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal fs k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal fs (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
k : Cont
v : List ℕ
s : Option Γ'
c : Cfg'
h₁ : TrCfg (stepNormal f (Cont.cons₁ fs v k) v) c
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal f (trCont (Cont.cons₁ fs v k))), var := none,
      stk := elim (trList v) [] [] (trContStack (Cont.cons₁ fs v k)) }
    c
⊢ elim ((trList v).reverse.reverseAux []) [] []
      ((trList v).reverse.reverseAux ((some Γ'.consₗ).getD default :: trContStack k)) =
    elim (trList v) [] [] (trContStack (Cont.cons₁ fs v k))
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case move
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.move p✝ k₁✝ k₂✝ q)
HS₁ : insert (Λ'.move p✝ k₁✝ k₂✝ q) (trStmts₁ q) ⊆ S
⊢ Supports (insert (Λ'.move p✝ k₁✝ k₂✝ q) (trStmts₁ q)) S

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁

Goal state after:
case move
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.move p✝ k₁✝ k₂✝ q)
HS₁ : insert (Λ'.move p✝ k₁✝ k₂✝ q) (trStmts₁ q) ⊆ S
h₁ : Λ'.move p✝ k₁✝ k₂✝ q ∈ S
h₂ : trStmts₁ q ⊆ S
⊢ Supports (insert (Λ'.move p✝ k₁✝ k₂✝ q) (trStmts₁ q)) S
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case clear
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
p✝ : Γ' → Bool
k✝ : K'
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.clear p✝ k✝ q)
HS₁ : insert (Λ'.clear p✝ k✝ q) (trStmts₁ q) ⊆ S
⊢ Supports (insert (Λ'.clear p✝ k✝ q) (trStmts₁ q)) S

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁

Goal state after:
case clear
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
p✝ : Γ' → Bool
k✝ : K'
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.clear p✝ k✝ q)
HS₁ : insert (Λ'.clear p✝ k✝ q) (trStmts₁ q) ⊆ S
h₁ : Λ'.clear p✝ k✝ q ∈ S
h₂ : trStmts₁ q ⊆ S
⊢ Supports (insert (Λ'.clear p✝ k✝ q) (trStmts₁ q)) S
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case copy
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.copy
HS₁ : insert q.copy (trStmts₁ q) ⊆ S
⊢ Supports (insert q.copy (trStmts₁ q)) S

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁

Goal state after:
case copy
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.copy
HS₁ : insert q.copy (trStmts₁ q) ⊆ S
h₁ : q.copy ∈ S
h₂ : trStmts₁ q ⊆ S
⊢ Supports (insert q.copy (trStmts₁ q)) S
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case push
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
k✝ : K'
s✝ : Option Γ' → Option Γ'
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.push k✝ s✝ q)
HS₁ : insert (Λ'.push k✝ s✝ q) (trStmts₁ q) ⊆ S
⊢ Supports (insert (Λ'.push k✝ s✝ q) (trStmts₁ q)) S

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁

Goal state after:
case push
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
k✝ : K'
s✝ : Option Γ' → Option Γ'
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.push k✝ s✝ q)
HS₁ : insert (Λ'.push k✝ s✝ q) (trStmts₁ q) ⊆ S
h₁ : Λ'.push k✝ s✝ q ∈ S
h₂ : trStmts₁ q ⊆ S
⊢ Supports (insert (Λ'.push k✝ s✝ q) (trStmts₁ q)) S
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case read
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), Λ'.Supports S (q a) → trStmts₁ (q a) ⊆ S → Supports (trStmts₁ (q a)) S
H₁ : Λ'.Supports S (Λ'.read q)
HS₁ : insert (Λ'.read q) (Finset.univ.biUnion fun s ↦ trStmts₁ (q s)) ⊆ S
⊢ Supports (insert (Λ'.read q) (Finset.univ.biUnion fun s ↦ trStmts₁ (q s))) S

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁

Goal state after:
case read
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), Λ'.Supports S (q a) → trStmts₁ (q a) ⊆ S → Supports (trStmts₁ (q a)) S
H₁ : Λ'.Supports S (Λ'.read q)
HS₁ : insert (Λ'.read q) (Finset.univ.biUnion fun s ↦ trStmts₁ (q s)) ⊆ S
h₁ : Λ'.read q ∈ S
h₂ : (Finset.univ.biUnion fun s ↦ trStmts₁ (q s)) ⊆ S
⊢ Supports (insert (Λ'.read q) (Finset.univ.biUnion fun s ↦ trStmts₁ (q s))) S
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case succ
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.succ
HS₁ : insert q.succ (insert (unrev q) (trStmts₁ q)) ⊆ S
⊢ Supports (insert q.succ (insert (unrev q) (trStmts₁ q))) S

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁

Goal state after:
case succ
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.succ
HS₁ : insert q.succ (insert (unrev q) (trStmts₁ q)) ⊆ S
h₁ : q.succ ∈ S
h₂ : insert (unrev q) (trStmts₁ q) ⊆ S
⊢ Supports (insert q.succ (insert (unrev q) (trStmts₁ q))) S