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

Goal state before:
pp: case cons.cons.false
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := o, stk := update S k L₂ }
s : Option Γ'
S : K' → List Γ'
a' : Γ'
Sk : List Γ'
e :
  (bif p a' then ([], some a', Sk)
    else
      match splitAtPred p Sk with
      | (l₁, o, l₂) => (a' :: l₁, o, l₂)) =
    (a :: L₁, o, L₂)
e₁ : S k = a' :: Sk
e₂ : p a' = false
⊢ 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)
    (bif
        match (a' :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (a' :: Sk).head?, stk := update S k (a' :: Sk).tail }
    else { l := some (Λ'.clear p k q), var := (a' :: Sk).head?, stk := update S k (a' :: Sk).tail })
    { l := some q, var := o, stk := update S k L₂ }

Tactic:
simp only [e₂, cond] at e

Goal state after:
case cons.cons.false
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := o, stk := update S k L₂ }
s : Option Γ'
S : K' → List Γ'
a' : Γ'
Sk : List Γ'
e₁ : S k = a' :: Sk
e₂ : p a' = false
e : (a' :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2) = (a :: 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)
    (bif
        match (a' :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (a' :: Sk).head?, stk := update S k (a' :: Sk).tail }
    else { l := some (Λ'.clear p k q), var := (a' :: Sk).head?, stk := update S k (a' :: Sk).tail })
    { l := some q, var := o, stk := update S k L₂ }
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons.cons.true
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := o, stk := update S k L₂ }
s : Option Γ'
S : K' → List Γ'
a' : Γ'
Sk : List Γ'
e :
  (bif p a' then ([], some a', Sk)
    else
      match splitAtPred p Sk with
      | (l₁, o, l₂) => (a' :: l₁, o, l₂)) =
    (a :: L₁, o, L₂)
e₁ : S k = a' :: Sk
e₂ : p a' = true
⊢ 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)
    (bif
        match (a' :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (a' :: Sk).head?, stk := update S k (a' :: Sk).tail }
    else { l := some (Λ'.clear p k q), var := (a' :: Sk).head?, stk := update S k (a' :: Sk).tail })
    { l := some q, var := o, stk := update S k L₂ }

Tactic:
simp only [e₂, cond] at e

Goal state after:
case cons.cons.true
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := o, stk := update S k L₂ }
s : Option Γ'
S : K' → List Γ'
a' : Γ'
Sk : List Γ'
e₁ : S k = a' :: Sk
e₂ : p a' = true
e : ([], some a', Sk) = (a :: 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)
    (bif
        match (a' :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (a' :: Sk).head?, stk := update S k (a' :: Sk).tail }
    else { l := some (Λ'.clear p k q), var := (a' :: Sk).head?, stk := update S k (a' :: Sk).tail })
    { l := some q, var := o, stk := update S k L₂ }
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case hf
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 : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
U : Set (X i)
a✝ : IsOpen U
j : ι
⊢ IsOpen (Sigma.mk j ⁻¹' Sigma.mk i '' U)

Tactic:
by_cases ij : i = j

Goal state after:
case pos
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 : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
U : Set (X i)
a✝ : IsOpen U
j : ι
ij : i = j
⊢ IsOpen (Sigma.mk j ⁻¹' Sigma.mk i '' U)

case neg
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 : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
U : Set (X i)
a✝ : IsOpen U
j : ι
ij : ¬i = j
⊢ IsOpen (Sigma.mk j ⁻¹' Sigma.mk i '' U)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
⊢ Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trList [n]) [] c d }
    { l := some q, var := none, stk := elim (trList [n.succ]) [] c d }

Tactic:
simp only [trList, trNat.eq_1, Nat.cast_succ, Num.add_one]
  rcases (n : Num) with - | a
  · refine TransGen.head rfl ?_
    simp only [Option.mem_def]
    convert! unrev_ok using 1
    simp only [elim_update_rev, elim_rev, elim_main, List.reverseAux_nil, elim_update_main]
    rfl
  simp only [trNum, Num.succ, Num.succ']
  suffices ∀ l₁, ∃ l₁' l₂' s',
      List.reverseAux l₁ (trPosNum a.succ) = List.reverseAux l₁' l₂' ∧
        Reaches₁ (TM2.step tr) ⟨some q.succ, s, K'.elim (trPosNum a ++ [Γ'.cons]) l₁ c d⟩
          ⟨some (unrev q), s', K'.elim (l₂' ++ [Γ'.cons]) l₁' c d⟩ by
    obtain ⟨l₁', l₂', s', e, h⟩ := this []
    simp only [List.reverseAux] at e
    refine h.trans ?_
    convert! unrev_ok using 2
    simp [e, List.reverseAux_eq]
  induction a generalizing s with intro l₁
  | one =>
    refine ⟨Γ'.bit0 :: l₁, [Γ'.bit1], some Γ'.cons, rfl, TransGen.head rfl (TransGen.single ?_)⟩
    simp [trPosNum]
  | bit1 m IH =>
    obtain ⟨l₁', l₂', s', e, h⟩ := IH (Γ'.bit0 :: l₁)
    refine ⟨l₁', l₂', s', e, TransGen.head ?_ h⟩
    simp [trPosNum]
    rfl
  | bit0 m _ =>
    refine ⟨l₁, _, some Γ'.bit0, rfl, TransGen.single ?_⟩
    simp only [TM2.step]; rw [tr]
    simp only [TM2.stepAux, pop', elim_main, elim_update_main,
      elim_rev, elim_update_rev, Function.update_self, Option.mem_def, Option.some.injEq]
    rfl

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
A : DiscreteQuotient X
⊢ map (ContinuousMap.id X) ⋯ = id

Tactic:
ext ⟨⟩; rfl

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
A : DiscreteQuotient X
B B' : DiscreteQuotient Y
cond : LEComap f A B
h : B ≤ B'
a : Quotient A.toSetoid
⊢ ofLE h (map f cond a) = map f ⋯ a

Tactic:
by
  rcases a with ⟨⟩
  rfl

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
toSetoid✝¹ : Setoid X
isOpen_setOfPred_rel✝¹ : ∀ (x : X), IsOpen[inst✝¹] (ofPred (toSetoid✝¹ x))
toSetoid✝ : Setoid X
isOpen_setOfPred_rel✝ : ∀ (x : X), IsOpen[inst✝¹] (ofPred (toSetoid✝ x))
h :
  (fun x ↦
        match x with
        | { toSetoid := f, isOpen_setOfPred_rel := isOpen_setOfPred_rel } => f.classes)
      { toSetoid := toSetoid✝¹, isOpen_setOfPred_rel := isOpen_setOfPred_rel✝¹ } =
    (fun x ↦
        match x with
        | { toSetoid := f, isOpen_setOfPred_rel := isOpen_setOfPred_rel } => f.classes)
      { toSetoid := toSetoid✝, isOpen_setOfPred_rel := isOpen_setOfPred_rel✝ }
⊢ toSetoid✝¹ = toSetoid✝

Tactic:
Setoid.classes_inj

Goal state after:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
toSetoid✝¹ : Setoid X
isOpen_setOfPred_rel✝¹ : ∀ (x : X), IsOpen[inst✝¹] (ofPred (toSetoid✝¹ x))
toSetoid✝ : Setoid X
isOpen_setOfPred_rel✝ : ∀ (x : X), IsOpen[inst✝¹] (ofPred (toSetoid✝ x))
h :
  (fun x ↦
        match x with
        | { toSetoid := f, isOpen_setOfPred_rel := isOpen_setOfPred_rel } => f.classes)
      { toSetoid := toSetoid✝¹, isOpen_setOfPred_rel := isOpen_setOfPred_rel✝¹ } =
    (fun x ↦
        match x with
        | { toSetoid := f, isOpen_setOfPred_rel := isOpen_setOfPred_rel } => f.classes)
      { toSetoid := toSetoid✝, isOpen_setOfPred_rel := isOpen_setOfPred_rel✝ }
⊢ toSetoid✝¹.classes = toSetoid✝.classes
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons.succ
f : Code
k : Cont
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₂
s : Option Γ'
tail✝ : List ℕ
n : ℕ
⊢ if ((n + 1) :: tail✝).headI = 0 then
    natEnd ((trList ((n + 1) :: tail✝)).head?.getD default) = true ∧
      (trList ((n + 1) :: tail✝)).tail = trList ((n + 1) :: tail✝).tail
  else
    natEnd ((trList ((n + 1) :: tail✝)).head?.getD default) = false ∧
      (trList ((n + 1) :: tail✝)).tail =
        (trNat ((n + 1) :: tail✝).headI).tail ++ Γ'.cons :: trList ((n + 1) :: tail✝).tail

Tactic:
rw [trList, List.headI, trNat, Nat.cast_succ, Num.add_one, Num.succ, List.tail]

Goal state after:
case cons.succ
f : Code
k : Cont
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₂
s : Option Γ'
tail✝ : List ℕ
n : ℕ
⊢ if n + 1 = 0 then
    natEnd ((trNum (Num.pos (↑n).succ') ++ Γ'.cons :: trList tail✝).head?.getD default) = true ∧
      (trNum (Num.pos (↑n).succ') ++ Γ'.cons :: trList tail✝).tail = trList tail✝
  else
    natEnd ((trNum (Num.pos (↑n).succ') ++ Γ'.cons :: trList tail✝).head?.getD default) = false ∧
      (trNum (Num.pos (↑n).succ') ++ Γ'.cons :: trList tail✝).tail =
        (trNum (Num.pos (↑n).succ')).tail ++ Γ'.cons :: trList tail✝
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: X✝ Y✝ : LightDiagram
f : X✝ ⟶ Y✝
⊢ lightDiagramToProfinite.map
      (InducedCategory.homMk (InducedCategory.homMk f.hom.hom) ≫
        lightDiagramToProfinite.preimage (𝟙 (of ↑Y✝.cone.pt.toTop).toLightDiagram.toProfinite)) =
    lightDiagramToProfinite.map
      (lightDiagramToProfinite.preimage (𝟙 (of ↑X✝.cone.pt.toTop).toLightDiagram.toProfinite) ≫ f)

Tactic:
apply InducedCategory.hom_ext

Goal state after:
X✝ Y✝ : LightDiagram
f : X✝ ⟶ Y✝
⊢ (lightDiagramToProfinite.map
        (InducedCategory.homMk (InducedCategory.homMk f.hom.hom) ≫
          lightDiagramToProfinite.preimage (𝟙 (of ↑Y✝.cone.pt.toTop).toLightDiagram.toProfinite))).hom =
    (lightDiagramToProfinite.map
        (lightDiagramToProfinite.preimage (𝟙 (of ↑X✝.cone.pt.toTop).toLightDiagram.toProfinite) ≫ f)).hom
Module: Mathlib.Topology.Category.TopCat.Yoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ TopCat
Y : Type w'
inst✝ : TopologicalSpace Y
x✝ : ℕ
K : Discrete (Fin x✝) ⥤ TopCatᵒᵖ
α✝ : Type
X : α✝ → TopCat
⊢ IsIso (piComparison (yonedaPresheaf' Y) fun x ↦ op (X x))

Tactic:
piComparison_fac

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ TopCat
Y : Type w'
inst✝ : TopologicalSpace Y
x✝ : ℕ
K : Discrete (Fin x✝) ⥤ TopCatᵒᵖ
α✝ : Type
X : α✝ → TopCat
⊢ IsIso
    ((yonedaPresheaf' Y).map ((opCoproductIsoProduct X).inv ≫ (TopCat.sigmaIsoSigma X).inv.op) ≫
      (equivEquivIso (sigmaEquiv Y fun x ↦ ↑(X x))).inv ≫ (Types.productIso fun i ↦ C(↑(X i), Y)).inv)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: q q' : Λ'
⊢ q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q

Tactic:
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 => _ <;>
  all_goals
    simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
    repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

Goal state after:
case read
q' : Λ'
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)
⊢ (q' ∈ Finset.univ.biUnion fun s ↦ trStmts₁ (q s)) →
    trStmts₁ q' ⊆ insert (Λ'.read q) (Finset.univ.biUnion fun s ↦ trStmts₁ (q s))

case succ
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ (q' = unrev q → trStmts₁ (unrev q) ⊆ insert q.succ (insert (unrev q) (trStmts₁ q))) ∧
    (q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert q.succ (insert (unrev q) (trStmts₁ q)))

case pred
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
⊢ (q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))) ∧
    (q' = unrev q₂ → trStmts₁ (unrev q₂) ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))) ∧
      (q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂)))
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: S : Finset Λ'
k : K'
q : Λ'
H : Λ'.Supports S q
x✝ : Option Γ'
⊢ Λ'.Supports S ((if x✝ = some Γ'.consₗ then id else Λ'.clear (fun x ↦ decide (x = Γ'.consₗ)) k) (unrev q))

Tactic:
split_ifs

Goal state after:
case pos
S : Finset Λ'
k : K'
q : Λ'
H : Λ'.Supports S q
x✝ : Option Γ'
h✝ : x✝ = some Γ'.consₗ
⊢ Λ'.Supports S (id (unrev q))

case neg
S : Finset Λ'
k : K'
q : Λ'
H : Λ'.Supports S q
x✝ : Option Γ'
h✝ : ¬x✝ = some Γ'.consₗ
⊢ Λ'.Supports S (Λ'.clear (fun x ↦ decide (x = Γ'.consₗ)) k (unrev q))
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

Goal state after:
case pos
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.succ k ⊆ S
s✝ : Option Γ'
h✝ : s✝ = some Γ'.consₗ
⊢ Λ'.Supports S (id (unrev (Λ'.ret k).succ))

case neg
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.succ k ⊆ S
s✝ : Option Γ'
h✝ : ¬s✝ = some Γ'.consₗ
⊢ Λ'.Supports S (Λ'.clear (fun x ↦ decide (x = Γ'.consₗ)) main (unrev (Λ'.ret k).succ))
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
IHfs : ∀ {k : Cont'}, codeSupp fs k ⊆ S → Supports (codeSupp' fs k) S
k : Cont'
H : codeSupp (f.cons fs) k ⊆ S
H' : trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧ codeSupp f (Cont'.cons₁ fs k) ⊆ S
h :
  codeSupp' f (Cont'.cons₁ fs k) ∪
      (trStmts₁
          (move₂ (fun x ↦ false) main aux
            (move₂ (fun s ↦ decide (s = Γ'.consₗ)) stack main
              (move₂ (fun x ↦ false) aux stack (trNormal fs k.cons₂)))) ∪
        (codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k)))) ⊆
    S
⊢ Supports
    (codeSupp' f (Cont'.cons₁ fs k) ∪
      (trStmts₁
          (move₂ (fun x ↦ false) main aux
            (move₂ (fun s ↦ decide (s = Γ'.consₗ)) stack main
              (move₂ (fun x ↦ false) aux stack (trNormal fs k.cons₂)))) ∪
        (codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k)))))
    S

Tactic:
refine supports_union.2 ⟨IHf H'.2, ?_⟩

Goal state after:
case cons
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
IHfs : ∀ {k : Cont'}, codeSupp fs k ⊆ S → Supports (codeSupp' fs k) S
k : Cont'
H : codeSupp (f.cons fs) k ⊆ S
H' : trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧ codeSupp f (Cont'.cons₁ fs k) ⊆ S
h :
  codeSupp' f (Cont'.cons₁ fs k) ∪
      (trStmts₁
          (move₂ (fun x ↦ false) main aux
            (move₂ (fun s ↦ decide (s = Γ'.consₗ)) stack main
              (move₂ (fun x ↦ false) aux stack (trNormal fs k.cons₂)))) ∪
        (codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k)))) ⊆
    S
⊢ Supports
    (trStmts₁
        (move₂ (fun x ↦ false) main aux
          (move₂ (fun s ↦ decide (s = Γ'.consₗ)) stack main (move₂ (fun x ↦ false) aux stack (trNormal fs k.cons₂)))) ∪
      (codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k))))
    S
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case fix
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
k : Cont'
H : codeSupp f.fix k ⊆ S
H' : trStmts₁ (trNormal f.fix k) ⊆ S ∧ codeSupp f (Cont'.fix f k) ⊆ S
h : codeSupp' f (Cont'.fix f k) ∪ (trStmts₁ (Λ'.clear natEnd main (trNormal f (Cont'.fix f k))) ∪ {Λ'.ret k}) ⊆ S
⊢ Supports (codeSupp' f (Cont'.fix f k) ∪ (trStmts₁ (Λ'.clear natEnd main (trNormal f (Cont'.fix f k))) ∪ {Λ'.ret k})) S

Tactic:
refine supports_union.2 ⟨IHf H'.2, ?_⟩

Goal state after:
case fix
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
k : Cont'
H : codeSupp f.fix k ⊆ S
H' : trStmts₁ (trNormal f.fix k) ⊆ S ∧ codeSupp f (Cont'.fix f k) ⊆ S
h : codeSupp' f (Cont'.fix f k) ∪ (trStmts₁ (Λ'.clear natEnd main (trNormal f (Cont'.fix f k))) ∪ {Λ'.ret k}) ⊆ S
⊢ Supports (trStmts₁ (Λ'.clear natEnd main (trNormal f (Cont'.fix f k))) ∪ {Λ'.ret k}) S
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})))
inst✝¹ : PreservesFiniteProducts Y
inst✝ : HasExplicitFiniteCoproducts P
a : Fiber ⇑f
⊢ (ConcreteCategory.hom (Y.map (sigmaIso f).op.hom ≫ (sigmaComparison Y fun a ↦ ↑(fiber f a).toTop) ≫ ↾fun g ↦ g a))
      ((ConcreteCategory.hom (counitAppApp S Y)) f) =
    counitAppAppImage f a

Tactic:
Iso.op_hom,

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})))
inst✝¹ : PreservesFiniteProducts Y
inst✝ : HasExplicitFiniteCoproducts P
a : Fiber ⇑f
⊢ (ConcreteCategory.hom (Y.map (sigmaIso f).hom.op ≫ (sigmaComparison Y fun a ↦ ↑(fiber f a).toTop) ≫ ↾fun g ↦ g a))
      ((ConcreteCategory.hom (counitAppApp S Y)) f) =
    counitAppAppImage f a
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 Y : Sheaf (coherentTopology (CompHausLike P)) (Type (max u w))
g : X ⟶ Y
this : Preregular (CompHausLike P)
⊢ ((sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj (op (of P PUnit.{u + 1})) ⋙
            functor P hs).map
        g ≫
      ObjectProperty.homMk (counitApp Y.obj) =
    ObjectProperty.homMk (counitApp X.obj) ≫ (𝟭 (Sheaf (coherentTopology (CompHausLike P)) (Type (max u w)))).map g

Tactic:
apply InducedCategory.hom_ext

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 Y : Sheaf (coherentTopology (CompHausLike P)) (Type (max u w))
g : X ⟶ Y
this : Preregular (CompHausLike P)
⊢ (((sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj (op (of P PUnit.{u + 1})) ⋙
              functor P hs).map
          g ≫
        ObjectProperty.homMk (counitApp Y.obj)).hom =
    (ObjectProperty.homMk (counitApp X.obj) ≫
        (𝟭 (Sheaf (coherentTopology (CompHausLike P)) (Type (max u w)))).map g).hom
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
⊢ (lanPresheafNatIso fun x ↦
          isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))) x).inv ≫
      (lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom =
    counitApp X

Tactic:
Iso.inv_comp_eq

Goal state after:
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
⊢ (lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom =
    (lanPresheafNatIso fun x ↦
          isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))) x).hom ≫
      counitApp X
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: X : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts X
hX : (S : LightProfinite) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
⊢ (lanPresheafNatIso fun x ↦
          isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) x).inv ≫
      (lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom =
    counitApp X

Tactic:
Iso.inv_comp_eq

Goal state after:
X : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts X
hX : (S : LightProfinite) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
⊢ (lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom =
    (lanPresheafNatIso fun x ↦
          isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) x).hom ≫
      counitApp X
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case id_traverse
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α α✝ : Type u
x✝ : t α α✝
⊢ traverse pure x✝ = pure x✝

Tactic:
simp [traverse, comp_tsnd, functor_norm]

Goal state after:
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case comp_traverse
t : Type u → Type u → Type u
inst✝⁶ : Bitraversable t
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : LawfulBitraversable t
α : Type u
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
f✝ : β✝ → F✝ γ✝
g✝ : α✝ → G✝ β✝
x✝ : t α α✝
⊢ traverse (Comp.mk ∘ map f✝ ∘ g✝) x✝ = Comp.mk (traverse f✝ <$> traverse g✝ x✝)

Tactic:
simp [traverse, comp_tsnd, functor_norm]

Goal state after: