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

Goal state before:
pp: case tail
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ b✝ c✝ : σ₂
a✝ : ReflTransGen (fun a b ↦ b ∈ f₂ a) a₂ b✝
cd : c✝ ∈ f₂ b✝
IH : ∃ c₁ c₂, Reaches f₂ b✝ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
⊢ ∃ c₁ c₂, Reaches f₂ c✝ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
rcases IH with ⟨e₁, e₂, ce, ee, ae⟩
    rcases ReflTransGen.cases_head ce with (rfl | ⟨d', cd', de⟩)
    · have := H ee
      revert this
      rcases eg : f₁ e₁ with - | g₁ <;> simp only [and_imp, exists_imp]
      · intro c0
        cases cd.symm.trans c0
      · intro g₂ gg cg
        rcases TransGen.head'_iff.1 cg with ⟨d', cd', dg⟩
        cases Option.mem_unique cd cd'
        exact ⟨_, _, dg, gg, ae.tail eg⟩
    · cases Option.mem_unique cd cd'
      exact ⟨_, _, de, ee, ae⟩

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l : List Γ
⊢ (List.map f.f l).headI = f.f l.headI

Tactic:
cases l <;> [exact (PointedMap.map_pt f).symm; rfl]

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

Goal state before:
pp: n✝² : ℕ
f✝¹ : List.Vector ℕ n✝² →. ℕ
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ → ℕ
n✝ : ℕ
f : List.Vector ℕ n✝ → ℕ
g : List.Vector ℕ (n✝ + 2) → ℕ
a✝² : Nat.Primrec' f
a✝¹ : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n✝ + 1)
hf : cf.eval (↑v).tail = pure (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v).tail) = pure (pure (g (a ::ᵥ b ::ᵥ v.tail)))
n : ℕ
a✝ :
  (cf.prec cg).eval (n :: (↑v).tail) =
    pure (pure (Nat.rec (f (n ::ᵥ v.tail).tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ (n ::ᵥ v.tail).tail)) (n ::ᵥ v.tail).head))
this :
  ∀ (a b : ℕ),
    a + b = n →
      n.succ :: 0 :: g (n ::ᵥ Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) :: (↑v).tail ∈
        PFun.fix
          (fun v ↦
            (cg.eval (v.headI :: v.tail.tail)).bind fun x ↦
              Part.some
                (if v.tail.headI = 0 then Sum.inl (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)
                else Sum.inr (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)))
          (a :: b :: Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail)
⊢ (cf.prec cg).eval ((n + 1) :: (↑v).tail) =
    pure
      (pure
        (Nat.rec (f ((n + 1) ::ᵥ v.tail).tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ ((n + 1) ::ᵥ v.tail).tail))
          ((n + 1) ::ᵥ v.tail).head))

Tactic:
by
        have := Part.eq_some_iff.mpr (this _ _ (zero_add _))
        simp [prec, Part.bind_assoc, Bind.bind]
        simp_all

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

Goal state before:
pp: n✝ : ℕ
f✝ : List.Vector ℕ n✝ →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
v : List.Vector ℕ n
hf : ∀ (a : ℕ), cf.eval (a :: ↑v) = Part.some [f (a ::ᵥ v)]
v' : List ℕ
h1 :
  v' ∈
    PFun.fix
      (fun v ↦
        (cf.eval v).bind fun y ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (0 :: ↑v)
this :
  ∀ (v₁ : List ℕ),
    v' ∈
        PFun.fix
          (fun v ↦
            (cf.eval v).bind fun y ↦
              Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
          v₁ →
      ∀ (n_1 : ℕ),
        v₁ = n_1 :: ↑v →
          (∀ m < n_1, ¬f (m ::ᵥ v) = 0) →
            ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
⊢ ∀ m < 0, ¬f (m ::ᵥ v) = 0

Tactic:
by rintro _ ⟨⟩

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

Goal state before:
pp: P : TopCat → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst✝ : HasExplicitPullback f g
Z : CompHausLike P
a b : Z ⟶ pullback f g
z : ↑Z.toTop
hfst : (ConcreteCategory.hom (a ≫ fst f g)) z = (ConcreteCategory.hom (b ≫ fst f g)) z
hsnd : (ConcreteCategory.hom (a ≫ snd f g)) z = (ConcreteCategory.hom (b ≫ snd f g)) z
⊢ ↑((ConcreteCategory.hom a) z) = ↑((ConcreteCategory.hom b) z)

Tactic:
apply Prod.ext

Goal state after:
case fst
P : TopCat → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst✝ : HasExplicitPullback f g
Z : CompHausLike P
a b : Z ⟶ pullback f g
z : ↑Z.toTop
hfst : (ConcreteCategory.hom (a ≫ fst f g)) z = (ConcreteCategory.hom (b ≫ fst f g)) z
hsnd : (ConcreteCategory.hom (a ≫ snd f g)) z = (ConcreteCategory.hom (b ≫ snd f g)) z
⊢ (↑((ConcreteCategory.hom a) z)).1 = (↑((ConcreteCategory.hom b) z)).1

case snd
P : TopCat → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst✝ : HasExplicitPullback f g
Z : CompHausLike P
a b : Z ⟶ pullback f g
z : ↑Z.toTop
hfst : (ConcreteCategory.hom (a ≫ fst f g)) z = (ConcreteCategory.hom (b ≫ fst f g)) z
hsnd : (ConcreteCategory.hom (a ≫ snd f g)) z = (ConcreteCategory.hom (b ≫ snd f g)) z
⊢ (↑((ConcreteCategory.hom a) z)).2 = (↑((ConcreteCategory.hom b) z)).2
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case fix
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, (a✝.then k').eval v = a✝.eval v >>= k'.eval
v : List ℕ
⊢ ((fix a✝¹ a✝).then k').eval v = (fix a✝¹ a✝).eval v >>= k'.eval

Tactic:
| fix _ _ k_ih =>

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

Goal state before:
pp: case fix
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
⊢ (if v.headI = 0 then (stepRet a✝ v.tail).then k' else stepNormal a✝¹ (Cont.fix a✝¹ (a✝.then k')) v.tail) =
    (if v.headI = 0 then stepRet a✝ v.tail else stepNormal a✝¹ (Cont.fix a✝¹ a✝) v.tail).then k'

Tactic:
| fix _ _ k_ih =>

Goal state after:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case neg
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
x : X
hx : x ∉ U
⊢ ∃ a, f a = x

Tactic:
exact ⟨⟨(x, true), Or.inl ⟨hx, mem_singleton _⟩⟩, rfl⟩

Goal state after:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case neg
A E : Type u
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
G_empty : ¬G = ∅
a : A
⊢ a ∈ ρ '' G → a ∈ closure (ρ '' Gᶜ)ᶜ

Tactic:
ha

Goal state after:
case neg
A E : Type u
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
G : Set E
hG : IsOpen G
G_empty : ¬G = ∅
a : A
ha : a ∈ ρ '' G
⊢ a ∈ closure (ρ '' Gᶜ)ᶜ
Module: Mathlib.Topology.Category.Profinite.EffectiveEpi

Goal state before:
pp: α : Type
inst✝ : Finite α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
⊢ [EffectiveEpiFamily X π, Epi (Sigma.desc π), ∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b].TFAE

Tactic:
tfae_have 2 → 1
  | _ => by
    simpa [← effectiveEpi_desc_iff_effectiveEpiFamily, (effectiveEpi_tfae (Sigma.desc π)).out 0 1]
  tfae_have 1 → 2 := fun _ ↦ inferInstance
  tfae_have 3 ↔ 1 := by
    erw [((CompHaus.effectiveEpiFamily_tfae
      (fun a ↦ profiniteToCompHaus.obj (X a)) (fun a ↦ profiniteToCompHaus.map (π a))).out 2 0 :)]
    exact ⟨fun h ↦ profiniteToCompHaus.finite_effectiveEpiFamily_of_map _ _ h,
      fun _ ↦ inferInstance⟩
  tfae_finish

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

Goal state before:
pp: q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
⊢ ∀ x ∈ [], natEnd x = false

Tactic:
by rintro _ ⟨⟩

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

Goal state before:
pp: case cons.zero
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
⊢ ∃ s',
    Reaches₁ (TM2.step tr) { l := some (q₁.pred q₂), var := s, stk := elim (trList (0 :: v)) [] c d }
      (Nat.rec { l := some q₁, var := s', stk := elim (trList (0 :: v).tail) [] c d }
        (fun n x ↦ { l := some q₂, var := s', stk := elim (trList (n :: (0 :: v).tail)) [] c d }) (0 :: v).headI)

Tactic:
refine ⟨some Γ'.cons, TransGen.single ?_⟩

Goal state after:
case cons.zero
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
⊢ Nat.rec { l := some q₁, var := some Γ'.cons, stk := elim (trList (0 :: v).tail) [] c d }
      (fun n x ↦ { l := some q₂, var := some Γ'.cons, stk := elim (trList (n :: (0 :: v).tail)) [] c d })
      (0 :: v).headI ∈
    TM2.step tr { l := some (q₁.pred q₂), var := s, stk := elim (trList (0 :: v)) [] c d }
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)
⊢ ∃ I, W = I.sup fun i ↦ i.1 ×ˢ i.2

Tactic:
choose! U hxU V hxV hUV using fun x ↦ W.exists_prod_subset (a := x)
  rcases W.2.1.isCompact.elim_nhds_subcover (fun x ↦ U x ×ˢ V x) (fun x hx ↦
    (U x ×ˢ V x).2.isOpen.mem_nhds ⟨hxU x hx, hxV x hx⟩) with ⟨I, hIW, hWI⟩
  classical
  use I.image fun x ↦ (U x, V x)
  rw [Finset.sup_image]
  refine le_antisymm (fun x hx ↦ ?_) (Finset.sup_le fun x hx ↦ ?_)
  · rcases Set.mem_iUnion₂.1 (hWI hx) with ⟨i, hi, hxi⟩
    exact SetLike.le_def.1 (Finset.le_sup hi) hxi
  · exact hUV _ <| hIW _ hx

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

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

Tactic:
intro s h x h'

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

Goal state before:
pp: case succ.left
q : Λ'
q_ih : unrev q ∈ trStmts₁ q → trStmts₁ (unrev q) ⊆ trStmts₁ q
⊢ trStmts₁ (unrev q) ⊆ insert q.succ (insert (unrev q) (trStmts₁ q))

Tactic:
apply Finset.subset_insert

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

Goal state before:
pp: Y : Type u_2
Z : Type u_3
f : Y → Z
a : Fiber f
⊢ (↑a).Nonempty

Tactic:
refine ⟨preimage f a, ?_⟩

Goal state after:
Y : Type u_2
Z : Type u_3
f : Y → Z
a : Fiber f
⊢ preimage f a ∈ ↑a
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
h₁ : Λ'.move p✝ k₁✝ k₂✝ q ∈ S
h₂ : trStmts₁ q ⊆ S
⊢ Supports (insert (Λ'.move p✝ k₁✝ k₂✝ q) (trStmts₁ q)) S

Tactic:
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
h₁ : Λ'.clear p✝ k✝ q ∈ S
h₂ : trStmts₁ q ⊆ S
⊢ Supports (insert (Λ'.clear p✝ k✝ q) (trStmts₁ q)) S

Tactic:
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
h₁ : q.copy ∈ S
h₂ : trStmts₁ q ⊆ S
⊢ Supports (insert q.copy (trStmts₁ q)) S

Tactic:
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
h₁ : Λ'.push k✝ s✝ q ∈ S
h₂ : trStmts₁ q ⊆ S
⊢ Supports (insert (Λ'.push k✝ s✝ q) (trStmts₁ q)) S

Tactic:
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
h₁ : Λ'.read q ∈ S
h₂ : (Finset.univ.biUnion fun s ↦ trStmts₁ (q s)) ⊆ S
⊢ Supports (insert (Λ'.read q) (Finset.univ.biUnion fun s ↦ trStmts₁ (q s))) S

Tactic:
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
h₁ : q.succ ∈ S
h₂ : insert (unrev q) (trStmts₁ q) ⊆ S
⊢ Supports (insert q.succ (insert (unrev q) (trStmts₁ q))) S

Tactic:
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
h₁ : q₁.pred q₂ ∈ S
h₂ : insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂) ⊆ S
⊢ Supports (insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂))) S

Tactic:
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.Topology.Category.Profinite.Extend

Goal state before:
pp: case right
I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
e : I ≌ ULiftHom (ULift.{w, u} I) := ULiftHomULiftCategory.equiv I
left✝¹ : Discrete PUnit.{1}
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
i : I
left✝ : ((e.inverse ⋙ functor c).obj { down := i }).left ⟶ { left := left✝¹, right := X, hom := f }.left
s : F.obj i ⟶ X
w : f = c.π.app i ≫ toProfinite.map s
⊢ ∀ (s' : (e.inverse ⋙ functor c).obj { down := i } ⟶ { left := left✝¹, right := X, hom := f }),
    ∃ c' t, (e.inverse ⋙ functor c).map t ≫ { left := left✝, right := s, w := w } = (e.inverse ⋙ functor c).map t ≫ s'

Tactic:
⟨_, (s' : F.obj i ⟶ X), (w' : f = c.π.app i ≫ _)⟩

Goal state after:
case right
I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
e : I ≌ ULiftHom (ULift.{w, u} I) := ULiftHomULiftCategory.equiv I
left✝² : Discrete PUnit.{1}
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
i : I
left✝¹ : ((e.inverse ⋙ functor c).obj { down := i }).left ⟶ { left := left✝², right := X, hom := f }.left
s : F.obj i ⟶ X
w : f = c.π.app i ≫ toProfinite.map s
left✝ : ((e.inverse ⋙ functor c).obj { down := i }).left ⟶ { left := left✝², right := X, hom := f }.left
s' : F.obj i ⟶ X
w' : f = c.π.app i ≫ toProfinite.map s'
⊢ ∃ c' t,
    (e.inverse ⋙ functor c).map t ≫ { left := left✝¹, right := s, w := w } =
      (e.inverse ⋙ functor c).map t ≫ { left := left✝, right := s', w := w' }
Module: Mathlib.Condensed.Discrete.Module

Goal state before:
pp: P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
M : ModuleCat R
this✝ : (constantSheaf (coherentTopology CompHaus) (Type (u + 1))).Faithful
this : (constantSheaf (coherentTopology CompHaus) (Type (u + 1))).Full
⊢ (discrete (Type (u + 1))).essImage
    ((sheafCompose (coherentTopology CompHaus) (CategoryTheory.forget (ModuleCat R))).obj ((functor R).obj M))

Tactic:
rw [essImage_eq_of_natIso CondensedSet.LocallyConstant.iso.symm]

Goal state after:
P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
M : ModuleCat R
this✝ : (constantSheaf (coherentTopology CompHaus) (Type (u + 1))).Faithful
this : (constantSheaf (coherentTopology CompHaus) (Type (u + 1))).Full
⊢ CondensedSet.LocallyConstant.functor.essImage
    ((sheafCompose (coherentTopology CompHaus) (CategoryTheory.forget (ModuleCat R))).obj ((functor R).obj M))
Module: Mathlib.Condensed.Discrete.Module

Goal state before:
pp: P : TopCat → Prop
R : Type u
inst✝ : Ring R
M : ModuleCat R
this✝ : (constantSheaf (coherentTopology LightProfinite) (Type u)).Faithful
this : (constantSheaf (coherentTopology LightProfinite) (Type u)).Full
⊢ (discrete (Type u)).essImage
    ((sheafCompose (coherentTopology LightProfinite) (CategoryTheory.forget (ModuleCat R))).obj ((functor R).obj M))

Tactic:
rw [essImage_eq_of_natIso LightCondSet.LocallyConstant.iso.symm]

Goal state after:
P : TopCat → Prop
R : Type u
inst✝ : Ring R
M : ModuleCat R
this✝ : (constantSheaf (coherentTopology LightProfinite) (Type u)).Faithful
this : (constantSheaf (coherentTopology LightProfinite) (Type u)).Full
⊢ LightCondSet.LocallyConstant.functor.essImage
    ((sheafCompose (coherentTopology LightProfinite) (CategoryTheory.forget (ModuleCat R))).obj ((functor R).obj M))
Module: Mathlib.Control.EquivFunctor.Instances

Goal state before:
pp: α : Type ?u.4
⊢ (fun x ↦ Fintype.ofBijective ⇑(Equiv.refl α) ⋯) = id

Tactic:
by ext; simp [eq_iff_true_of_subsingleton]

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b : β x
hb : b ∈ approx (⇑f) i x
b' : β x
h' : b' ∈ Part.fix (⇑f) x
hb' : b ∈ Part.fix (⇑f) x
⊢ b' ∈ approx (⇑f) i x

Tactic:
obtain rfl := Part.mem_unique h' hb'

Goal state after:
case pos
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b' : β x
h' : b' ∈ Part.fix (⇑f) x
hb : b' ∈ approx (⇑f) i x
hb' : b' ∈ Part.fix (⇑f) x
⊢ b' ∈ approx (⇑f) i x
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
ρ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ReaderT ρ m α✝
⊢ (callCC fun x ↦ dummy✝) = dummy✝

Tactic:
simp only [callCC, ReaderT.callCC, @callCC_dummy m _]

Goal state after:
m : Type u → Type v
ρ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ReaderT ρ m α✝
⊢ (ReaderT.mk fun r ↦ dummy✝.run r) = dummy✝
Module: Mathlib.Data.TypeVec

Goal state before:
pp: α : TypeVec.{u} 0
ps : α ⟹ «repeat» 0 Prop
⊢ ∀ (x : Fin2 0), subtypeVal ps x = nilFun x

Tactic:
by rintro ⟨⟩

Goal state after:
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
f : Filter α
F : f.Realizer
a : Set α
⊢ a ∈ f ↔ ∃ b, F.F.f b ⊆ a

Tactic:
by
  cases F; subst f; rfl

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

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
P : (Fin n → α) → Prop
hf : P f
h :
  ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n),
    i < j → (f ∘ ⇑σ) j < (f ∘ ⇑σ) i → P (f ∘ ⇑σ) → P (f ∘ ⇑σ ∘ ⇑(Equiv.swap i j))
this : Preorder (Equiv.Perm (Fin n)) := Preorder.lift fun σ ↦ toLex (f ∘ ⇑σ)
σ : Fin n ≃ Fin n
hσ : f ∘ ⇑σ ≠ f ∘ ⇑(sort f)
hfσ : P (f ∘ ⇑σ)
⊢ ∃ c < σ, P (f ∘ ⇑c)

Tactic:
obtain ⟨i, j, hij₁, hij₂⟩ := antitone_pair_of_not_sorted' hσ

Goal state after:
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
P : (Fin n → α) → Prop
hf : P f
h :
  ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n),
    i < j → (f ∘ ⇑σ) j < (f ∘ ⇑σ) i → P (f ∘ ⇑σ) → P (f ∘ ⇑σ ∘ ⇑(Equiv.swap i j))
this : Preorder (Equiv.Perm (Fin n)) := Preorder.lift fun σ ↦ toLex (f ∘ ⇑σ)
σ : Fin n ≃ Fin n
hσ : f ∘ ⇑σ ≠ f ∘ ⇑(sort f)
hfσ : P (f ∘ ⇑σ)
i j : Fin n
hij₁ : i < j
hij₂ : (f ∘ ⇑σ) j < (f ∘ ⇑σ) i
⊢ ∃ c < σ, P (f ∘ ⇑c)
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
inst✝ : FinEnum α
⊢ (toList α).Nodup

Tactic:
by
  simp only [toList]; apply List.Nodup.map <;> [apply Equiv.injective; apply List.nodup_finRange]

Goal state after:
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: α : Type u_1
f g : α → Option α
a : α
l : List α
H : ∀ (a_1 : α), a_1 ∈ a :: l → f a_1 = g a_1
⊢ lookmap f (a :: l) = lookmap g (a :: l)

Tactic:
by
    obtain ⟨H₁, H₂⟩ := forall_mem_cons.1 H
    rcases h : g a with - | b
    · simp [h, H₁.trans h, lookmap_congr H₂]
    · simp [lookmap_cons_some _ _ h, lookmap_cons_some _ _ (H₁.trans h)]

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ tl.keys → ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a ∈ tl.keys
b : β a
tl₁ tl₂ : List (Sigma β)
h₁ : ¬a ∈ tl₁.keys
h₂ : tl = tl₁ ++ ⟨a, b⟩ :: tl₂
h₃ : kerase a tl = tl₁ ++ tl₂
⊢ kerase a (hd :: tl) = hd :: tl₁ ++ tl₂

Tactic:
simp [e, h₃]

Goal state after: