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

Goal state before:
pp: case cons
α : Type u
σ : Type v
M : NFA α σ
x : α
xs : List α
ih :
  ∀ {S S' : Set σ},
    Disjoint S (List.foldl M.reverse.stepSet S' xs) → Disjoint S' (List.foldr (fun x y ↦ M.stepSet y x) S xs)
S S' : Set σ
h : Disjoint S (List.foldl M.reverse.stepSet (M.reverse.stepSet S' x) xs)
⊢ Disjoint S' (M.stepSet (List.foldr (fun x y ↦ M.stepSet y x) S xs) x)

Tactic:
← NFA.disjoint_stepSet_reverse,

Goal state after:
case cons
α : Type u
σ : Type v
M : NFA α σ
x : α
xs : List α
ih :
  ∀ {S S' : Set σ},
    Disjoint S (List.foldl M.reverse.stepSet S' xs) → Disjoint S' (List.foldr (fun x y ↦ M.stepSet y x) S xs)
S S' : Set σ
h : Disjoint S (List.foldl M.reverse.stepSet (M.reverse.stepSet S' x) xs)
⊢ Disjoint (List.foldr (fun x y ↦ M.stepSet y x) S xs) (M.reverse.stepSet S' x)
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
l₃ : ListBlank Γ
⊢ append (l₁ ++ l₂) l₃ = append l₁ (append l₂ l₃)

Tactic:
refine l₃.induction_on fun l ↦ ?_
  simp only [ListBlank.append_mk, List.append_assoc]

Goal state after:
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α →. σ
O : Set (ℕ →. ℕ)
hO : ∀ g ∈ O, Partrec g
hf : RecursiveIn O f
⊢ ∀ g ∈ O, Nat.Partrec g

Tactic:
by simpa only [Partrec.nat_iff] using hO

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

Goal state before:
pp: case none
Γ : Type u_1
inst✝³ : Inhabited Γ
Γ' : Type u_2
inst✝² : Inhabited Γ'
Λ : Type u_3
inst✝¹ : Inhabited Λ
Λ' : Type u_4
inst✝ : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
c : Cfg Γ Λ
a₂✝ : Cfg Γ' Λ'
cs : c.q ∈ S
e : step M c = none
⊢ match none with
  | some b₁ =>
    ∃ b₂,
      (fun a b ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧ Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) (Cfg.map f₁ g₁.f c) b₂
  | none => step (M.map f₁ f₂ g₁.f g₂) (Cfg.map f₁ g₁.f c) = none

pp: case some
Γ : Type u_1
inst✝³ : Inhabited Γ
Γ' : Type u_2
inst✝² : Inhabited Γ'
Λ : Type u_3
inst✝¹ : Inhabited Λ
Λ' : Type u_4
inst✝ : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
c : Cfg Γ Λ
a₂✝ : Cfg Γ' Λ'
cs : c.q ∈ S
val✝ : Cfg Γ Λ
e : step M c = some val✝
⊢ match some val✝ with
  | some b₁ =>
    ∃ b₂,
      (fun a b ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧ Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) (Cfg.map f₁ g₁.f c) b₂
  | none => step (M.map f₁ f₂ g₁.f g₂) (Cfg.map f₁ g₁.f c) = none

Tactic:
· rw [← M.map_step f₁ f₂ g₁ g₂ f₂₁ g₂₁ _ cs, e]
    rfl

Goal state after:
case some
Γ : Type u_1
inst✝³ : Inhabited Γ
Γ' : Type u_2
inst✝² : Inhabited Γ'
Λ : Type u_3
inst✝¹ : Inhabited Λ
Λ' : Type u_4
inst✝ : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
c : Cfg Γ Λ
a₂✝ : Cfg Γ' Λ'
cs : c.q ∈ S
val✝ : Cfg Γ Λ
e : step M c = some val✝
⊢ match some val✝ with
  | some b₁ =>
    ∃ b₂,
      (fun a b ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧ Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) (Cfg.map f₁ g₁.f c) b₂
  | none => step (M.map f₁ f₂ g₁.f g₂) (Cfg.map f₁ g₁.f c) = none
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt Γ Λ σ
⊢ q₁ ∈ stmts₁ q₂ → stmts₁ q₁ ⊆ stmts₁ q₂

Tactic:
classical
  intro h₁₂ q₀ h₀₁
  induction q₂ with (
    simp only [stmts₁] at h₁₂ ⊢
    simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h₁₂)
  | branch p q₁ q₂ IH₁ IH₂ =>
    rcases h₁₂ with (rfl | h₁₂ | h₁₂)
    · unfold stmts₁ at h₀₁
      exact h₀₁
    · grind
    · grind
  | goto l => subst h₁₂; exact h₀₁
  | halt => subst h₁₂; exact h₀₁
  | _ _ q IH =>
    rcases h₁₂ with rfl | h₁₂
    · exact h₀₁
    · grind

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

Goal state before:
pp: m : Num
n : ℕ
⊢ ↑(m <<< n) = ↑m <<< n

Tactic:
cases m <;> dsimp only [← shiftl_eq_shiftLeft, shiftl]
  · symm
    apply Nat.zero_shiftLeft
  simp only [cast_pos]
  induction n with
  | zero => rfl
  | succ n IH =>
    simp [PosNum.shiftl_succ_eq_bit0_shiftl, Nat.shiftLeft_succ, IH, mul_comm,
      -shiftl_eq_shiftLeft, -PosNum.shiftl_eq_shiftLeft, mul_two]

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

Goal state before:
pp: case prim.prec.succ.zero
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))
a : ℕ
e : a + 0 = 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 :: 0 :: Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail)

Tactic:
refine PFun.mem_fix_iff.2 (Or.inl <| Part.eq_some_iff.1 ?_)
        simp only [hg, ← e, Part.bind_some, List.tail_cons, pure]
        rfl

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

Goal state before:
pp: case pos.hn
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h : i = tl.length
⊢ (List.map some tl).reverse.length ≤ tl.length

Tactic:
List.length_reverse,

Goal state after:
case pos.hn
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h : i = tl.length
⊢ (List.map some tl).length ≤ tl.length
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case cons
k' : Cont
c c' : Code
ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k'
k : Cont
v : List ℕ
⊢ stepNormal c (Cont.cons₁ c' v (k.then k')) v = (stepNormal c (Cont.cons₁ c' v k) v).then k'

Tactic:
| cons c c' ih _ =>

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

Goal state before:
pp: X : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
Z U : Set X
hZ : IsClosed[inst✝³] Z
hU : IsOpen[inst✝³] U
hZU : Z ⊆ U
V : ↑Z → Set X
hV : ∀ (z : ↑Z), IsClopen (V z) ∧ ↑z ∈ V z ∧ V z ⊆ U
V_cover : Z ⊆ ⋃ z, V z
⊢ ∃ C, IsClopen C ∧ Z ⊆ C ∧ C ⊆ U

Tactic:
choose I hI using hZ.isCompact.elim_finite_subcover V (fun z ↦ (hV z).1.isOpen) V_cover

Goal state after:
X : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
Z U : Set X
hZ : IsClosed[inst✝³] Z
hU : IsOpen[inst✝³] U
hZU : Z ⊆ U
V : ↑Z → Set X
hV : ∀ (z : ↑Z), IsClopen (V z) ∧ ↑z ∈ V z ∧ V z ⊆ U
V_cover : Z ⊆ ⋃ z, V z
I : Finset ↑Z
hI : Z ⊆ ⋃ i ∈ I, V i
⊢ ∃ C, IsClopen C ∧ Z ⊆ C ∧ C ⊆ U
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
l' : Λ' K Γ Λ σ
h : l' ∈ trSupp M S
⊢ ∀ (q : TM2.Stmt Γ Λ σ),
    TM2.SupportsStmt S q →
      (∀ x ∈ trStmts₁ q, x ∈ trSupp M S) →
        TM1.SupportsStmt (trSupp M S) (trNormal q) ∧ ∀ l' ∈ trStmts₁ q, TM1.SupportsStmt (trSupp M S) (tr M l')

Tactic:
clear h l'

Goal state after:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
⊢ ∀ (q : TM2.Stmt Γ Λ σ),
    TM2.SupportsStmt S q →
      (∀ x ∈ trStmts₁ q, x ∈ trSupp M S) →
        TM1.SupportsStmt (trSupp M S) (trNormal q) ∧ ∀ l' ∈ trStmts₁ q, TM1.SupportsStmt (trSupp M S) (tr M l')
Module: Mathlib.Topology.ExtremallyDisconnected

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

Tactic:
let s : Z → Y := fun z => Classical.choose <| g_sur z

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

Goal state before:
pp: X : CompHaus
inst✝ : Projective X
⊢ ExtremallyDisconnected ↑X.toTop

Tactic:
apply CompactT2.Projective.extremallyDisconnected
  intro A B _ _ _ _ _ _ f g hf hg hsurj
  let A' : CompHaus := CompHaus.of A
  let B' : CompHaus := CompHaus.of B
  let f' : X ⟶ B' := CompHausLike.ofHom _ ⟨f, hf⟩
  let g' : A' ⟶ B' := CompHausLike.ofHom _ ⟨g,hg⟩
  have : Epi g' := by
    rw [CompHaus.epi_iff_surjective]
    assumption
  obtain ⟨h, hh⟩ := Projective.factors f' g'
  refine ⟨h, h.hom.hom.2, ?_⟩
  ext t
  apply_fun (fun e => e t) at hh
  exact hh

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

Goal state before:
pp: X : Stonean
B C : CompHaus
φ : toCompHaus.obj X ⟶ C
f : B ⟶ C
inst✝ : Epi f
this : ExtremallyDisconnected ↑(toCompHaus.obj X).toTop
⊢ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
rwa [← CompHaus.epi_iff_surjective]

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : CompactSpace X
this : CompactSpace (Quotient S.toSetoid)
⊢ Finite (Quotient S.toSetoid)

Tactic:
← isCompact_univ_iff,

Goal state after:
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : CompactSpace X
this : IsCompact univ
⊢ Finite (Quotient S.toSetoid)
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
d : DiscreteQuotient X
x✝¹ : Set X
x✝ : ∃ y, x✝¹ = {x | d.toSetoid x y}
y : X
h : x✝¹ = {x | d.toSetoid x y}
⊢ d.proj ⁻¹' {d.proj y} = x✝¹

Tactic:
by ext; simp [h, proj, Quotient.eq]

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

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

Tactic:
change SecondCountableTopology ({ u : ∀ j : J, F.obj j | _ } : Type _)
          apply IsInducing.subtypeVal.secondCountableTopology

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

Goal state before:
pp: 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)
⊢ (functor c).Initial

Tactic:
let e : I ≌ ULiftHom.{w} (ULift.{w} I) := ULiftHomULiftCategory.equiv _
  suffices (e.inverse ⋙ functor c).Initial from initial_of_equivalence_comp e.inverse (functor c)
  rw [initial_iff_of_isCofiltered (F := e.inverse ⋙ functor c)]
  constructor
  · intro ⟨_, X, (f : c.pt ⟶ _)⟩
    obtain ⟨i, g, h⟩ := exists_hom c hc f
    exact ⟨⟨i⟩, ⟨StructuredArrow.homMk g h.symm⟩⟩
  · intro ⟨_, X, (f : c.pt ⟶ _)⟩ ⟨i⟩ ⟨_, (s : F.obj i ⟶ X), (w : f = c.π.app i ≫ _)⟩
      ⟨_, (s' : F.obj i ⟶ X), (w' : f = c.π.app i ≫ _)⟩
    simp only [StructuredArrow.hom_eq_iff,
      StructuredArrow.comp_right]
    refine ⟨⟨i⟩, 𝟙 _, ?_⟩
    simp only [CategoryTheory.Functor.map_id]
    rw [w] at w'
    exact toProfinite.map_injective <| Epi.left_cancellation _ _ w'

Goal state after:
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)
⊢ (isoLocallyConstantOfIsColimit X hX).inv = counitApp X

Tactic:
dsimp [isoLocallyConstantOfIsColimit]
  simp only [Category.assoc]
  rw [Iso.inv_comp_eq]
  ext S : 2
  apply colimit.hom_ext
  intro ⟨Y, _, g⟩
  suffices _ ≫ (isoFinYonedaComponents _ _).inv ≫ X.map g =
    (locallyConstantPresheaf _).map g ≫ counitAppApp (Opposite.unop S) X by
      simpa [locallyConstantIsoFinYoneda, isoFinYoneda, counitApp]
  erw [(counitApp.{u, u + 1} X).naturality]
  simp only [← Category.assoc, op_obj, functorToPresheaves_obj_obj]
  congr
  ext f
  simp only [toProfinite_obj, TypeCat.Fun.toFun_apply, CategoryTheory.comp_apply,
    ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk, counitApp_app]
  apply presheaf_ext.{u, u + 1} (X := X) (Y := X) (f := f)
  intro x
  dsimp [toProfinite_obj]
  rw [incl_of_counitAppApp.{u, u + 1}]
  simp only [counitAppAppImage]
  have : Finite (fiber.{u, u + 1} f x) :=
    Finite.of_injective (sigmaIncl.{u, u + 1} f x).1 Subtype.val_injective
  apply injective_of_mono (isoFinYonedaComponents X (fiber.{u, u + 1} f x)).hom
  ext y
  simp only [toProfinite_obj, isoFinYonedaComponents_hom, ConcreteCategory.hom_ofHom,
    TypeCat.Fun.coe_mk, ← Functor.map_comp_apply, ← op_comp]
  rw [show (Profinite.of PUnit.{u + 1}).const y ≫
    IsTerminal.from _ (fiber.{u, u + 1} f x) = 𝟙 _ from rfl]
  simp only [op_comp, Functor.map_comp_apply, op_id, Functor.map_id_apply]
  simpa [← dsimp% isoFinYonedaComponents_inv_comp X _ (sigmaIncl.{u, u + 1} f x),
    ← isoFinYonedaComponents_hom_apply, -isoFinYonedaComponents_hom] using! x.map_eq_image f y

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

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
P A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : P ⊗ (free R).obj S.toCondensed ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj S'.toCondensed ⊗ P ⟶ A
hh : (lightProfiniteToLightCondSet ⋙ free R).map π ▷ P ≫ (β_ P ((free R).obj S.toCondensed)).inv ≫ g = g' ≫ e
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ g = g' ≫ e

Tactic:
refine ⟨S', π, hπ, (β_ _ _).hom ≫ g', ?_⟩

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
P A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : P ⊗ (free R).obj S.toCondensed ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj S'.toCondensed ⊗ P ⟶ A
hh : (lightProfiniteToLightCondSet ⋙ free R).map π ▷ P ≫ (β_ P ((free R).obj S.toCondensed)).inv ≫ g = g' ≫ e
⊢ P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ g = ((β_ P ((free R).obj S'.toCondensed)).hom ≫ g') ≫ e
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
inst✝ : Monad m
α β ε : Type u
x : Label (Except ε α) m β
i : α
⊢ goto (mkLabel x) i = mk (Except.ok <$> goto x (Except.ok i))

Tactic:
by
  cases x; rfl

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: β : Type u_1
γ : Type u_2
x : γ
n : ℕ
α : TypeVec.{u_1} n
⊢ TypeVec.const x (α ::: β) = (TypeVec.const x α ::: fun x_1 ↦ x)

Tactic:
ext i : 1

Goal state after:
β : Type u_1
γ : Type u_2
x : γ
n : ℕ
α : TypeVec.{u_1} n
i : Fin2 (n + 1)
⊢ TypeVec.const x (α ::: β) i = (TypeVec.const x α ::: fun x_1 ↦ x) i
Module: Mathlib.Data.TypeVec

Goal state before:
pp: β : Type u_1
x : β
α : TypeVec.{u_2} 0
⊢ TypeVec.const x α = nilFun

Tactic:
ext i : 1

Goal state after:
β : Type u_1
x : β
α : TypeVec.{u_2} 0
i : Fin2 0
⊢ TypeVec.const x α i = nilFun i
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ (dlookup a l).isSome = true ↔ a ∈ l.keys

Tactic:
by
  induction l with
  | nil => simp
  | cons s _ _ => by_cases a = s.fst <;> grind

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

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : Option.map (Sigma.mk a) (dlookup a tail✝) = find? (fun s ↦ decide (a = s.fst)) tail✝
⊢ Option.map (Sigma.mk a) (dlookup a (s :: tail✝)) = find? (fun s ↦ decide (a = s.fst)) (s :: tail✝)

Tactic:
by_cases s.fst = a

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : Option.map (Sigma.mk a) (dlookup a tail✝) = find? (fun s ↦ decide (a = s.fst)) tail✝
h✝ : s.fst = a
⊢ Option.map (Sigma.mk a) (dlookup a (s :: tail✝)) = find? (fun s ↦ decide (a = s.fst)) (s :: tail✝)

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : Option.map (Sigma.mk a) (dlookup a tail✝) = find? (fun s ↦ decide (a = s.fst)) tail✝
h✝ : ¬s.fst = a
⊢ Option.map (Sigma.mk a) (dlookup a (s :: tail✝)) = find? (fun s ↦ decide (a = s.fst)) (s :: tail✝)
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
hs : s.Nonempty
f : β✝ → β✝
hf : ∃ a ∈ s, const α✝ id a = f
b : β✝
hb : b ∈ t
⊢ f b ∈ t

Tactic:
obtain ⟨_, _, rfl⟩ := hf

Goal state after:
case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
hs : s.Nonempty
b : β✝
hb : b ∈ t
w✝ : α✝
left✝ : w✝ ∈ s
⊢ const α✝ id w✝ b ∈ t
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
h₁ : a = ah
h₂ : a' = ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)

pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
h₁ : a = ah
h₂ : ¬a' = ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)

pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
h₁ : ¬a = ah
h₂ : a' = ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)

pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
h₁ : ¬a = ah
h₂ : ¬a' = ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)

Tactic:
· subst h₁ h₂
      cases Ne.irrefl h

Goal state after:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
h₁ : a = ah
h₂ : ¬a' = ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)

case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
h₁ : ¬a = ah
h₂ : a' = ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
h₁ : ¬a = ah
h₂ : ¬a' = ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
⊢ a ∈ (kinsert a' b' l).keys ↔ a = a' ∨ a ∈ l.keys

Tactic:
by by_cases h : a = a' <;> simp [h]

Goal state after:
Module: Mathlib.Data.Finsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f g : α →₀ N
⊢ (f + g).neLocus f = g.support

Tactic:
rw [neLocus_comm, neLocus_self_add_right]

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

Goal state before:
pp: case pos
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : AddMonoid M
k : κ
f g : ι k →₀ M
k' : κ
i : ι k'
hk : k' = k
⊢ (f + g).embSigma ⟨k', i⟩ = (f.embSigma + g.embSigma) ⟨k', i⟩

pp: case neg
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : AddMonoid M
k : κ
f g : ι k →₀ M
k' : κ
i : ι k'
hk : ¬k' = k
⊢ (f + g).embSigma ⟨k', i⟩ = (f.embSigma + g.embSigma) ⟨k', i⟩

Tactic:
· subst hk
    simp

Goal state after:
case neg
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : AddMonoid M
k : κ
f g : ι k →₀ M
k' : κ
i : ι k'
hk : ¬k' = k
⊢ (f + g).embSigma ⟨k', i⟩ = (f.embSigma + g.embSigma) ⟨k', i⟩
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
hx : x ∈ takeWhile p l
⊢ p x = true

Tactic:
by
  induction l with simp [takeWhile] at hx
  | cons hd tl IH =>
    cases hp : p hd
    · simp [hp] at hx
    · rw [hp, mem_cons] at hx
      rcases hx with (rfl | hx)
      · exact hp
      · exact IH hx

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

Goal state before:
pp: α : Type u_1
p : ℕ
w : List α
lhs : ∀ i < w.length - p, w[i]? = w[i + p]?
i : ℕ
leni : i < w.length - p
⊢ w[i]? = some w[p + i]

Tactic:
have len : i + p < w.length := by lia

Goal state after:
α : Type u_1
p : ℕ
w : List α
lhs : ∀ i < w.length - p, w[i]? = w[i + p]?
i : ℕ
leni : i < w.length - p
len : i + p < w.length
⊢ w[i]? = some w[p + i]
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
a : α
l : List α
hn : a :: l ≠ []
h : IsChain (fun x y ↦ r x y = true) (a :: l)
⊢ splitBy.loop r l a [] [] = [a :: l]

Tactic:
← append_nil l,

Goal state after:
case cons
α : Type u_1
r : α → α → Bool
a : α
l : List α
hn : a :: l ≠ []
h : IsChain (fun x y ↦ r x y = true) (a :: l)
⊢ splitBy.loop r (l ++ []) a [] [] = [a :: (l ++ [])]
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case inr.inr.refine_1
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
⊢ ∀ (m_1 : List α), m_1 ∈ splitBy r l ++ splitBy r m → IsChain (fun x y ↦ r x y = true) m_1

pp: case inr.inr.refine_2
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
⊢ IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy r l ++ splitBy r m)

Tactic:
· aesop (add apply unsafe isChain_of_mem_splitBy)

Goal state after:
case inr.inr.refine_2
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
⊢ IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy r l ++ splitBy r m)