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

Goal state before:
pp: case inr.inr
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1
this :
  ∀ {Γ : Type u_1} [i : Inhabited Γ] {L₁ L₂ : ListBlank Γ} (l₁ l₂ : List Γ),
    (∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1) → l₁.length ≤ l₂.length → mk l₁ = mk l₂
h : ¬l₁.length ≤ l₂.length
h✝ : l₂.length ≤ l₁.length
⊢ mk l₁ = mk l₂

Tactic:
symm

Goal state after:
case inr.inr
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1
this :
  ∀ {Γ : Type u_1} [i : Inhabited Γ] {L₁ L₂ : ListBlank Γ} (l₁ l₂ : List Γ),
    (∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1) → l₁.length ≤ l₂.length → mk l₁ = mk l₂
h : ¬l₁.length ≤ l₂.length
h✝ : l₂.length ≤ l₁.length
⊢ mk l₂ = mk l₁
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case tail.inl.some
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ b✝ c✝ : σ₂
a✝ : ReflTransGen (fun a b ↦ b ∈ f₂ a) a₂ b✝
cd : c✝ ∈ f₂ b✝
e₁ : σ₁
ae : Reaches f₁ a₁ e₁
ce : Reaches f₂ b✝ b✝
ee : tr e₁ b✝
g₁ : σ₁
eg : f₁ e₁ = some g₁
⊢ ∀ (x : σ₂), tr g₁ x → Reaches₁ f₂ b✝ x → ∃ c₁ c₂, Reaches f₂ c✝ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
intro g₂

Goal state after:
case tail.inl.some
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ b✝ c✝ : σ₂
a✝ : ReflTransGen (fun a b ↦ b ∈ f₂ a) a₂ b✝
cd : c✝ ∈ f₂ b✝
e₁ : σ₁
ae : Reaches f₁ a₁ e₁
ce : Reaches f₂ b✝ b✝
ee : tr e₁ b✝
g₁ : σ₁
eg : f₁ e₁ = some g₁
g₂ : σ₂
⊢ tr g₁ g₂ → Reaches₁ f₂ b✝ g₂ → ∃ c₁ c₂, Reaches f₂ c✝ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
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:
induction i generalizing T with

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

Goal state before:
pp: 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)

Tactic:
symm

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.map { f := Prod.mk false, map_pt' := ⋯ } (ListBlank.modifyNth f n✝ L.tail) =
    ListBlank.modifyNth (fun a ↦ (a.1, f a.2)) n✝ (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail)
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
⊢ TM2.SupportsStmt S (stRun s q) ↔ TM2.SupportsStmt S q

Tactic:
by
  cases s <;> rfl

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

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
⊢ trNormal (stRun s q) = goto fun x x_1 ↦ go k s q

Tactic:
by
  cases s <;> rfl

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

Goal state before:
pp: case zero
n : ℕ
⊢ ↑0 = ↑zero <<< n

Tactic:
symm

Goal state after:
case zero
n : ℕ
⊢ ↑zero <<< n = ↑0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case zero
n : ℕ
⊢ ↑0 = ↑zero >>> n

Tactic:
symm

Goal state after:
case zero
n : ℕ
⊢ ↑zero >>> n = ↑0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.succ.one
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
⊢ ↑0 = ↑(pos one) / 2 ^ (n + 1)

Tactic:
symm

Goal state after:
case pos.succ.one
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
⊢ ↑(pos one) / 2 ^ (n + 1) = ↑0
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case some
Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : TM0.Machine Γ Λ
x✝ : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
s : TM0.Stmt Γ
e : M q T.head = some (q', s)
⊢ FRespects (TM1.step (tr M)) (trCfg M) (trCfg M { q := q, Tape := T }) (TM0.step M { q := q, Tape := T })

Tactic:
simp only [FRespects, TM0.step, trCfg, e, Option.isSome, cond, Option.map_some]

Goal state after:
case some
Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : TM0.Machine Γ Λ
x✝ : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
s : TM0.Stmt Γ
e : M q T.head = some (q', s)
⊢ Reaches₁ (TM1.step (tr M)) { l := some (Λ'.normal q), var := (), Tape := T }
    {
      l :=
        match
          match
            M q'
              (match s with
                | TM0.Stmt.move d => Tape.move d T
                | TM0.Stmt.write a => Tape.write a T).head with
          | some val => true
          | none => false with
        | true => some (Λ'.normal q')
        | false => none,
      var := (),
      Tape :=
        match s with
        | TM0.Stmt.move d => Tape.move d T
        | TM0.Stmt.write a => Tape.write a T }
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: c : Code
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal c k v = Cfg.ret k' v'

Tactic:
by
  induction c generalizing k v with
  | cons _f fs IHf _IHfs => apply IHf
  | comp f _g _IHf IHg => apply IHg
  | case f g IHf IHg =>
    rw [stepNormal]
    simp only
    cases v.headI <;> [apply IHf; apply IHg]
  | fix f IHf => apply IHf
  | _ => exact ⟨_, _, rfl⟩

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

Goal state before:
pp: q : Λ'
s : Option Γ'
S : K' → List Γ'
⊢ rev ≠ main

Tactic:
decide

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

Goal state before:
pp: q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn L none fun x x_1 ↦ some Γ'.cons
⊢ main ≠ rev

Tactic:
decide

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

Goal state before:
pp: q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
⊢ stack ≠ rev

Tactic:
decide

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

Goal state before:
pp: q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
L₂ : List ℕ
⊢ stack ≠ rev

Tactic:
decide

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

Goal state before:
pp: q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
m : PosNum
IH :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum m) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr)
          { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum m.succ ++ Γ'.cons :: trList v) l₁ c d }
          { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
s : Option Γ'
l₁ : List Γ'
a : Γ'
l : List Γ'
e : trPosNum m = a :: l
h : natEnd a = false
⊢ some Γ'.bit1 ≠ some Γ'.bit0

Tactic:
decide

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
A : DiscreteQuotient X
⊢ ofLE ⋯ = id

Tactic:
ext ⟨⟩
  rfl

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
A : DiscreteQuotient X
B : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
h1 : LEComap g B C
h2 : LEComap f A B
⊢ map (g.comp f) ⋯ = map g h1 ∘ map f h2

Tactic:
ext ⟨⟩
  rfl

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

Goal state before:
pp: 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
⊢ main ≠ rev

Tactic:
decide

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

Goal state before:
pp: case case.succ
f g : 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₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal g (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
k : Cont
v : List ℕ
s s' : Option Γ'
n : ℕ
h :
  Reaches₁ (TM2.step tr)
    { l := some ((trNormal f (trCont k)).pred (trNormal g (trCont k))), var := s,
      stk := elim (trList v) [] [] (trContStack k) }
    (Nat.rec { l := some (trNormal f (trCont k)), var := s', stk := elim (trList v.tail) [] [] (trContStack k) }
      (fun n x ↦
        { l := some (trNormal g (trCont k)), var := s', stk := elim (trList (n :: v.tail)) [] [] (trContStack k) })
      (n + 1))
⊢ ∃ b₂,
    TrCfg (Nat.rec (stepNormal f k v.tail) (fun y x ↦ stepNormal g k (y :: v.tail)) (n + 1)) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (trNormal (f.case g) (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂

Tactic:
· obtain ⟨c, h₁, h₂⟩ := IHg k _ s'
      exact ⟨_, h₁, h.trans h₂⟩

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

Goal state before:
pp: fs : Code
as : List ℕ
k : Cont
a_ih✝ :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal fs (trCont (Cont.cons₂ v k))), var := none,
      stk := elim (trList as) [] [] (trContStack (Cont.cons₂ v k)) }
    s'
⊢ main ≠ rev ∧ aux ≠ rev ∧ main ≠ aux

Tactic:
decide

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

Goal state before:
pp: fs : Code
as : List ℕ
k : Cont
a_ih✝ :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal fs (trCont (Cont.cons₂ v k))), var := none,
      stk := elim (trList as) [] [] (trContStack (Cont.cons₂ v k)) }
    s'
⊢ stack ≠ rev ∧ main ≠ rev ∧ stack ≠ main

Tactic:
decide

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

Goal state before:
pp: fs : Code
as : List ℕ
k : Cont
a_ih✝ :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal fs (trCont (Cont.cons₂ v k))), var := none,
      stk := elim (trList as) [] [] (trContStack (Cont.cons₂ v k)) }
    s'
⊢ aux ≠ rev ∧ stack ≠ rev ∧ aux ≠ stack

Tactic:
decide

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

Goal state before:
pp: case right
J : Type v
inst✝¹ : SmallCategory J
inst✝ : CountableCategory J
F : J ⥤ LightProfinite
⊢ SecondCountableTopology
    ↑{u |
        ∀ {i j : J} (f : i ⟶ j),
          (ConcreteCategory.hom (((F ⋙ lightProfiniteToCompHaus) ⋙ compHausToTop).map f)) (u i) = u j}

Tactic:
apply IsInducing.subtypeVal.secondCountableTopology

Goal state after:
Module: Mathlib.Logic.Function.FiberPartition

Goal state before:
pp: Y : Type u_2
Z : Type u_3
W : Type u_4
f : Y → Z
g : Z → W
a : Fiber (g ∘ f)
⊢ g (f (preimage (g ∘ f) a)) = image (g ∘ f) a

Tactic:
rw [← map_preimage_eq_image, comp_apply]

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

Goal state before:
pp: case inl
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
ff : Quotient S.toSetoid → α := ⇑f.lift
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (j : J), Nonempty ↑(F.obj j).toTop
this✝ : ∀ (j : J), Nonempty ↑((F ⋙ toTopCat).obj j)
this : ∀ (j : J), T2Space ↑((F ⋙ toTopCat).obj j)
⊢ False

Tactic:
have : ∀ j : J, CompactSpace ((F ⋙ Profinite.toTopCat).obj j) := fun j =>
      (inferInstance : CompactSpace (F.obj j))

Goal state after:
case inl
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
ff : Quotient S.toSetoid → α := ⇑f.lift
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (j : J), Nonempty ↑(F.obj j).toTop
this✝¹ : ∀ (j : J), Nonempty ↑((F ⋙ toTopCat).obj j)
this✝ : ∀ (j : J), T2Space ↑((F ⋙ toTopCat).obj j)
this : ∀ (j : J), CompactSpace ↑((F ⋙ toTopCat).obj j)
⊢ False
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:
by
  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.Module

Goal state before:
pp: P : TopCat → Prop
R : Type (max u w)
inst✝² : Ring R
inst✝¹ : HasExplicitFiniteCoproducts P
inst✝ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)
X : ModuleCat R
this : Preregular (CompHausLike P)
⊢ Presheaf.IsSheaf (coherentTopology (CompHausLike P)) ((functorToPresheaves R).obj X ⋙ forget (ModuleCat R))

Tactic:
exact ((CompHausLike.LocallyConstant.functor P hs).obj _).property

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

Goal state before:
pp: X : LightCondSet
⊢ [LightCondensed.IsDiscrete X, IsIso ((LightCondensed.discreteUnderlyingAdj (Type u)).counit.app X),
      (LightCondensed.discrete (Type u)).essImage X, functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      ∀ (S : LightProfinite), Nonempty (IsColimit (X.obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))].TFAE

Tactic:
by
  tfae_have 1 ↔ 2 := Sheaf.isConstant_iff_isIso_counit_app _ _ _
  tfae_have 1 ↔ 3 := ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩
  tfae_have 1 ↔ 4 := Sheaf.isConstant_iff_mem_essImage _ LightProfinite.isTerminalPUnit adjunction X
  tfae_have 1 ↔ 5 :=
    have : functor.Faithful := inferInstance
    have : functor.Full := inferInstance
    -- These `have` statements above shouldn't be needed, but they are.
    Sheaf.isConstant_iff_isIso_counit_app' _ LightProfinite.isTerminalPUnit adjunction X
  tfae_have 6 → 4 := fun h ↦
    mem_locallyConstant_essImage_of_isColimit_mapCocone X (fun S ↦ (h S).some)
  tfae_have 4 → 6 := fun ⟨Y, ⟨i⟩⟩ S ↦
    ⟨IsColimit.mapCoconeEquiv ((sheafToPresheaf _ _).mapIso i)
      (LightCondensed.isColimitLocallyConstantPresheafDiagram Y S)⟩
  tfae_finish

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)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝³ : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g : T ⟶ S
X✝ : TopCat
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Sheaf (coherentTopology (CompHausLike P)) (Type (max u w))
x : X.obj.obj (op (of P PUnit.{u + 1}))
this✝ : Preregular (CompHausLike P)
this : PreservesFiniteProducts ((sheafToPresheaf (coherentTopology (CompHausLike P)) (Type (max u w))).obj X) :=
  @CompHausLike.LocallyConstant.adjunction._proof_2 P inst✝² inst✝¹ hs X this✝
a : Fiber ⇑((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x)
⊢ counitAppAppImage ((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x) a =
    (ConcreteCategory.hom
        (X.obj.map (sigmaIncl ((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x) a).op))
      x

Tactic:
simp only [counitAppAppImage]

Goal state after:
P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝³ : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g : T ⟶ S
X✝ : TopCat
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Sheaf (coherentTopology (CompHausLike P)) (Type (max u w))
x : X.obj.obj (op (of P PUnit.{u + 1}))
this✝ : Preregular (CompHausLike P)
this : PreservesFiniteProducts ((sheafToPresheaf (coherentTopology (CompHausLike P)) (Type (max u w))).obj X) :=
  @CompHausLike.LocallyConstant.adjunction._proof_2 P inst✝² inst✝¹ hs X this✝
a : Fiber ⇑((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x)
⊢ (ConcreteCategory.hom
        (X.obj.map
          (isTerminalPUnit.from
              (fiber ((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x) a)).op))
      (Fiber.image (⇑((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x)) a) =
    (ConcreteCategory.hom
        (X.obj.map (sigmaIncl ((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x) a).op))
      x
Module: Mathlib.Condensed.Explicit

Goal state before:
pp: A : Type u_1
inst✝² : Category.{v_1, u_1} A
inst✝¹ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.op) A
F : Stoneanᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts F
⊢ IsSheaf (coherentTopology Stonean) F

Tactic:
rw [isSheaf_iff_preservesFiniteProducts_of_projective F]
      exact ⟨fun _ ↦ inferInstance⟩

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

Goal state before:
pp: case e_a
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
f :
  LocallyConstant (↑(toProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X) PUnit.{u + 1})))
x : Function.Fiber ⇑f
⊢ (ConcreteCategory.hom (X.map (sigmaIncl f x).op))
      ((ConcreteCategory.hom (isoFinYonedaComponents X (Profinite.of (Opposite.unop Y).obj)).inv) ⇑f) =
    counitAppAppImage f x

Tactic:
simp only [counitAppAppImage]

Goal state after:
case e_a
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
f :
  LocallyConstant (↑(toProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X) PUnit.{u + 1})))
x : Function.Fiber ⇑f
⊢ (ConcreteCategory.hom (X.map (sigmaIncl f x).op))
      ((ConcreteCategory.hom (isoFinYonedaComponents X (Profinite.of (Opposite.unop Y).obj)).inv) ⇑f) =
    (ConcreteCategory.hom (X.map (CompHausLike.isTerminalPUnit.from (fiber f x)).op)) (Function.Fiber.image (⇑f) x)
Module: Mathlib.Condensed.Light.Epi

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ Epi (c.π.app (Opposite.op 0))

Tactic:
by
  apply Functor.epi_of_epi_map (forget R)
  change Epi (((forget R).mapCone c).π.app ⟨0⟩)
  apply coherentTopology.epi_π_app_zero_of_epi
  · simp only [LightProfinite.effectiveEpi_iff_surjective]
    exact fun x h ↦ Concrete.surjective_π_app_zero_of_surjective_map (limit.isLimit x) h
  · have := (freeForgetAdjunction R).isRightAdjoint
    exact isLimitOfPreserves _ hc
  · exact fun _ ↦ (forget R).map_epi _

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

Goal state before:
pp: case e_a
X : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts X
hX : (S : LightProfinite) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toLightProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
f :
  LocallyConstant (↑(toLightProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj
      (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X) PUnit.{u + 1})))
x : Function.Fiber ⇑f
⊢ (ConcreteCategory.hom (X.map (sigmaIncl f x).op))
      ((ConcreteCategory.hom (isoFinYonedaComponents X (LightProfinite.of (Opposite.unop Y).obj)).inv) ⇑f) =
    counitAppAppImage f x

Tactic:
simp only [counitAppAppImage]

Goal state after:
case e_a
X : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts X
hX : (S : LightProfinite) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toLightProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
f :
  LocallyConstant (↑(toLightProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj
      (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X) PUnit.{u + 1})))
x : Function.Fiber ⇑f
⊢ (ConcreteCategory.hom (X.map (sigmaIncl f x).op))
      ((ConcreteCategory.hom (isoFinYonedaComponents X (LightProfinite.of (Opposite.unop Y).obj)).inv) ⇑f) =
    (ConcreteCategory.hom (X.map (CompHausLike.isTerminalPUnit.from (fiber f x)).op)) (Function.Fiber.image (⇑f) x)
Module: Mathlib.Control.Fold

Goal state before:
pp: α : Type u
xs : List α
⊢ toList xs = xs

Tactic:
simp only [toList_spec, foldMap, traverse]
  induction xs with
  | nil => rfl
  | cons _ _ ih => (conv_rhs => rw [← ih]); rfl

Goal state after: