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

Goal state before:
pp: case neg.inl
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 : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
i : ℕ
h✝ : ¬i = (S k).length
h : i < (S k).length
⊢ (List.map some (S k)).reverse.getI i = ((List.map some (S k)).reverse ++ [some (f v)]).getI i

Tactic:
List.getI_append

Goal state after:
case neg.inl
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 : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
i : ℕ
h✝ : ¬i = (S k).length
h : i < (S k).length
⊢ (List.map some (S k)).reverse.getI i = (List.map some (S k)).reverse.getI i

case neg.inl.h
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 : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
i : ℕ
h✝ : ¬i = (S k).length
h : i < (S k).length
⊢ i < (List.map some (S k)).reverse.length
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case neg.inl
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) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h✝ : ¬i = tl.length
h : i < tl.length
⊢ ((List.map some tl).reverse ++ [some hd]).getI i = (List.map some tl).reverse.getI i

Tactic:
List.getI_append

Goal state after:
case neg.inl
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) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h✝ : ¬i = tl.length
h : i < tl.length
⊢ (List.map some tl).reverse.getI i = (List.map some tl).reverse.getI i

case neg.inl.h
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) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h✝ : ¬i = tl.length
h : i < tl.length
⊢ i < (List.map some tl).reverse.length
Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi

Goal state before:
pp: P : TopCat → Prop
B X : CompHausLike P
π : X ⟶ B
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
W✝ : CompHausLike P
e : X ⟶ W✝
h : ∀ {Z : CompHausLike P} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W✝
hm : π ≫ g = e
this : g = ofHom P (⋯.liftEquiv ⟨TopCat.Hom.hom e.hom, ⋯⟩)
⊢ g = ofHom P (⋯.lift (TopCat.Hom.hom e.hom) ⋯)

Tactic:
assumption

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

Goal state before:
pp: α : Type
inst✝ : Finite α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
tfae_3_to_2 : (∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b) → Epi (Sigma.desc π)
x✝ : Epi (Sigma.desc π)
e : Function.Surjective ⇑(ConcreteCategory.hom (Sigma.desc π))
i : ∐ X ≅ finiteCoproduct X :=
  (colimit.isColimit (Discrete.functor X)).coconePointUniqueUpToIso (finiteCoproduct.isColimit X)
t : ↑(∐ X).toTop
q : (fun X ↦ ↑X.toTop) (finiteCoproduct X) := (ConcreteCategory.hom i.hom) t
⊢ t = (ConcreteCategory.hom (i.hom ≫ i.inv)) t

Tactic:
simp only [i.hom_inv_id]; rfl

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

Goal state before:
pp: case some.nil
α : Type u_1
p : α → Bool
a : α
L : List α
IH :
  ∀ (l₁ : List α) (o : Option α) (l₂ : List α),
    (∀ x ∈ l₁, p x = false) →
      Option.elim' (L = l₁ ∧ l₂ = []) (fun a ↦ p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)
h₁ : ∀ x ∈ [], p x = false
h₂ : p a = true
⊢ (bif p a then ([], some a, L)
    else
      match splitAtPred p L with
      | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
    ([], some a, L)

Tactic:
rw [h₂, cond]

Goal state after:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ✝ : CompactSpace Z
_csZ : T2Space Z
f : StoneCech X → Z
g : Y → Z
hf : Continuous f
hg : Continuous g
g_sur : Surjective g
s : Z → Y := fun z ↦ Classical.choose ⋯
⊢ ∃ h, Continuous h ∧ g ∘ h = f

Tactic:
have hs : g ∘ s = id := funext fun z => Classical.choose_spec (g_sur z)

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ✝ : CompactSpace Z
_csZ : T2Space Z
f : StoneCech X → Z
g : Y → Z
hf : Continuous f
hg : Continuous g
g_sur : Surjective g
s : Z → Y := fun z ↦ Classical.choose ⋯
hs : g ∘ s = id
⊢ ∃ h, Continuous h ∧ g ∘ h = f
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case refine_1.inr
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
x : X
hx : x ∈ U
hφ : φ x ∈ Z₂
⊢ x ∈ φ ⁻¹' Z₂

Tactic:
· exact hφ

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

Goal state before:
pp: case nil.cons.true
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
a : Γ'
Sk : List Γ'
e₁ : some a = o
e₂ : Sk = L₂
⊢ ReflTransGen
    (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)
    { l := some q, var := some a, stk := update S k Sk } { l := some q, var := o, stk := update S k L₂ }

Tactic:
rw [e₁, e₂]

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

Goal state before:
pp: X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
g : A → B
hf : Continuous[_, inst✝⁴] f
hg : Continuous[inst✝⁵, inst✝⁴] g
hsurj : Function.Surjective g
A' : CompHaus := of A
B' : CompHaus := of B
f' : X ⟶ B' := CompHausLike.ofHom (fun x ↦ True) { toFun := f, continuous_toFun := hf }
g' : A' ⟶ B' := CompHausLike.ofHom (fun x ↦ True) { toFun := g, continuous_toFun := hg }
⊢ Function.Surjective ⇑(ConcreteCategory.hom g')

Tactic:
assumption

Goal state after:
Module: Mathlib.Topology.ExtremallyDisconnected

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

Tactic:
assumption

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

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

Tactic:
tfae_have 3 → 1 := fun hπ ↦ ⟨⟨CompHausLike.effectiveEpiStruct π hπ⟩⟩

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

Goal state before:
pp: C : Type w
inst✝ : Category.{v, w} C
X Y : Condensed C
f g : X ⟶ Y
h : ∀ (S : CompHausᵒᵖ), f.hom.app S = g.hom.app S
x✝ : CompHausᵒᵖ
⊢ f.hom.app x✝ = g.hom.app x✝

Tactic:
exact h _

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

Goal state before:
pp: case h_option.refine_5.none.some
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
Z0_subset_U : Z none ⊆ U
V : Set X
V_clopen : IsClopen V
Z0_subset_V : Z none ⊆ V
V_subset_U : V ⊆ U
V_subset_D0 : V ⊆ D none
D' : I → Set X := fun i ↦ D (some i) \ V
D'_clopen : ∀ (i : I), IsClopen (D' i)
Z'_subset_D' : ∀ (i : I), Z' i ⊆ D' i
C' : I → Set X
C'_clopen : ∀ (i : I), IsClopen (C' i)
Z'_subset_C' : ∀ (i : I), Z (some i) ⊆ C' i
C'_subset_D' : ∀ (i : I), C' i ⊆ D' i
C'_cover_D' : ⋃ i, D' i ⊆ ⋃ i, C' i
C'_disj : univ.PairwiseDisjoint C'
C0 : Set X := D none \ ⋃ i, C' i
this✝ : IsClopen C0
this : Z none ⊆ C0
C : Option I → Set X := fun i ↦ Option.casesOn i C0 C'
a✝¹ : none ∈ univ
j : I
a✝ : some j ∈ univ
⊢ (C none ∩ C (some j)).Nonempty → none = some j

Tactic:
simpa [C, C0, Set.not_nonempty_iff_eq_empty, ← Set.disjoint_iff_inter_eq_empty] using
          Disjoint.mono_right (subset_iUnion C' j) disjoint_sdiff_left

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
x : X
⊢ IsOpen {S.proj x}

Tactic:
rw [← S.proj_isQuotientMap.isOpen_preimage, fiber_eq]
    exact S.isOpen_setOfPred_rel _

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered

Goal state before:
pp: case e'_3.mp.refine_2
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
U : (i : J) → Set ↑(F.obj i) := fun i ↦ if h : i = j then ⋯.mpr V else Set.univ
⊢ ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V = ⋂ i ∈ {j}, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i

Tactic:
simp [U]

Goal state after:
Module: Mathlib.Topology.ClopenBox

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace Y
inst✝ : CompactSpace X
W : Clopens (X × Y)
U : X × Y → Clopens X
hxU : ∀ x ∈ W, x.1 ∈ U x
V : X × Y → Clopens Y
hxV : ∀ x ∈ W, x.2 ∈ V x
hUV : ∀ x ∈ W, U x ×ˢ V x ≤ W
I : Finset (X × Y)
hIW : ∀ x ∈ I, x ∈ W.carrier
hWI : W.carrier ⊆ ⋃ x ∈ I, ↑(U x) ×ˢ ↑(V x)
⊢ ∃ I, W = I.sup fun i ↦ i.1 ×ˢ i.2

Tactic:
use I.image fun x ↦ (U x, V x)

Goal state after:
case h
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace Y
inst✝ : CompactSpace X
W : Clopens (X × Y)
U : X × Y → Clopens X
hxU : ∀ x ∈ W, x.1 ∈ U x
V : X × Y → Clopens Y
hxV : ∀ x ∈ W, x.2 ∈ V x
hUV : ∀ x ∈ W, U x ×ˢ V x ≤ W
I : Finset (X × Y)
hIW : ∀ x ∈ I, x ∈ W.carrier
hWI : W.carrier ⊆ ⋃ x ∈ I, ↑(U x) ×ˢ ↑(V x)
⊢ W = (Finset.image (fun x ↦ (U x, V x)) I).sup fun i ↦ i.1 ×ˢ i.2
Module: Mathlib.Condensed.Light.Basic

Goal state before:
pp: C : Type w
inst✝ : Category.{v, w} C
X Y : LightCondensed C
f g : X ⟶ Y
h : ∀ (S : LightProfiniteᵒᵖ), f.hom.app S = g.hom.app S
x✝ : LightProfiniteᵒᵖ
⊢ f.hom.app x✝ = g.hom.app x✝

Tactic:
exact h _

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

Goal state before:
pp: case refine_2
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
x : TM2.Cfg (fun x ↦ Γ') Λ' (Option Γ')
⊢ (∃ a ∈ c.eval v, halt a = x) → x ∈ eval (TM2.step tr) i

Tactic:
rintro ⟨v', hv, rfl⟩
    have := StateTransition.tr_eval (b₁ := Cfg.halt v') tr_respects h₁
    simp only [stepNormal_eval, Part.map_eq_map, Part.mem_map_iff, Cfg.halt.injEq,
      exists_eq_right] at this
    obtain ⟨_, ⟨⟩, h⟩ := this hv
    exact h

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

Goal state before:
pp: case hc
J : Type v
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b ↦ if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) gg
ι : α → α → Fin 2 := fun a b ↦ if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f ↦ if h : ∃ a, ι a = f then h.choose else default
x : ↑C.pt.toTop
h1 : ι (f x) = gg ((ConcreteCategory.hom (C.π.app j)) x)
h2 : ∃ a, ι a = gg ((ConcreteCategory.hom (C.π.app j)) x)
⊢ ∃ a, ι a = gg ((TopCat.Hom.hom (C.π.app j).hom) x)

Tactic:
assumption

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

Goal state before:
pp: S : Finset Λ'
q : Λ'
H₁ : Λ'.Supports S q
HS₁ : trStmts₁ q ⊆ S
⊢ Supports (trStmts₁ q) S

Tactic:
have W := fun {q} => trStmts₁_self q
  induction q with
  | move _ _ _ q q_ih => _ | clear _ _ q q_ih => _ | copy q q_ih => _ | push _ _ q q_ih => _
  | read q q_ih => _ | succ q q_ih => _ | pred q₁ q₂ q₁_ih q₂_ih => _ | ret => _ <;>
    simp [trStmts₁, -Finset.singleton_subset_iff] at HS₁ ⊢
  any_goals
    obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁
    first | have h₃ := h₂ W | try simp [Finset.subset_iff] at h₂
  · exact supports_insert.2 ⟨⟨fun _ => h₃, fun _ => h₁⟩, q_ih H₁ h₂⟩ -- move
  · exact supports_insert.2 ⟨⟨fun _ => h₃, fun _ => h₁⟩, q_ih H₁ h₂⟩ -- clear
  · exact supports_insert.2 ⟨⟨fun _ => h₁, fun _ => h₃⟩, q_ih H₁ h₂⟩ -- copy
  · exact supports_insert.2 ⟨⟨fun _ => h₃, fun _ => h₃⟩, q_ih H₁ h₂⟩ -- push
  · refine supports_insert.2 ⟨fun _ => h₂ _ W, ?_⟩ -- read
    exact supports_biUnion.2 fun _ => q_ih _ (H₁ _) fun _ h => h₂ _ h
  · refine supports_insert.2 ⟨⟨fun _ => h₁, fun _ => h₂.1, fun _ => h₂.1⟩, ?_⟩ -- succ
    exact supports_insert.2 ⟨⟨fun _ => h₂.2 _ W, fun _ => h₂.1⟩, q_ih H₁ h₂.2⟩
  · refine -- pred
      supports_insert.2 ⟨⟨fun _ => h₁, fun _ => h₂.2 _ (Or.inl W),
                          fun _ => h₂.1, fun _ => h₂.1⟩, ?_⟩
    refine supports_insert.2 ⟨⟨fun _ => h₂.2 _ (Or.inr W), fun _ => h₂.1⟩, ?_⟩
    refine supports_union.2 ⟨?_, ?_⟩
    · exact q₁_ih H₁.1 fun _ h => h₂.2 _ (Or.inl h)
    · exact q₂_ih H₁.2 fun _ h => h₂.2 _ (Or.inr h)
  · exact supports_singleton.2 (ret_supports H₁)

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
⊢ Presheaf.IsSheaf (coherentTopology (CompHausLike P)) ((functorToPresheaves R).obj X)

Tactic:
have := CompHausLike.preregular hs
    apply Presheaf.isSheaf_coherent_of_hasPullbacks_of_comp
      (s := CategoryTheory.forget (ModuleCat R))
    exact ((CompHausLike.LocallyConstant.functor P hs).obj _).property

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

Goal state before:
pp: P : TopCat → Prop
R : Type u
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ (functor R).map f ≫ (functorIsoDiscreteComponents R Y✝).symm.hom =
    (functorIsoDiscreteComponents R X✝).symm.hom ≫ (discrete (ModuleCat R)).map f

Tactic:
by
    dsimp
    rw [Iso.eq_inv_comp, ← Category.assoc, Iso.comp_inv_eq]
    dsimp [functorIsoDiscreteComponents]
    rw [Category.assoc, ← Iso.eq_inv_comp,
      ← (discreteUnderlyingAdj (ModuleCat R)).counit_naturality]
    simp only [← assoc]
    congr 1
    rw [← Iso.comp_inv_eq]
    apply Sheaf.hom_ext
    simp [functorIsoDiscreteAux₂, ← Functor.map_comp]
    rfl

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

Goal state before:
pp: I : Type u
inst✝² : Category.{u, u} I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
⊢ IsColimit ((locallyConstantPresheaf X).mapCocone c.op)

Tactic:
by
  refine Types.FilteredColimit.isColimitOf _ _ ?_ ?_
  · intro (f : LocallyConstant c.pt X)
    obtain ⟨j, h⟩ := Profinite.exists_locallyConstant.{_, u} c hc f
    exact ⟨⟨j⟩, h⟩
  · intro ⟨i⟩ ⟨j⟩ (fi : LocallyConstant _ _) (fj : LocallyConstant _ _)
      (h : fi.comap (c.π.app i).hom.hom = fj.comap (c.π.app j).hom.hom)
    obtain ⟨k, ki, kj, _⟩ := IsCofilteredOrEmpty.cone_objs i j
    refine ⟨⟨k⟩, ki.op, kj.op, ?_⟩
    dsimp
    ext x
    obtain ⟨x, hx⟩ := ((Profinite.epi_iff_surjective (c.π.app k)).mp inferInstance) x
    rw [← hx]
    change fi ((c.π.app k ≫ (F ⋙ toProfinite).map _) x) =
      fj ((c.π.app k ≫ (F ⋙ toProfinite).map _) x)
    have h := LocallyConstant.congr_fun h x
    dsimp [- CompHausLike.coe_comp] -- `coe_comp` prevents rewriting with `c.w`
    rwa [dsimp% c.w, dsimp% c.w]

Goal state after:
Module: Mathlib.Condensed.Light.TopCatAdjunction

Goal state before:
pp: X✝ Y : LightCondSet
f : X✝ ⟶ Y
X : TopCat
⊢ Epi (topCatAdjunction.counit.app X)

Tactic:
by
  rw [TopCat.epi_iff_surjective]
  exact (topCatAdjunctionCounit_bijective _).2

Goal state after:
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
P A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : ↑((P ⟹ B).obj.obj (Opposite.op S))
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : P ⊗ (free R).obj S'.toCondensed ⟶ A
hh : P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ (ihomPoints R P B S) g = g' ≫ e
this :
  (ihomPoints R P B S').symm (P ◁ (free R).map (lightProfiniteToLightCondSet.map π) ≫ (ihomPoints R P B S) g) =
    (ConcreteCategory.hom ((P ⟹ B).obj.map π.op)) ((ihomPoints R P B S).symm ((ihomPoints R P B S) g))
⊢ (ihomPoints R P B S').symm ((ihomPoints R P A S') ((ihomPoints R P A S').symm g') ≫ e) =
    (ConcreteCategory.hom ((P ⟹ B).obj.map (Opposite.op π))) g

Tactic:
dsimp at hh

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
P A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : ↑((P ⟹ B).obj.obj (Opposite.op S))
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : P ⊗ (free R).obj S'.toCondensed ⟶ A
hh : P ◁ (free R).map (lightProfiniteToLightCondSet.map π) ≫ (ihomPoints R P B S) g = g' ≫ e
this :
  (ihomPoints R P B S').symm (P ◁ (free R).map (lightProfiniteToLightCondSet.map π) ≫ (ihomPoints R P B S) g) =
    (ConcreteCategory.hom ((P ⟹ B).obj.map π.op)) ((ihomPoints R P B S).symm ((ihomPoints R P B S) g))
⊢ (ihomPoints R P B S').symm ((ihomPoints R P A S') ((ihomPoints R P A S').symm g') ≫ e) =
    (ConcreteCategory.hom ((P ⟹ B).obj.map (Opposite.op π))) g
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X✝ : CondensedSet
X : TopCat
⊢ Epi (topCatAdjunction.counit.app X)

Tactic:
by
  rw [TopCat.epi_iff_surjective]
  exact (topCatAdjunctionCounit_bijective _).2

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ (List.foldr cons [] (FreeMonoid.toList (foldMap FreeMonoid.of xs)).reverse).reverse =
    ((ConcreteCategory.hom (unop ((Foldl.ofFreeMonoid (flip cons)) (foldMap FreeMonoid.of xs)))) []).reverse

Tactic:
simp [Function.flip_def, List.foldr_reverse, Foldl.ofFreeMonoid, unop_op]

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α β : Type u} (dummy : ExceptT ε m α), (callCC fun x ↦ dummy) = dummy

Tactic:
intros; simp only [callCC, ExceptT.callCC, @callCC_dummy m _]; ext; rfl

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
β : Fin2.elim0 ⟹ Fin2.elim0 → Sort u_1
f : β nilFun
⊢ (f : Fin2.elim0 ⟹ Fin2.elim0) → β f

Tactic:
by
  intro g
  suffices g = nilFun by rwa [this]
  ext ⟨⟩

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos.mpr.inr.inl.h₀
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
h₁ : y ∈ approx (⇑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (⇑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (⇑f) i a → ∀ (j : ℕ), y ∈ approx (⇑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : i ≤ j
⊢ ∃ i, (approx (⇑?pos.mpr.inr.inl.f✝) i a).Dom

Tactic:
assumption

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos.mpr.inr.inl.hh
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
h₁ : y ∈ approx (⇑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (⇑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (⇑f) i a → ∀ (j : ℕ), y ∈ approx (⇑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : i ≤ j
⊢ b ∈ approx ⇑f ?pos.mpr.inr.inl.i✝ a

Tactic:
assumption

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos.mpr.inr.inl.h₁
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
h₁ : y ∈ approx (⇑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (⇑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (⇑f) i a → ∀ (j : ℕ), y ∈ approx (⇑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : i ≤ j
⊢ y ∈ approx ⇑f ?pos.mpr.inr.inl.j✝ a

Tactic:
assumption

Goal state after: