mathlib-initiative/mathlib-tactics huggingface dataset:
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 = ∅
⊢ ρ '' G ⊆ closure (ρ '' Gᶜ)ᶜ

Tactic:
intro a 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.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons
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 Γ'
e : splitAtPred p (S k) = (a :: 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₂ }

Tactic:
| cons a L₁ IH =>

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

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

Tactic:
rcases n with - | n

Goal state after:
case cons.zero
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 ℕ
⊢ if (0 :: tail✝).headI = 0 then
    natEnd ((trList (0 :: tail✝)).head?.getD default) = true ∧ (trList (0 :: tail✝)).tail = trList (0 :: tail✝).tail
  else
    natEnd ((trList (0 :: tail✝)).head?.getD default) = false ∧
      (trList (0 :: tail✝)).tail = (trNat (0 :: tail✝).headI).tail ++ Γ'.cons :: trList (0 :: tail✝).tail

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
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case fix
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a✝¹ : Code
a✝ : Cont'
H₁ : contSupp (Cont'.fix a✝¹ a✝) ⊆ S
⊢ TM2.SupportsStmt S (tr (Λ'.ret (Cont'.fix a✝¹ a✝)))

Tactic:
| fix =>

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

Goal state before:
pp: S : LightProfinite
x✝ : ℕᵒᵖ
⊢ S.asLimitConeAux.π.app x✝ =
    (lightToProfiniteFullyFaithful.preimageIso ((Cone.forget (S.diagram ⋙ lightToProfinite)).mapIso S.isoMapCone)).hom ≫
      S.asLimitCone.π.app x✝

Tactic:
by rw [← @Iso.inv_comp_eq]; rfl

Goal state after:
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✝
inst✝¹ : HasExplicitFiniteCoproducts P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝ : PreservesFiniteProducts Y
S T : (CompHausLike P)ᵒᵖ
g : S ⟶ T
f : (functorToPresheaves.obj (Y.obj (op (of P PUnit.{u + 1})))).obj S
a : Fiber ⇑(comap (TopCat.Hom.hom g.unop.hom) f)
⊢ (ConcreteCategory.hom (Y.map (sigmaIncl (comap (TopCat.Hom.hom g.unop.hom) f) a).op))
      ((ConcreteCategory.hom
            ((functorToPresheaves.obj (Y.obj (op (of P PUnit.{u + 1})))).map g ≫
              match T with
              | op S => counitAppApp S Y)).toFun
        f) =
    (ConcreteCategory.hom (Y.map (sigmaIncl (comap (TopCat.Hom.hom g.unop.hom) f) a).op))
      ((ConcreteCategory.hom
            ((match S with
              | op S => counitAppApp S Y) ≫
              Y.map g)).toFun
        f)

Tactic:
simp only [op_unop, functorToPresheaves_obj_obj, functorToPresheaves_obj_map,
      TypeCat.Fun.toFun_apply, CategoryTheory.comp_apply, ConcreteCategory.hom_ofHom,
      TypeCat.Fun.coe_mk]

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✝
inst✝¹ : HasExplicitFiniteCoproducts P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝ : PreservesFiniteProducts Y
S T : (CompHausLike P)ᵒᵖ
g : S ⟶ T
f : (functorToPresheaves.obj (Y.obj (op (of P PUnit.{u + 1})))).obj S
a : Fiber ⇑(comap (TopCat.Hom.hom g.unop.hom) f)
⊢ (ConcreteCategory.hom (Y.map (sigmaIncl (comap (TopCat.Hom.hom g.unop.hom) f) a).op))
      ((ConcreteCategory.hom (counitAppApp (unop T) Y)) (comap (TopCat.Hom.hom g.unop.hom) f)) =
    (ConcreteCategory.hom (Y.map (sigmaIncl (comap (TopCat.Hom.hom g.unop.hom) f) a).op))
      ((ConcreteCategory.hom (Y.map g)) ((ConcreteCategory.hom (counitAppApp (unop S) Y)) f))
Module: Mathlib.Condensed.Discrete.LocallyConstant

