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

Goal state before:
pp: case succ.comp
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.comp cg)) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.comp cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.comp cg)
lg : encode cg < encode (cf.comp cg)
⊢ ((evaln k cg n).bind fun x ↦
      lup
        (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.comp cg)))))
        (k' + 1, cf) x) =
    (evaln (k' + 1) cg n).bind fun x ↦ evaln (k' + 1) cf x

Tactic:
cases evaln k cg n

Goal state after:
case succ.comp.none
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.comp cg)) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.comp cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.comp cg)
lg : encode cg < encode (cf.comp cg)
⊢ (Option.none.bind fun x ↦
      lup
        (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.comp cg)))))
        (k' + 1, cf) x) =
    Option.none.bind fun x ↦ evaln (k' + 1) cf x

case succ.comp.some
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.comp cg)) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.comp cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.comp cg)
lg : encode cg < encode (cf.comp cg)
val✝ : ℕ
⊢ ((some val✝).bind fun x ↦
      lup
        (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.comp cg)))))
        (k' + 1, cf) x) =
    (some val✝).bind fun x ↦ evaln (k' + 1) cf x
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case lt
a b : PosNum
this : ↑a < ↑b
⊢ ↑a + ↑a < ↑b + ↑b + 1

pp: case eq
a b : PosNum
this : a = b
⊢ ↑a + ↑a < ↑b + ↑b + 1

pp: case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b + 1 < ↑a + ↑a

Tactic:
· exact Nat.le_succ_of_le (Nat.add_lt_add this this)

Goal state after:
case eq
a b : PosNum
this : a = b
⊢ ↑a + ↑a < ↑b + ↑b + 1

case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b + 1 < ↑a + ↑a
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b < ↑a + ↑a + 1

Tactic:
· exact Nat.le_succ_of_le (Nat.add_lt_add this this)

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: ⊢ 1 = Num.pos 1

Tactic:
norm_cast

Goal state after:
Module: Mathlib.Computability.Halting

Goal state before:
pp: C : Set Code
H : ∀ (cf cg : Code), cf.eval = cg.eval → (cf ∈ C ↔ cg ∈ C)
hC : ∀ (f : Code), f ∈ C ↔ f.eval ∈ eval '' C
h : C = ∅ ∨ C = Set.univ
⊢ ComputablePred fun c ↦ c ∈ C

Tactic:
by {
          obtain rfl | rfl := h <;> simpa [ComputablePred, Set.mem_empty_iff_false] using
            Computable.const _}

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.zero
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
m : PosNum
⊢ ↑(bif g true false then pos m else 0) = if g true false = true then ↑(pos m) else 0

Tactic:
cases g true false

Goal state after:
case pos.zero.false
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
m : PosNum
⊢ ↑(bif false then pos m else 0) = if false = true then ↑(pos m) else 0

case pos.zero.true
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
m : PosNum
⊢ ↑(bif true then pos m else 0) = if true = true then ↑(pos m) else 0
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case left.left
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
⊢ default.1 ∈ TM1.stmts M S

Tactic:
simp only [default, TM1.stmts, Finset.mem_insertNone, Option.mem_def, Option.some_inj,
        forall_eq', Finset.mem_biUnion]

Goal state after:
case left.left
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
⊢ ∃ a ∈ S, M default ∈ TM1.stmts₁ (M a)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
T : Tape Bool
⊢ ∀ (i : ℕ), stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)

Tactic:
intro i

Goal state after:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
T : Tape Bool
i : ℕ
⊢ stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
S : Finset (Λ' Γ Λ σ)
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
⊢ ∀ {i : ℕ}, SupportsStmt S ((Stmt.move d)^[i] q) = SupportsStmt S q

Tactic:
intro i

Goal state after:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
S : Finset (Λ' Γ Λ σ)
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
⊢ SupportsStmt S ((Stmt.move d)^[i] q) = SupportsStmt S q
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
⊢ ∀ (i : ℕ) (L : Tape Bool), (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L) = L

Tactic:
intro i

Goal state after:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
i : ℕ
⊢ ∀ (L : Tape Bool), (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L) = L
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case some
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
v : σ
L : ListBlank Γ
⊢ ∀ (q : Stmt Γ Λ σ) (R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux q v (Tape.mk' L R)))

Tactic:
intro q R

Goal state after:
case some
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
v : σ
L : ListBlank Γ
q : Stmt Γ Λ σ
R : ListBlank Γ
⊢ Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux q v (Tape.mk' L R)))
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case halt
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝¹ : Fintype Γ
inst✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
hs : SupportsStmt S Stmt.halt
hw : ∀ q' ∈ writes Stmt.halt, q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec Stmt.halt)

Tactic:
simp only [SupportsStmt, trNormal]

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P✝ : TopCat → Prop
α : Type w
inst✝² : Finite α
X : α → CompHausLike P✝
inst✝¹ : HasExplicitFiniteCoproduct X
P : TopCat → Prop
inst✝ : HasExplicitFiniteCoproducts P
P' : TopCat → Prop
h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop
⊢ PreservesFiniteCoproducts (toCompHausLike h)

Tactic:
have : PreservesFiniteCoproducts (toCompHausLike h ⋙ compHausLikeToTop P') :=
    inferInstanceAs (PreservesFiniteCoproducts (compHausLikeToTop _))

Goal state after:
P✝ : TopCat → Prop
α : Type w
inst✝² : Finite α
X : α → CompHausLike P✝
inst✝¹ : HasExplicitFiniteCoproduct X
P : TopCat → Prop
inst✝ : HasExplicitFiniteCoproducts P
P' : TopCat → Prop
h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop
this : PreservesFiniteCoproducts (toCompHausLike h ⋙ compHausLikeToTop P')
⊢ PreservesFiniteCoproducts (toCompHausLike h)
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)
⊢ TrCfg (TM2.init k L) ?m.33

Tactic:
refine ⟨ListBlank.mk (L.reverse.map fun a ↦ update default k (some a)), fun k' ↦ ?_⟩
    refine ListBlank.ext fun i ↦ ?_
    rw [ListBlank.map_mk, ListBlank.nth_mk, List.getI_eq_getElem?_getD, List.map_map]
    have : ((proj k').f ∘ fun a => update (β := fun k => Option (Γ k)) default k (some a))
      = fun a => (proj k').f (update (β := fun k => Option (Γ k)) default k (some a)) := rfl
    rw [this, List.getElem?_map, proj, PointedMap.mk_val]
    by_cases h : k' = k
    · subst k'
      simp only [Function.update_self]
      rw [ListBlank.nth_mk, List.getI_eq_getElem?_getD, ← List.map_reverse, List.getElem?_map]
    · simp only [Function.update_of_ne h]
      rw [ListBlank.nth_mk, List.getI_eq_getElem?_getD, List.map, List.reverse_nil]
      cases L.reverse[i]? <;> rfl

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

Goal state before:
pp: case neg.refl
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he✝ : v' ∈ f.fix.eval v✝
hr✝ : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step (stepRet k v')
v : List ℕ
he : v' ∈ f.fix.eval v
IH :
  ∀ (a'' : List ℕ),
    Sum.inr a'' ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v) →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v₁ : List ℕ
he₁ : v₁ ∈ f.eval v
h : ¬v₁.headI = 0
right✝ :
  v' ∈ PFun.fix (fun v ↦ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) v₁.tail
⊢ x ∈ eval step (stepRet (Cont.fix f k) v₁)

Tactic:
rw [stepRet, if_neg h]

Goal state after:
case neg.refl
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he✝ : v' ∈ f.fix.eval v✝
hr✝ : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step (stepRet k v')
v : List ℕ
he : v' ∈ f.fix.eval v
IH :
  ∀ (a'' : List ℕ),
    Sum.inr a'' ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v) →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v₁ : List ℕ
he₁ : v₁ ∈ f.eval v
h : ¬v₁.headI = 0
right✝ :
  v' ∈ PFun.fix (fun v ↦ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) v₁.tail
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v₁.tail)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ : List Γ'
o : Option Γ'
L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
e : splitAtPred p (S k₁) = (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)
    (TM2.stepAux (tr (Λ'.push k₁ id (Λ'.move (fun x ↦ false) rev k₂ q))) o
      (update (update S k₁ L₂) rev (L₁.reverseAux (S rev))))
    { l := some q, var := none,
      stk :=
        update
          (update S k₁
            ((match (motive := Option Γ' → (List Γ' → List Γ') → (Γ' → List Γ' → List Γ') → List Γ' → List Γ') o, id,
                List.cons with
              | some x, x_1, f => f x
              | none, y, x => y)
              L₂))
          k₂ (L₁ ++ S k₂) }

Tactic:
cases o <;> simp only

Goal state after:
case none
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
e : splitAtPred p (S k₁) = (L₁, none, 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)
    (TM2.stepAux (tr (Λ'.push k₁ id (Λ'.move (fun x ↦ false) rev k₂ q))) none
      (update (update S k₁ L₂) rev (L₁.reverseAux (S rev))))
    { l := some q, var := none, stk := update (update S k₁ (id L₂)) k₂ (L₁ ++ S k₂) }

case some
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
val✝ : Γ'
e : splitAtPred p (S k₁) = (L₁, some val✝, 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)
    (TM2.stepAux (tr (Λ'.push k₁ id (Λ'.move (fun x ↦ false) rev k₂ q))) (some val✝)
      (update (update S k₁ L₂) rev (L₁.reverseAux (S rev))))
    { l := some q, var := none, stk := update (update S k₁ (val✝ :: L₂)) k₂ (L₁ ++ S k₂) }
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case refine_1
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
f_sur : Surjective f
this : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
⊢ U ⊆ φ ⁻¹' Z₂

Tactic:
intro x hx
    have : φ x ∈ Z₁ ∪ Z₂ := (g x).2
    rcases this with hφ | hφ
    · exact ((hφ₁ x ▸ hφ.1) hx).elim
    · exact hφ

Goal state after:
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:
· simpa only [G_empty, image_empty] using empty_subset _

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.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 : ι), IsOpen (Sigma.mk i ⁻¹' closure s)

Tactic:
intro i

Goal state after:
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 : ι
⊢ IsOpen (Sigma.mk i ⁻¹' closure s)
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case refine_1
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
⊢ ∀ (j : J), TopologicalSpace.IsTopologicalBasis {W | IsClopen W}

Tactic:
intro i

Goal state after:
case refine_1
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
i : J
⊢ TopologicalSpace.IsTopologicalBasis {W | IsClopen W}
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case succ
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.succ k ⊆ S
s✝ : Option Γ'
⊢ Λ'.Supports S
    ((if s✝ = some Γ'.consₗ then id else Λ'.clear (fun x ↦ decide (x = Γ'.consₗ)) main) (unrev (Λ'.ret k).succ))

Tactic:
split_ifs <;> exact Finset.union_subset_right Hk

Goal state after:
Module: Mathlib.Condensed.Discrete.LocallyConstant

Goal state before:
pp: P : TopCat → Prop
inst✝¹ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
Q : CompHausLike P
Z : Type (max u w)
r : LocallyConstant (↑Q.toTop) Z
a : Fiber ⇑r
inst✝ : HasExplicitFiniteCoproducts P
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
⊢ ((X.mapIso (sigmaIso r).op).hom ≫ (sigmaComparison X fun a ↦ ↑(fiber r a).toTop) ≫ ↾fun g ↦ g a) =
    X.map (sigmaIncl r a).op

Tactic:
ext
  simp only [Functor.mapIso_hom, Iso.op_hom, sigmaComparison, TypeCat.Fun.toFun_apply,
    CategoryTheory.comp_apply, ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk,
    ← X.map_comp_apply]
  rfl

Goal state after:
Module: Mathlib.Condensed.Discrete.Characterization

Goal state before:
pp: X : CondensedSet
tfae_1_iff_2 : Condensed.IsDiscrete X ↔ IsIso ((discreteUnderlyingAdj (Type (u + 1))).counit.app X)
tfae_1_iff_3 : Condensed.IsDiscrete X ↔ (discrete (Type (u + 1))).essImage X
⊢ [Condensed.IsDiscrete X, IsIso ((discreteUnderlyingAdj (Type (u + 1))).counit.app X),
      (discrete (Type (u + 1))).essImage X, LocallyConstant.functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      Sheaf.IsConstant (coherentTopology Profinite) ((ProfiniteCompHaus.equivalence (Type (u + 1))).inverse.obj X),
      ∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ X.obj).mapCocone S.asLimitCone.op))].TFAE

Tactic:
tfae_have 1 ↔ 4 := Sheaf.isConstant_iff_mem_essImage _ CompHaus.isTerminalPUnit adjunction _

Goal state after:
X : CondensedSet
tfae_1_iff_2 : Condensed.IsDiscrete X ↔ IsIso ((discreteUnderlyingAdj (Type (u + 1))).counit.app X)
tfae_1_iff_3 : Condensed.IsDiscrete X ↔ (discrete (Type (u + 1))).essImage X
tfae_1_iff_4 : Condensed.IsDiscrete X ↔ LocallyConstant.functor.essImage X
⊢ [Condensed.IsDiscrete X, IsIso ((discreteUnderlyingAdj (Type (u + 1))).counit.app X),
      (discrete (Type (u + 1))).essImage X, LocallyConstant.functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      Sheaf.IsConstant (coherentTopology Profinite) ((ProfiniteCompHaus.equivalence (Type (u + 1))).inverse.obj X),
      ∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ X.obj).mapCocone S.asLimitCone.op))].TFAE
Module: Mathlib.Condensed.Discrete.Module

Goal state before:
pp: P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ (discrete (ModuleCat R)).map ((underlying (ModuleCat R)).map ((functor R).map f)) ≫
      (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj Y✝) =
    (functorIsoDiscreteAux₂ R X✝).inv ≫
      (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R)).map ((Functor.const CompHausᵒᵖ).map f) ≫
        (functorIsoDiscreteAux₂ R Y✝).hom ≫ (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj Y✝)

Tactic:
simp only [← assoc]

Goal state after:
P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ (discrete (ModuleCat R)).map ((underlying (ModuleCat R)).map ((functor R).map f)) ≫
      (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj Y✝) =
    (((functorIsoDiscreteAux₂ R X✝).inv ≫
          (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R)).map ((Functor.const CompHausᵒᵖ).map f)) ≫
        (functorIsoDiscreteAux₂ R Y✝).hom) ≫
      (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj Y✝)
Module: Mathlib.Condensed.Discrete.Characterization

Goal state before:
pp: R : Type u
inst✝ : Ring R
M : LightCondMod R
tfae_1_iff_2 : LightCondensed.IsDiscrete M ↔ IsIso ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ (LightCondensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : LightCondensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
h : ∀ (S : LightProfinite), Nonempty (IsColimit (M.obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))
⊢ LightCondensed.IsDiscrete M

Tactic:
rw [isDiscrete_iff_isDiscrete_forget, ((LightCondSet.isDiscrete_tfae _).out 0 5 :)]

Goal state after:
R : Type u
inst✝ : Ring R
M : LightCondMod R
tfae_1_iff_2 : LightCondensed.IsDiscrete M ↔ IsIso ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ (LightCondensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : LightCondensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
h : ∀ (S : LightProfinite), Nonempty (IsColimit (M.obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))
⊢ ∀ (S : LightProfinite),
    Nonempty (IsColimit (((LightCondensed.forget R).obj M).obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))