mathlib-initiative/mathlib-tactics huggingface dataset:
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
f_sur : Surjective f
this : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
⊢ IsOpen (closure U)

Tactic:
let φ := Subtype.val ∘ g

Goal state after:
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
⊢ IsOpen (closure U)
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
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 φ
⊢ IsOpen (closure U)

Tactic:
have hφ₁ : ∀ x, (φ x).1 = x := congr_fun g_sec

Goal state after:
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
⊢ IsOpen (closure U)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons₁
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'
⊢ ∃ b₂,
    TrCfg (stepRet (Cont.cons₁ fs as k) v) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (Λ'.ret (trCont (Cont.cons₁ fs as k))), var := s,
          stk := elim (trList v) [] [] (trContStack (Cont.cons₁ fs as k)) }
        b₂

Tactic:
refine ⟨s', h₁, TransGen.head rfl ?_⟩

Goal state after:
case cons₁
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'
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (TM2.stepAux (tr (Λ'.ret (trCont (Cont.cons₁ fs as k)))) s
      (elim (trList v) [] [] (trContStack (Cont.cons₁ fs as k))))
    s'
Module: Mathlib.Topology.Category.LightProfinite.Limits

Goal state before:
pp: X Y Z : LightProfinite
f : X ⟶ Z
g : Y ⟶ Z
h : Function.Surjective ⇑(ConcreteCategory.hom g)
x : ↑X.toTop
⊢ ∃ a, (ConcreteCategory.hom (CompHausLike.pullback.fst f g)) a = x

Tactic:
obtain ⟨y, hy⟩ := h (f x)

Goal state after:
X Y Z : LightProfinite
f : X ⟶ Z
g : Y ⟶ Z
h : Function.Surjective ⇑(ConcreteCategory.hom g)
x : ↑X.toTop
y : ↑Y.toTop
hy : (ConcreteCategory.hom g) y = (ConcreteCategory.hom f) x
⊢ ∃ a, (ConcreteCategory.hom (CompHausLike.pullback.fst f g)) a = x
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: case mp
X Y : LightProfinite
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
⊢ False

Tactic:
classical
      let Z := of (ULift.{u} <| Fin 2)
      let g : Y ⟶ Z := CompHausLike.ofHom _
        ⟨(LocallyConstant.ofIsClopen hV).map ULift.up, LocallyConstant.continuous _⟩
      let h : Y ⟶ Z := CompHausLike.ofHom _ ⟨fun _ => ⟨1⟩, continuous_const⟩
      have H : h = g := by
        rw [← cancel_epi f]
        ext x
        dsimp [g, LocallyConstant.ofIsClopen]
        rw [ContinuousMap.coe_mk, ContinuousMap.coe_mk, hom_ofHom, ContinuousMap.coe_mk,
          Function.comp_apply, if_neg]
        refine mt (fun α => hVU α) ?_
        simp [U, C]
      apply_fun fun e => (e y).down at H
      dsimp [g, LocallyConstant.ofIsClopen] at H
      rw [ContinuousMap.coe_mk, ContinuousMap.coe_mk, Function.comp_apply, if_pos hyV] at H
      exact top_ne_bot H

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

Goal state before:
pp: P : TopCat → Prop
inst✝⁶ : HasExplicitFiniteCoproducts P
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝⁵ : PreservesFiniteProducts X
α : Type u
inst✝⁴ : Finite α
σ : α → Type u
inst✝³ : (a : α) → TopologicalSpace (σ a)
inst✝² : ∀ (a : α), CompactSpace (σ a)
inst✝¹ : ∀ (a : α), T2Space (σ a)
inst✝ : ∀ (a : α), HasProp P (σ a)
x : X.obj (Opposite.op (of P ((a : α) × σ a)))
a : α
this :
  ∀ (x : ToType (X.obj (∏ᶜ fun a ↦ Opposite.op (of P (σ a))))),
    (ConcreteCategory.hom (Pi.π (fun b ↦ X.obj (Opposite.op (of P (σ b)))) a))
        ((ConcreteCategory.hom (piComparison X fun a ↦ Opposite.op (of P (σ a)))) x) =
      (ConcreteCategory.hom (X.map (Pi.π (fun a ↦ Opposite.op (of P (σ a))) a))) x
⊢ ofHom P { toFun := Sigma.mk a, continuous_toFun := ⋯ } =
    Sigma.ι (fun a ↦ of P (σ a)) a ≫
      ((finiteCoproduct.isColimit fun a ↦ of P (σ a)).coconePointUniqueUpToIso
              (coproductIsCoproduct fun a ↦ of P (σ a))).op.inv.unop

Tactic:
erw [IsColimit.fac]

Goal state after:
P : TopCat → Prop
inst✝⁶ : HasExplicitFiniteCoproducts P
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝⁵ : PreservesFiniteProducts X
α : Type u
inst✝⁴ : Finite α
σ : α → Type u
inst✝³ : (a : α) → TopologicalSpace (σ a)
inst✝² : ∀ (a : α), CompactSpace (σ a)
inst✝¹ : ∀ (a : α), T2Space (σ a)
inst✝ : ∀ (a : α), HasProp P (σ a)
x : X.obj (Opposite.op (of P ((a : α) × σ a)))
a : α
this :
  ∀ (x : ToType (X.obj (∏ᶜ fun a ↦ Opposite.op (of P (σ a))))),
    (ConcreteCategory.hom (Pi.π (fun b ↦ X.obj (Opposite.op (of P (σ b)))) a))
        ((ConcreteCategory.hom (piComparison X fun a ↦ Opposite.op (of P (σ a)))) x) =
      (ConcreteCategory.hom (X.map (Pi.π (fun a ↦ Opposite.op (of P (σ a))) a))) x
⊢ ofHom P { toFun := Sigma.mk a, continuous_toFun := ⋯ } = (finiteCoproduct.cofan fun a ↦ of P (σ a)).ι.app { as := a }
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) (Fin 2)
U : Set ↑C.pt.toTop := ⋯
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toTop
hV : IsClopen V
h : U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V
⊢ ⇑f ⁻¹' {0} = ⇑(LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) (LocallyConstant.ofIsClopen hV)) ⁻¹' {0}

Tactic:
simp only [Fin.isValue, LocallyConstant.coe_comap, Set.preimage_comp,
    LocallyConstant.ofIsClopen_fiber_zero]

Goal state after:
case h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) (Fin 2)
U : Set ↑C.pt.toTop := ⇑f ⁻¹' {0}
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toTop
hV : IsClopen V
h : U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V
⊢ ⇑f ⁻¹' {0} = ⇑(TopCat.Hom.hom (C.π.app j).hom) ⁻¹' V
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: 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
⊢ f x = if h : ∃ a, ι a = gg ((TopCat.Hom.hom (C.π.app j).hom) x) then h.choose else default

Tactic:
have h1 : ι (f x) = gg (C.π.app j x) := by
    change f.map (fun a b => if a = b then (0 : Fin 2) else 1) x = _
    rw [h]
    rfl

Goal state after:
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)
⊢ f x = if h : ∃ a, ι a = gg ((TopCat.Hom.hom (C.π.app j).hom) x) then h.choose else default
Module: Mathlib.Computability.TuringMachine.ToPartrec

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

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁
    first | have h₃ := h₂ W | try simp [Finset.subset_iff] at h₂

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

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

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁
    first | have h₃ := h₂ W | try simp [Finset.subset_iff] at h₂

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

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

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁
    first | have h₃ := h₂ W | try simp [Finset.subset_iff] at h₂

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

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

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁
    first | have h₃ := h₂ W | try simp [Finset.subset_iff] at h₂

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

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

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁
    first | have h₃ := h₂ W | try simp [Finset.subset_iff] at h₂

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

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

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁
    first | have h₃ := h₂ W | try simp [Finset.subset_iff] at h₂

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

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

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁
    first | have h₃ := h₂ W | try simp [Finset.subset_iff] at h₂

Goal state after:
case pred
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q₁ q₂ : Λ'
q₁_ih : Λ'.Supports S q₁ → trStmts₁ q₁ ⊆ S → Supports (trStmts₁ q₁) S
q₂_ih : Λ'.Supports S q₂ → trStmts₁ q₂ ⊆ S → Supports (trStmts₁ q₂) S
H₁ : Λ'.Supports S (q₁.pred q₂)
HS₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S
h₁ : q₁.pred q₂ ∈ S
h₂ : unrev q₂ ∈ S ∧ ∀ (a : Λ'), a ∈ trStmts₁ q₁ ∨ a ∈ trStmts₁ q₂ → a ∈ S
⊢ Supports (insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂))) S
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case ret
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
k✝ : Cont'
H₁ : Λ'.Supports S (Λ'.ret k✝)
HS₁ : {Λ'.ret k✝} ⊆ S
⊢ Supports {Λ'.ret k✝} S

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁
    first | have h₃ := h₂ W | try simp [Finset.subset_iff] at h₂

Goal state after:
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)
tfae_6_to_1 :
  (∀ (S : LightProfinite), Nonempty (IsColimit (M.obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))) →
    LightCondensed.IsDiscrete M
h :
  ∀ (S : LightProfinite),
    Nonempty (IsColimit (((LightCondensed.forget R).obj M).obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))
S : LightProfinite
⊢ Nonempty (IsColimit (M.obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))

Tactic:
let : ReflectsFilteredColimitsOfSize.{0, 0} (forget (ModuleCat R)) :=
      reflectsFilteredColimitsOfSize_shrink.{0, u, 0, u} _

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)
tfae_6_to_1 :
  (∀ (S : LightProfinite), Nonempty (IsColimit (M.obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))) →
    LightCondensed.IsDiscrete M
h :
  ∀ (S : LightProfinite),
    Nonempty (IsColimit (((LightCondensed.forget R).obj M).obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))
S : LightProfinite
this : ReflectsFilteredColimitsOfSize.{0, 0, u, u, u + 1, u + 1} (forget (ModuleCat R)) :=
  reflectsFilteredColimitsOfSize_shrink (forget (ModuleCat R))
⊢ Nonempty (IsColimit (M.obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))
Module: Mathlib.Control.Fold

Goal state before:
pp: case cons
α : Type u
head✝ : α
tail✝ : List α
ih : FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
⊢ FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) (head✝ :: tail✝)) = head✝ :: tail✝

Tactic:
| cons _ _ ih =>

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: case cons
α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
head✝ : α
tail✝ : List α
ih : ∀ (n : ℕ), (List.foldl (fun l x ↦ { down := l.down + 1 }) { down := n } tail✝).down = tail✝.length + n
n : ℕ
⊢ (List.foldl (fun l x ↦ { down := l.down + 1 }) { down := n } (head✝ :: tail✝)).down = (head✝ :: tail✝).length + n

Tactic:
| cons _ _ ih =>

Goal state after:
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁶ : Traversable t
inst✝⁵ : LawfulTraversable t
inst✝⁴ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
x✝² : β✝ → F✝ γ✝
x✝¹ : α✝ → G✝ β✝
x✝ : t' α✝
⊢ Comp.mk (Equiv.traverse eqv x✝² <$> Equiv.traverse eqv x✝¹ x✝) = Comp.mk (traverse x✝² <$> traverse x✝¹ x✝)

Tactic:
h₂

Goal state after:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁶ : Traversable t
inst✝⁵ : LawfulTraversable t
inst✝⁴ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
x✝² : β✝ → F✝ γ✝
x✝¹ : α✝ → G✝ β✝
x✝ : t' α✝
⊢ Comp.mk (Equiv.traverse eqv x✝² <$> Equiv.traverse eqv x✝¹ x✝) = Comp.mk (Equiv.traverse eqv x✝² <$> traverse x✝¹ x✝)
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: case e_a
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁶ : Traversable t
inst✝⁵ : LawfulTraversable t
inst✝⁴ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
x✝² : β✝ → F✝ γ✝
x✝¹ : α✝ → G✝ β✝
x✝ : t' α✝
⊢ Equiv.traverse eqv x✝¹ x✝ = traverse x✝¹ x✝

Tactic:
h₂

Goal state after:
case e_a
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁶ : Traversable t
inst✝⁵ : LawfulTraversable t
inst✝⁴ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
x✝² : β✝ → F✝ γ✝
x✝¹ : α✝ → G✝ β✝
x✝ : t' α✝
⊢ Equiv.traverse eqv x✝¹ x✝ = Equiv.traverse eqv x✝¹ x✝
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁶ : Traversable t
inst✝⁵ : LawfulTraversable t
inst✝⁴ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
x✝⁴ : ApplicativeTransformation F✝ G✝
x✝³ x✝² : Type u
x✝¹ : x✝³ → F✝ x✝²
x✝ : t' x✝³
⊢ Equiv.traverse eqv ((fun {α} ↦ x✝⁴.app α) ∘ x✝¹) x✝ = traverse ((fun {α} ↦ x✝⁴.app α) ∘ x✝¹) x✝

Tactic:
h₂

Goal state after:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁶ : Traversable t
inst✝⁵ : LawfulTraversable t
inst✝⁴ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
x✝⁴ : ApplicativeTransformation F✝ G✝
x✝³ x✝² : Type u
x✝¹ : x✝³ → F✝ x✝²
x✝ : t' x✝³
⊢ Equiv.traverse eqv ((fun {α} ↦ x✝⁴.app α) ∘ x✝¹) x✝ = Equiv.traverse eqv ((fun {α} ↦ x✝⁴.app α) ∘ x✝¹) x✝