Goal state before:
pp: P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
inst✝³ : HasProp P PUnit.{u + 1}
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Type (max u w)
S : CompHausLike P
f : LocallyConstant (↑S.toTop) X
this : Preregular (CompHausLike P)
a : Fiber ⇑(map (⇑(ConcreteCategory.hom ((unit P hs).app X))) f)
⊢ (ConcreteCategory.hom
        (((functor P hs).obj X).obj.map (sigmaIncl (map (⇑(ConcreteCategory.hom ((unit P hs).app X))) f) a).op))
      ((ConcreteCategory.hom ((ObjectProperty.homMk (counitApp ((functor P hs).obj X).obj)).hom.app (op S)))
        (map (fun x ↦ LocallyConstant.const PUnit.{u + 1} x) f)) =
    (ConcreteCategory.hom
        (((functor P hs).obj X).obj.map (sigmaIncl (map (⇑(ConcreteCategory.hom ((unit P hs).app X))) f) a).op))
      f

Tactic:
erw [incl_of_counitAppApp]

Goal state after:
P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
inst✝³ : HasProp P PUnit.{u + 1}
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Type (max u w)
S : CompHausLike P
f : LocallyConstant (↑S.toTop) X
this : Preregular (CompHausLike P)
a : Fiber ⇑(map (⇑(ConcreteCategory.hom ((unit P hs).app X))) f)
⊢ counitAppAppImage (map (⇑(ConcreteCategory.hom ((unit P hs).app X))) f) a =
    (ConcreteCategory.hom
        (((functor P hs).obj X).obj.map (sigmaIncl (map (⇑(ConcreteCategory.hom ((unit P hs).app X))) f) a).op))
      f
Module: Mathlib.Condensed.Discrete.Characterization

Goal state before:
pp: X : LightCondSet
⊢ [LightCondensed.IsDiscrete X, IsIso ((LightCondensed.discreteUnderlyingAdj (Type u)).counit.app X),
      (LightCondensed.discrete (Type u)).essImage X, functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      ∀ (S : LightProfinite), Nonempty (IsColimit (X.obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))].TFAE

Tactic:
tfae_have 1 ↔ 2 := Sheaf.isConstant_iff_isIso_counit_app _ _ _
  tfae_have 1 ↔ 3 := ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩
  tfae_have 1 ↔ 4 := Sheaf.isConstant_iff_mem_essImage _ LightProfinite.isTerminalPUnit adjunction X
  tfae_have 1 ↔ 5 :=
    have : functor.Faithful := inferInstance
    have : functor.Full := inferInstance
    -- These `have` statements above shouldn't be needed, but they are.
    Sheaf.isConstant_iff_isIso_counit_app' _ LightProfinite.isTerminalPUnit adjunction X
  tfae_have 6 → 4 := fun h ↦
    mem_locallyConstant_essImage_of_isColimit_mapCocone X (fun S ↦ (h S).some)
  tfae_have 4 → 6 := fun ⟨Y, ⟨i⟩⟩ S ↦
    ⟨IsColimit.mapCoconeEquiv ((sheafToPresheaf _ _).mapIso i)
      (LightCondensed.isColimitLocallyConstantPresheafDiagram Y S)⟩
  tfae_finish

Goal state after:
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 : Sheaf (coherentTopology (CompHausLike P)) (Type (max u w))
x : X.obj.obj (op (of P PUnit.{u + 1}))
this✝ : Preregular (CompHausLike P)
this : PreservesFiniteProducts ((sheafToPresheaf (coherentTopology (CompHausLike P)) (Type (max u w))).obj X) :=
  @CompHausLike.LocallyConstant.adjunction._proof_2 P inst✝² inst✝¹ hs X this✝
a : Fiber ⇑((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x)
⊢ (ConcreteCategory.hom
        (X.obj.map (sigmaIncl ((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x) a).op))
      ((ConcreteCategory.hom (((counit P hs).app X).hom.app (op (of P PUnit.{u + 1}))))
        ((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x)) =
    (ConcreteCategory.hom
        (X.obj.map (sigmaIncl ((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x) a).op))
      x

Tactic:
erw [incl_of_counitAppApp]

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 : Sheaf (coherentTopology (CompHausLike P)) (Type (max u w))
x : X.obj.obj (op (of P PUnit.{u + 1}))
this✝ : Preregular (CompHausLike P)
this : PreservesFiniteProducts ((sheafToPresheaf (coherentTopology (CompHausLike P)) (Type (max u w))).obj X) :=
  @CompHausLike.LocallyConstant.adjunction._proof_2 P inst✝² inst✝¹ hs X this✝
a : Fiber ⇑((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x)
⊢ counitAppAppImage ((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x) a =
    (ConcreteCategory.hom
        (X.obj.map (sigmaIncl ((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x) a).op))
      x
Module: Mathlib.Condensed.Light.Epi

Goal state before:
pp: R : Type u
inst✝ : Ring R
X Y : LightCondMod R
f✝ : X ⟶ Y
X✝ Y✝ : LightCondMod R
f : X✝ ⟶ Y✝
hf : IsLocallySurjective f
⊢ IsLocallySurjective ((LightCondensed.forget R).map f)

Tactic:
exact (Presheaf.isLocallySurjective_iff_whisker_forget _ f.hom).mp hf

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
X Y : LightCondMod R
f : X ⟶ Y
inst✝ : Epi f
S : LightProfinite
p : (LightCondensed.free R).obj S.toCondensed ⟶ Y
this :
  ∀ (S : LightProfinite) (y : ((LightCondensed.forget R).obj Y).obj.obj (Opposite.op S)),
    ∃ S' φ,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
        ∃ x,
          (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op S'))) x =
            (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op φ))) y
T : LightProfinite
π : T ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
x : ((LightCondensed.forget R).obj X).obj.obj (Opposite.op T)
hx :
  (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op T))) x =
    (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op π)))
      ((coherentTopology LightProfinite).yonedaEquiv
        (((LightCondensed.freeForgetAdjunction R).homEquiv S.toCondensed Y) p))
⊢ lightProfiniteToLightCondSet.map π ≫
      ((LightCondensed.freeForgetAdjunction R).homEquiv (lightProfiniteToLightCondSet.obj S) Y) p =
    ((LightCondensed.freeForgetAdjunction R).homEquiv (lightProfiniteToLightCondSet.obj T) X)
        (((LightCondensed.freeForgetAdjunction R).homEquiv T.toCondensed X).symm
          ((coherentTopology LightProfinite).yonedaEquiv.symm x)) ≫
      (LightCondensed.forget R).map f

Tactic:
Sheaf.hom_ext_iff,

Goal state after:
R : Type u
inst✝¹ : Ring R
X Y : LightCondMod R
f : X ⟶ Y
inst✝ : Epi f
S : LightProfinite
p : (LightCondensed.free R).obj S.toCondensed ⟶ Y
this :
  ∀ (S : LightProfinite) (y : ((LightCondensed.forget R).obj Y).obj.obj (Opposite.op S)),
    ∃ S' φ,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
        ∃ x,
          (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op S'))) x =
            (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op φ))) y
T : LightProfinite
π : T ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
x : ((LightCondensed.forget R).obj X).obj.obj (Opposite.op T)
hx :
  (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op T))) x =
    (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op π)))
      ((coherentTopology LightProfinite).yonedaEquiv
        (((LightCondensed.freeForgetAdjunction R).homEquiv S.toCondensed Y) p))
⊢ (lightProfiniteToLightCondSet.map π ≫
        ((LightCondensed.freeForgetAdjunction R).homEquiv (lightProfiniteToLightCondSet.obj S) Y) p).hom =
    (((LightCondensed.freeForgetAdjunction R).homEquiv (lightProfiniteToLightCondSet.obj T) X)
          (((LightCondensed.freeForgetAdjunction R).homEquiv T.toCondensed X).symm
            ((coherentTopology LightProfinite).yonedaEquiv.symm x)) ≫
        (LightCondensed.forget R).map f).hom
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
⊢ traverse (Comp.mk ∘ map h ∘ g) = Comp.mk ∘ map (traverse h) ∘ traverse g

Tactic:
by
  ext
  exact comp_traverse _ _ _

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
a : α
b : β a
hh : b ∈ approx (⇑f) i a
⊢ b ∈ Part.fix (⇑f) a

Tactic:
rw [mem_iff f]
  exact ⟨_, hh⟩

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

Goal state before:
pp: α : Type u_1
e : Fin 2 ↪ α
⊢ (fun x ↦
        match x with
        | ⟨(a, b), h⟩ => { toFun := fun i ↦ if i = 0 then a else b, inj' := ⋯ })
      ((fun e ↦ ⟨(e 0, e 1), ⋯⟩) e) =
    e

Tactic:
ext i
    by_cases hi : i = 0
    · simp [hi]
    · simp [Fin.eq_one_of_ne_zero i hi]

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

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

Tactic:
simp [h, H₁.trans h, lookmap_congr H₂]

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

Goal state before:
pp: case swap.none.none
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
h₁ : f a = none
h₂ : f b = none
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

Tactic:
simpa [h₁, h₂] using Perm.swap _ _ _

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

Goal state before:
pp: case mp
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝ →
    dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝

Tactic:
intro h'

Goal state after:
case mp
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝
⊢ dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝
Module: Mathlib.Data.List.AList

Goal state before:
pp: case mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
⊢ dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝ →
    dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝

Tactic:
intro h'

Goal state after:
case mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
l : List (Sigma β)
h : a = a'
⊢ kerase a (kerase a' l) = kerase a' (kerase a l)

pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
l : List (Sigma β)
h : ¬a = a'
⊢ kerase a (kerase a' l) = kerase a' (kerase a l)

Tactic:
· subst a'; rfl

Goal state after:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
l : List (Sigma β)
h : ¬a = a'
⊢ kerase a (kerase a' l) = kerase a' (kerase a l)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n✝ k i n : ℕ
⊢ ↑m >>> (↑i + 1) = ↑(Nat.shiftLeft' false m n >>> (n + i + 1))

Tactic:
Nat.shiftLeft'_false,

Goal state after:
m n✝ k i n : ℕ
⊢ ↑m >>> (↑i + 1) = ↑(m <<< n >>> (n + i + 1))
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, (splitBy.loop r l a g []).flatten = g.reverse ++ a :: l
a : α
g : List α
⊢ (splitBy.loop r (b :: l) a g []).flatten = g.reverse ++ a :: b :: l

Tactic:
rw [splitBy.loop, splitByLoop_eq_append [_]]

Goal state after:
case cons
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, (splitBy.loop r l a g []).flatten = g.reverse ++ a :: l
a : α
g : List α
⊢ (match r a b with
      | true => splitBy.loop r l b (a :: g) []
      | false => [(a :: g).reverse].reverse ++ splitBy.loop r l b [] []).flatten =
    g.reverse ++ a :: b :: l
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case zero
α : Type u_1
r : α → α → Prop
h : WellFounded r
a : List α
len_a : a = []
⊢ Acc (Shortlex r) a

Tactic:
len_a

Goal state after:
case zero
α : Type u_1
r : α → α → Prop
h : WellFounded r
a : List α
len_a : a = []
⊢ Acc (Shortlex r) []
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case zero
α : Type u_1
r : α → α → Prop
h : WellFounded r
a : List α
len_a : a.length = 0
⊢ Acc (Shortlex r) a

Tactic:
rw [List.length_eq_zero_iff] at len_a
    rw [len_a]
    exact Acc.intro _ <| fun _ ylt => (not_shortlex_nil_right ylt).elim

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

Goal state before:
pp: case neg.inl
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
p_zero : ¬p = 0
small : i < p
⊢ w[i % p]? = w[i]?

Tactic:
have eq : i % p = i := mod_eq_of_lt small

Goal state after:
case neg.inl
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
p_zero : ¬p = 0
small : i < p
eq : i % p = i
⊢ w[i % p]? = w[i]?
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: α : Type u_1
r : α → α → Bool
l : List α
⊢ IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy r l)

Tactic:
by
  cases l with
  | nil => exact isChain_nil
  | cons _ _ =>
    apply isChain_getLast_head_splitByLoop _ not_mem_nil isChain_nil
    rintro _ ⟨⟩

Goal state after:
Module: Mathlib.Data.Multiset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ #(Finset.Ioc s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s) - 1

Tactic:
rw [Finset.card_Ioc_eq_card_Icc_sub_one, card_Icc]

Goal state after:
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case empty
α : Type u_1
inst✝ : Preorder α
M N X Y : Multiset α
hZ : 0 ≠ ∅
hM : M = X + Y
hN : N = X + 0
hYZ : ∀ (y : α), y ∈ Y → ∃ z, z ∈ 0 ∧ y < z
⊢ TransGen OneStep M N

Tactic:
simp at hZ

Goal state after:
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case cons.inr.refine_2
α : Type u_1
inst✝ : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    Z ≠ ∅ → M = X + Y → N = X + Z → (∀ (y : α), y ∈ Y → ∃ z, z ∈ Z ∧ y < z) → TransGen OneStep M N
M N X Y : Multiset α
hZ✝ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ (y : α), y ∈ Y → ∃ z_1, z_1 ∈ z ::ₘ Z ∧ y < z_1
hZ : Z ≠ 0
Y' : Multiset α := filter (fun x ↦ x < z) Y
y : α
hy : y ∈ Y - Y'
⊢ ∃ z, z ∈ Z ∧ y < z

Tactic:
simp only [sub_filter_eq_filter_not, mem_filter, Y'] at hy
    simpa [hy.2] using hYZ y (by simp_all)

Goal state after:
Module: Mathlib.Data.Nat.Digits.Div

Goal state before:
pp: n : ℕ
⊢ ↑n ≡ (List.map (fun n ↦ ↑n) (digits 10 n)).alternatingSum [ZMOD 11]

Tactic:
have t := zmodeq_ofDigits_digits 11 10 (-1 : ℤ) (by unfold Int.ModEq; rfl) n
  rwa [ofDigits_neg_one] at t

Goal state after:
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: case succ
A : Type u_1
inst✝ : Semiring A
k : ℕ
ih : ∀ {m : ℕ}, IsUnit ↑(m + k)! → IsUnit ↑m !
m : ℕ
hn_fac : IsUnit ↑(m + 1 + k)!
this : IsUnit (↑(m + 1) * ↑m !)
⊢ IsUnit ↑m !

Tactic:
Nat.cast_commute _ _ |>.isUnit_mul_iff

Goal state after:
case succ
A : Type u_1
inst✝ : Semiring A
k : ℕ
ih : ∀ {m : ℕ}, IsUnit ↑(m + k)! → IsUnit ↑m !
m : ℕ
hn_fac : IsUnit ↑(m + 1 + k)!
this : IsUnit ↑(m + 1) ∧ IsUnit ↑m !
⊢ IsUnit ↑m !
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
⊢ {n ∈ range (nth p (k + 1)) | p n} ⊆ insert (nth p k) ({n ∈ range (nth p k) | p n})

Tactic:
intro a ha

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
k a : ℕ
ha : a ∈ {n ∈ range (nth p (k + 1)) | p n}
⊢ a ∈ insert (nth p k) ({n ∈ range (nth p k) | p n})
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case zero
α : Type u_1
inst✝ : AddGroupWithOne α
⊢ ↑(zero + 0) = ↑zero + ↑0

Tactic:
exact (_root_.add_zero _).symm

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : AddGroupWithOne α
a✝ : PosNum
⊢ ↑(pos a✝ + 0) = ↑(pos a✝) + ↑0

Tactic:
exact (_root_.add_zero _).symm

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : AddGroupWithOne α
a✝ : PosNum
⊢ ↑(neg a✝ + 0) = ↑(neg a✝) + ↑0

Tactic:
exact (_root_.add_zero _).symm

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

Goal state before:
pp: ⊢ ↑(-0) = -↑0

Tactic:
Int.cast_neg

Goal state after:
⊢ -↑0 = -↑0