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

Goal state before:
pp: case some.load
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
x✝ : TM1.Cfg Γ Λ σ
l₁ : Λ
a✝¹ : Γ → σ → σ
a✝ : TM1.Stmt Γ Λ σ
IH :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝ v T).var),
        Tape := (TM1.stepAux a✝ v T).Tape }
v : σ
T : Tape Γ
⊢ Reaches₁ (TM0.step (tr M)) { q := (some (TM1.Stmt.load a✝¹ a✝), v), Tape := T }
    {
      q :=
        (match (TM1.stepAux (TM1.Stmt.load a✝¹ a✝) v T).l with
          | some x => some (M x)
          | none => none,
          (TM1.stepAux (TM1.Stmt.load a✝¹ a✝) v T).var),
      Tape := (TM1.stepAux (TM1.Stmt.load a✝¹ a✝) v T).Tape }

Tactic:
| load _ _ IH =>

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

Goal state before:
pp: case succ.left
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
⊢ ∀ (v : List.Vector Bool i), SupportsStmt S (f (true ::ᵥ v))

Tactic:
intro

Goal state after:
case succ.left
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
v✝ : List.Vector Bool i
⊢ SupportsStmt S (f (true ::ᵥ v✝))
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case succ.right
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
⊢ ∀ (v : List.Vector Bool i), SupportsStmt S (f (false ::ᵥ v))

Tactic:
intro

Goal state after:
case succ.right
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
v✝ : List.Vector Bool i
⊢ SupportsStmt S (f (false ::ᵥ v✝))
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
this :
  ∀ (i : ℕ) (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
hf : ∀ (a : Γ), SupportsStmt S (f✝ a)
⊢ ∀ (v : List.Vector Bool n), SupportsStmt S (move n Dir.left (f✝ (dec v)))

Tactic:
intro

Goal state after:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
this :
  ∀ (i : ℕ) (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
hf : ∀ (a : Γ), SupportsStmt S (f✝ a)
v✝ : List.Vector Bool n
⊢ SupportsStmt S (move n Dir.left (f✝ (dec v✝)))
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
L'✝ R'✝ : ListBlank Bool
⊢ ∀ {l₁ l₂ : List Bool},
    (enc a).toList = l₁.reverseAux l₂ →
      (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L'✝) (ListBlank.append l₂ R'✝)) =
        Tape.mk' L'✝ (ListBlank.append (enc a).toList R'✝)

Tactic:
l₁

Goal state after:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
L'✝ R'✝ : ListBlank Bool
l₁ : List Bool
⊢ ∀ {l₂ : List Bool},
    (enc a).toList = l₁.reverseAux l₂ →
      (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L'✝) (ListBlank.append l₂ R'✝)) =
        Tape.mk' L'✝ (ListBlank.append (enc a).toList R'✝)
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case load
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
q₁ : Stmt Γ Λ σ
a✝¹ : σ → σ
a✝ : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ a✝ → SupportsStmt S a✝ → SupportsStmt S q₁
hs : SupportsStmt S a✝
h : q₁ = load a✝¹ a✝ ∨ q₁ ∈ stmts₁ a✝
⊢ SupportsStmt S q₁

Tactic:
| load _ _ IH =>

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

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L' R' : ListBlank Bool
⊢ ∀ (l₁ l₂ l₂' : List Bool),
    l₂'.length = l₂.length →
      stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
        stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')

Tactic:
l₁

Goal state after:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L' R' : ListBlank Bool
l₁ : List Bool
⊢ ∀ (l₂ l₂' : List Bool),
    l₂'.length = l₂.length →
      stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
        stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case load
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : Inhabited Λ
inst✝ : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
a✝¹ : σ → σ
a✝ : Stmt Γ Λ σ
IH : ∀ (v : σ) (T : (k : K) → List (Γ k)), SupportsStmt S a✝ → (stepAux a✝ v T).l ∈ Finset.insertNone S
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt S (load a✝¹ a✝)
⊢ (stepAux (load a✝¹ a✝) v T).l ∈ Finset.insertNone S

Tactic:
| load _ _ IH =>

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✝ : ℕ
⊢ ∀ (x : (k : K) → Option (Γ k)),
    { f := Prod.mk false, map_pt' := ⋯ }.f (f x) =
      (({ f := Prod.mk false, map_pt' := ⋯ }.f x).1, f ({ f := Prod.mk false, map_pt' := ⋯ }.f x).2)

Tactic:
intro

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✝ : ℕ
x✝ : (k : K) → Option (Γ k)
⊢ { f := Prod.mk false, map_pt' := ⋯ }.f (f x✝) =
    (({ f := Prod.mk false, map_pt' := ⋯ }.f x✝).1, f ({ f := Prod.mk false, map_pt' := ⋯ }.f x✝).2)
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
P : RegularExpression α
⊢ map f (P ^ 0) = map f P ^ 0

Tactic:
unfold map; rfl

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

Goal state before:
pp: n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
m : PosNum
⊢ ∀ (m : ℕ), (m + m).div2 = m

Tactic:
intro

Goal state after:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
m : PosNum
m✝ : ℕ
⊢ (m✝ + m✝).div2 = m✝
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
inst✝¹ : HasExplicitFiniteCoproducts P
inst✝ : HasExplicitPullbacksOfInclusions P
X Y Z : CompHausLike P
f : Z ⟶ X ⨿ Y
⊢ PreservesLimit (cospan coprod.inl f) (compHausLikeToTop P)

Tactic:
infer_instance

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

Goal state before:
pp: P : TopCat → Prop
inst✝¹ : HasExplicitPullbacks P
inst✝ : HasExplicitFiniteCoproducts P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)
this : Preregular (CompHausLike P)
⊢ Precoherent (CompHausLike P)

Tactic:
infer_instance

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

Goal state before:
pp: case h_empty
X : Type u_4
I : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : TotallyDisconnectedSpace X
inst✝ : Finite I
Z D : PEmpty.{u_5 + 1} → Set X
Z_closed : ∀ (i : PEmpty.{u_5 + 1}), IsClosed[inst✝⁴] (Z i)
D_clopen : ∀ (i : PEmpty.{u_5 + 1}), IsClopen (D i)
Z_subset_D : ∀ (i : PEmpty.{u_5 + 1}), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
⊢ ∃ C,
    (∀ (i : PEmpty.{u_5 + 1}), IsClopen (C i)) ∧
      (∀ (i : PEmpty.{u_5 + 1}), Z i ⊆ C i) ∧
        (∀ (i : PEmpty.{u_5 + 1}), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C

Tactic:
| h_empty =>

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

Goal state before:
pp: case e_a
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v v' : List ℕ
⊢ eval step (Cfg.ret (Cont.cons₂ v k) v') = eval step (Cfg.ret k (v.headI :: v'))

Tactic:
refine Eq.trans (b := eval step (stepRet (Cont.cons₂ v k) v')) ?_ (Eq.symm ?_) <;>
      exact reaches_eval (ReflTransGen.single rfl)

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

Goal state before:
pp: case nil
q : Λ'
c : List Γ'
s : Option Γ'
a d : List Γ'
⊢ Reaches₁ (TM2.step tr) { l := some q.copy, var := s, stk := elim a [] c d }
    { l := some q, var := none, stk := elim ([].reverseAux a) [] c ([].reverseAux d) }

Tactic:
refine TransGen.single ?_
    simp

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

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

Tactic:
induction b generalizing a d s with
  | nil =>
    refine TransGen.single ?_
    simp
  | cons x b IH =>
    refine TransGen.head rfl ?_
    rw [tr]
    simp only [TM2.step, Option.mem_def, TM2.stepAux, elim_rev, List.head?_cons, Option.isSome_some,
      List.tail_cons, elim_update_rev, elim_main, elim_update_main,
      elim_stack, elim_update_stack, cond_true, List.reverseAux_cons, pop', push']
    exact IH _ _ _

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

Goal state before:
pp: case mp
X : CompHaus
h : Projective X
⊢ ExtremallyDisconnected ↑X.toStonean.toTop

Tactic:
infer_instance

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

Goal state before:
pp: case pos.bit0
q : Λ'
n : ℕ
c d : List Γ'
m : PosNum
a_ih✝ :
  ∀ {s : Option Γ'} (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum m ++ [Γ'.cons]) l₁ c d }
          { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
s : Option Γ'
l₁ : List Γ'
⊢ ∃ l₁' l₂' s',
    l₁.reverseAux (trPosNum m.bit0.succ) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum m.bit0 ++ [Γ'.cons]) l₁ c d }
        { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }

Tactic:
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.Condensed.Limits

Goal state before:
pp: ⊢ HasLimits (Sheaf (coherentTopology CompHaus) (Type (u + 1)))

Tactic:
infer_instance

Goal state after:
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 Γ'
⊢ ∃ 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:
obtain ⟨s', h₁, h₂⟩ := trNormal_respects fs (Cont.cons₂ v k) as none

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'
⊢ ∃ 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₂
Module: Mathlib.Topology.Category.LightProfinite.EffectiveEpi

Goal state before:
pp: X Y : LightProfinite
f : X ⟶ Y
h : EffectiveEpi f
⊢ Epi f

Tactic:
infer_instance

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

Goal state before:
pp: case left
J : Type v
inst✝¹ : SmallCategory J
inst✝ : CountableCategory J
F : J ⥤ LightProfinite
⊢ TotallyDisconnectedSpace ↑(CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).pt.toTop

Tactic:
infer_instance

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

Goal state before:
pp: S : LightProfinite
⊢ SecondCountableTopology ↑S.toTop

Tactic:
infer_instance

Goal state after:
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
    ((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)

Tactic:
infer_instance

Goal state after:
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
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) (Fin 2)
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
let U := f ⁻¹' {0}

Goal state after:
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}
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
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)
⊢ IsIso
    ((X.mapIso
          (opCoproductIsoProduct' (finiteCoproduct.isColimit fun a ↦ of P (σ a))
            (productIsProduct fun x ↦ Opposite.op (of P (σ x))))).hom ≫
      (PreservesProduct.iso X fun a ↦ Opposite.op (of P (σ a))).hom ≫
        (Types.productIso fun a ↦ X.obj (Opposite.op (of P (σ a)))).hom)

Tactic:
infer_instance

Goal state after:
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:
intro

Goal state after:
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))
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case fix
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.fix f k) ⊆ S
⊢ Supports (contSupp (Cont'.fix f k)) S

Tactic:
rw [contSupp] at H

Goal state after:
case fix
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : codeSupp' f.fix k ∪ contSupp k ⊆ S
⊢ Supports (contSupp (Cont'.fix f k)) S
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: case refine_2
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)
i j : I
fi : LocallyConstant (↑((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
fj : LocallyConstant (↑((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op j))).toTop) X
h✝¹ :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : I
ki : k ⟶ i
kj : k ⟶ j
h✝ : True
x✝ : ↑(toProfinite.obj (F.obj k)).toTop
x : ↑(((const I).obj c.pt).obj k).toTop
hx : (ConcreteCategory.hom (c.π.app k)) x = x✝
h :
  (LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi) x =
    (LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj) x
⊢ fi ((ConcreteCategory.hom (c.π.app k ≫ toProfinite.map (F.map ki))) x) =
    fj ((ConcreteCategory.hom (c.π.app k ≫ toProfinite.map (F.map kj))) x)

Tactic:
rwa [dsimp% c.w, dsimp% c.w]

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

Goal state before:
pp: case refine_2
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
i j : ℕᵒᵖ
fi : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
fj : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op j))).toTop) X
h✝¹ :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : ℕᵒᵖ
ki : k ⟶ i
kj : k ⟶ j
h✝ : True
x✝ : ↑(toLightProfinite.obj (F.obj k)).toTop
x : ↑(((const ℕᵒᵖ).obj c.pt).obj k).toTop
hx : (ConcreteCategory.hom (c.π.app k)) x = x✝
h :
  (LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi) x =
    (LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj) x
⊢ fi ((ConcreteCategory.hom (c.π.app k ≫ toLightProfinite.map (F.map ki))) x) =
    fj ((ConcreteCategory.hom (c.π.app k ≫ toLightProfinite.map (F.map kj))) x)

Tactic:
rwa [dsimp% c.w, dsimp% c.w]

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

Goal state before:
pp: n✝ : ℕ
R : Type u
inst✝¹ : Ring R
M N : ℕ → LightCondMod R
f : (n : ℕ) → M n ⟶ N n
inst✝ : ∀ (n : ℕ), Epi (f n)
n : ℕ
⊢ Epi (functorMap f n)

Tactic:
infer_instance

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

Goal state before:
pp: n : ℕ
R : Type u
inst✝¹ : Ring R
M N : ℕ → LightCondMod R
f✝ : (n : ℕ) → M n ⟶ N n
inst✝ : ∀ (n : ℕ), Epi (f✝ n)
X✝ Y✝ : Discrete ℕ ⥤ LightCondMod R
f : X✝ ⟶ Y✝
x✝ : Epi f
this : lim.map f = (Pi.isoLimit X✝).inv ≫ (Limits.Pi.map fun x ↦ f.app { as := x }) ≫ (Pi.isoLimit Y✝).hom
⊢ Epi ((Pi.isoLimit X✝).inv ≫ (Limits.Pi.map fun x ↦ f.app { as := x }) ≫ (Pi.isoLimit Y✝).hom)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Condensed.Solid

Goal state before:
pp: R : Type (u + 1)
inst✝ : Ring R
⊢ (FintypeCat.toProfinite.rightKanExtension (finFree R)).IsRightKanExtension
    (FintypeCat.toProfinite.rightKanExtensionCounit (finFree R))

Tactic:
infer_instance

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

Goal state before:
pp: α✝ β✝ γ✝ : Type ?u.4
k : α✝ ≃ β✝
h : β✝ ≃ γ✝
x✝ : Finset α✝
a✝ : γ✝
⊢ a✝ ∈ Finset.map (k.trans h).toEmbedding x✝ ↔
    a✝ ∈ ((fun s ↦ Finset.map h.toEmbedding s) ∘ fun s ↦ Finset.map k.toEmbedding s) x✝

Tactic:
simp [-trans_toEmbedding]

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
n✝ : ℕ
i_ih : approx (⇑f) n✝ ≤ approx (⇑f) n✝.succ
⊢ approx (⇑f) (n✝ + 1) ≤ approx (⇑f) (n✝ + 1).succ

Tactic:
intro

Goal state after:
case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
n✝ : ℕ
i_ih : approx (⇑f) n✝ ≤ approx (⇑f) n✝.succ
i✝ : α
⊢ approx (⇑f) (n✝ + 1) i✝ ≤ approx (⇑f) (n✝ + 1).succ i✝
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∀ (x : ℕ) (x_1 : β a), x_1 ∉ approx (⇑f) x a
⊢ ∀ (x : ℕ), b ∉ approx (⇑f) x a

Tactic:
intro

Goal state after:
case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∀ (x : ℕ) (x_1 : β a), x_1 ∉ approx (⇑f) x a
x✝ : ℕ
⊢ b ∉ approx (⇑f) x✝ a
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
α β : Type u
f : α → β
x : t' α
⊢ Equiv.traverse eqv (pure ∘ f) x = pure (Equiv.map eqv f x)

Tactic:
simp only [Equiv.traverse, traverse_eq_map_id]; rfl

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

Goal state before:
pp: case refine_1
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this✝ : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) :=
  fun n ↦ { hom := TopCat.ofHom { toFun := fun x ↦ ↑x n, continuous_toFun := ⋯ } }
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S :=
  ConcreteCategory.ofHom { toFun := y ⇑(ConcreteCategory.hom π), continuous_toFun := ⋯ }
π' : pullback π (y' ▷ ℕ∪{∞}) ⟶ LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⊗ ℕ∪{∞} := pullback.snd π (y' ▷ ℕ∪{∞})
σ' : ↑ℕ∪{∞}.toTop → ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop → ↑(pullback π (y' ▷ ℕ∪{∞})).toTop :=
  fun n ↦
    ⇑(ConcreteCategory.hom
        (pullback.lift π (y' ▷ ℕ∪{∞}) (S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞}))
          (lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
            (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n))
          ⋯))
hσ :
  ∀ (x : ↑ℕ∪{∞}.toTop) (s : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop),
    ((ConcreteCategory.hom π') (σ' x s)).1 = s
hσ' :
  ∀ (x : ↑ℕ∪{∞}.toTop) (s : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop),
    ((ConcreteCategory.hom π') (σ' x s)).2 = x
this : CompactSpace ↑(fibres (⇑(ConcreteCategory.hom π')) σ')
⊢ Epi (pullback.snd π (y' ▷ ℕ∪{∞}))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
⊢ ∀ (h : ∀ a_1 ∈ mk aq, ∀ b ∈ mk aq, f a_1 = f b), (mk aq).liftOn f h = f a

Tactic:
intro

Goal state after:
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
h✝ : ∀ a_1 ∈ mk aq, ∀ b ∈ mk aq, f a_1 = f b
⊢ (mk aq).liftOn f h✝ = f a
Module: Mathlib.Data.Fin.Init

Goal state before:
pp: k : ℕ
a b : Fin k
⊢ a ^^^ b = b ^^^ a

Tactic:
grind [Fin.xor_val]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Embedding

Goal state before:
pp: α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : ¬a ∈ range ⇑x
i : Fin n
⊢ Fin.snoc (⇑x) a i.castSucc = x i

Tactic:
Fin.snoc_castSucc

Goal state after:
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : ¬a ∈ range ⇑x
i : Fin n
⊢ x i = x i