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

Goal state before:
pp: Γ : Type ?u.8
Γ' : Type ?u.12
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
l✝ : ListBlank Γ
f : Γ → List Γ'
l : List Γ
i n : ℕ
e : f default = List.replicate n default
⊢ List.flatMap f l ++ List.flatMap f (List.replicate i default) = List.flatMap f l ++ List.replicate (n * i) default

Tactic:
congr

Goal state after:
case e_a
Γ : Type ?u.8
Γ' : Type ?u.12
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
l✝ : ListBlank Γ
f : Γ → List Γ'
l : List Γ
i n : ℕ
e : f default = List.replicate n default
⊢ List.flatMap f (List.replicate i default) = List.replicate (n * i) default
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case pos.mp.inl
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
t u : List α
h✝ : x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true
⊢ ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

pp: case pos.mp.inr
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
h : (Q.deriv a).rmatch x = true
⊢ ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
· exact ⟨a :: t, u, by tauto⟩

Goal state after:
case pos.mp.inr
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
h : (Q.deriv a).rmatch x = true
⊢ ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case neg.mp
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
t u : List α
h : x = t ++ u
hP : (P.deriv a).rmatch t = true
hQ : Q.rmatch u = true
⊢ ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

pp: case neg.mpr
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
t u : List α
h : a :: x = t ++ u
hP : P.rmatch t = true
hQ : Q.rmatch u = true
⊢ ∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true

Tactic:
· exact ⟨a :: t, u, by tauto⟩

Goal state after:
case neg.mpr
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
t u : List α
h : a :: x = t ++ u
hP : P.rmatch t = true
hQ : Q.rmatch u = true
⊢ ∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
this :
  ∀ (i : ℕ) (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
hf : ∀ (a : Γ), SupportsStmt S (f✝ a)
⊢ ∀ (v : List.Vector Bool n), SupportsStmt S (move n Dir.left (f✝ (dec v)))

Tactic:
by intro; simp only [supportsStmt_move, hf]

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

Goal state before:
pp: case succ
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n✝ : ℕ
⊢ ListBlank.cons (true, L.head)
      (ListBlank.modifyNth (fun a ↦ (a.1, f a.2)) n✝ (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail)) =
    ListBlank.cons (true, L.head) (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } (ListBlank.modifyNth f n✝ L.tail))

Tactic:
congr

Goal state after:
case e_l
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n✝ : ℕ
⊢ ListBlank.modifyNth (fun a ↦ (a.1, f a.2)) n✝ (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail) =
    ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } (ListBlank.modifyNth f n✝ L.tail)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑(pos m) >>> n = ↑(pos m.bit1) >>> (n + 1)

Tactic:
change Nat.shiftRight m n = Nat.shiftRight (m + m + 1) (n + 1)

Goal state after:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ (↑m).shiftRight n = (↑m + ↑m + 1).shiftRight (n + 1)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ (↑m).shiftRight n = (↑m + ↑m + 1) >>> (1 + n)

Tactic:
Nat.shiftRight_add

Goal state after:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ (↑m).shiftRight n = (↑m + ↑m + 1) >>> 1 >>> n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ (↑m).shiftRight n = (↑m + ↑m) >>> (1 + n)

Tactic:
Nat.shiftRight_add

Goal state after:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ (↑m).shiftRight n = (↑m + ↑m) >>> 1 >>> n
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case right
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
⊢ TM1.stepAux q (f v ((Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L)))).head.2 k))
      ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L))) =
    TM1.stepAux q (f v (S k).head?) ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L)))

Tactic:
congr

Goal state after:
case right.e_a.e_a
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
⊢ (Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L)))).head.2 k = (S k).head?
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
a : α
x : ↑(X a).toTop
⊢ ∀ ⦃a₂ : (fun X ↦ ↑X.toTop) (X a)⦄, (ConcreteCategory.hom (ι X a)) x = (ConcreteCategory.hom (ι X a)) a₂ → x = a₂

Tactic:
y

Goal state after:
P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
a : α
x y : ↑(X a).toTop
⊢ (ConcreteCategory.hom (ι X a)) x = (ConcreteCategory.hom (ι X a)) y → x = y
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case fix
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, (a✝.then k').eval v = a✝.eval v >>= k'.eval
v : List ℕ
⊢ (if v.headI = 0 then a✝.eval v.tail >>= k'.eval else a✝¹.fix.eval v.tail >>= (a✝.then k').eval) =
    (if v.headI = 0 then a✝.eval v.tail else a✝¹.fix.eval v.tail >>= a✝.eval) >>= k'.eval

Tactic:
split_ifs <;> [rfl; simp only [← k_ih, bind_assoc]]

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

Goal state before:
pp: c : Code
h : c.Ok
v : List ℕ
⊢ (do
      let v ← c.eval v
      StateTransition.eval step (Cfg.ret Cont.halt v)) =
    do
    let a ← c.eval v
    pure (Cfg.halt a)

Tactic:
congr

Goal state after:
case e_a
c : Code
h : c.Ok
v : List ℕ
⊢ (fun v ↦ StateTransition.eval step (Cfg.ret Cont.halt v)) = fun a ↦ pure (Cfg.halt a)
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 Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
IH :
  Reaches₀ (TM1.step (tr M))
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
    { l := some (ret q), var := v, Tape := Tape.mk' ∅ (addBottom L) }
⊢ (bif false then
      TM1.stepAux (trNormal q) v ((Tape.move Dir.right ∘ (Tape.move Dir.right)^[n]) (Tape.mk' ∅ (addBottom L)))
    else
      TM1.stepAux (goto fun x x_1 ↦ ret q) v
        (Tape.move Dir.left ((Tape.move Dir.right ∘ (Tape.move Dir.right)^[n]) (Tape.mk' ∅ (addBottom L))))) =
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }

Tactic:
Function.comp_apply,

Goal state after:
case succ
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
IH :
  Reaches₀ (TM1.step (tr M))
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
    { l := some (ret q), var := v, Tape := Tape.mk' ∅ (addBottom L) }
⊢ (bif false then
      TM1.stepAux (trNormal q) v (Tape.move Dir.right ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L))))
    else
      TM1.stepAux (goto fun x x_1 ↦ ret q) v
        (Tape.move Dir.left (Tape.move Dir.right ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)))))) =
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst✝³] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x ↦ ↑↑x) = Subtype.val ∘ Subtype.val
f0 : IsEmbedding fun x ↦ ↑↑x
⊢ IsOpen[inst✝³] (range fun x ↦ ↑↑x)

Tactic:
have : Set.range ((↑) : u → H) = interior s := by
          rw [this, Set.range_comp, Subtype.range_coe, Subtype.image_preimage_coe]
          apply Set.inter_eq_self_of_subset_right interior_subset

Goal state after:
H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst✝³] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝¹ : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this✝ : (fun x ↦ ↑↑x) = Subtype.val ∘ Subtype.val
f0 : IsEmbedding fun x ↦ ↑↑x
this : (range fun x ↦ ↑↑x) = interior s
⊢ IsOpen[inst✝³] (range fun x ↦ ↑↑x)
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝² : DecidableEq K
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
⊢ { l := some default, var := default,
      Tape :=
        Tape.mk₁
          ((true, (List.map (fun a ↦ (false, update (fun x ↦ none) k (some a))) L.reverse).headI.2) ::
            (List.map (fun a ↦ (false, update (fun x ↦ none) k (some a))) L.reverse).tail) } =
    { l := Option.map normal (some default), var := default,
      Tape := Tape.mk' ∅ (addBottom (ListBlank.mk (List.map (fun a ↦ update default k (some a)) L.reverse))) }

Tactic:
congr

Goal state after:
case e_Tape.e_head.e_snd
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝² : DecidableEq K
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
⊢ (List.map (fun a ↦ (false, update (fun x ↦ none) k (some a))) L.reverse).headI.2 =
    (ListBlank.mk (List.map (fun a ↦ update default k (some a)) L.reverse)).head

case e_Tape.e_tail
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝² : DecidableEq K
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
⊢ (List.map (fun a ↦ (false, update (fun x ↦ none) k (some a))) L.reverse).tail =
    List.map { f := Prod.mk false, map_pt' := ⋯ }.f (List.map (fun a ↦ update default k (some a)) L.reverse).tail
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case cons
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
⊢ (do
      let v_1 ← f.eval v
      eval step (Cfg.ret (Cont.cons₁ fs v k) v_1)) =
    do
    let x ← f.eval v
    let x_1 ← fs.eval v
    eval step (Cfg.ret k (x.headI :: x_1))

Tactic:
congr

Goal state after:
case e_a
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
⊢ (fun v_1 ↦ eval step (Cfg.ret (Cont.cons₁ fs v k) v_1)) = fun x ↦ do
    let x_1 ← fs.eval v
    eval step (Cfg.ret k (x.headI :: x_1))
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case e_a
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ (do
      let v_1 ← fs.eval v✝
      eval step (Cfg.ret (Cont.cons₂ v k) v_1)) =
    do
    let x ← fs.eval v✝
    eval step (Cfg.ret k (v.headI :: x))

Tactic:
congr

Goal state after:
case e_a
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ (fun v_1 ↦ eval step (Cfg.ret (Cont.cons₂ v k) v_1)) = fun x ↦ eval step (Cfg.ret k (v.headI :: x))
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case comp
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ (do
      let v ← g.eval v
      eval step (Cfg.ret (Cont.comp f k) v)) =
    do
    let x ← g.eval v
    let v ← f.eval x
    eval step (Cfg.ret k v)

Tactic:
congr

Goal state after:
case e_a
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ (fun v ↦ eval step (Cfg.ret (Cont.comp f k) v)) = fun x ↦ do
    let v ← f.eval x
    eval step (Cfg.ret k v)
Module: Mathlib.Computability.TuringMachine.Config

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

Tactic:
congr

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 : List ℕ
⊢ (fun v_1 ↦ eval step (Cfg.ret (Cont.cons₂ v k) v_1)) = fun x ↦ do
    let a ← k.eval (v.headI :: x)
    pure (Cfg.halt a)
Module: Mathlib.Computability.TuringMachine.Config

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

Tactic:
congr

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

Goal state before:
pp: case neg
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
h✝ : ¬v.headI = 0
⊢ (do
      let v ← f.fix.eval v.tail
      eval step (Cfg.ret k v)) =
    do
    let x ← f.fix.eval v.tail
    let a ← k.eval x
    pure (Cfg.halt a)

Tactic:
congr

Goal state after:
case e_a
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
h✝ : ¬v.headI = 0
⊢ (fun v ↦ eval step (Cfg.ret k v)) = fun x ↦ do
    let a ← k.eval x
    pure (Cfg.halt a)
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
a✝ : x ∈ univ
⊢ ∀ ⦃y : X⦄, y ∈ univ → x ≠ y → (fun x y ↦ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v) x y

Tactic:
y

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
a✝ : x ∈ univ
y : X
⊢ y ∈ univ → x ≠ y → (fun x y ↦ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v) x y
Module: Mathlib.Topology.Category.Profinite.Basic

Goal state before:
pp: X Y : Profinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : Profinite := of (ULift.{u, 0} (Fin 2))
g : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X)
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ Z := ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
x : ↑X.toTop
⊢ ↑({ toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }.toFun ((ConcreteCategory.hom f).toFun x)).down =
    ↑((ULift.up ∘ fun x ↦ if x ∈ V then 0 else 1) ((ConcreteCategory.hom f).toFun x)).down

Tactic:
Function.comp_apply,

Goal state after:
X Y : Profinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : Profinite := of (ULift.{u, 0} (Fin 2))
g : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X)
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ Z := ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
x : ↑X.toTop
⊢ ↑({ toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }.toFun ((ConcreteCategory.hom f).toFun x)).down =
    ↑{ down := if (ConcreteCategory.hom f).toFun x ∈ V then 0 else 1 }.down
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : ↑Z → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
x : X
⊢ ∃ a, f a = x

Tactic:
by_cases hx : x ∈ U

Goal state after:
case pos
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : ↑Z → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
x : X
hx : x ∈ U
⊢ ∃ a, f a = x

case neg
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : ↑Z → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
x : X
hx : x ∉ U
⊢ ∃ a, f a = x
Module: Mathlib.Topology.Category.Profinite.Basic

Goal state before:
pp: case mp
X Y : Profinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : Profinite := of (ULift.{u, 0} (Fin 2))
g : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X)
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ Z := ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
H : ((ConcreteCategory.hom h).toFun y).down = ((ULift.up ∘ fun x ↦ if x ∈ V then 0 else 1) y).down
⊢ False

Tactic:
Function.comp_apply,

Goal state after:
case mp
X Y : Profinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : Profinite := of (ULift.{u, 0} (Fin 2))
g : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X)
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ Z := ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
H : ((ConcreteCategory.hom h).toFun y).down = { down := if y ∈ V then 0 else 1 }.down
⊢ False
Module: Mathlib.Computability.TuringMachine.ToPartrec

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

Tactic:
simp only [trList, List.mem_append, List.mem_cons] at h
    obtain h | rfl | h := h
    · rintro rfl
      cases trNat_natEnd _ _ h
    · rintro ⟨⟩
    · exact trList_ne_consₗ l _ h

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

Goal state before:
pp: X Y : Stonean
f : X ⟶ Y
h : Epi f
⊢ ∀ (b : ↑Y.toTop), ∃ a, (ConcreteCategory.hom f) a = b

Tactic:
y

Goal state after:
X Y : Stonean
f : X ⟶ Y
h : Epi f
y : ↑Y.toTop
⊢ ∃ a, (ConcreteCategory.hom f) a = y
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
toSetoid✝¹ : Setoid X
isOpen_setOfPred_rel✝¹ : ∀ (x : X), IsOpen[inst✝] (ofPred (toSetoid✝¹ x))
toSetoid✝ : Setoid X
isOpen_setOfPred_rel✝ : ∀ (x : X), IsOpen[inst✝] (ofPred (toSetoid✝ x))
x✝ :
  { toSetoid := toSetoid✝¹, isOpen_setOfPred_rel := isOpen_setOfPred_rel✝¹ }.toSetoid =
    { toSetoid := toSetoid✝, isOpen_setOfPred_rel := isOpen_setOfPred_rel✝ }.toSetoid
⊢ { toSetoid := toSetoid✝¹, isOpen_setOfPred_rel := isOpen_setOfPred_rel✝¹ } =
    { toSetoid := toSetoid✝, isOpen_setOfPred_rel := isOpen_setOfPred_rel✝ }

Tactic:
congr

Goal state after: